diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index 9defc43..a57899d 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -32,61 +32,66 @@ ofD     = hl Syntax "of"
 returnD = hl Syntax "return"
 
 
-export covering
+export
 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 (hang 2 $ !(prettyQtyBinds qtys (TV x)) <++> colonD
-                <//> !(prettyM s)) <++> arr
-        <//> !(under T x $ prettyM t)
+prettyBindType qtys x s arr t = do
+  var <- prettyQtyBinds qtys $ TV x
+  s   <- withPrec Outer $ prettyM s
+  t   <- withPrec Outer $ under T x $ prettyM t
+  let bind = parens (var <++> colonD <//> hang 2 s)
+  parensIfM Outer $ hang 2 $ bind <//> t
 
-export covering
+export
+prettyArm : PrettyHL a => Pretty.HasEnv m =>
+            BinderSort -> List BaseName -> Doc HL -> a -> m (Doc HL)
+prettyArm sort xs pat body = do
+  body <- withPrec Outer $ unders sort xs $ prettyM body
+  pure $ hang 2 $ sep [pat <+> dotD, body]
+
+export
 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
-  header <- sequence $ [hl TVar <$> prettyM x | x <- names]
-  body   <- unders sort names $ prettyM body
-  parensIfM Outer $ (sep (lam :: header) <+> dotD) <//> body
+             Maybe (Doc HL) -> BinderSort -> List BaseName -> a -> m (Doc HL)
+prettyLams lam sort names body = do
+  let var = case sort of T => TVar; D => DVar
+  header <- sequence $ [hlF var $ prettyM x | x <- names]
+  let header = sep $ maybe header (:: header) lam
+  parensIfM Outer =<< prettyArm sort names header body
 
-export covering
+export
 prettyApps : PrettyHL f => PrettyHL a => Pretty.HasEnv m =>
              Maybe (Doc HL) -> f -> List a -> m (Doc HL)
-prettyApps pfx fun args =
-  parensIfM App =<< withPrec Arg
-    [|prettyM fun <//> (align . sep <$> traverse prettyArg args)|]
+prettyApps pfx fun args = do
+  fun  <- withPrec Arg $ prettyM fun
+  args <- traverse (withPrec Arg . prettyArg) args
+  parensIfM App $ hang 2 $ sep $ fun :: args
  where
   prettyArg : a -> m (Doc HL)
-  prettyArg x = maybe id (\p => map (hl Delim p <+>)) pfx $ prettyM x
+  prettyArg = case pfx of
+    Nothing  => prettyM
+    Just pfx => \x => pure $ hl Delim pfx <+> !(prettyM x)
 
-export covering
+export
 prettyTuple : PrettyHL a => Pretty.HasEnv m => List a -> m (Doc HL)
 prettyTuple = map (parens . align . separate commaD) . traverse prettyM
 
-export covering
-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
+export
 prettyArms : PrettyHL a => Pretty.HasEnv m =>
              List (List BaseName, Doc HL, a) -> m (Doc HL)
-prettyArms = map (braces . align . sep) . traverse prettyArm
+prettyArms =
+  map (braces . asep) . traverse (\(xs, l, r) => prettyArm T xs l r)
 
-export covering
+export
 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 =
-  pure $ align $ sep $
-    [hsep [caseD,   !(prettyQtyBinds [pi] elim)],
-     hsep [returnD, !(prettyM r) <+> dotD, !(under T r $ prettyM ret)],
-     hsep [ofD,     !(prettyArms arms)]]
+prettyCase pi elim r ret arms = do
+  elim <- prettyQtyBinds [pi] elim
+  ret  <- prettyLams Nothing T [r] ret
+  arms <- prettyArms arms
+  pure $ asep [caseD <++> elim, returnD <++> ret, ofD <++> arms]
 
 -- [fixme] put delimiters around tags that aren't simple names
 export
@@ -105,7 +110,7 @@ parameters (showSubsts : Bool)
       prettyBindType [qty] x s !arrowD t.term
     prettyM (Lam (S x t)) =
       let GotLams {names, body, _} = getLams' x t.term Refl in
-      prettyLams T (toList names) body
+      prettyLams (Just !lamD) T (toList names) body
     prettyM (Sig s (S [x] t)) =
       prettyBindType {q} [] x s !timesD t.term
     prettyM (Pair s t) =
@@ -116,21 +121,19 @@ parameters (showSubsts : Bool)
         Prelude.toList tags
     prettyM (Tag t) =
       pure $ prettyTag t
-    prettyM (Eq (S _ (N ty)) l r) =
-      parensIfM Eq !(withPrec InEq $ pure $
-        sep [!(prettyM l) <++> !eqndD,
-             !(prettyM r) <++> colonD, !(prettyM ty)])
-    prettyM (Eq (S [i] (Y ty)) l r) =
-      parensIfM App $
-        eqD <++>
-        sep [bracks !(withPrec Outer $ pure $ hang 2 $
-               sep [hl DVar !(prettyM i) <+> dotD,
-                    !(under D i $ prettyM ty)]),
-             !(withPrec Arg $ prettyM l),
-             !(withPrec Arg $ prettyM r)]
+    prettyM (Eq (S _ (N ty)) l r) = do
+      l  <- withPrec InEq $ prettyM l
+      r  <- withPrec InEq $ prettyM r
+      ty <- withPrec InEq $ prettyM ty
+      parensIfM Eq $ asep [l <++> !eqndD, r <++> colonD, ty]
+    prettyM (Eq (S [i] (Y ty)) l r) = do
+      ty <- bracks <$> withPrec Outer (prettyLams Nothing D [i] ty)
+      l  <- withPrec Arg $ prettyM l
+      r  <- withPrec Arg $ prettyM r
+      parensIfM App $ eqD <++> asep [ty, l, r]
     prettyM (DLam (S i t)) =
       let GotDLams {names, body, _} = getDLams' i t.term Refl in
-      prettyLams D (toList names) body
+      prettyLams (Just !dlamD) D (toList names) body
     prettyM (E e) = bracks <$> prettyM e
     prettyM (CloT s th) =
       if showSubsts then
@@ -156,8 +159,7 @@ parameters (showSubsts : Bool)
       let GotArgs {fun, args, _} = getArgs' e [s] in
       prettyApps Nothing fun args
     prettyM (CasePair pi p (S [r] ret) (S [x, y] body)) = do
-      pat <- (parens . separate commaD . map (hl TVar)) <$>
-             traverse prettyM [x, y]
+      pat <- parens . separate commaD <$> traverse (hlF TVar . prettyM) [x, y]
       prettyCase pi p r ret.term [([x, y], pat, body.term)]
     prettyM (CaseEnum pi t (S [r] ret) arms) =
       prettyCase pi t r ret.term
@@ -165,10 +167,10 @@ parameters (showSubsts : Bool)
     prettyM (e :% d) =
       let GotDArgs {fun, args, _} = getDArgs' e [d] in
       prettyApps (Just "@") fun args
-    prettyM (s :# a) =
-      parensIfM Ann $ hang 2 $
-        !(withPrec AnnL $ prettyM s) <++> !annD
-          <//> !(withPrec Ann $ prettyM a)
+    prettyM (s :# a) = do
+      s <- withPrec AnnL $ prettyM s
+      a <- withPrec Ann  $ prettyM a
+      parensIfM Ann $ hang 2 $ s <++> !annD <//> a
     prettyM (CloE e th)  =
       if showSubsts then
         parensIfM SApp . hang 2 =<<