From fc987a6f11c2f874f7be37542e5e690146a558b1 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sat, 4 Oct 2025 18:11:24 -0700
Subject: [PATCH] cleanup

---
 src/Lib/Compile.newt   | 2 --
 src/Lib/LiftWhere.newt | 5 -----
 src/Lib/TCO.newt       | 2 --
 src/Prelude.newt       | 7 +++++--
 4 files changed, 5 insertions(+), 11 deletions(-)

diff --git a/src/Lib/Compile.newt b/src/Lib/Compile.newt
index bd900c9..d7fa712 100644
--- a/src/Lib/Compile.newt
+++ b/src/Lib/Compile.newt
@@ -444,8 +444,6 @@ process name = do
   -- Maybe move this dance into liftWhere
   ref <- newIORef entries
   let foo = MkRef ref -- for the autos below
-  -- TODO, erasure needs to happen on Tm, but can be part of Tm -> CExp
-  -- if we move the liftWhere down.
   eraseEntries
   liftWhere
   entries <- readIORef ref
diff --git a/src/Lib/LiftWhere.newt b/src/Lib/LiftWhere.newt
index cc160eb..f4d8b6b 100644
--- a/src/Lib/LiftWhere.newt
+++ b/src/Lib/LiftWhere.newt
@@ -58,11 +58,6 @@ liftWhereTm name env (LetRec fc nm ty t u) = do
       let (Just _) = lookupMap qn' top | _ => pure qn'
       getName qn (ext ++ "'")
 
-    -- Hacky - CompileExp expects a pi type that matches arity
-    wrapPi : Nat → Tm → Tm
-    wrapPi Z tm = tm
-    wrapPi (S k) tm = Pi fc "_" Explicit Many (Erased fc) $ wrapPi k tm
-
     wrapLam : Nat → Tm → Tm
     wrapLam Z tm = tm
     -- REVIEW We've already erased, hopefully we don't need quantity
diff --git a/src/Lib/TCO.newt b/src/Lib/TCO.newt
index cb38e7d..0e750a0 100644
--- a/src/Lib/TCO.newt
+++ b/src/Lib/TCO.newt
@@ -32,8 +32,6 @@ tailNames (CConstr _ _ args) = Nil
 tailNames (CBnd _) = Nil
 tailNames (CFun _ tm) = tailNames tm
 tailNames (CLam _ _) = Nil
--- should not happen, FIXME
-tailNames (CAppRef t args n) = Nil
 tailNames (CApp t u) = Nil
 tailNames (CRef _) = Nil
 tailNames CErased = Nil
diff --git a/src/Prelude.newt b/src/Prelude.newt
index f8040af..1607b38 100644
--- a/src/Prelude.newt
+++ b/src/Prelude.newt
@@ -523,8 +523,11 @@ enumerate {a} xs = go Z xs
     go k (x :: xs) = (k,x) :: go (S k) xs
 
 filter : ∀ a. (a → Bool) → List a → List a
-filter pred Nil = Nil
-filter pred (x :: xs) = if pred x then x :: filter pred xs else filter pred xs
+filter {a} pred xs = go xs Lin
+  where
+    go : List a → SnocList a → List a
+    go Nil acc = acc <>> Nil
+    go (x :: xs) acc = if pred x then go xs (acc :< x) else go xs acc
 
 drop : ∀ a. Nat → List a → List a
 drop _ Nil = Nil