add coercion regularity to the equality checker (not to whnf)

lib/Quox/Equal.idr

@@ -8,6 +8,7 @@ import Quox.EffExtra
 
 import Data.List1
 import Data.Maybe
+import Data.Either
 
 %default total
 
@@ -527,7 +528,7 @@ namespace Elim
   EqualElim : List (Type -> Type)
   EqualElim = InnerErrEff :: EqualInner
 
-  private covering
+  private covering %inline
   computeElimTypeE : (defs : Definitions) -> (ctx : EqContext n) ->
                      (sg : SQty) ->
                      (e : Elim 0 n) -> (0 ne : NotRedexEq defs ctx sg e) =>
@@ -535,14 +536,18 @@ namespace Elim
   computeElimTypeE defs ectx sg e = lift $
     computeElimType defs (toWhnfContext ectx) sg e
 
-  private
+  private %inline
   putError : Has InnerErrEff fs => Error -> Eff fs ()
   putError err = modifyAt InnerErr (<|> Just err)
 
-  private
+  private %inline
   try : Eff EqualInner () -> Eff EqualElim ()
   try act = lift $ catch putError $ lift act {fs' = EqualElim}
 
+  private %inline
+  nested : Eff EqualInner a -> Eff EqualElim (Either Error a)
+  nested act = lift $ runExcept act
+
   private covering %inline
   clashE : (defs : Definitions) -> (ctx : EqContext n) -> (sg : SQty) ->
            (e, f : Elim 0 n) -> (0 nf : NotRedexEq defs ctx sg f) =>
@@ -580,6 +585,52 @@ namespace Elim
                    (0 nf : NotRedexEq defs ctx sg f) ->
                    Eff EqualElim (Term 0 n)
 
+  -- (no neutral dim apps or comps in a closed dctx)
+  compare0Inner' _ _ _ (DApp _ (K {}) _) _ ne _ =
+    void $ absurd $ noOr2 $ noOr2 ne
+  compare0Inner' _ _ _ _ (DApp _ (K {}) _) _ nf =
+    void $ absurd $ noOr2 $ 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
+
+  --  Ψ | Γ ⊢ A‹p₁/𝑖› <: B‹p₂/𝑖›
+  --  Ψ | Γ ⊢ A‹q₁/𝑖› <: B‹q₂/𝑖›
+  --  Ψ | Γ ⊢ s <: t ⇐ B‹p₂/𝑖›
+  -- -----------------------------------------------------------
+  --  Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ s
+  --       <: coe [𝑖 ⇒ B] @p₂ @q₂ t ⇒ B‹q₂/𝑖›
+  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 sg ty_p val1 val2
+    pure $ ty_q
+
+  -- an adaptation of the rule
+  --
+  --  Ψ | Γ ⊢ A‹0/𝑖› = A‹1/𝑖› ⇐ ★
+  -- -----------------------------------------------------
+  --  Ψ | Γ ⊢ coe (𝑖 ⇒ A) @p @q s ⇝ (s ∷ A‹1/𝑖›) ⇒ A‹1/𝑖›
+  --
+  -- it's here so that whnf doesn't have to depend on the equality checker
+  compare0Inner' defs ctx sg (Coe ty p q val loc) f _ _ = do
+    tyEq <- nested $ local_ Equal $ compareType defs ctx ty.zero ty.one
+    if isRight tyEq
+       then compare0Inner defs ctx sg (Ann val (dsub1 ty q) loc) f
+       else clashE defs ctx sg (Coe ty p q val loc) f
+
+  -- symmetric version of the above
+  compare0Inner' defs ctx sg e (Coe ty p q val loc) _ _ = do
+    tyEq <- nested $ local_ Equal $ compareType defs ctx ty.zero ty.one
+    if isRight tyEq
+       then compare0Inner defs ctx sg e (Ann val (dsub1 ty q) loc)
+       else clashE defs ctx sg e (Coe ty p q val loc)
+
   compare0Inner' defs ctx sg e@(F {}) f _ _ = do
     if e == f then computeElimTypeE defs ctx sg f
               else clashE defs ctx sg e f
@@ -711,12 +762,6 @@ namespace Elim
       pure $ sub1 eret e
   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
-
   --  Ψ | Γ ⊢ s <: t : B
   -- --------------------------------
   --  Ψ | Γ ⊢ (s ∷ A) <: (t ∷ B) ⇒ B
@@ -727,29 +772,6 @@ namespace Elim
     try $ Term.compare0 defs ctx sg ty s t
     pure ty
 
-  --  Ψ | Γ ⊢ A‹p₁/𝑖› <: B‹p₂/𝑖›
-  --  Ψ | Γ ⊢ A‹q₁/𝑖› <: B‹q₂/𝑖›
-  --  Ψ | Γ ⊢ s <: t ⇐ B‹p₂/𝑖›
-  -- -----------------------------------------------------------
-  --  Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ s
-  --       <: coe [𝑖 ⇒ B] @p₂ @q₂ t ⇒ B‹q₂/𝑖›
-  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 sg ty_p val1 val2
-    pure $ ty_q
-  compare0Inner' defs ctx sg e@(Coe {}) f _ _ = clashE defs ctx sg e f
-
-  -- (no neutral compositions in a closed dctx)
-  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 sg (TypeCase ty1 ret1 arms1 def1 eloc)
                              (TypeCase ty2 ret2 arms2 def2 floc) ne _ =