From fae534dae0fb624c9057796336933b4f2593bfd0 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 26 Mar 2023 14:38:37 +0200
Subject: [PATCH] tweaks in equality checking

---
 lib/Quox/Equal.idr | 44 +++++++++++++++++++++++++-------------------
 1 file changed, 25 insertions(+), 19 deletions(-)

diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index e84e18a..61635b7 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -40,6 +40,10 @@ parameters {auto _ : CanEqual q m} (ctx : EqContext q n)
   clashE : Elim q 0 n -> Elim q 0 n -> m a
   clashE e f = throwError $ ClashE ctx !mode e f
 
+  private %inline
+  wrongType : Term q 0 n -> Term q 0 n -> m a
+  wrongType ty s = throwError $ WrongType ctx ty s
+
 
 ||| true if a term is syntactically a type, or is neutral.
 |||
@@ -161,9 +165,9 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
 
           (E e, E f) => Elim.compare0 ctx e f
 
-          (Lam _, t) => throwError $ WrongType ctx ty t
-          (E _,   t) => throwError $ WrongType ctx ty t
-          (s,     _) => throwError $ WrongType ctx ty s
+          (Lam _, t) => wrongType ctx ty t
+          (E _,   t) => wrongType ctx ty t
+          (s,     _) => wrongType ctx ty s
         where
           ctx' : EqContext q (S n)
           ctx' = extendTy qty res.name arg ctx
@@ -185,9 +189,12 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
 
           (E e, E f) => Elim.compare0 ctx e f
 
-          (Pair {}, t) => throwError $ WrongType ctx ty t
-          (E _,     t) => throwError $ WrongType ctx ty t
-          (s,       _) => throwError $ WrongType ctx ty s
+          (Pair {}, E _)     => clashT ctx ty s t
+          (E _,     Pair {}) => clashT ctx ty s t
+
+          (Pair {}, t) => wrongType ctx ty t
+          (E _,     t) => wrongType ctx ty t
+          (s,       _) => wrongType ctx ty s
 
       compare0' ctx ty@(Enum tags) s t = local {mode := Equal} $
         case (s, t) of
@@ -198,9 +205,12 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
           (Tag t1, Tag t2) => unless (t1 == t2) $ clashT ctx ty s t
           (E e,    E f)    => Elim.compare0 ctx e f
 
-          (Tag _, t) => throwError $ WrongType ctx ty t
-          (E _,   t) => throwError $ WrongType ctx ty t
-          (s,     _) => throwError $ WrongType ctx ty s
+          (Tag _, E _)   => clashT ctx ty s t
+          (E _,   Tag _) => clashT ctx ty s t
+
+          (Tag _, t) => wrongType ctx ty t
+          (E _,   t) => wrongType ctx ty t
+          (s,     _) => wrongType ctx ty s
 
       compare0' _ (Eq {}) _ _ =
         -- ✨ uip ✨
@@ -211,8 +221,8 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
       compare0' ctx ty@(E _) s t = do
         -- a neutral type can only be inhabited by neutral values
         -- e.g. an abstract value in an abstract type, bound variables, …
-        E e <- pure s | _ => throwError $ WrongType ctx ty s
-        E f <- pure t | _ => throwError $ WrongType ctx ty t
+        E e <- pure s | _ => wrongType ctx ty s
+        E f <- pure t | _ => wrongType ctx ty t
         Elim.compare0 ctx e f
 
     ||| compares two types, using the current variance `mode` for universes.
@@ -295,20 +305,16 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
     computeElimType ctx (F x) _ = do
       defs <- lookupFree' defs x
       pure $ injectT ctx defs.type
-    computeElimType ctx (B i) _ = do
-      pure $ ctx.tctx !! i
+    computeElimType ctx (B i) _ = pure $ ctx.tctx !! i
     computeElimType ctx (f :@ s) ne = do
       (_, arg, res) <- expectPiE defs ctx !(computeElimType ctx f (noOr1 ne))
       pure $ sub1 res (s :# arg)
-    computeElimType ctx (CasePair {pair, ret, _}) _ = do
-      pure $ sub1 ret pair
-    computeElimType ctx (CaseEnum {tag, ret, _}) _ = do
-      pure $ sub1 ret tag
+    computeElimType ctx (CasePair {pair, ret, _}) _ = pure $ sub1 ret pair
+    computeElimType ctx (CaseEnum {tag, ret, _}) _ = pure $ sub1 ret tag
     computeElimType ctx (f :% p) ne = do
       (ty, _, _) <- expectEqE defs ctx !(computeElimType ctx f (noOr1 ne))
       pure $ dsub1 ty p
-    computeElimType ctx (_ :# ty) _ = do
-      pure ty
+    computeElimType ctx (_ :# ty) _ = pure ty
 
     private covering
     replaceEnd : EqContext q n ->