stop throwing names away

lib/Quox/Syntax/Term/Tighten.idr

@@ -250,19 +250,19 @@ export Tighten (\d => Elim d n) where tighten p e = dtightenE p e
 
 parameters {auto _ : Tighten f} {s : Nat}
   export
-  squeeze : Scoped s f n -> Either (BContext s, f (s + n)) (f n)
-  squeeze (S ns (N t)) = Right t
-  squeeze (S ns (Y t)) = maybe (Left (ns, t)) Right $ tightenN s t
+  squeeze : Scoped s f n -> (BContext s, Either (f (s + n)) (f n))
+  squeeze (S ns (N t)) = (ns, Right t)
+  squeeze (S ns (Y t)) = (ns, maybe (Left t) Right $ tightenN s t)
 
   export
   squeeze' : Scoped s f n -> Scoped s f n
-  squeeze' = either (uncurry SY) SN . squeeze
+  squeeze' t = let (ns, res) = squeeze t in S ns $ either Y N res
 
 parameters {0 f : Nat -> Nat -> Type}
            {auto tt : Tighten (\d => f d n)} {s : Nat}
   export
   dsqueeze : Scoped s (\d => f d n) d ->
-             Either (BContext s, f (s + d) n) (f d n)
+             (BContext s, Either (f (s + d) n) (f d n))
   dsqueeze = squeeze
 
   export
@@ -272,11 +272,11 @@ parameters {0 f : Nat -> Nat -> Type}
 
 -- versions of SY, etc, that try to tighten and use SN automatically
 
-public export
+public export %inline
 ST : Tighten f => {s : Nat} -> BContext s -> f (s + n) -> Scoped s f n
 ST names body = squeeze' $ SY names body
 
-public export
+public export %inline
 DST : {s : Nat} -> BContext s -> Term (s + d) n -> DScopeTermN s d n
 DST names body = dsqueeze' {f = Term} $ SY names body
 

lib/Quox/Whnf/Main.idr

@@ -145,7 +145,7 @@ CanWhnf Elim Interface.isRedexE where
     --
     -- [fixme] needs a real equality check between A‹0/𝑖› and A‹1/𝑖›
     case dsqueeze sty {f = Term} of
-      Left ([< i], ty) =>
+      ([< i], Left ty) =>
         case p `decEqv` q of
           -- coe (𝑖 ⇒ A) @p @p s ⇝ (s ∷ A‹p/𝑖›)
           Yes _   => whnf defs ctx $ Ann val (dsub1 sty p) coeLoc
@@ -155,7 +155,7 @@ CanWhnf Elim Interface.isRedexE where
               Left  pc  => pushCoe defs ctx i ty p q val coeLoc
               Right npc => pure $ Element (Coe (SY [< i] ty) p q val coeLoc)
                                           (tynf `orNo` npc `orNo` notYesNo npq)
-      Right ty =>
+      (_, Right ty) =>
         whnf defs ctx $ Ann val ty coeLoc
 
   whnf defs ctx (Comp ty p q val r zero one compLoc) =