From 92ac4a0d05f3037c32c1e34615c21e7455873334 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 15 Apr 2024 22:40:20 +0200
Subject: [PATCH] add coercion regularity directly

---
 lib/Quox/Equal.idr | 78 +++++++++++++++++++++++++++-------------------
 1 file changed, 46 insertions(+), 32 deletions(-)

diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index 796b6ff..0188ca3 100644
--- a/lib/Quox/Equal.idr
+++ b/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,44 @@ 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
+
+  compare0Inner' defs ctx sg (Coe ty p q val loc) f ne nf = do
+    tyEq <- nested $ local_ Equal $ compareType defs ctx ty.zero ty.one
+    if isRight tyEq
+       then Elim.compare0Inner defs ctx sg (Ann val (dsub1 ty q) loc) f
+       else clashE defs ctx sg (Coe ty p q val loc) f
+
+  compare0Inner' defs ctx sg e (Coe ty p q val loc) ne nf = do
+    tyEq <- nested $ local_ Equal $ compareType defs ctx ty.zero ty.one
+    if isRight tyEq
+       then Elim.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 +754,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 +764,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 _ =