fix the other similar loops

closes #38, again

lib/Quox/Whnf/Coercion.idr

@@ -119,7 +119,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
   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›)
+    -- comp [j ⇒ A‹r/i›] @p @q ((eq ∷ (Eq [i ⇒ A] L R)‹p/j›) @r)
     --   @r { 0 j ⇒ L; 1 j ⇒ R }
     let ctx1 = extendDim j ctx
     Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
@@ -147,6 +147,10 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
       (ST body.names $ body.term // (a' ::: shift 1)) loc
 
 
+-- new params block to call the above functions at different `n`
+parameters {auto _ : CanWhnf Term Interface.isRedexT}
+           {auto _ : CanWhnf Elim Interface.isRedexE}
+           (defs : Definitions) (ctx : WhnfContext d n) (sg : SQty)
   ||| pushes a coercion inside a whnf-ed term
   export covering
   pushCoe : BindName ->
@@ -163,17 +167,22 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
       IOState tyLoc =>
         whnf defs ctx sg $ Ann s (IOState tyLoc) loc
 
-      -- η expand it so that whnf for App can deal with it
+      -- η expand, then simplify the Coe/App in the body
       --
       -- (coe (𝑖 ⇒ π.(x : A) → B) @p @q s)
       --   ⇝
       -- (λ 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
+      --   ⇝     ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
+      -- (λ y ⇒ ⋯) ∷ (π.(x : A) → B)‹q/𝑖›   -- see `piCoe`
+      --
+      -- do the piCoe step here because otherwise equality checking keeps
+      -- doing the η forever
+      Pi {arg, res = S [< x] _, _} => do
+        let ctx' = extendTy x (arg // one p) ctx
+        body <- piCoe defs ctx' sg
+          (weakDS 1 $ SY [< i] ty) p q (weakT 1 s) (BVT 0 loc) loc
         whnf defs ctx sg $
-          Ann (LamY !(mnb "y" loc)
-                  (E $ App (weakE 1 inner) (BVT 0 loc) loc) loc)
-              (ty // one q) loc
+          Ann (LamY x (E body.fst) loc) (ty // one q) loc
 
       -- no η!!!
       -- push into a pair constructor, otherwise still stuck
@@ -199,17 +208,23 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
       Enum cases tyLoc =>
         whnf defs ctx sg $ Ann s (Enum cases tyLoc) loc
 
-      -- η expand, same as for Π
+      -- η expand/simplify, same as for Π
       --
       -- (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @q s)
       --   ⇝
       -- (δ 𝑘 ⇒ (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
+      --   ⇝     ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
+      -- (δ 𝑘 ⇒ ⋯) ∷ (Eq (𝑗 ⇒ A) l r)‹q/𝑖›   -- see `eqCoe`
+      --
+      -- do the eqCoe step here because otherwise equality checking keeps
+      -- doing the η forever
+      Eq {ty = S [< j] _, _} => do
+        let ctx' = extendDim j ctx
+        body <- eqCoe defs ctx' sg
+          (dweakDS 1 $ S [< i] $ Y ty) (weakD 1 p) (weakD 1 q)
+          (dweakT 1 s) (BV 0 loc) loc
         whnf defs ctx sg $
-          Ann (DLamY !(mnb "k" loc)
-                  (E $ DApp (dweakE 1 inner) (BV 0 loc) loc) loc)
-              (ty // one q) loc
+          Ann (DLamY i (E body.fst) loc) (ty // one q) loc
 
       -- (coe ℕ @_ @_ s) ⇝ (s ∷ ℕ)
       NAT tyLoc =>
@@ -219,22 +234,19 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
       STRING tyLoc =>
         whnf defs ctx sg $ Ann s (STRING tyLoc) loc
 
-      -- η expand.... kinda
+      -- η expand/simplify
       --
-      -- (coe (𝑖 ⇒ [π. A]) @p @q s)
+      -- (coe (𝑖 ⇒ [π.A]) @p @q s)
       --   ⇝
-      -- [case1 s ∷ [π.A]‹p/𝑖› return A‹q/𝑖›
-      --  of {[x] ⇒ coe (𝑖 ⇒ A) @p @q x}] ∷ [π.A]‹q/𝑖›
+      -- [case coe (𝑖 ⇒ [π.A]) @p @q s return A‹q/𝑖› of {[x] ⇒ x}]
+      --   ⇝
+      -- [case1 s ∷ [π.A]‹p/𝑖› ⋯] ∷ [π.A]‹q/𝑖›   -- see `boxCoe`
       --
-      -- a literal η expansion of `e ⇝ [case e of {[x] ⇒ x}]` causes a loop in
-      -- the equality checker because whnf of `case e ⋯` requires whnf of `e`
+      -- do the eqCoe step here because otherwise equality checking keeps
+      -- doing the η forever
       BOX qty inner tyLoc => do
-        let inner = CaseBox {
-              qty  = One,
-              box  = Ann s (ty // one p) s.loc,
-              ret  = SN $ inner // one q,
-              body = SY [< !(mnb "x" loc)] $ E $
-                     Coe (ST [< i] $ weakT 1 inner) p q (BVT 0 s.loc) s.loc,
-              loc
-            }
-        whnf defs ctx sg $ Ann (Box (E inner) loc) (ty // one q) loc
+        body <- boxCoe defs ctx sg qty
+          (SY [< i] ty) p q s
+          (SN $ inner // one q)
+          (SY [< !(mnb "inner" loc)] (BVT 0 loc)) loc
+        whnf defs ctx sg $ Ann (Box (E body.fst) loc) (ty // one q) loc