diff --git a/lib/Quox/Typing/Context.idr b/lib/Quox/Typing/Context.idr
index 00afc1b..31c851b 100644
--- a/lib/Quox/Typing/Context.idr
+++ b/lib/Quox/Typing/Context.idr
@@ -220,26 +220,29 @@ parameters {auto _ : (Eq q, PrettyHL q, IsQty q)} (unicode : Bool)
   pipeD = hl Syntax "|"
 
   export covering
-  prettyTContext : QContext q n -> NContext n -> TContext q d n -> Doc HL
-  prettyTContext qs ns ctx = separate comma $ toList $ go qs ns ctx where
+  prettyTContext : NContext d ->
+                   QContext q n -> NContext n ->
+                   TContext q d n -> Doc HL
+  prettyTContext ds qs xs ctx = separate comma $ toList $ go qs xs ctx where
     go : QContext q m -> NContext m -> TContext q 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 :< runPretty unicode (pretty0M bind)
+      go qs xs ctx :<
+      runPrettyWith unicode (toSnocList' ds) (toSnocList' xs) (pretty0M bind)
 
   export covering
   prettyTyContext : TyContext q d n -> Doc HL
   prettyTyContext (MkTyContext dctx dnames tctx tnames qtys) =
     case dctx of
-      C [<] => prettyTContext qtys tnames tctx
+      C [<] => prettyTContext dnames qtys tnames tctx
       _     => sep [prettyDimEq dnames dctx <++> pipeD,
-                    prettyTContext qtys tnames tctx]
+                    prettyTContext dnames qtys tnames tctx]
 
   export covering
   prettyEqContext : EqContext q n -> Doc HL
   prettyEqContext (MkEqContext dassign dnames tctx tnames qtys) =
     case dassign of
-      [<] => prettyTContext qtys tnames tctx
+      [<] => prettyTContext [<] qtys tnames tctx
       _   => sep [prettyDimEq dnames (fromGround dassign) <++> pipeD,
-                  prettyTContext qtys tnames tctx]
+                  prettyTContext [<] qtys tnames tctx]