diff --git a/lib/Quox/Name.idr b/lib/Quox/Name.idr
index a8c9803..a31560b 100644
--- a/lib/Quox/Name.idr
+++ b/lib/Quox/Name.idr
@@ -181,12 +181,11 @@ mn base = do
 ||| generate a fresh binding name with the given base and
 ||| (optionally) location `loc`
 export
-mnb : Has NameGen fs =>
-      PBaseName -> {default noLoc loc : Loc} -> Eff fs BindName
-mnb base = pure $ BN !(mn base) loc
+mnb : Has NameGen fs => PBaseName -> Loc -> Eff fs BindName
+mnb base loc = pure $ BN !(mn base) loc
 
 export
 fresh : Has NameGen fs => BindName -> Eff fs BindName
-fresh (BN (UN str)   loc) = mnb str {loc}
-fresh (BN (MN str k) loc) = mnb str {loc}
-fresh (BN Unused     loc) = mnb "x" {loc}
+fresh (BN (UN str)   loc) = mnb str loc
+fresh (BN (MN str k) loc) = mnb str loc
+fresh (BN Unused     loc) = mnb "x" loc
diff --git a/lib/Quox/Whnf/TypeCase.idr b/lib/Quox/Whnf/TypeCase.idr
index f6344bb..8bc7fd6 100644
--- a/lib/Quox/Whnf/TypeCase.idr
+++ b/lib/Quox/Whnf/TypeCase.idr
@@ -43,7 +43,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
   tycasePi (E e) {tnf} = do
     ty <- computeElimType defs ctx e {ne = noOr2 tnf}
     let loc  = e.loc
-        narg = mnb "Arg"; nret = mnb "Ret"
+        narg = mnb "Arg" loc; nret = mnb "Ret" loc
         arg  = E $ typeCase1Y e ty KPi [< !narg, !nret] (BVT 1 loc) loc
         res' = typeCase1Y e (Arr Zero arg ty loc) KPi [< !narg, !nret]
                  (BVT 0 loc) loc
@@ -61,7 +61,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
   tycaseSig (E e) {tnf} = do
     ty <- computeElimType defs ctx e {ne = noOr2 tnf}
     let loc  = e.loc
-        nfst = mnb "Fst"; nsnd = mnb "Snd"
+        nfst = mnb "Fst" loc; nsnd = mnb "Snd" loc
         fst  = E $ typeCase1Y e ty KSig [< !nfst, !nsnd] (BVT 1 loc) loc
         snd' = typeCase1Y e (Arr Zero fst ty loc) KSig [< !nfst, !nsnd]
                  (BVT 0 loc) loc
@@ -78,7 +78,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
   tycaseBOX (BOX {ty, _}) = pure ty
   tycaseBOX (E e) {tnf} = do
     ty <- computeElimType defs ctx e {ne = noOr2 tnf}
-    pure $ E $ typeCase1Y e ty KBOX [< !(mnb "Ty")] (BVT 0 e.loc) e.loc
+    pure $ E $ typeCase1Y e ty KBOX [< !(mnb "Ty" e.loc)] (BVT 0 e.loc) e.loc
   tycaseBOX t = throw $ ExpectedBOX t.loc ctx.names t
 
   ||| for Eq [i ⇒ A] l r, returns (A‹0/i›, A‹1/i›, A, l, r);
@@ -91,11 +91,11 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
   tycaseEq (E e) {tnf} = do
     ty <- computeElimType defs ctx e {ne = noOr2 tnf}
     let loc   = e.loc
-        names = traverse' (\x => mnb x) [< "A0", "A1", "A", "L", "R"]
+        names = traverse' (\x => mnb x loc) [< "A0", "A1", "A", "L", "R"]
         a0    = E $ typeCase1Y e ty KEq !names (BVT 4 loc) loc
         a1    = E $ typeCase1Y e ty KEq !names (BVT 3 loc) loc
         a'    = typeCase1Y e (Eq0 ty a0 a1 loc) KEq !names (BVT 2 loc) loc
-        a     = DST [< !(mnb "i")] $ E $ DApp (dweakE 1 a') (B VZ loc) loc
+        a     = DST [< !(mnb "i" loc)] $ E $ DApp (dweakE 1 a') (B VZ loc) loc
         l     = E $ typeCase1Y e a0 KEq !names (BVT 1 loc) loc
         r     = E $ typeCase1Y e a1 KEq !names (BVT 0 loc) loc
     pure (a0, a1, a, l, r)