From e6c06a5c8105acd3a31621438ff14598dab517df Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 18 Sep 2023 18:21:30 +0200
Subject: [PATCH] pass the subject quantity through equality etc
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

in preparation for non-linear η laws
---
 exe/Main.idr                      |   4 +-
 lib/Quox/Definition.idr           |   2 +-
 lib/Quox/Equal.idr                | 320 +++++++++++++++---------------
 lib/Quox/Parser/FromParser.idr    |   6 +-
 lib/Quox/Syntax/Qty.idr           |  82 +++++---
 lib/Quox/Typechecker.idr          |  69 ++++---
 lib/Quox/Typing.idr               |  12 +-
 lib/Quox/Typing/Error.idr         |  84 ++++----
 lib/Quox/Whnf/Coercion.idr        |  44 ++--
 lib/Quox/Whnf/ComputeElimType.idr |  18 +-
 lib/Quox/Whnf/Interface.idr       | 125 ++++++------
 lib/Quox/Whnf/Main.idr            | 150 +++++++-------
 lib/Quox/Whnf/TypeCase.idr        |  32 +--
 tests/Tests/Equal.idr             |  68 ++++---
 tests/Tests/FromPTerm.idr         |   2 +-
 tests/Tests/Reduce.idr            |   7 +-
 tests/Tests/Typechecker.idr       | 234 +++++++++++-----------
 17 files changed, 654 insertions(+), 605 deletions(-)

diff --git a/exe/Main.idr b/exe/Main.idr
index 72232bf..e522169 100644
--- a/exe/Main.idr
+++ b/exe/Main.idr
@@ -23,9 +23,9 @@ die : Doc Opts -> IO a
 die err = do putDoc err; exitFailure
 
 private
-prettySig : {opts : _} -> Name -> Definition -> Eff Pretty (Doc opts)
+prettySig : Name -> Definition -> Eff Pretty (Doc Opts)
 prettySig name def = do
-  qty  <- prettyQty def.qty.fst
+  qty  <- prettyQty def.qty.qty
   name <- prettyFree name
   type <- prettyTerm [<] [<] def.type
   hangDSingle (hsep [hcat [qty, !dotD, name], !colonD]) type
diff --git a/lib/Quox/Definition.idr b/lib/Quox/Definition.idr
index 53becaf..030584c 100644
--- a/lib/Quox/Definition.idr
+++ b/lib/Quox/Definition.idr
@@ -65,7 +65,7 @@ parameters {d, n : Nat}
 
 public export %inline
 isZero : Definition -> Bool
-isZero g = g.qty.fst == Zero
+isZero g = g.qty == GZero
 
 
 public export
diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index d847cf2..6dddc39 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -70,22 +70,22 @@ sameTyCon (E    {}) _         = False
 ||| * `[π.A]` is empty if `A` is.
 ||| * that's it.
 public export covering
-isEmpty : {n : Nat} -> Definitions -> EqContext n -> Term 0 n ->
+isEmpty : {n : Nat} -> Definitions -> EqContext n -> SQty -> Term 0 n ->
           Eff EqualInner Bool
-isEmpty defs ctx ty0 = do
-  Element ty0 nc <- whnf defs ctx ty0.loc ty0
+isEmpty defs ctx sg ty0 = do
+  Element ty0 nc <- whnf defs ctx sg ty0.loc ty0
   case ty0 of
     TYPE {} => pure False
     Pi {arg, res, _} => pure False
     Sig {fst, snd, _} =>
-      isEmpty defs ctx fst `orM`
-      isEmpty defs (extendTy0 snd.name fst ctx) snd.term
+      isEmpty defs ctx sg fst `orM`
+      isEmpty defs (extendTy0 snd.name fst ctx) sg snd.term
     Enum {cases, _} =>
       pure $ null cases
     Eq {} => pure False
     Nat {} => pure False
-    BOX {ty, _} => isEmpty defs ctx ty
-    E (Ann {tm, _}) => isEmpty defs ctx tm
+    BOX {ty, _} => isEmpty defs ctx sg ty
+    E (Ann {tm, _}) => isEmpty defs ctx sg tm
     E _ => pure False
     Lam  {} => pure False
     Pair {} => pure False
@@ -106,24 +106,24 @@ isEmpty defs ctx ty0 = do
 ||| * an enum type is a subsingleton if it has zero or one tags.
 ||| * a box type is a subsingleton if its content is
 public export covering
-isSubSing : {n : Nat} -> Definitions -> EqContext n -> Term 0 n ->
+isSubSing : {n : Nat} -> Definitions -> EqContext n -> SQty -> Term 0 n ->
             Eff EqualInner Bool
-isSubSing defs ctx ty0 = do
-  Element ty0 nc <- whnf defs ctx ty0.loc ty0
+isSubSing defs ctx sg ty0 = do
+  Element ty0 nc <- whnf defs ctx sg ty0.loc ty0
   case ty0 of
     TYPE {} => pure False
     Pi {arg, res, _} =>
-      isEmpty defs ctx arg `orM`
-      isSubSing defs (extendTy0 res.name arg ctx) res.term
+      isEmpty defs ctx sg arg `orM`
+      isSubSing defs (extendTy0 res.name arg ctx) sg res.term
     Sig {fst, snd, _} =>
-      isSubSing defs ctx fst `andM`
-      isSubSing defs (extendTy0 snd.name fst ctx) snd.term
+      isSubSing defs ctx sg fst `andM`
+      isSubSing defs (extendTy0 snd.name fst ctx) sg snd.term
     Enum {cases, _} =>
       pure $ length (SortedSet.toList cases) <= 1
     Eq {} => pure True
     Nat {} => pure False
-    BOX {ty, _} => isSubSing defs ctx ty
-    E (Ann {tm, _}) => isSubSing defs ctx tm
+    BOX {ty, _} => isSubSing defs ctx sg ty
+    E (Ann {tm, _}) => isSubSing defs ctx sg tm
     E _ => pure False
     Lam  {} => pure False
     Pair {} => pure False
@@ -155,7 +155,7 @@ namespace Term
   |||
   ||| ⚠ **assumes that `s`, `t` have already been checked against `ty`**. ⚠
   export covering %inline
-  compare0 : Definitions -> EqContext n -> (ty, s, t : Term 0 n) ->
+  compare0 : Definitions -> EqContext n -> SQty -> (ty, s, t : Term 0 n) ->
              Eff EqualInner ()
 
 namespace Elim
@@ -164,7 +164,7 @@ namespace Elim
   ||| ⚠ **assumes that they have both been typechecked, and have
   ||| equal types.** ⚠
   export covering %inline
-  compare0 : Definitions -> EqContext n -> (e, f : Elim 0 n) ->
+  compare0 : Definitions -> EqContext n -> SQty -> (e, f : Elim 0 n) ->
              Eff EqualInner (Term 0 n)
 
 ||| compares two types, using the current variance `mode` for universes.
@@ -176,14 +176,14 @@ compareType : Definitions -> EqContext n -> (s, t : Term 0 n) ->
 
 namespace Term
   private covering
-  compare0' : (defs : Definitions) -> EqContext n ->
+  compare0' : (defs : Definitions) -> EqContext n -> (sg : SQty) ->
               (ty, s, t : Term 0 n) ->
-              (0 _ : NotRedex defs ty) => (0 _ : So (isTyConE ty)) =>
-              (0 _ : NotRedex defs s)  => (0 _ : NotRedex defs t) =>
+              (0 _ : NotRedex defs SZero ty) => (0 _ : So (isTyConE ty)) =>
+              (0 _ : NotRedex defs sg    s)  => (0 _ : NotRedex defs sg t) =>
               Eff EqualInner ()
-  compare0' defs ctx (TYPE {}) s t = compareType defs ctx s t
+  compare0' defs ctx sg (TYPE {}) s t = compareType defs ctx s t
 
-  compare0' defs ctx ty@(Pi {qty, arg, res, _}) s t = local_ Equal $
+  compare0' defs ctx sg ty@(Pi {qty, arg, res, _}) s t = local_ Equal $
     --              Γ ⊢ A empty
     -- -------------------------------------------
     --  Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) : (π·x : A) → B
@@ -193,7 +193,7 @@ namespace Term
       -- -------------------------------------------
       --  Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) : (π·x : A) → B
       (Lam b1 {}, Lam b2 {}) =>
-        compare0 defs ctx' res.term b1.term b2.term
+        compare0 defs ctx' sg res.term b1.term b2.term
 
       --       Γ, x : A ⊢ s = e x : B
       -- -----------------------------------
@@ -201,14 +201,14 @@ namespace Term
       (E e,      Lam b {}) => eta s.loc e b
       (Lam b {}, E e)      => eta s.loc e b
 
-      (E e, E f) => ignore $ Elim.compare0 defs ctx e f
+      (E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
 
       (Lam {}, t) => wrongType t.loc ctx ty t
       (E _,    t) => wrongType t.loc ctx ty t
       (s,      _) => wrongType s.loc ctx ty s
   where
     isEmpty' : Term 0 n -> Eff EqualInner Bool
-    isEmpty' t = let Val n = ctx.termLen in isEmpty defs ctx arg
+    isEmpty' t = let Val n = ctx.termLen in isEmpty defs ctx sg arg
 
     ctx' : EqContext (S n)
     ctx' = extendTy qty res.name arg ctx
@@ -218,9 +218,9 @@ namespace Term
 
     eta : Loc -> Elim 0 n -> ScopeTerm 0 n -> Eff EqualInner ()
     eta loc e (S _ (N _)) = clashT loc ctx ty s t
-    eta _   e (S _ (Y b)) = compare0 defs ctx' res.term (toLamBody e) b
+    eta _   e (S _ (Y b)) = compare0 defs ctx' sg res.term (toLamBody e) b
 
-  compare0' defs ctx ty@(Sig {fst, snd, _}) s t = local_ Equal $
+  compare0' defs ctx sg ty@(Sig {fst, snd, _}) s t = local_ Equal $
     case (s, t) of
       --  Γ ⊢ s₁ = t₁ : A     Γ ⊢ s₂ = t₂ : B{s₁/x}
       -- --------------------------------------------
@@ -228,10 +228,10 @@ namespace Term
       --
       -- [todo] η for π ≥ 0 maybe
       (Pair sFst sSnd {}, Pair tFst tSnd {}) => do
-        compare0 defs ctx fst sFst tFst
-        compare0 defs ctx (sub1 snd (Ann sFst fst fst.loc)) sSnd tSnd
+        compare0 defs ctx sg fst sFst tFst
+        compare0 defs ctx sg (sub1 snd (Ann sFst fst fst.loc)) sSnd tSnd
 
-      (E e, E f) => ignore $ Elim.compare0 defs ctx e f
+      (E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
 
       (Pair {}, E _)     => clashT s.loc ctx ty s t
       (E _,     Pair {}) => clashT s.loc ctx ty s t
@@ -240,7 +240,7 @@ namespace Term
       (E _,     t) => wrongType t.loc ctx ty t
       (s,       _) => wrongType s.loc ctx ty s
 
-  compare0' defs ctx ty@(Enum {}) s t = local_ Equal $
+  compare0' defs ctx sg ty@(Enum {}) s t = local_ Equal $
     case (s, t) of
       -- --------------------
       --  Γ ⊢ `t = `t : {ts}
@@ -248,7 +248,7 @@ namespace Term
       -- t ∈ ts is in the typechecker, not here, ofc
       (Tag t1 {}, Tag t2 {}) =>
         unless (t1 == t2) $ clashT s.loc ctx ty s t
-      (E e, E f) => ignore $ Elim.compare0 defs ctx e f
+      (E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
 
       (Tag {}, E _)    => clashT s.loc ctx ty s t
       (E _,    Tag {}) => clashT s.loc ctx ty s t
@@ -257,14 +257,14 @@ namespace Term
       (E _,    t) => wrongType t.loc ctx ty t
       (s,      _) => wrongType s.loc ctx ty s
 
-  compare0' _ _ (Eq {}) _ _ =
+  compare0' _ _ _ (Eq {}) _ _ =
     -- ✨ uip ✨
     --
     -- ----------------------------
     --  Γ ⊢ e = f : Eq [i ⇒ A] s t
     pure ()
 
-  compare0' defs ctx nat@(Nat {}) s t = local_ Equal $
+  compare0' defs ctx sg nat@(Nat {}) s t = local_ Equal $
     case (s, t) of
       -- ---------------
       --  Γ ⊢ 0 = 0 : ℕ
@@ -273,9 +273,9 @@ namespace Term
       --      Γ ⊢ s = t : ℕ
       -- -------------------------
       --  Γ ⊢ succ s = succ t : ℕ
-      (Succ s' {}, Succ t' {}) => compare0 defs ctx nat s' t'
+      (Succ s' {}, Succ t' {}) => compare0 defs ctx sg nat s' t'
 
-      (E e, E f) => ignore $ Elim.compare0 defs ctx e f
+      (E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
 
       (Zero {}, Succ {}) => clashT s.loc ctx nat s t
       (Zero {}, E _)     => clashT s.loc ctx nat s t
@@ -289,12 +289,12 @@ namespace Term
       (E _,     t) => wrongType t.loc ctx nat t
       (s,       _) => wrongType s.loc ctx nat s
 
-  compare0' defs ctx bty@(BOX q ty {}) s t = local_ Equal $
+  compare0' defs ctx sg bty@(BOX q ty {}) s t = local_ Equal $
     case (s, t) of
       --     Γ ⊢ s = t : A
       -- -----------------------
       --  Γ ⊢ [s] = [t] : [π.A]
-      (Box s _, Box t _) => compare0 defs ctx ty s t
+      (Box s _, Box t _) => compare0 defs ctx sg ty s t
 
       --   Γ ⊢ s = (case1 e return A of {[x] ⇒ x}) ⇐ A
       -- -----------------------------------------------
@@ -302,7 +302,7 @@ namespace Term
       (Box s loc, E f)       => eta s f
       (E e,       Box t loc) => eta t e
 
-      (E e, E f) => ignore $ Elim.compare0 defs ctx e f
+      (E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
 
       (Box {}, _) => wrongType t.loc ctx bty t
       (E   _,  _) => wrongType t.loc ctx bty t
@@ -312,20 +312,20 @@ namespace Term
     eta s e = do
       nm <- mnb "inner" e.loc
       let e = CaseBox One e (SN ty) (SY [< nm] (BVT 0 nm.loc)) e.loc
-      compare0 defs ctx ty s (E e)
+      compare0 defs ctx sg ty s (E e)
 
-  compare0' defs ctx ty@(E _) s t = do
+  compare0' defs ctx sg 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, …
     let E e = s | _ => wrongType s.loc ctx ty s
         E f = t | _ => wrongType t.loc ctx ty t
-    ignore $ Elim.compare0 defs ctx e f
+    ignore $ Elim.compare0 defs ctx sg e f
 
 
 private covering
 compareType' : (defs : Definitions) -> EqContext n -> (s, t : Term 0 n) ->
-               (0 _ : NotRedex defs s) => (0 _ : So (isTyConE s)) =>
-               (0 _ : NotRedex defs t) => (0 _ : So (isTyConE t)) =>
+               (0 _ : NotRedex defs SZero s) => (0 _ : So (isTyConE s)) =>
+               (0 _ : NotRedex defs SZero t) => (0 _ : So (isTyConE t)) =>
                (0 _ : So (sameTyCon s t)) =>
                Eff EqualInner ()
 -- equality is the same as subtyping, except with the
@@ -363,8 +363,8 @@ compareType' defs ctx (Eq {ty = sTy, l = sl, r = sr, _})
   compareType defs (extendDim sTy.name One  ctx) sTy.one  tTy.one
   ty <- bigger sTy tTy
   local_ Equal $ do
-    Term.compare0 defs ctx ty.zero sl tl
-    Term.compare0 defs ctx ty.one  sr tr
+    Term.compare0 defs ctx SZero ty.zero sl tl
+    Term.compare0 defs ctx SZero ty.one  sr tr
 
 compareType' defs ctx s@(Enum tags1 {}) t@(Enum tags2 {}) = do
   -- ------------------
@@ -386,7 +386,7 @@ compareType' defs ctx (BOX pi a loc) (BOX rh b {}) = do
 compareType' defs ctx (E e) (E f) = do
   -- no fanciness needed here cos anything other than a neutral
   -- has been inlined by whnf
-  ignore $ Elim.compare0 defs ctx e f
+  ignore $ Elim.compare0 defs ctx SZero e f
 
 
 private
@@ -411,12 +411,12 @@ namespace Elim
   EqualElim = InnerErrEff :: EqualInner
 
   private covering
-  computeElimTypeE : (defs : Definitions) -> EqContext n ->
-                     (e : Elim 0 n) -> (0 ne : NotRedex defs e) =>
+  computeElimTypeE : (defs : Definitions) -> EqContext n -> (sg : SQty) ->
+                     (e : Elim 0 n) -> (0 ne : NotRedex defs sg e) =>
                      Eff EqualElim (Term 0 n)
-  computeElimTypeE defs ectx e =
+  computeElimTypeE defs ectx sg e =
     let Val n = ectx.termLen in
-    lift $ computeElimType defs (toWhnfContext ectx) e
+    lift $ computeElimType defs (toWhnfContext ectx) sg e
 
   private
   putError : Has InnerErrEff fs => Error -> Eff fs ()
@@ -427,12 +427,12 @@ namespace Elim
   try act = lift $ catch putError $ lift act {fs' = EqualElim}
 
   private covering %inline
-  clashE : (defs : Definitions) -> EqContext n ->
-           (e, f : Elim 0 n) -> (0 nf : NotRedex defs f) =>
+  clashE : (defs : Definitions) -> EqContext n -> (sg : SQty) ->
+           (e, f : Elim 0 n) -> (0 nf : NotRedex defs sg f) =>
            Eff EqualElim (Term 0 n)
-  clashE defs ctx e f = do
+  clashE defs ctx sg e f = do
     putError $ ClashE e.loc ctx !mode e f
-    computeElimTypeE defs ctx f
+    computeElimTypeE defs ctx sg f
 
 
   ||| compare two type-case branches, which came from the arms of the given
@@ -454,24 +454,24 @@ namespace Elim
                   (b1, b2 : TypeCaseArmBody k 0 n) ->
                   Eff EqualElim ()
     compareArm_ defs ctx KTYPE ret u b1 b2 =
-      try $ Term.compare0 defs ctx ret b1.term b2.term
+      try $ Term.compare0 defs ctx SZero ret b1.term b2.term
 
     compareArm_ defs ctx KPi ret u b1 b2 = do
       let [< a, b] = b1.names
           ctx = extendTyN0
             [< (a, TYPE u a.loc),
                (b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx
-      try $ Term.compare0 defs ctx (weakT 2 ret) b1.term b2.term
+      try $ Term.compare0 defs ctx SZero (weakT 2 ret) b1.term b2.term
 
     compareArm_ defs ctx KSig ret u b1 b2 = do
       let [< a, b] = b1.names
           ctx = extendTyN0
             [< (a, TYPE u a.loc),
                (b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx
-      try $ Term.compare0 defs ctx (weakT 2 ret) b1.term b2.term
+      try $ Term.compare0 defs ctx SZero (weakT 2 ret) b1.term b2.term
 
     compareArm_ defs ctx KEnum ret u b1 b2 =
-      try $ Term.compare0 defs ctx ret b1.term b2.term
+      try $ Term.compare0 defs ctx SZero ret b1.term b2.term
 
     compareArm_ defs ctx KEq ret u b1 b2 = do
       let [< a0, a1, a, l, r] = b1.names
@@ -481,45 +481,45 @@ namespace Elim
                (a,  Eq0 (TYPE u a.loc) (BVT 1 a0.loc) (BVT 0 a1.loc) a.loc),
                (l,  BVT 2 a0.loc),
                (r,  BVT 2 a1.loc)] ctx
-      try $ Term.compare0 defs ctx (weakT 5 ret) b1.term b2.term
+      try $ Term.compare0 defs ctx SZero (weakT 5 ret) b1.term b2.term
 
     compareArm_ defs ctx KNat ret u b1 b2 =
-      try $ Term.compare0 defs ctx ret b1.term b2.term
+      try $ Term.compare0 defs ctx SZero ret b1.term b2.term
 
     compareArm_ defs ctx KBOX ret u b1 b2 = do
       let ctx = extendTy0 b1.name (TYPE u b1.name.loc) ctx
-      try $ Term.compare0 defs ctx (weakT 1 ret) b1.term b1.term
+      try $ Term.compare0 defs ctx SZero (weakT 1 ret) b1.term b1.term
 
 
   private covering
-  compare0Inner : Definitions -> EqContext n -> (e, f : Elim 0 n) ->
-                  Eff EqualElim (Term 0 n)
+  compare0Inner : Definitions -> EqContext n -> (sg : SQty) ->
+                  (e, f : Elim 0 n) -> Eff EqualElim (Term 0 n)
 
   private covering
-  compare0Inner' : (defs : Definitions) -> EqContext n ->
+  compare0Inner' : (defs : Definitions) -> EqContext n -> (sg : SQty) ->
                    (e, f : Elim 0 n) ->
-                   (0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) ->
+                   (0 ne : NotRedex defs sg e) -> (0 nf : NotRedex defs sg f) ->
                    Eff EqualElim (Term 0 n)
 
-  compare0Inner' defs ctx e@(F {}) f _ _ = do
-    if e == f then computeElimTypeE defs ctx f
-              else clashE defs ctx e f
+  compare0Inner' defs ctx sg e@(F {}) f _ _ = do
+    if e == f then computeElimTypeE defs ctx sg f
+              else clashE defs ctx sg e f
 
-  compare0Inner' defs ctx e@(B {}) f _ _ = do
-    if e == f then computeElimTypeE defs ctx f
-              else clashE defs ctx e f
+  compare0Inner' defs ctx sg e@(B {}) f _ _ = do
+    if e == f then computeElimTypeE defs ctx sg f
+              else clashE defs ctx sg e f
 
   --  Ψ | Γ ⊢ e = f ⇒ π.(x : A) → B
   --  Ψ | Γ ⊢ s = t ⇐ A
   -- -------------------------------
   --  Ψ | Γ ⊢ e s = f t ⇒ B[s∷A/x]
-  compare0Inner' defs ctx (App e s eloc) (App f t floc) ne nf = do
-    ety <- compare0Inner defs ctx e f
-    (_, arg, res) <- expectPi defs ctx eloc ety
-    try $ Term.compare0 defs ctx arg s t
+  compare0Inner' defs ctx sg (App e s eloc) (App f t floc) ne nf = do
+    ety <- compare0Inner defs ctx sg e f
+    (_, arg, res) <- expectPi defs ctx sg eloc ety
+    try $ Term.compare0 defs ctx sg arg s t
     pure $ sub1 res $ Ann s arg s.loc
-  compare0Inner' defs ctx e'@(App {}) f' ne nf =
-    clashE defs ctx e' f'
+  compare0Inner' defs ctx sg e'@(App {}) f' ne nf =
+    clashE defs ctx sg e' f'
 
   --  Ψ | Γ ⊢ e = f ⇒ (x : A) × B
   --  Ψ | Γ, 0.p : (x : A) × B ⊢ Q = R
@@ -527,22 +527,22 @@ namespace Elim
   -- -----------------------------------------------------------
   --    Ψ | Γ ⊢ caseπ e return Q of { (x, y) ⇒ s }
   --          = caseπ f return R of { (x, y) ⇒ t } ⇒ Q[e/p]
-  compare0Inner' defs ctx (CasePair epi e eret ebody eloc)
-                          (CasePair fpi f fret fbody floc) ne nf =
+  compare0Inner' defs ctx sg (CasePair epi e eret ebody eloc)
+                             (CasePair fpi f fret fbody floc) ne nf =
     local_ Equal $ do
-      ety <- compare0Inner defs ctx e f
-      (fst, snd) <- expectSig defs ctx eloc ety
+      ety <- compare0Inner defs ctx sg e f
+      (fst, snd) <- expectSig defs ctx sg eloc ety
       let [< x, y] = ebody.names
       try $ do
         compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term
         Term.compare0 defs
-          (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx)
+          (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx) sg
           (substCasePairRet ebody.names ety eret)
           ebody.term fbody.term
         expectEqualQ e.loc epi fpi
       pure $ sub1 eret e
-  compare0Inner' defs ctx e'@(CasePair {}) f' ne nf =
-    clashE defs ctx e' f'
+  compare0Inner' defs ctx sg e'@(CasePair {}) f' ne nf =
+    clashE defs ctx sg e' f'
 
   --  Ψ | Γ ⊢ e = f ⇒ {𝐚s}
   --  Ψ | Γ, x : {𝐚s} ⊢ Q = R
@@ -550,20 +550,20 @@ namespace Elim
   -- --------------------------------------------------
   --  Ψ | Γ ⊢ caseπ e return Q of { '𝐚ᵢ ⇒ sᵢ }
   --        = caseπ f return R of { '𝐚ᵢ ⇒ tᵢ } ⇒ Q[e/x]
-  compare0Inner' defs ctx (CaseEnum epi e eret earms eloc)
-                          (CaseEnum fpi f fret farms floc) ne nf =
+  compare0Inner' defs ctx sg (CaseEnum epi e eret earms eloc)
+                             (CaseEnum fpi f fret farms floc) ne nf =
     local_ Equal $ do
-      ety <- compare0Inner defs ctx e f
+      ety <- compare0Inner defs ctx sg e f
       try $
         compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term
       for_ (SortedMap.toList earms) $ \(t, l) => do
         let Just r = lookup t farms
           | Nothing => putError $ TagNotIn floc t (fromList $ keys farms)
         let t' = Ann (Tag t l.loc) ety l.loc
-        try $ Term.compare0 defs ctx (sub1 eret t') l r
+        try $ Term.compare0 defs ctx sg (sub1 eret t') l r
       try $ expectEqualQ eloc epi fpi
       pure $ sub1 eret e
-  compare0Inner' defs ctx e@(CaseEnum {}) f _ _ = clashE defs ctx e f
+  compare0Inner' defs ctx sg e@(CaseEnum {}) f _ _ = clashE defs ctx sg e f
 
   --  Ψ | Γ ⊢ e = f ⇒ ℕ
   --  Ψ | Γ, x : ℕ ⊢ Q = R
@@ -573,23 +573,23 @@ namespace Elim
   --  Ψ | Γ ⊢ caseπ e return Q of { 0 ⇒ s₀; x, π.y ⇒ s₁ }
   --        = caseπ f return R of { 0 ⇒ t₀; x, π.y ⇒ t₁ }
   --        ⇒ Q[e/x]
-  compare0Inner' defs ctx (CaseNat epi epi' e eret ezer esuc eloc)
-                          (CaseNat fpi fpi' f fret fzer fsuc floc) ne nf =
+  compare0Inner' defs ctx sg (CaseNat epi epi' e eret ezer esuc eloc)
+                             (CaseNat fpi fpi' f fret fzer fsuc floc) ne nf =
     local_ Equal $ do
-      ety <- compare0Inner defs ctx e f
+      ety <- compare0Inner defs ctx sg e f
       let [< p, ih] = esuc.names
       try $ do
         compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term
-        Term.compare0 defs ctx
+        Term.compare0 defs ctx sg
           (sub1 eret (Ann (Zero ezer.loc) (Nat ezer.loc) ezer.loc))
           ezer fzer
         Term.compare0 defs
-          (extendTyN [< (epi, p, Nat p.loc), (epi', ih, eret.term)] ctx)
+          (extendTyN [< (epi, p, Nat p.loc), (epi', ih, eret.term)] ctx) sg
           (substCaseSuccRet esuc.names eret) esuc.term fsuc.term
         expectEqualQ e.loc epi  fpi
         expectEqualQ e.loc epi' fpi'
       pure $ sub1 eret e
-  compare0Inner' defs ctx e@(CaseNat {}) f _ _ = clashE defs ctx e f
+  compare0Inner' defs ctx sg e@(CaseNat {}) f _ _ = clashE defs ctx sg e f
 
   --  Ψ | Γ ⊢ e = f ⇒ [ρ. A]
   --  Ψ | Γ, x : [ρ. A] ⊢ Q = R
@@ -597,32 +597,34 @@ namespace Elim
   -- --------------------------------------------------
   --  Ψ | Γ ⊢ caseπ e return Q of { [x] ⇒ s }
   --        = caseπ f return R of { [x] ⇒ t } ⇒ Q[e/x]
-  compare0Inner' defs ctx (CaseBox epi e eret ebody eloc)
-                          (CaseBox fpi f fret fbody floc) ne nf =
+  compare0Inner' defs ctx sg (CaseBox epi e eret ebody eloc)
+                             (CaseBox fpi f fret fbody floc) ne nf =
     local_ Equal $ do
-      ety <- compare0Inner defs ctx e f
-      (q, ty) <- expectBOX defs ctx eloc ety
+      ety <- compare0Inner defs ctx sg e f
+      (q, ty) <- expectBOX defs ctx sg eloc ety
       try $ do
         compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term
-        Term.compare0 defs (extendTy (epi * q) ebody.name ty ctx)
+        Term.compare0 defs (extendTy (epi * q) ebody.name ty ctx) sg
           (substCaseBoxRet ebody.name ety eret)
           ebody.term fbody.term
         expectEqualQ eloc epi fpi
       pure $ sub1 eret e
-  compare0Inner' defs ctx e@(CaseBox {}) f _ _ = clashE defs ctx e f
+  compare0Inner' defs ctx sg e@(CaseBox {}) f _ _ = clashE defs ctx sg e f
 
   -- (no neutral dim apps in a closed dctx)
-  compare0Inner' _ _ (DApp _ (K {}) _) _ ne _ = void $ absurd $ noOr2 $ noOr2 ne
-  compare0Inner' _ _ _ (DApp _ (K {}) _) _ nf = void $ absurd $ noOr2 $ noOr2 nf
+  compare0Inner' _ _ _ (DApp _ (K {}) _) _ ne _ =
+    void $ absurd $ noOr2 $ noOr2 ne
+  compare0Inner' _ _ _ _ (DApp _ (K {}) _) _ nf =
+    void $ absurd $ noOr2 $ noOr2 nf
 
   --  Ψ | Γ ⊢ s <: t : B
   -- --------------------------------
   --  Ψ | Γ ⊢ (s ∷ A) <: (t ∷ B) ⇒ B
   --
   -- and similar for :> and A
-  compare0Inner' defs ctx (Ann s a _) (Ann t b _) _ _ = do
+  compare0Inner' defs ctx sg (Ann s a _) (Ann t b _) _ _ = do
     ty <- bigger a b
-    try $ Term.compare0 defs ctx ty s t
+    try $ Term.compare0 defs ctx sg ty s t
     pure ty
 
   --  Ψ | Γ ⊢ A‹p₁/𝑖› <: B‹p₂/𝑖›
@@ -631,82 +633,86 @@ namespace Elim
   -- -----------------------------------------------------------
   --  Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ s
   --       <: coe [𝑖 ⇒ B] @p₂ @q₂ t ⇒ B‹q₂/𝑖›
-  compare0Inner' defs ctx (Coe ty1 p1 q1 val1 _)
-                          (Coe ty2 p2 q2 val2 _) ne nf = do
+  compare0Inner' defs ctx sg (Coe ty1 p1 q1 val1 _)
+                             (Coe ty2 p2 q2 val2 _) ne nf = do
     let ty1p = dsub1 ty1 p1; ty2p = dsub1 ty2 p2
         ty1q = dsub1 ty1 q1; ty2q = dsub1 ty2 q2
     (ty_p, ty_q) <- bigger (ty1p, ty1q) (ty2p, ty2q)
     try $ do
       compareType defs ctx ty1p ty2p
       compareType defs ctx ty1q ty2q
-      Term.compare0 defs ctx ty_p val1 val2
+      Term.compare0 defs ctx sg ty_p val1 val2
     pure $ ty_q
-  compare0Inner' defs ctx e@(Coe {}) f _ _ = clashE defs ctx e f
+  compare0Inner' defs ctx sg e@(Coe {}) f _ _ = clashE defs ctx sg e f
 
   -- (no neutral compositions in a closed dctx)
-  compare0Inner' _ _ (Comp {r = K e _, _}) _ ne _ = void $ absurd $ noOr2 ne
-  compare0Inner' _ _ (Comp {r = B i _, _}) _ _ _ = absurd i
-  compare0Inner' _ _ _ (Comp {r = K _ _, _}) _ nf = void $ absurd $ noOr2 nf
+  compare0Inner' _ _ _ (Comp {r = K {}, _}) _ ne _ = void $ absurd $ noOr2 ne
+  compare0Inner' _ _ _ (Comp {r = B i _, _}) _ _ _ = absurd i
+  compare0Inner' _ _ _ _ (Comp {r = K {}, _}) _ nf = void $ absurd $ noOr2 nf
 
   -- (type case equality purely structural)
-  compare0Inner' defs ctx (TypeCase ty1 ret1 arms1 def1 eloc)
-                          (TypeCase ty2 ret2 arms2 def2 floc) ne _ =
-    local_ Equal $ do
-      ety <- compare0Inner defs ctx ty1 ty2
-      u   <- expectTYPE defs ctx eloc ety
-      try $ do
-        compareType defs ctx ret1 ret2
-        compareType defs ctx def1 def2
-      for_ allKinds $ \k =>
-        compareArm defs ctx k ret1 u
-          (lookupPrecise k arms1) (lookupPrecise k arms2) def1
-      pure ret1
-  compare0Inner' defs ctx e@(TypeCase {}) f _ _ = clashE defs ctx e f
+  compare0Inner' defs ctx sg (TypeCase ty1 ret1 arms1 def1 eloc)
+                             (TypeCase ty2 ret2 arms2 def2 floc) ne _ =
+    case sg `decEq` SZero of
+      Yes Refl => local_ Equal $ do
+        ety <- compare0Inner defs ctx SZero ty1 ty2
+        u   <- expectTYPE defs ctx SZero eloc ety
+        try $ do
+          compareType defs ctx ret1 ret2
+          compareType defs ctx def1 def2
+        for_ allKinds $ \k =>
+          compareArm defs ctx k ret1 u
+            (lookupPrecise k arms1) (lookupPrecise k arms2) def1
+        pure ret1
+      No _ => do
+        putError $ ClashQ eloc sg.qty Zero
+        computeElimTypeE defs ctx sg $ TypeCase ty1 ret1 arms1 def1 eloc
+  compare0Inner' defs ctx sg e@(TypeCase {}) f _ _ = clashE defs ctx sg e f
 
   --     Ψ | Γ ⊢ s <: f ⇐ A
   -- --------------------------
   --  Ψ | Γ ⊢ (s ∷ A) <: f ⇒ A
   --
   -- and vice versa
-  compare0Inner' defs ctx (Ann s a _) f _ _ = do
-    try $ Term.compare0 defs ctx a s (E f)
+  compare0Inner' defs ctx sg (Ann s a _) f _ _ = do
+    try $ Term.compare0 defs ctx sg a s (E f)
     pure a
-  compare0Inner' defs ctx e (Ann t b _) _ _ = do
-    try $ Term.compare0 defs ctx b (E e) t
+  compare0Inner' defs ctx sg e (Ann t b _) _ _ = do
+    try $ Term.compare0 defs ctx sg b (E e) t
     pure b
-  compare0Inner' defs ctx e@(Ann {}) f _ _ =
-    clashE defs ctx e f
+  compare0Inner' defs ctx sg e@(Ann {}) f _ _ =
+    clashE defs ctx sg e f
 
-  compare0Inner defs ctx e f = do
+  compare0Inner defs ctx sg e f = do
     let Val n = ctx.termLen
-    Element e ne <- whnf defs ctx e.loc e
-    Element f nf <- whnf defs ctx f.loc f
-    ty <- compare0Inner' defs ctx e f ne nf
-    if !(lift $ isSubSing defs ctx ty)
+    Element e ne <- whnf defs ctx sg e.loc e
+    Element f nf <- whnf defs ctx sg f.loc f
+    ty <- compare0Inner' defs ctx sg e f ne nf
+    if !(lift $ isSubSing defs ctx sg ty) && isJust !(getAt InnerErr)
        then putAt InnerErr Nothing
-       else modifyAt InnerErr $ map $ WhileComparingE ctx !mode e f
+       else modifyAt InnerErr $ map $ WhileComparingE ctx !mode sg e f
     pure ty
 
 
 namespace Term
-  compare0 defs ctx ty s t =
-    wrapErr (WhileComparingT ctx !mode ty s t) $ do
+  compare0 defs ctx sg ty s t =
+    wrapErr (WhileComparingT ctx !mode sg ty s t) $ do
       let Val n = ctx.termLen
-      Element ty' _ <- whnf defs ctx ty.loc ty
-      Element s'  _ <- whnf defs ctx s.loc  s
-      Element t'  _ <- whnf defs ctx t.loc  t
+      Element ty' _ <- whnf defs ctx SZero ty.loc ty
+      Element s'  _ <- whnf defs ctx sg s.loc  s
+      Element t'  _ <- whnf defs ctx sg t.loc  t
       tty <- ensureTyCon ty.loc ctx ty'
-      compare0' defs ctx ty' s' t'
+      compare0' defs ctx sg ty' s' t'
 
 namespace Elim
-  compare0 defs ctx e f = do
-    (ty, err) <- runStateAt InnerErr Nothing $ compare0Inner defs ctx e f
+  compare0 defs ctx sg e f = do
+    (ty, err) <- runStateAt InnerErr Nothing $ compare0Inner defs ctx sg e f
     maybe (pure ty) throw err
 
 compareType defs ctx s t = do
   let Val n = ctx.termLen
-  Element s' _ <- whnf defs ctx s.loc s
-  Element t' _ <- whnf defs ctx t.loc t
+  Element s' _ <- whnf defs ctx SZero s.loc s
+  Element t' _ <- whnf defs ctx SZero t.loc t
   ts <- ensureTyCon s.loc ctx s'
   tt <- ensureTyCon t.loc ctx t'
   st <- either pure (const $ clashTy s.loc ctx s' t') $
@@ -744,9 +750,9 @@ parameters (loc : Loc) (ctx : TyContext d n)
 
     namespace Term
       export covering
-      compare : (ty, s, t : Term d n) -> Eff Equal ()
-      compare ty s t = runCompare (fdvAll [ty, s, t]) $ \defs, ectx, th =>
-        compare0 defs ectx (ty // th) (s // th) (t // th)
+      compare : SQty -> (ty, s, t : Term d n) -> Eff Equal ()
+      compare sg ty s t = runCompare (fdvAll [ty, s, t]) $ \defs, ectx, th =>
+        compare0 defs ectx sg (ty // th) (s // th) (t // th)
 
       export covering
       compareType : (s, t : Term d n) -> Eff Equal ()
@@ -757,13 +763,13 @@ parameters (loc : Loc) (ctx : TyContext d n)
       ||| you don't have to pass the type in but the arguments must still be
       ||| of the same type!!
       export covering
-      compare : (e, f : Elim d n) -> Eff Equal ()
-      compare e f = runCompare (fdvAll [e, f]) $ \defs, ectx, th =>
-        ignore $ compare0 defs ectx (e // th) (f // th)
+      compare : SQty -> (e, f : Elim d n) -> Eff Equal ()
+      compare sg e f = runCompare (fdvAll [e, f]) $ \defs, ectx, th =>
+        ignore $ compare0 defs ectx sg (e // th) (f // th)
 
   namespace Term
     export covering %inline
-    equal, sub, super : (ty, s, t : Term d n) -> Eff Equal ()
+    equal, sub, super : SQty -> (ty, s, t : Term d n) -> Eff Equal ()
     equal = compare Equal
     sub   = compare Sub
     super = compare Super
@@ -776,7 +782,7 @@ parameters (loc : Loc) (ctx : TyContext d n)
 
   namespace Elim
     export covering %inline
-    equal, sub, super : (e, f : Elim d n) -> Eff Equal ()
+    equal, sub, super : SQty -> (e, f : Elim d n) -> Eff Equal ()
     equal = compare Equal
     sub   = compare Sub
     super = compare Super
diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr
index e8282c4..1f05ab9 100644
--- a/lib/Quox/Parser/FromParser.idr
+++ b/lib/Quox/Parser/FromParser.idr
@@ -267,9 +267,9 @@ fromPTerm = fromPTermWith [<] [<]
 
 export
 globalPQty : Has (Except Error) fs => (q : Qty) -> Loc -> Eff fs GQty
-globalPQty pi loc = case choose $ isGlobal pi of
-  Left  y => pure $ Element pi y
-  Right _ => throw $ QtyNotGlobal loc pi
+globalPQty pi loc = case toGlobal pi of
+  Just g  => pure g
+  Nothing => throw $ QtyNotGlobal loc pi
 
 export
 fromPBaseNameNS : Has (StateL NS Mods) fs => PBaseName -> Eff fs Name
diff --git a/lib/Quox/Syntax/Qty.idr b/lib/Quox/Syntax/Qty.idr
index 1aa0ba0..5133eff 100644
--- a/lib/Quox/Syntax/Qty.idr
+++ b/lib/Quox/Syntax/Qty.idr
@@ -78,26 +78,16 @@ lub p q = if p == q then p else Any
 ||| to maintain subject reduction, only 0 or 1 can occur
 ||| for the subject of a typing judgment. see @qtt, §2.3 for more detail
 public export
-isSubj : Qty -> Bool
-isSubj Zero = True
-isSubj One  = True
-isSubj Any  = False
-
-public export
-SQty : Type
-SQty = Subset Qty $ So . isSubj
-
-public export %inline
-szero, sone : SQty
-szero = Element Zero Oh
-sone  = Element One  Oh
+data SQty = SZero | SOne
+%runElab derive "SQty" [Eq, Ord, Show]
+%name Qty.SQty sg
 
 ||| "σ ⨴ π"
 |||
-||| σ ⨭ π is 0 if either of σ or π are, otherwise it is σ.
+||| σ ⨴ π is 0 if either of σ or π are, otherwise it is σ.
 public export
 subjMult : SQty -> Qty -> SQty
-subjMult _  Zero = szero
+subjMult _  Zero = SZero
 subjMult sg _    = sg
 
 
@@ -105,23 +95,59 @@ subjMult sg _    = sg
 ||| quantity of 1, so the only distinction is whether it is present
 ||| at runtime at all or not
 public export
-isGlobal : Qty -> Bool
-isGlobal Zero = True
-isGlobal One  = False
-isGlobal Any  = True
+data GQty = GZero | GAny
+%runElab derive "GQty" [Eq, Ord, Show]
+%name GQty rh
 
 public export
-GQty : Type
-GQty = Subset Qty $ So . isGlobal
-
-public export
-gzero, gany : GQty
-gzero = Element Zero Oh
-gany  = Element Any  Oh
+toGlobal : Qty -> Maybe GQty
+toGlobal Zero = Just GZero
+toGlobal Any  = Just GAny
+toGlobal One  = Nothing
 
 ||| when checking a definition, a 0 definition is checked at 0,
 ||| but an ω definition is checked at 1 since ω isn't a subject quantity
 public export %inline
 globalToSubj : GQty -> SQty
-globalToSubj (Element Zero _) = szero
-globalToSubj (Element Any  _) = sone
+globalToSubj GZero = SZero
+globalToSubj GAny  = SOne
+
+
+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
+
+public export
+DecEq SQty where
+  decEq SZero SZero = Yes Refl
+  decEq SZero SOne  = No $ \case _ impossible
+  decEq SOne  SZero = No $ \case _ impossible
+  decEq SOne  SOne  = Yes Refl
+
+public export
+DecEq GQty where
+  decEq GZero GZero = Yes Refl
+  decEq GZero GAny  = No $ \case _ impossible
+  decEq GAny  GZero = No $ \case _ impossible
+  decEq GAny  GAny  = Yes Refl
+
+
+namespace SQty
+  public export %inline
+  (.qty) : SQty -> Qty
+  (SZero).qty = Zero
+  (SOne).qty  = One
+
+namespace GQty
+  public export %inline
+  (.qty) : GQty -> Qty
+  (GZero).qty = Zero
+  (GAny).qty  = Any
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index 3809760..96f3d9e 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -88,7 +88,7 @@ mutual
   ||| `check0 ctx subj ty` checks a term (as `check`) in a zero context.
   export covering %inline
   check0 : TyContext d n -> Term d n -> Term d n -> Eff TC ()
-  check0 ctx tm ty = ignore $ check ctx szero tm ty
+  check0 ctx tm ty = ignore $ check ctx SZero tm ty
     -- the output will always be 𝟎 because the subject quantity is 0
 
   ||| `check`, assuming the dimension context is consistent
@@ -96,7 +96,7 @@ mutual
   checkC : (ctx : TyContext d n) -> SQty -> Term d n -> Term d n ->
            Eff TC (CheckResult' n)
   checkC ctx sg subj ty =
-    wrapErr (WhileChecking ctx sg.fst subj ty) $
+    wrapErr (WhileChecking ctx sg subj ty) $
     checkCNoWrap ctx sg subj ty
 
   export covering %inline
@@ -142,7 +142,7 @@ mutual
   inferC : (ctx : TyContext d n) -> SQty -> Elim d n ->
            Eff TC (InferResult' d n)
   inferC ctx sg subj =
-    wrapErr (WhileInferring ctx sg.fst subj) $
+    wrapErr (WhileInferring ctx sg subj) $
       let Element subj nc = pushSubsts subj in
       infer' ctx sg subj
 
@@ -152,8 +152,8 @@ mutual
                 (subj : Term d n) -> (0 nc : NotClo subj) => Term d n ->
                 Eff TC (CheckResult' n)
   toCheckType ctx sg t ty = do
-    u <- expectTYPE !(askAt DEFS) ctx ty.loc ty
-    expectEqualQ t.loc Zero sg.fst
+    u <- expectTYPE !(askAt DEFS) ctx sg ty.loc ty
+    expectEqualQ t.loc Zero sg.qty
     checkTypeNoWrap ctx t (Just u)
     pure $ zeroFor ctx
 
@@ -167,10 +167,10 @@ mutual
   check' ctx sg t@(Pi {}) ty = toCheckType ctx sg t ty
 
   check' ctx sg (Lam body loc) ty = do
-    (qty, arg, res) <- expectPi !(askAt DEFS) ctx ty.loc ty
+    (qty, arg, res) <- expectPi !(askAt DEFS) ctx SZero ty.loc ty
     -- if Ψ | Γ, x : A ⊢ σ · t ⇐ B ⊳ Σ, ρ·x
     -- with ρ ≤ σπ
-    let qty' = sg.fst * qty
+    let qty' = sg.qty * qty
     qout <- checkC (extendTy qty' body.name arg ctx) sg body.term res.term
     -- then Ψ | Γ ⊢ σ · (λx ⇒ t) ⇐ (π·x : A) → B ⊳ Σ
     popQ loc qty' qout
@@ -178,7 +178,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 !(askAt DEFS) ctx ty.loc ty
+    (tfst, tsnd) <- expectSig !(askAt DEFS) ctx SZero ty.loc ty
     -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ₁
     qfst <- checkC ctx sg fst tfst
     let tsnd = sub1 tsnd (Ann fst tfst fst.loc)
@@ -190,7 +190,7 @@ mutual
   check' ctx sg t@(Enum {}) ty = toCheckType ctx sg t ty
 
   check' ctx sg (Tag t loc) ty = do
-    tags <- expectEnum !(askAt DEFS) ctx ty.loc ty
+    tags <- expectEnum !(askAt DEFS) ctx SZero ty.loc ty
     -- if t ∈ ts
     unless (t `elem` tags) $ throw $ TagNotIn loc t tags
     -- then Ψ | Γ ⊢ σ · t ⇐ {ts} ⊳ 𝟎
@@ -199,33 +199,35 @@ mutual
   check' ctx sg t@(Eq {}) ty = toCheckType ctx sg t ty
 
   check' ctx sg (DLam body loc) ty = do
-    (ty, l, r) <- expectEq !(askAt DEFS) ctx ty.loc ty
+    (ty, l, r) <- expectEq !(askAt DEFS) ctx SZero ty.loc ty
     let ctx' = extendDim body.name ctx
         ty   = ty.term
         body = body.term
     -- if Ψ, i | Γ ⊢ σ · t ⇐ A ⊳ Σ
     qout <- checkC ctx' sg body ty
     -- if Ψ, i, i = 0 | Γ ⊢ t = l : A
-    lift $ equal loc (eqDim (B VZ loc) (K Zero loc) ctx') ty body (dweakT 1 l)
+    let ctx0 = eqDim (B VZ loc) (K Zero loc) ctx'
+    lift $ equal loc ctx0 sg ty body $ dweakT 1 l
     -- if Ψ, i, i = 1 | Γ ⊢ t = r : A
-    lift $ equal loc (eqDim (B VZ loc) (K One loc)  ctx') ty body (dweakT 1 r)
+    let ctx1 = eqDim (B VZ loc) (K One loc) ctx'
+    lift $ equal loc ctx1 sg ty body $ dweakT 1 r
     -- then Ψ | Γ ⊢ σ · (δ i ⇒ t) ⇐ Eq [i ⇒ A] l r ⊳ Σ
     pure qout
 
   check' ctx sg t@(Nat {}) ty = toCheckType ctx sg t ty
 
   check' ctx sg (Zero {}) ty = do
-    expectNat !(askAt DEFS) ctx ty.loc ty
+    expectNat !(askAt DEFS) ctx SZero ty.loc ty
     pure $ zeroFor ctx
 
   check' ctx sg (Succ n {}) ty = do
-    expectNat !(askAt DEFS) ctx ty.loc ty
+    expectNat !(askAt DEFS) ctx SZero 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 !(askAt DEFS) ctx ty.loc ty
+    (q, ty) <- expectBOX !(askAt DEFS) ctx SZero ty.loc ty
     -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ
     valout <- checkC ctx sg val ty
     -- then Ψ | Γ ⊢ σ · [s] ⇐ [π.A] ⊳ πΣ
@@ -299,11 +301,11 @@ mutual
 
   checkType' ctx (E e) u = do
     -- if Ψ | Γ ⊢₀ E ⇒ Type ℓ
-    infres <- inferC ctx szero e
+    infres <- inferC ctx SZero e
     -- if Ψ | Γ ⊢ Type ℓ <: Type 𝓀
     case u of
       Just u  => lift $ subtype e.loc ctx infres.type (TYPE u noLoc)
-      Nothing => ignore $ expectTYPE !(askAt DEFS) ctx e.loc infres.type
+      Nothing => ignore $ expectTYPE !(askAt DEFS) ctx SZero e.loc infres.type
     -- then Ψ | Γ ⊢₀ E ⇐ Type 𝓀
 
 
@@ -324,7 +326,7 @@ mutual
     -- if π·x : A {≔ s} in global context
     g <- lookupFree x loc !(askAt DEFS)
     -- if σ ≤ π
-    expectCompatQ loc sg.fst g.qty.fst
+    expectCompatQ loc sg.qty g.qty.qty
     -- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ 𝟎
     let Val d = ctx.dimLen; Val n = ctx.termLen
     pure $ InfRes {type = g.typeAt u, qout = zeroFor ctx}
@@ -332,7 +334,7 @@ mutual
   infer' ctx sg (B i _) =
     -- if x : A ∈ Γ
     -- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ (𝟎, σ·x, 𝟎)
-    pure $ lookupBound sg.fst i ctx.tctx
+    pure $ lookupBound sg.qty i ctx.tctx
   where
     lookupBound : forall n. Qty -> Var n -> TContext d n -> InferResult' d n
     lookupBound pi VZ (ctx :< type) =
@@ -344,7 +346,7 @@ mutual
   infer' ctx sg (App fun arg loc) = do
     -- if Ψ | Γ ⊢ σ · f ⇒ (π·x : A) → B ⊳ Σ₁
     funres <- inferC ctx sg fun
-    (qty, argty, res) <- expectPi !(askAt DEFS) ctx fun.loc funres.type
+    (qty, argty, res) <- expectPi !(askAt DEFS) ctx SZero fun.loc funres.type
     -- if Ψ | Γ ⊢ σ ⨴ π · s ⇐ A ⊳ Σ₂
     argout <- checkC ctx (subjMult sg qty) arg argty
     -- then Ψ | Γ ⊢ σ · f s ⇒ B[s] ⊳ Σ₁ + πΣ₂
@@ -361,12 +363,12 @@ 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 !(askAt DEFS) ctx pair.loc pairres.type
+    (tfst, tsnd) <- expectSig !(askAt DEFS) ctx SZero pair.loc pairres.type
     -- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐
     --    ret[(x, y) ∷ (x : A) × B/p] ⊳ Σ₂, ρ₁·x, ρ₂·y
     -- with ρ₁, ρ₂ ≤ πσ
     let [< x, y]  = body.names
-        pisg    = pi * sg.fst
+        pisg    = pi * sg.qty
         bodyctx = extendTyN [< (pisg, x, tfst), (pisg, y, tsnd.term)] ctx
         bodyty  = substCasePairRet body.names pairres.type ret
     bodyout <- checkC bodyctx sg body.term bodyty >>=
@@ -380,7 +382,7 @@ mutual
   infer' ctx sg (CaseEnum pi t ret arms loc) {d, n} = do
     -- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁
     tres <- inferC ctx sg t
-    ttags <- expectEnum !(askAt DEFS) ctx t.loc tres.type
+    ttags <- expectEnum !(askAt DEFS) ctx SZero 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
@@ -404,7 +406,7 @@ mutual
     -- if Ψ | Γ ⊢ σ · n ⇒ ℕ ⊳ Σn
     nres <- inferC ctx sg n
     let nat = nres.type
-    expectNat !(askAt DEFS) ctx n.loc nat
+    expectNat !(askAt DEFS) ctx SZero n.loc nat
     -- if Ψ | Γ, n : ℕ ⊢₀ A ⇐ Type
     checkTypeC (extendTy Zero ret.name nat ctx) ret.term Nothing
     -- if Ψ | Γ ⊢ σ · zer ⇐ A[0 ∷ ℕ/n] ⊳ Σz
@@ -412,11 +414,11 @@ mutual
     -- if Ψ | Γ, n : ℕ, ih : A ⊢ σ · suc ⇐ A[succ p ∷ ℕ/n] ⊳ Σs, ρ₁.p, ρ₂.ih
     -- with ρ₂ ≤ π'σ, (ρ₁ + ρ₂) ≤ πσ
     let [< p, ih] = suc.names
-        pisg      = pi * sg.fst
+        pisg      = pi * sg.qty
         sucCtx    = extendTyN [< (pisg, p, Nat p.loc), (pi', ih, ret.term)] ctx
         sucType   = substCaseSuccRet suc.names ret
     sucout :< qp :< qih <- checkC sucCtx sg suc.term sucType
-    expectCompatQ loc qih (pi' * sg.fst)
+    expectCompatQ loc qih (pi' * sg.qty)
     -- [fixme] better error here
     expectCompatQ loc (qp + qih) pisg
     -- then Ψ | Γ ⊢ caseπ ⋯ ⇒ A[n] ⊳ πΣn + Σz + ωΣs
@@ -428,12 +430,12 @@ mutual
   infer' ctx sg (CaseBox pi box ret body loc) = do
     -- if Ψ | Γ ⊢ σ · b ⇒ [ρ.A] ⊳ Σ₁
     boxres <- inferC ctx sg box
-    (q, ty) <- expectBOX !(askAt DEFS) ctx box.loc boxres.type
+    (q, ty) <- expectBOX !(askAt DEFS) ctx SZero 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
     --   with ς ≤ ρπσ
-    let qpisg    = q * pi * sg.fst
+    let qpisg    = q * pi * sg.qty
         bodyCtx  = extendTy qpisg body.name ty ctx
         bodyType = substCaseBoxRet body.name ty ret
     bodyout <- checkC bodyCtx sg body.term bodyType >>= popQ loc qpisg
@@ -446,7 +448,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 !(askAt DEFS) ctx fun.loc type
+    ty <- fst <$> expectEq !(askAt DEFS) ctx SZero fun.loc type
     -- then Ψ | Γ ⊢ σ · f p ⇒ A‹p/𝑖› ⊳ Σ
     pure $ InfRes {type = dsub1 ty dim, qout}
 
@@ -462,19 +464,20 @@ mutual
         ctx0 = extendDim j0 $ eqDim r (K Zero j0.loc) ctx
         val0 = getTerm val0
     qout0 <- check ctx0 sg val0 ty'
-    lift $ equal loc (eqDim (B VZ p.loc) p' ctx0) ty' val0 val'
+    lift $ equal loc (eqDim (B VZ p.loc) p' ctx0) sg ty' val0 val'
     let ctx1 = extendDim j1 $ eqDim r (K One j1.loc) ctx
         val1  = getTerm val1
     qout1 <- check ctx1 sg val1 ty'
-    lift $ equal loc (eqDim (B VZ p.loc) p' ctx1) ty' val1 val'
+    lift $ equal loc (eqDim (B VZ p.loc) p' ctx1) sg ty' val1 val'
     let qouts  = qout :: catMaybes [toMaybe qout0, toMaybe qout1]
     pure $ InfRes {type = ty, qout = lubs ctx qouts}
 
   infer' ctx sg (TypeCase ty ret arms def loc) = do
     -- if σ = 0
-    expectEqualQ loc Zero sg.fst
+    expectEqualQ loc Zero sg.qty
     -- if Ψ, Γ ⊢₀ e ⇒ Type u
-    u <- expectTYPE !(askAt DEFS) ctx ty.loc . type =<< inferC ctx szero ty
+    u <- inferC ctx SZero ty >>=
+         expectTYPE !(askAt DEFS) ctx SZero ty.loc . type
     -- if Ψ, Γ ⊢₀ C ⇐ Type (non-dependent return type)
     checkTypeC ctx ret Nothing
     -- if Ψ, Γ' ⊢₀ A ⇐ C for each rhs A
diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr
index 065961e..ad4fec3 100644
--- a/lib/Quox/Typing.idr
+++ b/lib/Quox/Typing.idr
@@ -67,13 +67,13 @@ substCaseBoxRet x dty retty =
 
 parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
   namespace TyContext
-   parameters (ctx : TyContext d n) (loc : Loc)
+   parameters (ctx : TyContext d n) (sg : SQty) (loc : Loc)
     export covering
     whnf : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
-           tm d n -> Eff fs (NonRedex tm d n defs)
+           tm d n -> Eff fs (NonRedex tm d n defs sg)
     whnf tm = do
       let Val n = ctx.termLen; Val d = ctx.dimLen
-      res <- lift $ runExcept $ whnf defs (toWhnfContext ctx) tm
+      res <- lift $ runExcept $ whnf defs (toWhnfContext ctx) sg tm
       rethrow res
 
     private covering %macro
@@ -113,13 +113,13 @@ parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
 
 
   namespace EqContext
-   parameters (ctx : EqContext n) (loc : Loc)
+   parameters (ctx : EqContext n) (sg : SQty) (loc : Loc)
     export covering
     whnf : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
-           tm 0 n -> Eff fs (NonRedex tm 0 n defs)
+           tm 0 n -> Eff fs (NonRedex tm 0 n defs sg)
     whnf tm = do
       let Val n = ctx.termLen
-      res <- lift $ runExcept $ whnf defs (toWhnfContext ctx) tm
+      res <- lift $ runExcept $ whnf defs (toWhnfContext ctx) sg tm
       rethrow res
 
     private covering %macro
diff --git a/lib/Quox/Typing/Error.idr b/lib/Quox/Typing/Error.idr
index 342fb05..a48b4d7 100644
--- a/lib/Quox/Typing/Error.idr
+++ b/lib/Quox/Typing/Error.idr
@@ -87,7 +87,7 @@ data Error
 
 -- extra context
 | WhileChecking
-    (TyContext d n) Qty
+    (TyContext d n) SQty
     (Term d n) -- term
     (Term d n) -- type
     Error
@@ -97,16 +97,16 @@ data Error
     (Maybe Universe)
     Error
 | WhileInferring
-    (TyContext d n) Qty
+    (TyContext d n) SQty
     (Elim d n)
     Error
 | WhileComparingT
-    (EqContext n) EqMode
+    (EqContext n) EqMode SQty
     (Term 0 n) -- type
     (Term 0 n) (Term 0 n) -- lhs/rhs
     Error
 | WhileComparingE
-    (EqContext n) EqMode
+    (EqContext n) EqMode SQty
     (Elim 0 n) (Elim 0 n)
     Error
 %name Error err
@@ -119,31 +119,31 @@ ErrorEff = Except Error
 
 export
 Located Error where
-  (ExpectedTYPE    loc _ _).loc       = loc
-  (ExpectedPi      loc _ _).loc       = loc
-  (ExpectedSig     loc _ _).loc       = loc
-  (ExpectedEnum    loc _ _).loc       = loc
-  (ExpectedEq      loc _ _).loc       = loc
-  (ExpectedNat     loc _ _).loc       = loc
-  (ExpectedBOX     loc _ _).loc       = loc
-  (BadUniverse     loc _ _).loc       = loc
-  (TagNotIn        loc _ _).loc       = loc
-  (BadCaseEnum     loc _ _).loc       = loc
-  (BadQtys         loc _ _ _).loc     = loc
-  (ClashT          loc _ _ _ _ _).loc = loc
-  (ClashTy         loc _ _ _ _).loc   = loc
-  (ClashE          loc _ _ _ _).loc   = loc
-  (ClashU          loc _ _ _).loc     = loc
-  (ClashQ          loc _ _).loc       = loc
-  (NotInScope      loc _).loc         = loc
-  (NotType         loc _ _).loc       = loc
-  (WrongType       loc _ _ _).loc     = loc
-  (MissingEnumArm  loc _ _).loc       = loc
-  (WhileChecking   _ _ _ _ err).loc   = err.loc
-  (WhileCheckingTy _ _ _ err).loc     = err.loc
-  (WhileInferring  _ _ _ err).loc     = err.loc
-  (WhileComparingT _ _ _ _ _ err).loc = err.loc
-  (WhileComparingE _ _ _ _ err).loc   = err.loc
+  (ExpectedTYPE    loc _ _).loc         = loc
+  (ExpectedPi      loc _ _).loc         = loc
+  (ExpectedSig     loc _ _).loc         = loc
+  (ExpectedEnum    loc _ _).loc         = loc
+  (ExpectedEq      loc _ _).loc         = loc
+  (ExpectedNat     loc _ _).loc         = loc
+  (ExpectedBOX     loc _ _).loc         = loc
+  (BadUniverse     loc _ _).loc         = loc
+  (TagNotIn        loc _ _).loc         = loc
+  (BadCaseEnum     loc _ _).loc         = loc
+  (BadQtys         loc _ _ _).loc       = loc
+  (ClashT          loc _ _ _ _ _).loc   = loc
+  (ClashTy         loc _ _ _ _).loc     = loc
+  (ClashE          loc _ _ _ _).loc     = loc
+  (ClashU          loc _ _ _).loc       = loc
+  (ClashQ          loc _ _).loc         = loc
+  (NotInScope      loc _).loc           = loc
+  (NotType         loc _ _).loc         = loc
+  (WrongType       loc _ _ _).loc       = loc
+  (MissingEnumArm  loc _ _).loc         = loc
+  (WhileChecking   _ _ _ _ err).loc     = err.loc
+  (WhileCheckingTy _ _ _ err).loc       = err.loc
+  (WhileInferring  _ _ _ err).loc       = err.loc
+  (WhileComparingT _ _ _ _ _ _ err).loc = err.loc
+  (WhileComparingE _ _ _ _ _ err).loc   = err.loc
 
 
 ||| separates out all the error context layers
@@ -156,10 +156,10 @@ 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 (WhileComparingT ctx x sg s t r err) =
+  mapFst (WhileComparingT ctx x sg s t r ::) $ explodeContext err
+explodeContext (WhileComparingE ctx x sg e f err) =
+  mapFst (WhileComparingE ctx x sg e f ::) $ explodeContext err
 explodeContext err = ([], err)
 
 ||| leaves the outermost context layer, and the innermost (up to) n, and removes
@@ -342,12 +342,12 @@ prettyErrorNoLoc showContext = \case
     sep [hsep ["the tag", !(prettyTag tag), "is not contained in"],
          !(prettyTerm [<] [<] $ Enum (fromList tags) noLoc)]
 
-  WhileChecking ctx pi s a err =>
+  WhileChecking ctx sg 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)])
+           hangDSingle "with quantity"  !(prettyQty sg.qty)])
         (prettyErrorNoLoc showContext err)|]
 
   WhileCheckingTy ctx a k err =>
@@ -357,29 +357,31 @@ prettyErrorNoLoc showContext = \case
            pure $ text $ isTypeInUniverse k])
         (prettyErrorNoLoc showContext err)|]
 
-  WhileInferring ctx pi e err =>
+  WhileInferring ctx sg e err =>
     [|vappendBlank
         (inTContext ctx . sep =<< sequence
           [hangDSingle "while inferring the type of"
               !(prettyElim ctx.dnames ctx.tnames e),
-           hangDSingle "with quantity"  !(prettyQty pi)])
+           hangDSingle "with quantity" !(prettyQty sg.qty)])
         (prettyErrorNoLoc showContext err)|]
 
-  WhileComparingT ctx mode a s t err =>
+  WhileComparingT ctx mode sg 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)])
+           hangDSingle "at type" !(prettyTerm [<] ctx.tnames a),
+           hangDSingle "with quantity" !(prettyQty sg.qty)])
         (prettyErrorNoLoc showContext err)|]
 
-  WhileComparingE ctx mode e f err =>
+  WhileComparingE ctx mode sg 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)])
+              !(prettyElim [<] ctx.tnames f),
+           hangDSingle "with quantity" !(prettyQty sg.qty)])
         (prettyErrorNoLoc showContext err)|]
 
 where
diff --git a/lib/Quox/Whnf/Coercion.idr b/lib/Quox/Whnf/Coercion.idr
index de00b91..a46d3e8 100644
--- a/lib/Quox/Whnf/Coercion.idr
+++ b/lib/Quox/Whnf/Coercion.idr
@@ -23,12 +23,12 @@ where
 
 parameters {auto _ : CanWhnf Term Interface.isRedexT}
            {auto _ : CanWhnf Elim Interface.isRedexE}
-           {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
+           {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n) (pi : SQty)
   ||| reduce a function application `App (Coe ty p q val) s loc`
   export covering
   piCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) ->
           (val, s : Term d n) -> Loc ->
-          Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
+          Eff Whnf (Subset (Elim d n) (No . isRedexE defs pi))
   piCoe sty@(S [< i] ty) p q val s loc = do
     -- (coe [i ⇒ π.(x : A) → B] @p @q t) s ⇝
     -- coe [i ⇒ B[𝒔‹i›/x] @p @q ((t ∷ (π.(x : A) → B)‹p/i›) 𝒔‹p›)
@@ -36,20 +36,20 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
     --
     -- type-case is used to expose A,B if the type is neutral
     let ctx1 = extendDim i ctx
-    Element ty tynf <- whnf defs ctx1 $ getTerm ty
+    Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
     (arg, res) <- tycasePi defs ctx1 ty
     let s0   = CoeT i arg q p s s.loc
         body = E $ App (Ann val (ty // one p) val.loc) (E s0) loc
         s1   = CoeT i (arg // (BV 0 i.loc ::: shift 2)) (weakD 1 q) (BV 0 i.loc)
                     (s // shift 1) s.loc
-    whnf defs ctx $ CoeT i (sub1 res s1) p q body loc
+    whnf defs ctx pi $ CoeT i (sub1 res s1) p q body loc
 
   ||| reduce a pair elimination `CasePair pi (Coe ty p q val) ret body loc`
   export covering
   sigCoe : (qty : Qty) ->
            (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
            (ret : ScopeTerm d n) -> (body : ScopeTermN 2 d n) -> Loc ->
-           Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
+           Eff Whnf (Subset (Elim d n) (No . isRedexE defs pi))
   sigCoe qty sty@(S [< i] ty) p q val ret body loc = do
     -- caseπ (coe [i ⇒ (x : A) × B] @p @q s) return z ⇒ C of { (a, b) ⇒ e }
     -- ⇝
@@ -60,7 +60,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
     --
     -- type-case is used to expose A,B if the type is neutral
     let ctx1 = extendDim i ctx
-    Element ty tynf <- whnf defs ctx1 $ getTerm ty
+    Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
     (tfst, tsnd) <- tycaseSig defs ctx1 ty
     let [< x, y] = body.names
         a' = CoeT i (weakT 2 tfst) p q (BVT 1 noLoc) x.loc
@@ -68,41 +68,41 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
           (CoeT i (weakT 2 $ tfst // (B VZ noLoc ::: shift 2))
             (weakD 1 p) (B VZ noLoc) (BVT 1 noLoc) y.loc ::: shift 2)
         b' = CoeT i tsnd' p q (BVT 0 noLoc) y.loc
-    whnf defs ctx $ CasePair qty (Ann val (ty // one p) val.loc) ret
+    whnf defs ctx pi $ CasePair qty (Ann val (ty // one p) val.loc) ret
       (ST body.names $ body.term // (a' ::: b' ::: shift 2)) loc
 
   ||| reduce a dimension application `DApp (Coe ty p q val) r loc`
   export covering
   eqCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
           (r : Dim d) -> Loc ->
-          Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
+          Eff Whnf (Subset (Elim d n) (No . isRedexE defs pi))
   eqCoe sty@(S [< j] ty) p q val r loc = do
     -- (coe [j ⇒ Eq [i ⇒ A] L R] @p @q eq) @r
     -- ⇝
     -- comp [j ⇒ A‹r/i›] @p @q (eq ∷ (Eq [i ⇒ A] L R)‹p/j›)
     --   @r { 0 j ⇒ L; 1 j ⇒ R }
     let ctx1 = extendDim j ctx
-    Element ty tynf <- whnf defs ctx1 $ getTerm ty
+    Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
     (a0, a1, a, s, t) <- tycaseEq defs ctx1 ty
     let a'   = dsub1 a (weakD 1 r)
         val' = E $ DApp (Ann val (ty // one p) val.loc) r loc
-    whnf defs ctx $ CompH j a' p q val' r j s j t loc
+    whnf defs ctx pi $ CompH j a' p q val' r j s j t loc
 
   ||| reduce a pair elimination `CaseBox pi (Coe ty p q val) ret body`
   export covering
   boxCoe : (qty : Qty) ->
            (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
            (ret : ScopeTerm d n) -> (body : ScopeTerm d n) -> Loc ->
-           Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
+           Eff Whnf (Subset (Elim d n) (No . isRedexE defs pi))
   boxCoe qty sty@(S [< i] ty) p q val ret body loc = do
     -- caseπ (coe [i ⇒ [ρ. A]] @p @q s) return z ⇒ C of { [a] ⇒ e }
     -- ⇝
     -- caseπ s ∷ [ρ. A]‹p/i› return z ⇒ C of { [a] ⇒ e[(coe [i ⇒ A] p q a)/a] }
     let ctx1 = extendDim i ctx
-    Element ty tynf <- whnf defs ctx1 $ getTerm ty
+    Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
     ta <- tycaseBOX defs ctx1 ty
     let a' = CoeT i (weakT 1 ta) p q (BVT 0 noLoc) body.name.loc
-    whnf defs ctx $ CaseBox qty (Ann val (ty // one p) val.loc) ret
+    whnf defs ctx pi $ CaseBox qty (Ann val (ty // one p) val.loc) ret
       (ST body.names $ body.term // (a' ::: shift 1)) loc
 
 
@@ -110,13 +110,13 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
   export covering
   pushCoe : BindName ->
             (ty : Term (S d) n) -> (p, q : Dim d) -> (s : Term d n) -> Loc ->
-            (0 pc : So (canPushCoe ty s)) =>
-            Eff Whnf (NonRedex Elim d n defs)
+            (0 pc : So (canPushCoe pi ty s)) =>
+            Eff Whnf (NonRedex Elim d n defs pi)
   pushCoe i ty p q s loc =
     case ty of
       -- (coe ★ᵢ @_ @_ s) ⇝ (s ∷ ★ᵢ)
       TYPE l tyLoc =>
-        whnf defs ctx $ Ann s (TYPE l tyLoc) loc
+        whnf defs ctx pi $ Ann s (TYPE l tyLoc) loc
 
       -- η expand it so that whnf for App can deal with it
       --
@@ -125,7 +125,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
       -- (λ y ⇒ (coe (𝑖 ⇒ π.(x : A) → B) @p @q s) y) ∷ (π.(x : A) → B)‹q/𝑖›
       Pi {} =>
         let inner = Coe (SY [< i] ty) p q s loc in
-        whnf defs ctx $
+        whnf defs ctx pi $
           Ann (LamY !(mnb "y" loc)
                   (E $ App (weakE 1 inner) (BVT 0 loc) loc) loc)
               (ty // one q) loc
@@ -147,12 +147,12 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
                    (tfst // (BV 0 loc ::: shift 2))
                    (weakD 1 p) (BV 0 loc) (dweakT 1 s) fst.loc
             snd' = CoeT i (sub1 tsnd fstInSnd) p q snd snd.loc
-        whnf defs ctx $
+        whnf defs ctx pi $
           Ann (Pair (E fst') (E snd') sLoc) (ty // one q) loc
 
       -- (coe {𝐚̄} @_ @_ s) ⇝ (s ∷ {𝐚̄})
       Enum cases tyLoc =>
-        whnf defs ctx $ Ann s (Enum cases tyLoc) loc
+        whnf defs ctx pi $ Ann s (Enum cases tyLoc) loc
 
       -- η expand, same as for Π
       --
@@ -161,14 +161,14 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
       -- (δ 𝑘 ⇒ (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @q s) @𝑘) ∷ (Eq (𝑗 ⇒ A) l r)‹q/𝑖›
       Eq {} =>
         let inner = Coe (SY [< i] ty) p q s loc in
-        whnf defs ctx $
+        whnf defs ctx pi $
           Ann (DLamY !(mnb "k" loc)
                   (E $ DApp (dweakE 1 inner) (BV 0 loc) loc) loc)
               (ty // one q) loc
 
       -- (coe ℕ @_ @_ s) ⇝ (s ∷ ℕ)
       Nat tyLoc =>
-        whnf defs ctx $ Ann s (Nat tyLoc) loc
+        whnf defs ctx pi $ Ann s (Nat tyLoc) loc
 
       -- η expand
       --
@@ -185,4 +185,4 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
               loc
             }
         in
-        whnf defs ctx $ Ann (Box (E inner) loc) (ty // one q) loc
+        whnf defs ctx pi $ Ann (Box (E inner) loc) (ty // one q) loc
diff --git a/lib/Quox/Whnf/ComputeElimType.idr b/lib/Quox/Whnf/ComputeElimType.idr
index 7a5d09d..9e73fd1 100644
--- a/lib/Quox/Whnf/ComputeElimType.idr
+++ b/lib/Quox/Whnf/ComputeElimType.idr
@@ -14,8 +14,8 @@ export covering
 computeElimType : CanWhnf Term Interface.isRedexT =>
                   CanWhnf Elim Interface.isRedexE =>
                   {d, n : Nat} ->
-                  (defs : Definitions) -> WhnfContext d n ->
-                  (e : Elim d n) -> (0 ne : No (isRedexE defs e)) =>
+                  (defs : Definitions) -> WhnfContext d n -> (pi : SQty) ->
+                  (e : Elim d n) -> (0 ne : No (isRedexE defs pi e)) =>
                   Eff Whnf (Term d n)
 
 
@@ -24,11 +24,11 @@ export covering
 computeWhnfElimType0 : CanWhnf Term Interface.isRedexT =>
                        CanWhnf Elim Interface.isRedexE =>
                        {d, n : Nat} ->
-                       (defs : Definitions) -> WhnfContext d n ->
-                       (e : Elim d n) -> (0 ne : No (isRedexE defs e)) =>
+                       (defs : Definitions) -> WhnfContext d n -> (pi : SQty) ->
+                       (e : Elim d n) -> (0 ne : No (isRedexE defs pi e)) =>
                        Eff Whnf (Term d n)
 
-computeElimType defs ctx e {ne} =
+computeElimType defs ctx pi e {ne} =
   case e of
     F x u loc => do
       let Just def = lookup x defs
@@ -39,7 +39,7 @@ computeElimType defs ctx e {ne} =
       pure $ ctx.tctx !! i
 
     App f s loc =>
-      case !(computeWhnfElimType0 defs ctx f {ne = noOr1 ne}) of
+      case !(computeWhnfElimType0 defs ctx pi f {ne = noOr1 ne}) of
         Pi {arg, res, _} => pure $ sub1 res $ Ann s arg loc
         t                => throw $ ExpectedPi loc ctx.names t
 
@@ -56,7 +56,7 @@ computeElimType defs ctx e {ne} =
       pure $ sub1 ret box
 
     DApp {fun = f, arg = p, loc} =>
-      case !(computeWhnfElimType0 defs ctx f {ne = noOr1 ne}) of
+      case !(computeWhnfElimType0 defs ctx pi f {ne = noOr1 ne}) of
         Eq {ty, _} => pure $ dsub1 ty p
         t          => throw $ ExpectedEq loc ctx.names t
 
@@ -72,5 +72,5 @@ computeElimType defs ctx e {ne} =
     TypeCase {ret, _} =>
       pure ret
 
-computeWhnfElimType0 defs ctx e =
-  computeElimType defs ctx e >>= whnf0 defs ctx
+computeWhnfElimType0 defs ctx pi e =
+  computeElimType defs ctx pi e >>= whnf0 defs ctx pi
diff --git a/lib/Quox/Whnf/Interface.idr b/lib/Quox/Whnf/Interface.idr
index 596a812..68bb919 100644
--- a/lib/Quox/Whnf/Interface.idr
+++ b/lib/Quox/Whnf/Interface.idr
@@ -18,14 +18,14 @@ Whnf = [NameGen, Except Error]
 
 public export
 0 RedexTest : TermLike -> Type
-RedexTest tm = {d, n : Nat} -> Definitions -> tm d n -> Bool
+RedexTest tm = {d, n : Nat} -> Definitions -> SQty -> tm d n -> Bool
 
 public export
 interface CanWhnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm
 where
   whnf : {d, n : Nat} -> (defs : Definitions) ->
-         (ctx : WhnfContext d n) ->
-         tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs))
+         (ctx : WhnfContext d n) -> (q : SQty) ->
+         tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs q))
   -- having isRedex be part of the class header, and needing to be explicitly
   -- quantified on every use since idris can't infer its type, is a little ugly.
   -- but none of the alternatives i've thought of so far work. e.g. in some
@@ -33,23 +33,24 @@ where
 
 public export %inline
 whnf0 : {d, n : Nat} -> {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
-        (defs : Definitions) -> WhnfContext d n -> tm d n -> Eff Whnf (tm d n)
-whnf0 defs ctx t = fst <$> whnf defs ctx t
+        Definitions -> WhnfContext d n -> SQty -> tm d n -> Eff Whnf (tm d n)
+whnf0 defs ctx q t = fst <$> whnf defs ctx q t
 
 public export
 0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
-                      Definitions -> Pred (tm d n)
-IsRedex  defs = So . isRedex defs
-NotRedex defs = No . isRedex defs
+                      Definitions -> SQty -> Pred (tm d n)
+IsRedex  defs q = So . isRedex defs q
+NotRedex defs q = No . isRedex defs q
 
 public export
 0 NonRedex : (tm : TermLike) -> {isRedex : RedexTest tm} ->
-             CanWhnf tm isRedex => (d, n : Nat) -> (defs : Definitions) -> Type
-NonRedex tm d n defs = Subset (tm d n) (NotRedex defs)
+             CanWhnf tm isRedex => (d, n : Nat) ->
+             (defs : Definitions) -> SQty -> Type
+NonRedex tm d n defs q = Subset (tm d n) (NotRedex defs q)
 
 public export %inline
 nred : {0 isRedex : RedexTest tm} -> (0 _ : CanWhnf tm isRedex) =>
-       (t : tm d n) -> (0 nr : NotRedex defs t) => NonRedex tm d n defs
+       (t : tm d n) -> (0 nr : NotRedex defs q t) => NonRedex tm d n defs q
 nred t = Element t nr
 
 
@@ -153,25 +154,25 @@ isK _      = False
 ||| - `ty` has η
 ||| - `val` is a constructor form
 public export %inline
-canPushCoe : (ty, val : Term {}) -> Bool
-canPushCoe (TYPE  {}) _         = True
-canPushCoe (Pi    {}) _         = True
-canPushCoe (Lam   {}) _         = False
-canPushCoe (Sig   {}) (Pair {}) = True
-canPushCoe (Sig   {}) _         = False
-canPushCoe (Pair  {}) _         = False
-canPushCoe (Enum  {}) _         = True
-canPushCoe (Tag   {}) _         = False
-canPushCoe (Eq    {}) _         = True
-canPushCoe (DLam  {}) _         = False
-canPushCoe (Nat   {}) _         = True
-canPushCoe (Zero  {}) _         = False
-canPushCoe (Succ  {}) _         = False
-canPushCoe (BOX   {}) _         = True
-canPushCoe (Box   {}) _         = False
-canPushCoe (E     {}) _         = False
-canPushCoe (CloT  {}) _         = False
-canPushCoe (DCloT {}) _         = False
+canPushCoe : SQty -> (ty, val : Term {}) -> Bool
+canPushCoe pi (TYPE  {}) _         = True
+canPushCoe pi (Pi    {}) _         = True
+canPushCoe pi (Lam   {}) _         = False
+canPushCoe pi (Sig   {}) (Pair {}) = True
+canPushCoe pi (Sig   {}) _         = False
+canPushCoe pi (Pair  {}) _         = False
+canPushCoe pi (Enum  {}) _         = True
+canPushCoe pi (Tag   {}) _         = False
+canPushCoe pi (Eq    {}) _         = True
+canPushCoe pi (DLam  {}) _         = False
+canPushCoe pi (Nat   {}) _         = True
+canPushCoe pi (Zero  {}) _         = False
+canPushCoe pi (Succ  {}) _         = False
+canPushCoe pi (BOX   {}) _         = True
+canPushCoe pi (Box   {}) _         = False
+canPushCoe pi (E     {}) _         = False
+canPushCoe pi (CloT  {}) _         = False
+canPushCoe pi (DCloT {}) _         = False
 
 
 mutual
@@ -183,42 +184,42 @@ mutual
   |||    an application whose head is an annotated lambda,
   |||    a case expression whose head is an annotated constructor form, etc
   ||| 4. a redundant annotation, or one whose term or type is reducible
-  ||| 5. a coercion `coe (𝑖 ⇒ A) @p @q s` where:
+  ||| 5. a coercion `coe (𝑖 ⇒ A) @p @pi s` where:
   |||      a. `A` is reducible or a type constructor, or
   |||      b. `𝑖` is not mentioned in `A`
   |||         ([fixme] should be A‹0/𝑖› = A‹1/𝑖›), or
-  |||      c. `p = q`
-  ||| 6. a composition `comp A @p @q s @r {⋯}`
-  |||    where `p = q`, `r = 0`, or `r = 1`
+  |||      c. `p = pi`
+  ||| 6. a composition `comp A @p @pi s @r {⋯}`
+  |||    where `p = pi`, `r = 0`, or `r = 1`
   ||| 7. a closure
   public export
   isRedexE : RedexTest Elim
-  isRedexE defs (F {x, u, _}) {d, n} =
+  isRedexE defs pi (F {x, u, _}) {d, n} =
     isJust $ lookupElim x u defs {d, n}
-  isRedexE _ (B {}) = False
-  isRedexE defs (App {fun, _}) =
-    isRedexE defs fun || isLamHead fun
-  isRedexE defs (CasePair {pair, _}) =
-    isRedexE defs pair || isPairHead pair
-  isRedexE defs (CaseEnum {tag, _}) =
-    isRedexE defs tag || isTagHead tag
-  isRedexE defs (CaseNat {nat, _}) =
-    isRedexE defs nat || isNatHead nat
-  isRedexE defs (CaseBox {box, _}) =
-    isRedexE defs box || isBoxHead box
-  isRedexE defs (DApp {fun, arg, _}) =
-    isRedexE defs fun || isDLamHead fun || isK arg
-  isRedexE defs (Ann {tm, ty, _}) =
-    isE tm || isRedexT defs tm || isRedexT defs ty
-  isRedexE defs (Coe {ty = S _ (N _), _}) = True
-  isRedexE defs (Coe {ty = S _ (Y ty), p, q, val, _}) =
-    isRedexT defs ty || canPushCoe ty val || isYes (p `decEqv` q)
-  isRedexE defs (Comp {ty, p, q, r, _}) =
+  isRedexE _ pi (B {}) = False
+  isRedexE defs pi (App {fun, _}) =
+    isRedexE defs pi fun || isLamHead fun
+  isRedexE defs pi (CasePair {pair, _}) =
+    isRedexE defs pi pair || isPairHead pair
+  isRedexE defs pi (CaseEnum {tag, _}) =
+    isRedexE defs pi tag || isTagHead tag
+  isRedexE defs pi (CaseNat {nat, _}) =
+    isRedexE defs pi nat || isNatHead nat
+  isRedexE defs pi (CaseBox {box, _}) =
+    isRedexE defs pi box || isBoxHead box
+  isRedexE defs pi (DApp {fun, arg, _}) =
+    isRedexE defs pi fun || isDLamHead fun || isK arg
+  isRedexE defs pi (Ann {tm, ty, _}) =
+    isE tm || isRedexT defs pi tm || isRedexT defs SZero ty
+  isRedexE defs pi (Coe {ty = S _ (N _), _}) = True
+  isRedexE defs pi (Coe {ty = S _ (Y ty), p, q, val, _}) =
+    isRedexT defs SZero ty || canPushCoe pi ty val || isYes (p `decEqv` q)
+  isRedexE defs pi (Comp {ty, p, q, r, _}) =
     isYes (p `decEqv` q) || isK r
-  isRedexE defs (TypeCase {ty, ret, _}) =
-    isRedexE defs ty || isRedexT defs ret || isAnnTyCon ty
-  isRedexE _ (CloE  {}) = True
-  isRedexE _ (DCloE {}) = True
+  isRedexE defs pi (TypeCase {ty, ret, _}) =
+    isRedexE defs pi ty || isRedexT defs pi ret || isAnnTyCon ty
+  isRedexE _ _ (CloE  {}) = True
+  isRedexE _ _ (DCloE {}) = True
 
   ||| a reducible term
   |||
@@ -228,7 +229,7 @@ mutual
   ||| 3. a closure
   public export
   isRedexT : RedexTest Term
-  isRedexT _    (CloT  {}) = True
-  isRedexT _    (DCloT {}) = True
-  isRedexT defs (E {e, _}) = isAnn e || isRedexE defs e
-  isRedexT _    _          = False
+  isRedexT _    _  (CloT  {}) = True
+  isRedexT _    _  (DCloT {}) = True
+  isRedexT defs pi (E {e, _}) = isAnn e || isRedexE defs pi e
+  isRedexT _    _  _          = False
diff --git a/lib/Quox/Whnf/Main.idr b/lib/Quox/Whnf/Main.idr
index c4a7a76..93f8515 100644
--- a/lib/Quox/Whnf/Main.idr
+++ b/lib/Quox/Whnf/Main.idr
@@ -16,53 +16,53 @@ export covering CanWhnf Elim Interface.isRedexE
 
 covering
 CanWhnf Elim Interface.isRedexE where
-  whnf defs ctx (F x u loc) with (lookupElim x u defs) proof eq
-    _ | Just y  = whnf defs ctx $ setLoc loc y
+  whnf defs ctx rh (F x u loc) with (lookupElim x u defs) proof eq
+    _ | Just y  = whnf defs ctx rh $ setLoc loc y
     _ | Nothing = pure $ Element (F x u loc) $ rewrite eq in Ah
 
-  whnf _ _ (B i loc) = pure $ nred $ B i loc
+  whnf _ _ _ (B i loc) = pure $ nred $ B i loc
 
   -- ((λ x ⇒ t) ∷ (π.x : A) → B) s ⇝ t[s∷A/x] ∷ B[s∷A/x]
-  whnf defs ctx (App f s appLoc) = do
-    Element f fnf <- whnf defs ctx f
+  whnf defs ctx rh (App f s appLoc) = do
+    Element f fnf <- whnf defs ctx rh f
     case nchoose $ isLamHead f of
       Left _ => case f of
         Ann (Lam {body, _}) (Pi {arg, res, _}) floc =>
           let s = Ann s arg s.loc in
-          whnf defs ctx $ Ann (sub1 body s) (sub1 res s) appLoc
-        Coe ty p q val _ => piCoe defs ctx ty p q val s appLoc
+          whnf defs ctx rh $ Ann (sub1 body s) (sub1 res s) appLoc
+        Coe ty p q val _ => piCoe defs ctx rh ty p q val s appLoc
       Right nlh => pure $ Element (App f s appLoc) $ fnf `orNo` nlh
 
   -- case (s, t) ∷ (x : A) × B return p ⇒ C of { (a, b) ⇒ u } ⇝
   -- u[s∷A/a, t∷B[s∷A/x]] ∷ C[(s, t)∷((x : A) × B)/p]
-  whnf defs ctx (CasePair pi pair ret body caseLoc) = do
-    Element pair pairnf <- whnf defs ctx pair
+  whnf defs ctx rh (CasePair pi pair ret body caseLoc) = do
+    Element pair pairnf <- whnf defs ctx rh pair
     case nchoose $ isPairHead pair of
       Left _ => case pair of
         Ann (Pair {fst, snd, _}) (Sig {fst = tfst, snd = tsnd, _}) pairLoc =>
           let fst = Ann fst tfst fst.loc
               snd = Ann snd (sub1 tsnd fst) snd.loc
           in
-          whnf defs ctx $ Ann (subN body [< fst, snd]) (sub1 ret pair) caseLoc
+          whnf defs ctx rh $ Ann (subN body [< fst, snd]) (sub1 ret pair) caseLoc
         Coe ty p q val _ => do
-          sigCoe defs ctx pi ty p q val ret body caseLoc
+          sigCoe defs ctx rh pi ty p q val ret body caseLoc
       Right np =>
         pure $ Element (CasePair pi pair ret body caseLoc) $ pairnf `orNo` np
 
   -- case 'a ∷ {a,…} return p ⇒ C of { 'a ⇒ u } ⇝
   -- u ∷ C['a∷{a,…}/p]
-  whnf defs ctx (CaseEnum pi tag ret arms caseLoc) = do
-    Element tag tagnf <- whnf defs ctx tag
+  whnf defs ctx rh (CaseEnum pi tag ret arms caseLoc) = do
+    Element tag tagnf <- whnf defs ctx rh tag
     case nchoose $ isTagHead tag of
       Left _ => case tag of
         Ann (Tag t _) (Enum ts _) _ =>
           let ty = sub1 ret tag in
           case lookup t arms of
-            Just arm => whnf defs ctx $ Ann arm ty arm.loc
+            Just arm => whnf defs ctx rh $ Ann arm ty arm.loc
             Nothing  => throw $ MissingEnumArm caseLoc t (keys arms)
         Coe ty p q val _ =>
           -- there is nowhere an equality can be hiding inside an enum type
-          whnf defs ctx $
+          whnf defs ctx rh $
             CaseEnum pi (Ann val (dsub1 ty q) val.loc) ret arms caseLoc
       Right nt =>
         pure $ Element (CaseEnum pi tag ret arms caseLoc) $ tagnf `orNo` nt
@@ -72,37 +72,37 @@ CanWhnf Elim Interface.isRedexE where
   --
   -- case succ n ∷ ℕ return p ⇒ C of { succ n', π.ih ⇒ u; … } ⇝
   --   u[n∷ℕ/n', (case n ∷ ℕ ⋯)/ih] ∷ C[succ n ∷ ℕ/p]
-  whnf defs ctx (CaseNat pi piIH nat ret zer suc caseLoc) = do
-    Element nat natnf <- whnf defs ctx nat
+  whnf defs ctx rh (CaseNat pi piIH nat ret zer suc caseLoc) = do
+    Element nat natnf <- whnf defs ctx rh nat
     case nchoose $ isNatHead nat of
       Left _ =>
         let ty = sub1 ret nat in
         case nat of
           Ann (Zero _) (Nat _) _ =>
-            whnf defs ctx $ Ann zer ty zer.loc
+            whnf defs ctx rh $ Ann zer ty zer.loc
           Ann (Succ n succLoc) (Nat natLoc) _ =>
             let nn = Ann n (Nat natLoc) succLoc
                 tm = subN suc [< nn, CaseNat pi piIH nn ret zer suc caseLoc]
             in
-            whnf defs ctx $ Ann tm ty caseLoc
+            whnf defs ctx rh $ Ann tm ty caseLoc
           Coe ty p q val _ =>
             -- same deal as Enum
-            whnf defs ctx $
+            whnf defs ctx rh $
               CaseNat pi piIH (Ann val (dsub1 ty q) val.loc) ret zer suc caseLoc
       Right nn => pure $
         Element (CaseNat pi piIH nat ret zer suc caseLoc) (natnf `orNo` nn)
 
   -- case [t] ∷ [π.A] return p ⇒ C of { [x] ⇒ u } ⇝
   --   u[t∷A/x] ∷ C[[t] ∷ [π.A]/p]
-  whnf defs ctx (CaseBox pi box ret body caseLoc) = do
-    Element box boxnf <- whnf defs ctx box
+  whnf defs ctx rh (CaseBox pi box ret body caseLoc) = do
+    Element box boxnf <- whnf defs ctx rh box
     case nchoose $ isBoxHead box of
       Left _ => case box of
         Ann (Box val boxLoc) (BOX q bty tyLoc) _ =>
           let ty = sub1 ret box in
-          whnf defs ctx $ Ann (sub1 body (Ann val bty val.loc)) ty caseLoc
+          whnf defs ctx rh $ Ann (sub1 body (Ann val bty val.loc)) ty caseLoc
         Coe ty p q val _ =>
-          boxCoe defs ctx pi ty p q val ret body caseLoc
+          boxCoe defs ctx rh pi ty p q val ret body caseLoc
       Right nb =>
         pure $ Element (CaseBox pi box ret body caseLoc) (boxnf `orNo` nb)
 
@@ -110,35 +110,35 @@ CanWhnf Elim Interface.isRedexE where
   -- e : Eq (𝑗 ⇒ A) t u ⊢ e @1 ⇝ u ∷ A‹1/𝑗›
   --
   -- ((δ 𝑖 ⇒ s) ∷ Eq (𝑗 ⇒ A) t u) @𝑘 ⇝ s‹𝑘/𝑖› ∷ A‹𝑘/𝑗›
-  whnf defs ctx (DApp f p appLoc) = do
-    Element f fnf <- whnf defs ctx f
+  whnf defs ctx rh (DApp f p appLoc) = do
+    Element f fnf <- whnf defs ctx rh f
     case nchoose $ isDLamHead f of
       Left _ => case f of
         Ann (DLam {body, _}) (Eq {ty, l, r, _}) _ =>
-          whnf defs ctx $
+          whnf defs ctx rh $
             Ann (endsOr (setLoc appLoc l) (setLoc appLoc r) (dsub1 body p) p)
                 (dsub1 ty p) appLoc
         Coe ty p' q' val _ =>
-          eqCoe defs ctx ty p' q' val p appLoc
+          eqCoe defs ctx rh ty p' q' val p appLoc
       Right ndlh => case p of
         K e _ => do
-          Eq {l, r, ty, _} <- computeWhnfElimType0 defs ctx f
+          Eq {l, r, ty, _} <- computeWhnfElimType0 defs ctx rh f
             | ty => throw $ ExpectedEq ty.loc ctx.names ty
-          whnf defs ctx $
+          whnf defs ctx rh $
             ends (Ann (setLoc appLoc l) ty.zero appLoc)
                  (Ann (setLoc appLoc r) ty.one  appLoc) e
         B {} => pure $ Element (DApp f p appLoc) (fnf `orNo` ndlh `orNo` Ah)
 
   -- e ∷ A ⇝ e
-  whnf defs ctx (Ann s a annLoc) = do
-    Element s snf <- whnf defs ctx s
+  whnf defs ctx rh (Ann s a annLoc) = do
+    Element s snf <- whnf defs ctx rh s
     case nchoose $ isE s of
       Left  _  => let E e = s in pure $ Element e $ noOr2 snf
       Right ne => do
-        Element a anf <- whnf defs ctx a
+        Element a anf <- whnf defs ctx SZero a
         pure $ Element (Ann s a annLoc) (ne `orNo` snf `orNo` anf)
 
-  whnf defs ctx (Coe sty p q val coeLoc) =
+  whnf defs ctx rh (Coe sty p q val coeLoc) =
     --   𝑖 ∉ fv(A)
     -- -------------------------------
     --   coe (𝑖 ⇒ A) @p @q s ⇝ s ∷ A
@@ -148,63 +148,71 @@ CanWhnf Elim Interface.isRedexE where
       ([< i], Left ty) =>
         case p `decEqv` q of
           -- coe (𝑖 ⇒ A) @p @p s ⇝ (s ∷ A‹p/𝑖›)
-          Yes _   => whnf defs ctx $ Ann val (dsub1 sty p) coeLoc
+          Yes _   => whnf defs ctx rh $ Ann val (dsub1 sty p) coeLoc
           No  npq => do
-            Element ty tynf <- whnf defs (extendDim i ctx) ty
-            case nchoose $ canPushCoe ty val of
-              Left  pc  => pushCoe defs ctx i ty p q val coeLoc
+            Element ty tynf <- whnf defs (extendDim i ctx) SZero ty
+            case nchoose $ canPushCoe rh ty val of
+              Left  pc  => pushCoe defs ctx rh i ty p q val coeLoc
               Right npc => pure $ Element (Coe (SY [< i] ty) p q val coeLoc)
                                           (tynf `orNo` npc `orNo` notYesNo npq)
       (_, Right ty) =>
-        whnf defs ctx $ Ann val ty coeLoc
+        whnf defs ctx rh $ Ann val ty coeLoc
 
-  whnf defs ctx (Comp ty p q val r zero one compLoc) =
+  whnf defs ctx rh (Comp ty p q val r zero one compLoc) =
     case p `decEqv` q of
       -- comp [A] @p @p s @r { ⋯ } ⇝ s ∷ A
-      Yes y   => whnf defs ctx $ Ann val ty compLoc
+      Yes y   => whnf defs ctx rh $ Ann val ty compLoc
       No  npq => case r of
         -- comp [A] @p @q s @0 { 0 𝑗 ⇒ t₀; ⋯ } ⇝ t₀‹q/𝑗› ∷ A
-        K Zero _ => whnf defs ctx $ Ann (dsub1 zero q) ty compLoc
+        K Zero _ => whnf defs ctx rh $ Ann (dsub1 zero q) ty compLoc
         -- comp [A] @p @q s @1 { 1 𝑗 ⇒ t₁; ⋯ } ⇝ t₁‹q/𝑗› ∷ A
-        K One  _ => whnf defs ctx $ Ann (dsub1 one  q) ty compLoc
+        K One  _ => whnf defs ctx rh $ Ann (dsub1 one  q) ty compLoc
         B {}     => pure $ Element (Comp ty p q val r zero one compLoc)
                                    (notYesNo npq `orNo` Ah)
 
-  whnf defs ctx (TypeCase ty ret arms def tcLoc) = do
-    Element ty  tynf  <- whnf defs ctx ty
-    Element ret retnf <- whnf defs ctx ret
-    case nchoose $ isAnnTyCon ty of
-      Left  y  => let Ann ty (TYPE u _) _ = ty in
-                  reduceTypeCase defs ctx ty u ret arms def tcLoc
-      Right nt => pure $ Element (TypeCase ty ret arms def tcLoc)
-                                 (tynf `orNo` retnf `orNo` nt)
+  whnf defs ctx rh (TypeCase ty ret arms def tcLoc) =
+    case rh `decEq` SZero of
+      Yes Refl => do
+        Element ty  tynf  <- whnf defs ctx SZero ty
+        Element ret retnf <- whnf defs ctx SZero ret
+        case nchoose $ isAnnTyCon ty of
+          Left  y  => let Ann ty (TYPE u _) _ = ty in
+                      reduceTypeCase defs ctx ty u ret arms def tcLoc
+          Right nt => pure $ Element (TypeCase ty ret arms def tcLoc)
+                                     (tynf `orNo` retnf `orNo` nt)
+      No _ =>
+        throw $ ClashQ tcLoc rh.qty Zero
 
-  whnf defs ctx (CloE  (Sub el th)) = whnf defs ctx $ pushSubstsWith' id th el
-  whnf defs ctx (DCloE (Sub el th)) = whnf defs ctx $ pushSubstsWith' th id el
+  whnf defs ctx rh (CloE (Sub el th)) =
+    whnf defs ctx rh $ pushSubstsWith' id th el
+  whnf defs ctx rh (DCloE (Sub el th)) =
+    whnf defs ctx rh $ pushSubstsWith' th id el
 
 covering
 CanWhnf Term Interface.isRedexT where
-  whnf _ _ t@(TYPE {}) = pure $ nred t
-  whnf _ _ t@(Pi   {}) = pure $ nred t
-  whnf _ _ t@(Lam  {}) = pure $ nred t
-  whnf _ _ t@(Sig  {}) = pure $ nred t
-  whnf _ _ t@(Pair {}) = pure $ nred t
-  whnf _ _ t@(Enum {}) = pure $ nred t
-  whnf _ _ t@(Tag  {}) = pure $ nred t
-  whnf _ _ t@(Eq   {}) = pure $ nred t
-  whnf _ _ t@(DLam {}) = pure $ nred t
-  whnf _ _ t@(Nat  {}) = pure $ nred t
-  whnf _ _ t@(Zero {}) = pure $ nred t
-  whnf _ _ t@(Succ {}) = pure $ nred t
-  whnf _ _ t@(BOX  {}) = pure $ nred t
-  whnf _ _ t@(Box  {}) = pure $ nred t
+  whnf _ _ _ t@(TYPE {}) = pure $ nred t
+  whnf _ _ _ t@(Pi   {}) = pure $ nred t
+  whnf _ _ _ t@(Lam  {}) = pure $ nred t
+  whnf _ _ _ t@(Sig  {}) = pure $ nred t
+  whnf _ _ _ t@(Pair {}) = pure $ nred t
+  whnf _ _ _ t@(Enum {}) = pure $ nred t
+  whnf _ _ _ t@(Tag  {}) = pure $ nred t
+  whnf _ _ _ t@(Eq   {}) = pure $ nred t
+  whnf _ _ _ t@(DLam {}) = pure $ nred t
+  whnf _ _ _ t@(Nat  {}) = pure $ nred t
+  whnf _ _ _ t@(Zero {}) = pure $ nred t
+  whnf _ _ _ t@(Succ {}) = pure $ nred t
+  whnf _ _ _ t@(BOX  {}) = pure $ nred t
+  whnf _ _ _ t@(Box  {}) = pure $ nred t
 
   -- s ∷ A ⇝ s   (in term context)
-  whnf defs ctx (E e) = do
-    Element e enf <- whnf defs ctx e
+  whnf defs ctx rh (E e) = do
+    Element e enf <- whnf defs ctx rh e
     case nchoose $ isAnn e of
       Left  _  => let Ann {tm, _} = e in pure $ Element tm $ noOr1 $ noOr2 enf
       Right na => pure $ Element (E e) $ na `orNo` enf
 
-  whnf defs ctx (CloT  (Sub tm th)) = whnf defs ctx $ pushSubstsWith' id th tm
-  whnf defs ctx (DCloT (Sub tm th)) = whnf defs ctx $ pushSubstsWith' th id tm
+  whnf defs ctx rh (CloT (Sub tm th)) =
+    whnf defs ctx rh $ pushSubstsWith' id th tm
+  whnf defs ctx rh (DCloT (Sub tm th)) =
+    whnf defs ctx rh $ pushSubstsWith' th id tm
diff --git a/lib/Quox/Whnf/TypeCase.idr b/lib/Quox/Whnf/TypeCase.idr
index ae38a29..c30cd71 100644
--- a/lib/Quox/Whnf/TypeCase.idr
+++ b/lib/Quox/Whnf/TypeCase.idr
@@ -35,11 +35,11 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
   ||| for an elim returns a pair of type-cases that will reduce to that;
   ||| for other intro forms error
   export covering
-  tycasePi : (t : Term d n) -> (0 tnf : No (isRedexT defs t)) =>
+  tycasePi : (t : Term d n) -> (0 tnf : No (isRedexT defs SZero t)) =>
              Eff Whnf (Term d n, ScopeTerm d n)
   tycasePi (Pi {arg, res, _}) = pure (arg, res)
   tycasePi (E e) {tnf} = do
-    ty <- computeElimType defs ctx e {ne = noOr2 tnf}
+    ty <- computeElimType defs ctx SZero e {ne = noOr2 tnf}
     let loc  = e.loc
         narg = mnb "Arg" loc; nret = mnb "Ret" loc
         arg  = E $ typeCase1Y e ty KPi [< !narg, !nret] (BVT 1 loc) loc
@@ -53,11 +53,11 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
   ||| for an elim returns a pair of type-cases that will reduce to that;
   ||| for other intro forms error
   export covering
-  tycaseSig : (t : Term d n) -> (0 tnf : No (isRedexT defs t)) =>
+  tycaseSig : (t : Term d n) -> (0 tnf : No (isRedexT defs SZero t)) =>
               Eff Whnf (Term d n, ScopeTerm d n)
   tycaseSig (Sig {fst, snd, _}) = pure (fst, snd)
   tycaseSig (E e) {tnf} = do
-    ty <- computeElimType defs ctx e {ne = noOr2 tnf}
+    ty <- computeElimType defs ctx SZero e {ne = noOr2 tnf}
     let loc  = e.loc
         nfst = mnb "Fst" loc; nsnd = mnb "Snd" loc
         fst  = E $ typeCase1Y e ty KSig [< !nfst, !nsnd] (BVT 1 loc) loc
@@ -71,11 +71,11 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
   ||| for an elim returns a type-case that will reduce to that;
   ||| for other intro forms error
   export covering
-  tycaseBOX : (t : Term d n) -> (0 tnf : No (isRedexT defs t)) =>
+  tycaseBOX : (t : Term d n) -> (0 tnf : No (isRedexT defs SZero t)) =>
               Eff Whnf (Term d n)
   tycaseBOX (BOX {ty, _}) = pure ty
   tycaseBOX (E e) {tnf} = do
-    ty <- computeElimType defs ctx e {ne = noOr2 tnf}
+    ty <- computeElimType defs ctx SZero e {ne = noOr2 tnf}
     pure $ E $ typeCase1Y e ty KBOX [< !(mnb "Ty" e.loc)] (BVT 0 e.loc) e.loc
   tycaseBOX t = throw $ ExpectedBOX t.loc ctx.names t
 
@@ -83,11 +83,11 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
   ||| for an elim returns five type-cases that will reduce to that;
   ||| for other intro forms error
   export covering
-  tycaseEq : (t : Term d n) -> (0 tnf : No (isRedexT defs t)) =>
+  tycaseEq : (t : Term d n) -> (0 tnf : No (isRedexT defs SZero t)) =>
              Eff Whnf (Term d n, Term d n, DScopeTerm d n, Term d n, Term d n)
   tycaseEq (Eq {ty, l, r, _}) = pure (ty.zero, ty.one, ty, l, r)
   tycaseEq (E e) {tnf} = do
-    ty <- computeElimType defs ctx e {ne = noOr2 tnf}
+    ty <- computeElimType defs ctx SZero e {ne = noOr2 tnf}
     let loc   = e.loc
         names = traverse' (\x => mnb x loc) [< "A0", "A1", "A", "L", "R"]
         a0    = E $ typeCase1Y e ty KEq !names (BVT 4 loc) loc
@@ -108,11 +108,11 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
   reduceTypeCase : (ty : Term d n) -> (u : Universe) -> (ret : Term d n) ->
                    (arms : TypeCaseArms d n) -> (def : Term d n) ->
                    (0 _ : So (isTyCon ty)) => Loc ->
-                   Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
+                   Eff Whnf (Subset (Elim d n) (No . isRedexE defs SZero))
   reduceTypeCase ty u ret arms def loc = case ty of
     -- (type-case ★ᵢ ∷ _ return Q of { ★ ⇒ s; ⋯ }) ⇝ s ∷ Q
     TYPE {} =>
-      whnf defs ctx $ Ann (tycaseRhsDef0 def KTYPE arms) ret loc
+      whnf defs ctx SZero $ Ann (tycaseRhsDef0 def KTYPE arms) ret loc
 
     -- (type-case π.(x : A) → B ∷ ★ᵢ return Q of { (a → b) ⇒ s; ⋯ }) ⇝
     -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q
@@ -121,7 +121,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
           res' = Ann (Lam res res.loc)
                      (Arr Zero arg (TYPE u noLoc) arg.loc) res.loc
       in
-      whnf defs ctx $
+      whnf defs ctx SZero $
         Ann (subN (tycaseRhsDef def KPi arms) [< arg', res']) ret loc
 
     -- (type-case (x : A) × B ∷ ★ᵢ return Q of { (a × b) ⇒ s; ⋯ }) ⇝
@@ -131,12 +131,12 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
           snd' = Ann (Lam snd snd.loc)
                      (Arr Zero fst (TYPE u noLoc) fst.loc) snd.loc
       in
-      whnf defs ctx $
+      whnf defs ctx SZero $
         Ann (subN (tycaseRhsDef def KSig arms) [< fst', snd']) ret loc
 
     -- (type-case {⋯} ∷ _ return Q of { {} ⇒ s; ⋯ }) ⇝ s ∷ Q
     Enum {} =>
-      whnf defs ctx $ Ann (tycaseRhsDef0 def KEnum arms) ret loc
+      whnf defs ctx SZero $ Ann (tycaseRhsDef0 def KEnum arms) ret loc
 
     -- (type-case Eq [i ⇒ A] L R ∷ ★ᵢ return Q
     --  of { Eq a₀ a₁ a l r ⇒ s; ⋯ }) ⇝
@@ -145,7 +145,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
     --   (L ∷ A‹0/i›)/l, (R ∷ A‹1/i›)/r] ∷ Q
     Eq {ty = a, l, r, loc = eqLoc, _} =>
       let a0 = a.zero; a1 = a.one in
-      whnf defs ctx $ Ann
+      whnf defs ctx SZero $ Ann
         (subN (tycaseRhsDef def KEq arms)
            [< Ann a0 (TYPE u noLoc) a.loc, Ann a1 (TYPE u noLoc) a.loc,
               Ann (DLam a a.loc) (Eq0 (TYPE u noLoc) a0 a1 a.loc) a.loc,
@@ -154,10 +154,10 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
 
     -- (type-case ℕ ∷ _ return Q of { ℕ ⇒ s; ⋯ }) ⇝ s ∷ Q
     Nat {} =>
-      whnf defs ctx $ Ann (tycaseRhsDef0 def KNat arms) ret loc
+      whnf defs ctx SZero $ Ann (tycaseRhsDef0 def KNat arms) ret loc
 
     -- (type-case [π.A] ∷ ★ᵢ return Q of { [a] ⇒ s; ⋯ }) ⇝ s[(A ∷ ★ᵢ)/a] ∷ Q
     BOX {ty = a, loc = boxLoc, _} =>
-      whnf defs ctx $ Ann
+      whnf defs ctx SZero $ Ann
         (sub1 (tycaseRhsDef def KBOX arms) (Ann a (TYPE u noLoc) a.loc))
         ret loc
diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr
index 128131c..19568f4 100644
--- a/tests/Tests/Equal.idr
+++ b/tests/Tests/Equal.idr
@@ -12,15 +12,15 @@ import AstExtra
 
 defGlobals : Definitions
 defGlobals = fromList
-  [("A", ^mkPostulate gzero (^TYPE 0)),
-   ("B", ^mkPostulate gzero (^TYPE 0)),
-   ("a", ^mkPostulate gany (^FT "A" 0)),
-   ("a'", ^mkPostulate gany (^FT "A" 0)),
-   ("b", ^mkPostulate gany (^FT "B" 0)),
-   ("f", ^mkPostulate gany (^Arr One (^FT "A" 0) (^FT "A" 0))),
-   ("id", ^mkDef gany (^Arr One (^FT "A" 0) (^FT "A" 0)) (^LamY "x" (^BVT 0))),
-   ("eq-AB", ^mkPostulate gzero (^Eq0 (^TYPE 0) (^FT "A" 0) (^FT "B" 0))),
-   ("two", ^mkDef gany (^Nat) (^Succ (^Succ (^Zero))))]
+  [("A", ^mkPostulate GZero (^TYPE 0)),
+   ("B", ^mkPostulate GZero (^TYPE 0)),
+   ("a", ^mkPostulate GAny (^FT "A" 0)),
+   ("a'", ^mkPostulate GAny (^FT "A" 0)),
+   ("b", ^mkPostulate GAny (^FT "B" 0)),
+   ("f", ^mkPostulate GAny (^Arr One (^FT "A" 0) (^FT "A" 0))),
+   ("id", ^mkDef GAny (^Arr One (^FT "A" 0) (^FT "A" 0)) (^LamY "x" (^BVT 0))),
+   ("eq-AB", ^mkPostulate GZero (^Eq0 (^TYPE 0) (^FT "A" 0) (^FT "B" 0))),
+   ("two", ^mkDef GAny (^Nat) (^Succ (^Succ (^Zero))))]
 
 parameters (label : String) (act : Eff Equal ())
            {default defGlobals globals : Definitions}
@@ -32,15 +32,17 @@ parameters (label : String) (act : Eff Equal ())
 
 
 parameters (ctx : TyContext d n)
-  subT, equalT : Term d n -> Term d n -> Term d n -> Eff TC ()
-  subT ty s t = lift $ Term.sub noLoc ctx ty s t
-  equalT ty s t = lift $ Term.equal noLoc ctx ty s t
+  subT, equalT : {default SOne sg : SQty} ->
+                 Term d n -> Term d n -> Term d n -> Eff TC ()
+  subT ty s t {sg} = lift $ Term.sub noLoc ctx sg ty s t
+  equalT ty s t {sg} = lift $ Term.equal noLoc ctx sg ty s t
   equalTy : Term d n -> Term d n -> Eff TC ()
   equalTy s t = lift $ Term.equalType noLoc ctx s t
 
-  subE, equalE : Elim d n -> Elim d n -> Eff TC ()
-  subE e f = lift $ Elim.sub noLoc ctx e f
-  equalE e f = lift $ Elim.equal noLoc ctx e f
+  subE, equalE : {default SOne sg : SQty} ->
+                 Elim d n -> Elim d n -> Eff TC ()
+  subE e f {sg} = lift $ Elim.sub noLoc ctx sg e f
+  equalE e f {sg} = lift $ Elim.equal noLoc ctx sg e f
 
 
 export
@@ -154,7 +156,7 @@ tests = "equality & subtyping" :- [
       let tm = ^Eq0 (^TYPE 1) (^TYPE 0) (^TYPE 0) in
       equalT empty (^TYPE 2) tm tm,
     testEq "A ≔ ★₁ ⊢ (★₀ ≡ ★₀ : ★₁) = (★₀ ≡ ★₀ : A)"
-        {globals = fromList [("A", ^mkDef gzero (^TYPE 2) (^TYPE 1))]} $
+        {globals = fromList [("A", ^mkDef GZero (^TYPE 2) (^TYPE 1))]} $
       equalT empty (^TYPE 2)
         (^Eq0 (^TYPE 1) (^TYPE 0) (^TYPE 0))
         (^Eq0 (^FT "A" 0) (^TYPE 0) (^TYPE 0)),
@@ -174,7 +176,7 @@ tests = "equality & subtyping" :- [
 
     testEq "p : (a ≡ a' : A), q : (a ≡ a' : A) ∥ ⊢ p = q  (free)"
            {globals =
-              let def = ^mkPostulate gzero
+              let def = ^mkPostulate GZero
                           (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0))
               in defGlobals `mergeLeft` fromList [("p", def), ("q", def)]} $
       equalE empty (^F "p" 0) (^F "q" 0),
@@ -193,32 +195,32 @@ tests = "equality & subtyping" :- [
 
     testEq "E ≔ a ≡ a' : A, EE ≔ E ∥ x : EE, y : EE ⊢ x = y"
            {globals = defGlobals `mergeLeft` fromList
-              [("E", ^mkDef gzero (^TYPE 0)
+              [("E", ^mkDef GZero (^TYPE 0)
                         (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0))),
-               ("EE", ^mkDef gzero (^TYPE 0) (^FT "E" 0))]} $
+               ("EE", ^mkDef GZero (^TYPE 0) (^FT "E" 0))]} $
       equalE
         (extendTyN [< (Any, "x", ^FT "EE" 0), (Any, "y", ^FT "EE" 0)] empty)
         (^BV 0) (^BV 1),
 
     testEq "E ≔ a ≡ a' : A, EE ≔ E ∥ x : EE, y : E ⊢ x = y"
            {globals = defGlobals `mergeLeft` fromList
-              [("E", ^mkDef gzero (^TYPE 0)
+              [("E", ^mkDef GZero (^TYPE 0)
                         (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0))),
-               ("EE", ^mkDef gzero (^TYPE 0) (^FT "E" 0))]} $
+               ("EE", ^mkDef GZero (^TYPE 0) (^FT "E" 0))]} $
       equalE
         (extendTyN [< (Any, "x", ^FT "EE" 0), (Any, "y", ^FT "E" 0)] empty)
         (^BV 0) (^BV 1),
 
     testEq "E ≔ a ≡ a' : A ∥ x : E, y : E ⊢ x = y"
            {globals = defGlobals `mergeLeft` fromList
-              [("E", ^mkDef gzero (^TYPE 0)
+              [("E", ^mkDef GZero (^TYPE 0)
                         (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0)))]} $
       equalE (extendTyN [< (Any, "x", ^FT "E" 0), (Any, "y", ^FT "E" 0)] empty)
         (^BV 0) (^BV 1),
 
     testEq "E ≔ a ≡ a' : A ∥ x : (E×E), y : (E×E) ⊢ x = y"
            {globals = defGlobals `mergeLeft` fromList
-              [("E", ^mkDef gzero (^TYPE 0)
+              [("E", ^mkDef GZero (^TYPE 0)
                         (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0)))]} $
       let ty : forall n. Term 0 n := ^Sig (^FT "E" 0) (SN $ ^FT "E" 0) in
       equalE (extendTyN [< (Any, "x", ty), (Any, "y", ty)] empty)
@@ -226,9 +228,9 @@ tests = "equality & subtyping" :- [
 
     testEq "E ≔ a ≡ a' : A, W ≔ E × E ∥ x : W, y : E×E ⊢ x = y"
            {globals = defGlobals `mergeLeft` fromList
-              [("E", ^mkDef gzero (^TYPE 0)
+              [("E", ^mkDef GZero (^TYPE 0)
                       (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0))),
-               ("W", ^mkDef gzero (^TYPE 0) (^And (^FT "E" 0) (^FT "E" 0)))]} $
+               ("W", ^mkDef GZero (^TYPE 0) (^And (^FT "E" 0) (^FT "E" 0)))]} $
       equalE
         (extendTyN [< (Any, "x", ^FT "W" 0),
                       (Any, "y", ^And (^FT "E" 0) (^FT "E" 0))] empty)
@@ -278,11 +280,11 @@ tests = "equality & subtyping" :- [
 
   "free var" :-
   let au_bu = fromList
-        [("A", ^mkDef gany (^TYPE 1) (^TYPE 0)),
-         ("B", ^mkDef gany (^TYPE 1) (^TYPE 0))]
+        [("A", ^mkDef GAny (^TYPE 1) (^TYPE 0)),
+         ("B", ^mkDef GAny (^TYPE 1) (^TYPE 0))]
       au_ba = fromList
-        [("A", ^mkDef gany (^TYPE 1) (^TYPE 0)),
-         ("B", ^mkDef gany (^TYPE 1) (^FT "A" 0))]
+        [("A", ^mkDef GAny (^TYPE 1) (^TYPE 0)),
+         ("B", ^mkDef GAny (^TYPE 1) (^FT "A" 0))]
   in [
     testEq "A = A" $
       equalE empty (^F "A" 0) (^F "A" 0),
@@ -303,13 +305,13 @@ tests = "equality & subtyping" :- [
     testNeq "A ≮: B" $
       subE empty (^F "A" 0) (^F "B" 0),
     testEq "A : ★₃ ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: B"
-        {globals = fromList [("A", ^mkDef gany (^TYPE 3) (^TYPE 0)),
-                             ("B", ^mkDef gany (^TYPE 3) (^TYPE 2))]} $
+        {globals = fromList [("A", ^mkDef GAny (^TYPE 3) (^TYPE 0)),
+                             ("B", ^mkDef GAny (^TYPE 3) (^TYPE 2))]} $
       subE empty (^F "A" 0) (^F "B" 0),
     note "(A and B in different universes)",
     testEq "A : ★₁ ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: B"
-        {globals = fromList [("A", ^mkDef gany (^TYPE 1) (^TYPE 0)),
-                             ("B", ^mkDef gany (^TYPE 3) (^TYPE 2))]} $
+        {globals = fromList [("A", ^mkDef GAny (^TYPE 1) (^TYPE 0)),
+                             ("B", ^mkDef GAny (^TYPE 3) (^TYPE 2))]} $
       subE empty (^F "A" 0) (^F "B" 0),
     testEq "0=1 ⊢ A <: B" $
       subE empty01 (^F "A" 0) (^F "B" 0)
diff --git a/tests/Tests/FromPTerm.idr b/tests/Tests/FromPTerm.idr
index 52c4b78..bf8a947 100644
--- a/tests/Tests/FromPTerm.idr
+++ b/tests/Tests/FromPTerm.idr
@@ -85,7 +85,7 @@ tests = "PTerm → Term" :- [
   ],
 
   "terms" :-
-  let defs = fromList [("f", mkDef gany (Nat noLoc) (Zero noLoc) noLoc)]
+  let defs = fromList [("f", mkDef GAny (Nat noLoc) (Zero noLoc) noLoc)]
         -- doesn't have to be well typed yet, just well scoped
       fromPTerm = runFromParser {defs} .
                   fromPTermWith [< "𝑖", "𝑗"] [< "A", "x", "y", "z"]
diff --git a/tests/Tests/Reduce.idr b/tests/Tests/Reduce.idr
index 6848bb8..6da572d 100644
--- a/tests/Tests/Reduce.idr
+++ b/tests/Tests/Reduce.idr
@@ -19,10 +19,11 @@ runWhnf act = runSTErr $ do
 parameters {0 isRedex : RedexTest tm} {auto _ : CanWhnf tm isRedex} {d, n : Nat}
            {auto _ : (Eq (tm d n), Show (tm d n))}
            {default empty defs : Definitions}
+           {default SOne sg : SQty}
   private
   testWhnf : String -> WhnfContext d n -> tm d n -> tm d n -> Test
   testWhnf label ctx from to = test "\{label}  (whnf)" $ do
-    result <- mapFst toInfo $ runWhnf $ whnf0 defs ctx from
+    result <- mapFst toInfo $ runWhnf $ whnf0 defs ctx sg from
     unless (result == to) $ Left [("exp", show to), ("got", show result)]
 
   private
@@ -71,10 +72,10 @@ tests = "whnf" :- [
 
   "definitions" :- [
     testWhnf "a  (transparent)" empty
-      {defs = fromList [("a", ^mkDef gzero (^TYPE 1) (^TYPE 0))]}
+      {defs = fromList [("a", ^mkDef GZero (^TYPE 1) (^TYPE 0))]}
       (^F "a" 0) (^Ann (^TYPE 0) (^TYPE 1)),
     testNoStep "a  (opaque)" empty
-      {defs = fromList [("a", ^mkPostulate gzero (^TYPE 1))]}
+      {defs = fromList [("a", ^mkPostulate GZero (^TYPE 1))]}
       (^F "a" 0)
   ],
 
diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr
index 1365f3e..7e44ecd 100644
--- a/tests/Tests/Typechecker.idr
+++ b/tests/Tests/Typechecker.idr
@@ -87,28 +87,28 @@ apps = foldl (\f, s => ^App f s)
 
 defGlobals : Definitions
 defGlobals = fromList
-  [("A",  ^mkPostulate gzero (^TYPE 0)),
-   ("B",  ^mkPostulate gzero (^TYPE 0)),
-   ("C",  ^mkPostulate gzero (^TYPE 1)),
-   ("D",  ^mkPostulate gzero (^TYPE 1)),
-   ("P",  ^mkPostulate gzero (^Arr Any (^FT "A" 0) (^TYPE 0))),
-   ("a",  ^mkPostulate gany  (^FT "A" 0)),
-   ("a'", ^mkPostulate gany  (^FT "A" 0)),
-   ("b",  ^mkPostulate gany  (^FT "B" 0)),
-   ("c",  ^mkPostulate gany  (^FT "C" 0)),
-   ("d",  ^mkPostulate gany  (^FT "D" 0)),
-   ("f",  ^mkPostulate gany  (^Arr One (^FT "A" 0) (^FT "A" 0))),
-   ("fω", ^mkPostulate gany  (^Arr Any (^FT "A" 0) (^FT "A" 0))),
-   ("g",  ^mkPostulate gany  (^Arr One (^FT "A" 0) (^FT "B" 0))),
-   ("f2", ^mkPostulate gany
+  [("A",  ^mkPostulate GZero (^TYPE 0)),
+   ("B",  ^mkPostulate GZero (^TYPE 0)),
+   ("C",  ^mkPostulate GZero (^TYPE 1)),
+   ("D",  ^mkPostulate GZero (^TYPE 1)),
+   ("P",  ^mkPostulate GZero (^Arr Any (^FT "A" 0) (^TYPE 0))),
+   ("a",  ^mkPostulate GAny  (^FT "A" 0)),
+   ("a'", ^mkPostulate GAny  (^FT "A" 0)),
+   ("b",  ^mkPostulate GAny  (^FT "B" 0)),
+   ("c",  ^mkPostulate GAny  (^FT "C" 0)),
+   ("d",  ^mkPostulate GAny  (^FT "D" 0)),
+   ("f",  ^mkPostulate GAny  (^Arr One (^FT "A" 0) (^FT "A" 0))),
+   ("fω", ^mkPostulate GAny  (^Arr Any (^FT "A" 0) (^FT "A" 0))),
+   ("g",  ^mkPostulate GAny  (^Arr One (^FT "A" 0) (^FT "B" 0))),
+   ("f2", ^mkPostulate GAny
       (^Arr One (^FT "A" 0) (^Arr One (^FT "A" 0) (^FT "B" 0)))),
-   ("p",  ^mkPostulate gany
+   ("p",  ^mkPostulate GAny
       (^PiY One "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))),
-   ("q",  ^mkPostulate gany
+   ("q",  ^mkPostulate GAny
       (^PiY One "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))),
-   ("refl", ^mkDef gany reflTy reflDef),
-   ("fst",  ^mkDef gany fstTy fstDef),
-   ("snd",  ^mkDef gany sndTy sndDef)]
+   ("refl", ^mkDef GAny reflTy reflDef),
+   ("fst",  ^mkDef GAny fstTy fstDef),
+   ("snd",  ^mkDef GAny sndTy sndDef)]
 
 parameters (label : String) (act : Lazy (Eff Test ()))
            {default defGlobals globals : Definitions}
@@ -168,7 +168,7 @@ tests = "typechecker" :- [
     testTC "0 · ★₀ ⇐ ★₁  # by checkType" $
       checkType_ empty (^TYPE 0) (Just 1),
     testTC "0 · ★₀ ⇐ ★₁  # by check" $
-      check_ empty szero (^TYPE 0) (^TYPE 1),
+      check_ empty SZero (^TYPE 0) (^TYPE 1),
     testTC "0 · ★₀ ⇐ ★₂" $
       checkType_ empty (^TYPE 0) (Just 2),
     testTC "0 · ★₀ ⇐ ★_" $
@@ -180,241 +180,241 @@ tests = "typechecker" :- [
     testTC "0=1 ⊢ 0 · ★₁ ⇐ ★₀" $
       checkType_ empty01 (^TYPE 1) (Just 0),
     testTCFail "1 · ★₀ ⇍ ★₁  # by check" $
-      check_ empty sone (^TYPE 0) (^TYPE 1)
+      check_ empty SOne (^TYPE 0) (^TYPE 1)
   ],
 
   "function types" :- [
     note "A, B : ★₀;  C, D : ★₁;  P : 0.A → ★₀",
     testTC "0 · 1.A → B ⇐ ★₀" $
-      check_ empty szero (^Arr One (^FT "A" 0) (^FT "B" 0)) (^TYPE 0),
+      check_ empty SZero (^Arr One (^FT "A" 0) (^FT "B" 0)) (^TYPE 0),
     note "subtyping",
     testTC "0 · 1.A → B ⇐ ★₁" $
-      check_ empty szero (^Arr One (^FT "A" 0) (^FT "B" 0)) (^TYPE 1),
+      check_ empty SZero (^Arr One (^FT "A" 0) (^FT "B" 0)) (^TYPE 1),
     testTC "0 · 1.C → D ⇐ ★₁" $
-      check_ empty szero (^Arr One (^FT "C" 0) (^FT "D" 0)) (^TYPE 1),
+      check_ empty SZero (^Arr One (^FT "C" 0) (^FT "D" 0)) (^TYPE 1),
     testTCFail "0 · 1.C → D ⇍ ★₀" $
-      check_ empty szero (^Arr One (^FT "C" 0) (^FT "D" 0)) (^TYPE 0),
+      check_ empty SZero (^Arr One (^FT "C" 0) (^FT "D" 0)) (^TYPE 0),
     testTC "0 · 1.(x : A) → P x ⇐ ★₀" $
-      check_ empty szero
+      check_ empty SZero
         (^PiY One "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))
         (^TYPE 0),
     testTCFail "0 · 1.A → P ⇍ ★₀" $
-      check_ empty szero (^Arr One (^FT "A" 0) (^FT "P" 0)) (^TYPE 0),
+      check_ empty SZero (^Arr One (^FT "A" 0) (^FT "P" 0)) (^TYPE 0),
     testTC "0=1 ⊢ 0 · 1.A → P ⇐ ★₀" $
-      check_ empty01 szero (^Arr One (^FT "A" 0) (^FT "P" 0)) (^TYPE 0)
+      check_ empty01 SZero (^Arr One (^FT "A" 0) (^FT "P" 0)) (^TYPE 0)
   ],
 
   "pair types" :- [
     testTC "0 · A × A ⇐ ★₀" $
-      check_ empty szero (^And (^FT "A" 0) (^FT "A" 0)) (^TYPE 0),
+      check_ empty SZero (^And (^FT "A" 0) (^FT "A" 0)) (^TYPE 0),
     testTCFail "0 · A × P ⇍ ★₀" $
-      check_ empty szero (^And (^FT "A" 0) (^FT "P" 0)) (^TYPE 0),
+      check_ empty SZero (^And (^FT "A" 0) (^FT "P" 0)) (^TYPE 0),
     testTC "0 · (x : A) × P x ⇐ ★₀" $
-      check_ empty szero
+      check_ empty SZero
         (^SigY "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))
         (^TYPE 0),
     testTC "0 · (x : A) × P x ⇐ ★₁" $
-      check_ empty szero
+      check_ empty SZero
         (^SigY "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))
         (^TYPE 1),
     testTC "0 · (A : ★₀) × A ⇐ ★₁" $
-      check_ empty szero
+      check_ empty SZero
         (^SigY "A" (^TYPE 0) (^BVT 0))
         (^TYPE 1),
     testTCFail "0 · (A : ★₀) × A ⇍ ★₀" $
-      check_ empty szero
+      check_ empty SZero
         (^SigY "A" (^TYPE 0) (^BVT 0))
         (^TYPE 0),
     testTCFail "1 · A × A ⇍ ★₀" $
-      check_ empty sone
+      check_ empty SOne
         (^And (^FT "A" 0) (^FT "A" 0))
         (^TYPE 0)
   ],
 
   "enum types" :- [
-    testTC "0 · {} ⇐ ★₀" $ check_ empty szero (^enum []) (^TYPE 0),
-    testTC "0 · {} ⇐ ★₃" $ check_ empty szero (^enum []) (^TYPE 3),
+    testTC "0 · {} ⇐ ★₀" $ check_ empty SZero (^enum []) (^TYPE 0),
+    testTC "0 · {} ⇐ ★₃" $ check_ empty SZero (^enum []) (^TYPE 3),
     testTC "0 · {a,b,c} ⇐ ★₀" $
-      check_ empty szero (^enum ["a", "b", "c"]) (^TYPE 0),
+      check_ empty SZero (^enum ["a", "b", "c"]) (^TYPE 0),
     testTC "0 · {a,b,c} ⇐ ★₃" $
-      check_ empty szero (^enum ["a", "b", "c"]) (^TYPE 3),
-    testTCFail "1 · {} ⇍ ★₀" $ check_ empty sone (^enum []) (^TYPE 0),
-    testTC "0=1 ⊢ 1 · {} ⇐ ★₀" $ check_ empty01 sone (^enum []) (^TYPE 0)
+      check_ empty SZero (^enum ["a", "b", "c"]) (^TYPE 3),
+    testTCFail "1 · {} ⇍ ★₀" $ check_ empty SOne (^enum []) (^TYPE 0),
+    testTC "0=1 ⊢ 1 · {} ⇐ ★₀" $ check_ empty01 SOne (^enum []) (^TYPE 0)
   ],
 
   "free vars" :- [
     note "A : ★₀",
     testTC "0 · A ⇒ ★₀" $
-      inferAs empty szero (^F "A" 0) (^TYPE 0),
+      inferAs empty SZero (^F "A" 0) (^TYPE 0),
     testTC "0 · [A] ⇐ ★₀" $
-      check_ empty szero (^FT "A" 0) (^TYPE 0),
+      check_ empty SZero (^FT "A" 0) (^TYPE 0),
     note "subtyping",
     testTC "0 · [A] ⇐ ★₁" $
-      check_ empty szero (^FT "A" 0) (^TYPE 1),
+      check_ empty SZero (^FT "A" 0) (^TYPE 1),
     note "(fail) runtime-relevant type",
     testTCFail "1 · A ⇏ ★₀" $
-      infer_ empty sone (^F "A" 0),
+      infer_ empty SOne (^F "A" 0),
     testTC "1 . f ⇒ 1.A → A" $
-      inferAs empty sone (^F "f" 0) (^Arr One (^FT "A" 0) (^FT "A" 0)),
+      inferAs empty SOne (^F "f" 0) (^Arr One (^FT "A" 0) (^FT "A" 0)),
     testTC "1 . f ⇐ 1.A → A" $
-      check_ empty sone (^FT "f" 0) (^Arr One (^FT "A" 0) (^FT "A" 0)),
+      check_ empty SOne (^FT "f" 0) (^Arr One (^FT "A" 0) (^FT "A" 0)),
     testTCFail "1 . f ⇍ 0.A → A" $
-      check_ empty sone (^FT "f" 0) (^Arr Zero (^FT "A" 0) (^FT "A" 0)),
+      check_ empty SOne (^FT "f" 0) (^Arr Zero (^FT "A" 0) (^FT "A" 0)),
     testTCFail "1 . f ⇍ ω.A → A" $
-      check_ empty sone (^FT "f" 0) (^Arr Any (^FT "A" 0) (^FT "A" 0)),
+      check_ empty SOne (^FT "f" 0) (^Arr Any (^FT "A" 0) (^FT "A" 0)),
     testTC "1 . (λ x ⇒ f x) ⇐ 1.A → A" $
-      check_ empty sone
+      check_ empty SOne
         (^LamY "x" (E $ ^App (^F "f" 0) (^BVT 0)))
         (^Arr One (^FT "A" 0) (^FT "A" 0)),
     testTC "1 . (λ x ⇒ f x) ⇐ ω.A → A" $
-      check_ empty sone
+      check_ empty SOne
         (^LamY "x" (E $ ^App (^F "f" 0) (^BVT 0)))
         (^Arr Any (^FT "A" 0) (^FT "A" 0)),
     testTCFail "1 . (λ x ⇒ f x) ⇍ 0.A → A" $
-      check_ empty sone
+      check_ empty SOne
         (^LamY "x" (E $ ^App (^F "f" 0) (^BVT 0)))
         (^Arr Zero (^FT "A" 0) (^FT "A" 0)),
     testTC "1 . fω ⇒ ω.A → A" $
-      inferAs empty sone (^F "fω" 0) (^Arr Any (^FT "A" 0) (^FT "A" 0)),
+      inferAs empty SOne (^F "fω" 0) (^Arr Any (^FT "A" 0) (^FT "A" 0)),
     testTC "1 . (λ x ⇒ fω x) ⇐ ω.A → A" $
-      check_ empty sone
+      check_ empty SOne
         (^LamY "x" (E $ ^App (^F "fω" 0) (^BVT 0)))
         (^Arr Any (^FT "A" 0) (^FT "A" 0)),
     testTCFail "1 . (λ x ⇒ fω x) ⇍ 0.A → A" $
-      check_ empty sone
+      check_ empty SOne
         (^LamY "x" (E $ ^App (^F "fω" 0) (^BVT 0)))
         (^Arr Zero (^FT "A" 0) (^FT "A" 0)),
     testTCFail "1 . (λ x ⇒ fω x) ⇍ 1.A → A" $
-      check_ empty sone
+      check_ empty SOne
         (^LamY "x" (E $ ^App (^F "fω" 0) (^BVT 0)))
         (^Arr One (^FT "A" 0) (^FT "A" 0)),
     note "refl : (0·A : ★₀) → (1·x : A) → (x ≡ x : A) ≔ (λ A x ⇒ δ _ ⇒ x)",
-    testTC "1 · refl ⇒ ⋯" $ inferAs empty sone (^F "refl" 0) reflTy,
-    testTC "1 · [refl] ⇐ ⋯" $ check_ empty sone (^FT "refl" 0) reflTy
+    testTC "1 · refl ⇒ ⋯" $ inferAs empty SOne (^F "refl" 0) reflTy,
+    testTC "1 · [refl] ⇐ ⋯" $ check_ empty SOne (^FT "refl" 0) reflTy
   ],
 
   "bound vars" :- [
     testTC "x : A ⊢ 1 · x ⇒ A ⊳ 1·x" $
-      inferAsQ (ctx [< ("x", ^FT "A" 0)]) sone
+      inferAsQ (ctx [< ("x", ^FT "A" 0)]) SOne
         (^BV 0) (^FT "A" 0) [< One],
     testTC "x : A ⊢ 1 · x ⇐ A ⊳ 1·x" $
-      checkQ (ctx [< ("x", ^FT "A" 0)]) sone (^BVT 0) (^FT "A" 0) [< One],
+      checkQ (ctx [< ("x", ^FT "A" 0)]) SOne (^BVT 0) (^FT "A" 0) [< One],
     note "f2 : 1.A → 1.A → B",
     testTC "x : A ⊢ 1 · f2 x x ⇒ B ⊳ ω·x" $
-      inferAsQ (ctx [< ("x", ^FT "A" 0)]) sone
+      inferAsQ (ctx [< ("x", ^FT "A" 0)]) SOne
         (^App (^App (^F "f2" 0) (^BVT 0)) (^BVT 0)) (^FT "B" 0) [< Any]
   ],
 
   "lambda" :- [
     note "linear & unrestricted identity",
     testTC "1 · (λ x ⇒ x) ⇐ A → A" $
-      check_ empty sone
+      check_ empty SOne
         (^LamY "x" (^BVT 0))
         (^Arr One (^FT "A" 0) (^FT "A" 0)),
     testTC "1 · (λ x ⇒ x) ⇐ ω.A → A" $
-      check_ empty sone
+      check_ empty SOne
         (^LamY "x" (^BVT 0))
         (^Arr Any (^FT "A" 0) (^FT "A" 0)),
     note "(fail) zero binding used relevantly",
     testTCFail "1 · (λ x ⇒ x) ⇍ 0.A → A" $
-      check_ empty sone
+      check_ empty SOne
         (^LamY "x" (^BVT 0))
         (^Arr Zero (^FT "A" 0) (^FT "A" 0)),
     note "(but ok in overall erased context)",
     testTC "0 · (λ x ⇒ x) ⇐ A ⇾ A" $
-      check_ empty szero
+      check_ empty SZero
         (^LamY "x" (^BVT 0))
         (^Arr Zero (^FT "A" 0) (^FT "A" 0)),
     testTC "1 · (λ A x ⇒ refl A x) ⇐ ⋯  # (type of refl)" $
-      check_ empty sone
+      check_ empty SOne
         (^LamY "A" (^LamY "x"
           (E $ ^App (^App (^F "refl" 0) (^BVT 1)) (^BVT 0))))
         reflTy,
     testTC "1 · (λ A x ⇒ δ i ⇒ x) ⇐ ⋯  # (def. and type of refl)" $
-      check_ empty sone reflDef reflTy
+      check_ empty SOne reflDef reflTy
   ],
 
   "pairs" :- [
     testTC "1 · (a, a) ⇐ A × A" $
-      check_ empty sone
+      check_ empty SOne
         (^Pair (^FT "a" 0) (^FT "a" 0)) (^And (^FT "A" 0) (^FT "A" 0)),
     testTC "x : A ⊢ 1 · (x, x) ⇐ A × A ⊳ ω·x" $
-      checkQ (ctx [< ("x", ^FT "A" 0)]) sone
+      checkQ (ctx [< ("x", ^FT "A" 0)]) SOne
         (^Pair (^BVT 0) (^BVT 0)) (^And (^FT "A" 0) (^FT "A" 0)) [< Any],
     testTC "1 · (a, δ i ⇒ a) ⇐ (x : A) × (x ≡ a)" $
-      check_ empty sone
+      check_ empty SOne
         (^Pair (^FT "a" 0) (^DLamN (^FT "a" 0)))
         (^SigY "x" (^FT "A" 0) (^Eq0 (^FT "A" 0) (^BVT 0) (^FT "a" 0)))
   ],
 
   "unpairing" :- [
     testTC "x : A × A ⊢ 1 · (case1 x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 1·x" $
-      inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "A" 0))]) sone
+      inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "A" 0))]) SOne
         (^CasePair One (^BV 0) (SN $ ^FT "B" 0)
           (SY [< "l", "r"] $ E $ ^App (^App (^F "f2" 0) (^BVT 1)) (^BVT 0)))
         (^FT "B" 0) [< One],
     testTC "x : A × A ⊢ 1 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ ω·x" $
-      inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "A" 0))]) sone
+      inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "A" 0))]) SOne
         (^CasePair Any (^BV 0) (SN $ ^FT "B" 0)
           (SY [< "l", "r"] $ E $ ^App (^App (^F "f2" 0) (^BVT 1)) (^BVT 0)))
         (^FT "B" 0) [< Any],
     testTC "x : A × A ⊢ 0 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 0·x" $
-      inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "A" 0))]) szero
+      inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "A" 0))]) SZero
         (^CasePair Any (^BV 0) (SN $ ^FT "B" 0)
           (SY [< "l", "r"] $ E $ ^App (^App (^F "f2" 0) (^BVT 1)) (^BVT 0)))
         (^FT "B" 0) [< Zero],
     testTCFail "x : A × A ⊢ 1 · (case0 x return B of (l,r) ⇒ f2 l r) ⇏" $
-      infer_ (ctx [< ("x", ^And (^FT "A" 0) (^FT "A" 0))]) sone
+      infer_ (ctx [< ("x", ^And (^FT "A" 0) (^FT "A" 0))]) SOne
         (^CasePair Zero (^BV 0) (SN $ ^FT "B" 0)
           (SY [< "l", "r"] $ E $ ^App (^App (^F "f2" 0) (^BVT 1)) (^BVT 0))),
     testTC "x : A × B ⊢ 1 · (caseω x return A of (l,r) ⇒ l) ⇒ A ⊳ ω·x" $
-      inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "B" 0))]) sone
+      inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "B" 0))]) SOne
         (^CasePair Any (^BV 0) (SN $ ^FT "A" 0)
           (SY [< "l", "r"] $ ^BVT 1))
         (^FT "A" 0) [< Any],
     testTC "x : A × B ⊢ 0 · (case1 x return A of (l,r) ⇒ l) ⇒ A ⊳ 0·x" $
-      inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "B" 0))]) szero
+      inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "B" 0))]) SZero
         (^CasePair One (^BV 0) (SN $ ^FT "A" 0)
           (SY [< "l", "r"] $ ^BVT 1))
         (^FT "A" 0) [< Zero],
     testTCFail "x : A × B ⊢ 1 · (case1 x return A of (l,r) ⇒ l) ⇏" $
-      infer_ (ctx [< ("x", ^And (^FT "A" 0) (^FT "B" 0))]) sone
+      infer_ (ctx [< ("x", ^And (^FT "A" 0) (^FT "B" 0))]) SOne
         (^CasePair One (^BV 0) (SN $ ^FT "A" 0)
           (SY [< "l", "r"] $ ^BVT 1)),
     note "fst : 0.(A : ★₀) → 0.(B : ω.A → ★₀) → ω.((x : A) × B x) → A",
     note "    ≔ (λ A B p ⇒ caseω p return A of (x, y) ⇒ x)",
     testTC "0 · ‹type of fst› ⇐ ★₁" $
-      check_ empty szero fstTy (^TYPE 1),
+      check_ empty SZero fstTy (^TYPE 1),
     testTC "1 · ‹def of fst› ⇐ ‹type of fst›" $
-      check_ empty sone fstDef fstTy,
+      check_ empty SOne fstDef fstTy,
     note "snd : 0.(A : ★₀) → 0.(B : A ↠ ★₀) → ω.(p : (x : A) × B x) → B (fst A B p)",
     note "    ≔ (λ A B p ⇒ caseω p return p ⇒ B (fst A B p) of (x, y) ⇒ y)",
     testTC "0 · ‹type of snd› ⇐ ★₁" $
-      check_ empty szero sndTy (^TYPE 1),
+      check_ empty SZero sndTy (^TYPE 1),
     testTC "1 · ‹def of snd› ⇐ ‹type of snd›" $
-      check_ empty sone sndDef sndTy,
+      check_ empty SOne sndDef sndTy,
     testTC "0 · snd A P ⇒ ω.(p : (x : A) × P x) → P (fst A P p)" $
-      inferAs empty szero
+      inferAs empty SZero
         (^App (^App (^F "snd" 0) (^FT "A" 0)) (^FT "P" 0))
         (^PiY Any "p" (^SigY "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))
           (E $ ^App (^F "P" 0)
             (E $ apps (^F "fst" 0) [^FT "A" 0, ^FT "P" 0, ^BVT 0]))),
     testTC "1 · fst A (λ _ ⇒ B) (a, b) ⇒ A" $
-      inferAs empty sone
+      inferAs empty SOne
         (apps (^F "fst" 0)
               [^FT "A" 0, ^LamN (^FT "B" 0), ^Pair (^FT "a" 0) (^FT "b" 0)])
         (^FT "A" 0),
     testTC "1 · fst¹ A (λ _ ⇒ B) (a, b) ⇒ A" $
-      inferAs empty sone
+      inferAs empty SOne
         (apps (^F "fst" 1)
               [^FT "A" 0, ^LamN (^FT "B" 0), ^Pair (^FT "a" 0) (^FT "b" 0)])
         (^FT "A" 0),
     testTCFail "1 · fst ★⁰ (λ _ ⇒ ★⁰) (A, B) ⇏" $
-      infer_ empty sone
+      infer_ empty SOne
         (apps (^F "fst" 0)
               [^TYPE 0, ^LamN (^TYPE 0), ^Pair (^FT "A" 0) (^FT "B" 0)]),
     testTC "0 · fst¹ ★⁰ (λ _ ⇒ ★⁰) (A, B) ⇒ ★⁰" $
-      inferAs empty szero
+      inferAs empty SZero
         (apps (^F "fst" 1)
               [^TYPE 0, ^LamN (^TYPE 0), ^Pair (^FT "A" 0) (^FT "B" 0)])
         (^TYPE 0)
@@ -422,23 +422,23 @@ tests = "typechecker" :- [
 
   "enums" :- [
     testTC "1 · 'a ⇐ {a}" $
-      check_ empty sone (^Tag "a") (^enum ["a"]),
+      check_ empty SOne (^Tag "a") (^enum ["a"]),
     testTC "1 · 'a ⇐ {a, b, c}" $
-      check_ empty sone (^Tag "a") (^enum ["a", "b", "c"]),
+      check_ empty SOne (^Tag "a") (^enum ["a", "b", "c"]),
     testTCFail "1 · 'a ⇍ {b, c}" $
-      check_ empty sone (^Tag "a") (^enum ["b", "c"]),
+      check_ empty SOne (^Tag "a") (^enum ["b", "c"]),
     testTC "0=1 ⊢ 1 · 'a ⇐ {b, c}" $
-      check_ empty01 sone (^Tag "a") (^enum ["b", "c"])
+      check_ empty01 SOne (^Tag "a") (^enum ["b", "c"])
   ],
 
   "enum matching" :- [
     testTC "ω.x : {tt} ⊢ 1 · case1 x return {tt} of { 'tt ⇒ 'tt } ⇒ {tt}" $
-      inferAs (ctx [< ("x", ^enum ["tt"])]) sone
+      inferAs (ctx [< ("x", ^enum ["tt"])]) SOne
         (^CaseEnum One (^BV 0) (SN (^enum ["tt"]))
           (singleton "tt" (^Tag "tt")))
         (^enum ["tt"]),
     testTCFail "ω.x : {tt} ⊢ 1 · case1 x return {tt} of { 'ff ⇒ 'tt } ⇏" $
-      infer_ (ctx [< ("x", ^enum ["tt"])]) sone
+      infer_ (ctx [< ("x", ^enum ["tt"])]) SOne
         (^CaseEnum One (^BV 0) (SN (^enum ["tt"]))
           (singleton "ff" (^Tag "tt")))
   ],
@@ -447,44 +447,44 @@ tests = "typechecker" :- [
     testTC "0 · ℕ ≡ ℕ : ★₀ ⇐ Type" $
       checkType_ empty (^Eq0 (^TYPE 0) nat nat) Nothing,
     testTC "0 · ℕ ≡ ℕ : ★₀ ⇐ ★₁" $
-      check_ empty szero (^Eq0 (^TYPE 0) nat nat) (^TYPE 1),
+      check_ empty SZero (^Eq0 (^TYPE 0) nat nat) (^TYPE 1),
     testTCFail "1 · ℕ ≡ ℕ : ★₀ ⇍ ★₁" $
-      check_ empty sone (^Eq0 (^TYPE 0) nat nat) (^TYPE 1),
+      check_ empty SOne (^Eq0 (^TYPE 0) nat nat) (^TYPE 1),
     testTC "0 · ℕ ≡ ℕ : ★₀ ⇐ ★₂" $
-      check_ empty szero (^Eq0 (^TYPE 0) nat nat) (^TYPE 2),
+      check_ empty SZero (^Eq0 (^TYPE 0) nat nat) (^TYPE 2),
     testTC "0 · ℕ ≡ ℕ : ★₁ ⇐ ★₂" $
-      check_ empty szero (^Eq0 (^TYPE 1) nat nat) (^TYPE 2),
+      check_ empty SZero (^Eq0 (^TYPE 1) nat nat) (^TYPE 2),
     testTCFail "0 · ℕ ≡ ℕ : ★₁ ⇍ ★₁" $
-      check_ empty szero (^Eq0 (^TYPE 1) nat nat) (^TYPE 1),
+      check_ empty SZero (^Eq0 (^TYPE 1) nat nat) (^TYPE 1),
     testTCFail "0 ≡ 'beep : {beep} ⇍ Type" $
       checkType_ empty
         (^Eq0 (^enum ["beep"]) (^Zero) (^Tag "beep"))
         Nothing,
     testTC "ab : A ≡ B : ★₀, x : A, y : B ⊢ 0 · Eq [i ⇒ ab i] x y ⇐ ★₀" $
       check_ (ctx [< ("ab", ^Eq0 (^TYPE 0) (^FT "A" 0) (^FT "B" 0)),
-                     ("x", ^FT "A" 0), ("y", ^FT "B" 0)]) szero
+                     ("x", ^FT "A" 0), ("y", ^FT "B" 0)]) SZero
         (^EqY "i" (E $ ^DApp (^BV 2) (^BV 0)) (^BVT 1) (^BVT 0))
         (^TYPE 0),
     testTCFail "ab : A ≡ B : ★₀, x : A, y : B ⊢ Eq [i ⇒ ab i] y x ⇍ Type" $
       check_ (ctx [< ("ab", ^Eq0 (^TYPE 0) (^FT "A" 0) (^FT "B" 0)),
-                     ("x", ^FT "A" 0), ("y", ^FT "B" 0)]) szero
+                     ("x", ^FT "A" 0), ("y", ^FT "B" 0)]) SZero
         (^EqY "i" (E $ ^DApp (^BV 2) (^BV 0)) (^BVT 0) (^BVT 1))
         (^TYPE 0)
   ],
 
   "equalities" :- [
     testTC "1 · (δ i ⇒ a) ⇐ a ≡ a" $
-      check_ empty sone (^DLamN (^FT "a" 0))
+      check_ empty SOne (^DLamN (^FT "a" 0))
         (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0)),
     testTC "0 · (λ p q ⇒ δ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q  # uip" $
-      check_ empty szero
+      check_ empty SZero
         (^LamY "p" (^LamY "q" (^DLamN (^BVT 1))))
         (^PiY Any "p" (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0))
           (^PiY Any "q" (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0))
             (^Eq0 (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0))
               (^BVT 1) (^BVT 0)))),
     testTC "0 · (λ p q ⇒ δ i ⇒ q) ⇐ (ω·p q : a ≡ a') → p ≡ q  # uip(2)" $
-      check_ empty szero
+      check_ empty SZero
         (^LamY "p" (^LamY "q" (^DLamN (^BVT 0))))
         (^PiY Any "p" (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0))
           (^PiY Any "q" (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0))
@@ -493,15 +493,15 @@ tests = "typechecker" :- [
   ],
 
   "natural numbers" :- [
-    testTC "0 · ℕ ⇐ ★₀" $ check_ empty szero nat (^TYPE 0),
-    testTC "0 · ℕ ⇐ ★₇" $ check_ empty szero nat (^TYPE 7),
-    testTCFail "1 · ℕ ⇍ ★₀" $ check_ empty sone nat (^TYPE 0),
-    testTC "1 · zero ⇐ ℕ" $ check_ empty sone (^Zero) nat,
-    testTCFail "1 · zero ⇍ ℕ×ℕ" $ check_ empty sone (^Zero) (^And nat nat),
+    testTC "0 · ℕ ⇐ ★₀" $ check_ empty SZero nat (^TYPE 0),
+    testTC "0 · ℕ ⇐ ★₇" $ check_ empty SZero nat (^TYPE 7),
+    testTCFail "1 · ℕ ⇍ ★₀" $ check_ empty SOne nat (^TYPE 0),
+    testTC "1 · zero ⇐ ℕ" $ check_ empty SOne (^Zero) nat,
+    testTCFail "1 · zero ⇍ ℕ×ℕ" $ check_ empty SOne (^Zero) (^And nat nat),
     testTC "ω·n : ℕ ⊢ 1 · succ n ⇐ ℕ" $
-      check_ (ctx [< ("n", nat)]) sone (^Succ (^BVT 0)) nat,
+      check_ (ctx [< ("n", nat)]) SOne (^Succ (^BVT 0)) nat,
     testTC "1 · λ n ⇒ succ n ⇐ 1.ℕ → ℕ" $
-      check_ empty sone
+      check_ empty SOne
         (^LamY "n" (^Succ (^BVT 0)))
         (^Arr One nat nat)
   ],
@@ -510,7 +510,7 @@ tests = "typechecker" :- [
     note "1 · λ n ⇒ case1 n return ℕ of { zero ⇒ 0; succ n ⇒ n }",
     note "    ⇐ 1.ℕ → ℕ",
     testTC "pred" $
-      check_ empty sone
+      check_ empty SOne
         (^LamY "n" (E $
           ^CaseNat One Zero (^BV 0) (SN nat)
             (^Zero) (SY [< "n", ^BN Unused] $ ^BVT 1)))
@@ -518,7 +518,7 @@ tests = "typechecker" :- [
     note "1 · λ m n ⇒ case1 m return ℕ of { zero ⇒ n; succ _, 1.p ⇒ succ p }",
     note "    ⇐ 1.ℕ → 1.ℕ → 1.ℕ",
     testTC "plus" $
-      check_ empty sone
+      check_ empty SOne
         (^LamY "m" (^LamY "n" (E $
           ^CaseNat One One (^BV 1) (SN nat)
             (^BVT 0)
@@ -528,11 +528,11 @@ tests = "typechecker" :- [
 
   "box types" :- [
     testTC "0 · [0.ℕ] ⇐ ★₀" $
-      check_ empty szero (^BOX Zero nat) (^TYPE 0),
+      check_ empty SZero (^BOX Zero nat) (^TYPE 0),
     testTC "0 · [0.★₀] ⇐ ★₁" $
-      check_ empty szero (^BOX Zero (^TYPE 0)) (^TYPE 1),
+      check_ empty SZero (^BOX Zero (^TYPE 0)) (^TYPE 1),
     testTCFail "0 · [0.★₀] ⇍ ★₀" $
-      check_ empty szero (^BOX Zero (^TYPE 0)) (^TYPE 0)
+      check_ empty SZero (^BOX Zero (^TYPE 0)) (^TYPE 0)
   ],
 
   todo "box values",
@@ -540,7 +540,7 @@ tests = "typechecker" :- [
 
   "type-case" :- [
     testTC "0 · type-case ℕ ∷ ★₀ return ★₀ of { _ ⇒ ℕ } ⇒ ★₀" $
-      inferAs empty szero
+      inferAs empty SZero
         (^TypeCase (^Ann nat (^TYPE 0)) (^TYPE 0) empty nat)
         (^TYPE 0)
   ],
@@ -555,7 +555,7 @@ tests = "typechecker" :- [
     note "1 · λ x y xy ⇒ δ i ⇒ p (xy i)",
     note "  ⇐ (0·x y : A) → (1·xy : x ≡ y) → Eq [i ⇒ P (xy i)] (p x) (p y)",
     testTC "cong" $
-      check_ empty sone
+      check_ empty SOne
         ([< "x", "y", "xy"] :\\ [< "i"] :\\% E (F "p" :@ E (BV 0 :% BV 0)))
         (PiY Zero "x"  (FT "A") $
          PiY Zero "y"  (FT "A") $
@@ -568,7 +568,7 @@ tests = "typechecker" :- [
     note "1 · λ eq ⇒ δ i ⇒ λ x ⇒ eq x i",
     note "  ⇐ (1·eq : (1·x : A) → p x ≡ q x) → p ≡ q",
     testTC "funext" $
-      check_ empty sone
+      check_ empty SOne
         ([< "eq"] :\\ [< "i"] :\\% [< "x"] :\\ E (BV 1 :@ BVT 0 :% BV 0))
         (PiY One "eq"
           (PiY One "x" (FT "A")