From 4db373a84fcaa5e48af70a3becffa89f8d97ea02 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 17 Apr 2023 21:55:12 +0200
Subject: [PATCH] =?UTF-8?q?use=20constraints=20when=20checking=20=CE=B4?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

when checking δ 𝑖 ⇒ s, add 𝑖=ε to Ψ instead of checking s‹ε/𝑖›.
this has the same effect but an error message will show "𝑖, 𝑖=ε" in
the context
---
 lib/Quox/Typechecker.idr | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index 9d337d4..1c2199b 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -196,12 +196,15 @@ mutual
 
   check' ctx sg (DLam body) ty = do
     (ty, l, r) <- expectEq !ask ctx ty
+    let ctx' = extendDim body.name ctx
+        ty   = ty.term
+        body = body.term
     -- if Ψ, i | Γ ⊢ σ · t ⇐ A ⊳ Σ
-    qout <- checkC (extendDim body.name ctx) sg body.term ty.term
-    -- if Ψ | Γ ⊢ t‹0› = l : A‹0›
-    equal ctx ty.zero body.zero l
-    -- if Ψ | Γ ⊢ t‹1› = r : A‹1›
-    equal ctx ty.one body.one  r
+    qout <- checkC ctx' sg body ty
+    -- if Ψ, i, i = 0 | Γ ⊢ t = l : A
+    equal (eqDim (BV 0) (K Zero) ctx') ty body (dweakT 1 l)
+    -- if Ψ, i, i = 1 | Γ ⊢ t = r : A
+    equal (eqDim (BV 0) (K One)  ctx') ty body (dweakT 1 r)
     -- then Ψ | Γ ⊢ σ · (δ i ⇒ t) ⇐ Eq [i ⇒ A] l r ⊳ Σ
     pure qout