From a24ebe070298e71157fd45d3c6ba46b282961159 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Thu, 24 Aug 2023 17:45:37 +0200
Subject: [PATCH] tycasePi etc don't actually need a scope of (S d)

---
 lib/Quox/Reduce.idr | 27 ++++++++++++---------------
 1 file changed, 12 insertions(+), 15 deletions(-)

diff --git a/lib/Quox/Reduce.idr b/lib/Quox/Reduce.idr
index 460d951..4525b93 100644
--- a/lib/Quox/Reduce.idr
+++ b/lib/Quox/Reduce.idr
@@ -261,11 +261,8 @@ coeScoped ty p q loc (S names (N body)) =
   S names $ N $ E $ Coe ty p q body loc
 
 
-export covering
-CanWhnf Term Reduce.isRedexT
-
-export covering
-CanWhnf Elim Reduce.isRedexE
+export covering CanWhnf Term Reduce.isRedexT
+export covering CanWhnf Elim Reduce.isRedexE
 
 parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
   ||| performs the minimum work required to recompute the type of an elim.
@@ -295,13 +292,14 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
   computeElimType (Comp {ty, _}) = pure ty
   computeElimType (TypeCase {ret, _}) = pure ret
 
-parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
+
+parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
   ||| for π.(x : A) → B, returns (A, B);
   ||| for an elim returns a pair of type-cases that will reduce to that;
   ||| for other intro forms error
   private covering
-  tycasePi : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
-             Eff Whnf (Term (S d) n, ScopeTerm (S d) n)
+  tycasePi : (t : Term d n) -> (0 tnf : No (isRedexT defs t)) =>
+             Eff Whnf (Term d n, ScopeTerm d n)
   tycasePi (Pi {arg, res, _}) = pure (arg, res)
   tycasePi (E e) {tnf} = do
     ty <- computeElimType defs ctx e @{noOr2 tnf}
@@ -318,8 +316,8 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
   ||| for an elim returns a pair of type-cases that will reduce to that;
   ||| for other intro forms error
   private covering
-  tycaseSig : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
-              Eff Whnf (Term (S d) n, ScopeTerm (S d) n)
+  tycaseSig : (t : Term d n) -> (0 tnf : No (isRedexT defs t)) =>
+              Eff Whnf (Term d n, ScopeTerm d n)
   tycaseSig (Sig {fst, snd, _}) = pure (fst, snd)
   tycaseSig (E e) {tnf} = do
     ty <- computeElimType defs ctx e @{noOr2 tnf}
@@ -336,8 +334,8 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
   ||| for an elim returns a type-case that will reduce to that;
   ||| for other intro forms error
   private covering
-  tycaseBOX : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
-              Eff Whnf (Term (S d) n)
+  tycaseBOX : (t : Term d n) -> (0 tnf : No (isRedexT defs t)) =>
+              Eff Whnf (Term d n)
   tycaseBOX (BOX {ty, _}) = pure ty
   tycaseBOX (E e) {tnf} = do
     ty <- computeElimType defs ctx e @{noOr2 tnf}
@@ -348,9 +346,8 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
   ||| for an elim returns five type-cases that will reduce to that;
   ||| for other intro forms error
   private covering
-  tycaseEq : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
-             Eff Whnf (Term (S d) n, Term (S d) n, DScopeTerm (S d) n,
-                       Term (S d) n, Term (S d) n)
+  tycaseEq : (t : Term d n) -> (0 tnf : No (isRedexT defs t)) =>
+             Eff Whnf (Term d n, Term d n, DScopeTerm d n, Term d n, Term d n)
   tycaseEq (Eq {ty, l, r, _}) = pure (ty.zero, ty.one, ty, l, r)
   tycaseEq (E e) {tnf} = do
     ty <- computeElimType defs ctx e @{noOr2 tnf}