.gitignore

@@ -5,5 +5,5 @@ result
 *~
 quox
 quox-tests
-quox-golden-tests/tests/*/output
-quox-golden-tests/tests/*/*.ss
+golden-tests/tests/*/output
+golden-tests/tests/*/*.ss

golden-tests/tests/regularity/expected

@@ -0,0 +1 @@
+0.reggie : 1.(A : ★) → 1.(AA : A ≡ A : ★) → 1.(s : A) → 1.(P : 1.A → ★) → 1.(P (coe (𝑖 ⇒ AA @𝑖) @0 @1 s)) → P s

golden-tests/tests/regularity/regularity.quox

@@ -0,0 +1,12 @@
+-- this definition depends on coercion regularity in xtt. which is this
+-- (adapted to quox):
+--
+--           Ψ | Γ ⊢ 0 · A‹0/𝑖› = A‹1/𝑖› ⇐ ★
+-- ---------------------------------------------------------
+--  Ψ | Γ ⊢ π · coe (𝑖 ⇒ A) @p @q s ⇝ (s ∷ A‹1/𝑖›) ⇒ A‹1/𝑖›
+--
+-- otherwise, the types P (coe ⋯ s) and P s are incompatible
+
+def0 reggie : (A : ★) → (AA : A ≡ A : ★) → (s : A) →
+              (P : A → ★) → P (coe (𝑖 ⇒ AA @𝑖) s) → P s =
+  λ A AA s P p ⇒ p

golden-tests/tests/regularity/run

@@ -0,0 +1,2 @@
+. ../lib.sh
+check "$1" regularity.quox

lib/Quox/Equal.idr

@@ -8,6 +8,7 @@ import Quox.EffExtra
 
 import Data.List1
 import Data.Maybe
+import Data.Either
 
 %default total
 
@@ -29,6 +30,10 @@ export %inline
 mode : Has EqModeState fs => Eff fs EqMode
 mode = get
 
+private %inline
+withEqual : Has EqModeState fs => Eff fs a -> Eff fs a
+withEqual = local_ Equal
+
 
 parameters (loc : Loc) (ctx : EqContext n)
   private %inline
@@ -241,7 +246,7 @@ namespace Term
       (E _, _)   => wrongType t.loc ctx ty t
       _          => wrongType s.loc ctx ty s
 
-  compare0' defs ctx sg ty@(Pi {qty, arg, res, _}) s t = local_ Equal $
+  compare0' defs ctx sg ty@(Pi {qty, arg, res, _}) s t = withEqual $
     --              Γ ⊢ A empty
     -- -------------------------------------------
     --  Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) ⇐ (π·x : A) → B
@@ -275,7 +280,7 @@ namespace Term
     eta loc e (S _ (N _)) = clashT loc ctx ty s t
     eta _   e (S _ (Y b)) = compare0 defs ctx' sg res.term (toLamBody e) b
 
-  compare0' defs ctx sg ty@(Sig {fst, snd, _}) s t = local_ Equal $
+  compare0' defs ctx sg ty@(Sig {fst, snd, _}) s t = withEqual $
     case (s, t) of
       --  Γ ⊢ s₁ = t₁ ⇐ A     Γ ⊢ s₂ = t₂ ⇐ B{s₁/x}
       -- --------------------------------------------
@@ -301,7 +306,7 @@ namespace Term
           compare0 defs ctx sg (sub1 snd (Ann s fst s.loc)) (E $ Snd e e.loc) t
         SOne => clashT loc ctx ty s t
 
-  compare0' defs ctx sg ty@(Enum cases _) s t = local_ Equal $
+  compare0' defs ctx sg ty@(Enum cases _) s t = withEqual $
     -- η for empty & singleton enums
     if length (SortedSet.toList cases) <= 1 then pure () else
     case (s, t) of
@@ -326,7 +331,7 @@ namespace Term
     --  Γ ⊢ e = f ⇐ Eq [i ⇒ A] s t
     pure ()
 
-  compare0' defs ctx sg nat@(NAT {}) s t = local_ Equal $
+  compare0' defs ctx sg nat@(NAT {}) s t = withEqual $
     case (s, t) of
       -- ---------------
       --  Γ ⊢ n = n ⇐ ℕ
@@ -353,7 +358,7 @@ namespace Term
       (E _,     t) => wrongType t.loc ctx nat t
       (s,       _) => wrongType s.loc ctx nat s
 
-  compare0' defs ctx sg str@(STRING {}) s t = local_ Equal $
+  compare0' defs ctx sg str@(STRING {}) s t = withEqual $
     case (s, t) of
       (Str x _, Str y _) => unless (x == y) $ clashT s.loc ctx str s t
 
@@ -366,7 +371,7 @@ namespace Term
       (E _,    _) => wrongType t.loc ctx str t
       _           => wrongType s.loc ctx str s
 
-  compare0' defs ctx sg bty@(BOX q ty {}) s t = local_ Equal $
+  compare0' defs ctx sg bty@(BOX q ty {}) s t = withEqual $
     case (s, t) of
       --     Γ ⊢ s = t ⇐ A
       -- -----------------------
@@ -444,7 +449,7 @@ compareType' defs ctx (Eq {ty = sTy, l = sl, r = sr, _})
   compareType defs (extendDim sTy.name Zero ctx) sTy.zero tTy.zero
   compareType defs (extendDim sTy.name One  ctx) sTy.one  tTy.one
   ty <- bigger sTy tTy
-  local_ Equal $ do
+  withEqual $ do
     Term.compare0 defs ctx SZero ty.zero sl tl
     Term.compare0 defs ctx SZero ty.one  sr tr
 
@@ -527,7 +532,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 +540,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
+  succeeds : Eff EqualInner a -> Eff EqualElim Bool
+  succeeds act = lift $ map isRight $ 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 +589,50 @@ 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 _ _ =
+    if !(succeeds $ withEqual $ compareType defs ctx ty.zero ty.one)
+       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) _ _ =
+    if !(succeeds $ withEqual $ compareType defs ctx ty.zero ty.one)
+       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
@@ -608,7 +661,7 @@ namespace Elim
   --          = caseπ f return R of { (x, y) ⇒ t } ⇒ Q[e/p]
   compare0Inner' defs ctx sg (CasePair epi e eret ebody eloc)
                              (CasePair fpi f fret fbody floc) ne nf =
-    local_ Equal $ do
+    withEqual $ do
       ety <- compare0Inner defs ctx sg e f
       (fst, snd) <- expectSig defs ctx sg eloc ety
       let [< x, y] = ebody.names
@@ -627,7 +680,7 @@ namespace Elim
   -- ------------------------------
   --  Ψ | Γ ⊢ fst e = fst f ⇒ A
   compare0Inner' defs ctx sg (Fst e eloc) (Fst f floc) ne nf =
-    local_ Equal $ do
+    withEqual $ do
       ety <- compare0Inner defs ctx sg e f
       fst <$> expectSig defs ctx sg eloc ety
   compare0Inner' defs ctx sg e@(Fst {}) f _ _ =
@@ -637,7 +690,7 @@ namespace Elim
   -- ------------------------------------
   --  Ψ | Γ ⊢ snd e = snd f ⇒ B[fst e/x]
   compare0Inner' defs ctx sg (Snd e eloc) (Snd f floc) ne nf =
-    local_ Equal $ do
+    withEqual $ do
       ety <- compare0Inner defs ctx sg e f
       (_, tsnd) <- expectSig defs ctx sg eloc ety
       pure $ sub1 tsnd (Fst e eloc)
@@ -652,7 +705,7 @@ namespace Elim
   --        = caseπ f return R of { '𝐚ᵢ ⇒ tᵢ } ⇒ Q[e/x]
   compare0Inner' defs ctx sg (CaseEnum epi e eret earms eloc)
                              (CaseEnum fpi f fret farms floc) ne nf =
-    local_ Equal $ do
+    withEqual $ do
       ety <- compare0Inner defs ctx sg e f
       try $
         compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term
@@ -675,7 +728,7 @@ namespace Elim
   --        ⇒ Q[e/x]
   compare0Inner' defs ctx sg (CaseNat epi epi' e eret ezer esuc eloc)
                              (CaseNat fpi fpi' f fret fzer fsuc floc) ne nf =
-    local_ Equal $ do
+    withEqual $ do
       ety <- compare0Inner defs ctx sg e f
       let [< p, ih] = esuc.names
       try $ do
@@ -699,7 +752,7 @@ namespace Elim
   --        = caseπ f return R of { [x] ⇒ t } ⇒ Q[e/x]
   compare0Inner' defs ctx sg (CaseBox epi e eret ebody eloc)
                              (CaseBox fpi f fret fbody floc) ne nf =
-    local_ Equal $ do
+    withEqual $ do
       ety <- compare0Inner defs ctx sg e f
       (q, ty) <- expectBOX defs ctx sg eloc ety
       try $ do
@@ -711,12 +764,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,34 +774,11 @@ 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 _ =
     case sg `decEq` SZero of
-      Yes Refl => local_ Equal $ do
+      Yes Refl => withEqual $ do
         ety <- compare0Inner defs ctx SZero ty1 ty2
         u   <- expectTYPE defs ctx SZero eloc ety
         try $ do