diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index 7a0089f..a980f02 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -33,16 +33,17 @@ returnD = hl Syntax "return"
 
 
 export covering
-prettyBindType : Pretty.HasEnv m =>
-                 PrettyHL q => PrettyHL a => PrettyHL b =>
+prettyBindType : PrettyHL a => PrettyHL b => PrettyHL q =>
+                 Pretty.HasEnv m =>
                  List q -> BaseName -> a -> Doc HL -> b -> m (Doc HL)
 prettyBindType qtys x s arr t =
     parensIfM Outer $ hang 2 $
-      parens !(prettyQtyBinds qtys $ TV x) <++> arr
+      parens (hang 2 $ !(prettyQtyBinds qtys (TV x)) <++> colonD
+                <//> !(prettyM s)) <++> arr
         <//> !(under T x $ prettyM t)
 
 export covering
-prettyLams : Pretty.HasEnv m => PrettyHL a =>
+prettyLams : PrettyHL a => Pretty.HasEnv m =>
              BinderSort -> List BaseName -> a -> m (Doc HL)
 prettyLams sort names body = do
   lam    <- case sort of T => lamD; D => dlamD
@@ -51,31 +52,31 @@ prettyLams sort names body = do
   parensIfM Outer $ (sep (lam :: header) <+> dotD) <//> body
 
 export covering
-prettyApps : Pretty.HasEnv m => PrettyHL f => PrettyHL a =>
+prettyApps : PrettyHL f => PrettyHL a => Pretty.HasEnv m =>
              f -> List a -> m (Doc HL)
 prettyApps fun args =
   parensIfM App =<< withPrec Arg
     [|prettyM fun <//> (align . sep <$> traverse prettyM args)|]
 
 export covering
-prettyTuple : Pretty.HasEnv m => PrettyHL a => List a -> m (Doc HL)
+prettyTuple : PrettyHL a => Pretty.HasEnv m => List a -> m (Doc HL)
 prettyTuple = map (parens . align . separate commaD) . traverse prettyM
 
 export covering
-prettyArm : Pretty.HasEnv m => PrettyHL a =>
+prettyArm : PrettyHL a => Pretty.HasEnv m =>
             (List BaseName, Doc HL, a) -> m (Doc HL)
 prettyArm (xs, pat, body) =
   pure $ hang 2 $ sep
     [pat <+> dotD, !(withPrec Outer $ unders T xs $ prettyM body)]
 
 export covering
-prettyArms : Pretty.HasEnv m => PrettyHL a =>
+prettyArms : PrettyHL a => Pretty.HasEnv m =>
              List (List BaseName, Doc HL, a) -> m (Doc HL)
 prettyArms = map (braces . align . sep) . traverse prettyArm
 
 export covering
-prettyCase : Pretty.HasEnv m =>
-             PrettyHL q => PrettyHL a => PrettyHL b => PrettyHL c =>
+prettyCase : PrettyHL a => PrettyHL b => PrettyHL c => PrettyHL q =>
+             Pretty.HasEnv m =>
              q -> a -> BaseName -> b -> List (List BaseName, Doc HL, c) ->
              m (Doc HL)
 prettyCase pi elim r ret arms =