From d5d30ee1984c71ba246976d8f78d386b7aa715b1 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 28 Aug 2023 20:03:06 +0200
Subject: [PATCH] loosen pushCoe's type slightly

---
 lib/Quox/Whnf/Coercion.idr | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/lib/Quox/Whnf/Coercion.idr b/lib/Quox/Whnf/Coercion.idr
index f3faadd..3e6d8a4 100644
--- a/lib/Quox/Whnf/Coercion.idr
+++ b/lib/Quox/Whnf/Coercion.idr
@@ -97,8 +97,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
   boxCoe qty sty@(S [< i] ty) p q val ret body loc = do
     -- caseπ (coe [i ⇒ [ρ. A]] @p @q s) return z ⇒ C of { [a] ⇒ e }
     -- ⇝
-    -- caseπ s ∷ [ρ. A]‹p/i› return z ⇒ C
-    -- of { [a] ⇒ e[(coe [i ⇒ A] p q a)/a] }
+    -- caseπ s ∷ [ρ. A]‹p/i› return z ⇒ C of { [a] ⇒ e[(coe [i ⇒ A] p q a)/a] }
     let ctx1 = extendDim i ctx
     Element ty tynf <- whnf defs ctx1 ty.term
     ta <- tycaseBOX defs ctx1 ty
@@ -110,9 +109,8 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
   ||| pushes a coercion inside a whnf-ed term
   export covering
   pushCoe : BindName ->
-            (ty : Term (S d) n) ->
-            (p, q : Dim d) -> (0 npq : Not (p `Eqv` q)) =>
-            (s : Term d n) -> (0 pc : So (canPushCoe ty s)) => Loc ->
+            (ty : Term (S d) n) -> (p, q : Dim d) -> (s : Term d n) -> Loc ->
+            (0 pc : So (canPushCoe ty s)) =>
             Eff Whnf (NonRedex Elim d n defs)
   pushCoe i ty p q s loc =
     case ty of