From 924fd991f9741e2d5f77e398e213b42de5ee34dc Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sat, 1 Apr 2023 16:02:02 +0200
Subject: [PATCH] fix equality types

---
 lib/Quox/Typechecker.idr    |  4 ++--
 tests/Tests/Typechecker.idr | 21 +++++++++++++++++++++
 2 files changed, 23 insertions(+), 2 deletions(-)

diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index f3a966a..e5126bf 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -257,9 +257,9 @@ parameters {auto _ : IsQty q}
       Y t' => checkTypeC (extendDim t.name ctx) t' u
       N t' => checkTypeC ctx                    t' u
     -- if Ψ | Γ ⊢₀ l ⇐ A‹0›
-    check0 ctx t.zero l
+    check0 ctx l t.zero
     -- if Ψ | Γ ⊢₀ r ⇐ A‹1›
-    check0 ctx t.one  r
+    check0 ctx r t.one
     -- then Ψ | Γ ⊢₀ Eq [i ⇒ A] l r ⇐ Type ℓ
 
   checkType' ctx t@(DLam {}) u =
diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr
index 202287a..eb99ca8 100644
--- a/tests/Tests/Typechecker.idr
+++ b/tests/Tests/Typechecker.idr
@@ -370,6 +370,27 @@ tests = "typechecker" :- [
           singleton "ff" (Tag "tt"))
   ],
 
+  "equality types" :- [
+    testTC "0 · ℕ = ℕ : ★₀ ⇐ ★₁" $
+      check_ empty szero (Eq0 (TYPE 0) Nat Nat) (TYPE 1),
+    testTC "0 · ℕ = ℕ : ★₀ ⇐ ★₂" $
+      check_ empty szero (Eq0 (TYPE 0) Nat Nat) (TYPE 2),
+    testTC "0 · ℕ = ℕ : ★₁ ⇐ ★₂" $
+      check_ empty szero (Eq0 (TYPE 1) Nat Nat) (TYPE 2),
+    testTCFail "0 · ℕ = ℕ : ★₁ ⇍ ★₁" $
+      check_ empty szero (Eq0 (TYPE 1) Nat Nat) (TYPE 1),
+    testTC "ab : A ≡ B : ★₀, x : A, y : B ⊢ Eq [i ⇒ ab i] x y ⇐ ★₀" $
+      check_ (ctx [< ("ab", Eq0 (TYPE 0) (FT "A") (FT "B")),
+                     ("x", FT "A"), ("y", FT "B")]) szero
+        (Eq (SY [< "i"] $ E $ BV 2 :% BV 0) (BVT 1) (BVT 0))
+        (TYPE 0),
+    testTCFail "ab : A ≡ B : ★₀, x : A, y : B ⊢ Eq [i ⇒ ab i] y x ⇍ ★₀" $
+      check_ (ctx [< ("ab", Eq0 (TYPE 0) (FT "A") (FT "B")),
+                     ("x", FT "A"), ("y", FT "B")]) szero
+        (Eq (SY [< "i"] $ E $ BV 2 :% BV 0) (BVT 0) (BVT 1))
+        (TYPE 0)
+  ],
+
   "equalities" :- [
     testTC "1 · (δ i ⇒ a) ⇐ a ≡ a" $
       check_ empty sone (DLam $ SN $ FT "a")