add test for regularity

lib/Quox/Equal.idr

@@ -611,16 +611,24 @@ namespace Elim
       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
+  -- 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 Elim.compare0Inner defs ctx sg (Ann val (dsub1 ty q) loc) f
+       then 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
+  -- 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 Elim.compare0Inner defs ctx sg e (Ann val (dsub1 ty q) loc)
+       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