diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index e715584..b76ba98 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -83,8 +83,8 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
 
   ||| `check0 ctx subj ty` checks a term in a zero context.
   export covering %inline
-  check0 : TyContext q d n -> Term q d n -> Term q d n -> m (CheckResult q n)
-  check0 ctx = check (zeroed ctx) szero
+  check0 : TyContext q d n -> Term q d n -> Term q d n -> m ()
+  check0 ctx tm ty = ignore $ check (zeroed ctx) szero tm ty
 
   ||| `infer ctx sg subj` infers the type of `subj` in the context `ctx`,
   ||| and returns its type and the bound variables it used.
@@ -111,30 +111,31 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     l <- expectTYPE !ask ty
     expectEqualQ zero sg.fst
     -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
-    ignore $ check0 ctx arg (TYPE l)
+    check0 ctx arg (TYPE l)
     -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
     case res of
-      TUsed   res => ignore $ check0 (extendTy arg zero ctx) res (TYPE l)
-      TUnused res => ignore $ check0 ctx res (TYPE l)
+      TUsed   res => check0 (extendTy arg zero ctx) res (TYPE l)
+      TUnused res => check0 ctx res (TYPE l)
     -- then Ψ | Γ ⊢₀ (π·x : A) → B ⇐ Type ℓ
     pure $ zeroFor ctx
 
   check' ctx sg (Lam _ body) _ ty = do
     (qty, arg, res) <- expectPi !ask ty
     -- if Ψ | Γ, πσ·x : A ⊢ σ · t ⇐ B ⊳ Σ, σπ·x
-    qout <- check (extendTy arg (sg.fst * qty) ctx) sg body.term res.term
+    let qty' = sg.fst * qty
+    qout <- check (extendTy arg qty' ctx) sg body.term res.term
     -- then Ψ | Γ ⊢ σ · (λx ⇒ t) ⇐ (π·x : A) → B ⊳ Σ
-    popQ (sg.fst * qty) qout
+    popQ qty' qout
 
   check' ctx sg (Sig _ fst snd) _ ty = do
     l <- expectTYPE !ask ty
     expectEqualQ zero sg.fst
     -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
-    ignore $ check0 ctx fst (TYPE l)
+    check0 ctx fst (TYPE l)
     -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
     case snd of
-      TUsed   snd => ignore $ check0 (extendTy fst zero ctx) snd (TYPE l)
-      TUnused snd => ignore $ check0 ctx snd (TYPE l)
+      TUsed   snd => check0 (extendTy fst zero ctx) snd (TYPE l)
+      TUnused snd => check0 ctx snd (TYPE l)
     -- then Ψ | Γ ⊢₀ (x : A) × B ⇐ Type ℓ
     pure $ zeroFor ctx
 
@@ -153,12 +154,12 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     expectEqualQ zero sg.fst
     -- if Ψ, i | Γ ⊢₀ A ⇐ Type ℓ
     case t of
-      DUsed   t => ignore $ check0 (extendDim ctx) t (TYPE u)
-      DUnused t => ignore $ check0 ctx t (TYPE u)
+      DUsed   t => check0 (extendDim ctx) t (TYPE u)
+      DUnused t => check0 ctx t (TYPE u)
     -- if Ψ | Γ ⊢₀ l ⇐ A‹0›
-    ignore $ check0 ctx t.zero l
+    check0 ctx t.zero l
     -- if Ψ | Γ ⊢₀ r ⇐ A‹1›
-    ignore $ check0 ctx t.one  r
+    check0 ctx t.one  r
     -- then Ψ | Γ ⊢₀ Eq [i ⇒ A] l r ⇐ Type ℓ
     pure $ zeroFor ctx
 
@@ -218,7 +219,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     expectCompatQ one pi
     -- if Ψ | Γ ⊢ 1 · pair ⇒ (x : A) × B ⊳ Σ₁
     pairres <- infer ctx sone pair
-    ignore $ check0 (extendTy pairres.type zero ctx) ret.term (TYPE UAny)
+    check0 (extendTy pairres.type zero ctx) ret.term (TYPE UAny)
     (tfst, tsnd) <- expectSig !ask pairres.type
     -- if Ψ | Γ, π·x : A, π·y : B ⊢ σ body ⇐ ret[(x, y)]
     --      ⊳ Σ₂, π₁·x, π₂·y
@@ -241,7 +242,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
 
   infer' ctx sg (term :# type) _ = do
     -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
-    ignore $ check0 ctx type (TYPE UAny)
+    check0 ctx type (TYPE UAny)
     -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ
     qout <- check ctx sg term type
     -- then Ψ | Γ ⊢ σ · (s ∷ A) ⇒ A ⊳ Σ