diff --git a/lib/Quox/Context.idr b/lib/Quox/Context.idr
index 0d6f60d..773fb06 100644
--- a/lib/Quox/Context.idr
+++ b/lib/Quox/Context.idr
@@ -2,6 +2,7 @@ module Quox.Context
 
 import Quox.Syntax.Shift
 import Quox.Pretty
+import Quox.Name
 
 import Data.DPair
 import Data.Nat
@@ -34,6 +35,14 @@ public export
 Context' : (a : Type) -> (len : Nat) -> Type
 Context' a = Context (\_ => a)
 
+public export
+NContext : Nat -> Type
+NContext = Context' BaseName
+
+
+public export
+head : Context tm (S n) -> tm n
+head (_ :< t) = t
 
 public export
 tail : Context tm (S n) -> Context tm n
@@ -180,18 +189,26 @@ unzip : Telescope (\n => (tm1 n, tm2 n)) from to ->
 unzip [<]             = ([<], [<])
 unzip (tel :< (x, y)) = let (xs, ys) = unzip tel in (xs :< x, ys :< y)
 
+export
+unzip3 : Telescope (\n => (tm1 n, tm2 n, tm3 n)) from to ->
+         (Telescope tm1 from to, Telescope tm2 from to, Telescope tm3 from to)
+unzip3 [<] = ([<], [<], [<])
+unzip3 (tel :< (x, y, z)) =
+  let (xs, ys, zs) = unzip3 tel in (xs :< x, ys :< y, zs :< z)
+
+
 
 export
-lengthPrf : Telescope _ from to -> Subset Nat (\len => len + from = to)
-lengthPrf [<]        = Element 0 Refl
+lengthPrf : Telescope _ from to -> (len ** len + from = to)
+lengthPrf [<]        = (0 ** Refl)
 lengthPrf (tel :< _) =
-  let len = lengthPrf tel in Element (S len.fst) (cong S len.snd)
+  let len = lengthPrf tel in (S len.fst ** cong S len.snd)
 
 export
-lengthPrf0 : Context _ to -> Subset Nat (\len => len = to)
+lengthPrf0 : Context _ to -> (len ** len = to)
 lengthPrf0 ctx =
   let len = lengthPrf ctx in
-  Element len.fst (rewrite sym $ plusZeroRightNeutral len.fst in len.snd)
+  (len.fst ** rewrite sym $ plusZeroRightNeutral len.fst in len.snd)
 
 public export %inline
 length : Telescope {} -> Nat
diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index d7a3b25..fba3987 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -107,22 +107,14 @@ parameters (defs : Definitions' q g)
       E    _          => pure False
 
 
-parameters {auto _ : HasErr q m}
-  export %inline
-  ensure : (a -> Error q) -> (p : a -> Bool) -> (t : a) -> m (So (p t))
-  ensure e p t = case nchoose $ p t of
-    Left  y => pure y
-    Right _ => throwError $ e t
+export
+ensureTyCon : HasErr q m =>
+              (ctx : EqContext q n) -> (t : Term q 0 n) -> m (So (isTyCon t))
+ensureTyCon ctx t = case nchoose $ isTyCon t of
+  Left  y => pure y
+  Right n => throwError $ NotType (toTyContext ctx) (t // shift0 ctx.dimLen)
 
-  export %inline
-  ensureTyCon : (ctx : EqContext q n) -> (t : Term q 0 n) -> m (So (isTyCon t))
-  ensureTyCon ctx t = case nchoose $ isTyCon t of
-    Left  y => pure y
-    Right n =>
-      let (d ** ctx) = toTyContext ctx in
-      throwError $ NotType ctx (t // shift0 d)
-
-parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
+parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
   mutual
     namespace Term
       ||| `compare0 ctx ty s t` compares `s` and `t` at type `ty`, according to
@@ -153,24 +145,27 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
                   m ()
       compare0' ctx (TYPE _) s t = compareType ctx s t
 
-      compare0' ctx ty@(Pi {arg, res, _}) s t {n} = local {mode := Equal} $
+      compare0' ctx ty@(Pi {qty, arg, res}) s t {n} = local {mode := Equal} $
         case (s, t) of
-          --          Γ, x : A ⊢ s = t : B
-          -- -----------------------------------------
-          --  Γ ⊢ (λx ⇒ s) = (λx ⇒ t) : (π·x : A) → B
+          --           Γ, x : A ⊢ s = t : B
+          -- -------------------------------------------
+          --  Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) : (π·x : A) → B
           (Lam b1, Lam b2) => compare0 ctx' res.term b1.term b2.term
 
           --       Γ, x : A ⊢ s = e x : B
-          -- ----------------------------------
-          --  Γ ⊢ (λx ⇒ s) = e : (π·x : A) → B
+          -- -----------------------------------
+          --  Γ ⊢ (λ x ⇒ s) = e : (π·x : A) → B
           (E e,   Lam b) => eta e b
           (Lam b, E e)   => eta e b
 
           (E e, E f) => Elim.compare0 ctx e f
-          _ => throwError $ WrongType ctx ty s t
+
+          (Lam _, t) => throwError $ WrongType ctx ty t
+          (E _,   t) => throwError $ WrongType ctx ty t
+          (s,     _) => throwError $ WrongType ctx ty s
         where
           ctx' : EqContext q (S n)
-          ctx' = extendTy res.name arg ctx
+          ctx' = extendTy qty res.name arg ctx
 
           eta : Elim q 0 n -> ScopeTerm q 0 n -> m ()
           eta e (S _ (Y b)) = compare0 ctx' res.term (toLamBody e) b
@@ -179,16 +174,19 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
       compare0' ctx ty@(Sig {fst, snd, _}) s t = local {mode := Equal} $
         case (s, t) of
           --  Γ ⊢ s₁ = t₁ : A     Γ ⊢ s₂ = t₂ : B{s₁/x}
-          -- -------------------------------------------
-          --     Γ ⊢ (s₁,t₁) = (s₂,t₂) : (x : A) × B
+          -- --------------------------------------------
+          --     Γ ⊢ (s₁, t₁) = (s₂,t₂) : (x : A) × B
           --
           -- [todo] η for π ≥ 0 maybe
           (Pair sFst sSnd, Pair tFst tSnd) => do
             compare0 ctx fst sFst tFst
             compare0 ctx (sub1 snd (sFst :# fst)) sSnd tSnd
 
-          (E e, E f) => compare0 ctx e f
-          _ => throwError $ WrongType ctx ty s t
+          (E e, E f) => Elim.compare0 ctx e f
+
+          (Pair {}, t) => throwError $ WrongType ctx ty t
+          (E _,     t) => throwError $ WrongType ctx ty t
+          (s,       _) => throwError $ WrongType ctx ty s
 
       compare0' ctx ty@(Enum tags) s t = local {mode := Equal} $
         case (s, t) of
@@ -197,8 +195,11 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
           --
           -- t ∈ ts is in the typechecker, not here, ofc
           (Tag t1, Tag t2) => unless (t1 == t2) $ clashT ctx ty s t
-          (E e,    E f)    => compare0 ctx e f
-          _                => throwError $ WrongType ctx ty s t
+          (E e,    E f)    => Elim.compare0 ctx e f
+
+          (Tag _, t) => throwError $ WrongType ctx ty t
+          (E _,   t) => throwError $ WrongType ctx ty t
+          (s,     _) => throwError $ WrongType ctx ty s
 
       compare0' _ (Eq {}) _ _ =
         -- ✨ uip ✨
@@ -209,8 +210,8 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
       compare0' ctx ty@(E _) s t = do
         -- a neutral type can only be inhabited by neutral values
         -- e.g. an abstract value in an abstract type, bound variables, …
-        E e <- pure s | _ => throwError $ WrongType ctx ty s t
-        E f <- pure t | _ => throwError $ WrongType ctx ty s t
+        E e <- pure s | _ => throwError $ WrongType ctx ty s
+        E f <- pure t | _ => throwError $ WrongType ctx ty t
         Elim.compare0 ctx e f
 
     ||| compares two types, using the current variance `mode` for universes.
@@ -247,7 +248,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
       --  Γ ⊢ (π·x : A₁) → B₁ <: (π·x : A₂) → B₂
       expectEqualQ sQty tQty
       local {mode $= flip} $ compareType ctx sArg tArg -- contra
-      compareType (extendTy sRes.name sArg ctx) sRes.term tRes.term
+      compareType (extendTy zero sRes.name sArg ctx) sRes.term tRes.term
 
     compareType' ctx (Sig {fst = sFst, snd = sSnd, _})
                      (Sig {fst = tFst, snd = tSnd, _}) = do
@@ -255,7 +256,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
       -- --------------------------------------
       --   Γ ⊢ (x : A₁) × B₁ <: (x : A₂) × B₂
       compareType ctx sFst tFst
-      compareType (extendTy sSnd.name sFst ctx) sSnd.term tSnd.term
+      compareType (extendTy zero sSnd.name sFst ctx) sSnd.term tSnd.term
 
     compareType' ctx (Eq {ty = sTy, l = sl, r = sr, _})
                      (Eq {ty = tTy, l = tl, r = tr, _}) = do
@@ -365,10 +366,10 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
         local {mode := Equal} $ do
           compare0 ctx e f
           ety <- computeElimType ctx e (noOr1 ne)
-          compareType (extendTy eret.name ety ctx) eret.term fret.term
+          compareType (extendTy zero eret.name ety ctx) eret.term fret.term
           (fst, snd) <- expectSigE defs ctx ety
           let [x, y] = ebody.names
-          Term.compare0 (extendTyN [< (x, fst), (y, snd.term)] ctx)
+          Term.compare0 (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx)
                         (substCasePairRet ety eret)
                         ebody.term fbody.term
           expectEqualQ epi fpi
@@ -379,7 +380,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
         local {mode := Equal} $ do
           compare0 ctx e f
           ety <- computeElimType ctx e (noOr1 ne)
-          compareType (extendTy eret.name ety ctx) eret.term fret.term
+          compareType (extendTy zero eret.name ety ctx) eret.term fret.term
           for_ !(expectEnumE defs ctx ety) $ \t =>
             compare0 ctx (sub1 eret $ Tag t :# ety)
               !(lookupArm t earms) !(lookupArm t farms)
@@ -402,7 +403,8 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
       compare0' ctx e@(_ :# _) f        _ _ = clashE ctx e f
 
 
-parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)} (ctx : TyContext q d n)
+parameters {auto _ : (HasDefs' q _ m, HasErr q m, IsQty q)}
+           (ctx : TyContext q d n)
   -- [todo] only split on the dvars that are actually used anywhere in
   -- the calls to `splits`
 
diff --git a/lib/Quox/Pretty.idr b/lib/Quox/Pretty.idr
index 9deb2d4..96b9a36 100644
--- a/lib/Quox/Pretty.idr
+++ b/lib/Quox/Pretty.idr
@@ -172,11 +172,15 @@ export %inline
 pretty0M : (PrettyHL a, HasEnv m) => a -> m (Doc HL)
 pretty0M = local {prec := Outer} . prettyM
 
+export %inline
+runPretty : (unicode : Bool) -> Reader PrettyEnv a -> a
+runPretty unicode act =
+  let env = MakePrettyEnv {dnames = [<], tnames = [<], unicode, prec = Outer} in
+  runReader env act
+
 export %inline
 pretty0 : PrettyHL a => (unicode : Bool) -> a -> Doc HL
-pretty0 unicode x =
-  let env = MakePrettyEnv {dnames = [], tnames = [], unicode, prec = Outer} in
-  runReader env $ prettyM x
+pretty0 unicode = runPretty unicode . prettyM
 
 
 export
diff --git a/lib/Quox/Syntax/Dim.idr b/lib/Quox/Syntax/Dim.idr
index 5145d0e..0f90b35 100644
--- a/lib/Quox/Syntax/Dim.idr
+++ b/lib/Quox/Syntax/Dim.idr
@@ -1,8 +1,10 @@
 module Quox.Syntax.Dim
 
+import Quox.Name
 import Quox.Syntax.Var
 import Quox.Syntax.Subst
 import Quox.Pretty
+import Quox.Context
 
 import Decidable.Equality
 import Control.Function
@@ -31,29 +33,26 @@ data Dim : Nat -> Type where
   B : Var d -> Dim d
 %name Dim.Dim p, q
 
-private %inline
-drepr : Dim n -> Either DimConst (Var n)
-drepr (K k) = Left k
-drepr (B x) = Right x
-
-export Eq  (Dim n) where (==) = (==) `on` drepr
-export Ord (Dim n) where compare = compare `on` drepr
-
-export
-Show (Dim n) where
-  show (K k) = showCon App "K" $ show k
-  show (B i) = showCon App "B" $ show i
+%runElab deriveIndexed "Dim" [Eq, Ord, Show]
 
 export
 PrettyHL DimConst where
-  prettyM Zero = hl Dim <$> ifUnicode "𝟬" "0"
-  prettyM One  = hl Dim <$> ifUnicode "𝟭" "1"
+  prettyM = pure . hl Dim . 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`;
diff --git a/lib/Quox/Syntax/Qty/Three.idr b/lib/Quox/Syntax/Qty/Three.idr
index 47cb1a4..6bc78ba 100644
--- a/lib/Quox/Syntax/Qty/Three.idr
+++ b/lib/Quox/Syntax/Qty/Three.idr
@@ -19,9 +19,9 @@ export
 PrettyHL Three where
   prettyM pi = hl Qty <$>
     case pi of
-      Zero => ifUnicode "𝟬" "0"
-      One  => ifUnicode "𝟭" "1"
-      Any  => ifUnicode "𝛚" "*"
+      Zero => pure "0"
+      One  => pure "1"
+      Any  => ifUnicode "ω" "#"
 
 public export
 DecEq Three where
@@ -88,6 +88,7 @@ data IsGlobal3 : Pred Three where
   GZero : IsGlobal3 Zero
   GAny  : IsGlobal3 Any
 
+public export
 isGlobal3 : Dec1 IsGlobal3
 isGlobal3 Zero = Yes GZero
 isGlobal3 One  = No $ \case _ impossible
diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index bcc4f69..a0e8cc7 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -3,6 +3,7 @@ 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
@@ -42,16 +43,26 @@ prettyUnivSuffix l =
     '0' => '₀'; '1' => '₁'; '2' => '₂'; '3' => '₃'; '4' => '₄'
     '5' => '₅'; '6' => '₆'; '7' => '₇'; '8' => '₈'; '9' => '₉'; _ => c
 
+export
+prettyUniverse : Universe -> Doc HL
+prettyUniverse = hl Syntax . pretty
+
+export
+prettyBind : PrettyHL a => PrettyHL q => Pretty.HasEnv m =>
+             List q -> BaseName -> a -> m (Doc HL)
+prettyBind qtys x s = do
+  var <- prettyQtyBinds qtys $ TV x
+  s   <- withPrec Outer $ prettyM s
+  pure $ var <++> colonD <%%> hang 2 s
+
 export
 prettyBindType : PrettyHL a => PrettyHL b => PrettyHL q =>
                  Pretty.HasEnv m =>
                  List q -> BaseName -> a -> Doc HL -> b -> m (Doc HL)
 prettyBindType qtys x s arr t = do
-  var <- prettyQtyBinds qtys $ TV x
-  s   <- withPrec Outer $ prettyM s
-  t   <- withPrec Outer $ under T x $ prettyM t
-  let bind = parens (var <++> colonD <%%> hang 2 s)
-  parensIfM Outer $ hang 2 $ bind <%%> t
+  bind <- prettyBind qtys x s
+  t    <- withPrec Outer $ under T x $ prettyM t
+  parensIfM Outer $ hang 2 $ parens bind <++> arr <%%> t
 
 export
 prettyArm : PrettyHL a => Pretty.HasEnv m =>
@@ -144,7 +155,7 @@ parameters (showSubsts : Bool)
     prettyM (DLam (S i t)) =
       let GotDLams {names, body, _} = getDLams' i t.term Refl in
       prettyLams (Just !dlamD) D (toList names) body
-    prettyM (E e) = bracks <$> prettyM e
+    prettyM (E e) = prettyM e
     prettyM (CloT s th) =
       if showSubsts then
         parensIfM SApp . hang 2 =<<
@@ -207,3 +218,16 @@ PrettyHL q => PrettyHL (Term q d n) where
 export covering %inline
 PrettyHL q => PrettyHL (Elim q d n) where
   prettyM = prettyM @{ElimSubst False}
+
+
+export covering
+prettyTerm : PrettyHL q => (unicode : Bool) ->
+             (dnames : NContext d) -> (tnames : NContext n) ->
+             Term q d n -> Doc HL
+prettyTerm unicode dnames tnames term =
+  let env = MakePrettyEnv {
+    dnames = toSnocList' dnames,
+    tnames = toSnocList' tnames,
+    unicode, prec = Outer
+  } in
+  runReader env $ prettyM term
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index cc27f22..b24d6b1 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -128,7 +128,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- if Ψ | Γ, x : A ⊢ σ · t ⇐ B ⊳ Σ, ρ·x
     -- with ρ ≤ σπ
     let qty' = sg.fst * qty
-    qout <- checkC (extendTy body.name arg ctx) sg body.term res.term
+    qout <- checkC (extendTy qty' body.name arg ctx) sg body.term res.term
     -- then Ψ | Γ ⊢ σ · (λx ⇒ t) ⇐ (π·x : A) → B ⊳ Σ
     popQ qty' qout
 
@@ -190,8 +190,8 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     checkTypeC ctx arg u
     -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
     case res.body of
-      Y res' => checkTypeC (extendTy res.name arg ctx) res' u
-      N res' => checkTypeC ctx                         res' u
+      Y res' => checkTypeC (extendTy zero res.name arg ctx) res' u
+      N res' => checkTypeC ctx                              res' u
     -- then Ψ | Γ ⊢₀ (π·x : A) → B ⇐ Type ℓ
 
   checkType' ctx t@(Lam {}) u =
@@ -202,8 +202,8 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     checkTypeC ctx fst u
     -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
     case snd.body of
-      Y snd' => checkTypeC (extendTy snd.name fst ctx) snd' u
-      N snd' => checkTypeC ctx                         snd' u
+      Y snd' => checkTypeC (extendTy zero snd.name fst ctx) snd' u
+      N snd' => checkTypeC ctx                              snd' u
     -- then Ψ | Γ ⊢₀ (x : A) × B ⇐ Type ℓ
 
   checkType' ctx t@(Pair {}) u =
@@ -285,15 +285,15 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- if Ψ | Γ ⊢ σ · pair ⇒ (x : A) × B ⊳ Σ₁
     pairres <- inferC ctx sg pair
     -- if Ψ | Γ, p : (x : A) × B ⊢₀ ret ⇐ Type
-    checkTypeC (extendTy ret.name pairres.type ctx) ret.term Nothing
+    checkTypeC (extendTy zero ret.name pairres.type ctx) ret.term Nothing
     (tfst, tsnd) <- expectSig !ask ctx pairres.type
     -- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐
     --    ret[(x, y) ∷ (x : A) × B/p] ⊳ Σ₂, ρ₁·x, ρ₂·y
     -- with ρ₁, ρ₂ ≤ πσ
     let [x, y]  = body.names
-        bodyctx = extendTyN [< (x, tfst), (y, tsnd.term)] ctx
-        bodyty  = substCasePairRet pairres.type ret
         pisg    = pi * sg.fst
+        bodyctx = extendTyN [< (pisg, x, tfst), (pisg, y, tsnd.term)] ctx
+        bodyty  = substCasePairRet pairres.type ret
     bodyout <- checkC bodyctx sg body.term bodyty
     -- then Ψ | Γ ⊢ σ · case ⋯ ⇒ ret[pair/p] ⊳ πΣ₁ + Σ₂
     pure $ InfRes {
@@ -307,7 +307,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁
     tres <- inferC ctx sg t
     -- if Ψ | Γ, x : {ts} ⊢₀ A ⇐ Type
-    checkTypeC (extendTy ret.name tres.type ctx) ret.term Nothing
+    checkTypeC (extendTy zero ret.name tres.type ctx) ret.term Nothing
     -- if for each "a ⇒ s" in arms,
     --   Ψ | Γ ⊢ σ · s ⇐ A[a ∷ {ts}/x] ⊳ Σ₂
     -- for fixed Σ₂
@@ -325,7 +325,8 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     allEqual [] = pure $ zeroFor ctx
     allEqual lst@((x, _) :: xs) =
       if all (\y => x == fst y) xs then pure x
-      else throwError $ BadCaseQtys ctx lst
+      else throwError $ BadCaseQtys ctx $
+             map (\(qs, t, s) => (qs, Tag t, s)) lst
 
   infer' ctx sg (fun :% dim) = do
     -- if Ψ | Γ ⊢ σ · f ⇒ Eq [i ⇒ A] l r ⊳ Σ
diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr
index 94a1b13..40e7339 100644
--- a/lib/Quox/Typing.idr
+++ b/lib/Quox/Typing.idr
@@ -110,30 +110,20 @@ parameters {auto _ : HasErr q m} (defs : Definitions' q _)
   parameters (ctx : EqContext q n)
     export covering %inline
     expectTYPEE : Term q 0 n -> m Universe
-    expectTYPEE t =
-      let ctx = delay (toTyContext ctx) in
-      expectTYPE_ (DPair.snd ctx) (shift0 $ DPair.fst ctx) t
+    expectTYPEE t = expectTYPE_ (toTyContext ctx) (shift0 ctx.dimLen) t
 
     export covering %inline
     expectPiE : Term q 0 n -> m (q, Term q 0 n, ScopeTerm q 0 n)
-    expectPiE t =
-      let ctx = delay (toTyContext ctx) in
-      expectPi_ (DPair.snd ctx) (shift0 $ DPair.fst ctx) t
+    expectPiE t = expectPi_ (toTyContext ctx) (shift0 ctx.dimLen) t
 
     export covering %inline
     expectSigE : Term q 0 n -> m (Term q 0 n, ScopeTerm q 0 n)
-    expectSigE t =
-      let ctx = delay (toTyContext ctx) in
-      expectSig_ (DPair.snd ctx) (shift0 $ DPair.fst ctx) t
+    expectSigE t = expectSig_ (toTyContext ctx) (shift0 ctx.dimLen) t
 
     export covering %inline
     expectEnumE : Term q 0 n -> m (SortedSet TagVal)
-    expectEnumE t =
-      let ctx = delay (toTyContext ctx) in
-      expectEnum_ (DPair.snd ctx) (shift0 $ DPair.fst ctx) t
+    expectEnumE t = expectEnum_ (toTyContext ctx) (shift0 ctx.dimLen) t
 
     export covering %inline
     expectEqE : Term q 0 n -> m (DScopeTerm q 0 n, Term q 0 n, Term q 0 n)
-    expectEqE t =
-      let ctx = delay (toTyContext ctx) in
-      expectEq_ (DPair.snd ctx) (shift0 $ DPair.fst ctx) t
+    expectEqE t = expectEq_ (toTyContext ctx) (shift0 ctx.dimLen) t
diff --git a/lib/Quox/Typing/Context.idr b/lib/Quox/Typing/Context.idr
index 53807c8..c1c9dd2 100644
--- a/lib/Quox/Typing/Context.idr
+++ b/lib/Quox/Typing/Context.idr
@@ -2,10 +2,15 @@ module Quox.Typing.Context
 
 import Quox.Syntax
 import Quox.Context
+import Quox.Pretty
 
 %default total
 
 
+public export
+QContext : Type -> Nat -> Type
+QContext = Context'
+
 public export
 TContext : Type -> Nat -> Nat -> Type
 TContext q d = Context (Term q d)
@@ -14,10 +19,6 @@ public export
 QOutput : Type -> Nat -> Type
 QOutput = Context'
 
-public export
-NContext : Nat -> Type
-NContext = Context' BaseName
-
 public export
 DimAssign : Nat -> Type
 DimAssign = Context' DimConst
@@ -30,17 +31,19 @@ record TyContext q d n where
   dnames : NContext d
   tctx   : TContext q d n
   tnames : NContext n
+  qtys   : QContext q n -- only used for printing
 %name TyContext ctx
 
 
 public export
 record EqContext q n where
   constructor MkEqContext
-  -- (only used for errors; not needed by the actual equality test)
-  dassign : DimAssign dimLen
-  dnames  : NContext dimLen
+  {dimLen : Nat}
+  dassign : DimAssign dimLen -- only used for printing
+  dnames  : NContext dimLen -- only used for printing
   tctx    : TContext q 0 n
   tnames  : NContext n
+  qtys    : QContext q n -- only used for printing
 %name EqContext ctx
 
 
@@ -56,17 +59,20 @@ namespace TContext
 namespace TyContext
   public export %inline
   empty : TyContext q 0 0
-  empty = MkTyContext {dctx = new, dnames = [<], tctx = [<], tnames = [<]}
+  empty =
+    MkTyContext {dctx = new, dnames = [<], tctx = [<], tnames = [<], qtys = [<]}
 
   export %inline
-  extendTyN : Telescope (\n => (BaseName, Term q d n)) from to ->
+  extendTyN : Telescope (\n => (q, BaseName, Term q d n)) from to ->
               TyContext q d from -> TyContext q d to
   extendTyN xss ctx =
-    let (xs, ss) = unzip xss in {tctx $= (. ss), tnames $= (. xs)} ctx
+    let (qs, xs, ss) = unzip3 xss in
+    {qtys $= (. qs), tctx $= (. ss), tnames $= (. xs)} ctx
 
   export %inline
-  extendTy : BaseName -> Term q d n -> TyContext q d n -> TyContext q d (S n)
-  extendTy x s = extendTyN [< (x, s)]
+  extendTy : q -> BaseName -> Term q d n -> TyContext q d n ->
+             TyContext q d (S n)
+  extendTy q x s = extendTyN [< (q, x, s)]
 
   export %inline
   extendDim : BaseName -> TyContext q d n -> TyContext q (S d) n
@@ -98,41 +104,96 @@ makeDAssign (Shift SZ)   = [<]
 makeDAssign (K e ::: th) = makeDAssign th :< e
 
 export
-makeEqContext : TyContext q d n -> DSubst d 0 -> EqContext q n
-makeEqContext ctx th = MkEqContext {
+makeEqContext' : {d : Nat} -> TyContext q d n -> DSubst d 0 -> EqContext q n
+makeEqContext' ctx th = MkEqContext {
   dassign = makeDAssign th,
   dnames  = ctx.dnames,
   tctx    = map (// th) ctx.tctx,
-  tnames  = ctx.tnames
+  tnames  = ctx.tnames,
+  qtys    = ctx.qtys
 }
 
+export
+makeEqContext : TyContext q d n -> DSubst d 0 -> EqContext q n
+makeEqContext ctx@(MkTyContext {dnames, _}) th =
+  let (d' ** Refl) = lengthPrf0 dnames in makeEqContext' ctx th
+
 namespace EqContext
   public export %inline
   empty : EqContext q 0
-  empty = MkEqContext [<] [<] [<] [<]
+  empty = MkEqContext {
+    dassign = [<], dnames = [<], tctx = [<], tnames = [<], qtys = [<]
+  }
 
   export %inline
-  extendTyN : Telescope (\n => (BaseName, Term q 0 n)) from to ->
+  extendTyN : Telescope (\n => (q, BaseName, Term q 0 n)) from to ->
               EqContext q from -> EqContext q to
   extendTyN tel ctx =
-    let (xs, ss) = unzip tel in {tctx $= (. ss), tnames $= (. xs)} ctx
+    let (qs, xs, ss) = unzip3 tel in
+    {qtys $= (. qs), tctx $= (. ss), tnames $= (. xs)} ctx
 
   export %inline
-  extendTy : BaseName -> Term q 0 n -> EqContext q n -> EqContext q (S n)
-  extendTy x s = extendTyN [< (x, s)]
+  extendTy : q -> BaseName -> Term q 0 n -> EqContext q n -> EqContext q (S n)
+  extendTy q x s = extendTyN [< (q, x, s)]
 
   export %inline
   extendDim : BaseName -> DimConst -> EqContext q n -> EqContext q n
   extendDim x e ctx = {dassign $= (:< e), dnames $= (:< x)} ctx
 
   export
-  toTyContext : (e : EqContext q n) -> (d ** TyContext q d n)
-  toTyContext (MkEqContext {dassign, dnames, tctx, tnames})
-      with (lengthPrf0 dnames)
-    _ | Element d eq =
-      (d ** MkTyContext {
-        dctx   = rewrite eq in fromGround dassign,
-        dnames = rewrite eq in dnames,
-        tctx   = map (// shift0 d) tctx,
-        tnames
-      })
+  toTyContext : (e : EqContext q n) -> TyContext q e.dimLen n
+  toTyContext (MkEqContext {dimLen, dassign, dnames, tctx, tnames, qtys}) =
+    MkTyContext {
+      dctx = fromGround dassign,
+      tctx = map (// shift0 dimLen) tctx,
+      dnames, tnames, qtys
+    }
+
+
+parameters {auto _ : (Eq q, PrettyHL q)} (unicode : Bool)
+  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
+    go : QContext q m -> NContext m -> TContext q d m -> SnocList (Doc HL)
+    go [<]       [<]       [<] = [<]
+    go (qs :< q) (xs :< x) (ctx :< t) =
+      go qs xs ctx :< runPretty unicode (prettyBind [q] x t)
+
+  private
+  prettyDVars : NContext d -> Doc HL
+  prettyDVars ds = hseparate comma $ map (pretty0 unicode . DV) $ toList' ds
+
+  export
+  prettyDimEq1 : (PrettyHL a, PrettyHL b) => NContext d -> a -> b -> Doc HL
+  prettyDimEq1 ds p q = runPretty unicode $
+    local {dnames := toSnocList' ds} $ do
+      p <- pretty0M p; q <- pretty0M q
+      pure $ hsep [p, hl Syntax "=", q]
+
+  export
+  prettyDimEqCons : NContext d -> DimEq' d -> Doc HL
+  prettyDimEqCons ds eqs = hseparate comma $ toList $ go ds eqs
+  where
+    go : NContext e -> Context (Maybe . Dim) e -> SnocList (Doc HL)
+    go [<]       [<]              = [<]
+    go (ds :< _) (eqs :< Nothing) = go ds eqs
+    go (ds :< x) (eqs :< Just d)  = go ds eqs :< prettyDimEq1 ds (DV x) d
+
+  export
+  prettyDimEq : NContext d -> DimEq d -> Doc HL
+  prettyDimEq ds ZeroIsOne =
+    prettyDVars ds <+> comma <++> prettyDimEq1 [<] Zero One
+  prettyDimEq ds (C eqs) =
+    prettyDVars ds <+> comma <%%> prettyDimEqCons ds eqs
+
+  export covering
+  prettyTyContext : TyContext q d n -> Doc HL
+  prettyTyContext (MkTyContext dctx dnames tctx tnames qtys) =
+    sep [prettyDimEq dnames dctx <++> hl Syntax "|",
+         prettyTContext qtys tnames tctx]
+
+  export covering
+  prettyEqContext : EqContext q n -> Doc HL
+  prettyEqContext (MkEqContext dassign dnames tctx tnames qtys) =
+    sep [prettyDimEqCons dnames (fromGround' dassign) <++> hl Syntax "|",
+         prettyTContext qtys tnames tctx]
diff --git a/lib/Quox/Typing/Error.idr b/lib/Quox/Typing/Error.idr
index 9f1e131..cf87e79 100644
--- a/lib/Quox/Typing/Error.idr
+++ b/lib/Quox/Typing/Error.idr
@@ -19,7 +19,7 @@ data Error q
 | ExpectedEq   (TyContext q d n) (Term q d n)
 | BadUniverse  Universe Universe
 | TagNotIn     TagVal (SortedSet TagVal)
-| BadCaseQtys  (TyContext q d n) (List (QOutput q n, TagVal, Term q d n))
+| BadCaseQtys  (TyContext q d n) (List (QOutput q n, Term q d n, Term q d n))
 
 -- first term arg of ClashT is the type
 | ClashT  (EqContext q n) EqMode (Term q 0 n) (Term q 0 n) (Term q 0 n)
@@ -30,7 +30,7 @@ data Error q
 | NotInScope Name
 
 | NotType (TyContext q d n) (Term q d n)
-| WrongType (EqContext q n) (Term q 0 n) (Term q 0 n) (Term q 0 n)
+| WrongType (EqContext q n) (Term q 0 n) (Term q 0 n)
 
 -- extra context
 | WhileChecking
@@ -136,3 +136,167 @@ parameters {auto _ : HasErr q m}
   expectModeU : EqMode -> Universe -> Universe -> m ()
   expectModeU mode = expect (ClashU mode) $ ucmp mode
 
+
+private
+prettyMode : EqMode -> Doc HL
+prettyMode Equal = "equal to"
+prettyMode Sub   = "a subtype of"
+prettyMode Super = "a supertype of"
+
+private
+prettyModeU : EqMode -> Doc HL
+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 Nothing  = "is a type"
+isTypeInUniverse (Just k) = "is a type in universe" <++> prettyUniverse k
+
+parameters {auto _ : (Eq q, PrettyHL q)} (unicode : Bool)
+  private
+  termt : TyContext q d n -> Term q d n -> Doc HL
+  termt ctx = hang 4 . prettyTerm unicode ctx.dnames ctx.tnames
+
+  private
+  terme : EqContext q n -> Term q 0 n -> Doc HL
+  terme ctx = hang 4 . prettyTerm unicode [<] ctx.tnames
+
+  private
+  dissectCaseQtys : TyContext q d n ->
+                    NContext n' -> List (QOutput q n', Term q d n, z) ->
+                    List (Doc HL)
+  dissectCaseQtys ctx [<]        arms = []
+  dissectCaseQtys ctx (tel :< x) arms =
+    let qs = map (head . fst) arms
+        tl = dissectCaseQtys ctx tel (map (mapFst tail) arms)
+    in
+    if allSame qs then tl else
+    ("-" <++> asep [hsep [pretty0 unicode $ TV x, "is used with quantities"],
+                    hseparate comma $ map (pretty0 unicode) qs]) :: tl
+  where
+    allSame : List q -> Bool
+    allSame []        = True
+    allSame (q :: qs) = all (== q) qs
+
+  export
+  prettyWhnfError : WhnfError -> Doc HL
+  prettyWhnfError = \case
+    MissingEnumArm tag tags =>
+      sep [hsep ["the tag", hl Tag $ pretty tag, "is not contained in"],
+           termt empty $ Enum $ fromList tags]
+
+  -- [todo] only show some contexts, probably
+  export
+  prettyError : (showContext : Bool) -> Error q -> Doc HL
+  prettyError showContext = \case
+    ExpectedTYPE ctx s =>
+      sep ["expected a type universe, but got", termt ctx s]
+
+    ExpectedPi ctx s =>
+      sep ["expected a function type, but got", termt ctx s]
+
+    ExpectedSig ctx s =>
+      sep ["expected a pair type, but got", termt ctx s]
+
+    ExpectedEnum ctx s =>
+      sep ["expected an enumeration type, but got", termt ctx s]
+
+    ExpectedEq ctx s =>
+      sep ["expected an equality type, but got", termt ctx s]
+
+    BadUniverse k l =>
+      sep ["the universe level", prettyUniverse k,
+           "is not strictly less than", prettyUniverse l]
+
+    TagNotIn tag set =>
+      sep [sep ["tag", prettyTag tag, "is not contained in"],
+           termt empty (Enum set)]
+
+    BadCaseQtys ctx arms =>
+      hang 4 $ sep $
+        "inconsistent variable usage in case arms" ::
+        dissectCaseQtys ctx ctx.tnames arms
+
+    ClashT ctx mode ty s t =>
+      inEContext ctx $
+      sep ["the term", terme ctx s,
+           hsep ["is not", prettyMode mode], terme ctx t,
+           "at type", terme ctx ty]
+
+    ClashTy ctx mode a b =>
+      inEContext ctx $
+      sep ["the type", terme ctx a,
+           hsep ["is not", prettyMode mode], terme ctx b]
+
+    ClashE ctx mode e f =>
+      inEContext ctx $
+      sep ["the term", terme ctx $ E e,
+           hsep ["is not", prettyMode mode], terme ctx $ E f]
+
+    ClashU mode k l =>
+      sep ["the universe level", prettyUniverse k,
+           hsep ["is not", prettyMode mode], prettyUniverse l]
+
+    ClashQ pi rh =>
+      sep ["the quantity", pretty0 unicode pi,
+           "is not equal to", pretty0 unicode rh]
+
+    NotInScope x =>
+      hsep [hl' Free $ pretty0 unicode x, "is not in scope"]
+
+    NotType ctx s =>
+      inTContext ctx $
+      sep ["the term", termt ctx s, "is not a type"]
+
+    WrongType ctx ty s =>
+      inEContext ctx $
+      sep ["the term", terme ctx s,
+           "cannot have type", terme ctx ty]
+
+    WhileChecking ctx pi s a err =>
+      vsep [inTContext ctx $
+              sep ["while checking", termt ctx s,
+                   "has type", termt ctx a,
+                   hsep ["with quantity", pretty0 unicode pi]],
+            prettyError showContext err]
+
+    WhileCheckingTy ctx a k err =>
+      vsep [inTContext ctx $
+              sep ["while checking", termt ctx a,
+                   isTypeInUniverse k],
+            prettyError showContext err]
+
+    WhileInferring ctx pi e err =>
+      vsep [inTContext ctx $
+              sep ["while inferring the type of", termt ctx $ E e,
+                   hsep ["with quantity", pretty0 unicode pi]],
+            prettyError showContext err]
+
+    WhileComparingT ctx mode s t a err =>
+      vsep [inEContext ctx $
+              sep ["while checking that", terme ctx s,
+                   hsep ["is", prettyMode mode], terme ctx t,
+                   "at type", terme ctx a],
+            prettyError showContext err]
+
+    WhileComparingE ctx mode e f err =>
+      vsep [inEContext ctx $
+              sep ["while checking that", terme ctx $ E e,
+                   hsep ["is", prettyMode mode], terme ctx $ E f],
+            prettyError showContext err]
+
+    WhnfError err => prettyWhnfError err
+  where
+    inTContext : TyContext q d n -> Doc HL -> Doc HL
+    inTContext ctx doc =
+      if showContext then
+        vsep [sep ["in context", prettyTyContext unicode ctx], doc]
+      else doc
+
+    inEContext : EqContext q n -> Doc HL -> Doc HL
+    inEContext ctx doc =
+      if showContext then
+        vsep [sep ["in context", prettyEqContext unicode ctx], doc]
+      else doc
diff --git a/tests/Tests.idr b/tests/Tests.idr
index c8c0ecf..300314a 100644
--- a/tests/Tests.idr
+++ b/tests/Tests.idr
@@ -17,7 +17,10 @@ allTests = [
   Typechecker.tests,
   Lexer.tests,
   Parser.tests,
-  FromPTerm.tests
+  FromPTerm.tests,
+  todo "DimEq",
+  todo "Pretty term & dim",
+  todo "Pretty dctx/tctx/tyctx/eqctx"
 ]
 
 main : IO ()
diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr
index 9bc1c58..a339712 100644
--- a/tests/Tests/Equal.idr
+++ b/tests/Tests/Equal.idr
@@ -184,53 +184,55 @@ tests = "equality & subtyping" :- [
 
     testEq "∥ x : (a ≡ a' : A), y : (a ≡ a' : A) ⊢ x = y  (bound)" $
       let ty : forall n. Term Three 0 n := Eq0 (FT "A") (FT "a") (FT "a'") in
-      equalE (extendTyN [< ("x", ty), ("y", ty)] empty)
+      equalE (extendTyN [< (Any, "x", ty), (Any, "y", ty)] empty)
         (BV 0) (BV 1),
 
     testEq "∥ x : [(a ≡ a' : A) ∷ Type 0], y : [ditto] ⊢ x = y" $
       let ty : forall n. Term Three 0 n :=
             E (Eq0 (FT "A") (FT "a") (FT "a'") :# TYPE 0) in
-      equalE (extendTyN [< ("x", ty), ("y", ty)] empty)
+      equalE (extendTyN [< (Any, "x", ty), (Any, "y", ty)] empty)
         (BV 0) (BV 1),
 
     testEq "E ≔ a ≡ a' : A, EE ≔ E ∥ x : EE, y : EE ⊢ x = y"
            {globals = defGlobals `mergeLeft` fromList
               [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))),
                ("EE", mkDef zero (TYPE 0) (FT "E"))]} $
-      equalE (extendTyN [< ("x", FT "EE"), ("y", FT "EE")] empty)
+      equalE (extendTyN [< (Any, "x", FT "EE"), (Any, "y", FT "EE")] empty)
         (BV 0) (BV 1),
 
     testEq "E ≔ a ≡ a' : A, EE ≔ E ∥ x : EE, y : E ⊢ x = y"
            {globals = defGlobals `mergeLeft` fromList
               [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))),
                ("EE", mkDef zero (TYPE 0) (FT "E"))]} $
-      equalE (extendTyN [< ("x", FT "EE"), ("y", FT "E")] empty)
+      equalE (extendTyN [< (Any, "x", FT "EE"), (Any, "y", FT "E")] empty)
         (BV 0) (BV 1),
 
     testEq "E ≔ a ≡ a' : A ∥ x : E, y : E ⊢ x = y"
            {globals = defGlobals `mergeLeft` fromList
               [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'")))]} $
-      equalE (extendTyN [< ("x", FT "E"), ("y", FT "E")] empty) (BV 0) (BV 1),
+      equalE (extendTyN [< (Any, "x", FT "E"), (Any, "y", FT "E")] empty)
+        (BV 0) (BV 1),
 
     testEq "E ≔ a ≡ a' : A ∥ x : (E×E), y : (E×E) ⊢ x = y"
            {globals = defGlobals `mergeLeft` fromList
               [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'")))]} $
       let ty : forall n. Term Three 0 n :=
             Sig (FT "E") $ S ["_"] $ N $ FT "E" in
-      equalE (extendTyN [< ("x", ty), ("y", ty)] empty) (BV 0) (BV 1),
+      equalE (extendTyN [< (Any, "x", ty), (Any, "y", ty)] empty)
+        (BV 0) (BV 1),
 
     testEq "E ≔ a ≡ a' : A, W ≔ E × E ∥ x : W, y : W ⊢ x = y"
            {globals = defGlobals `mergeLeft` fromList
               [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))),
                ("W", mkDef zero (TYPE 0) (FT "E" `And` FT "E"))]} $
       equalE
-        (extendTyN [< ("x", FT "W"), ("y", FT "W")] empty)
+        (extendTyN [< (Any, "x", FT "W"), (Any, "y", FT "W")] empty)
         (BV 0) (BV 1)
   ],
 
   "term closure" :- [
     testEq "[#0]{} = [#0] : A" $
-      equalT (extendTy "x" (FT "A") empty)
+      equalT (extendTy Any "x" (FT "A") empty)
         (FT "A")
         (CloT (BVT 0) id)
         (BVT 0),
@@ -311,15 +313,18 @@ tests = "equality & subtyping" :- [
 
   "bound var" :- [
     testEq "#0 = #0" $
-      equalE (extendTy "A" (TYPE 0) empty) (BV 0) (BV 0),
+      equalE (extendTy Any "A" (TYPE 0) empty) (BV 0) (BV 0),
     testEq "#0 <: #0" $
-      subE (extendTy "A" (TYPE 0) empty) (BV 0) (BV 0),
+      subE (extendTy Any "A" (TYPE 0) empty) (BV 0) (BV 0),
     testNeq "#0 ≠ #1" $
-      equalE (extendTyN [< ("A", TYPE 0), ("B", TYPE 0)] empty) (BV 0) (BV 1),
+      equalE (extendTyN [< (Any, "A", TYPE 0), (Any, "B", TYPE 0)] empty)
+        (BV 0) (BV 1),
     testNeq "#0 ≮: #1" $
-      subE (extendTyN [< ("A", TYPE 0), ("B", TYPE 0)] empty) (BV 0) (BV 1),
+      subE (extendTyN [< (Any, "A", TYPE 0), (Any, "B", TYPE 0)] empty)
+        (BV 0) (BV 1),
     testEq "0=1 ⊢ #0 = #1" $
-      equalE (extendTyN [< ("A", TYPE 0), ("B", TYPE 0)] empty01) (BV 0) (BV 1)
+      equalE (extendTyN [< (Any, "A", TYPE 0), (Any, "B", TYPE 0)] empty01)
+        (BV 0) (BV 1)
   ],
 
   "application" :- [
@@ -416,7 +421,7 @@ tests = "equality & subtyping" :- [
     testEq "#0{a} = a" $
       equalE empty (CloE (BV 0) (F "a" ::: id)) (F "a"),
     testEq "#1{a} = #0" $
-      equalE (extendTy "x" (FT "A") empty)
+      equalE (extendTy Any "x" (FT "A") empty)
         (CloE (BV 1) (F "a" ::: id)) (BV 0)
   ],
 
@@ -451,7 +456,7 @@ tests = "equality & subtyping" :- [
         (F "eq-AB" :% K Zero),
     testEq "#0‹𝟎› = #0  # term and dim vars distinct" $
       equalED 1
-        (extendTy "x" (FT "A") $ extendDim "𝑖" empty)
+        (extendTy Any "x" (FT "A") $ extendDim "𝑖" empty)
         (DCloE (BV 0) (K Zero ::: id)) (BV 0),
     testEq "a‹𝟎› = a" $
       equalED 1 (extendDim "𝑖" empty) (DCloE (F "a") (K Zero ::: id)) (F "a"),
diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr
index 7aadb25..14f1d81 100644
--- a/tests/Tests/Typechecker.idr
+++ b/tests/Tests/Typechecker.idr
@@ -98,9 +98,16 @@ parameters (label : String) (act : Lazy (M ()))
   testTCFail = testThrows label (const True) $ runReaderT globals act
 
 
-ctx, ctx01 : Context (\n => (BaseName, Term Three 0 n)) n -> TyContext Three 0 n
-ctx tel = MkTyContext new [<] (map snd tel) (map fst tel)
-ctx01 tel = MkTyContext ZeroIsOne [<] (map snd tel) (map fst tel)
+anys : {n : Nat} -> QContext Three n
+anys {n = 0}   = [<]
+anys {n = S n} = anys :< Any
+
+ctx, ctx01 : {n : Nat} -> Context (\n => (BaseName, Term Three 0 n)) n ->
+             TyContext Three 0 n
+ctx tel = let (ns, ts) = unzip tel in
+          MkTyContext new [<] ts ns anys
+ctx01 tel = let (ns, ts) = unzip tel in
+            MkTyContext ZeroIsOne [<] ts ns anys
 
 empty01 : TyContext Three 0 0
 empty01 = {dctx := ZeroIsOne} empty
diff --git a/tests/TypingImpls.idr b/tests/TypingImpls.idr
index 9b45b7f..08d79cf 100644
--- a/tests/TypingImpls.idr
+++ b/tests/TypingImpls.idr
@@ -33,76 +33,5 @@ ToInfo WhnfError where
      ("list", show ts)]
 
 export
-PrettyHL q => ToInfo (Error q) where
-  toInfo (NotInScope x) =
-    [("type", "NotInScope"),
-     ("name", show x)]
-  toInfo (ExpectedTYPE _ t) =
-    [("type", "ExpectedTYPE"),
-     ("got",  prettyStr True t)]
-  toInfo (ExpectedPi _ t) =
-    [("type", "ExpectedPi"),
-     ("got",  prettyStr True t)]
-  toInfo (ExpectedSig _ t) =
-    [("type", "ExpectedSig"),
-     ("got",  prettyStr True t)]
-  toInfo (ExpectedEnum _ t) =
-    [("type", "ExpectedEnum"),
-     ("got",  prettyStr True t)]
-  toInfo (ExpectedEq _ t) =
-    [("type", "ExpectedEq"),
-     ("got",  prettyStr True t)]
-  toInfo (BadUniverse k l) =
-    [("type", "BadUniverse"),
-     ("low",  show k),
-     ("high", show l)]
-  toInfo (TagNotIn t ts) =
-    [("type", "TagNotIn"),
-     ("tag", show t),
-     ("set", show $ SortedSet.toList ts)]
-  toInfo (BadCaseQtys _ qouts) =
-    ("type", "BadCaseQtys") ::
-    [(show i, prettyStr True q) | (i, _, _, q) <- zip [1 .. length qouts] qouts]
-
-  toInfo (ClashT _ mode ty s t) =
-    [("type",  "ClashT"),
-     ("mode",  show mode),
-     ("ty",    prettyStr True ty),
-     ("left",  prettyStr True s),
-     ("right", prettyStr True t)]
-  toInfo (ClashTy _ mode s t) =
-    [("type",  "ClashTy"),
-     ("mode",  show mode),
-     ("left",  prettyStr True s),
-     ("right", prettyStr True t)]
-  toInfo (ClashE _ mode e f) =
-    [("type",  "ClashE"),
-     ("mode",  show mode),
-     ("left",  prettyStr True e),
-     ("right", prettyStr True f)]
-  toInfo (ClashU mode k l) =
-    [("type",  "ClashU"),
-     ("mode",  show mode),
-     ("left",  show k),
-     ("right", show l)]
-  toInfo (ClashQ pi rh) =
-    [("type",  "ClashQ"),
-     ("left",  prettyStr True pi),
-     ("right", prettyStr True rh)]
-  toInfo (NotType _ ty) =
-    [("type", "NotType"),
-     ("got",  prettyStr True ty)]
-  toInfo (WrongType _ ty s t) =
-    [("type",  "WrongType"),
-     ("ty",    prettyStr True ty),
-     ("left",  prettyStr True s),
-     ("right", prettyStr True t)]
-
-  -- [todo] add nested yamls to TAP and include context here
-  toInfo (WhileChecking   _ _ _ _   err) = toInfo err
-  toInfo (WhileCheckingTy _ _ _     err) = toInfo err
-  toInfo (WhileInferring  _ _ _     err) = toInfo err
-  toInfo (WhileComparingT _ _ _ _ _ err) = toInfo err
-  toInfo (WhileComparingE _ _ _ _   err) = toInfo err
-
-  toInfo (WhnfError err) = toInfo err
+(Eq q, PrettyHL q) => ToInfo (Error q) where
+  toInfo err = [("err", show $ prettyError True True err)]