don't keep erased applications actually

lib/Quox/Untyped/Erase.idr

@@ -144,18 +144,20 @@ eraseTerm ctx _ s@(TYPE {}) =
 eraseTerm ctx _ s@(Pi {}) =
   throw $ CompileTimeOnly ctx s
 
---        x : A | π.x ⊢ s ⤋ s' ⇐ B
+--      x : A | 0.x ⊢ s ⤋ s' ⇐ B
+-- -------------------------------------
+--  (λ x ⇒ s) ⤋ s'[⌷/x] ⇐ 0.(x : A) → B
+--
+--    x : A | π.x ⊢ s ⤋ s' ⇐ B   π ≠ 0
 -- ----------------------------------------
 --  (λ 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
+  let x = body.name
   (qty, arg, res) <- wrapExpect `(expectPi) ctx loc ty
-  let x = case isErased qty of Kept   => body.name
+  body            <- eraseTerm (extendTy qty x arg ctx) res.term body.term
-                               Erased => BN Unused body.name.loc
+  pure $ case isErased qty of
-  body <- eraseTerm (extendTy qty x arg ctx) res.term body.term
+    Kept   => U.Lam x body loc
-  pure $ U.Lam x body loc
+    Erased => sub1 (Erased loc) body
 
 eraseTerm ctx _ s@(Sig {}) =
   throw $ CompileTimeOnly ctx s
@@ -251,13 +253,13 @@ eraseElim ctx e@(B i loc) = do
 --
 --  f ⤋ f' ⇒ 0.(x : A) → B
 -- -------------------------
---    f s ⤋ f' ⌷ ⇒ B[s/x]
+--    f s ⤋ f' ⇒ B[s/x]
 eraseElim ctx (App fun arg loc) = do
   efun              <- eraseElim ctx fun
   (qty, targ, tres) <- wrapExpect `(expectPi) ctx loc efun.type
   let ty = sub1 tres (Ann arg targ arg.loc)
   case isErased qty of
-    Erased => pure $ EraRes ty $ App efun.term (Erased arg.loc) loc
+    Erased => pure $ EraRes ty efun.term
     Kept   => do arg <- eraseTerm ctx targ arg
                  pure $ EraRes ty $ App efun.term arg loc