erasure to untyped syntax

examples/all.quox

@@ -6,3 +6,4 @@ load "nat.quox"
 load "pair.quox"
 load "list.quox"
 load "eta.quox"
+load "fail.quox"

examples/eta.quox

@@ -18,8 +18,8 @@ def0 pair : (A : ★) → (B : A → ★) → (P : Σ A B → ★) → (e : Σ A
   λ A B P e p ⇒ p
 
 -- not exactly η, but kinda related
-def0 from-false : (A : ★) → (P : (False → A) → ★) → (f : False → A) →
-                  P (λ x ⇒ void A x) → P f =
+def0 from-false : (A : ★) → (P : (0.False → A) → ★) → (f : 0.False → A) →
+                  P (void A) → P f =
   λ A P f p ⇒ p
 
 }

lib/Quox/Equal.idr

@@ -74,6 +74,8 @@ isEmpty : {n : Nat} -> Definitions -> EqContext n -> SQty -> Term 0 n ->
           Eff EqualInner Bool
 isEmpty defs ctx sg ty0 = do
   Element ty0 nc <- whnf defs ctx sg ty0.loc ty0
+  let Left  y = choose $ isTyConE ty0
+    | Right n => pure False
   case ty0 of
     TYPE {} => pure False
     Pi {arg, res, _} => pure False
@@ -85,15 +87,7 @@ isEmpty defs ctx sg ty0 = do
     Eq {} => pure False
     Nat {} => pure False
     BOX {ty, _} => isEmpty defs ctx sg ty
-    E (Ann {tm, _}) => isEmpty defs ctx sg tm
     E _ => pure False
-    Lam  {} => pure False
-    Pair {} => pure False
-    Tag  {} => pure False
-    DLam {} => pure False
-    Zero {} => pure False
-    Succ {} => pure False
-    Box  {} => pure False
 
 ||| true if a type is known to be a subsingleton purely by its form.
 ||| a subsingleton is a type with only zero or one possible values.
@@ -110,6 +104,8 @@ isSubSing : {n : Nat} -> Definitions -> EqContext n -> SQty -> Term 0 n ->
             Eff EqualInner Bool
 isSubSing defs ctx sg ty0 = do
   Element ty0 nc <- whnf defs ctx sg ty0.loc ty0
+  let Left  y = choose $ isTyConE ty0
+    | Right n => pure False
   case ty0 of
     TYPE {} => pure False
     Pi {arg, res, _} =>
@@ -123,15 +119,7 @@ isSubSing defs ctx sg ty0 = do
     Eq {} => pure True
     Nat {} => pure False
     BOX {ty, _} => isSubSing defs ctx sg ty
-    E (Ann {tm, _}) => isSubSing defs ctx sg tm
     E _ => pure False
-    Lam  {} => pure False
-    Pair {} => pure False
-    Tag  {} => pure False
-    DLam {} => pure False
-    Zero {} => pure False
-    Succ {} => pure False
-    Box  {} => pure False
 
 
 ||| the left argument if the current mode is `Super`; otherwise the right one.
@@ -424,7 +412,7 @@ namespace Elim
                      Eff EqualElim (Term 0 n)
   computeElimTypeE defs ectx sg e =
     let Val n = ectx.termLen in
-    lift $ computeElimType defs (toWhnfContext ectx) e {ne}
+    lift $ computeElimType defs (toWhnfContext ectx) sg e
 
   private
   putError : Has InnerErrEff fs => Error -> Eff fs ()

lib/Quox/Untyped/Erase.idr

@@ -27,6 +27,12 @@ isErased Zero = Erased
 isErased One  = Kept
 isErased Any  = Kept
 
+public export
+ifErased : Qty -> Lazy a -> Lazy a -> a
+ifErased pi x y = case isErased pi of
+  Erased => x
+  Kept   => y
+
 
 public export
 EContext : Nat -> Type
@@ -91,7 +97,7 @@ computeElimType ctx sg e = do
       ctx   = toWhnfContext ctx
   defs          <- askAt DEFS
   Element e enf <- liftWhnf $ whnf defs ctx sg e
-  liftWhnf $ computeElimType defs ctx e {ne = enf}
+  liftWhnf $ computeElimType defs ctx sg e
 
 
 parameters (ctx : ErasureContext d n) (loc : Loc)
@@ -162,13 +168,20 @@ extendDim i (MkEContexts {dimLen, dnames, tnames, tctx, erased}) =
   }
 
 
+public export
+record EraseElimResult d n where
+  constructor EraRes
+  type : Lazy (Q.Term d n)
+  term : U.Term n
+
+
 export covering
 eraseTerm : ErasureContext d n ->
             (ty, tm : Q.Term d n) -> Eff Erase (U.Term n)
 
 export covering
 eraseElim : ErasureContext d n -> (tm : Q.Elim d n) ->
-            Eff Erase (Q.Term d n, U.Term n)
+            Eff Erase (EraseElimResult d n)
 
 eraseTerm ctx _ s@(TYPE {}) =
   throw $ CompileTimeOnly ctx s
@@ -176,23 +189,24 @@ eraseTerm ctx _ s@(TYPE {}) =
 eraseTerm ctx _ s@(Pi {}) =
   throw $ CompileTimeOnly ctx s
 
+--         π.x : A ⊢ s ⤋ s' ⇐ B
+-- ----------------------------------------
+--  (λ x ⇒ s) ⤋ (λ x ⇒ s') ⇐ π.(x : A) → B
+--
+-- becomes a lambda even when π = 0,
+-- to preserve expected evaluation order
 eraseTerm ctx ty (Lam body loc) = do
   (qty, arg, res) <- expectPi ctx loc ty
-  case isErased qty of
-    Erased => do
-      -- replace with a fake name like "<erased x>"
-      -- a little trap for future me :3c
-      let name  = baseStr body.name.val
-          dummy = F (unq $ UN "<erased \{name}>") 0 noLoc
-      eraseTerm ctx (sub1 res dummy) (sub1 body dummy)
-    Kept => do
-      let x = body.name
-      body <- eraseTerm (extendTy qty x arg ctx) res.term body.term
-      pure $ U.Lam x body loc
+  let x = body.name
+  body <- eraseTerm (extendTy qty x arg ctx) res.term body.term
+  pure $ U.Lam x body loc
 
 eraseTerm ctx _ s@(Sig {}) =
   throw $ CompileTimeOnly ctx s
 
+--   s ⤋ s' ⇐ A    t ⤋ t' ⇐ B[s/x]
+-- ---------------------------------
+--  (s, t) ⤋ (s', t') ⇐ (x : A) × B
 eraseTerm ctx ty (Pair fst snd loc) = do
   (a, b) <- expectSig ctx loc ty
   let b = sub1 b (Ann fst a a.loc)
@@ -203,22 +217,30 @@ eraseTerm ctx ty (Pair fst snd loc) = do
 eraseTerm ctx _ s@(Enum {}) =
   throw $ CompileTimeOnly ctx s
 
+-- '𝐚 ⤋ '𝐚 ⇐ {⋯}
 eraseTerm ctx _ (Tag tag loc) =
   pure $ Tag tag loc
 
 eraseTerm ctx ty s@(Eq {}) =
   throw $ CompileTimeOnly ctx s
 
+--        𝑖 ⊢ s ⤋ s' ⇐ A
+-- ---------------------------------
+--  (δ 𝑖 ⇒ s) ⤋ s' ⇐ Eq (𝑖 ⇒ A) l r
 eraseTerm ctx ty (DLam body loc) = do
-  (a, _, _) <- expectEq ctx loc ty
+  a <- fst <$> expectEq ctx loc ty
   eraseTerm (extendDim body.name ctx) a.term body.term
 
 eraseTerm ctx _ s@(Nat {}) =
   throw $ CompileTimeOnly ctx s
 
+-- 0 ⤋ 0 ⇐ ℕ
 eraseTerm _ _ (Zero loc) =
   pure $ Zero loc
 
+--       s ⤋ s' ⇐ ℕ
+-- -----------------------
+--  succ s ⤋ succ s' ⇐ ℕ
 eraseTerm ctx ty (Succ p loc) = do
   p <- eraseTerm ctx ty p
   pure $ Succ p loc
@@ -226,21 +248,32 @@ eraseTerm ctx ty (Succ p loc) = do
 eraseTerm ctx ty s@(BOX {}) =
   throw $ CompileTimeOnly ctx s
 
+-- [s] ⤋ ⌷ ⇐ [0.A]
+--
+--  π ≠ 0   s ⤋ s' ⇐ A
+-- --------------------
+--   [s] ⤋ s' ⇐ [π.A]
 eraseTerm ctx ty (Box val loc) = do
   (qty, a) <- expectBOX ctx loc ty
   case isErased qty of
-    Erased => pure $ ErasedBox loc -- lmao
+    Erased => pure $ Erased loc
     Kept   => eraseTerm ctx a val
 
+--  e ⤋ e' ⇒ B
+-- ------------
+--  e ⤋ e' ⇐ A
 eraseTerm ctx ty (E e) =
-  snd <$> eraseElim ctx e
+  term <$> eraseElim ctx e
 
-eraseTerm ctx ty (CloT  (Sub term th)) =
+eraseTerm ctx ty (CloT (Sub term th)) =
   eraseTerm ctx ty $ pushSubstsWith' id th term
 
 eraseTerm ctx ty (DCloT (Sub term th)) =
   eraseTerm ctx ty $ pushSubstsWith' th id term
 
+--  defω x : A = s
+-- ----------------
+--    x ⤋ x ⇒ A
 eraseElim ctx e@(F x u loc) = do
   Just def <- asksAt DEFS $ lookup x
     | Nothing => throw $ NotInScope x
@@ -248,54 +281,103 @@ eraseElim ctx e@(F x u loc) = do
     Erased => throw $ CompileTimeOnly ctx $ E e
     Kept =>
       let Val d = ctx.dimLen; Val n = ctx.termLen in
-      pure (def.type, F x loc)
+      pure $ EraRes def.type $ F x loc
 
+--            π ≠ 0
+-- ----------------------------
+--  Γ, π.x : A, Γ' ⊢ x ⤋ x ⇒ A
 eraseElim ctx e@(B i loc) = do
   case ctx.erased !!! i of
     Erased => throw $ CompileTimeOnly ctx $ E e
-    Kept   => pure (ctx.tctx !! i, B i loc)
+    Kept   => pure $ EraRes (ctx.tctx !! i) $ B i loc
 
+--  f ⤋ f' ⇒ π.(x : A) → B   s ⤋ s' ⇒ A   π ≠ 0
+-- ---------------------------------------------
+--             f s ⤋ f' s' ⇒ B[s/x]
+--
+--  f ⤋ f' ⇒ 0.(x : A) → B
+-- -------------------------
+--    f s ⤋ f' ⌷ ⇒ B[s/x]
 eraseElim ctx (App fun arg loc) = do
-  (tfun, fun)       <- eraseElim ctx fun
-  (qty, targ, tres) <- expectPi ctx loc tfun
+  efun              <- eraseElim ctx fun
+  (qty, targ, tres) <- expectPi ctx loc efun.type
   let ty = sub1 tres (Ann arg targ arg.loc)
   case isErased qty of
-    Erased => pure (ty, fun)
+    Erased => pure $ EraRes ty $ App efun.term (Erased arg.loc) loc
     Kept   => do arg <- eraseTerm ctx targ arg
-                 pure (ty, App fun arg loc)
+                 pure $ EraRes ty $ App efun.term arg loc
 
+--                     e ⤋ e' ⇒ (x : A) × B
+--       ρ.x : A, ρ.y : B ⊢ s ⤋ s' ⇐ R[((x,y) ∷ (x : A) × B)/z]
+--  x̃ ≔ if ρ = 0 then ⌷ else fst e'   ỹ ≔ if ρ = 0 then ⌷ else snd e'
+-- -------------------------------------------------------------------
+--   (caseρ e return z ⇒ R of {(x, y) ⇒ s}) ⤋ s'[x̃/x, ỹ/y] ⇒ R[e/z]
 eraseElim ctx (CasePair qty pair ret body loc) = do
-  ty <- computeElimType ctx SOne pair
-  eraseElim ctx $
-    Ann (subN body [< Fst pair pair.loc, Snd pair pair.loc])
-        (sub1 ret pair) loc
+  epair <- eraseElim ctx pair
+  let ty = sub1 (ret // shift 2) $
+           Ann (Pair (BVT 0 loc) (BVT 1 loc) loc) (weakT 2 epair.type) loc
+  (tfst, tsnd) <- expectSig ctx loc epair.type
+  let [< x, y] = body.names
+  let ctx' = extendTyN [< (qty, x, tfst), (qty, y, tsnd.term)] ctx
+  body' <- eraseTerm ctx' ty body.term
+  let x' = ifErased qty (Erased loc) (Fst epair.term loc)
+      y' = ifErased qty (Erased loc) (Snd epair.term loc)
+  pure $ EraRes (sub1 ret pair) $ body' // fromSnocVect [< x', y']
 
+--  e ⤋ e' ⇒ (x : A) × B
+-- ----------------------
+--   fst e ⤋ fst e' ⇒ A
 eraseElim ctx (Fst pair loc) = do
-  (ty, pair) <- eraseElim ctx pair
-  (a,  _)    <- expectSig ctx loc ty
-  pure (a, Fst pair loc)
+  epair      <- eraseElim ctx pair
+  a          <- fst <$> expectSig ctx loc epair.type
+  pure $ EraRes a $ Fst epair.term loc
 
-eraseElim ctx (Snd pair0 loc) = do
-  (ty, pair) <- eraseElim ctx pair0
-  (_,  b)    <- expectSig ctx loc ty
-  pure (sub1 b (Fst pair0 loc), Snd pair loc)
+--     e ⤋ e' ⇒ (x : A) × B
+-- -----------------------------
+--  snd e ⤋ snd e' ⇒ B[fst e/x]
+eraseElim ctx (Snd pair loc) = do
+  epair      <- eraseElim ctx pair
+  b          <- snd <$> expectSig ctx loc epair.type
+  pure $ EraRes (sub1 b (Fst pair loc)) $ Snd epair.term loc
 
+-- case0 e return z ⇒ R of {} ⤋ absurd ⇒ R[e/z]
+--
+--               s ⤋ s' ⇐ R[𝐚∷{𝐚}/z]
+-- -----------------------------------------------
+--  case0 e return z ⇒ R of {𝐚 ⇒ s} ⤋ s' ⇒ R[e/z]
+--
+--           e ⤋ e' ⇒ A   ρ ≠ 0    sᵢ ⤋ s'ᵢ ⇐ R[𝐚ᵢ/z]
+-- -------------------------------------------------------------------
+--  caseρ e return z ⇒ R of {𝐚ᵢ ⇒ sᵢ} ⤋ case e of {𝐚ᵢ ⇒ s'ᵢ} ⇒ R[e/z]
 eraseElim ctx e@(CaseEnum qty tag ret arms loc) =
   case isErased qty of
     Erased => case SortedMap.toList arms of
-      []         => pure (sub1 ret tag, Absurd loc)
-      [(_, arm)] => let ty = sub1 ret tag in (ty,) <$> eraseTerm ctx ty arm
+      []         => pure $ EraRes (sub1 ret tag) $ Absurd loc
+      [(t, arm)] => do
+        let ty  = sub1 ret tag
+            ty' = sub1 ret (Ann (Tag t loc) (enum [t] loc) loc)
+        arm' <- eraseTerm ctx ty' arm
+        pure $ EraRes ty arm'
       _          => throw $ CompileTimeOnly ctx $ E e
     Kept => do
       let ty = sub1 ret tag
-      (tagTy, tag) <- eraseElim ctx tag
-      arms <- for (SortedMap.toList arms) $ \(t, rhs) =>
-        (t,) <$> eraseTerm ctx (sub1 ret $ Ann (Tag t loc) tagTy loc) rhs
-      pure (ty, CaseEnum tag arms loc)
+      etag <- eraseElim ctx tag
+      arms <- for (SortedMap.toList arms) $ \(t, rhs) => do
+        let ty' = sub1 ret (Ann (Tag t loc) etag.type loc)
+        rhs' <- eraseTerm ctx ty' rhs
+        pure (t, rhs')
+      pure $ EraRes ty $ CaseEnum etag.term arms loc
 
+--          n ⤋ n' ⇒ ℕ   z ⤋ z' ⇐ R[zero∷ℕ/z]
+--  ρ.m : ℕ, ς.ih : R[m/z] ⊢ s ⤋ s' ⇐ R[(succ m)∷ℕ/z]
+-- ---------------------------------------------------
+--  caseρ n return z ⇒ R of {0 ⇒ z; succ m, ς.ih ⇒ s}
+--    ⤋
+--  case n' of {0 ⇒ z'; succ m, ih ⇒ s'}
+--    ⇒ R[n/z]
 eraseElim ctx (CaseNat qty qtyIH nat ret zero succ loc) = do
   let ty = sub1 ret nat
-  (_, nat) <- eraseElim ctx nat
+  enat <- eraseElim ctx nat
   zero <- eraseTerm ctx (sub1 ret (Ann (Zero loc) (Nat loc) loc)) zero
   let [< p, ih] = succ.names
   succ <- eraseTerm
@@ -303,27 +385,60 @@ eraseElim ctx (CaseNat qty qtyIH nat ret zero succ loc) = do
                   (qtyIH, ih, sub1 (ret // shift 1) (BV 0 loc))] ctx)
     (sub1 (ret // shift 2) (Ann (Succ (BVT 1 loc) loc) (Nat loc) loc))
     succ.term
-  pure (ty, CaseNat nat zero p ih succ loc)
+  pure $ EraRes ty $ CaseNat enat.term zero p ih succ loc
 
+--                b ⤋ b' ⇒ [π.A]   π ≠ 0
+--          πρ.x : A ⊢ s ⤋ s' ⇐ R[[x]∷[π.A]/z]
+-- -------------------------------------------------------
+--  caseρ b return z ⇒ R of {[x] ⇒ s} ⤋ s'[b'/x] ⇒ R[b/z]
+--
+--     b ⇒ [0.A]   0.x : A ⊢ s ⤋ s' ⇐ R[[x]∷[0.A]/z]
+-- -------------------------------------------------------
+--   caseρ b return z ⇒ R of {[x] ⇒ s} ⤋ s'[⌷/x] ⇒ R[b/z]
 eraseElim ctx (CaseBox qty box ret body loc) = do
-  let ty = sub1 ret box
-  body <- eraseTerm ctx ty $ sub1 body box
-  pure (ty, body)
+  tbox <- computeElimType ctx SOne box -- [fixme] is there any way to avoid this?
+  (pi, tinner) <- expectBOX ctx loc tbox
+  let ctx' = extendTy Zero body.name tinner ctx
+      bty  = sub1 (ret // shift 1) $
+             Ann (Box (BVT 0 loc) loc) (weakT 1 tbox) loc
+  case isErased pi of
+    Kept => do
+      ebox  <- eraseElim ctx box
+      ebody <- eraseTerm ctx' bty body.term
+      pure $ EraRes (sub1 ret box) $ ebody // one ebox.term
+    Erased => do
+      body' <- eraseTerm ctx' bty body.term
+      pure $ EraRes (sub1 ret box) $ body' // one (Erased loc)
 
+--    f ⤋ f' ⇒ Eq (𝑖 ⇒ A) l r
+-- ------------------------------
+--      f @r ⤋ f' ⇒ A‹r/𝑖›
 eraseElim ctx (DApp fun arg loc) = do
-  (tfun, fun) <- eraseElim ctx fun
-  (a, _, _)   <- expectEq ctx loc tfun
-  pure (dsub1 a arg, fun)
+  efun <- eraseElim ctx fun
+  a    <- fst <$> expectEq ctx loc efun.type
+  pure $ EraRes (dsub1 a arg) efun.term
 
+--    s ⤋ s' ⇐ A
+-- ----------------
+--  s ∷ A ⤋ s' ⇒ A
 eraseElim ctx (Ann tm ty loc) =
-  (ty,) <$> eraseTerm ctx ty tm
+  EraRes ty <$> eraseTerm ctx ty tm
 
+--        s ⤋ s' ⇐ A‹p/𝑖›
+-- -----------------------------------
+--  coe (𝑖 ⇒ A) @p @q s ⤋ s' ⇒ A‹q/𝑖›
 eraseElim ctx (Coe ty p q val loc) = do
-  val <- eraseTerm ctx (dsub1 ty q) val
-  pure (dsub1 ty p, val)
+  val <- eraseTerm ctx (dsub1 ty p) val
+  pure $ EraRes (dsub1 ty q) val
 
+--          s ⤋ s' ⇐ A
+-- --------------------------------
+--  comp A @p @q s @r {⋯} ⤋ s' ⇒ A
+--
+-- [todo] is this ok? they are equal, but even so,
+-- maybe t₀ and t₁ have different performance characteristics
 eraseElim ctx (Comp ty p q val r zero one loc) =
-  (ty,) <$> eraseTerm ctx ty val
+  EraRes ty <$> eraseTerm ctx ty val
 
 eraseElim ctx t@(TypeCase ty ret arms def loc) =
   throw $ CompileTimeOnly ctx $ E t

lib/Quox/Whnf/ComputeElimType.idr

@@ -11,24 +11,26 @@ import Quox.Displace
 ||| - assumes the elim is already typechecked
 ||| - the return value is not reduced
 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 sg e)) =>
-                  Eff Whnf (Term d n)
+computeElimType :
+  CanWhnf Term Interface.isRedexT =>
+  CanWhnf Elim Interface.isRedexE =>
+  {d, n : Nat} ->
+  (defs : Definitions) -> WhnfContext d n -> (0 sg : SQty) ->
+  (e : Elim d n) -> (0 ne : No (isRedexE defs sg e)) =>
+  Eff Whnf (Term d n)
 
 
 ||| computes a type and then reduces it to whnf
 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 sg e)) =>
-                       Eff Whnf (Term d n)
+computeWhnfElimType0 :
+  CanWhnf Term Interface.isRedexT =>
+  CanWhnf Elim Interface.isRedexE =>
+  {d, n : Nat} ->
+  (defs : Definitions) -> WhnfContext d n -> (0 sg : SQty) ->
+  (e : Elim d n) -> (0 ne : No (isRedexE defs sg e)) =>
+  Eff Whnf (Term d n)
 
-computeElimType defs ctx e {ne} =
+computeElimType defs ctx sg e =
   case e of
     F x u loc => do
       let Just def = lookup x defs
@@ -39,7 +41,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 sg f {ne = noOr1 ne}) of
         Pi {arg, res, _} => pure $ sub1 res $ Ann s arg loc
         ty               => throw $ ExpectedPi loc ctx.names ty
 
@@ -47,12 +49,12 @@ computeElimType defs ctx e {ne} =
       pure $ sub1 ret pair
 
     Fst pair loc =>
-      case !(computeWhnfElimType0 defs ctx pair {ne = noOr1 ne}) of
+      case !(computeWhnfElimType0 defs ctx sg pair {ne = noOr1 ne}) of
         Sig {fst, _} => pure fst
         ty           => throw $ ExpectedSig loc ctx.names ty
 
     Snd pair loc =>
-      case !(computeWhnfElimType0 defs ctx pair {ne = noOr1 ne}) of
+      case !(computeWhnfElimType0 defs ctx sg pair {ne = noOr1 ne}) of
         Sig {snd, _} => pure $ sub1 snd $ Fst pair loc
         ty           => throw $ ExpectedSig loc ctx.names ty
 
@@ -66,7 +68,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 sg f {ne = noOr1 ne}) of
         Eq {ty, _} => pure $ dsub1 ty p
         t          => throw $ ExpectedEq loc ctx.names t
 
@@ -82,5 +84,5 @@ computeElimType defs ctx e {ne} =
     TypeCase {ret, _} =>
       pure ret
 
-computeWhnfElimType0 defs ctx e =
-  computeElimType defs ctx e {sg} >>= whnf0 defs ctx SZero
+computeWhnfElimType0 defs ctx sg e =
+  computeElimType defs ctx sg e >>= whnf0 defs ctx SZero

lib/Quox/Whnf/Main.idr

@@ -157,7 +157,7 @@ CanWhnf Elim Interface.isRedexE where
           eqCoe defs ctx sg ty p' q' val p appLoc
       Right ndlh => case p of
         K e _ => do
-          Eq {l, r, ty, _} <- computeWhnfElimType0 defs ctx f {ne = fnf}
+          Eq {l, r, ty, _} <- computeWhnfElimType0 defs ctx sg f
             | ty => throw $ ExpectedEq ty.loc ctx.names ty
           whnf defs ctx sg $
             ends (Ann (setLoc appLoc l) ty.zero appLoc)

lib/Quox/Whnf/TypeCase.idr

@@ -39,7 +39,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
              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
@@ -57,7 +57,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
               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
@@ -75,7 +75,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
               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
 
@@ -87,7 +87,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
              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