diff --git a/lib/Quox/Definition.idr b/lib/Quox/Definition.idr
index 2642b29..693012a 100644
--- a/lib/Quox/Definition.idr
+++ b/lib/Quox/Definition.idr
@@ -74,10 +74,6 @@ public export
 DefsState : Type -> Type
 DefsState = StateL DEFS Definitions
 
-export
-defs : Has DefsReader fs => Eff fs Definitions
-defs = askAt DEFS
-
 
 public export %inline
 lookupElim : {d, n : Nat} -> Name -> Definitions -> Maybe (Elim d n)
diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index 5efdcb3..c3e49dc 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -637,7 +637,7 @@ parameters (loc : Loc) (ctx : TyContext d n)
     private
     runCompare : (Definitions -> EqContext n -> DSubst d 0 -> Equal_ ()) ->
                  Equal ()
-    runCompare act = fromEqual_ $ eachFace $ act !defs
+    runCompare act = fromEqual_ $ eachFace $ act !(askAt DEFS)
 
     namespace Term
       export covering
diff --git a/lib/Quox/Parser/FromParser/Error.idr b/lib/Quox/Parser/FromParser/Error.idr
index 98313ce..6bc2b0b 100644
--- a/lib/Quox/Parser/FromParser/Error.idr
+++ b/lib/Quox/Parser/FromParser/Error.idr
@@ -6,6 +6,8 @@ import System.File
 
 import Quox.Pretty
 
+%hide Text.PrettyPrint.Prettyprinter.Doc.infixr.(<++>)
+
 
 public export
 TypeError, LexError, ParseError : Type
diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index 112185c..e7addb1 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -58,11 +58,12 @@ pbname (_, x, _) = x
 private
 record SplitPi d n where
   constructor MkSplitPi
+  {0 inner : Nat}
   binds : Telescope (PiBind d) n inner
   cod   : Term d inner
 
 private
-splitPi : Telescope (PiBind d) n inner -> Term d inner -> SplitPi d n
+splitPi : Telescope (PiBind d) n n' -> Term d n' -> SplitPi d n
 splitPi binds (Pi qty arg res _) =
   splitPi (binds :< (qty, res.name, arg)) $
     assert_smaller res $ pushSubsts' res.term
@@ -87,7 +88,7 @@ prettyPiBind1 pi x dnames tnames s = hcat <$> sequence
 private
 prettyPiBinds : {opts : _} ->
                 BContext d -> BContext n ->
-                Telescope (PiBind d) n inner ->
+                Telescope (PiBind d) n n' ->
                 Eff Pretty (SnocList (Doc opts))
 prettyPiBinds _ _ [<] = pure [<]
 prettyPiBinds dnames tnames (binds :< (q, x, t)) =
@@ -103,11 +104,12 @@ SigBind d n = (BindName, Term d n)
 private
 record SplitSig d n where
   constructor MkSplitSig
+  {0 inner : Nat}
   binds : Telescope (SigBind d) n inner
   last  : Term d inner
 
 private
-splitSig : Telescope (SigBind d) n inner -> Term d inner -> SplitSig d n
+splitSig : Telescope (SigBind d) n n' -> Term d n' -> SplitSig d n
 splitSig binds (Sig fst snd _) =
   splitSig (binds :< (snd.name, fst)) $
     assert_smaller snd $ pushSubsts' snd.term
@@ -129,7 +131,7 @@ prettySigBind1 x dnames tnames s = hcat <$> sequence
 private
 prettySigBinds : {opts : _} ->
                  BContext d -> BContext n ->
-                 Telescope (SigBind d) n inner ->
+                 Telescope (SigBind d) n n' ->
                  Eff Pretty (SnocList (Doc opts))
 prettySigBinds _ _ [<] = pure [<]
 prettySigBinds dnames tnames (binds :< (x, t)) =
@@ -163,6 +165,7 @@ NameChunks = SnocList (NameSort, SnocList BindName)
 private
 record SplitLams d n where
   constructor MkSplitLams
+  {0 dinner, ninner : Nat}
   dnames : BTelescope d dinner
   tnames : BTelescope n ninner
   chunks : NameChunks
@@ -178,9 +181,9 @@ where
     if s == s' then xss :< (s', xs :< y)
     else xss :< (s', xs) :< (s, [< y])
 
-  go : BTelescope d dinner -> BTelescope n ninner ->
+  go : BTelescope d d' -> BTelescope n n' ->
        SnocList (NameSort, SnocList BindName) ->
-       Term dinner ninner -> SplitLams d n
+       Term d' n' -> 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
@@ -235,6 +238,7 @@ prettyDTApps dnames tnames f xs = do
 private
 record CaseArm opts d n where
   constructor MkCaseArm
+  {0 dinner, ninner : Nat}
   pat    : Doc opts
   dbinds : BTelescope d dinner -- 🍴
   tbinds : BTelescope n ninner
diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr
index 06a9a25..c0b62f6 100644
--- a/lib/Quox/Syntax/Term/Subst.idr
+++ b/lib/Quox/Syntax/Term/Subst.idr
@@ -10,7 +10,7 @@ import Data.SnocVect
 namespace CanDSubst
   public export
   interface CanDSubst (0 tm : TermLike) where
-    (//) : tm dfrom n -> Lazy (DSubst dfrom dto) -> tm dto n
+    (//) : tm d1 n -> Lazy (DSubst d1 d2) -> tm d2 n
 
 ||| does the minimal reasonable work:
 ||| - deletes the closure around an atomic constant like `TYPE`
@@ -25,7 +25,7 @@ CanDSubst Term where
   s                // th       = DCloT $ Sub s th
 
 private
-subDArgs : Elim dfrom n -> DSubst dfrom dto -> Elim dto n
+subDArgs : Elim d1 n -> DSubst d1 d2 -> Elim d2 n
 subDArgs (DApp f d loc) th = DApp (subDArgs f th) (d // th) loc
 subDArgs e              th = DCloE $ Sub e th
 
@@ -47,16 +47,16 @@ CanDSubst Elim where
 
 namespace DSubst.ScopeTermN
   export %inline
-  (//) : ScopeTermN s dfrom n -> Lazy (DSubst dfrom dto) ->
-         ScopeTermN s dto n
+  (//) : ScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
+         ScopeTermN s d2 n
   S ns (Y body) // th = S ns $ Y $ body // th
   S ns (N body) // th = S ns $ N $ body // th
 
 namespace DSubst.DScopeTermN
   export %inline
   (//) : {s : Nat} ->
-         DScopeTermN s dfrom n -> Lazy (DSubst dfrom dto) ->
-         DScopeTermN s dto n
+         DScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
+         DScopeTermN s d2 n
   S ns (Y body) // th = S ns $ Y $ body // pushN s th
   S ns (N body) // th = S ns $ N $ body // th
 
@@ -83,7 +83,7 @@ CanSubstSelf (Elim d) where
 namespace CanTSubst
   public export
   interface CanTSubst (0 tm : TermLike) where
-    (//) : tm d from -> Lazy (TSubst d from to) -> tm d to
+    (//) : tm d n1 -> Lazy (TSubst d n1 n2) -> tm d n2
 
 ||| does the minimal reasonable work:
 ||| - deletes the closure around an atomic constant like `TYPE`
@@ -103,16 +103,15 @@ CanTSubst Term where
 namespace ScopeTermN
   export %inline
   (//) : {s : Nat} ->
-         ScopeTermN s d from -> Lazy (TSubst d from to) ->
-         ScopeTermN s d to
+         ScopeTermN s d n1 -> Lazy (TSubst d n1 n2) ->
+         ScopeTermN s d n2
   S ns (Y body) // th = S ns $ Y $ body // pushN s th
   S ns (N body) // th = S ns $ N $ body // th
 
 namespace DScopeTermN
   export %inline
   (//) : {s : Nat} ->
-         DScopeTermN s d from -> Lazy (TSubst d from to) ->
-         DScopeTermN s d to
+         DScopeTermN s d n1 -> Lazy (TSubst d n1 n2) -> DScopeTermN s d n2
   S ns (Y body) // th = S ns $ Y $ body // map (// shift s) th
   S ns (N body) // th = S ns $ N $ body // th
 
@@ -125,8 +124,7 @@ export %inline
 
 
 export %inline
-comp : DSubst dfrom dto -> TSubst dfrom from mid -> TSubst dto mid to ->
-       TSubst dto from to
+comp : DSubst d1 d2 -> TSubst d1 n1 mid -> TSubst d2 mid n2 -> TSubst d2 n1 n2
 comp th ps ph = map (// th) ps . ph
 
 
@@ -205,8 +203,8 @@ public export
 CloTest tm = forall d, n. tm d n -> Bool
 
 interface PushSubsts (0 tm : TermLike) (0 isClo : CloTest tm) | tm where
-  pushSubstsWith : DSubst dfrom dto -> TSubst dto from to ->
-                   tm dfrom from -> Subset (tm dto to) (No . isClo)
+  pushSubstsWith : DSubst d1 d2 -> TSubst d2 n1 n2 ->
+                   tm d1 n1 -> Subset (tm d2 n2) (No . isClo)
 
 public export
 0 NotClo : {isClo : CloTest tm} -> PushSubsts tm isClo => Pred (tm d n)
@@ -230,8 +228,7 @@ parameters {0 isClo : CloTest tm} {auto _ : PushSubsts tm isClo}
   pushSubsts s = pushSubstsWith id id s
 
   export %inline
-  pushSubstsWith' : DSubst dfrom dto -> TSubst dto from to ->
-                    tm dfrom from -> tm dto to
+  pushSubstsWith' : DSubst d1 d2 -> TSubst d2 n1 n2 -> tm d1 n1 -> tm d2 n2
   pushSubstsWith' th ph x = fst $ pushSubstsWith th ph x
 
   export %inline
diff --git a/lib/Quox/Syntax/Term/Tighten.idr b/lib/Quox/Syntax/Term/Tighten.idr
index dee04ff..931ac65 100644
--- a/lib/Quox/Syntax/Term/Tighten.idr
+++ b/lib/Quox/Syntax/Term/Tighten.idr
@@ -8,10 +8,10 @@ import public Quox.OPE
 
 
 export
-Tighten (Shift from) where
+Tighten (Shift f) where
   -- `OPE m n` is a spicy `m ≤ n`,
-  -- and `Shift from n` is a (different) spicy `from ≤ n`
-  -- so the value is `from ≤ m` (as a `Shift`), if that is the case
+  -- and `Shift f n` is a (different) spicy `f ≤ n`
+  -- so the value is `f ≤ m` (as a `Shift`), if that is the case
   tighten _        SZ      = Nothing
   tighten Id       by      = Just by
   tighten (Drop p) (SS by) = tighten p by
@@ -26,12 +26,12 @@ Tighten Dim where
 
 export
 tightenSub : (forall m, n. OPE m n -> env n -> Maybe (env m)) ->
-             OPE to1 to2 -> Subst env from to2 -> Maybe (Subst env from to1)
+             OPE t1 t2 -> Subst env f t2 -> Maybe (Subst env f t1)
 tightenSub f p (Shift by) = [|Shift $ tighten p by|]
 tightenSub f p (t ::: th) = [|f p t !::: tightenSub f p th|]
 
 export
-Tighten env => Tighten (Subst env from) where
+Tighten env => Tighten (Subst env f) where
   tighten p th = tightenSub tighten p th
 
 
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index 3a019e9..d5cb0e6 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -163,7 +163,7 @@ mutual
                 (subj : Term d n) -> (0 nc : NotClo subj) => Term d n ->
                 TC (CheckResult' n)
   toCheckType ctx sg t ty = do
-    u <- expectTYPE !defs ctx ty.loc ty
+    u <- expectTYPE !(askAt DEFS) ctx ty.loc ty
     expectEqualQ t.loc Zero sg.fst
     checkTypeNoWrap ctx t (Just u)
     pure $ zeroFor ctx
@@ -178,7 +178,7 @@ mutual
   check' ctx sg t@(Pi {}) ty = toCheckType ctx sg t ty
 
   check' ctx sg (Lam body loc) ty = do
-    (qty, arg, res) <- expectPi !defs ctx ty.loc ty
+    (qty, arg, res) <- expectPi !(askAt DEFS) ctx ty.loc ty
     -- if Ψ | Γ, x : A ⊢ σ · t ⇐ B ⊳ Σ, ρ·x
     -- with ρ ≤ σπ
     let qty' = sg.fst * qty
@@ -189,7 +189,7 @@ mutual
   check' ctx sg t@(Sig {}) ty = toCheckType ctx sg t ty
 
   check' ctx sg (Pair fst snd loc) ty = do
-    (tfst, tsnd) <- expectSig !defs ctx ty.loc ty
+    (tfst, tsnd) <- expectSig !(askAt DEFS) ctx ty.loc ty
     -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ₁
     qfst <- checkC ctx sg fst tfst
     let tsnd = sub1 tsnd (Ann fst tfst fst.loc)
@@ -201,7 +201,7 @@ mutual
   check' ctx sg t@(Enum {}) ty = toCheckType ctx sg t ty
 
   check' ctx sg (Tag t loc) ty = do
-    tags <- expectEnum !defs ctx ty.loc ty
+    tags <- expectEnum !(askAt DEFS) ctx ty.loc ty
     -- if t ∈ ts
     unless (t `elem` tags) $ throw $ TagNotIn loc t tags
     -- then Ψ | Γ ⊢ σ · t ⇐ {ts} ⊳ 𝟎
@@ -210,7 +210,7 @@ mutual
   check' ctx sg t@(Eq {}) ty = toCheckType ctx sg t ty
 
   check' ctx sg (DLam body loc) ty = do
-    (ty, l, r) <- expectEq !defs ctx ty.loc ty
+    (ty, l, r) <- expectEq !(askAt DEFS) ctx ty.loc ty
     let ctx' = extendDim body.name ctx
         ty   = ty.term
         body = body.term
@@ -226,17 +226,17 @@ mutual
   check' ctx sg t@(Nat {}) ty = toCheckType ctx sg t ty
 
   check' ctx sg (Zero {}) ty = do
-    expectNat !defs ctx ty.loc ty
+    expectNat !(askAt DEFS) ctx ty.loc ty
     pure $ zeroFor ctx
 
   check' ctx sg (Succ n {}) ty = do
-    expectNat !defs ctx ty.loc ty
+    expectNat !(askAt DEFS) ctx ty.loc ty
     checkC ctx sg n ty
 
   check' ctx sg t@(BOX {}) ty = toCheckType ctx sg t ty
 
   check' ctx sg (Box val loc) ty = do
-    (q, ty) <- expectBOX !defs ctx ty.loc ty
+    (q, ty) <- expectBOX !(askAt DEFS) ctx ty.loc ty
     -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ
     valout <- checkC ctx sg val ty
     -- then Ψ | Γ ⊢ σ · [s] ⇐ [π.A] ⊳ πΣ
@@ -314,7 +314,7 @@ mutual
     -- if Ψ | Γ ⊢ Type ℓ <: Type 𝓀
     case u of
       Just u  => lift $ subtype e.loc ctx infres.type (TYPE u noLoc)
-      Nothing => ignore $ expectTYPE !defs ctx e.loc infres.type
+      Nothing => ignore $ expectTYPE !(askAt DEFS) ctx e.loc infres.type
     -- then Ψ | Γ ⊢₀ E ⇐ Type 𝓀
 
 
@@ -333,7 +333,7 @@ mutual
 
   infer' ctx sg (F x u loc) = do
     -- if π·x : A {≔ s} in global context
-    g <- lookupFree x loc !defs
+    g <- lookupFree x loc !(askAt DEFS)
     -- if σ ≤ π
     expectCompatQ loc sg.fst g.qty.fst
     -- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ 𝟎
@@ -355,7 +355,7 @@ mutual
   infer' ctx sg (App fun arg loc) = do
     -- if Ψ | Γ ⊢ σ · f ⇒ (π·x : A) → B ⊳ Σ₁
     funres <- inferC ctx sg fun
-    (qty, argty, res) <- expectPi !defs ctx fun.loc funres.type
+    (qty, argty, res) <- expectPi !(askAt DEFS) ctx fun.loc funres.type
     -- if Ψ | Γ ⊢ σ ⨴ π · s ⇐ A ⊳ Σ₂
     argout <- checkC ctx (subjMult sg qty) arg argty
     -- then Ψ | Γ ⊢ σ · f s ⇒ B[s] ⊳ Σ₁ + πΣ₂
@@ -372,7 +372,7 @@ mutual
     pairres <- inferC ctx sg pair
     -- if Ψ | Γ, p : (x : A) × B ⊢₀ ret ⇐ Type
     checkTypeC (extendTy Zero ret.name pairres.type ctx) ret.term Nothing
-    (tfst, tsnd) <- expectSig !defs ctx pair.loc pairres.type
+    (tfst, tsnd) <- expectSig !(askAt DEFS) ctx pair.loc pairres.type
     -- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐
     --    ret[(x, y) ∷ (x : A) × B/p] ⊳ Σ₂, ρ₁·x, ρ₂·y
     -- with ρ₁, ρ₂ ≤ πσ
@@ -391,7 +391,7 @@ mutual
   infer' ctx sg (CaseEnum pi t ret arms loc) {d, n} = do
     -- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁
     tres <- inferC ctx sg t
-    ttags <- expectEnum !defs ctx t.loc tres.type
+    ttags <- expectEnum !(askAt DEFS) ctx t.loc tres.type
     -- if 1 ≤ π, OR there is only zero or one option
     unless (length (SortedSet.toList ttags) <= 1) $ expectCompatQ loc One pi
     -- if Ψ | Γ, x : {ts} ⊢₀ A ⇐ Type
@@ -415,7 +415,7 @@ mutual
     -- if Ψ | Γ ⊢ σ · n ⇒ ℕ ⊳ Σn
     nres <- inferC ctx sg n
     let nat = nres.type
-    expectNat !defs ctx n.loc nat
+    expectNat !(askAt DEFS) ctx n.loc nat
     -- if Ψ | Γ, n : ℕ ⊢₀ A ⇐ Type
     checkTypeC (extendTy Zero ret.name nat ctx) ret.term Nothing
     -- if Ψ | Γ ⊢ σ · zer ⇐ A[0 ∷ ℕ/n] ⊳ Σz
@@ -439,7 +439,7 @@ mutual
   infer' ctx sg (CaseBox pi box ret body loc) = do
     -- if Ψ | Γ ⊢ σ · b ⇒ [ρ.A] ⊳ Σ₁
     boxres <- inferC ctx sg box
-    (q, ty) <- expectBOX !defs ctx box.loc boxres.type
+    (q, ty) <- expectBOX !(askAt DEFS) ctx box.loc boxres.type
     -- if Ψ | Γ, x : [ρ.A] ⊢₀ R ⇐ Type
     checkTypeC (extendTy Zero ret.name boxres.type ctx) ret.term Nothing
     -- if Ψ | Γ, x : A ⊢ t ⇐ R[[x] ∷ [ρ.A/x]] ⊳ Σ₂, ς·x
@@ -457,7 +457,7 @@ mutual
   infer' ctx sg (DApp fun dim loc) = do
     -- if Ψ | Γ ⊢ σ · f ⇒ Eq [𝑖 ⇒ A] l r ⊳ Σ
     InfRes {type, qout} <- inferC ctx sg fun
-    ty <- fst <$> expectEq !defs ctx fun.loc type
+    ty <- fst <$> expectEq !(askAt DEFS) ctx fun.loc type
     -- then Ψ | Γ ⊢ σ · f p ⇒ A‹p/𝑖› ⊳ Σ
     pure $ InfRes {type = dsub1 ty dim, qout}
 
@@ -485,7 +485,7 @@ mutual
     -- if σ = 0
     expectEqualQ loc Zero sg.fst
     -- if Ψ, Γ ⊢₀ e ⇒ Type u
-    u <- expectTYPE !defs ctx ty.loc . type =<< inferC ctx szero ty
+    u <- expectTYPE !(askAt DEFS) ctx ty.loc . type =<< inferC ctx szero ty
     -- if Ψ, Γ ⊢₀ C ⇐ Type (non-dependent return type)
     checkTypeC ctx ret Nothing
     -- if Ψ, Γ' ⊢₀ A ⇐ C for each rhs A
diff --git a/lib/Quox/Typing/Context.idr b/lib/Quox/Typing/Context.idr
index 8d44bc9..c1db5fe 100644
--- a/lib/Quox/Typing/Context.idr
+++ b/lib/Quox/Typing/Context.idr
@@ -69,7 +69,7 @@ namespace TContext
   zeroFor ctx = Zero <$ ctx
 
 private
-extendLen : Telescope a from to -> Singleton from -> Singleton to
+extendLen : Telescope a n1 n2 -> Singleton n1 -> Singleton n2
 extendLen [<]        x = x
 extendLen (tel :< _) x = [|S $ extendLen tel x|]
 
@@ -89,7 +89,7 @@ namespace TyContext
   null ctx = null ctx.dnames && null ctx.tnames
 
   export %inline
-  extendTyN : CtxExtension d from to -> TyContext d from -> TyContext d to
+  extendTyN : CtxExtension d n1 n2 -> TyContext d n1 -> TyContext d n2
   extendTyN xss (MkTyContext {termLen, dctx, dnames, tctx, tnames, qtys}) =
     let (qs, xs, ss) = unzip3 xss in
     MkTyContext {
@@ -172,7 +172,7 @@ namespace EqContext
   null ctx = null ctx.dnames && null ctx.tnames
 
   export %inline
-  extendTyN : CtxExtension 0 from to -> EqContext from -> EqContext to
+  extendTyN : CtxExtension 0 n1 n2 -> EqContext n1 -> EqContext n2
   extendTyN xss (MkEqContext {termLen, dassign, dnames, tctx, tnames, qtys}) =
     let (qs, xs, ss) = unzip3 xss in
     MkEqContext {
diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr
index d9e91bc..248d415 100644
--- a/tests/Tests/Typechecker.idr
+++ b/tests/Tests/Typechecker.idr
@@ -34,7 +34,7 @@ ToInfo Error' where
 M = Eff [Except Error', DefsReader]
 
 inj : TC a -> M a
-inj act = rethrow $ mapFst TCError $ runTC !defs act
+inj act = rethrow $ mapFst TCError $ runTC !(askAt DEFS) act
 
 
 reflTy : Term d n