From f3376258013e5f4eaa05208be41f643823e260eb Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 27 Nov 2023 21:01:36 +0100
Subject: [PATCH] remove most noLocs

---
 lib/Quox/FreeVars.idr           |  16 +--
 lib/Quox/Loc.idr                |  18 +++
 lib/Quox/Parser/FromParser.idr  |   2 +-
 lib/Quox/Scoped.idr             |  19 +++
 lib/Quox/Syntax/DimEq.idr       |  10 +-
 lib/Quox/Syntax/Subst.idr       |  12 +-
 lib/Quox/Syntax/Term/Base.idr   | 205 +++++++++++++++-----------------
 lib/Quox/Syntax/Term/Pretty.idr |   2 +-
 lib/Quox/Syntax/Term/Subst.idr  |  10 +-
 lib/Quox/Typechecker.idr        |   2 +-
 lib/Quox/Typing.idr             |   2 +-
 lib/Quox/Typing/Context.idr     |   2 +-
 lib/Quox/Untyped/Syntax.idr     |  11 +-
 lib/Quox/Var.idr                |   3 -
 lib/Quox/Whnf/Coercion.idr      |  11 +-
 lib/Quox/Whnf/TypeCase.idr      |  14 +--
 16 files changed, 178 insertions(+), 161 deletions(-)

diff --git a/lib/Quox/FreeVars.idr b/lib/Quox/FreeVars.idr
index 29c08ca..de52813 100644
--- a/lib/Quox/FreeVars.idr
+++ b/lib/Quox/FreeVars.idr
@@ -229,27 +229,27 @@ HasFreeVars (Elim d) where
 
 
 private
-expandDShift : {d1 : Nat} -> Shift d1 d2 -> Context' (Dim d2) d1
-expandDShift by = tabulateLT d1 (\i => BV i noLoc // by)
+expandDShift : {d1 : Nat} -> Shift d1 d2 -> Loc -> Context' (Dim d2) d1
+expandDShift by loc = tabulateLT d1 (\i => BV i loc // by)
 
 private
-expandDSubst : {d1 : Nat} -> DSubst d1 d2 -> Context' (Dim d2) d1
-expandDSubst (Shift by) = expandDShift by
-expandDSubst (t ::: th) = expandDSubst th :< t
+expandDSubst : {d1 : Nat} -> DSubst d1 d2 -> Loc -> Context' (Dim d2) d1
+expandDSubst (Shift by) loc = expandDShift by loc
+expandDSubst (t ::: th) loc = expandDSubst th loc :< t
 
 
 private
-fdvSubst' : {d1, d2, n : Nat} -> HasFreeDVars tm =>
+fdvSubst' : {d1, d2, n : Nat} -> (Located2 tm, HasFreeDVars tm) =>
             tm d1 n -> DSubst d1 d2 -> FreeVars d2
 fdvSubst' t th =
-  fold $ zipWith maybeOnly (fdv t).vars (expandDSubst th)
+  fold $ zipWith maybeOnly (fdv t).vars (expandDSubst th t.loc)
 where
   maybeOnly : {d : Nat} -> Bool -> Dim d -> FreeVars d
   maybeOnly True (B i _) = only i
   maybeOnly _    _       = none
 
 private
-fdvSubst : {d, n : Nat} -> HasFreeDVars tm =>
+fdvSubst : {d, n : Nat} -> (Located2 tm, HasFreeDVars tm) =>
            WithSubst (\d => tm d n) Dim d -> FreeVars d
 fdvSubst (Sub t th) = let Val from = getFrom th in fdvSubst' t th
 
diff --git a/lib/Quox/Loc.idr b/lib/Quox/Loc.idr
index 5776ec9..7aeb229 100644
--- a/lib/Quox/Loc.idr
+++ b/lib/Quox/Loc.idr
@@ -118,6 +118,11 @@ export %inline
 or : Loc -> Loc -> Loc
 or (L l1) (L l2) = L $ l1 `or_` l2
 
+export %inline
+extendOr : Loc -> Loc -> Loc
+extendOr l1 l2 = (l1 `extendL` l2) `or` l2
+
+
 
 public export
 interface Located a where (.loc) : a -> Loc
@@ -126,9 +131,22 @@ public export
 0 Located1 : (a -> Type) -> Type
 Located1 f = forall x. Located (f x)
 
+public export
+0 Located2 : (a -> b -> Type) -> Type
+Located2 f = forall x, y. Located (f x y)
+
 public export
 interface Located a => Relocatable a where setLoc : Loc -> a -> a
 
 public export
 0 Relocatable1 : (a -> Type) -> Type
 Relocatable1 f = forall x. Relocatable (f x)
+
+public export
+0 Relocatable2 : (a -> b -> Type) -> Type
+Relocatable2 f = forall x, y. Relocatable (f x y)
+
+
+export
+locs : Located a => Foldable t => t a -> Loc
+locs = foldl (\loc, y => loc `extendOr` y.loc) noLoc
diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr
index 42b8d57..ce22ae2 100644
--- a/lib/Quox/Parser/FromParser.idr
+++ b/lib/Quox/Parser/FromParser.idr
@@ -302,7 +302,7 @@ mutual
                     Eff FromParserPure (DScopeTermN s d n)
   fromPTermDScope ds ns xs t =
     if all isUnused xs then
-      SN <$> fromPTermWith ds ns t
+      SN {f = \d => Term d n} <$> fromPTermWith ds ns t
     else
       DST (fromSnocVect $ map fromPatVar xs) <$> fromPTermWith (ds ++ xs) ns t
 
diff --git a/lib/Quox/Scoped.idr b/lib/Quox/Scoped.idr
index be43cfe..ea575cf 100644
--- a/lib/Quox/Scoped.idr
+++ b/lib/Quox/Scoped.idr
@@ -38,3 +38,22 @@ export %inline
 export %inline %hint
 ShowScoped : (forall n. Show (f n)) => Show (Scoped s f n)
 ShowScoped = deriveShow
+
+
+||| scope which ignores all its binders
+public export %inline
+SN : Located1 f => {s : Nat} -> f n -> Scoped s f n
+SN body = S (replicate s $ BN Unused body.loc) $ N body
+
+||| scope which uses its binders
+public export %inline
+SY : BContext s -> f (s + n) -> Scoped s f n
+SY ns = S ns . Y
+
+public export %inline
+name : Scoped 1 f n -> BindName
+name (S [< x] _) = x
+
+public export %inline
+(.name) : Scoped 1 f n -> BindName
+s.name = name s
diff --git a/lib/Quox/Syntax/DimEq.idr b/lib/Quox/Syntax/DimEq.idr
index 574414f..020b947 100644
--- a/lib/Quox/Syntax/DimEq.idr
+++ b/lib/Quox/Syntax/DimEq.idr
@@ -71,13 +71,13 @@ toMaybe (Just x) = Just x
 
 
 export
-fromGround' : Context' DimConst d -> DimEq' d
-fromGround' [<]        = [<]
-fromGround' (ctx :< e) = fromGround' ctx :< Just (K e noLoc)
+fromGround' : BContext d -> Context' DimConst d -> DimEq' d
+fromGround' [<]       [<]        = [<]
+fromGround' (xs :< x) (ctx :< e) = fromGround' xs ctx :< Just (K e x.loc)
 
 export
-fromGround : Context' DimConst d -> DimEq d
-fromGround = C . fromGround'
+fromGround : BContext d -> Context' DimConst d -> DimEq d
+fromGround = C .: fromGround'
 
 
 public export %inline
diff --git a/lib/Quox/Syntax/Subst.idr b/lib/Quox/Syntax/Subst.idr
index d5c2ed8..aebe6a4 100644
--- a/lib/Quox/Syntax/Subst.idr
+++ b/lib/Quox/Syntax/Subst.idr
@@ -96,18 +96,18 @@ map f (t ::: th) = f t ::: map f th
 
 
 public export %inline
-push : CanSubstSelf f => Subst f from to -> Subst f (S from) (S to)
-push th = fromVar VZ ::: (th . shift 1)
+push : CanSubstSelf f => Loc -> Subst f from to -> Subst f (S from) (S to)
+push loc th = fromVarLoc VZ loc ::: (th . shift 1)
 
 -- [fixme] a better way to do this?
 public export
-pushN : CanSubstSelf f => (s : Nat) ->
+pushN : CanSubstSelf f => (s : Nat) -> Loc ->
         Subst f from to -> Subst f (s + from) (s + to)
-pushN 0     th = th
-pushN (S s) th =
+pushN 0     _   th = th
+pushN (S s) loc th =
   rewrite plusSuccRightSucc s from in
   rewrite plusSuccRightSucc s to in
-  pushN s $ fromVar VZ ::: (th . shift 1)
+  pushN s loc $ fromVarLoc VZ loc ::: (th . shift 1)
 
 public export
 drop1 : Subst f (S from) to -> Subst f from to
diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr
index 36715d4..88e7b07 100644
--- a/lib/Quox/Syntax/Term/Base.idr
+++ b/lib/Quox/Syntax/Term/Base.idr
@@ -236,117 +236,6 @@ mutual
   ShowElim : Show (Elim d n)
   ShowElim = assert_total {a = Show (Elim d n)} deriveShow
 
-||| scope which ignores all its binders
-public export %inline
-SN : {s : Nat} -> f n -> Scoped s f n
-SN = S (replicate s $ BN Unused noLoc) . N
-
-||| scope which uses its binders
-public export %inline
-SY : BContext s -> f (s + n) -> Scoped s f n
-SY ns = S ns . Y
-
-public export %inline
-name : Scoped 1 f n -> BindName
-name (S [< x] _) = x
-
-public export %inline
-(.name) : Scoped 1 f n -> BindName
-s.name = name s
-
-||| more convenient Pi
-public export %inline
-PiY : (qty : Qty) -> (x : BindName) ->
-      (arg : Term d n) -> (res : Term d (S n)) -> (loc : Loc) -> Term d n
-PiY {qty, x, arg, res, loc} = Pi {qty, arg, res = SY [< x] res, loc}
-
-||| more convenient Lam
-public export %inline
-LamY : (x : BindName) -> (body : Term d (S n)) -> (loc : Loc) -> Term d n
-LamY {x, body, loc} = Lam {body = SY [< x] body, loc}
-
-public export %inline
-LamN : (body : Term d n) -> (loc : Loc) -> Term d n
-LamN {body, loc} = Lam {body = SN body, loc}
-
-||| non dependent function type
-public export %inline
-Arr : (qty : Qty) -> (arg, res : Term d n) -> (loc : Loc) -> Term d n
-Arr {qty, arg, res, loc} = Pi {qty, arg, res = SN res, loc}
-
-||| more convenient Sig
-public export %inline
-SigY : (x : BindName) -> (fst : Term d n) ->
-       (snd : Term d (S n)) -> (loc : Loc) -> Term d n
-SigY {x, fst, snd, loc} = Sig {fst, snd = SY [< x] snd, loc}
-
-||| non dependent pair type
-public export %inline
-And : (fst, snd : Term d n) -> (loc : Loc) -> Term d n
-And {fst, snd, loc} = Sig {fst, snd = SN snd, loc}
-
-||| more convenient Eq
-public export %inline
-EqY : (i : BindName) -> (ty : Term (S d) n) ->
-      (l, r : Term d n) -> (loc : Loc) -> Term d n
-EqY {i, ty, l, r, loc} = Eq {ty = SY [< i] ty, l, r, loc}
-
-||| more convenient DLam
-public export %inline
-DLamY : (i : BindName) -> (body : Term (S d) n) -> (loc : Loc) -> Term d n
-DLamY {i, body, loc} = DLam {body = SY [< i] body, loc}
-
-public export %inline
-DLamN : (body : Term d n) -> (loc : Loc) -> Term d n
-DLamN {body, loc} = DLam {body = SN body, loc}
-
-||| non dependent equality type
-public export %inline
-Eq0 : (ty, l, r : Term d n) -> (loc : Loc) -> Term d n
-Eq0 {ty, l, r, loc} = Eq {ty = SN ty, l, r, loc}
-
-||| same as `F` but as a term
-public export %inline
-FT : Name -> Universe -> Loc -> Term d n
-FT x u loc = E $ F x u loc
-
-||| same as `B` but as a term
-public export %inline
-BT : Var n -> (loc : Loc) -> Term d n
-BT i loc = E $ B i loc
-
-||| abbreviation for a bound variable like `BV 4` instead of
-||| `B (VS (VS (VS (VS VZ))))`
-public export %inline
-BV : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Elim d n
-BV i loc = B (V i) loc
-
-||| same as `BV` but as a term
-public export %inline
-BVT : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Term d n
-BVT i loc = E $ BV i loc
-
-public export %inline
-Zero : Loc -> Term d n
-Zero = Nat 0
-
-public export %inline
-enum : List TagVal -> Loc -> Term d n
-enum ts loc = Enum (SortedSet.fromList ts) loc
-
-public export %inline
-typeCase : Elim d n -> Term d n ->
-           List (TypeCaseArm d n) -> Term d n -> Loc -> Elim d n
-typeCase ty ret arms def loc = TypeCase ty ret (fromList arms) def loc
-
-public export %inline
-typeCase1Y : Elim d n -> Term d n ->
-             (k : TyConKind) -> BContext (arity k) -> Term d (arity k + n) ->
-             (loc : Loc) ->
-             {default (NAT loc) def : Term d n} ->
-             Elim d n
-typeCase1Y ty ret k ns body loc = typeCase ty ret [(k ** SY ns body)] def loc
-
 
 export
 Located (Elim d n) where
@@ -463,3 +352,97 @@ Relocatable1 f => Relocatable (ScopedBody s f n) where
 export
 Relocatable1 f => Relocatable (Scoped s f n) where
   setLoc loc (S names body) = S (setLoc loc <$> names) (setLoc loc body)
+
+
+||| more convenient Pi
+public export %inline
+PiY : (qty : Qty) -> (x : BindName) ->
+      (arg : Term d n) -> (res : Term d (S n)) -> (loc : Loc) -> Term d n
+PiY {qty, x, arg, res, loc} = Pi {qty, arg, res = SY [< x] res, loc}
+
+||| more convenient Lam
+public export %inline
+LamY : (x : BindName) -> (body : Term d (S n)) -> (loc : Loc) -> Term d n
+LamY {x, body, loc} = Lam {body = SY [< x] body, loc}
+
+public export %inline
+LamN : (body : Term d n) -> (loc : Loc) -> Term d n
+LamN {body, loc} = Lam {body = SN body, loc}
+
+||| non dependent function type
+public export %inline
+Arr : (qty : Qty) -> (arg, res : Term d n) -> (loc : Loc) -> Term d n
+Arr {qty, arg, res, loc} = Pi {qty, arg, res = SN res, loc}
+
+||| more convenient Sig
+public export %inline
+SigY : (x : BindName) -> (fst : Term d n) ->
+       (snd : Term d (S n)) -> (loc : Loc) -> Term d n
+SigY {x, fst, snd, loc} = Sig {fst, snd = SY [< x] snd, loc}
+
+||| non dependent pair type
+public export %inline
+And : (fst, snd : Term d n) -> (loc : Loc) -> Term d n
+And {fst, snd, loc} = Sig {fst, snd = SN snd, loc}
+
+||| more convenient Eq
+public export %inline
+EqY : (i : BindName) -> (ty : Term (S d) n) ->
+      (l, r : Term d n) -> (loc : Loc) -> Term d n
+EqY {i, ty, l, r, loc} = Eq {ty = SY [< i] ty, l, r, loc}
+
+||| more convenient DLam
+public export %inline
+DLamY : (i : BindName) -> (body : Term (S d) n) -> (loc : Loc) -> Term d n
+DLamY {i, body, loc} = DLam {body = SY [< i] body, loc}
+
+public export %inline
+DLamN : (body : Term d n) -> (loc : Loc) -> Term d n
+DLamN {body, loc} = DLam {body = SN body, loc}
+
+||| non dependent equality type
+public export %inline
+Eq0 : (ty, l, r : Term d n) -> (loc : Loc) -> Term d n
+Eq0 {ty, l, r, loc} = Eq {ty = SN ty, l, r, loc}
+
+||| same as `F` but as a term
+public export %inline
+FT : Name -> Universe -> Loc -> Term d n
+FT x u loc = E $ F x u loc
+
+||| same as `B` but as a term
+public export %inline
+BT : Var n -> (loc : Loc) -> Term d n
+BT i loc = E $ B i loc
+
+||| abbreviation for a bound variable like `BV 4` instead of
+||| `B (VS (VS (VS (VS VZ))))`
+public export %inline
+BV : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Elim d n
+BV i loc = B (V i) loc
+
+||| same as `BV` but as a term
+public export %inline
+BVT : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Term d n
+BVT i loc = E $ BV i loc
+
+public export %inline
+Zero : Loc -> Term d n
+Zero = Nat 0
+
+public export %inline
+enum : List TagVal -> Loc -> Term d n
+enum ts loc = Enum (SortedSet.fromList ts) loc
+
+public export %inline
+typeCase : Elim d n -> Term d n ->
+           List (TypeCaseArm d n) -> Term d n -> Loc -> Elim d n
+typeCase ty ret arms def loc = TypeCase ty ret (fromList arms) def loc
+
+public export %inline
+typeCase1Y : Elim d n -> Term d n ->
+             (k : TyConKind) -> BContext (arity k) -> Term d (arity k + n) ->
+             (loc : Loc) ->
+             {default (NAT loc) def : Term d n} ->
+             Elim d n
+typeCase1Y ty ret k ns body loc = typeCase ty ret [(k ** SY ns body)] def loc
diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index 5a925cf..a5d06b1 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -608,7 +608,7 @@ prettyElim dnames tnames (Coe ty p q val _) =
 
 prettyElim dnames tnames e@(Comp ty p q val r zero one _) =
   parensIfM App =<< do
-    ty   <- prettyTypeLine dnames tnames $ assert_smaller e $ SN ty
+    ty   <- assert_total $ prettyTypeLine dnames tnames $ SN ty
     pq   <- sep <$> sequence [prettyDArg dnames p, prettyDArg dnames q]
     val  <- prettyTArg dnames tnames val
     r    <- prettyDArg dnames r
diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr
index 330a10e..316b2bb 100644
--- a/lib/Quox/Syntax/Term/Subst.idr
+++ b/lib/Quox/Syntax/Term/Subst.idr
@@ -56,12 +56,12 @@ namespace DSubst.DScopeTermN
   (//) : {s : Nat} ->
          DScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
          DScopeTermN s d2 n
-  S ns (Y body) // th = S ns $ Y $ body // pushN s th
+  S ns (Y body) // th = S ns $ Y $ body // pushN s (locs $ toList' ns) th
   S ns (N body) // th = S ns $ N $ body // th
 
 
 export %inline FromVar (Elim d) where fromVarLoc = B
-export %inline FromVar (Term d) where fromVarLoc = E .: fromVar
+export %inline FromVar (Term d) where fromVarLoc = E .: fromVarLoc
 
 
 ||| does the minimal reasonable work:
@@ -104,7 +104,7 @@ namespace ScopeTermN
   (//) : {s : Nat} ->
          ScopeTermN s d n1 -> Lazy (TSubst d n1 n2) ->
          ScopeTermN s d n2
-  S ns (Y body) // th = S ns $ Y $ body // pushN s th
+  S ns (Y body) // th = S ns $ Y $ body // pushN s (locs $ toList' ns) th
   S ns (N body) // th = S ns $ N $ body // th
 
 namespace DScopeTermN
@@ -189,11 +189,11 @@ dsub1 t p = dsubN t [< p]
 
 
 public export %inline
-(.zero) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n
+(.zero) : (body : DScopeTerm d n) -> {default body.loc loc : Loc} -> Term d n
 body.zero = dsub1 body $ K Zero loc
 
 public export %inline
-(.one) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n
+(.one) : (body : DScopeTerm d n) -> {default body.loc loc : Loc} -> Term d n
 body.one = dsub1 body $ K One loc
 
 
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index 2a2ef36..a25e3cd 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -304,7 +304,7 @@ mutual
     infres <- inferC ctx SZero e
     -- if Ψ | Γ ⊢ Type ℓ <: Type 𝓀
     case u of
-      Just u  => lift $ subtype e.loc ctx infres.type (TYPE u noLoc)
+      Just u  => lift $ subtype e.loc ctx infres.type (TYPE u e.loc)
       Nothing => ignore $ expectTYPE !(askAt DEFS) ctx SZero e.loc infres.type
     -- then Ψ | Γ ⊢₀ E ⇐ Type 𝓀
 
diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr
index 5d62e8a..46238b4 100644
--- a/lib/Quox/Typing.idr
+++ b/lib/Quox/Typing.idr
@@ -54,7 +54,7 @@ substCasePairRet [< x, y] dty retty =
 public export
 substCaseSuccRet : BContext 2 -> ScopeTerm d n -> Term d (2 + n)
 substCaseSuccRet [< p, ih] retty =
-  let arg = Ann (Succ (BVT 1 p.loc) p.loc) (NAT noLoc) $ p.loc `extendL` ih.loc
+  let arg = Ann (Succ (BVT 1 p.loc) p.loc) (NAT p.loc) $ p.loc `extendL` ih.loc
   in
   retty.term // (arg ::: shift 2)
 
diff --git a/lib/Quox/Typing/Context.idr b/lib/Quox/Typing/Context.idr
index 36eb65c..671a06c 100644
--- a/lib/Quox/Typing/Context.idr
+++ b/lib/Quox/Typing/Context.idr
@@ -272,7 +272,7 @@ namespace EqContext
   toTyContext : (e : EqContext n) -> TyContext e.dimLen n
   toTyContext (MkEqContext {dimLen, dassign, dnames, tctx, tnames, qtys}) =
     MkTyContext {
-      dctx = fromGround dassign,
+      dctx = fromGround dnames dassign,
       tctx = map (subD $ shift0 dimLen) tctx,
       dnames, tnames, qtys
     }
diff --git a/lib/Quox/Untyped/Syntax.idr b/lib/Quox/Untyped/Syntax.idr
index bed1927..06f02f0 100644
--- a/lib/Quox/Untyped/Syntax.idr
+++ b/lib/Quox/Untyped/Syntax.idr
@@ -266,7 +266,7 @@ CanSubstSelf Term where
     B i loc =>
       getLoc th i loc
     Lam x body loc =>
-      Lam x (assert_total $ body // push th) loc
+      Lam x (assert_total $ body // push x.loc th) loc
     App fun arg loc =>
       App (fun // th) (arg // th) loc
     Pair fst snd loc =>
@@ -286,19 +286,18 @@ CanSubstSelf Term where
     Succ nat loc =>
       Succ (nat // th) loc
     CaseNat nat zer suc loc =>
-      CaseNat (nat // th) (zer // th)
-              (assert_total substSuc suc th) loc
+      CaseNat (nat // th) (zer // th) (assert_total substSuc suc th) loc
     Str s loc =>
       Str s loc
     Let u x rhs body loc =>
-      Let u x (rhs // th) (assert_total $ body // push th) loc
+      Let u x (rhs // th) (assert_total $ body // push x.loc th) loc
     Erased loc =>
       Erased loc
   where
     substSuc : forall from, to.
                CaseNatSuc from -> USubst from to -> CaseNatSuc to
-    substSuc (NSRec    x ih t) th = NSRec    x ih $ t // pushN 2 th
-    substSuc (NSNonrec x    t) th = NSNonrec x    $ t // push    th
+    substSuc (NSRec    x ih t) th = NSRec    x ih $ t // pushN 2 x.loc th
+    substSuc (NSNonrec x    t) th = NSNonrec x    $ t // push    x.loc th
 
 public export
 subN : SnocVect s (Term n) -> Term (s + n) -> Term n
diff --git a/lib/Quox/Var.idr b/lib/Quox/Var.idr
index ed52579..732b012 100644
--- a/lib/Quox/Var.idr
+++ b/lib/Quox/Var.idr
@@ -141,9 +141,6 @@ weakIsSpec p i = toNatInj $ trans (weakCorrect p i) (sym $ weakSpecCorrect p i)
 public export
 interface FromVar f where %inline fromVarLoc : Var n -> Loc -> f n
 
-public export %inline
-fromVar : FromVar f => Var n -> {default noLoc loc : Loc} -> f n
-fromVar x = fromVarLoc x loc
 
 public export FromVar Var where fromVarLoc x _ = x
 
diff --git a/lib/Quox/Whnf/Coercion.idr b/lib/Quox/Whnf/Coercion.idr
index 2e95742..f8c0e12 100644
--- a/lib/Quox/Whnf/Coercion.idr
+++ b/lib/Quox/Whnf/Coercion.idr
@@ -63,11 +63,11 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
     Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
     (tfst, tsnd) <- tycaseSig defs ctx1 ty
     let [< x, y] = body.names
-        a' = CoeT i (weakT 2 tfst) p q (BVT 1 noLoc) x.loc
+        a' = CoeT i (weakT 2 tfst) p q (BVT 1 x.loc) x.loc
         tsnd' = tsnd.term //
-          (CoeT i (weakT 2 $ tfst // (B VZ noLoc ::: shift 2))
-            (weakD 1 p) (B VZ noLoc) (BVT 1 noLoc) y.loc ::: shift 2)
-        b' = CoeT i tsnd' p q (BVT 0 noLoc) y.loc
+          (CoeT i (weakT 2 $ tfst // (B VZ tsnd.loc ::: shift 2))
+            (weakD 1 p) (B VZ i.loc) (BVT 1 tsnd.loc) y.loc ::: shift 2)
+        b' = CoeT i tsnd' p q (BVT 0 y.loc) y.loc
     whnf defs ctx sg $ CasePair qty (Ann val (ty // one p) val.loc) ret
       (ST body.names $ body.term // (a' ::: b' ::: shift 2)) loc
 
@@ -141,7 +141,8 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
     let ctx1 = extendDim i ctx
     Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
     ta <- tycaseBOX defs ctx1 ty
-    let a' = CoeT i (weakT 1 ta) p q (BVT 0 noLoc) body.name.loc
+    let xloc = body.name.loc
+    let a' = CoeT i (weakT 1 ta) p q (BVT 0 xloc) xloc
     whnf defs ctx sg $ CaseBox qty (Ann val (ty // one p) val.loc) ret
       (ST body.names $ body.term // (a' ::: shift 1)) loc
 
diff --git a/lib/Quox/Whnf/TypeCase.idr b/lib/Quox/Whnf/TypeCase.idr
index 2fc34ba..9b3645f 100644
--- a/lib/Quox/Whnf/TypeCase.idr
+++ b/lib/Quox/Whnf/TypeCase.idr
@@ -120,9 +120,9 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
     -- (type-case π.(x : A) → B ∷ ★ᵢ return Q of { (a → b) ⇒ s; ⋯ }) ⇝
     -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q
     Pi {arg, res, loc = piLoc, _} =>
-      let arg' = Ann arg (TYPE u noLoc) arg.loc
+      let arg' = Ann arg (TYPE u arg.loc) arg.loc
           res' = Ann (Lam res res.loc)
-                     (Arr Zero arg (TYPE u noLoc) arg.loc) res.loc
+                     (Arr Zero arg (TYPE u arg.loc) arg.loc) res.loc
       in
       whnf defs ctx SZero $
         Ann (subN (tycaseRhsDef def KPi arms) [< arg', res']) ret loc
@@ -130,9 +130,9 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
     -- (type-case (x : A) × B ∷ ★ᵢ return Q of { (a × b) ⇒ s; ⋯ }) ⇝
     -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q
     Sig {fst, snd, loc = sigLoc, _} =>
-      let fst' = Ann fst (TYPE u noLoc) fst.loc
+      let fst' = Ann fst (TYPE u fst.loc) fst.loc
           snd' = Ann (Lam snd snd.loc)
-                     (Arr Zero fst (TYPE u noLoc) fst.loc) snd.loc
+                     (Arr Zero fst (TYPE u fst.loc) fst.loc) snd.loc
       in
       whnf defs ctx SZero $
         Ann (subN (tycaseRhsDef def KSig arms) [< fst', snd']) ret loc
@@ -150,8 +150,8 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
       let a0 = a.zero; a1 = a.one in
       whnf defs ctx SZero $ Ann
         (subN (tycaseRhsDef def KEq arms)
-           [< Ann a0 (TYPE u noLoc) a.loc, Ann a1 (TYPE u noLoc) a.loc,
-              Ann (DLam a a.loc) (Eq0 (TYPE u noLoc) a0 a1 a.loc) a.loc,
+           [< Ann a0 (TYPE u a.loc) a.loc, Ann a1 (TYPE u a.loc) a.loc,
+              Ann (DLam a a.loc) (Eq0 (TYPE u a.loc) a0 a1 a.loc) a.loc,
               Ann l a0 l.loc, Ann r a1 r.loc])
         ret loc
 
@@ -166,5 +166,5 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
     -- (type-case [π.A] ∷ ★ᵢ return Q of { [a] ⇒ s; ⋯ }) ⇝ s[(A ∷ ★ᵢ)/a] ∷ Q
     BOX {ty = a, loc = boxLoc, _} =>
       whnf defs ctx SZero $ Ann
-        (sub1 (tycaseRhsDef def KBOX arms) (Ann a (TYPE u noLoc) a.loc))
+        (sub1 (tycaseRhsDef def KBOX arms) (Ann a (TYPE u a.loc) a.loc))
         ret loc