From f0d3529f63a10aae7aa571524d6ec3e6d605f7f3 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Thu, 22 Jun 2023 22:20:12 +0200
Subject: [PATCH] fix subtype stuff for Eq

---
 lib/Quox/Equal.idr | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index d4f9890..5efdcb3 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -347,9 +347,10 @@ parameters (defs : Definitions)
       --    Γ ⊢ Eq [i ⇒ A₁] l₁ r₂ <: Eq [i ⇒ A₂] l₂ r₂
       compareType (extendDim sTy.name Zero ctx) sTy.zero tTy.zero
       compareType (extendDim sTy.name One  ctx) sTy.one  tTy.one
+      let ty = case !mode of Super => sTy; _ => tTy
       local_ Equal $ do
-        Term.compare0 ctx sTy.zero sl tl
-        Term.compare0 ctx sTy.one  sr tr
+        Term.compare0 ctx ty.zero sl tl
+        Term.compare0 ctx ty.one  sr tr
 
     compareType' ctx s@(Enum tags1 {}) t@(Enum tags2 {}) = do
       -- ------------------