diff --git a/exe/Main.idr b/exe/Main.idr
index 8014772..2329980 100644
--- a/exe/Main.idr
+++ b/exe/Main.idr
@@ -9,11 +9,26 @@ import System
 import Data.IORef
 import Data.SortedSet
 import Control.Eff
-import Text.PrettyPrint.Prettyprinter.Render.Terminal
 
-export
-die : Doc HL -> IO a
-die err = do putDoc $ termHL <$> err; exitFailure
+private
+Opts : LayoutOpts
+Opts = Opts 80
+
+private
+putDoc : Doc Opts -> IO ()
+putDoc = putStr . render Opts
+
+private
+die : Doc Opts -> IO a
+die err = do putDoc err; exitFailure
+
+private
+prettySig : {opts : _} -> Name -> Definition -> Eff Pretty (Doc opts)
+prettySig name def = do
+  qty  <- prettyQty def.qty.fst
+  name <- prettyFree name
+  type <- prettyTerm [<] [<] def.type
+  hangDSingle (hsep [hcat [qty, !dotD, name], !colonD]) type
 
 export
 main : IO ()
@@ -24,15 +39,11 @@ main = do
   for_ (drop 1 !getArgs) $ \file => do
     putStrLn "checking \{file}"
     Right res <- fromParserIO ["."] seen suf defs $ loadProcessFile noLoc file
-      | Left err => die $ prettyError True True err
-    for_ res $ \(name, def) => do
-      putDoc $ map termHL $ nest 2 $
-        sep [hsep [hcat [pretty0 True def.qty.fst, dotD,
-                         hl Free (pretty0 True name)],
-                   colonD],
-             prettyTerm True [<] [<] def.type]
+      | Left err => die $ runPrettyColor $ prettyError True err
+    for_ res $ \(name, def) => putDoc $ runPrettyColor $ prettySig name def
 
 -----------------------------------
+{-
 
 private
 text : PrettyOpts -> List String
@@ -73,3 +84,4 @@ join1 opts l r =
 export
 banner : PrettyOpts -> String
 banner opts = unlines $ zipWith (join1 opts) (qtuwu opts) (text opts)
+-}
diff --git a/lib/Quox/Context.idr b/lib/Quox/Context.idr
index 1b13dba..b1a9376 100644
--- a/lib/Quox/Context.idr
+++ b/lib/Quox/Context.idr
@@ -319,9 +319,27 @@ export %inline
   showPrec d = showPrec d . toSnocList
     where Show (Exists tm) where showPrec d t = showPrec d t.snd
 
-export %inline
-(forall n. PrettyHL (tm n)) => PrettyHL (Telescope tm from to) where
-  prettyM tel = separate (hl Delim ";") <$> traverse prettyM (toList tel)
+
+parameters {opts : LayoutOpts} {0 tm : Nat -> Type}
+           (nameHL : HL)
+           (pterm : forall n. BContext n -> tm n -> Eff Pretty (Doc opts))
+  private
+  prettyOne : BindName -> BContext to -> tm to -> Eff Pretty (Doc opts)
+  prettyOne x xs tm = hsep <$> sequence
+    [hl nameHL $ prettyBind' x, hl Delim $ text ":", pterm xs tm]
+
+  private
+  prettyEach : BContext to -> Telescope tm from to ->
+               Eff Pretty (Telescope' (Doc opts) from to)
+  prettyEach _         [<]       = pure [<]
+  prettyEach (xs :< x) (ts :< t) = [|prettyEach xs ts :< prettyOne x xs t|]
+
+  export
+  prettyTel : BContext to -> Telescope tm from to -> Eff Pretty (Doc opts)
+  prettyTel names tel = do
+    docs <- prettyEach names tel
+    comma <- hl Delim $ text ","
+    pure $ separateTight comma $ toList' docs
 
 
 namespace BContext
diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr
index 8420c16..312585b 100644
--- a/lib/Quox/Parser/FromParser.idr
+++ b/lib/Quox/Parser/FromParser.idr
@@ -6,6 +6,7 @@ import Quox.Parser.Parser
 import Quox.Typechecker
 
 import Data.List
+import Data.Maybe
 import Data.SnocVect
 import Quox.EffExtra
 
diff --git a/lib/Quox/Parser/FromParser/Error.idr b/lib/Quox/Parser/FromParser/Error.idr
index 6b0a885..49c6df7 100644
--- a/lib/Quox/Parser/FromParser/Error.idr
+++ b/lib/Quox/Parser/FromParser/Error.idr
@@ -29,56 +29,73 @@ data Error =
   | WrapParseError String ParseError
 
 
-parameters (unicode, showContext : Bool)
-  export
-  prettyParseError1 : String -> ParsingError _ -> Doc HL
-  prettyParseError1 file (Error msg Nothing) =
-    pretty msg
-  prettyParseError1 file (Error msg (Just bounds)) =
-    hsep [prettyLoc $ makeLoc file bounds, pretty msg]
+export
+prettyLexError : {opts : _} -> String -> LexError -> Eff Pretty (Doc opts)
+prettyLexError file (Err reason line col char) = do
+  let loc = makeLoc file (MkBounds line col line col)
+  reason <- case reason of
+    EndInput    => pure "unexpected end of input"
+    NoRuleApply => pure $ text "unrecognised character: \{show char}"
+    ComposeNotClosing (sl, sc) (el, ec) => pure $
+      hsep ["unterminated token at", !(prettyBounds (MkBounds sl sc el ec))]
+  pure $ vappend !(prettyLoc loc) reason
 
-  export
-  prettyParseError : String -> ParseError -> Doc HL
-  prettyParseError file (LexError   err) =
-    vsep ["lexical error:", nest 2 $ pretty $ show err]
-  prettyParseError file (ParseError errs) =
-    vsep $ "parse error:" ::
-           map (("-" <++>) . prettyParseError1 file) (toList errs)
+export
+prettyParseError1 : {opts : _} -> String -> ParsingError _ ->
+                    Eff Pretty (Doc opts)
+prettyParseError1 file (Error msg Nothing) =
+  pure $ text msg
+prettyParseError1 file (Error msg (Just bounds)) =
+  pure $ vappend !(prettyLoc $ makeLoc file bounds) (text msg)
 
+export
+prettyParseError : {opts : _} -> String -> ParseError ->
+                   Eff Pretty (Doc opts)
+prettyParseError file (LexError err) =
+  pure $ vsep ["lexical error:", !(prettyLexError file err)]
+prettyParseError file (ParseError errs) =
+  map (vsep . ("parse error:" ::)) $
+    traverse (map ("-" <++>) . prettyParseError1 file) (toList errs)
+
+
+parameters (showContext : Bool)
   export
-  prettyError : Error -> Doc HL
+  prettyError : {opts : _} -> Error -> Eff Pretty (Doc opts)
   prettyError (AnnotationNeeded loc ctx tm) =
-    sep [prettyLoc loc <++> "the term",
-         prettyTerm unicode ctx.dnames ctx.tnames tm,
-         "needs a type annotation"]
+    [|vappend (prettyLoc loc)
+        (hangD "type annotation needed on"
+               !(prettyTerm ctx.dnames ctx.tnames tm))|]
     -- [todo] print the original PTerm instead
 
   prettyError (DuplicatesInEnum loc tags) =
-    sep [prettyLoc loc <++> "duplicate tags in enum type",
-         braces $ fillSep $ map pretty tags]
+    [|vappend (prettyLoc loc)
+        (hangD "duplicate tags in enum type" !(prettyEnum tags))|]
 
   prettyError (DimNotInScope loc i) =
-    sep [prettyLoc loc <++> "dimension",
-         pretty0 unicode $ DV $ fromString i, "not in scope"]
+    [|vappend (prettyLoc loc)
+        (pure $ hsep ["dimension", !(hl DVar $ text i), "not in scope"])|]
 
   prettyError (TermNotInScope loc x) =
-    sep [prettyLoc loc <++> "term variable",
-         hl Free $ pretty0 unicode x, "not in scope"]
+    [|vappend (prettyLoc loc)
+        (pure $ hsep ["term variable", !(prettyFree x), "not in scope"])|]
 
-  prettyError (QtyNotGlobal loc pi) =
-    sep [prettyLoc loc <++> "quantity", pretty0 unicode pi,
-         "can't be used on a top level declaration"]
+  prettyError (QtyNotGlobal loc pi) = pure $
+    vappend !(prettyLoc loc)
+      (sep ["quantity" <++> !(prettyQty pi),
+            "can't be used on a top level declaration"])
 
-  prettyError (DimNameInTerm loc i) =
-    sep [prettyLoc loc <++> "dimension variable",
-         pretty0 unicode $ DV $ fromString i, "used in a term context"]
+  prettyError (DimNameInTerm loc i) = pure $
+    vappend !(prettyLoc loc)
+      (sep ["dimension" <++> !(hl DVar $ text i),
+            "used in a term context"])
 
   prettyError (WrapTypeError err) =
-    Typing.prettyError unicode showContext $ trimContext 2 err
+    Typing.prettyError showContext $ trimContext 2 err
 
-  prettyError (LoadError loc str err) =
-    vsep [hsep [prettyLoc loc, "couldn't load file", pretty str],
-          fromString $ show err]
+  prettyError (LoadError loc str err) = pure $
+    vsep [!(prettyLoc loc),
+          "couldn't load file" <++> text str,
+          text $ show err]
 
   prettyError (WrapParseError file err) =
     prettyParseError file err
diff --git a/lib/Quox/Pretty.idr b/lib/Quox/Pretty.idr
index b8cbac5..718899f 100644
--- a/lib/Quox/Pretty.idr
+++ b/lib/Quox/Pretty.idr
@@ -3,15 +3,14 @@ module Quox.Pretty
 import Quox.Loc
 import Quox.Name
 
-import public Text.PrettyPrint.Prettyprinter.Doc
-import Text.PrettyPrint.Prettyprinter.Render.String
-import Text.PrettyPrint.Prettyprinter.Render.Terminal
+import public Text.PrettyPrint.Bernardy
+import public Text.PrettyPrint.Bernardy.Core.Decorate
+import public Quox.EffExtra
 import public Data.String
+import Control.ANSI.SGR
+
 import Data.DPair
 import Data.SnocList
-
-import public Control.Monad.Identity
-import public Control.Monad.Reader
 import Derive.Prelude
 
 %default total
@@ -21,13 +20,17 @@ import Derive.Prelude
 
 
 public export
-record PrettyOpts where
-  constructor MakePrettyOpts
-  unicode, color : Bool
-
-public export
-defPrettyOpts : PrettyOpts
-defPrettyOpts = MakePrettyOpts {unicode = True, color = True}
+data PPrec
+= Outer
+| Times   -- "_ × _"
+| InTimes -- arguments of ×
+| AnnL    -- left of "∷"
+| Eq      -- "_ ≡ _ : _"
+| InEq    -- arguments of ≡
+  -- ...
+| App  -- term/dimension application
+| Arg  -- argument to nonfix function
+%runElab derive "PPrec" [Eq, Ord, Show]
 
 
 public export
@@ -40,254 +43,253 @@ data HL
 | Tag
 %runElab derive "HL" [Eq, Ord, Show]
 
+
 public export
-data PPrec
-= Outer
-| AnnR    -- right of "∷"
-| AnnL    -- left  of "∷"
-| Eq      -- "_ ≡ _ : _"
-| InEq    -- arguments of ≡
-| Times   -- "_ × _"
-| InTimes -- arguments of ×
-  -- ...
-| App  -- term/dimension application
-| SApp -- substitution application
-| Arg  -- argument to nonfix function
-%runElab derive "PPrec" [Eq, Ord, Show]
+data Flavor = Unicode | Ascii
+%runElab derive "Flavor" [Eq, Ord, Show]
+
+export %inline
+noHighlight : HL -> Highlight
+noHighlight _ = MkHighlight "" ""
+
+
+public export
+data EffTag = PREC | FLAVOR | HIGHLIGHT | INDENT
+
+public export
+Pretty : List (Type -> Type)
+Pretty = [StateL PREC PPrec, ReaderL FLAVOR Flavor,
+          ReaderL HIGHLIGHT (HL -> Highlight), ReaderL INDENT Nat]
+
+export %inline
+runPrettyWith : PPrec -> Flavor -> (HL -> Highlight) -> Nat ->
+                Eff Pretty a -> a
+runPrettyWith prec flavor highlight indent act =
+  extract $
+  evalStateAt PREC prec $
+  runReaderAt FLAVOR flavor $
+  runReaderAt HIGHLIGHT highlight $
+  runReaderAt INDENT indent act
 
 
 export %inline
-hl : HL -> Doc HL -> Doc HL
-hl = annotate
+toSGR : HL -> List SGR
+toSGR Delim   = []
+toSGR TVar    = [SetForeground BrightYellow]
+toSGR TVarErr = [SetForeground BrightYellow, SetStyle SingleUnderline]
+toSGR Dim     = [SetForeground BrightGreen]
+toSGR DVar    = [SetForeground BrightGreen]
+toSGR DVarErr = [SetForeground BrightGreen, SetStyle SingleUnderline]
+toSGR Qty     = [SetForeground BrightMagenta]
+toSGR Free    = [SetForeground BrightBlue]
+toSGR Syntax  = [SetForeground BrightCyan]
+toSGR Tag     = [SetForeground BrightRed]
 
 export %inline
-hl' : HL -> Doc HL -> Doc HL
-hl' h = hl h . unAnnotate
-
-export %inline
-hlF : Functor f => HL -> f (Doc HL) -> f (Doc HL)
-hlF = map . hl
-
-export %inline
-hlF' : Functor f => HL -> f (Doc HL) -> f (Doc HL)
-hlF' = map . hl'
+highlightSGR : HL -> Highlight
+highlightSGR h = MkHighlight (escapeSGR $ toSGR h) (escapeSGR [Reset])
 
 
 export %inline
-delims : Doc HL -> Doc HL -> Doc HL -> Doc HL
-delims l r doc = hl Delim l <+> doc <+> hl Delim r
+runPretty : Eff Pretty a -> a
+runPretty = runPrettyWith Outer Unicode noHighlight 2
 
 export %inline
-parens : Doc HL -> Doc HL
-parens = delims "(" ")"
+runPrettyColor : Eff Pretty a -> a
+runPrettyColor = runPrettyWith Outer Unicode highlightSGR 2
+
 
 export %inline
-bracks : Doc HL -> Doc HL
-bracks = delims "[" "]"
+hl : {opts : _} -> HL -> Doc opts -> Eff Pretty (Doc opts)
+hl h doc = asksAt HIGHLIGHT $ \f => decorate (f h) doc
 
-||| includes spaces inside the braces
-export %inline
-braces : Doc HL -> Doc HL
-braces doc = hl Delim "{" <++> nest 2 doc <++> hl Delim "}"
 
 export %inline
-parensIf : Bool -> Doc HL -> Doc HL
+indentD : {opts : _} -> Doc opts -> Eff Pretty (Doc opts)
+indentD doc = pure $ indent !(askAt INDENT) doc
+
+export %inline
+hangD : {opts : _} -> Doc opts -> Doc opts -> Eff Pretty (Doc opts)
+hangD d1 d2 = pure $ hangSep !(askAt INDENT) d1 d2
+
+export %inline
+hangDSingle : {opts : _} -> Doc opts -> Doc opts -> Eff Pretty (Doc opts)
+hangDSingle d1 d2 =
+  pure $ ifMultiline (d1 <++> d2) (vappend d1 !(indentD d2))
+
+
+export
+tightDelims : {opts : _} -> (l, r : String) -> (inner : Doc opts) ->
+              Eff Pretty (Doc opts)
+tightDelims l r inner = do
+  l <- hl Delim $ text l
+  r <- hl Delim $ text r
+  pure $ hcat [l, inner, r]
+
+export
+looseDelims : {opts : _} -> (l, r : String) -> (inner : Doc opts) ->
+              Eff Pretty (Doc opts)
+looseDelims l r inner = do
+  l <- hl Delim $ text l
+  r <- hl Delim $ text r
+  let short = hsep [l, inner, r]
+      long  = vsep [l, !(indentD inner), r]
+  pure $ ifMultiline short long
+
+export %inline
+parens : {opts : _} -> Doc opts -> Eff Pretty (Doc opts)
+parens = tightDelims "(" ")"
+
+export %inline
+bracks : {opts : _} -> Doc opts -> Eff Pretty (Doc opts)
+bracks = tightDelims "[" "]"
+
+export %inline
+braces : {opts : _} -> Doc opts -> Eff Pretty (Doc opts)
+braces = looseDelims "{" "}"
+
+export %inline
+parensIf : {opts : _} -> Bool -> Doc opts -> Eff Pretty (Doc opts)
 parensIf True  = parens
-parensIf False = id
-
-export %inline
-comma : Doc HL
-comma = hl Delim ","
+parensIf False = pure
 
 
-export %inline
-asep : List (Doc a) -> Doc a
-asep = align . sep
+||| uses hsep only if the whole list fits on one line
+export
+sepSingle : {opts : _} -> List (Doc opts) -> Doc opts
+sepSingle xs = ifMultiline (hsep xs) (vsep xs)
 
 export
-separate' : Doc a -> List (Doc a) -> List (Doc a)
-separate' s []        = []
-separate' s [x]       = [x]
-separate' s (x :: xs) = x <+> s :: separate' s xs
+fillSep : {opts : _} -> List (Doc opts) -> Doc opts
+fillSep []        = empty
+fillSep (x :: xs) = foldl (\x, y => sep [x, y]) x xs
+
+export
+exceptLast : {opts : _} -> (Doc opts -> Doc opts) ->
+             List (Doc opts) -> List (Doc opts)
+exceptLast f []        = []
+exceptLast f [x]       = [x]
+exceptLast f (x :: xs) = f x :: exceptLast f xs
+
+parameters {opts : LayoutOpts} {auto _ : Foldable t}
+  export
+  separateLoose : Doc opts -> t (Doc opts) -> Doc opts
+  separateLoose d = sep . exceptLast (<++> d) . toList
+
+  export
+  separateTight : Doc opts -> t (Doc opts) -> Doc opts
+  separateTight d = sep . exceptLast (<+> d) . toList
+
+  export
+  fillSeparateTight : Doc opts -> t (Doc opts) -> Doc opts
+  fillSeparateTight d = fillSep . exceptLast (<+> d) . toList
+
 
 export %inline
-separate : Doc a -> List (Doc a) -> Doc a
-separate s = sep . separate' s
+ifUnicode : (uni, asc : Lazy a) -> Eff Pretty a
+ifUnicode uni asc =
+  asksAt FLAVOR $ \case
+    Unicode => uni
+    Ascii   => asc
 
 export %inline
-hseparate : Doc a -> List (Doc a) -> Doc a
-hseparate s = hsep . separate' s
+parensIfM : {opts : _} -> PPrec -> Doc opts -> Eff Pretty (Doc opts)
+parensIfM d doc = parensIf (!(getAt PREC) > d) doc
 
 export %inline
-vseparate : Doc a -> List (Doc a) -> Doc a
-vseparate s = vsep . separate' s
-
-export %inline
-aseparate : Doc a -> List (Doc a) -> Doc a
-aseparate s = align . separate s
-
-
-public export
-record PrettyEnv where
-  constructor MakePrettyEnv
-  ||| names of bound dimension variables
-  dnames  : SnocList BaseName
-  ||| names of bound term variables
-  tnames  : SnocList BaseName
-  ||| use non-ascii characters for syntax
-  unicode : Bool
-  ||| surrounding precedence level
-  prec    : PPrec
-
-public export
-HasEnv : (Type -> Type) -> Type
-HasEnv = MonadReader PrettyEnv
-
-export %inline
-ifUnicode : HasEnv m => (uni, asc : Lazy a) -> m a
-ifUnicode uni asc = if (!ask).unicode then [|uni|] else [|asc|]
-
-export %inline
-parensIfM : HasEnv m => PPrec -> Doc HL -> m (Doc HL)
-parensIfM d doc = pure $ parensIf ((!ask).prec > d) doc
-
-export %inline
-withPrec : HasEnv m => PPrec -> m a -> m a
-withPrec d = local {prec := d}
-
-public export data BinderSort = T | D
-
-export %inline
-unders : HasEnv m => BinderSort -> SnocList BaseName -> m a -> m a
-unders T xs = local {prec := Outer, tnames $= (++ xs)}
-unders D xs = local {prec := Outer, dnames $= (++ xs)}
-
-export %inline
-under : HasEnv m => BinderSort -> BaseName -> m a -> m a
-under t x = unders t [< x]
-
-
-public export
-interface PrettyHL a where
-  prettyM : HasEnv m => a -> m (Doc HL)
-
-export %inline
-pretty0M : (PrettyHL a, HasEnv m) => a -> m (Doc HL)
-pretty0M = local {prec := Outer} . prettyM
-
-export %inline
-runPrettyWith : (unicode : Bool) -> (dnames, tnames : SnocList BaseName) ->
-                Reader PrettyEnv a -> a
-runPrettyWith unicode dnames tnames act =
-  let env = MakePrettyEnv {dnames, tnames, unicode, prec = Outer} in
-  runReader env act
-
-export %inline
-runPretty : (unicode : Bool) -> Reader PrettyEnv a -> a
-runPretty unicode = runPrettyWith unicode [<] [<]
-
-export %inline
-pretty0With : PrettyHL a => (unicode : Bool) ->
-             (dnames, tnames : SnocList BaseName) ->
-             a -> Doc HL
-pretty0With {unicode, dnames, tnames} =
-  runPrettyWith {unicode, dnames, tnames} . prettyM
-
-export %inline
-pretty0 : PrettyHL a => (unicode : Bool) -> a -> Doc HL
-pretty0 unicode = pretty0With unicode [<] [<]
-
-
-
-export PrettyHL BaseName where prettyM = pure . pretty . baseStr
-export PrettyHL Name     where prettyM = pure . pretty . toDots
-export PrettyHL BindName where prettyM = prettyM . name
+withPrec : PPrec -> Eff Pretty a -> Eff Pretty a
+withPrec = localAt_ PREC
 
 
 export
-nameSeq : HL -> List Name -> Doc HL
-nameSeq h = hl h . asep . map (pretty0 False)
+prettyFree : {opts : _} -> Name -> Eff Pretty (Doc opts)
+prettyFree = hl Free . text . toDots
+
+export
+prettyBind' : BindName -> Doc opts
+prettyBind' = text . baseStr . name
+
+export
+prettyTBind : {opts : _} -> BindName -> Eff Pretty (Doc opts)
+prettyTBind = hl TVar . prettyBind'
+
+export
+prettyDBind : {opts : _} -> BindName -> Eff Pretty (Doc opts)
+prettyDBind = hl DVar . prettyBind'
+
+
 
 export %inline
-prettyStr : PrettyHL a => (unicode : Bool) -> a -> String
-prettyStr unicode =
-  let layout = layoutSmart (MkLayoutOptions (AvailablePerLine 80 0.8)) in
-  renderString . layout . pretty0 unicode
+typeD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD,
+eqD, colonD, commaD, semiD, caseD, typecaseD, returnD,
+ofD, dotD, zeroD, succD, coeD, compD, undD, cstD, pipeD :
+  {opts : _} -> Eff Pretty (Doc opts)
+typeD     = hl Syntax . text =<< ifUnicode "★" "Type"
+arrowD    = hl Delim  . text =<< ifUnicode "→" "->"
+darrowD   = hl Delim  . text =<< ifUnicode "⇒" "=>"
+timesD    = hl Delim  . text =<< ifUnicode "×" "**"
+lamD      = hl Syntax . text =<< ifUnicode "λ" "fun"
+eqndD     = hl Delim  . text =<< ifUnicode "≡" "=="
+dlamD     = hl Syntax . text =<< ifUnicode "δ" "dfun"
+annD      = hl Delim  . text =<< ifUnicode "∷" "::"
+natD      = hl Syntax . text =<< ifUnicode "ℕ" "Nat"
+eqD       = hl Syntax $ text "Eq"
+colonD    = hl Delim  $ text ":"
+commaD    = hl Delim  $ text ","
+semiD     = hl Delim  $ text ";"
+caseD     = hl Syntax $ text "case"
+typecaseD = hl Syntax $ text "type-case"
+ofD       = hl Syntax $ text "of"
+returnD   = hl Syntax $ text "return"
+dotD      = hl Delim  $ text "."
+zeroD     = hl Syntax $ text "zero"
+succD     = hl Syntax $ text "succ"
+coeD      = hl Syntax $ text "coe"
+compD     = hl Syntax $ text "comp"
+undD      = hl Syntax $ text "_"
+cstD      = hl Syntax $ text "="
+pipeD     = hl Syntax $ text "|"
 
 
 export
-termHL : HL -> AnsiStyle
-termHL Delim   = neutral
-termHL TVar    = color BrightYellow
-termHL TVarErr = color BrightYellow  <+> underline
-termHL Dim     = color BrightGreen
-termHL DVar    = color BrightGreen
-termHL DVarErr = color BrightGreen   <+> underline
-termHL Qty     = color BrightMagenta
-termHL Free    = color BrightBlue
-termHL Syntax  = color BrightCyan
-termHL Tag     = color BrightRed
+prettyApp : {opts : _} -> Nat -> Doc opts -> List (Doc opts) -> Doc opts
+prettyApp ind f args =
+      hsep (f :: args)
+  <|> hsep [f, vsep args]
+  <|> vsep (f :: map (indent ind) args)
 
-export %inline
-prettyIO : PrettyOpts -> PrettyHL a => a -> IO Unit
-prettyIO opts x =
-  let reann = if opts.color then map termHL else unAnnotate in
-  Terminal.putDoc $ reann $ pretty0 opts.unicode x
-
-export %inline
-prettyIODef : PrettyHL a => a -> IO Unit
-prettyIODef = prettyIO defPrettyOpts
-
-
-infixr 6 <%%>, <%>
-export %inline
-(<%%>) : Doc a -> Doc a -> Doc a
-a <%%> b = sep [a, b]
-
-export %inline
-(<%>) : Doc a -> Doc a -> Doc a
-a <%> b = cat [a, b]
-
-
-
-||| wrapper for names that pretty-prints highlighted as a `TVar`.
-public export data TVarName = TV BaseName
-export %inline PrettyHL TVarName where prettyM (TV x) = hlF TVar $ prettyM x
-
-||| wrapper for names that pretty-prints highlighted as a `DVar`.
-public export data DVarName = DV BaseName
-export %inline PrettyHL DVarName where prettyM (DV x) = hlF DVar $ prettyM x
+export
+prettyAppD : {opts : _} -> Doc opts -> List (Doc opts) -> Eff Pretty (Doc opts)
+prettyAppD f args = pure $ prettyApp !(askAt INDENT) f args
 
 
 export
-(forall a. PrettyHL (f a)) => PrettyHL (Exists f) where
-  prettyM x = prettyM x.snd
+escapeString : String -> String
+escapeString = concatMap esc1 . unpack where
+  esc1 : Char -> String
+  esc1 '"'  = #"\""#
+  esc1 '\\' = #"\\"#
+  esc1 '\n' = #"\n"#
+  esc1 c    = singleton c
 
 export
-PrettyHL a => PrettyHL (Subset a b) where
-  prettyM x = prettyM x.fst
-
-public export
-WithPretty : Type -> Type
-WithPretty a = (PrettyHL a, a)
-
-export %inline PrettyHL (WithPretty a) where prettyM x = prettyM $ snd x
-
-export %inline
-epretty : PrettyHL a => a -> Exists WithPretty
-epretty @{p} x = Evidence a (p, x)
-
-
-public export data Lit = L (Doc HL)
-export PrettyHL Lit where prettyM (L doc) = pure doc
-
+quoteTag : String -> String
+quoteTag tag =
+  if isName tag then tag else
+  "\"" ++ escapeString tag ++ "\""
 
 export
-prettyLoc : Loc -> Doc HL
-prettyLoc (L NoLoc) = hl TVarErr "no location" <+> hl Delim ":"
-prettyLoc (L (YesLoc file (MkBounds l1 c1 l2 c2))) =
-    hcat [hl Free $ pretty file, hl Delim ":",
-          hl TVar $ pretty l1,   hl Delim ":",
-          hl DVar $ pretty c1,   hl Delim "-",
-          hl TVar $ pretty l2,   hl Delim ":",
-          hl DVar $ pretty c2,   hl Delim ":"]
+prettyBounds : {opts : _} -> Bounds -> Eff Pretty (Doc opts)
+prettyBounds (MkBounds l1 c1 l2 c2) =
+  hcat <$> sequence
+    [hl TVar $ text $ show l1, colonD,
+     hl DVar $ text $ show c1, hl Delim "-",
+     hl TVar $ text $ show l2, colonD,
+     hl DVar $ text $ show c2, colonD]
+
+export
+prettyLoc : {opts : _} -> Loc -> Eff Pretty (Doc opts)
+prettyLoc (L NoLoc) =
+  hcat <$> sequence [hl TVarErr "no location", colonD]
+prettyLoc (L (YesLoc file b)) =
+  hcat <$> sequence [hl Free $ text file, colonD, prettyBounds b]
diff --git a/lib/Quox/Syntax/Dim.idr b/lib/Quox/Syntax/Dim.idr
index 2271515..363e082 100644
--- a/lib/Quox/Syntax/Dim.idr
+++ b/lib/Quox/Syntax/Dim.idr
@@ -44,6 +44,15 @@ data Dim : Nat -> Type where
 %name Dim.Dim p, q
 %runElab deriveIndexed "Dim" [Eq, Ord, Show]
 
+
+||| `endsOr l r x p` returns `ends l r ε` if `p` is a constant ε, and
+||| `x` otherwise.
+public export
+endsOr : Lazy a -> Lazy a -> Lazy a -> Dim n -> a
+endsOr l r x (K e _) = ends l r e
+endsOr l r x (B _ _) = x
+
+
 export
 Located (Dim d) where
   (K _ loc).loc = loc
@@ -55,32 +64,13 @@ Relocatable (Dim d) where
   setLoc loc (B i _) = B i loc
 
 export
-PrettyHL DimConst where
-  prettyM = pure . hl Dim . ends "0" "1"
+prettyDimConst : {opts : _} -> DimConst -> Eff Pretty (Doc opts)
+prettyDimConst = hl Dim . text . ends "0" "1"
 
 export
-PrettyHL (Dim n) where
-  prettyM (K e _) = prettyM e
-  prettyM (B i _) = prettyVar DVar DVarErr (!ask).dnames i
-
-export
-prettyDim : (dnames : NContext d) -> Dim d -> Doc HL
-prettyDim dnames p =
-  let env = MakePrettyEnv {
-    dnames = toSnocList' dnames, tnames = [<],
-    unicode = True, prec = Outer
-  } in
-  runReader env $ prettyM p
-
-
-||| `endsOr l r x e` returns:
-||| - `l` if `p` is `K Zero`;
-||| - `r` if `p` is `K One`;
-||| - `x` otherwise.
-public export
-endsOr : Lazy a -> Lazy a -> Lazy a -> Dim n -> a
-endsOr l r x (K e _) = ends l r e
-endsOr l r x (B _ _) = x
+prettyDim : {opts : _} -> BContext d -> Dim d -> Eff Pretty (Doc opts)
+prettyDim names (K e _) = prettyDimConst e
+prettyDim names (B i _) = prettyDBind $ names !!! i
 
 
 public export %inline
@@ -93,13 +83,6 @@ DSubst : Nat -> Nat -> Type
 DSubst = Subst Dim
 
 
-export %inline
-prettyDSubst : Pretty.HasEnv m => DSubst from to -> m (Doc HL)
-prettyDSubst th =
-  prettySubstM prettyM (!ask).dnames DVar
-    !(ifUnicode "⟨" "<") !(ifUnicode "⟩" ">") th
-
-
 public export FromVar Dim where fromVarLoc = B
 
 
diff --git a/lib/Quox/Syntax/DimEq.idr b/lib/Quox/Syntax/DimEq.idr
index ddea7eb..c8079d8 100644
--- a/lib/Quox/Syntax/DimEq.idr
+++ b/lib/Quox/Syntax/DimEq.idr
@@ -229,46 +229,37 @@ setSelf (B i _)    (C eqs) with (compareP i i) | (compare i.nat i.nat)
 
 
 private
-prettyDVars : Pretty.HasEnv m => m (SnocList (Doc HL))
-prettyDVars = map (pretty0 False . DV) <$> asks dnames
+prettyDVars : {opts : _} -> BContext d -> Eff Pretty (SnocList (Doc opts))
+prettyDVars = traverse prettyDBind . toSnocList'
 
 private
-prettyCst : (PrettyHL a, PrettyHL b, Pretty.HasEnv m) => a -> b -> m (Doc HL)
-prettyCst p q = do
-  p <- pretty0M p
-  q <- pretty0M q
-  pure $ hsep [p, hl Syntax "=", q]
+prettyCst : {opts : _} -> BContext d -> Dim d -> Dim d -> Eff Pretty (Doc opts)
+prettyCst dnames p q =
+  hsep <$> sequence [prettyDim dnames p, cstD, prettyDim dnames q]
+
+private
+prettyCsts : {opts : _} -> BContext d -> DimEq' d ->
+             Eff Pretty (SnocList (Doc opts))
+prettyCsts [<] [<] = pure [<]
+prettyCsts dnames (eqs :< Nothing) = prettyCsts (tail dnames) eqs
+prettyCsts dnames (eqs :< Just q)  =
+  [|prettyCsts (tail dnames) eqs :< prettyCst dnames (BV 0 noLoc) (weakD 1 q)|]
 
 export
-PrettyHL (DimEq' d) where
-  prettyM eqs {m} = do
-    vars <- prettyDVars
-    eqs  <- go eqs
-    let prec = if length vars <= 1 && null eqs then Arg else Outer
-    parensIfM prec $ align $ fillSep $ punctuate comma $ toList $ vars ++ eqs
-  where
-    tail : SnocList a -> SnocList a
-    tail [<] = [<]
-    tail (xs :< _) = xs
-
-    go : DimEq' d' -> m (SnocList (Doc HL))
-    go [<]              = pure [<]
-    go (eqs :< Nothing) = local {dnames $= tail} $ go eqs
-    go (eqs :< Just p)  = do
-      eq  <- prettyCst (BV {d = 1} 0 noLoc) (weakD 1 p)
-      eqs <- local {dnames $= tail} $ go eqs
-      pure $ eqs :< eq
+prettyDimEq' : {opts : _} -> BContext d -> DimEq' d -> Eff Pretty (Doc opts)
+prettyDimEq' dnames eqs = do
+  vars <- prettyDVars dnames
+  eqs  <- prettyCsts dnames eqs
+  let prec = if length vars <= 1 && null eqs then Arg else Outer
+  parensIfM prec $ fillSeparateTight !commaD $ toList vars ++ toList eqs
 
 export
-PrettyHL (DimEq d) where
-  prettyM ZeroIsOne = parensIfM Outer $
-    align $ fillSep $ punctuate comma $ toList $
-    !prettyDVars :< !(prettyCst Zero One)
-  prettyM (C eqs)   = prettyM eqs
-
-export
-prettyDimEq : BContext d -> DimEq d -> Doc HL
-prettyDimEq ds = pretty0With False (toNames ds) [<]
+prettyDimEq : {opts : _} -> BContext d -> DimEq d -> Eff Pretty (Doc opts)
+prettyDimEq dnames ZeroIsOne = do
+  vars <- prettyDVars dnames
+  cst  <- prettyCst [<] (K Zero noLoc) (K One noLoc)
+  pure $ separateTight !commaD $ vars :< cst
+prettyDimEq dnames (C eqs) = prettyDimEq' dnames eqs
 
 
 public export
diff --git a/lib/Quox/Syntax/Qty.idr b/lib/Quox/Syntax/Qty.idr
index 86672b6..1aa0ba0 100644
--- a/lib/Quox/Syntax/Qty.idr
+++ b/lib/Quox/Syntax/Qty.idr
@@ -20,35 +20,20 @@ import Derive.Prelude
 ||| - ω (or #): don't care. an ω variable *can* also be used 0/1 time
 public export
 data Qty = Zero | One | Any
-%name Qty.Qty pi, rh
-
 %runElab derive "Qty" [Eq, Ord, Show]
+%name Qty.Qty pi, rh
 
 
 export
-PrettyHL Qty where
-  prettyM pi = hl Qty <$>
-    case pi of
-      Zero => pure "0"
-      One  => pure "1"
-      Any  => ifUnicode "ω" "#"
+prettyQty : {opts : _} -> Qty -> Eff Pretty (Doc opts)
+prettyQty Zero = hl Qty $ text "0"
+prettyQty One  = hl Qty $ text "1"
+prettyQty Any  = hl Qty =<< ifUnicode (text "ω") (text "#")
 
 ||| prints in a form that can be a suffix of "case"
 public export
-prettySuffix : Pretty.HasEnv m => Qty -> m (Doc HL)
-prettySuffix = prettyM
-
-public export
-DecEq Qty where
-  decEq Zero Zero = Yes Refl
-  decEq Zero One  = No $ \case _ impossible
-  decEq Zero Any  = No $ \case _ impossible
-  decEq One  Zero = No $ \case _ impossible
-  decEq One  One  = Yes Refl
-  decEq One  Any  = No $ \case _ impossible
-  decEq Any  Zero = No $ \case _ impossible
-  decEq Any  One  = No $ \case _ impossible
-  decEq Any  Any  = Yes Refl
+prettySuffix : {opts : _} -> Qty -> Eff Pretty (Doc opts)
+prettySuffix = prettyQty
 
 
 ||| e.g. if in the expression `(s, t)`, the variable `x` is
diff --git a/lib/Quox/Syntax/Shift.idr b/lib/Quox/Syntax/Shift.idr
index 79a7e2b..ecfe476 100644
--- a/lib/Quox/Syntax/Shift.idr
+++ b/lib/Quox/Syntax/Shift.idr
@@ -1,7 +1,6 @@
 module Quox.Syntax.Shift
 
 import public Quox.Syntax.Var
-import Quox.Pretty
 
 import Data.Nat
 import Data.So
@@ -206,24 +205,6 @@ compViaNatCorrect by (SS bz) =
 %transform "Shift.(.)" Shift.(.) = compViaNat
 
 
-||| `prettyShift bnd unicode prec by` pretty-prints the shift `by`, with the
-||| following arguments:
-|||
-||| * `by : Shift from to`
-||| * `bnd : HL` is the highlight used for bound variables of this kind
-||| * `unicode : Bool` is whether to use unicode characters in the output
-||| * `prec : PPrec` is the surrounding precedence level
-export
-prettyShift : Pretty.HasEnv m => (bnd : HL) -> Shift from to -> m (Doc HL)
-prettyShift bnd by =
-  parensIfM Outer $ hsep $
-    [hl bnd   !(ifUnicode "𝑖"  "i"), hl Delim !(ifUnicode "≔" ":="),
-     hl bnd $ !(ifUnicode "𝑖+" "i+") <+> pretty by.nat]
-
-||| prints using the `TVar` highlight for variables
-export PrettyHL (Shift from to) where prettyM = prettyShift TVar
-
-
 infixl 8 //
 public export
 interface CanShift f where
diff --git a/lib/Quox/Syntax/Subst.idr b/lib/Quox/Syntax/Subst.idr
index b152664..a14c232 100644
--- a/lib/Quox/Syntax/Subst.idr
+++ b/lib/Quox/Syntax/Subst.idr
@@ -3,7 +3,6 @@ module Quox.Syntax.Subst
 import public Quox.Syntax.Shift
 import Quox.Syntax.Var
 import Quox.Name
-import Quox.Pretty
 
 import Data.Nat
 import Data.List
@@ -54,11 +53,6 @@ getLoc (Shift by) i      loc = fromVarLoc (shift by i) loc
 getLoc (t ::: th) VZ     _   = t
 getLoc (t ::: th) (VS i) loc = getLoc th i loc
 
--- infixl 8 !!
--- public export
--- (!!) : FromVar term => Subst term from to -> Var from -> term to
--- th !! i = getLoc th i noLoc
-
 
 public export
 CanSubstSelf Var where
@@ -130,40 +124,6 @@ one : f n -> Subst f (S n) n
 one x = fromSnocVect [< x]
 
 
-||| `prettySubst pr names bnd op cl th` pretty-prints the substitution `th`,
-||| with the following arguments:
-|||
-||| * `th : Subst f from to`
-||| * `pr : f to -> m (Doc HL)` prints a single element
-||| * `names : List Name` is a list of known bound var names
-||| * `bnd : HL` is the highlight to use for bound variables being subsituted
-||| * `op, cl : Doc HL` are the opening and closing brackets
-export
-prettySubstM : Pretty.HasEnv m =>
-               (pr : f to -> m (Doc HL)) ->
-               (names : SnocList BaseName) -> (bnd : HL) -> (op, cl : Doc HL) ->
-               Subst f from to -> m (Doc HL)
-prettySubstM pr names bnd op cl th =
-  encloseSep (hl Delim op) (hl Delim cl) (hl Delim "; ") <$>
-    withPrec Outer (go 0 th)
- where
-  go1 : Nat -> f to -> m (Doc HL)
-  go1 i t = pure $ hang 2 $ sep
-    [hsep [!(prettyVar' bnd bnd names i),
-           hl Delim !(ifUnicode "≔" ":=")],
-     !(pr t)]
-
-  go : forall from. Nat -> Subst f from to -> m (List (Doc HL))
-  go _ (Shift SZ) = pure []
-  go _ (Shift by) = [|pure (prettyShift bnd by)|]
-  go i (t ::: th) = [|go1 i t :: go (S i) th|]
-
-||| prints with [square brackets] and the `TVar` highlight for variables
-export
-PrettyHL (f to) => PrettyHL (Subst f from to) where
-  prettyM th = prettySubstM prettyM (!ask).tnames TVar "[" "]" th
-
-
 ||| whether two substitutions with the same codomain have the same shape
 ||| (the same number of terms and the same shift at the end). if so, they
 ||| also have the same domain
diff --git a/lib/Quox/Syntax/Term.idr b/lib/Quox/Syntax/Term.idr
index b0dddec..2ac69a4 100644
--- a/lib/Quox/Syntax/Term.idr
+++ b/lib/Quox/Syntax/Term.idr
@@ -1,7 +1,6 @@
 module Quox.Syntax.Term
 
 import public Quox.Syntax.Term.Base
-import public Quox.Syntax.Term.Split
 import public Quox.Syntax.Term.Subst
 import public Quox.Syntax.Term.Pretty
 import public Quox.Syntax.Term.Tighten
diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index 7bf10d6..d24a854 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -1,423 +1,519 @@
 module Quox.Syntax.Term.Pretty
 
 import Quox.Syntax.Term.Base
-import Quox.Syntax.Term.Split
 import Quox.Syntax.Term.Subst
 import Quox.Context
 import Quox.Pretty
 
 import Data.Vect
+import Derive.Prelude
 
 %default total
-
-
-export %inline
-typeD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD :
-  Pretty.HasEnv m => m (Doc HL)
-typeD   = hlF Syntax $ ifUnicode "★" "Type"
-arrowD  = hlF Delim  $ ifUnicode "→" "->"
-darrowD = hlF Delim  $ ifUnicode "⇒" "=>"
-timesD  = hlF Delim  $ ifUnicode "×" "**"
-lamD    = hlF Syntax $ ifUnicode "λ" "fun"
-eqndD   = hlF Delim  $ ifUnicode "≡" "=="
-dlamD   = hlF Syntax $ ifUnicode "δ" "dfun"
-annD    = hlF Delim  $ ifUnicode "∷" "::"
-natD    = hlF Syntax $ ifUnicode "ℕ" "Nat"
-
-export %inline
-eqD, colonD, commaD, semiD, caseD, typecaseD, returnD,
-ofD, dotD, zeroD, succD, coeD, compD : Doc HL
-eqD       = hl Syntax "Eq"
-colonD    = hl Delim  ":"
-commaD    = hl Delim  ","
-semiD     = hl Delim  ";"
-caseD     = hl Syntax "case"
-typecaseD = hl Syntax "type-case"
-ofD       = hl Syntax "of"
-returnD   = hl Syntax "return"
-dotD      = hl Delim "."
-zeroD     = hl Syntax "zero"
-succD     = hl Syntax "succ"
-coeD      = hl Syntax "coe"
-compD     = hl Syntax "compD"
+%language ElabReflection
 
 
 export
-prettyUnivSuffix : Pretty.HasEnv m => Universe -> m (Doc HL)
-prettyUnivSuffix l =
-  ifUnicode (pretty $ pack $ map sub $ unpack $ show l) (pretty l)
- where
+prettyUniverse : {opts : _} -> Universe -> Eff Pretty (Doc opts)
+prettyUniverse = hl Syntax . text . show
+
+
+export
+prettyTerm : {opts : _} -> BContext d -> BContext n -> Term d n ->
+             Eff Pretty (Doc opts)
+
+export
+prettyElim : {opts : _} -> BContext d -> BContext n -> Elim d n ->
+             Eff Pretty (Doc opts)
+
+private
+BTelescope : Nat -> Nat -> Type
+BTelescope = Telescope' BindName
+
+
+private
+subscript : String -> String
+subscript = pack . map sub . unpack where
   sub : Char -> Char
   sub c = case c of
     '0' => '₀'; '1' => '₁'; '2' => '₂'; '3' => '₃'; '4' => '₄'
     '5' => '₅'; '6' => '₆'; '7' => '₇'; '8' => '₈'; '9' => '₉'; _ => c
 
-export
-prettyUniverse : Universe -> Doc HL
-prettyUniverse = hl Syntax . pretty
-
-
-public export
-data WithQty a = MkWithQty Qty a
-
-export
-PrettyHL a => PrettyHL (WithQty a) where
-  prettyM (MkWithQty q x) = do
-    q <- pretty0M q
-    x <- withPrec Arg $ prettyM x
-    pure $ hcat [q, dotD, x]
-
-
-public export
-data Binder a = MkBinder BaseName a
-
-export
-PrettyHL a => PrettyHL (Binder a) where
-  prettyM (MkBinder x ty) = do
-    x  <- pretty0M $ TV x
-    ty <- align <$> pretty0M ty
-    pure $ parens $ sep [hsep [x, colonD], ty]
-
-
-export
-prettyBindType : PrettyHL a => PrettyHL b =>
-                 Pretty.HasEnv m =>
-                 Maybe Qty -> BindName -> a -> Doc HL -> b -> m (Doc HL)
-prettyBindType q (BN x _) s arr t = do
-  bind <- case q of
-    Nothing => pretty0M $ MkBinder x s
-    Just q  => pretty0M $ MkWithQty q $ MkBinder x s
-  t <- withPrec AnnR $ under T x $ prettyM t
-  parensIfM AnnR $ hang 2 $ bind <++> arr <%%> t
-
-export
-prettyArm : PrettyHL a => Pretty.HasEnv m =>
-            BinderSort -> SnocList BindName -> Doc HL -> a -> m (Doc HL)
-prettyArm sort xs pat body = do
-  let xs = map name xs
-  body <- withPrec Outer $ unders sort xs $ prettyM body
-  pure $ hang 2 $ sep [pat <++> !darrowD, body]
-
-export
-prettyLams : PrettyHL a => Pretty.HasEnv m =>
-             Maybe (Doc HL) -> BinderSort -> SnocList BindName -> 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 <- toList names]
-  let header = sep $ maybe header (:: header) lam
-  parensIfM Outer =<< prettyArm sort names header body
-
-
-public export
-data TypeLine a = MkTypeLine BindName a
-
-export
-PrettyHL a => PrettyHL (TypeLine a) where
-  prettyM (MkTypeLine i ty) =
-    if i.name == Unused then
-      bracks <$> pretty0M ty
-    else
-      map bracks $ withPrec Outer $ prettyLams Nothing D [< i] ty
-
-
-export
-prettyApps' : PrettyHL f => PrettyHL a => Pretty.HasEnv m =>
-              f -> List (Maybe (Doc HL), a) -> m (Doc HL)
-prettyApps' fun args = do
-  fun  <- withPrec App $ prettyM fun
-  args <- traverse prettyArg args
-  parensIfM App $ hang 2 $ sep $ fun :: args
- where
-  prettyArg : (Maybe (Doc HL), a) -> m (Doc HL)
-  prettyArg (Nothing,  arg) = withPrec Arg (prettyM arg)
-  prettyArg (Just pfx, arg) = (hl Delim pfx <+>) <$> withPrec Arg (prettyM arg)
-
-export
-prettyApps : PrettyHL f => PrettyHL a => Pretty.HasEnv m =>
-             Maybe (Doc HL) -> f -> List a -> m (Doc HL)
-prettyApps pfx f args = prettyApps' f (map (pfx,) args)
-
-export
-prettyTuple : PrettyHL a => Pretty.HasEnv m => List a -> m (Doc HL)
-prettyTuple = map (parens . align . separate commaD) . traverse prettyM
-
-export
-prettyArms : PrettyHL a => Pretty.HasEnv m =>
-             BinderSort -> List (SnocList BindName, Doc HL, a) -> m (Doc HL)
-prettyArms s =
-  map (braces . aseparate semiD) .
-  traverse (\(xs, l, r) => prettyArm s xs l r)
-
-export
-prettyCase' : (PrettyHL a, PrettyHL b, PrettyHL c, Pretty.HasEnv m) =>
-              Doc HL -> a -> BindName -> b ->
-              List (SnocList BindName, Doc HL, c) ->
-              m (Doc HL)
-prettyCase' intro elim r ret arms = do
-  elim  <- pretty0M elim
-  ret   <- case r.name of
-    Unused => under T r.name $ pretty0M ret
-    _      => prettyLams Nothing T [< r] ret
-  arms  <- prettyArms T arms
-  pure $ asep [intro <++> elim, returnD <++> ret, ofD <++> arms]
-
-export
-prettyCase : (PrettyHL a, PrettyHL b, PrettyHL c, Pretty.HasEnv m) =>
-             Qty -> a -> BindName -> b ->
-             List (SnocList BindName, Doc HL, c) ->
-             m (Doc HL)
-prettyCase pi elim r ret arms = do
-  caseq <- (caseD <+>) <$> prettySuffix pi
-  prettyCase' caseq elim r ret arms
-
-export
-escapeString : String -> String
-escapeString = concatMap esc1 . unpack where
-  esc1 : Char -> String
-  esc1 '"'  = #"\""#
-  esc1 '\\' = #"\\"#
-  esc1 '\n' = #"\n"#
-  esc1 c    = singleton c
-
-export
-quoteTag : TagVal -> Doc HL
-quoteTag tag =
-  if isName tag then fromString tag else
-  hcat ["\"", fromString $ escapeString tag, "\""]
-
-export
-prettyTag : TagVal -> Doc HL
-prettyTag t = hl Tag $ "'" <+> quoteTag t
-
-export
-prettyTagBare : TagVal -> Doc HL
-prettyTagBare t = hl Tag $ quoteTag t
-
-export
-prettyBoxVal : PrettyHL a => Pretty.HasEnv m => a -> m (Doc HL)
-prettyBoxVal val = bracks <$> pretty0M val
-
-export
-prettyCompPat : Pretty.HasEnv m => DimConst -> BindName -> m (Doc HL)
-prettyCompPat e j = hsep <$> sequence [pretty0M e, pretty0M $ DV j.name]
-
-export
-toNatLit : Term d n -> Maybe Nat
-toNatLit (Zero _)   = Just 0
-toNatLit (Succ n _) = [|S $ toNatLit n|]
-toNatLit _          = Nothing
 
 private
-eterm : Term d n -> Exists (Term d)
-eterm = Evidence n
+PiBind : Nat -> Nat -> Type
+PiBind d n = (Qty, BindName, Term d n)
+
+private
+pbname : PiBind d n -> BindName
+pbname (_, x, _) = x
+
+private
+record SplitPi d n where
+  constructor MkSplitPi
+  binds : Telescope (PiBind d) n inner
+  cod   : Term d inner
+
+private
+splitPi : Telescope (PiBind d) n inner -> Term d inner -> SplitPi d n
+splitPi binds (Pi qty arg res _) =
+  splitPi (binds :< (qty, res.name, arg)) $
+    assert_smaller res $ pushSubsts' res.term
+splitPi binds cod = MkSplitPi {binds, cod}
+
+private
+prettyPiBind1 : {opts : _} ->
+                Qty -> BindName -> BContext d -> BContext n -> Term d n ->
+                Eff Pretty (Doc opts)
+prettyPiBind1 pi (BN Unused _) dnames tnames s =
+  hcat <$> sequence
+    [prettyQty pi, dotD,
+     withPrec Arg $ assert_total prettyTerm dnames tnames s]
+prettyPiBind1 pi x dnames tnames s = hcat <$> sequence
+  [prettyQty pi, dotD,
+   hl Delim $ text "(",
+   hsep <$> sequence
+     [prettyTBind x, hl Delim $ text ":",
+      withPrec Outer $ assert_total prettyTerm dnames tnames s],
+   hl Delim $ text ")"]
+
+private
+prettyPiBinds : {opts : _} ->
+                BContext d -> BContext n ->
+                Telescope (PiBind d) n inner ->
+                Eff Pretty (SnocList (Doc opts))
+prettyPiBinds _ _ [<] = pure [<]
+prettyPiBinds dnames tnames (binds :< (q, x, t)) =
+  let tnames' = tnames . map pbname binds in
+  [|prettyPiBinds dnames tnames binds :<
+    prettyPiBind1 q x dnames tnames' t|]
 
 
-parameters (showSubsts : Bool)
- mutual
-  export covering
-  [TermSubst] PrettyHL (Term d n) using ElimSubst
-  where
-    prettyM (TYPE l _) =
-      pure $ !typeD <+> hl Syntax !(prettyUnivSuffix l)
+private
+SigBind : Nat -> Nat -> Type
+SigBind d n = (BindName, Term d n)
 
-    prettyM (Pi qty s (S _ (N t)) _) = do
-      dom <- pretty0M $ MkWithQty qty s
-      cod <- withPrec AnnR $ prettyM t
-      parensIfM AnnR $ asep [dom <++> !arrowD, cod]
+private
+record SplitSig d n where
+  constructor MkSplitSig
+  binds : Telescope (SigBind d) n inner
+  last  : Term d inner
 
-    prettyM (Pi qty s (S [< x] (Y t)) _) =
-      prettyBindType (Just qty) x s !arrowD t
+private
+splitSig : Telescope (SigBind d) n inner -> Term d inner -> SplitSig d n
+splitSig binds (Sig fst snd _) =
+  splitSig (binds :< (snd.name, fst)) $
+    assert_smaller snd $ pushSubsts' snd.term
+splitSig binds last = MkSplitSig {binds, last}
 
-    prettyM (Lam (S x t) _) =
-      let GotLams {names, body, _} = getLams' x t.term Refl in
-      prettyLams (Just !lamD) T (toSnocList' names) body
+private
+prettySigBind1 : {opts : _} ->
+                 BindName -> BContext d -> BContext n -> Term d n ->
+                 Eff Pretty (Doc opts)
+prettySigBind1 (BN Unused _) dnames tnames s =
+  withPrec InTimes $ assert_total prettyTerm dnames tnames s
+prettySigBind1 x dnames tnames s = hcat <$> sequence
+  [hl Delim $ text "(",
+   hsep <$> sequence
+     [prettyTBind x, hl Delim $ text ":",
+      withPrec Outer $ assert_total prettyTerm dnames tnames s],
+   hl Delim $ text ")"]
 
-    prettyM (Sig s (S _ (N t)) _) = do
-      s <- withPrec InTimes $ prettyM s
-      t <- withPrec Times   $ prettyM t
-      parensIfM Times $ asep [s <++> !timesD, t]
-
-    prettyM (Sig s (S [< x] (Y t)) _) =
-      prettyBindType Nothing x s !timesD t
-
-    prettyM (Pair s t _) =
-      let GotPairs {init, last, _} = getPairs' [< s] t in
-      prettyTuple $ toList $ init :< last
-
-    prettyM (Enum tags _) =
-      pure $ delims "{" "}" . aseparate comma $ map prettyTagBare $
-        Prelude.toList tags
-
-    prettyM (Tag t _) =
-      pure $ prettyTag t
-
-    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
-      prettyApps Nothing (L eqD)
-        [epretty $ MkTypeLine i ty, epretty l, epretty r]
-
-    prettyM (DLam (S i t) _) =
-      let GotDLams {names, body, _} = getDLams' i t.term Refl in
-      prettyLams (Just !dlamD) D (toSnocList' names) body
-
-    prettyM (Nat _) = natD
-
-    prettyM (Zero _) = pure $ hl Syntax "0"
-
-    prettyM (Succ n _) =
-      case toNatLit n of
-        Just n  => pure $ hl Syntax $ pretty $ S n
-        Nothing => prettyApps Nothing (L succD) [n]
-
-    prettyM (BOX pi ty _) = do
-      pi <- pretty0M pi
-      ty <- pretty0M ty
-      pure $ bracks $ hcat [pi, dotD, align ty]
-
-    prettyM (Box val _) = prettyBoxVal val
-
-    prettyM (E e) = prettyM e
-
-    prettyM (CloT (Sub s th)) =
-      if showSubsts then
-        parensIfM SApp . hang 2 =<<
-          [|withPrec SApp (prettyM s) <%> prettyTSubst th|]
-      else
-        prettyM $ pushSubstsWith' id th s
-
-    prettyM (DCloT (Sub s th)) =
-      if showSubsts then
-        parensIfM SApp . hang 2 =<<
-          [|withPrec SApp (prettyM s) <%> prettyDSubst th|]
-      else
-        prettyM $ pushSubstsWith' th id s
-
-  export covering
-  [ElimSubst] PrettyHL (Elim d n) using TermSubst
-  where
-    prettyM (F x _) =
-      hl' Free <$> prettyM x
-
-    prettyM (B i _) =
-      prettyVar TVar TVarErr (!ask).tnames i
-
-    prettyM (App e s _) =
-      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 <$> 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
-        [([<], prettyTag t, b) | (t, b) <- SortedMap.toList arms]
-
-    prettyM (CaseNat pi pi' nat (S [< r] ret) zer (S [< s, ih] suc) _) =
-      prettyCase pi nat r ret.term
-        [([<],       zeroD,    eterm zer),
-         ([< s, ih], !succPat, eterm suc.term)]
-    where
-      succPat : m (Doc HL)
-      succPat = case (ih, pi') of
-        (BN Unused _, Zero) => pure $ succD <++> !(pretty0M s)
-        _ => pure $ asep [succD <++> !(pretty0M s) <+> comma,
-                          !(pretty0M $ MkWithQty pi' ih)]
-
-    prettyM (CaseBox pi box (S [< r] ret) (S [< u] body) _) =
-      prettyCase pi box r ret.term
-        [([< u], !(prettyBoxVal $ TV u.name), body.term)]
-
-    prettyM (DApp e d _) =
-      let GotDArgs {fun, args, _} = getDArgs' e [d] in
-      prettyApps (Just "@") fun args
-
-    prettyM (Ann s a _) = do
-      s <- withPrec AnnL $ prettyM s
-      a <- withPrec AnnR $ prettyM a
-      parensIfM AnnR $ hang 2 $ s <++> !annD <%%> a
-
-    prettyM (Coe (S [< i] ty) p q val _) =
-      let ty = case ty of
-            Y ty => epretty $ MkTypeLine i ty
-            N ty => epretty ty
-      in
-      prettyApps' (L coeD)
-        [(Nothing,  ty),
-         (Just "@", epretty p),
-         (Just "@", epretty q),
-         (Nothing,  epretty val)]
-
-    prettyM (Comp ty p q val r (S [< z] zero) (S [< o] one) _) = do
-      apps <- prettyApps' (L compD)
-        [(Nothing,  epretty $ MkTypeLine (BN Unused noLoc) ty),
-         (Just "@", epretty p),
-         (Just "@", epretty q),
-         (Nothing,  epretty val),
-         (Just "@", epretty r)]
-      arms <- prettyArms D
-        [([< z], !(prettyCompPat Zero z), zero.term),
-         ([< o], !(prettyCompPat One  o), one.term)]
-      pure $ apps <++> arms
-
-    prettyM (TypeCase ty ret arms def _) = do
-      arms <- traverse fromArm (toList arms)
-      prettyCase' typecaseD ty (BN Unused noLoc) ret $
-        arms ++ [([<], hl Syntax "_", eterm def)]
-    where
-      v : BindName -> Doc HL
-      v = pretty0 True . TV . name
-
-      tyCasePat : (k : TyConKind) -> BContext (arity k) -> m (Doc HL)
-      tyCasePat KTYPE [<] = typeD
-      tyCasePat KPi   [< a, b] = pure $ parens $ hsep [v a, !arrowD, v b]
-      tyCasePat KSig  [< a, b] = pure $ parens $ hsep [v a, !arrowD, v b]
-      tyCasePat KEnum [<]   = pure $ hl Syntax "{}"
-      tyCasePat KNat  [<]   = natD
-      tyCasePat KBOX  [< a] = pure $ bracks $ v a
-      tyCasePat KEq   vars  =
-        prettyApps Nothing (L eqD) $ map (TV . name) $ toList' vars
-
-      fromArm : TypeCaseArm d n ->
-                m (SnocList BindName, Doc HL, Exists (Term d))
-      fromArm (k ** S ns t) =
-        pure (toSnocList' ns, !(tyCasePat k ns), eterm t.term)
-
-    prettyM (CloE (Sub e th)) =
-      if showSubsts then
-        parensIfM SApp . hang 2 =<<
-          [|withPrec SApp (prettyM e) <%> prettyTSubst th|]
-      else
-        prettyM $ pushSubstsWith' id th e
-
-    prettyM (DCloE (Sub e th)) =
-      if showSubsts then
-        parensIfM SApp . hang 2 =<<
-          [|withPrec SApp (prettyM e) <%> prettyDSubst th|]
-      else
-        prettyM $ pushSubstsWith' th id e
-
-  export covering
-  prettyTSubst : Pretty.HasEnv m => TSubst d from to -> m (Doc HL)
-  prettyTSubst s =
-    prettySubstM (prettyM @{ElimSubst}) (!ask).tnames TVar "[" "]" s
-
-export covering %inline
-PrettyHL (Term d n) where prettyM = prettyM @{TermSubst False}
-
-export covering %inline
-PrettyHL (Elim d n) where prettyM = prettyM @{ElimSubst False}
+private
+prettySigBinds : {opts : _} ->
+                 BContext d -> BContext n ->
+                 Telescope (SigBind d) n inner ->
+                 Eff Pretty (SnocList (Doc opts))
+prettySigBinds _ _ [<] = pure [<]
+prettySigBinds dnames tnames (binds :< (x, t)) =
+  let tnames' = tnames . map fst binds in
+  [|prettySigBinds dnames tnames binds :<
+    prettySigBind1 x dnames tnames' t|]
 
 
-export covering
-prettyTerm : (unicode : Bool) ->
-             (dnames : BContext d) -> (tnames : BContext n) ->
-             Term d n -> Doc HL
-prettyTerm unicode dnames tnames term =
-  pretty0With unicode (toNames dnames) (toNames tnames) term
+private
+prettyTypeLine : {opts : _} ->
+                 BContext d -> BContext n ->
+                 DScopeTerm d n ->
+                 Eff Pretty (Doc opts)
+prettyTypeLine dnames tnames (S _ (N body)) =
+  bracks =<< withPrec Outer (prettyTerm dnames tnames body)
+prettyTypeLine dnames tnames (S [< i] (Y body)) =
+  bracks =<< do
+    i'  <- prettyDBind i
+    ty' <- withPrec Outer $ prettyTerm (dnames :< i) tnames body
+    pure $ sep [hsep [i', !darrowD], ty']
+
+
+private
+data NameSort = T | D
+%runElab derive "NameSort" [Eq]
+
+private
+NameChunks : Type
+NameChunks = SnocList (NameSort, SnocList BindName)
+
+private
+record SplitLams d n where
+  constructor MkSplitLams
+  dnames : BTelescope d dinner
+  tnames : BTelescope n ninner
+  chunks : NameChunks
+  body   : Term dinner ninner
+
+private
+splitLams : Term d n -> SplitLams d n
+splitLams s = go [<] [<] [<] (pushSubsts' s)
+where
+  push : NameSort -> BindName -> NameChunks -> NameChunks
+  push s y [<] = [< (s, [< y])]
+  push s y (xss :< (s', xs)) =
+    if s == s' then xss :< (s', xs :< y)
+    else xss :< (s', xs) :< (s, [< y])
+
+  go : BTelescope d dinner -> BTelescope n ninner ->
+       SnocList (NameSort, SnocList BindName) ->
+       Term dinner ninner -> SplitLams d n
+  go dnames tnames chunks (Lam b _) =
+    go dnames (tnames :< b.name) (push T b.name chunks) $
+       assert_smaller b $ pushSubsts' b.term
+  go dnames tnames chunks (DLam b _) =
+    go (dnames :< b.name) tnames (push D b.name chunks) $
+       assert_smaller b $ pushSubsts' b.term
+  go dnames tnames chunks s =
+    MkSplitLams dnames tnames chunks s
+
+
+private
+splitTuple : SnocList (Term d n) -> Term d n -> SnocList (Term d n)
+splitTuple ss p@(Pair t1 t2 _) =
+  splitTuple (ss :< t1) $ assert_smaller p $ pushSubsts' t2
+splitTuple ss t = ss :< t
+
+
+private
+prettyTArg : {opts : _} -> BContext d -> BContext n ->
+             Term d n -> Eff Pretty (Doc opts)
+prettyTArg dnames tnames s =
+  withPrec Arg $ assert_total prettyTerm dnames tnames s
+
+private
+prettyDArg : {opts : _} -> BContext d -> Dim d -> Eff Pretty (Doc opts)
+prettyDArg dnames p =
+  map (text "@" <+>) $ withPrec Arg $ prettyDim dnames p
+
+private
+splitApps : Elim d n -> (Elim d n, List (Either (Dim d) (Term d n)))
+splitApps e = go [] (pushSubsts' e)
+where
+  go : List (Either (Dim d) (Term d n)) -> Elim d n ->
+       (Elim d n, List (Either (Dim d) (Term d n)))
+  go xs e@(App  f s _) =
+    go (Right s :: xs) $ assert_smaller e $ pushSubsts' f
+  go xs e@(DApp f p _) =
+    go (Left  p :: xs) $ assert_smaller e $ pushSubsts' f
+  go xs s = (s, xs)
+
+export FromString (Elim d n) where fromString s = F (fromString s) noLoc
+export FromString (Term d n) where fromString s = FT (fromString s) noLoc
+
+private
+prettyDTApps : {opts : _} ->
+               BContext d -> BContext n ->
+               Elim d n -> List (Either (Dim d) (Term d n)) ->
+               Eff Pretty (Doc opts)
+prettyDTApps dnames tnames f xs = do
+  f  <- withPrec Arg $ assert_total prettyElim dnames tnames f
+  xs <- for xs $ either (prettyDArg dnames) (prettyTArg dnames tnames)
+  parensIfM App =<< prettyAppD f xs
+
+
+private
+record CaseArm opts d n where
+  constructor MkCaseArm
+  pat    : Doc opts
+  dbinds : BTelescope d dinner -- 🍴
+  tbinds : BTelescope n ninner
+  body   : Term dinner ninner
+
+parameters {opts : LayoutOpts} (dnames : BContext d) (tnames : BContext n)
+  private
+  prettyCaseArm : CaseArm opts d n -> Eff Pretty (Doc opts)
+  prettyCaseArm (MkCaseArm pat dbinds tbinds body) = do
+    body <- withPrec Outer $ assert_total
+            prettyTerm (dnames . dbinds) (tnames . tbinds) body
+    header <- (pat <++>) <$> darrowD
+    pure $ hsep [header, body] <|> vsep [header, !(indentD body)]
+
+  private
+  prettyCaseBody : List (CaseArm opts d n) -> Eff Pretty (Doc opts)
+  prettyCaseBody xs =
+    braces . separateTight !semiD =<< traverse prettyCaseArm xs
+
+private
+prettyCompPat : {opts : _} -> DimConst -> BindName -> Eff Pretty (Doc opts)
+prettyCompPat e x = [|prettyDimConst e <++> prettyDBind x|]
+
+
+export
+prettyTag : {opts : _} -> String -> Eff Pretty (Doc opts)
+prettyTag tag = hl Tag $ text $ "'" ++ quoteTag tag
+
+export
+prettyEnum : {opts : _} -> List String -> Eff Pretty (Doc opts)
+prettyEnum cases =
+  tightDelims "{" "}" =<<
+  fillSeparateTight !commaD <$>
+  traverse (hl Tag . text . quoteTag) cases
+
+private
+prettyCaseRet : {opts : _} ->
+                BContext d -> BContext n ->
+                ScopeTerm d n -> Eff Pretty (Doc opts)
+prettyCaseRet dnames tnames body = withPrec Outer $ case body of
+  S _     (N tm) => assert_total prettyTerm dnames tnames tm
+  S [< x] (Y tm) => do
+    header <- [|prettyTBind x <++> darrowD|]
+    body   <- assert_total prettyTerm dnames (tnames :< x) tm
+    pure $ hsep [header, body] <|> vsep [header, !(indentD body)]
+
+private
+prettyCase_ : {opts : _} ->
+              BContext d -> BContext n ->
+              Doc opts -> Elim d n -> ScopeTerm d n -> List (CaseArm opts d n) ->
+              Eff Pretty (Doc opts)
+prettyCase_ dnames tnames intro head ret body = do
+  head <- assert_total prettyElim dnames tnames head
+  ret  <- prettyCaseRet dnames tnames ret
+  body <- prettyCaseBody dnames tnames body
+  parensIfM Outer $ sep [intro <++> head, !returnD <++> ret, !ofD <++> body]
+
+private
+prettyCase : {opts : _} ->
+             BContext d -> BContext n ->
+             Qty -> Elim d n -> ScopeTerm d n -> List (CaseArm opts d n) ->
+             Eff Pretty (Doc opts)
+prettyCase dnames tnames qty head ret body =
+  prettyCase_ dnames tnames ![|caseD <+> prettyQty qty|] head ret body
+
+
+-- [fixme] use telescopes in Scoped
+private
+toTel : BContext s -> BTelescope n (s + n)
+toTel [<]        = [<]
+toTel (ctx :< x) = toTel ctx :< x
+
+private
+prettyTyCasePat : {opts : _} ->
+                  (k : TyConKind) -> BContext (arity k) ->
+                  Eff Pretty (Doc opts)
+prettyTyCasePat KTYPE [<] = typeD
+prettyTyCasePat KPi [< a, b] =
+  parens . hsep =<< sequence [prettyTBind a, arrowD, prettyTBind b]
+prettyTyCasePat KSig [< a, b] =
+  parens . hsep =<< sequence [prettyTBind a, timesD, prettyTBind b]
+prettyTyCasePat KEnum [<] = hl Syntax $ text "{}"
+prettyTyCasePat KEq [< a0, a1, a, l, r] =
+  hsep <$> sequence (eqD :: map prettyTBind [a0, a1, a, l, r])
+prettyTyCasePat KNat [<] = natD
+prettyTyCasePat KBOX [< a] = bracks =<< prettyTBind a
+
+
+prettyLambda : {opts : _} -> BContext d -> BContext n ->
+               Term d n -> Eff Pretty (Doc opts)
+prettyLambda dnames tnames s =
+  parensIfM Outer =<< do
+    let MkSplitLams {dnames = ds, tnames = ts, chunks, body} = splitLams s
+    hangDSingle !(header chunks)
+      !(assert_total prettyTerm (dnames . ds) (tnames . ts) body)
+where
+  introChar : NameSort -> Eff Pretty (Doc opts)
+  introChar T = lamD
+  introChar D = dlamD
+
+  prettyBind : NameSort -> BindName -> Eff Pretty (Doc opts)
+  prettyBind T = prettyTBind
+  prettyBind D = prettyDBind
+
+  header1 : NameSort -> List BindName -> Eff Pretty (Doc opts)
+  header1 s xs = hsep <$> sequence
+    [introChar s, sep <$> traverse (prettyBind s) xs, darrowD]
+
+  header : NameChunks -> Eff Pretty (Doc opts)
+  header cs = sep <$> traverse (\(s, xs) => header1 s (toList xs)) (toList cs)
+
+
+prettyTerm dnames tnames (TYPE l _) =
+  hl Syntax =<<
+    case !(askAt FLAVOR) of
+      Unicode => pure $ text $ "★" ++ subscript (show l)
+      Ascii   => prettyAppD (text "Type") [text $ show l]
+
+prettyTerm dnames tnames (Pi qty arg res _) =
+  parensIfM Outer =<< do
+    let MkSplitPi {binds, cod} = splitPi [< (qty, res.name, arg)] res.term
+    arr   <- arrowD
+    lines <- map (<++> arr) <$> prettyPiBinds dnames tnames binds
+    let tnames = tnames . map pbname binds
+    cod <- withPrec Outer $ prettyTerm dnames tnames (assert_smaller res cod)
+    pure $ sepSingle $ toList $ lines :< cod
+
+prettyTerm dnames tnames s@(Lam {}) =
+  prettyLambda dnames tnames s
+
+prettyTerm dnames tnames (Sig fst snd _) =
+  parensIfM Times =<< do
+    let MkSplitSig {binds, last} = splitSig [< (snd.name, fst)] snd.term
+    times <- timesD
+    lines <- map (<++> times) <$> prettySigBinds dnames tnames binds
+    let tnames = tnames . map Builtin.fst binds
+    last <- withPrec InTimes $
+            prettyTerm dnames tnames (assert_smaller snd last)
+    pure $ sepSingle $ toList $ lines :< last
+
+prettyTerm dnames tnames p@(Pair fst snd _) =
+  parens =<< do
+    let elems = splitTuple [< fst] snd
+    lines <- for elems $ \t =>
+      withPrec Outer $ prettyTerm dnames tnames $ assert_smaller p t
+    pure $ separateTight !commaD lines
+
+prettyTerm dnames tnames (Enum cases _) =
+  prettyEnum $ SortedSet.toList cases
+
+prettyTerm dnames tnames (Tag tag _) =
+  prettyTag tag
+
+prettyTerm dnames tnames (Eq (S _ (N ty)) l r _) = do
+  l  <- withPrec InEq $ prettyTerm dnames tnames l
+  r  <- withPrec InEq $ prettyTerm dnames tnames r
+  ty <- withPrec InEq $ prettyTerm dnames tnames ty
+  pure $ sep [l <++> !eqndD, r <++> !colonD, ty]
+
+prettyTerm dnames tnames (Eq ty l r _) = do
+  ty <- prettyTypeLine dnames tnames ty
+  l  <- withPrec Arg $ prettyTerm dnames tnames l
+  r  <- withPrec Arg $ prettyTerm dnames tnames r
+  prettyAppD !eqD [ty, l, r]
+
+prettyTerm dnames tnames s@(DLam {}) =
+  prettyLambda dnames tnames s
+
+prettyTerm dnames tnames (Nat _) = natD
+prettyTerm dnames tnames (Zero _) = hl Syntax "0"
+prettyTerm dnames tnames (Succ p _) = do
+  succD <- succD
+  let succ : Doc opts -> Eff Pretty (Doc opts)
+      succ t = prettyAppD succD [t]
+      toNat : Term d n -> Eff Pretty (Either (Doc opts) Nat)
+      toNat s with (pushSubsts' s)
+        _ | Zero _   = pure $ Right 0
+        _ | Succ d _ = bitraverse succ (pure . S) =<<
+                       toNat (assert_smaller s d)
+        _ | s'       = map Left . withPrec Arg $
+                       prettyTerm dnames tnames $ assert_smaller s s'
+  either succ (hl Syntax . text . show . S) =<< toNat p
+
+prettyTerm dnames tnames (BOX qty ty _) =
+  bracks . hcat =<<
+    sequence [prettyQty qty, dotD,
+              withPrec Outer $ prettyTerm dnames tnames ty]
+
+prettyTerm dnames tnames (Box val _) =
+  bracks =<< withPrec Outer (prettyTerm dnames tnames val)
+
+prettyTerm dnames tnames (E e) = prettyElim dnames tnames e
+
+prettyTerm dnames tnames t0@(CloT (Sub t ph)) =
+  prettyTerm dnames tnames $ assert_smaller t0 $ pushSubstsWith' id ph t
+
+prettyTerm dnames tnames t0@(DCloT (Sub t ph)) =
+  prettyTerm dnames tnames $ assert_smaller t0 $ pushSubstsWith' ph id t
+
+prettyElim dnames tnames (F x _) =
+  prettyFree x
+
+prettyElim dnames tnames (B i _) =
+  prettyTBind $ tnames !!! i
+
+prettyElim dnames tnames e@(App {}) =
+  let (f, xs) = splitApps e in
+  prettyDTApps dnames tnames f xs
+
+prettyElim dnames tnames (CasePair qty pair ret body _) = do
+  let [< x, y] = body.names
+  pat <- parens . hsep =<< sequence
+         [[|prettyTBind x <+> commaD|], prettyTBind y]
+  prettyCase dnames tnames qty pair ret
+    [MkCaseArm pat [<] [< x, y] body.term]
+
+prettyElim dnames tnames (CaseEnum qty tag ret arms _) = do
+  arms <- for (SortedMap.toList arms) $ \(tag, body) =>
+    pure $ MkCaseArm !(prettyTag tag) [<] [<] body
+  prettyCase dnames tnames qty tag ret arms
+
+prettyElim dnames tnames (CaseNat qty qtyIH nat ret zero succ _) = do
+  let zarm = MkCaseArm !zeroD [<] [<] zero
+      [< p, ih] = succ.names
+  spat0 <- [|succD <++> prettyTBind p|]
+  ihpat0 <- map hcat $ sequence [prettyQty qtyIH, dotD, prettyTBind ih]
+  spat <- if ih.name == Unused
+          then pure spat0
+          else pure $ hsep [spat0 <+> !commaD, ihpat0]
+  let sarm = MkCaseArm spat [<] [< p, ih] succ.term
+  prettyCase dnames tnames qty nat ret [zarm, sarm]
+
+prettyElim dnames tnames (CaseBox qty box ret body _) = do
+  pat <- bracks =<< prettyTBind body.name
+  let arm = MkCaseArm pat [<] [< body.name] body.term
+  prettyCase dnames tnames qty box ret [arm]
+
+prettyElim dnames tnames e@(DApp {}) =
+  let (f, xs) = splitApps e in
+  prettyDTApps dnames tnames f xs
+
+prettyElim dnames tnames (Ann tm ty _) =
+  parensIfM Outer =<<
+    hangDSingle !(withPrec AnnL  [|prettyTerm dnames tnames tm <++> annD|])
+                !(withPrec Outer (prettyTerm dnames tnames ty))
+
+prettyElim dnames tnames (Coe ty p q val _) =
+  parensIfM App =<< do
+    ty  <- prettyTypeLine dnames tnames ty
+    p   <- prettyDArg dnames p
+    q   <- prettyDArg dnames q
+    val <- prettyTArg dnames tnames val
+    prettyAppD !coeD [ty, sep [p, q], val]
+
+prettyElim dnames tnames e@(Comp ty p q val r zero one _) =
+  parensIfM App =<< do
+    ty   <- prettyTypeLine dnames tnames $ assert_smaller e $ SN ty
+    p    <- prettyDArg dnames p
+    q    <- prettyDArg dnames q
+    val  <- prettyTArg dnames tnames val
+    r    <- prettyDArg dnames r
+    comp <- compD; lb <- hl Delim "{"; rb <- hl Delim "}"; sc <- semiD
+    arm0 <- map (<+> sc) $ prettyCaseArm dnames tnames $
+      MkCaseArm !(prettyCompPat Zero zero.name) [< zero.name] [<] zero.term
+    arm1 <- prettyCaseArm dnames tnames $
+      MkCaseArm !(prettyCompPat One one.name) [< one.name] [<] one.term
+    ind  <- askAt INDENT
+    pure $ ifMultiline
+      (hsep [comp, ty, p, q, val, r, lb, arm0, arm1, rb])
+      (comp <++> vsep [sep [ty, sep [p, q]], val, r <++> lb,
+                       indent ind $ vsep [arm0, arm1], rb] <|>
+       vsep (comp :: map (indent ind)
+        [ty, sep [p, q], val, r <++> lb,
+         indent ind $ vsep [arm0, arm1], rb]))
+
+prettyElim dnames tnames (TypeCase ty ret arms def _) = do
+  arms <- for (toList arms) $ \(k ** body) => do
+    pat <- prettyTyCasePat k body.names
+    pure $ MkCaseArm pat [<] (toTel body.names) body.term
+  let darm = MkCaseArm !undD [<] [<] def
+  prettyCase_ dnames tnames !typecaseD ty (SN ret) $ arms ++ [darm]
+
+prettyElim dnames tnames e0@(CloE (Sub e ph)) =
+  prettyElim dnames tnames $ assert_smaller e0 $ pushSubstsWith' id ph e
+
+prettyElim dnames tnames e0@(DCloE (Sub e ph)) =
+  prettyElim dnames tnames $ assert_smaller e0 $ pushSubstsWith' ph id e
diff --git a/lib/Quox/Syntax/Term/Split.idr b/lib/Quox/Syntax/Term/Split.idr
deleted file mode 100644
index 300cf2c..0000000
--- a/lib/Quox/Syntax/Term/Split.idr
+++ /dev/null
@@ -1,251 +0,0 @@
-module Quox.Syntax.Term.Split
-
-import Quox.Syntax.Term.Base
-import Quox.Syntax.Term.Subst
-import Quox.Syntax.Term.Tighten
-import Quox.Context
-
-import public Quox.No
-import public Data.Vect
-
-%default total
-
-
-public export %inline
-isLam : Term {} -> Bool
-isLam (Lam {}) = True
-isLam _        = False
-
-public export
-0 NotLam : Pred $ Term {}
-NotLam = No . isLam
-
-
-public export %inline
-isDLam : Term {} -> Bool
-isDLam (DLam {}) = True
-isDLam _         = False
-
-public export
-0 NotDLam : Pred $ Term {}
-NotDLam = No . isDLam
-
-
-public export %inline
-isPair : Term {} -> Bool
-isPair (Pair {}) = True
-isPair _         = False
-
-public export
-0 NotPair : Pred $ Term {}
-NotPair = No . isPair
-
-
-public export %inline
-isApp : Elim {} -> Bool
-isApp (App {}) = True
-isApp _        = False
-
-public export
-0 NotApp : Pred $ Elim {}
-NotApp = No . isApp
-
-
-public export %inline
-isDApp : Elim {} -> Bool
-isDApp (DApp {}) = True
-isDApp _         = False
-
-public export
-0 NotDApp : Pred $ Elim {}
-NotDApp = No . isDApp
-
-
--- infixl 9 :@@
--- ||| apply multiple arguments at once
--- public export %inline
--- (:@@) : Elim d n -> List (Term d n) -> Elim d n
--- f :@@ ss = foldl app f ss where
---   app : Elim d n -> Term d n -> Elim d n
---   app f s = App f s (f.loc `extend'` s.loc.bounds)
-
-public export
-record GetArgs d n where
-  constructor GotArgs
-  fun      : Elim d n
-  args     : List (Term d n)
-  0 notApp : NotApp fun
-
-mutual
-  export %inline
-  getArgs' : Elim d n -> List (Term d n) -> GetArgs d n
-  getArgs' fun0 args =
-    let Element fun nc = pushSubsts fun0 in
-    getArgsNc (assert_smaller fun0 fun) args
-
-  private
-  getArgsNc : (e : Elim d n) -> (0 nc : NotClo e) =>
-              List (Term d n) -> GetArgs d n
-  getArgsNc fun args = case nchoose $ isApp fun of
-    Left  y => let App f a _ = fun in getArgs' f (a :: args)
-    Right n => GotArgs {fun, args, notApp = n}
-
-||| splits an application into its head and arguments. if it's not an
-||| application then the list is just empty.
-||| looks through substitutions for applications.
-export %inline
-getArgs : Elim d n -> GetArgs d n
-getArgs e = getArgs' e []
-
-
--- infixl 9 :%%
--- ||| apply multiple dimension arguments at once
--- public export %inline
--- (:%%) : Elim d n -> List (Dim d) -> Elim d n
--- f :%% ss = foldl dapp f ss where
---   dapp : Elim d n -> Dim d -> Elim d n
---   dapp f p = DApp f p (f.loc `extend'` p.loc.bounds)
-
-public export
-record GetDArgs d n where
-  constructor GotDArgs
-  fun       : Elim d n
-  args      : List (Dim d)
-  0 notDApp : NotDApp fun
-
-mutual
-  export %inline
-  getDArgs' : Elim d n -> List (Dim d) -> GetDArgs d n
-  getDArgs' fun0 args =
-    let Element fun nc = pushSubsts fun0 in
-    getDArgsNc (assert_smaller fun0 fun) args
-
-  private
-  getDArgsNc : (e : Elim d n) -> (0 nc : NotClo e) =>
-               List (Dim d) -> GetDArgs d n
-  getDArgsNc fun args = case nchoose $ isDApp fun of
-    Left  y => let DApp f d _ = fun in getDArgs' f (d :: args)
-    Right n => GotDArgs {fun, args, notDApp = n}
-
-||| splits a dimension application into its head and arguments. if it's not an
-||| d application then the list is just empty
-export %inline
-getDArgs : Elim d n -> GetDArgs d n
-getDArgs e = getDArgs' e []
-
-
--- infixr 1 :\\
--- public export
--- absN : BContext m -> Term d (m + n) -> Term d n
--- absN [<]       s = s
--- absN (xs :< x) s = absN xs $ Lam (ST [< x] s) ?absloc
-
--- public export %inline
--- (:\\) : BContext m -> Term d (m + n) -> Term d n
--- (:\\) = absN
-
-
--- infixr 1 :\\%
--- public export
--- dabsN : BContext m -> Term (m + d) n -> Term d n
--- dabsN [<]       s = s
--- dabsN (xs :< x) s = dabsN xs $ DLam (DST [< x] s) ?dabsLoc
-
--- public export %inline
--- (:\\%) : BContext m -> Term (m + d) n -> Term d n
--- (:\\%) = dabsN
-
-
-public export
-record GetLams d n where
-  constructor GotLams
-  {0 lams, rest : Nat}
-  names    : BContext lams
-  body     : Term d rest
-  0 eq     : lams + n = rest
-  0 notLam : NotLam body
-
-mutual
-  export %inline
-  getLams' : forall lams, rest.
-             BContext lams -> Term d rest -> (0 eq : lams + n = rest) ->
-             GetLams d n
-  getLams' xs s0 eq =
-    let Element s nc = pushSubsts s0 in
-    getLamsNc xs (assert_smaller s0 s) eq
-
-  private
-  getLamsNc : forall lams, rest.
-              BContext lams ->
-              (t : Term d rest) -> (0 nc : NotClo t) =>
-              (0 eq : lams + n = rest) ->
-              GetLams d n
-  getLamsNc xs s Refl = case nchoose $ isLam s of
-    Left  y => let Lam (S [< x] body) _ = s in
-               getLams' (xs :< x) (assert_smaller s body.term) Refl
-    Right n => GotLams xs s Refl n
-
-export %inline
-getLams : Term d n -> GetLams d n
-getLams s = getLams' [<] s Refl
-
-
-public export
-record GetDLams d n where
-  constructor GotDLams
-  {0 lams, rest : Nat}
-  names     : BContext lams
-  body      : Term rest n
-  0 eq      : lams + d = rest
-  0 notDLam : NotDLam body
-
-mutual
-  export %inline
-  getDLams' : forall lams, rest.
-              BContext lams -> Term rest n -> (0 eq : lams + d = rest) ->
-              GetDLams d n
-  getDLams' xs s0 eq =
-    let Element s nc = pushSubsts s0 in
-    getDLamsNc xs (assert_smaller s0 s) eq
-
-  private
-  getDLamsNc : forall lams, rest.
-               BContext lams ->
-               (t : Term rest n) -> (0 nc : NotClo t) =>
-               (0 eq : lams + d = rest) ->
-               GetDLams d n
-  getDLamsNc is s Refl = case nchoose $ isDLam s of
-    Left  y => let DLam (S [< i] body) _ = s in
-               getDLams' (is :< i) (assert_smaller s body.term) Refl
-    Right n => GotDLams is s Refl n
-
-export %inline
-getDLams : Term d n -> GetDLams d n
-getDLams s = getDLams' [<] s Refl
-
-
-public export
-record GetPairs d n where
-  constructor GotPairs
-  init : SnocList $ Term d n
-  last : Term d n
-  notPair : NotPair last
-
-mutual
-  export %inline
-  getPairs' : SnocList (Term d n) -> Term d n -> GetPairs d n
-  getPairs' ss t0 =
-    let Element t nc = pushSubsts t0 in getPairsNc ss (assert_smaller t0 t)
-
-  private
-  getPairsNc : SnocList (Term d n) ->
-               (t : Term d n) -> (0 nc : NotClo t) =>
-               GetPairs d n
-  getPairsNc ss t = case nchoose $ isPair t of
-    Left  y => let Pair s t _ = t in
-               getPairs' (ss :< s) t
-    Right n => GotPairs ss t n
-
-export
-getPairs : Term d n -> GetPairs d n
-getPairs = getPairs' [<]
diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr
index e525bbc..191d3ac 100644
--- a/lib/Quox/Syntax/Term/Subst.idr
+++ b/lib/Quox/Syntax/Term/Subst.idr
@@ -234,6 +234,10 @@ parameters {0 isClo : CloTest tm} {auto _ : PushSubsts tm isClo}
                     tm dfrom from -> tm dto to
   pushSubstsWith' th ph x = fst $ pushSubstsWith th ph x
 
+  export %inline
+  pushSubsts' : tm d n -> tm d n
+  pushSubsts' s = fst $ pushSubsts s
+
 mutual
   public export
   isCloT : CloTest Term
diff --git a/lib/Quox/Syntax/Var.idr b/lib/Quox/Syntax/Var.idr
index c0b57fa..f9a648e 100644
--- a/lib/Quox/Syntax/Var.idr
+++ b/lib/Quox/Syntax/Var.idr
@@ -2,7 +2,6 @@ module Quox.Syntax.Var
 
 import public Quox.Loc
 import public Quox.Name
-import Quox.Pretty
 import Quox.OPE
 
 import Data.Nat
@@ -66,32 +65,6 @@ lookupS _     [<]       = Nothing
 lookupS Z     (sx :< x) = Just x
 lookupS (S i) (sx :< x) = lookupS i sx
 
-parameters {auto _ : Pretty.HasEnv m}
-  private
-  prettyIndex : Nat -> m (Doc a)
-  prettyIndex i =
-    ifUnicode (pretty $ pack $ map sup $ unpack $ show i) ("#" <+> pretty i)
-   where
-    sup : Char -> Char
-    sup c = case c of
-      '0' => '⁰'; '1' => '¹'; '2' => '²'; '3' => '³'; '4' => '⁴'
-      '5' => '⁵'; '6' => '⁶'; '7' => '⁷'; '8' => '⁸'; '9' => '⁹'; _ => c
-
-  ||| `prettyVar hlok hlerr names i` pretty prints the de Bruijn index `i`.
-  |||
-  ||| If it is within the bounds of `names`, then it uses the name at that index,
-  ||| highlighted as `hlok`. Otherwise it is just printed as a number highlighted
-  ||| as `hlerr`.
-  export
-  prettyVar' : HL -> HL -> SnocList BaseName -> Nat -> m (Doc HL)
-  prettyVar' hlok hlerr names i =
-    case lookupS i names of
-      Just x  => hlF' hlok $ prettyM x
-      Nothing => pure $ hl hlerr $ "#" <+> pretty i
-
-  export
-  prettyVar : HL -> HL -> SnocList BaseName -> Var n -> m (Doc HL)
-  prettyVar hlok hlerr names i = prettyVar' hlok hlerr names i.nat
 
 public export
 fromNatWith : (i : Nat) -> (0 p : i `LT` n) -> Var n
diff --git a/lib/Quox/Typing/Context.idr b/lib/Quox/Typing/Context.idr
index 1d5c7cd..8d44bc9 100644
--- a/lib/Quox/Typing/Context.idr
+++ b/lib/Quox/Typing/Context.idr
@@ -228,41 +228,38 @@ namespace WhnfContext
 
 
 private
-data CtxBinder a = MkCtxBinder BindName a
+prettyTContextElt : {opts : _} ->
+                    BContext d -> BContext n ->
+                    Qty -> BindName -> Term d n -> Eff Pretty (Doc opts)
+prettyTContextElt dnames tnames q x s =
+  pure $ hsep [hcat [!(prettyQty q), !dotD, !(prettyTBind x)], !colonD,
+               !(withPrec Outer $ prettyTerm dnames tnames s)]
 
-PrettyHL a => PrettyHL (CtxBinder a) where
-  prettyM (MkCtxBinder x t) = pure $
-    sep [hsep [!(pretty0M $ TV x.name), colonD], !(pretty0M t)]
+private
+prettyTContext' : {opts : _} ->
+                  BContext d -> QContext n -> BContext n ->
+                  TContext d n -> Eff Pretty (SnocList (Doc opts))
+prettyTContext' _ [<] [<] [<] = pure [<]
+prettyTContext' dnames (qtys :< q) (tnames :< x) (tys :< t) =
+  [|prettyTContext' dnames qtys tnames tys :<
+    prettyTContextElt dnames tnames q x t|]
 
-parameters (unicode : Bool)
-  private
-  pipeD : Doc HL
-  pipeD = hl Syntax "|"
+export
+prettyTContext : {opts : _} ->
+                 BContext d -> QContext n -> BContext n ->
+                 TContext d n -> Eff Pretty (Doc opts)
+prettyTContext dnames qtys tnames tys =
+  separateTight !commaD <$> prettyTContext' dnames qtys tnames tys
 
-  export covering
-  prettyTContext : BContext d ->
-                   QContext n -> BContext n ->
-                   TContext d n -> Doc HL
-  prettyTContext ds qs xs ctx = separate comma $ toList $ go qs xs ctx where
-    go : QContext m -> BContext m -> TContext d m -> SnocList (Doc HL)
-    go [<]       [<]       [<] = [<]
-    go (qs :< q) (xs :< x) (ctx :< t) =
-      let bind = MkWithQty q $ MkCtxBinder x t in
-      go qs xs ctx :<
-      runPrettyWith unicode (toNames ds) (toNames xs) (pretty0M bind)
+export
+prettyTyContext : {opts : _} -> TyContext d n -> Eff Pretty (Doc opts)
+prettyTyContext (MkTyContext dctx dnames tctx tnames qtys) =
+  case dctx of
+    C [<] => prettyTContext dnames qtys tnames tctx
+    _     => pure $
+      sep [!(prettyDimEq dnames dctx) <++> !pipeD,
+           !(prettyTContext dnames qtys tnames tctx)]
 
-  export covering
-  prettyTyContext : TyContext d n -> Doc HL
-  prettyTyContext (MkTyContext dctx dnames tctx tnames qtys) =
-    case dctx of
-      C [<] => prettyTContext dnames qtys tnames tctx
-      _     => sep [prettyDimEq dnames dctx <++> pipeD,
-                    prettyTContext dnames qtys tnames tctx]
-
-  export covering
-  prettyEqContext : EqContext n -> Doc HL
-  prettyEqContext (MkEqContext dassign dnames tctx tnames qtys) =
-    case dassign of
-      [<] => prettyTContext [<] qtys tnames tctx
-      _   => sep [prettyDimEq dnames (fromGround dassign) <++> pipeD,
-                  prettyTContext [<] qtys tnames tctx]
+export
+prettyEqContext : {opts : _} -> EqContext n -> Eff Pretty (Doc opts)
+prettyEqContext ctx = prettyTyContext $ toTyContext ctx
diff --git a/lib/Quox/Typing/Error.idr b/lib/Quox/Typing/Error.idr
index 4211504..5975445 100644
--- a/lib/Quox/Typing/Error.idr
+++ b/lib/Quox/Typing/Error.idr
@@ -140,43 +140,21 @@ Located Error where
   (WhileComparingE _ _ _ _ err).loc   = err.loc
 
 
-||| whether the error is surrounded in some context
-||| (e.g. "while checking s : A, …")
-public export
-isErrorContext : Error -> Bool
-isErrorContext (WhileChecking   {}) = True
-isErrorContext (WhileCheckingTy {}) = True
-isErrorContext (WhileInferring  {}) = True
-isErrorContext (WhileComparingT {}) = True
-isErrorContext (WhileComparingE {}) = True
-isErrorContext _                    = False
-
-||| remove one layer of context
-export
-peelContext : (e : Error) -> (0 _ : So (isErrorContext e)) =>
-              (Error -> Error, Error)
-peelContext (WhileChecking ctx x s t err) =
-  (WhileChecking ctx x s t, err)
-peelContext (WhileCheckingTy ctx s k err) =
-  (WhileCheckingTy ctx s k, err)
-peelContext (WhileInferring ctx x e err) =
-  (WhileInferring ctx x e, err)
-peelContext (WhileComparingT ctx x s t r err) =
-  (WhileComparingT ctx x s t r, err)
-peelContext (WhileComparingE ctx x e f err) =
-  (WhileComparingE ctx x e f, err)
-
 ||| separates out all the error context layers
 ||| (e.g. "while checking s : A, …")
 export
 explodeContext : Error -> (List (Error -> Error), Error)
-explodeContext err =
-  case choose $ isErrorContext err of
-    Left y =>
-      let (f,  inner) = peelContext err
-          (fs, root)  = explodeContext $ assert_smaller err inner in
-      (f :: fs, root)
-    Right n => ([], err)
+explodeContext (WhileChecking ctx x s t err) =
+  mapFst (WhileChecking ctx x s t ::) $ explodeContext err
+explodeContext (WhileCheckingTy ctx s k err) =
+  mapFst (WhileCheckingTy ctx s k ::) $ explodeContext err
+explodeContext (WhileInferring ctx x e err) =
+  mapFst (WhileInferring ctx x e ::) $ explodeContext err
+explodeContext (WhileComparingT ctx x s t r err) =
+  mapFst (WhileComparingT ctx x s t r ::) $ explodeContext err
+explodeContext (WhileComparingE ctx x e f err) =
+  mapFst (WhileComparingE ctx x e f ::) $ explodeContext err
+explodeContext err = ([], err)
 
 ||| leaves the outermost context layer, and the innermost (up to) n, and removes
 ||| the rest if there are more than n+1 in total
@@ -211,192 +189,211 @@ parameters {auto _ : Has ErrorEff fs} (loc : Loc)
 
 
 private
-prettyMode : EqMode -> Doc HL
+prettyMode : EqMode -> String
 prettyMode Equal = "equal to"
 prettyMode Sub   = "a subtype of"
 prettyMode Super = "a supertype of"
 
 private
-prettyModeU : EqMode -> Doc HL
+prettyModeU : EqMode -> String
 prettyModeU Equal = "equal to"
 prettyModeU Sub   = "less than or equal to"
 prettyModeU Super = "greater than or equal to"
 
 private
-isTypeInUniverse : Maybe Universe -> Doc HL
+isTypeInUniverse : Maybe Universe -> String
 isTypeInUniverse Nothing  = "is a type"
-isTypeInUniverse (Just k) = "is a type in universe" <++> prettyUniverse k
+isTypeInUniverse (Just k) = "is a type in universe \{show k}"
 
-parameters (unicode : Bool)
-  private
-  termn : NameContexts d n -> Term d n -> Doc HL
-  termn ctx = hang 4 . prettyTerm unicode ctx.dnames ctx.tnames
 
-  private
-  dstermn : {s : Nat} -> NameContexts d n -> DScopeTermN s d n -> Doc HL
-  dstermn ctx (S i t) = termn (extendDimN i ctx) t.term
+private
+filterSameQtys : BContext n -> List (QOutput n, z) ->
+                 Exists $ \n' => (BContext n', List (QOutput n', z))
+filterSameQtys [<]       qts = Evidence 0 ([<], qts)
+filterSameQtys (ns :< n) qts =
+  let (qs, qts) = unzip $ map (\(qs :< q, t) => (q, qs, t)) qts
+      Evidence l (ns, qts) = filterSameQtys ns qts
+  in
+  if allSame qs
+  then Evidence l (ns, qts)
+  else Evidence (S l) (ns :< n, zipWith (\(qs, t), q => (qs :< q, t)) qts qs)
+where
+  allSame : List Qty -> Bool
+  allSame []        = True
+  allSame (q :: qs) = all (== q) qs
 
-  private
-  filterSameQtys : BContext n -> List (QOutput n, z) ->
-                   Exists $ \n' => (BContext n', List (QOutput n', z))
-  filterSameQtys [<]       qts = Evidence 0 ([<], qts)
-  filterSameQtys (ns :< n) qts =
-    let (qs, qts) = unzip $ map (\(qs :< q, t) => (q, qs, t)) qts
-        Evidence l (ns, qts) = filterSameQtys ns qts
-    in
-    if allSame qs
-    then Evidence l (ns, qts)
-    else Evidence (S l) (ns :< n, zipWith (\(qs, t), q => (qs :< q, t)) qts qs)
-  where
-    allSame : List Qty -> Bool
-    allSame []        = True
-    allSame (q :: qs) = all (== q) qs
 
-  private
-  printCaseQtys : TyContext d n ->
-                  BContext n' -> List (QOutput n', Term d n) ->
-                  List (Doc HL)
-  printCaseQtys ctx ns qts =
-    let Evidence l (ns, qts) = filterSameQtys ns qts in
-    map (line ns) qts
-  where
-    commaList : PrettyHL a => Context' a l -> Doc HL
-    commaList = hseparate comma . map (pretty0 unicode) . toList'
+private
+printCaseQtys : {opts : _} -> TyContext d n ->
+                BContext n' -> List (QOutput n', Term d n) ->
+                Eff Pretty (List (Doc opts))
+printCaseQtys ctx ns qts =
+  let Evidence _ (ns, qts) = filterSameQtys ns qts in
+  traverse (line ns) qts
+where
+  line : BContext l -> (QOutput l, Term d n) -> Eff Pretty (Doc opts)
+  line ns (qs, t) = map (("-" <++>) . sep) $ sequence
+    [hangDSingle "the term"
+      !(prettyTerm ctx.dnames ctx.tnames t),
+     hangDSingle "uses variables" $
+      separateTight !commaD $ toSnocList' !(traverse prettyTBind ns),
+     hangDSingle "with quantities" $
+      separateTight !commaD $ toSnocList' !(traverse prettyQty qs)]
 
-    line : BContext l -> (QOutput l, Term d n) -> Doc HL
-    line ns (qs, t) =
-      "-" <++> asep ["the term", termn ctx.names t,
-                     "uses variables", commaList $ (TV . name) <$> ns,
-                     "with quantities", commaList qs]
+export
+prettyErrorNoLoc : {opts : _} -> (showContext : Bool) -> Error ->
+                   Eff Pretty (Doc opts)
+prettyErrorNoLoc showContext = \case
+  ExpectedTYPE _ ctx s =>
+    hangDSingle "expected a type universe, but got"
+      !(prettyTerm ctx.dnames ctx.tnames s)
 
-  export
-  prettyErrorNoLoc : (showContext : Bool) -> Error -> Doc HL
-  prettyErrorNoLoc showContext = \case
-    ExpectedTYPE _ ctx s =>
-      sep ["expected a type universe, but got", termn ctx s]
+  ExpectedPi _ ctx s =>
+    hangDSingle "expected a function type, but got"
+      !(prettyTerm ctx.dnames ctx.tnames s)
 
-    ExpectedPi loc ctx s =>
-      sep ["expected a function type, but got", termn ctx s]
+  ExpectedSig _ ctx s =>
+    hangDSingle "expected a pair type, but got"
+      !(prettyTerm ctx.dnames ctx.tnames s)
 
-    ExpectedSig loc ctx s =>
-      sep ["expected a pair type, but got", termn ctx s]
+  ExpectedEnum _ ctx s =>
+    hangDSingle "expected an enumeration type, but got"
+      !(prettyTerm ctx.dnames ctx.tnames s)
 
-    ExpectedEnum loc ctx s =>
-      sep ["expected an enumeration type, but got", termn ctx s]
+  ExpectedEq _ ctx s =>
+    hangDSingle "expected an enumeration type, but got"
+      !(prettyTerm ctx.dnames ctx.tnames s)
 
-    ExpectedEq loc ctx s =>
-      sep ["expected an equality type, but got", termn ctx s]
+  ExpectedNat _ ctx s =>
+    hangDSingle
+      ("expected the type" <++>
+        !(prettyTerm [<] [<] $ Nat noLoc) <+> ", but got")
+      !(prettyTerm ctx.dnames ctx.tnames s)
 
-    ExpectedNat loc ctx s {d, n} =>
-      sep ["expected the type",
-           pretty0 unicode $ Nat noLoc {d, n}, "but got", termn ctx s]
+  ExpectedBOX _ ctx s =>
+    hangDSingle "expected a box type, but got"
+      !(prettyTerm ctx.dnames ctx.tnames s)
 
-    ExpectedBOX loc ctx s =>
-      sep ["expected a box type, but got", termn ctx s]
+  BadUniverse _ k l => pure $
+    sep ["the universe level" <++> !(prettyUniverse k),
+         "is not strictly less than" <++> !(prettyUniverse l)]
 
-    BadUniverse loc k l =>
-      sep ["the universe level", prettyUniverse k,
-           "is not strictly less than", prettyUniverse l]
+  TagNotIn _ tag set =>
+    hangDSingle (hsep ["the tag", !(prettyTag tag), "is not contained in"])
+      !(prettyTerm [<] [<] $ Enum set noLoc)
 
-    TagNotIn loc tag set =>
-      sep [hsep ["tag", prettyTag tag, "is not contained in"],
-           termn empty (Enum set noLoc)]
+  BadCaseEnum _ head body => sep <$> sequence
+    [hangDSingle "case expression has head of type"
+       !(prettyTerm [<] [<] $ Enum head noLoc),
+     hangDSingle "but cases for"
+       !(prettyTerm [<] [<] $ Enum body noLoc)]
 
-    BadCaseEnum loc type arms =>
-      sep ["case expression has head of type",
-           termn empty (Enum type noLoc),
-           "but cases for", termn empty (Enum arms noLoc)]
+  BadQtys _ what ctx arms =>
+    hangDSingle (text "inconsistent variable usage in \{what}") $
+      sep !(printCaseQtys ctx ctx.tnames arms)
 
-    BadQtys loc what ctx arms =>
-      hang 4 $ sep $
-        hsep ["inconsistent variable usage in", fromString what]
-          :: printCaseQtys ctx ctx.tnames arms
+  ClashT _ ctx mode ty s t =>
+    inEContext ctx . sep =<< sequence
+    [hangDSingle "the term" !(prettyTerm [<] ctx.tnames s),
+     hangDSingle (text "is not \{prettyMode mode}")
+        !(prettyTerm [<] ctx.tnames t),
+     hangDSingle "at type" !(prettyTerm [<] ctx.tnames ty)]
 
-    ClashT loc ctx mode ty s t =>
-      inEContext ctx $
-      sep ["the term", termn ctx.names0 s,
-           hsep ["is not", prettyMode mode], termn ctx.names0 t,
-           "at type", termn ctx.names0 ty]
+  ClashTy _ ctx mode a b =>
+    inEContext ctx . sep =<< sequence
+    [hangDSingle "the type" !(prettyTerm [<] ctx.tnames a),
+     hangDSingle (text "is not \{prettyMode mode}")
+        !(prettyTerm [<] ctx.tnames b)]
 
-    ClashTy loc ctx mode a b =>
-      inEContext ctx $
-      sep ["the type", termn ctx.names0 a,
-           hsep ["is not", prettyMode mode], termn ctx.names0 b]
+  ClashE _ ctx mode e f =>
+    inEContext ctx . sep =<< sequence
+    [hangDSingle "the term" !(prettyElim [<] ctx.tnames e),
+     hangDSingle (text "is not \{prettyMode mode}")
+        !(prettyElim [<] ctx.tnames f)]
 
-    ClashE loc ctx mode e f =>
-      inEContext ctx $
-      sep ["the term", termn ctx.names0 $ E e,
-           hsep ["is not", prettyMode mode], termn ctx.names0 $ E f]
+  ClashU _ mode k l => pure $
+    sep ["the universe level" <++> !(prettyUniverse k),
+         text "is not \{prettyModeU mode}" <++> !(prettyUniverse l)]
 
-    ClashU loc mode k l =>
-      sep ["the universe level", prettyUniverse k,
-           hsep ["is not", prettyMode mode], prettyUniverse l]
+  ClashQ _ pi rh => pure $
+    sep ["the quantity" <++> !(prettyQty pi),
+         "is not equal to" <++> !(prettyQty rh)]
 
-    ClashQ loc pi rh =>
-      sep ["the quantity", pretty0 unicode pi,
-           "is not equal to", pretty0 unicode rh]
+  NotInScope _ x => pure $
+    hsep [!(prettyFree x), "is not in scope"]
 
-    NotInScope loc x =>
-      hsep [hl' Free $ pretty0 unicode x, "is not in scope"]
+  NotType _ ctx s =>
+    inTContext ctx . sep =<< sequence
+    [hangDSingle "the term" !(prettyTerm ctx.dnames ctx.tnames s),
+     pure "is not a type"]
 
-    NotType loc ctx s =>
-      inTContext ctx $
-      sep ["the term", termn ctx.names s, "is not a type"]
+  WrongType _ ctx ty s =>
+    inEContext ctx . sep =<< sequence
+    [hangDSingle "the term" !(prettyTerm [<] ctx.tnames s),
+     hangDSingle "cannot have type" !(prettyTerm [<] ctx.tnames ty)]
 
-    WrongType loc ctx ty s =>
-      inEContext ctx $
-      sep ["the term", termn ctx.names0 s,
-           "cannot have type", termn ctx.names0 ty]
+  MissingEnumArm _ tag tags => pure $
+    sep [hsep ["the tag", !(prettyTag tag), "is not contained in"],
+         !(prettyTerm [<] [<] $ Enum (fromList tags) noLoc)]
 
-    MissingEnumArm loc tag tags =>
-      sep [hsep ["the tag", hl Tag $ pretty tag, "is not contained in"],
-           termn empty $ Enum (fromList tags) noLoc]
+  WhileChecking ctx pi s a err =>
+    [|vappendBlank
+        (inTContext ctx . sep =<< sequence
+          [hangDSingle "while checking" !(prettyTerm ctx.dnames ctx.tnames s),
+           hangDSingle "has type"       !(prettyTerm ctx.dnames ctx.tnames a),
+           hangDSingle "with quantity"  !(prettyQty pi)])
+        (prettyErrorNoLoc showContext err)|]
 
-    WhileChecking ctx pi s a err =>
-      vsep [inTContext ctx $
-              sep ["while checking", termn ctx.names s,
-                   "has type", termn ctx.names a,
-                   hsep ["with quantity", pretty0 unicode pi]],
-            prettyErrorNoLoc showContext err]
+  WhileCheckingTy ctx a k err =>
+    [|vappendBlank
+        (inTContext ctx . sep =<< sequence
+          [hangDSingle "while checking" !(prettyTerm ctx.dnames ctx.tnames a),
+           pure $ text $ isTypeInUniverse k])
+        (prettyErrorNoLoc showContext err)|]
 
-    WhileCheckingTy ctx a k err =>
-      vsep [inTContext ctx $
-              sep ["while checking", termn ctx.names a,
-                   isTypeInUniverse k],
-            prettyErrorNoLoc showContext err]
+  WhileInferring ctx pi e err =>
+    [|vappendBlank
+        (inTContext ctx . sep =<< sequence
+          [hangDSingle "while inferring the type of"
+              !(prettyElim ctx.dnames ctx.tnames e),
+           hangDSingle "with quantity"  !(prettyQty pi)])
+        (prettyErrorNoLoc showContext err)|]
 
-    WhileInferring ctx pi e err =>
-      vsep [inTContext ctx $
-              sep ["while inferring the type of", termn ctx.names $ E e,
-                   hsep ["with quantity", pretty0 unicode pi]],
-            prettyErrorNoLoc showContext err]
+  WhileComparingT ctx mode a s t err =>
+    [|vappendBlank
+        (inEContext ctx . sep =<< sequence
+          [hangDSingle "while checking that" !(prettyTerm [<] ctx.tnames s),
+           hangDSingle (text "is \{prettyMode mode}")
+              !(prettyTerm [<] ctx.tnames t),
+           hangDSingle "at type" !(prettyTerm [<] ctx.tnames a)])
+        (prettyErrorNoLoc showContext err)|]
 
-    WhileComparingT ctx mode a s t err =>
-      vsep [inEContext ctx $
-              sep ["while checking that", termn ctx.names0 s,
-                   hsep ["is", prettyMode mode], termn ctx.names0 t,
-                   "at type", termn ctx.names0 a],
-            prettyErrorNoLoc showContext err]
+  WhileComparingE ctx mode e f err =>
+    [|vappendBlank
+        (inEContext ctx . sep =<< sequence
+          [hangDSingle "while checking that" !(prettyElim [<] ctx.tnames e),
+           hangDSingle (text "is \{prettyMode mode}")
+              !(prettyElim [<] ctx.tnames f)])
+        (prettyErrorNoLoc showContext err)|]
 
-    WhileComparingE ctx mode e f err =>
-      vsep [inEContext ctx $
-              sep ["while checking that", termn ctx.names0 $ E e,
-                   hsep ["is", prettyMode mode], termn ctx.names0 $ E f],
-            prettyErrorNoLoc showContext err]
-  where
-    inTContext : TyContext d n -> Doc HL -> Doc HL
-    inTContext ctx doc =
-      if showContext && not (null ctx) then
-        vsep [sep ["in context", prettyTyContext unicode ctx], doc]
-      else doc
+where
+  vappendBlank : Doc opts -> Doc opts -> Doc opts
+  vappendBlank a b = flush a `vappend` b
 
-    inEContext : EqContext n -> Doc HL -> Doc HL
-    inEContext ctx doc =
-      if showContext && not (null ctx) then
-        vsep [sep ["in context", prettyEqContext unicode ctx], doc]
-      else doc
+  inTContext : TyContext d n -> Doc opts -> Eff Pretty (Doc opts)
+  inTContext ctx doc =
+    if showContext && not (null ctx) then
+      pure $ vappend doc (sep ["in context", !(prettyTyContext ctx)])
+    else pure doc
 
-  export
-  prettyError : (showContext : Bool) -> Error -> Doc HL
-  prettyError showContext err =
-    sep [prettyLoc err.loc, indent 4 $ prettyErrorNoLoc showContext err]
+  inEContext : EqContext n -> Doc opts -> Eff Pretty (Doc opts)
+  inEContext ctx doc =
+    if showContext && not (null ctx) then
+      pure $ vappend doc (sep ["in context", !(prettyEqContext ctx)])
+    else pure doc
+
+export
+prettyError : {opts : _} -> (showContext : Bool) ->
+              Error -> Eff Pretty (Doc opts)
+prettyError showContext err = sep <$> sequence
+  [prettyLoc err.loc, indentD =<< prettyErrorNoLoc showContext err]
diff --git a/lib/Text/PrettyPrint/Bernardy/Core/Decorate.idr b/lib/Text/PrettyPrint/Bernardy/Core/Decorate.idr
new file mode 100644
index 0000000..9e276d6
--- /dev/null
+++ b/lib/Text/PrettyPrint/Bernardy/Core/Decorate.idr
@@ -0,0 +1,45 @@
+-- this module has to be called this because a module A.B's private elements are
+-- still visible to A.B.C, even if they're in different packages. which i don't
+-- think is a good idea but i also don't want to fork prettier over it
+module Text.PrettyPrint.Bernardy.Core.Decorate
+
+import public Text.PrettyPrint.Bernardy.Core
+import Data.DPair
+
+
+public export
+record Highlight where
+  constructor MkHighlight
+  before, after : String
+
+export
+emptyHL : Highlight -> Bool
+emptyHL (MkHighlight before after) = before == "" && after == ""
+
+
+-- taken from prettier-ansi
+private
+decorateImpl : Highlight ->
+               (ss : SnocList String) -> (0 _ : NonEmptySnoc ss) =>
+               Subset (SnocList String) NonEmptySnoc
+decorateImpl h [<x]      = Element [< h.before ++ x ++ h.after] %search
+decorateImpl h (sx :< x) = Element (go [] sx :< (x ++ h.after)) %search
+  where
+    go : List String -> SnocList String -> SnocList String
+    go strs [< x]     = [< h.before ++ x] <>< strs
+    go strs (sx :< x) = go (x :: strs) sx
+    go strs [<]       = [<] <>< strs
+
+||| Decorate a `Layout` with the given ANSI codes *without*
+||| changing its stats like width or height.
+export
+decorateLayout : Highlight -> Layout -> Layout
+decorateLayout h l@(MkLayout content stats) =
+  if emptyHL h then l else
+  layout (decorateImpl h content) stats
+
+||| Decorate a `Doc` with the given highlighting *without*
+||| changing its stats like width or height.
+export
+decorate : {opts : _} -> Highlight -> Doc opts -> Doc opts
+decorate h doc = doc >>= \l => pure (decorateLayout h l)
diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg
index 55749e0..53c93f6 100644
--- a/lib/quox-lib.ipkg
+++ b/lib/quox-lib.ipkg
@@ -5,9 +5,10 @@ authors   = "rhiannon morris"
 sourceloc = "https://git.rhiannon.website/rhi/quox"
 license   = "acsl"
 
-depends = base, contrib, elab-util, sop, snocvect, eff
+depends = base, contrib, elab-util, sop, snocvect, eff, prettier
 
 modules =
+  Text.PrettyPrint.Bernardy.Core.Decorate,
   Quox.BoolExtra,
   Quox.CharExtra,
   Quox.NatExtra,
@@ -28,7 +29,6 @@ modules =
   Quox.Syntax.Term.Base,
   Quox.Syntax.Term.Tighten,
   Quox.Syntax.Term.Pretty,
-  Quox.Syntax.Term.Split,
   Quox.Syntax.Term.Subst,
   Quox.Syntax.Var,
   Quox.Definition,
diff --git a/pack.toml b/pack.toml
index 0232224..22dccb9 100644
--- a/pack.toml
+++ b/pack.toml
@@ -1,4 +1,4 @@
-collection = "nightly-230323"
+collection = "nightly-230505"
 
 [custom.all.tap]
 type = "git"
diff --git a/tests/PrettyExtra.idr b/tests/PrettyExtra.idr
index 4570be9..0789ea7 100644
--- a/tests/PrettyExtra.idr
+++ b/tests/PrettyExtra.idr
@@ -10,22 +10,36 @@ squash = pack . squash' . unpack . trim where
   squash' : List Char -> List Char
   squash' [] = []
   squash' (c :: cs) =
-    if isSpace c then
-      ' ' :: squash' (dropWhile isSpace cs)
-    else
-      c :: squash' cs
+    if isSpace c then ' ' :: squash' (dropWhile isSpace cs)
+    else c :: squash' cs
+
+public export
+Printer : Type -> Type
+Printer a = {opts : _} -> a -> Eff Pretty (Doc opts)
 
 export
-renderSquash : Doc HL -> String
-renderSquash doc = squash $ renderShow (layoutCompact doc) ""
+renderSquash : ({opts : _} -> Doc opts) -> String
+renderSquash doc = squash $ render (Opts 10000) doc
 
 export
-testPretty : PrettyHL a => (dnames, tnames : SnocList BaseName) ->
-             a -> (uni, asc : String) ->
+prettySquash : Printer a -> Flavor -> a -> String
+prettySquash pr f x =
+  renderSquash $ runPrettyWith Outer f noHighlight 0 (pr x)
+
+export
+testPretty : Printer a -> a -> (uni, asc : String) ->
              {default uni label : String} -> Test
-testPretty dnames tnames t uni asc {label} = test {e = Info} label $ do
+testPretty pr t uni asc {label} = test {e = Info} label $ do
   let uni  = squash uni; asc = squash asc
-      uni' = renderSquash $ pretty0With True  dnames tnames t
-      asc' = renderSquash $ pretty0With False dnames tnames t
+      uni' = prettySquash pr Unicode t
+      asc' = prettySquash pr Ascii t
   unless (uni == uni') $ Left [("exp", uni), ("got", uni')]
   unless (asc == asc') $ Left [("exp", asc), ("got", asc')]
+
+export
+runPrettyDef : Eff Pretty a -> a
+runPrettyDef = runPrettyWith Outer Unicode noHighlight 0
+
+export
+prettyStr : ({opts : _} -> Eff Pretty (Doc opts)) -> String
+prettyStr doc = render (Opts 60) $ runPrettyDef doc
diff --git a/tests/Tests/DimEq.idr b/tests/Tests/DimEq.idr
index e0bf1fe..7f0a847 100644
--- a/tests/Tests/DimEq.idr
+++ b/tests/Tests/DimEq.idr
@@ -16,62 +16,65 @@ import Data.So
 -- [todo] 'set' never breaks existing equalities
 
 private
-prettyDimEq' : {default Arg prec : PPrec} -> NContext d -> DimEq d -> Doc HL
-prettyDimEq' [<] (C _) = "·"
-prettyDimEq' ds eqs =
-  runPrettyWith False (toSnocList' ds) [<] $ withPrec prec $ prettyM eqs
+prettyDimEq_ : {opts : _} -> {default Arg prec : PPrec} ->
+               BContext d -> DimEq d -> Eff Pretty (Doc opts)
+prettyDimEq_ [<] (C _) = pure "·"
+prettyDimEq_ ds eqs    = prettyDimEq ds eqs
 
 private
-testPrettyD : NContext d -> DimEq d -> (str : String) ->
+testPrettyD : BContext d -> DimEq d -> (str : String) ->
               {default str label : String} -> Test
 testPrettyD ds eqs str {label} =
-  testPretty (toSnocList' ds) [<] eqs str str {label}
+  testPretty (prettyDimEq ds) eqs str str {label}
 
 private
-testWf : NContext d -> DimEq d -> Test
+testWf : BContext d -> DimEq d -> Test
 testWf ds eqs =
-  test (renderSquash $ sep [prettyDimEq' {prec = Outer} ds eqs, "⊢", "✓"]) $
+  test (prettySquash (prettyDimEq_ ds) Unicode eqs ++ "⊢ ✓") $
     unless (wf eqs) $ Left ()
 
 private
-testNwf : NContext d -> DimEq d -> Test
+testNwf : BContext d -> DimEq d -> Test
 testNwf ds eqs =
-  test (renderSquash $ sep [prettyDimEq' {prec = Outer} ds eqs, "⊬", "✓"]) $
+  test (prettySquash (prettyDimEq_ ds) Unicode eqs ++ "⊢ ✗") $
     when (wf eqs) $ Left ()
 
 
 private
-testEqLabel : String -> (ds : NContext d) -> (exp, got : DimEq d) -> String
-testEqLabel op ds exp got = renderSquash $
-  sep [prettyDimEq' ds exp, fromString op, prettyDimEq' ds got]
+testEqLabel : String -> (ds : BContext d) -> (exp, got : DimEq d) -> String
+testEqLabel op ds exp got =
+  renderSquash $ runPrettyDef $ do
+  pure $ sep [!(prettyDimEq_ ds exp), text op, !(prettyDimEq_ ds got)]
 
 private
-testNeq : (ds : NContext d) -> (exp, got : DimEq d) ->
+testNeq : (ds : BContext d) -> (exp, got : DimEq d) ->
           {default (testEqLabel "≠" ds exp got) label : String} -> Test
 testNeq {label} ds exp got =
   test label $ unless (exp /= got) $ Left ()
 
 private
-testEq : (ds : NContext d) -> (exp, got : DimEq d) ->
+testEq : (ds : BContext d) -> (exp, got : DimEq d) ->
          {default (testEqLabel "=" ds exp got) label : String} -> Test
 testEq {label} ds exp got =
   test label $ unless (exp == got) $
-    Left [("exp", renderSquash $ prettyDimEq' ds exp),
-          ("got", renderSquash $ prettyDimEq' ds got)]
+    Left [("exp", prettySquash (prettyDimEq_ ds) Unicode exp),
+          ("got", prettySquash (prettyDimEq_ ds) Unicode got)]
 
 private
-testSetLabel : String -> NContext d -> DimEq d ->
+testSetLabel : String -> BContext d -> DimEq d ->
                DimEq d -> List (Dim d, Dim d) -> String
-testSetLabel op ds exp start sets = renderSquash $
-  sep [parens $ sep $ intersperse "/" $
-         prettyDimEq' {prec = Outer} ds start :: map prettySet sets,
-       fromString op, prettyDimEq' ds exp]
+testSetLabel op ds exp start sets = renderSquash $ runPrettyDef $ do
+  pure $ sep
+    [parens $ sep $ intersperse "/" $
+       !(prettyDimEq_ {prec = Outer} ds start) :: !(traverse prettySet sets),
+     text op, !(prettyDimEq_ ds exp)]
 where
-  prettySet : (Dim d, Dim d) -> Doc HL
-  prettySet (p, q) = hsep [prettyDim ds p, "≔", prettyDim ds q]
+  prettySet : {opts : _} -> (Dim d, Dim d) -> Eff Pretty (Doc opts)
+  prettySet (p, q) = pure $
+    hsep [!(prettyDim ds p), "≔", !(prettyDim ds q)]
 
 private
-testSet : (ds : NContext d) -> (exp, start : DimEq d) ->
+testSet : (ds : BContext d) -> (exp, start : DimEq d) ->
           (sets : List (Dim d, Dim d)) ->
           (0 _ : (So (wf start), So (wf exp))) =>
           Test
@@ -80,7 +83,7 @@ testSet ds exp start sets =
     foldl (\eqs, (p, q) => set p q eqs) start sets
 
 private
-ii, iijj, iijjkk, iijjkkll : NContext ?
+ii, iijj, iijjkk, iijjkkll : BContext ?
 ii = [< "𝑖"]
 iijj = [< "𝑖", "𝑗"]
 iijjkk = [< "𝑖", "𝑗", "𝑘"]
diff --git a/tests/Tests/FromPTerm.idr b/tests/Tests/FromPTerm.idr
index aecf622..a8b1ca6 100644
--- a/tests/Tests/FromPTerm.idr
+++ b/tests/Tests/FromPTerm.idr
@@ -7,6 +7,7 @@ import Tests.Parser as TParser
 import Quox.EffExtra
 import TAP
 import AstExtra
+import PrettyExtra
 
 import System.File
 import Derive.Prelude
@@ -29,7 +30,7 @@ ToInfo Failure where
   toInfo (ParseError err) = toInfo err
   toInfo (FromParser err) =
     [("type", "FromParserError"),
-     ("got", show $ prettyError True True err)]
+     ("got", prettyStr $ prettyError True err)]
   toInfo (WrongResult got) =
     [("type", "WrongResult"), ("got", got)]
   toInfo (ExpectedFail got) =
diff --git a/tests/Tests/PrettyTerm.idr b/tests/Tests/PrettyTerm.idr
index 324ac93..bdca2f6 100644
--- a/tests/Tests/PrettyTerm.idr
+++ b/tests/Tests/PrettyTerm.idr
@@ -5,11 +5,11 @@ import Quox.Syntax
 import PrettyExtra
 
 
-parameters (ds : NContext d) (ns : NContext n)
+parameters (ds : BContext d) (ns : BContext n)
   testPrettyT : Term d n -> (uni, asc : String) ->
                 {default uni label : String} -> Test
   testPrettyT t uni asc {label} =
-    testPretty (toSnocList' ds) (toSnocList' ns) t uni asc {label}
+    testPretty (prettyTerm ds ns) t uni asc {label}
 
   testPrettyT1 : Term d n -> (str : String) ->
                  {default str label : String} -> Test
@@ -101,8 +101,8 @@ tests = "pretty printing terms" :- [
   ],
 
   "type universes" :- [
-    testPrettyT [<] [<] (^TYPE 0) "★₀" "Type0",
-    testPrettyT [<] [<] (^TYPE 100) "★₁₀₀" "Type100"
+    testPrettyT [<] [<] (^TYPE 0) "★₀" "Type 0",
+    testPrettyT [<] [<] (^TYPE 100) "★₁₀₀" "Type 100"
   ],
 
   "function types" :- [
@@ -117,7 +117,7 @@ tests = "pretty printing terms" :- [
     testPrettyT [<] [<]
       (^PiY Zero "A" (^TYPE 0) (^Arr Any (^BVT 0) (^BVT 0)))
       "0.(A : ★₀) → ω.A → A"
-      "0.(A : Type0) -> #.A -> A",
+      "0.(A : Type 0) -> #.A -> A",
     testPrettyT [<] [<]
       (^Arr Any (^Arr Any (^FT "A") (^FT "A")) (^FT "A"))
       "ω.(ω.A → A) → A"
@@ -130,7 +130,7 @@ tests = "pretty printing terms" :- [
       (^PiY Zero "P" (^Arr Zero (^FT "A") (^TYPE 0))
         (E $ ^App (^BV 0) (^FT "a")))
       "0.(P : 0.A → ★₀) → P a"
-      "0.(P : 0.A -> Type0) -> P a"
+      "0.(P : 0.A -> Type 0) -> P a"
   ],
 
   "pair types" :- [
@@ -190,7 +190,7 @@ tests = "pretty printing terms" :- [
     testPrettyE [<] [<]
       (^CasePair One (^F "a") (SN $ ^TYPE 1) (SN $ ^TYPE 0))
       "case1 a return ★₁ of { (_, _) ⇒ ★₀ }"
-      "case1 a return Type1 of { (_, _) => Type0 }",
+      "case1 a return Type 1 of { (_, _) => Type 0 }",
     testPrettyT [<] [<]
       (^LamY "u" (E $
         ^CaseEnum One (^F "u")
@@ -208,7 +208,7 @@ tests = "pretty printing terms" :- [
       {label = "type-case ℕ ∷ ★₀ return ★₀ of { ⋯ }"}
       (^TypeCase (^Ann (^Nat) (^TYPE 0)) (^TYPE 0) empty (^Nat))
       "type-case ℕ ∷ ★₀ return ★₀ of { _ ⇒ ℕ }"
-      "type-case Nat :: Type0 return Type0 of { _ => Nat }"
+      "type-case Nat :: Type 0 return Type 0 of { _ => Nat }"
   ],
 
   "annotations" :- [
@@ -231,6 +231,6 @@ tests = "pretty printing terms" :- [
     testPrettyE [<] [<]
       (^Ann (^Arr One (^FT "A") (^FT "A")) (^TYPE 7))
       "(1.A → A) ∷ ★₇"
-      "(1.A -> A) :: Type7"
+      "(1.A -> A) :: Type 7"
   ]
 ]
diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr
index e4a1f4a..59b23f0 100644
--- a/tests/Tests/Typechecker.idr
+++ b/tests/Tests/Typechecker.idr
@@ -6,6 +6,7 @@ import public TypingImpls
 import TAP
 import Quox.EffExtra
 import AstExtra
+import PrettyExtra
 
 
 %hide Prelude.App
@@ -14,20 +15,20 @@ import AstExtra
 
 data Error'
   = TCError Typing.Error
-  | WrongInfer (Term d n) (Term d n)
+  | WrongInfer (BContext d) (BContext n) (Term d n) (Term d n)
   | WrongQOut (QOutput n) (QOutput n)
 
 export
 ToInfo Error' where
   toInfo (TCError e) = toInfo e
-  toInfo (WrongInfer good bad) =
+  toInfo (WrongInfer dnames tnames good bad) =
     [("type", "WrongInfer"),
-     ("wanted", prettyStr True good),
-     ("got", prettyStr True bad)]
+     ("wanted", prettyStr $ prettyTerm dnames tnames good),
+     ("got", prettyStr $ prettyTerm dnames tnames bad)]
   toInfo (WrongQOut good bad) =
     [("type", "WrongQOut"),
-     ("wanted", prettyStr True good),
-     ("wanted", prettyStr True bad)]
+     ("wanted", show good),
+     ("wanted", show bad)]
 
 0 M : Type -> Type
 M = Eff [Except Error', DefsReader]
@@ -116,7 +117,7 @@ parameters (label : String) (act : Lazy (M ()))
 
 inferredTypeEq : TyContext d n -> (exp, got : Term d n) -> M ()
 inferredTypeEq ctx exp got =
-  wrapErr (const $ WrongInfer exp got) $ inj $ lift $
+  wrapErr (const $ WrongInfer ctx.dnames ctx.tnames exp got) $ inj $ lift $
     equalType noLoc ctx exp got
 
 qoutEq : (exp, got : QOutput n) -> M ()
diff --git a/tests/TypingImpls.idr b/tests/TypingImpls.idr
index f747bc2..e84ed32 100644
--- a/tests/TypingImpls.idr
+++ b/tests/TypingImpls.idr
@@ -3,6 +3,7 @@ module TypingImpls
 import TAP
 import public Quox.Typing
 import public Quox.Pretty
+import PrettyExtra
 
 import Derive.Prelude
 %language ElabReflection
@@ -14,4 +15,7 @@ import Derive.Prelude
 %runElab derive "Error" [Show]
 
 export
-ToInfo Error where toInfo err = [("err", show $ prettyError True True err)]
+ToInfo Error where
+  toInfo err =
+    let str = render (Opts 60) $ runPrettyDef $ prettyError True err in
+    [("err", str)]