From 754839b063a578a4e0589b01d921b4530c070541 Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Sun, 1 Nov 2026 20:42:37 +0000
Subject: [PATCH 1/5] --typed: restricted type erasure

---
 agda2lambox.cabal                   |   1 +
 src/Agda/Utils.hs                   |   4 +-
 src/Agda/Utils/Erase.hs             | 371 ++++++++++++++++++++++++++++
 src/Agda/Utils/Treeless.hs          |  66 ++---
 src/Agda2Lambox/Compile/Function.hs |  21 +-
 src/Agda2Lambox/Compile/Utils.hs    |  10 +
 test/untyped/EtaCon.agda            |   8 +-
 test/untyped/Fannkuch.agda          |   2 +-
 test/untyped/Prelude.agda           |   8 +-
 9 files changed, 439 insertions(+), 52 deletions(-)
 create mode 100644 src/Agda/Utils/Erase.hs

diff --git a/agda2lambox.cabal b/agda2lambox.cabal
index 0fee13b..ebec092 100644
--- a/agda2lambox.cabal
+++ b/agda2lambox.cabal
@@ -19,6 +19,7 @@ executable agda2lambox
   main-is:             Main.hs
   other-modules:       Agda.Utils,
                        Agda.Utils.EliminateDefaults,
+                       Agda.Utils.Erase,
                        Agda.Utils.EtaExpandConstructors,
                        Agda.Utils.Simplify,
                        Agda.Utils.Treeless,
diff --git a/src/Agda/Utils.hs b/src/Agda/Utils.hs
index bf33f48..653c08d 100644
--- a/src/Agda/Utils.hs
+++ b/src/Agda/Utils.hs
@@ -100,8 +100,8 @@ etaExpand = \case
 -- ** toTreeless custom pipeline
 
 -- | Convert compiled clauses to treeless syntax, and return it.
-treeless :: QName -> TCM (Maybe TTerm)
-treeless = CustomTT.toTreeless EagerEvaluation
+treeless :: CustomTT.Erasure -> QName -> TCM (Maybe TTerm)
+treeless er = CustomTT.toTreeless (EagerEvaluation, er)
   
 -- * projections
 
diff --git a/src/Agda/Utils/Erase.hs b/src/Agda/Utils/Erase.hs
new file mode 100644
index 0000000..37f0594
--- /dev/null
+++ b/src/Agda/Utils/Erase.hs
@@ -0,0 +1,371 @@
+-- | The erasure pass of "Agda.Compiler.Treeless.Erase", parameterised by what it may erase.
+module Agda.Utils.Erase
+  ( Erasure(..)
+  , eraseTerms
+  ) where
+
+import Control.Arrow       ( first, second )
+import Control.Monad.State ( StateT, evalStateT, gets )
+
+import Data.Map (Map)
+import qualified Data.Map as Map
+
+import Agda.Syntax.Common
+import Agda.Syntax.Internal as I
+import Agda.Syntax.Treeless
+import Agda.Syntax.Literal
+
+import Agda.TypeChecking.Substitute
+import Agda.TypeChecking.Monad as I
+import Agda.TypeChecking.Telescope
+import Agda.TypeChecking.Datatypes
+import Agda.TypeChecking.Pretty
+import Agda.TypeChecking.Primitive
+
+import Agda.Compiler.Treeless.Subst
+import Agda.Compiler.Treeless.Unused
+
+import Agda.Utils.Functor
+import Agda.Utils.Lens
+import Agda.Utils.Maybe
+import Agda.Utils.Memo
+import Agda.Utils.Monad
+import Agda.Syntax.Common.Pretty (prettyShow)
+import Agda.Utils.IntSet.Infinite (IntSet)
+import qualified Agda.Utils.IntSet.Infinite as IntSet
+
+import Agda.Utils.Impossible
+
+-- | What the erasure pass replaces by @TErased@, besides arguments of erased modality.
+data Erasure
+  = EraseAll
+    -- ^ as Agda: also values of unit-like types, and unused or forced arguments
+  | EraseLogical (QName -> TCM Bool)
+    -- ^ only types, and values whose type is headed by a definition satisfying the predicate
+
+-- | State of the eraser.
+data ESt = ESt
+  { _erasure :: Erasure
+  , _funMap  :: Map QName FunInfo
+      -- ^ Memoize computed `FunInfo` for functions/constructors/... `QName`.
+  , _typeMap :: Map QName TypeInfo
+      -- ^ Memoize computed `TypeInfo` for data/record types `QName`.
+  }
+
+funMap :: Lens' ESt (Map QName FunInfo)
+funMap f r = f (_funMap r) <&> \ a -> r { _funMap = a }
+
+typeMap :: Lens' ESt (Map QName TypeInfo)
+typeMap f r = f (_typeMap r) <&> \ a -> r { _typeMap = a }
+
+-- | Eraser monad.
+type E = StateT ESt TCM
+
+runE :: Erasure -> E a -> TCM a
+runE er m = evalStateT m (ESt er Map.empty Map.empty)
+
+eraseTerms :: Erasure -> QName -> EvaluationStrategy -> TTerm -> TCM TTerm
+eraseTerms er q eval t = usedArguments q t *> runE er (eraseTop q t)
+  where
+    eraseTop q t = do
+      (_, h) <- getFunInfo q
+      case h of
+        Erasable -> pure TErased
+        Empty    -> pure TErased
+        _        -> erase t
+
+    erase t = case tAppView t of
+
+      (TCon c, vs) -> do
+        (rs, h) <- getFunInfo c
+        when (length rs < length vs) __IMPOSSIBLE__
+        case h of
+          Erasable -> pure TErased
+          Empty    -> pure TErased
+          _        -> tApp (TCon c) <$> zipWithM eraseRel rs vs
+
+      (TDef f, vs) -> do
+        (rs, h) <- getFunInfo f
+        case h of
+          Erasable -> pure TErased
+          Empty    -> pure TErased
+          _        -> tApp (TDef f) <$> zipWithM eraseRel (rs ++ repeat NotErasable) vs
+
+      _ -> case t of
+        TVar{}         -> pure t
+        TDef{}         -> pure t
+        TPrim{}        -> pure t
+        TLit{}         -> pure t
+        TCon{}         -> pure t
+        TApp f es      -> tApp <$> erase f <*> mapM erase es
+        TLam b         -> tLam <$> erase b
+        TLet e b       -> do
+          e <- erase e
+          if isErased e
+            then case b of
+                   TCase 0 _ _ _ -> tLet TErased <$> erase b
+                   _             -> erase $ subst 0 TErased b
+            else tLet e <$> erase b
+        TCase x t d bs -> do
+          (d, bs) <- pruneUnreachable x (caseErased t) (caseType t) d bs
+          d       <- erase d
+          bs      <- mapM eraseAlt bs
+          tCase x t d bs
+
+        TUnit          -> pure t
+        TSort          -> pure t
+        TErased        -> pure t
+        TError{}       -> pure t
+        TCoerce e      -> TCoerce <$> erase e
+
+    -- #3380: this is not safe for strict backends
+    tLam TErased | eval == LazyEvaluation = TErased
+    tLam t                                = TLam t
+
+    tLet e b
+      | freeIn 0 b = TLet e b
+      | otherwise  = strengthen impossible b
+
+    tApp f []                  = f
+    tApp TErased _             = TErased
+    tApp f _ | isUnreachable f = tUnreachable
+    tApp f es                  = mkTApp f es
+
+    tCase x t d bs
+      | isErased d && all (isErased . aBody) bs = pure TErased
+      | otherwise = case bs of
+        [b@(TACon c _ _)] -> do
+          h <- snd <$> getFunInfo c
+          case h of
+            NotErasable -> fallback
+            Empty       -> pure TErased
+            Erasable    -> erasedBody b
+        _ -> fallback
+      where
+        noerase = pure $ TCase x t d bs
+
+        erasedBody = \case
+          TACon _ arity body ->
+            (if arity == 0 then pure else erase) $
+               -- might enable more erasure
+            applySubst (replicate arity TErased ++# idS) body
+          TALit _ body   -> pure body
+          TAGuard _ body -> pure body
+
+        fallback = case (caseErased t, bs) of
+          (Erased{}, [b]) ->
+            -- The case variable is erased, and there is exactly one
+            -- case: use the case's body.
+            erasedBody b
+          (Erased{}, [])  ->
+            -- The case variable is erased, and there is no case: use
+            -- the default.
+            pure $ if isErased d then TErased else d
+          (Erased{}, _ : _ : _) ->
+            -- The case variable is erased, and there are at least two
+            -- cases: crash.
+            __IMPOSSIBLE__
+          _ ->
+            -- The case variable is not erased: do not erase anything.
+            noerase
+
+    isErased t = t == TErased || isUnreachable t
+
+    eraseRel r t | erasable r = pure TErased
+                 | otherwise  = erase t
+
+    eraseAlt = \case
+      TALit l b   -> TALit l   <$> erase b
+      TACon c a b -> do
+        rs <- map erasable . fst <$> getFunInfo c
+        let sub = foldr (\ e -> if e then (TErased :#) . wkS 1 else liftS 1) idS $ reverse rs
+        TACon c a <$> erase (applySubst sub b)
+      TAGuard g b -> TAGuard   <$> erase g <*> erase b
+
+pruneUnreachable ::
+  Int -> Erased -> CaseType -> TTerm -> [TAlt] -> E (TTerm, [TAlt])
+pruneUnreachable x erased t d bs = case erased of
+  NotErased{} -> pruneUnreachable' x erased t d bs
+  Erased{}    ->
+    -- If the match is on an erased argument, then the first branch
+    -- should match.
+    case bs of
+      []    -> pruneUnreachable' x erased t d            []
+      b : _ -> pruneUnreachable' x erased t tUnreachable [b]
+
+-- | Doesn't have any type information (other than the name of the data type),
+--   so we can't do better than checking if all constructors are present.
+pruneUnreachable' ::
+  Int -> Erased -> CaseType -> TTerm -> [TAlt] -> E (TTerm, [TAlt])
+pruneUnreachable' _ erased (CTData q) d bs' = do
+  -- Erased constructors are pruned iff the match is made on a
+  -- non-erased argument.
+  cs <- lift $
+        if isErased erased
+        then getConstructors q
+        else getNotErasedConstructors q
+  let bs | isErased erased = bs'
+         | otherwise       =
+           flip filter bs' $ \case
+             a@TACon{} -> (aCon a) `elem` cs
+             TAGuard{} -> True
+             TALit{}   -> True
+  let -- In the case of a match on an erased argument the value d is
+      -- equal to tUnreachable, except perhaps if bs is empty. In the
+      -- latter case complete is True exactly when the type has zero
+      -- constructors (erased or not), in which case it makes sense to
+      -- replace d with tUnreachable.
+      complete = length cs == length [ b | b@TACon{} <- bs ]
+      d' | complete  = tUnreachable
+         | otherwise = d
+  return (d', bs)
+pruneUnreachable' x _ CTNat d bs =
+  return $ pruneIntCase x d bs (IntSet.below 0)
+pruneUnreachable' x _ CTInt d bs =
+  return $ pruneIntCase x d bs IntSet.empty
+pruneUnreachable' _ _ _ d bs =
+  pure (d, bs)
+
+-- These are the guards we generate for Int/Nat pattern matching
+pattern Below :: Int -> Integer -> TTerm
+pattern Below x n = TApp (TPrim PLt)  [TVar x, TLit (LitNat n)]
+
+pattern Above :: Int -> Integer -> TTerm
+pattern Above x n = TApp (TPrim PGeq) [TVar x, TLit (LitNat n)]
+
+-- | Strip unreachable clauses (replace by tUnreachable for the default).
+--   Fourth argument is the set of ints covered so far.
+pruneIntCase :: Int -> TTerm -> [TAlt] -> IntSet -> (TTerm, [TAlt])
+pruneIntCase x d bs cover = go bs cover
+  where
+    go [] cover
+      | cover == IntSet.full = (tUnreachable, [])
+      | otherwise            = (d, [])
+    go (b : bs) cover =
+      case b of
+        TAGuard (Below y n) _ | x == y -> rec (IntSet.below n)
+        TAGuard (Above y n) _ | x == y -> rec (IntSet.above n)
+        TALit (LitNat n) _             -> rec (IntSet.singleton n)
+        _                                -> second (b :) $ go bs cover
+      where
+        rec this = second addAlt $ go bs cover'
+          where
+            this'  = IntSet.difference this cover
+            cover' = this' <> cover
+            addAlt = case IntSet.toFiniteList this' of
+                       Just []  -> id                                     -- unreachable case
+                       Just [n] -> (TALit (LitNat n) (aBody b) :) -- possibly refined case
+                       _        -> (b :)                                  -- unchanged case
+
+data TypeInfo = Empty | Erasable | NotErasable
+  deriving (Eq, Show)
+
+sumTypeInfo :: [TypeInfo] -> TypeInfo
+sumTypeInfo is = foldr plus Empty is
+  where
+    plus Empty       r           = r
+    plus r           Empty       = r
+    plus Erasable    r           = r
+    plus r           Erasable    = r
+    plus NotErasable NotErasable = NotErasable
+
+erasable :: TypeInfo -> Bool
+erasable Erasable    = True
+erasable Empty       = True
+erasable NotErasable = False
+
+type FunInfo = ([TypeInfo], TypeInfo)
+
+getFunInfo :: QName -> E FunInfo
+getFunInfo q = memo (funMap . key q) $ getInfo q
+  where
+    getInfo :: QName -> E FunInfo
+    getInfo q = do
+      er <- gets _erasure
+      (rs, t) <- do
+        (tel, t) <- lift $ typeWithoutParams q
+        is     <- mapM (getTypeInfo . snd . dget) tel
+        used   <- lift $ (++ repeat ArgUsed) . fromMaybe [] <$> getCompiledArgUse q
+        forced <- lift $ (++ repeat NotForced) <$> getForcedArgs q
+        return (zipWith3 (uncurry . mkR er . getModality) tel (zip forced used) is, t)
+      h <- if isAbsurdLambdaName q then pure Erasable else getTypeInfo t
+      lift $ reportSLn "treeless.opt.erase.info" 50 $ "type info for " ++ prettyShow q ++ ": " ++ show rs ++ " -> " ++ show h
+      lift $ setErasedConArgs q $ map erasable rs
+      return (rs, h)
+
+    -- Treat empty, erasable, or unused arguments as Erasable
+    mkR :: Erasure -> Modality -> IsForced -> ArgUsage -> TypeInfo -> TypeInfo
+    mkR er m f u i
+      | not (usableModality m)         = Erasable
+      | EraseAll <- er, ArgUnused <- u = Erasable
+      | EraseAll <- er, Forced <- f    = Erasable
+      | otherwise                      = i
+
+telListView :: Type -> TCM (ListTel, Type)
+telListView t = do
+  TelV tel t <- telViewPath t
+  return (telToList tel, t)
+
+typeWithoutParams :: QName -> TCM (ListTel, Type)
+typeWithoutParams q = do
+  def <- getConstInfo q
+  let d = case I.theDef def of
+        Function{ funProjection = Right Projection{ projIndex = i } } -> i - 1
+        Constructor{ conPars = n } -> n
+        _                          -> 0
+  first (drop d) <$> telListView (defType def)
+
+getTypeInfo :: Type -> E TypeInfo
+getTypeInfo t0 = do
+  (tel, t) <- lift $ telListView t0
+  et <- case I.unEl t of
+    I.Def d _ -> do
+      -- #2916: Only update the memo table for d. Results for other types are
+      -- under the assumption that d is erasable!
+      oldMap <- use typeMap
+      dInfo <- typeInfo d
+      typeMap .= Map.insert d dInfo oldMap
+      return dInfo
+    Sort{}    -> return Erasable
+    _         -> return NotErasable
+  is <- mapM (getTypeInfo . snd . dget) tel
+  let e | Empty `elem` is = Erasable
+        | null is         = et        -- TODO: guard should really be "all inhabited is"
+        | et == Empty     = Erasable
+        | otherwise       = et
+  lift $ reportSDoc "treeless.opt.erase.type" 50 $ prettyTCM t0 <+> text ("is " ++ show e)
+  return e
+  where
+  typeInfo :: QName -> E TypeInfo
+  typeInfo q = gets _erasure >>= \case
+    EraseLogical isLogical -> memo (typeMap . key q) $
+      lift (isLogical q) <&> \b -> if b then Erasable else NotErasable
+    EraseAll -> typeInfoAll q
+  typeInfoAll :: QName -> E TypeInfo
+  typeInfoAll q = ifM (erasureForbidden q) (return NotErasable) $ {-else-} do
+    memoRec (typeMap . key q) Erasable $ do  -- assume recursive occurrences are erasable
+      msizes <- lift $ mapM getBuiltinName
+                         [builtinSize, builtinSizeLt]
+      def    <- lift $ getConstInfo q
+      let mcs = case I.theDef def of
+                  I.Datatype{ dataCons = cs } -> Just cs
+                  I.Record{ recConHead = c }  -> Just [conName c]
+                  _                           -> Nothing
+      case mcs of
+        _ | Just q `elem` msizes -> return Erasable
+        Just [c] -> do
+          (ts, _) <- lift $ typeWithoutParams c
+          let rs = map getModality ts
+          is <- mapM (getTypeInfo . snd . dget) ts
+          let er = and [ erasable i || not (usableModality r) | (i, r) <- zip is rs ]
+          return $ if er then Erasable else NotErasable
+        Just []      -> return Empty
+        Just (_:_:_) -> return NotErasable
+        Nothing ->
+          case I.theDef def of
+            I.Function{ funClauses = cs } ->
+              sumTypeInfo <$> mapM (maybe (return Empty) (getTypeInfo . El __DUMMY_SORT__) . clauseBody) cs
+            _ -> return NotErasable
+  -- The backend also has a say whether a type is eraseable or not.
+  erasureForbidden :: QName -> E Bool
+  erasureForbidden q = lift $ not <$> activeBackendMayEraseType q
diff --git a/src/Agda/Utils/Treeless.hs b/src/Agda/Utils/Treeless.hs
index 6df08df..b327382 100644
--- a/src/Agda/Utils/Treeless.hs
+++ b/src/Agda/Utils/Treeless.hs
@@ -16,7 +16,7 @@ module Agda.Utils.Treeless
   , compilerPass
   , compilerPipeline
   , CCConfig
-  , CCSubst(..)
+  , Erasure(..)
   , alwaysInline
   ) where
 
@@ -47,7 +47,6 @@ import Agda.TypeChecking.Substitute
 
 import Agda.Compiler.Treeless.AsPatterns
 import Agda.Compiler.Treeless.Builtin
-import Agda.Compiler.Treeless.Erase
 import Agda.Compiler.Treeless.Identity
 import Agda.Compiler.Treeless.Simplify
 import Agda.Compiler.Treeless.Uncase
@@ -67,6 +66,7 @@ import qualified Agda.Utils.SmallSet as SmallSet
 import Agda.Utils.Impossible
 
 import Agda.Utils.EliminateDefaults
+import Agda.Utils.Erase
 import Agda.Utils.ThunkLets
 import Agda.Utils.EtaExpandConstructors
 import Agda.Utils.Simplify
@@ -91,7 +91,7 @@ getCompiledClauses q = do
   CC.compileClauses' q translate cs mst
 
 -- ** Types of pipelines; different backends might use their own custom pipeline.
-type BuildPipeline = Int -> QName -> Pipeline
+type BuildPipeline = Erasure -> Int -> QName -> Pipeline
 
 data Pipeline = FixedPoint Int Pipeline
               | Sequential [Pipeline]
@@ -106,7 +106,6 @@ data CompilerPass = CompilerPass
 
 type CC        = ReaderT CCEnv TCM
 type CCContext = [Int]
-data CCSubst   = EraseUnused | IgnoreUnused deriving Eq
 
 -- | Environment for treeless conversion.
 data CCEnv = CCEnv
@@ -117,19 +116,19 @@ data CCEnv = CCEnv
     -- If an inner case has no catch-all clause, we use the one from its parent.
   , ccEvaluation  :: EvaluationStrategy
     -- ^ Which evaluation strategy does the backend assumes.
-  , ccSubstUnused :: CCSubst
-    -- ^ Whether to erase unused arguments.
+  , ccErasure     :: Erasure
+    -- ^ What to erase, e.g. unused arguments.
   }
 
-type CCConfig  = (EvaluationStrategy, CCSubst)
+type CCConfig  = (EvaluationStrategy, Erasure)
 
 -- | Initial environment for expression generation.
 initCCEnv :: CCConfig -> CCEnv
-initCCEnv (eval, su) = CCEnv
+initCCEnv (eval, er) = CCEnv
   { ccCxt         = []
   , ccCatchall    = Nothing
   , ccEvaluation  = eval
-  , ccSubstUnused = su
+  , ccErasure     = er
   }
 
 -- | Converts compiled clauses to treeless syntax.
@@ -143,8 +142,8 @@ toTreelessWith pl cfg q
   = ifM (alwaysInline q) (pure Nothing)
   $ Just <$> toTreelessWith' pl cfg q
 
-toTreeless :: EvaluationStrategy -> QName -> TCM (Maybe C.TTerm)
-toTreeless eval = toTreelessWith compilerPipeline (eval, EraseUnused)
+toTreeless :: CCConfig -> QName -> TCM (Maybe C.TTerm)
+toTreeless = toTreelessWith compilerPipeline
 
 toTreelessWith' :: BuildPipeline -> CCConfig -> QName -> TCM C.TTerm
 toTreelessWith' pl cfg q =
@@ -155,20 +154,20 @@ toTreelessWith' pl cfg q =
       -- functions, since that would risk inlining to fail.
     ccToTreelessWith pl cfg q cc
 
-toTreeless' :: EvaluationStrategy -> QName -> TCM C.TTerm
-toTreeless' eval = toTreelessWith' compilerPipeline (eval, EraseUnused)
+toTreeless' :: CCConfig -> QName -> TCM C.TTerm
+toTreeless' = toTreelessWith' compilerPipeline
 
 ccToTreelessWith :: BuildPipeline -> CCConfig -> QName -> CC.CompiledClauses -> TCM C.TTerm
-ccToTreelessWith pl cfg@(eval, su) q cc = do
+ccToTreelessWith pl cfg@(eval, er) q cc = do
   let pbody b = pbody' "" b
       pbody' suf b = sep [ text (prettyShow q ++ suf) <+> "=", nest 2 $ prettyPure b ]
   v <- ifM (alwaysInline q) (return 20) (return 0)
   reportSDoc "treeless.convert" (30 + v) $ "-- compiled clauses of" <+> prettyTCM q $$ nest 2 (prettyPure cc)
   body <- casetreeTop cfg cc
   reportSDoc "treeless.opt.converted" (30 + v) $ "-- converted" $$ pbody body
-  body <- runPipeline eval q (pl v q) body
+  body <- runPipeline eval q (pl er v q) body
   used <- usedArguments q body
-  when (su == EraseUnused && ArgUnused `elem` used) $
+  when (erasesUnused er && ArgUnused `elem` used) $
     reportSDoc "treeless.opt.unused" (30 + v) $
       "-- used args:" <+> hsep [ if u == ArgUsed then text [x] else "_" | (x, u) <- zip ['a'..] used ] $$
       pbody' "[stripped]" (stripUnusedArguments used body)
@@ -177,20 +176,20 @@ ccToTreelessWith pl cfg@(eval, su) q cc = do
   setCompiledArgUse q used
   return body
 
-ccToTreeless :: EvaluationStrategy -> QName -> CC.CompiledClauses -> TCM C.TTerm
-ccToTreeless eval = ccToTreelessWith compilerPipeline (eval, EraseUnused)
+ccToTreeless :: CCConfig -> QName -> CC.CompiledClauses -> TCM C.TTerm
+ccToTreeless = ccToTreelessWith compilerPipeline
 
 compilerPass :: String -> Int -> String -> (EvaluationStrategy -> TTerm -> TCM TTerm) -> Pipeline
 compilerPass tag v name code = SinglePass (CompilerPass tag v name code)
 
 compilerPipeline :: BuildPipeline
-compilerPipeline v q =
+compilerPipeline er v q =
   Sequential
 
     -- [ compilerPass "builtin" (30 + v) "builtin translation" $ const translateBuiltins
     [ FixedPoint 5 $ Sequential
       -- [ compilerPass "simpl"  (30 + v) "simplification"     $ const simplifyTTerm
-      [ compilerPass "erase"  (30 + v) "erasure"            $ eraseTerms q
+      [ compilerPass "erase"  (30 + v) "erasure"            $ eraseTerms er q
       , compilerPass "uncase" (30 + v) "uncase"             $ const caseToSeq
 
 
@@ -618,36 +617,41 @@ normaliseStatic v@(I.Def f es) = lift $ do
 normaliseStatic v = pure v
 
 -- | Does not require the name to refer to a function.
-cacheTreeless :: EvaluationStrategy -> QName -> TCM ()
-cacheTreeless eval q = do
+cacheTreeless :: CCConfig -> QName -> TCM ()
+cacheTreeless cfg q = do
   def <- theDef <$> getConstInfo q
   case def of
-    Function{} -> () <$ toTreeless' eval q
+    Function{} -> () <$ toTreeless' cfg q
     _          -> return ()
 
+-- | Whether unused arguments are erased.
+erasesUnused :: Erasure -> Bool
+erasesUnused = \case
+  EraseAll       -> True
+  EraseLogical{} -> False
+
 maybeInlineDef :: I.QName -> I.Args -> CC C.TTerm
 maybeInlineDef q vs = do
-  eval <- asks ccEvaluation
-  ifM (lift $ alwaysInline q) (doinline eval) $ do
-    lift $ cacheTreeless eval q
+  cfg <- asks \ e -> (ccEvaluation e, ccErasure e)
+  ifM (lift $ alwaysInline q) (doinline cfg) $ do
+    lift $ cacheTreeless cfg q
     def <- lift $ getConstInfo q
     case theDef def of
       fun@Function{}
-        | fun ^. funInline -> doinline eval
+        | fun ^. funInline -> doinline cfg
         | otherwise -> do
         -- If ArgUsage hasn't been computed yet, we assume all arguments are used.
         used <- lift $ fromMaybe [] <$> getCompiledArgUse q
-        su <- asks ccSubstUnused
         let substUsed arg used
-              | used == ArgUnused && su == EraseUnused
+              | used == ArgUnused && erasesUnused (snd cfg)
               = pure C.TErased
               | otherwise
               = substArg arg
         C.mkTApp (C.TDef q) <$> zipWithM substUsed vs (used ++ repeat ArgUsed)
       _ -> C.mkTApp (C.TDef q) <$> substArgs vs
   where
-    doinline eval = C.mkTApp <$> inline eval q <*> substArgs vs
-    inline eval q = lift $ toTreeless' eval q
+    doinline cfg = C.mkTApp <$> inline cfg q <*> substArgs vs
+    inline cfg q = lift $ toTreeless' cfg q
 
 substArgs :: [Arg I.Term] -> CC [C.TTerm]
 substArgs = traverse substArg
diff --git a/src/Agda2Lambox/Compile/Function.hs b/src/Agda2Lambox/Compile/Function.hs
index 32a43cc..ec870c2 100644
--- a/src/Agda2Lambox/Compile/Function.hs
+++ b/src/Agda2Lambox/Compile/Function.hs
@@ -24,7 +24,7 @@ import Agda.Syntax.Internal.Names ( namesIn )
 import Agda.Syntax.Common.Pretty ( prettyShow )
 import Agda.Syntax.Common ( hasQuantityω )
 import Agda.Utils.Monad (guardWithError, whenM, ifNotM)
-import Agda.Utils.Treeless ( alwaysInline )
+import Agda.Utils.Treeless ( alwaysInline, Erasure )
 
 import Agda.Utils ( treeless, pp, isRecordProjection, isPiTy, etaExpand, isFunction )
 import Agda2Lambox.Compile.Target
@@ -40,9 +40,9 @@ import Agda.TypeChecking.Substitute ( TelV(theCore, theTel) )
 
 
 -- | Convert a function body to a λ□ term.
-compileFunctionBody :: [QName] -> Definition -> CompileM LBox.Term
-compileFunctionBody ms Defn{defName, defType} = do
-  Just t <- liftTCM $ treeless defName
+compileFunctionBody :: Erasure -> [QName] -> Definition -> CompileM LBox.Term
+compileFunctionBody er ms Defn{defName, defType} = do
+  Just t <- liftTCM $ treeless er defName
   reportSDoc "agda2lambox.compile.function" 10 $
     "treeless body:" <+> pretty t
   -- fixpoint bodies must always be lambdas, so η-expand recursive functions of
@@ -65,8 +65,8 @@ type MutualGraph = Map QName (Set QName)
 --
 -- NB: see the discussion on Agda issue #8111 on why @funMutuals@ is not enough,
 -- i.e. the positivity checker misses some calls on agruments it deems unused.
-recursiveGroup :: Definition -> TCM [QName]
-recursiveGroup Defn{defName, defMutual = block} =
+recursiveGroup :: Erasure -> Definition -> TCM [QName]
+recursiveGroup er Defn{defName, defMutual = block} =
   explore M.empty [defName] >>= pure . extractGroup
   where
   explore :: MutualGraph -> [QName] -> TCM MutualGraph
@@ -78,7 +78,7 @@ recursiveGroup Defn{defName, defMutual = block} =
     = calls q >>= \cs -> explore (M.insert q cs gr) (S.toList cs ++ qs)
 
   calls :: QName -> TCM (Set QName)
-  calls q = treeless q >>= \case
+  calls q = treeless er q >>= \case
     Nothing -> pure S.empty
     Just t  -> S.fromList <$> filterM inBlock (S.toList $ namesIn t)
 
@@ -96,7 +96,8 @@ recursiveGroup Defn{defName, defMutual = block} =
 compileFunction :: Target t -> Definition -> CompileM (Maybe (LBox.GlobalDecl t))
 compileFunction (t :: Target t) defn@Defn{defType} =
   ifNotM (liftTCM $ shouldCompileFunction defn) (pure Nothing) do
-  mnames <- liftTCM $ recursiveGroup defn
+  let er = targetErasure t
+  mnames <- liftTCM $ recursiveGroup er defn
   mdefs  <- liftTCM $ mapM getConstInfo mnames
   reportSDoc "agda2lambox.compile.function" 5 $
     "Recursive group:" <+> prettyTCM mnames
@@ -121,7 +122,7 @@ compileFunction (t :: Target t) defn@Defn{defType} =
       builder = Just . ConstantDecl . ConstantBody typ . Just
 
   -- if the function is not recursive, just compile the body
-  if null mdefs then builder <$> compileFunctionBody [] defn
+  if null mdefs then builder <$> compileFunctionBody er [] defn
 
   -- otherwise, take fixpoint
   else do
@@ -129,7 +130,7 @@ compileFunction (t :: Target t) defn@Defn{defType} =
 
     builder . flip LBox.LFix k <$>
       forM mdefs \def@Defn{defName} -> do
-        body <- compileFunctionBody mnames def >>= \case
+        body <- compileFunctionBody er mnames def >>= \case
           l@LBox.LLambda{} -> pure l
           LBox.LBox        -> pure $ LBox.LLambda LBox.Anon LBox.LBox
           _                -> genericError "Fixpoint body must be Lambda."
diff --git a/src/Agda2Lambox/Compile/Utils.hs b/src/Agda2Lambox/Compile/Utils.hs
index 630049b..32e0e72 100644
--- a/src/Agda2Lambox/Compile/Utils.hs
+++ b/src/Agda2Lambox/Compile/Utils.hs
@@ -22,7 +22,9 @@ import Agda.TypeChecking.Telescope ( telView, telViewUpTo, flattenTel )
 import Agda.Utils.Monad ( orM, andM, filterM, forM )
 
 import Agda.Utils ( getInductiveParams, isDataOrRecDef, isArity, dataOrRecMutuals )
+import Agda.Utils.Erase ( Erasure(..) )
 import Agda2Lambox.Compile.Monad
+import Agda2Lambox.Compile.Target
 import LambdaBox qualified as LBox
 
 -- | Convert an Agda module name to its "equivalent" λ□ module path.
@@ -134,3 +136,11 @@ instance MayBeLogical a => MayBeLogical (Dom a) where
 instance MayBeLogical a => MayBeLogical (Arg a) where
   isLogical arg | not (usableModality arg) = pure True
   isLogical arg = isLogical $ unArg arg
+
+-- | What the treeless translation erases for each target:
+--   typed output keeps all values whose types it keeps.
+targetErasure :: Target t -> Erasure
+targetErasure ToUntyped = EraseAll
+targetErasure ToTyped   = EraseLogical \q -> do
+  Defn{defArgInfo, defType} <- getConstInfo q
+  isLogical $ Arg defArgInfo defType
diff --git a/test/untyped/EtaCon.agda b/test/untyped/EtaCon.agda
index 4ca86d0..9ea1925 100644
--- a/test/untyped/EtaCon.agda
+++ b/test/untyped/EtaCon.agda
@@ -10,9 +10,9 @@ addone = suc
 cons : {A : Set} → A → List A → List A
 cons = _∷_
 
-example : List Nat
-example = cons 1 []
-{-# COMPILE AGDA2LAMBOX example #-}
+test : List Nat
+test = cons 1 []
+{-# COMPILE AGDA2LAMBOX test #-}
 
-_ : example ≡ 1 ∷ []
+_ : test ≡ 1 ∷ []
 _ = refl
diff --git a/test/untyped/Fannkuch.agda b/test/untyped/Fannkuch.agda
index 24605e6..cb928b3 100644
--- a/test/untyped/Fannkuch.agda
+++ b/test/untyped/Fannkuch.agda
@@ -16,7 +16,7 @@ open import Agda.Builtin.Maybe
 open import Agda.Builtin.List
 open import Agda.Builtin.Bool
 open import Agda.Builtin.Equality
-open import Prelude
+open import Prelude hiding (test)
 
 -- Reverse the first n elements of a list, keeping the rest
 
diff --git a/test/untyped/Prelude.agda b/test/untyped/Prelude.agda
index 5b6058d..270b78e 100644
--- a/test/untyped/Prelude.agda
+++ b/test/untyped/Prelude.agda
@@ -139,10 +139,10 @@ reverse l = reverseAux l []
 appendTR : List A -> List A -> List A
 appendTR l1 l2 = reverseAux (reverse l1) l2
 
-test′ : Nat
-test′ = length (appendTR (reverse (range n)) (invrange n))
+test : Nat
+test = length (appendTR (reverse (range n)) (invrange n))
   module _ where private n = 21
-{-# COMPILE AGDA2LAMBOX test′ #-}
+{-# COMPILE AGDA2LAMBOX test #-}
 
-_ : test′ ≡ 42
+_ : test ≡ 42
 _ = refl

From 60e8050c027d385291da6750e794a3bda5f3f2fa Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Sun, 1 Nov 2026 22:34:42 +0000
Subject: [PATCH 2/5] --typed: type aliases (or reduce if not alias)

---
 src/Agda/Utils.hs                     | 11 ++++++++++-
 src/Agda2Lambox/Compile.hs            | 14 ++++++++++----
 src/Agda2Lambox/Compile/Type.hs       | 26 ++++++++++++++++++--------
 src/Agda2Lambox/Compile/TypeScheme.hs | 22 +++++-----------------
 4 files changed, 43 insertions(+), 30 deletions(-)

diff --git a/src/Agda/Utils.hs b/src/Agda/Utils.hs
index 653c08d..4c85666 100644
--- a/src/Agda/Utils.hs
+++ b/src/Agda/Utils.hs
@@ -11,7 +11,7 @@ import Data.Text ( Text )
 
 import Agda.Compiler.Backend ( getUniqueCompilerPragma, PureTCM, HasConstInfo (getConstInfo) )
 import Agda.Syntax.Abstract.Name
-import Agda.Syntax.Common ( defaultArg )
+import Agda.Syntax.Common ( defaultArg, namedThing, unArg )
 import Agda.Syntax.Internal
 import Agda.TypeChecking.Monad.Base hiding ( conArity )
 import Agda.TypeChecking.Datatypes ( getConstructorInfo, ConstructorInfo(..) )
@@ -114,6 +114,15 @@ isRecordProjection d
   | otherwise
   = Nothing
 
+-- | Whether a type-level function is compiled to a type alias:
+--   it has a single clause, whose patterns are variables.
+isTypeAlias :: Defn -> Bool
+isTypeAlias = \case
+  Function{funClauses = [cl]} ->
+    all (isVarP . namedThing . unArg) (namedClausePats cl) && isJust (clauseBody cl)
+  _ -> False
+  where isVarP = \case VarP{} -> True; _ -> False
+
 -- | Try to unfold a definition if introduced by module application.
 maybeUnfoldCopy
   :: PureTCM m
diff --git a/src/Agda2Lambox/Compile.hs b/src/Agda2Lambox/Compile.hs
index f160c7d..c812b7a 100644
--- a/src/Agda2Lambox/Compile.hs
+++ b/src/Agda2Lambox/Compile.hs
@@ -32,6 +32,7 @@ import LambdaBox ( emptyName, emptyDecl )
 import LambdaBox.Names
 import LambdaBox.Env (GlobalEnv(..), GlobalDecl(..), ConstantBody(..))
 import LambdaBox.Term (Term(LBox))
+import LambdaBox.Type (Type(TBox))
 
 
 
@@ -61,12 +62,12 @@ compileDefinition target defn@Defn{..} = setCurrentRange defName do
 
   -- TODO: check that we indeed don't compile defs marked with @0
   --       especially record projections for erased fields
-  -- logical definitions are immediately compiled to □,
+  -- logical definitions are immediately compiled to □ (of type □),
   -- except constructors, which are compiled as part of their datatype
   ifM (case theDef of
          Constructor{} -> pure False
          _             -> liftTCM $ isLogical $ Arg defArgInfo defType)
-     (do typ <- whenTyped target $ compileTopLevelType defType
+     (do typ <- whenTyped target $ pure ([], TBox)
          pure $ Just $ ConstantDecl $ ConstantBody typ $ Just LBox) do
 
   case theDef of
@@ -74,8 +75,13 @@ compileDefinition target defn@Defn{..} = setCurrentRange defName do
     GeneralizableVar{} -> pure Nothing
 
     Axiom{} -> do
-      typ <- whenTyped target $ compileTopLevelType defType
-      pure $ Just $ ConstantDecl $ ConstantBody typ Nothing
+      isType <- liftTCM $ isArity defType
+      case target of
+        -- a postulated type is a type alias without definition
+        ToTyped | isType -> pure $ Just $ TypeAliasDecl Nothing
+        _ -> do
+          typ <- whenTyped target $ compileTopLevelType defType
+          pure $ Just $ ConstantDecl $ ConstantBody typ Nothing
 
     Constructor{conData} -> Nothing <$ requireDef conData
 
diff --git a/src/Agda2Lambox/Compile/Type.hs b/src/Agda2Lambox/Compile/Type.hs
index f698c9d..32998c7 100644
--- a/src/Agda2Lambox/Compile/Type.hs
+++ b/src/Agda2Lambox/Compile/Type.hs
@@ -32,7 +32,8 @@ import qualified LambdaBox as LBox
 import Agda2Lambox.Compile.Utils
 import Agda2Lambox.Compile.Monad
 import Agda.Compiler.Backend (HasConstInfo(getConstInfo), Definition(Defn), AddContext (addContext))
-import Agda.Utils (isDataOrRecDef, getInductiveParams, isArity, maybeUnfoldCopy)
+import Agda.Utils (isDataOrRecDef, getInductiveParams, isArity, maybeUnfoldCopy, isFunDef, isTypeAlias)
+import Agda.TypeChecking.Reduce ( reduce )
 
 
 -- | The kind of variables that are locally bound
@@ -190,19 +191,19 @@ compileTypeTerm t = do
         ([],) . foldl' LBox.TApp (LBox.TInd ind)
           <$> compileElims defType (take (getInductiveParams def) args)
 
+      -- a type-level function that is not an alias is compiled to its reduct, if any
+      else if isFunDef def && not (isTypeAlias def) then
+        liftTCM (reduce $ Def q es) >>= \case
+          Def q' _ | q' == q -> typeScheme q defType es
+          t'                 -> compileTypeTerm t'
+
       -- otherwise, it must have been compiled as a type scheme,
       -- and therefore is kept with all arguments.
 
       -- TODO(flupe): check whether indeed the fallback is always compiled to a typescheme.
       --              what about non-logical defs that are not arities or w/?
       -- TODO(flupe): possibly merge the logic with the above for datatypes
-      else do
-        q <- liftTCM $ canonicalName q
-        lift $ requireDef q
-        let ts = qnameToKName q
-        let args = mapMaybe isApplyElim es
-        ([],) . foldl' LBox.TApp (LBox.TConst ts)
-          <$> compileElims defType args
+      else typeScheme q defType es
 
     Pi dom codom -> do
       let domType   = unDom dom
@@ -225,3 +226,12 @@ compileTypeTerm t = do
         pure (name : vars, LBox.TArr LBox.TBox codomType')
 
     _ -> pure ([], LBox.TAny)
+
+-- | Compile the application of a type scheme, keeping all arguments.
+typeScheme :: QName -> Type -> Elims -> C ([LBox.Name], LBox.Type)
+typeScheme q defType es = do
+  q <- liftTCM $ canonicalName q
+  lift $ requireDef q
+  let args = mapMaybe isApplyElim es
+  ([],) . foldl' LBox.TApp (LBox.TConst $ qnameToKName q)
+    <$> compileElims defType args
diff --git a/src/Agda2Lambox/Compile/TypeScheme.hs b/src/Agda2Lambox/Compile/TypeScheme.hs
index a5bbf87..a8eb143 100644
--- a/src/Agda2Lambox/Compile/TypeScheme.hs
+++ b/src/Agda2Lambox/Compile/TypeScheme.hs
@@ -2,7 +2,6 @@
 module Agda2Lambox.Compile.TypeScheme where
 
 import Control.Monad.IO.Class ( liftIO )
-import Data.Maybe ( isJust )
 
 import Agda.Syntax.Internal
 import Agda.Syntax.Common
@@ -12,6 +11,7 @@ import Agda.TypeChecking.Telescope ( telView )
 import Agda.TypeChecking.Substitute ( TelV(TelV), absBody )
 import Agda.TypeChecking.Functions ( etaExpandClause )
 
+import Agda.Utils ( isTypeAlias )
 import Agda2Lambox.Compile.Monad
 import Agda2Lambox.Compile.Target
 import Agda2Lambox.Compile.Utils
@@ -29,15 +29,6 @@ import LambdaBox.Type qualified as LBox
  3. we eta-expand the body.
  -}
 
--- NOTE(flupe): may be fine with dot patterns or something, let's not care right now
--- | Checks that all the patterns of a clause are single-variables
-onlyVarsPat :: NAPs -> Bool
-onlyVarsPat =
-  all \(namedThing . unArg -> x) ->
-    case x of
-      VarP{} -> True
-      _      -> False
-
 compileTele :: Tele (Dom Type) -> CompileM [TypeVarInfo]
 compileTele EmptyTel = pure []
 compileTele (ExtendTel t tel) = do
@@ -49,11 +40,10 @@ compileTypeScheme :: Definition -> CompileM (GlobalDecl Typed)
 compileTypeScheme Defn{..} = do
   reportSDoc "agda2lambox.compile.typescheme" 5 $ "Compiling type scheme:" <+> prettyTCM defName
   TelV tyargs _ <- telView defType
+  tvarInfo <- compileTele tyargs
   let Function{..} = theDef
   case funClauses of
-    [cl]
-      | onlyVarsPat (namedClausePats cl)
-      , isJust (clauseBody cl) -> do
+    [cl] | isTypeAlias theDef -> do
 
       -- We eta-expand the clause to maximal arity by inserting variable patterns
       -- and applying the body to variables.
@@ -66,12 +56,10 @@ compileTypeScheme Defn{..} = do
         Just body = clauseBody cl
 
       (_, res) <- addContext (KeepNames $ clauseTel cl) $ runCNoVars nvars $ compileTypeTerm body
-      tvarInfo <- compileTele tyargs
 
       pure $ TypeAliasDecl $ Just (tvarInfo, res)
 
-    -- if there isn't exactly one clause, we give up
-    -- compiling the type alias and return TAny
+    -- otherwise, we give up compiling the type alias and return TAny
     _ -> do
       reportSDoc "agda2lambox.compile.typescheme" 5 "Could not compile type scheme. Defaulting to TAny."
-      pure $ TypeAliasDecl $ Just ([], LBox.TAny)
+      pure $ TypeAliasDecl $ Just (tvarInfo, LBox.TAny)

From 611b62a6e9e66ec67a9812fa5933688261c26a40 Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Sun, 1 Nov 2026 22:37:50 +0000
Subject: [PATCH 3/5] --typed: preserve types of projections (with their record
 telescope)

---
 src/Agda2Lambox/Compile/Function.hs | 21 ++++++---------------
 src/LambdaBox/Type.hs               |  5 +++++
 2 files changed, 11 insertions(+), 15 deletions(-)

diff --git a/src/Agda2Lambox/Compile/Function.hs b/src/Agda2Lambox/Compile/Function.hs
index ec870c2..6f077c8 100644
--- a/src/Agda2Lambox/Compile/Function.hs
+++ b/src/Agda2Lambox/Compile/Function.hs
@@ -14,14 +14,11 @@ import Data.Maybe ( fromMaybe )
 import Data.Set ( Set )
 import Data.Set qualified as S
 
-import Data.Foldable (toList)
 import Agda.Syntax.Abstract.Name ( QName, qnameModule )
 import Agda.TypeChecking.Monad.Base hiding ( None )
 import Agda.TypeChecking.Pretty
 import Agda.Compiler.Backend ( getConstInfo, reportSDoc )
-import Agda.Syntax.Internal (domName)
 import Agda.Syntax.Internal.Names ( namesIn )
-import Agda.Syntax.Common.Pretty ( prettyShow )
 import Agda.Syntax.Common ( hasQuantityω )
 import Agda.Utils.Monad (guardWithError, whenM, ifNotM)
 import Agda.Utils.Treeless ( alwaysInline, Erasure )
@@ -31,12 +28,12 @@ import Agda2Lambox.Compile.Target
 import Agda2Lambox.Compile.Utils
 import Agda2Lambox.Compile.Monad
 import Agda2Lambox.Compile.Term ( compileTerm )
-import Agda2Lambox.Compile.Type ( compileTopLevelType, compileType )
+import Agda2Lambox.Compile.Type ( compileTopLevelType )
 
 import LambdaBox qualified as LBox
 import LambdaBox.Env
 import Agda.TypeChecking.Telescope ( telViewUpTo )
-import Agda.TypeChecking.Substitute ( TelV(theCore, theTel) )
+import Agda.TypeChecking.Substitute ( TelV(..), telePi )
 
 
 -- | Convert a function body to a λ□ term.
@@ -107,16 +104,10 @@ compileFunction (t :: Target t) defn@Defn{defType} =
 
     -- if it is a (real) projection, drop the parameters from the type
     Just (recName, _) -> do
-      Record{recPars} <- fmap theDef $ liftTCM $ getConstInfo recName
-      projTel <- telViewUpTo recPars defType
-      projType <- theCore <$> telViewUpTo recPars defType
-      let names  = map domName $ toList $ theTel projTel
-          pnames = map (maybe LBox.Anon (LBox.Named . prettyShow)) names
-      (pnames,) <$> compileType recPars projType
-
-    -- TODO(flupe): ^ take care of projection-like functions
-    --                they should be eta-expanded somehow,
-    --                OR treated like projections
+      Defn{defType = recType, theDef = Record{recPars}} <- liftTCM $ getConstInfo recName
+      TelV pars _      <- telViewUpTo recPars recType
+      TelV _ projType  <- telViewUpTo recPars defType
+      fmap (LBox.dropArrows recPars) <$> compileTopLevelType (telePi pars projType)
 
   let builder :: LBox.Term -> Maybe (LBox.GlobalDecl t)
       builder = Just . ConstantDecl . ConstantBody typ . Just
diff --git a/src/LambdaBox/Type.hs b/src/LambdaBox/Type.hs
index 153e5d1..a917317 100644
--- a/src/LambdaBox/Type.hs
+++ b/src/LambdaBox/Type.hs
@@ -16,6 +16,11 @@ data Type
   | TInd Inductive
   | TConst KerName
 
+-- | Drop the first @n@ domains of a function type.
+dropArrows :: Int -> Type -> Type
+dropArrows n (TArr _ t) | n > 0 = dropArrows (n - 1) t
+dropArrows _ t = t
+
 instance Pretty Type where
   prettyPrec p = \case
     TBox         -> "□"

From e5a087db1cbf210e8f86507718d394efb4d9b368 Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Sun, 1 Nov 2026 22:39:48 +0000
Subject: [PATCH 4/5] main: only compile reachable definitions

---
 README.md   |  4 +++-
 src/Main.hs | 27 ++++++++++++++++-----------
 2 files changed, 19 insertions(+), 12 deletions(-)

diff --git a/README.md b/README.md
index d2a5a6f..7a00cd4 100644
--- a/README.md
+++ b/README.md
@@ -18,9 +18,11 @@ cabal install
 ```
 
 ```
-agda2lambox [AGDAFLAGS] [--out-dir DIR] [--typed] [--no-blocks] FILE
+agda2lambox [AGDAFLAGS] [--out-dir DIR] [--typed] [--rocq] [--export-all] FILE
 ```
 
+Only the definitions reachable from those marked with `{-# COMPILE AGDA2LAMBOX f #-}` get compiled; to extract a library instead, `--export-all` compiles the whole module.
+
 Then, use the [following tool][Peregrine] to further compile the generated `.ast` files to WASM, Rust, OCaml, C, and Elm.
 
 ## Setup
diff --git a/src/Main.hs b/src/Main.hs
index 157e765..dcd5c89 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -32,7 +32,6 @@ import Agda2Lambox.Compile ( compile )
 import CodeGen.Rocq ( prettyRocq  )
 import CodeGen.SExpr ( prettySexp )
 import LambdaBox.Env
-import LambdaBox.Names ( KerName )
 import Agda2Lambox.Compile.Monad ( runCompile, CompileEnv(..) )
 
 
@@ -47,10 +46,11 @@ data Options = forall t. Options
   { optOutDir   :: Maybe FilePath
   , optTarget   :: Target t
   , optOutputs  :: [Output]
+  , optLibrary  :: Bool
   }
 
 instance NFData Options where
-  rnf (Options m t o) = rnf m `seq` rnf t `seq` rnf o
+  rnf (Options m t o l) = rnf m `seq` rnf t `seq` rnf o `seq` rnf l
 
 -- | Setter for output directory option.
 outdirOpt :: Monad m => FilePath -> Options -> m Options
@@ -62,12 +62,16 @@ typedOpt opts = return opts { optTarget = ToTyped }
 rocqOpt :: Monad m => Options -> m Options
 rocqOpt opts = return opts { optOutputs = RocqOutput : optOutputs opts }
 
+libraryOpt :: Monad m => Options -> m Options
+libraryOpt opts = return opts { optLibrary = True }
+
 -- | Default backend options.
 defaultOptions :: Options
 defaultOptions  = Options
   { optOutDir   = Nothing
   , optTarget   = ToUntyped
   , optOutputs  = [AstOutput]
+  , optLibrary  = False
   }
 
 -- | Backend module environments.
@@ -92,6 +96,8 @@ agda2lambox = Backend backend
             "Compile to typed λ□ environments."
           , Option ['c'] ["rocq"] (NoArg rocqOpt)
             "Output a Rocq file."
+          , Option ['a'] ["export-all"] (NoArg libraryOpt)
+            "Compile every definition of the module, not only those reachable from a COMPILE pragma (to extract a library)."
           ]
       , isEnabled             = \ _ -> True
       , preCompile            = return
@@ -120,10 +126,14 @@ writeModule Options{..} menv IsMain m defs = do
   outDir   <- flip fromMaybe optOutDir <$> compileDir
   programs <- filterM hasPragma defs
 
-  -- get defs annotated with a COMPILE pragma
-  -- throw an error if none, when targetting untyped lbox
-  mains    <- getMain optTarget programs
-  env      <- runCompile CompileEnv $ compile optTarget defs
+  when (null programs && not optLibrary) $ genericError
+    "No main program specified. Please use a COMPILE pragma, or --export-all to extract a library."
+
+  -- only compile what is reachable from the programs, unless extracting a library
+  let roots = if optLibrary then defs else programs
+  env      <- runCompile CompileEnv $ compile optTarget roots
+
+  let mains = map qnameToKName programs
 
   liftIO $ createDirectoryIfMissing True outDir
 
@@ -143,8 +153,3 @@ writeModule Options{..} menv IsMain m defs = do
     putStrLn $ "Writing " <> fileName -<.> ".v"
     prettyRocq optTarget lboxMod <> "\n"
       & writeFile (fileName -<.> ".v")
-
-  where
-    getMain :: Target t -> [QName] -> TCM [KerName]
-    getMain ToUntyped [] = genericError "No main program specified. Please use a COMPILE pragma."
-    getMain _         qs = pure $ map qnameToKName qs

From f5ff66c7b186297afd1a498e68bc2e6e97c41a3f Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Sat, 31 Oct 2026 01:38:43 +0000
Subject: [PATCH 5/5] cleanup: unused imports/extension + tighter bounds

---
 agda2lambox.cabal                       |  49 +--
 src/Agda/Utils.hs                       |  15 +-
 src/Agda/Utils/EliminateDefaults.hs     |   1 -
 src/Agda/Utils/EtaExpandConstructors.hs |   2 -
 src/Agda/Utils/Simplify.hs              | 528 ------------------------
 src/Agda/Utils/Treeless.hs              |   6 +-
 src/Agda2Lambox/Compile.hs              |  12 +-
 src/Agda2Lambox/Compile/Function.hs     |  11 +-
 src/Agda2Lambox/Compile/Inductive.hs    |   3 -
 src/Agda2Lambox/Compile/Monad.hs        |   7 +-
 src/Agda2Lambox/Compile/Target.hs       |   1 -
 src/Agda2Lambox/Compile/Term.hs         |  15 +-
 src/Agda2Lambox/Compile/Type.hs         |  15 +-
 src/Agda2Lambox/Compile/TypeScheme.hs   |   6 +-
 src/Agda2Lambox/Compile/Utils.hs        |  11 +-
 src/CodeGen/Rocq.hs                     |   5 +-
 src/CodeGen/SExpr.hs                    |   7 +-
 src/LambdaBox.hs                        |   1 -
 src/LambdaBox/Names.hs                  |   1 -
 src/Main.hs                             |   9 +-
 test/Main.hs                            |   5 +-
 21 files changed, 49 insertions(+), 661 deletions(-)
 delete mode 100644 src/Agda/Utils/Simplify.hs

diff --git a/agda2lambox.cabal b/agda2lambox.cabal
index ebec092..f932262 100644
--- a/agda2lambox.cabal
+++ b/agda2lambox.cabal
@@ -21,7 +21,6 @@ executable agda2lambox
                        Agda.Utils.EliminateDefaults,
                        Agda.Utils.Erase,
                        Agda.Utils.EtaExpandConstructors,
-                       Agda.Utils.Simplify,
                        Agda.Utils.Treeless,
                        Agda.Utils.ThunkLets,
                        Agda2Lambox.Compile.Target,
@@ -42,45 +41,33 @@ executable agda2lambox
                        CodeGen.SExpr,
                        Paths_agda2lambox
   autogen-modules:     Paths_agda2lambox
-  build-depends:       base       >= 4.10  && < 4.22,
-                       Agda       >= 2.8   && < 2.9,
-                       deepseq    >= 1.4.4 && < 1.6,
-                       sexpresso  >= 1.2.5 && < 1.3,
-                       pretty-show,
-                       containers,
-                       directory,
-                       filepath,
-                       text,
-                       mtl
+  build-depends:       base       >= 4.20    && < 4.22,
+                       Agda       >= 2.8     && < 2.9,
+                       deepseq    >= 1.5     && < 1.6,
+                       sexpresso  >= 1.2.5   && < 1.3,
+                       containers >= 0.7     && < 0.8,
+                       directory  >= 1.3.8.3 && < 1.4,
+                       filepath   >= 1.5.2   && < 1.6,
+                       text       >= 2.1.1   && < 2.2,
+                       mtl        >= 2.3.1   && < 2.4
   default-language:    Haskell2010
   default-extensions:
     LambdaCase RecordWildCards PatternSynonyms TupleSections
-    ViewPatterns PatternGuards
-    ScopedTypeVariables
-    TypeFamilies TypeOperators TypeApplications
-    FunctionalDependencies TypeSynonymInstances ConstraintKinds
-    DoAndIfThenElse BlockArguments MultiWayIf
-    ImportQualifiedPost NamedFieldPuns
+    ScopedTypeVariables TypeFamilies MultiParamTypeClasses
+    BlockArguments MultiWayIf ImportQualifiedPost NamedFieldPuns
 
 test-suite agda2lambox-tests
   type:                exitcode-stdio-1.0
   hs-source-dirs:      test
   main-is:             Main.hs
-  build-depends:       base       >= 4.10  && < 4.22,
-                       tasty      >= 1.4   && < 1.6,
-                       tasty-hunit >= 0.10 && < 0.11,
-                       process    >= 1.6   && < 1.7,
-                       filepath   >= 1.4   && < 1.5,
-                       directory  >= 1.3   && < 1.4,
-                       text       >= 1.2   && < 2.2
+  build-depends:       base        >= 4.20    && < 4.22,
+                       tasty       >= 1.4.2.2 && < 1.6,
+                       tasty-hunit >= 0.10    && < 0.11,
+                       process     >= 1.6.19  && < 1.7,
+                       filepath    >= 1.5.2   && < 1.6,
+                       directory   >= 1.3.8.3 && < 1.4
   build-tool-depends:  agda2lambox:agda2lambox
   default-language:    Haskell2010
   default-extensions:
-    LambdaCase RecordWildCards PatternSynonyms TupleSections
-    ViewPatterns PatternGuards
-    ScopedTypeVariables
-    TypeFamilies TypeOperators TypeApplications
-    FunctionalDependencies TypeSynonymInstances ConstraintKinds
-    DoAndIfThenElse BlockArguments MultiWayIf
-    ImportQualifiedPost
+    TupleSections BlockArguments
 
diff --git a/src/Agda/Utils.hs b/src/Agda/Utils.hs
index 4c85666..a85ad50 100644
--- a/src/Agda/Utils.hs
+++ b/src/Agda/Utils.hs
@@ -1,12 +1,10 @@
-{-# LANGUAGE FlexibleContexts, OverloadedStrings, BangPatterns, NamedFieldPuns #-}
+{-# LANGUAGE OverloadedStrings #-}
 
 -- | Agda utilities.
 module Agda.Utils where
 
-import Control.Applicative ( liftA2 )
-import Data.Bifunctor ( second )
 import Data.Functor ( (<&>) )
-import Data.Maybe ( isJust, isNothing, catMaybes, fromMaybe )
+import Data.Maybe ( isJust, catMaybes, fromMaybe )
 import Data.Text ( Text )
 
 import Agda.Compiler.Backend ( getUniqueCompilerPragma, PureTCM, HasConstInfo (getConstInfo) )
@@ -14,22 +12,13 @@ import Agda.Syntax.Abstract.Name
 import Agda.Syntax.Common ( defaultArg, namedThing, unArg )
 import Agda.Syntax.Internal
 import Agda.TypeChecking.Monad.Base hiding ( conArity )
-import Agda.TypeChecking.Datatypes ( getConstructorInfo, ConstructorInfo(..) )
 import Agda.TypeChecking.Substitute ( raise, TelV (theCore) )
 import Agda.Syntax.Common.Pretty
 import Agda.Syntax.Treeless
 
-import Agda.Compiler.ToTreeless                 qualified as TT
-import Agda.Compiler.Treeless.Builtin           qualified as TT
-import Agda.Compiler.Treeless.Erase             qualified as TT
-import Agda.Compiler.Treeless.Simplify          qualified as TT
-import Agda.Compiler.Treeless.Identity          qualified as TT
-import Agda.Compiler.Treeless.Uncase            qualified as TT
-import Agda.Compiler.Treeless.AsPatterns        qualified as TT
 import Agda.TypeChecking.Telescope (telView, telViewUpTo)
 import Agda.TypeChecking.Substitute (TelV(theTel))
 
-import Agda.Utils.EliminateDefaults qualified as TT
 import Agda.Utils.Treeless qualified as CustomTT
 import Agda.TypeChecking.Reduce (reduceDefCopy)
 
diff --git a/src/Agda/Utils/EliminateDefaults.hs b/src/Agda/Utils/EliminateDefaults.hs
index d112b83..c6155e8 100644
--- a/src/Agda/Utils/EliminateDefaults.hs
+++ b/src/Agda/Utils/EliminateDefaults.hs
@@ -12,7 +12,6 @@ module Agda.Utils.EliminateDefaults where
 
 import Control.Monad
 import qualified Data.List as List
-import Control.Monad.IO.Class (liftIO)
 
 import Agda.Syntax.Treeless
 import Agda.TypeChecking.Monad
diff --git a/src/Agda/Utils/EtaExpandConstructors.hs b/src/Agda/Utils/EtaExpandConstructors.hs
index 94de117..14dce02 100644
--- a/src/Agda/Utils/EtaExpandConstructors.hs
+++ b/src/Agda/Utils/EtaExpandConstructors.hs
@@ -8,8 +8,6 @@ import Agda.TypeChecking.Monad
 import Agda.TypeChecking.Substitute
 import Agda.TypeChecking.Datatypes
 import Agda.Compiler.Treeless.Subst () --instance only
-import Agda.Compiler.Backend
-import Control.Monad.IO.Class (MonadIO(liftIO))
 
 
 -- | Check whether a treeless term is a constructor applied to (many) terms.
diff --git a/src/Agda/Utils/Simplify.hs b/src/Agda/Utils/Simplify.hs
deleted file mode 100644
index 6f215ce..0000000
--- a/src/Agda/Utils/Simplify.hs
+++ /dev/null
@@ -1,528 +0,0 @@
-{-# OPTIONS_GHC -Wunused-imports #-}
-
-module Agda.Utils.Simplify (simplifyTTerm) where
-
-import Control.Arrow        ( (***), second )
-import Control.Monad        ( (>=>), guard )
-import Control.Monad.Reader ( MonadReader(..), asks, Reader, runReader )
-import qualified Data.List as List
-
-import Agda.Syntax.Treeless
-import Agda.Syntax.Literal
-
-import Agda.TypeChecking.Monad
-import Agda.TypeChecking.Primitive
-import Agda.TypeChecking.Substitute
-
-import Agda.Compiler.Treeless.Compare
-
-import Agda.Utils.List
-import Agda.Utils.Maybe
-
-import Agda.Utils.Impossible
-
-data SEnv = SEnv
-  { envSubst   :: Substitution' TTerm
-  , envRewrite :: [(TTerm, TTerm)] }
-
-type S = Reader SEnv
-
-runS :: S a -> a
-runS m = runReader m $ SEnv IdS []
-
-lookupVar :: Int -> S TTerm
-lookupVar i = asks $ (`lookupS` i) . envSubst
-
-onSubst :: (Substitution' TTerm -> Substitution' TTerm) -> S a -> S a
-onSubst f = local $ \ env -> env { envSubst = f (envSubst env) }
-
-onRewrite :: Substitution' TTerm -> S a -> S a
-onRewrite rho = local $ \ env -> env { envRewrite = map (applySubst rho *** applySubst rho) (envRewrite env) }
-
-addRewrite :: TTerm -> TTerm -> S a -> S a
-addRewrite lhs rhs = local $ \ env -> env { envRewrite = (lhs, rhs) : envRewrite env }
-
-underLams :: Int -> S a -> S a
-underLams i = onRewrite (raiseS i) . onSubst (liftS i)
-
-underLam :: S a -> S a
-underLam = underLams 1
-
-underLet :: TTerm -> S a -> S a
-underLet u = onRewrite (raiseS 1) . onSubst (\rho -> wkS 1 $ u :# rho)
-
-bindVar :: Int -> TTerm -> S a -> S a
-bindVar x u = onSubst (inplaceS x u `composeS`)
-
-rewrite :: TTerm -> S TTerm
-rewrite t = do
-  rules <- asks envRewrite
-  case [ rhs | (lhs, rhs) <- rules, equalTerms t lhs ] of
-    rhs : _ -> pure rhs
-    []      -> pure t
-
-data FunctionKit = FunctionKit
-  { modAux, divAux, natMinus, true, false :: Maybe QName }
-
-simplifyTTerm :: TTerm -> TCM TTerm
-simplifyTTerm t = do
-  kit <- FunctionKit <$> getBuiltinName builtinNatModSucAux
-                     <*> getBuiltinName builtinNatDivSucAux
-                     <*> getBuiltinName builtinNatMinus
-                     <*> getBuiltinName builtinTrue
-                     <*> getBuiltinName builtinFalse
-  return $ runS $ simplify kit t
-
-simplify :: FunctionKit -> TTerm -> S TTerm
-simplify FunctionKit{..} = simpl
-  where
-    simpl = rewrite' >=> unchainCase >=> \case
-
-      t@TDef{}  -> pure t
-      t@TPrim{} -> pure t
-      t@TVar{}  -> pure t
-
-      {-
-      TApp (TDef f) [TLit (LitNat 0), m, n, m']
-        -- div/mod are equivalent to quot/rem on natural numbers.
-        | m == m', Just f == divAux -> simpl $ tOp PQuot n (tPlusK 1 m)
-        | m == m', Just f == modAux -> simpl $ tOp PRem n (tPlusK 1 m)
-
-      -- Word64 primitives --
-
-      --  toWord (a ∙ b) == toWord a ∙64 toWord b
-      TPFn PITo64 (TPOp op a b)
-        | Just op64 <- opTo64 op -> simpl $ tOp op64 (TPFn PITo64 a) (TPFn PITo64 b)
-        where
-          opTo64 op = lookup op [(PAdd, PAdd64), (PSub, PSub64), (PMul, PMul64),
-                                 (PQuot, PQuot64), (PRem, PRem64)]
-
--}
-      t@(TApp (TPrim _) _) -> pure t  -- taken care of by rewrite'
-
-      TCoerce t -> TCoerce <$> simpl t
-
-      TApp f es -> do
-        f  <- simpl f
-        es <- traverse simpl es
-        maybeMinusToPrim f es
-      TLam b    -> TLam <$> underLam (simpl b)
-      t@TLit{}  -> pure t
-      t@TCon{}  -> pure t
-      TLet e b  -> do
-        simpl e >>= \case
-          TPFn P64ToI a -> do
-            -- Inline calls to P64ToI since these trigger optimisations.
-            -- Ideally, the optimisations would trigger anyway, but at the
-            -- moment they only do if inlining the entire let looks like a
-            -- good idea.
-            let rho = inplaceS 0 (TPFn P64ToI (TVar 0))
-            tLet a <$> underLet a (simpl (applySubst rho b))
-          e -> tLet e <$> underLet e (simpl b)
-
-      TCase x t d bs -> do
-        v <- lookupVar x
-        let (lets, u) = tLetView v
-        (d, bs) <- pruneBoolGuards d <$> traverse (simplAlt x) bs
-        case u of                          -- TODO: also for literals
-          _ | Just (c, as)     <- conView u   -> simpl $ matchCon lets c as d bs
-            | Just (k, TVar y) <- plusKView u -> simpl . mkLets lets . TCase y t d =<< mapM (matchPlusK y x k) bs
-          TCase y t1 d1 bs1 -> simpl $ mkLets lets $ TCase y t1 (distrDef case1 d1) $
-                                       map (distrCase case1) bs1
-            where
-              -- Γ x Δ -> Γ _ Δ Θ y, where x maps to y and Θ are the lets
-              n     = length lets
-              rho   = liftS (x + n + 1) (raiseS 1)    `composeS`
-                      singletonS (x + n + 1) (TVar 0) `composeS`
-                      raiseS (n + 1)
-              case1 = applySubst rho (TCase x t d bs)
-
-              distrDef v d | isUnreachable d = tUnreachable
-                           | otherwise       = tLet d v
-
-              distrCase v (TACon c a b) = TACon c a $ TLet b $ raiseFrom 1 a v
-              distrCase v (TALit l b)   = TALit l   $ TLet b v
-              distrCase v (TAGuard g b) = TAGuard g $ TLet b v
-
-          _ -> do
-            d <- simpl d
-            tCase x t d bs
-
-      t@TUnit    -> pure t
-      t@TSort    -> pure t
-      t@TErased  -> pure t
-      t@TError{} -> pure t
-
-    conView (TCon c)    = Just (c, [])
-    conView (TApp f as) = second (++ as) <$> conView f
-    conView e           = Nothing
-
-    -- Collapse chained cases (case x of bs -> vs; _ -> case x of bs' -> vs'  ==>
-    --                         case x of bs -> vs; bs' -> vs')
-    unchainCase :: TTerm -> S TTerm
-    unchainCase e@(TCase x t d bs) = do
-      let (lets, u) = tLetView d
-          k = length lets
-      return $ case u of
-        TCase y _ d' bs' | x + k == y ->
-          mkLets lets $ TCase y t d' $ raise k bs ++ filter (`noOverlap` bs) bs'
-        _ -> e
-    unchainCase e = return e
-
-
-    mkLets es b = foldr TLet b es
-
-    matchCon _ _ _ d [] = d
-    matchCon lets c as d (TALit{}   : bs) = matchCon lets c as d bs
-    matchCon lets c as d (TAGuard{} : bs) = matchCon lets c as d bs
-    matchCon lets c as d (TACon c' a b : bs)
-      | c == c'        = flip (foldr TLet) lets $ mkLet 0 as (raiseFrom a (length lets) b)
-      | otherwise      = matchCon lets c as d bs
-      where
-        mkLet _ []       b = b
-        mkLet i (a : as) b = TLet (raise i a) $ mkLet (i + 1) as b
-
-    -- Simplify let y = x + k in case y of j     -> u; _ | g[y]     -> v
-    -- to       let y = x + k in case x of j - k -> u; _ | g[x + k] -> v
-    matchPlusK :: Int -> Int -> Integer -> TAlt -> S TAlt
-    matchPlusK x y k (TALit (LitNat j) b) = return $ TALit (LitNat (j - k)) b
-    matchPlusK x y k (TAGuard g b) = flip TAGuard b <$> simpl (applySubst (inplaceS y (tPlusK k (TVar x))) g)
-    matchPlusK x y k TACon{} = __IMPOSSIBLE__
-    matchPlusK x y k TALit{} = __IMPOSSIBLE__
-
-    simplPrim (TApp f@TPrim{} args) = do
-        args    <- mapM simpl args
-        inlined <- mapM inline args
-        let u = TApp f args
-            v = simplPrim' (TApp f inlined)
-        pure $ if v `betterThan` u then v else u
-      where
-        inline (TVar x)                   = do
-          v <- lookupVar x
-          if v == TVar x then pure v else inline v
-        inline (TApp f@TPrim{} args)      = TApp f <$> mapM inline args
-        inline u@(TLet _ (TCase 0 _ _ _)) = pure u
-        inline (TLet e b)                 = inline (subst 0 e b)
-        inline u                          = pure u
-    simplPrim t = pure t
-
-    simplPrim' :: TTerm -> TTerm
-    simplPrim' (TApp (TPrim PSeq) (u : v : vs))
-      | u == v             = mkTApp v vs
-      | TApp TCon{} _ <- u = mkTApp v vs
-      | TApp TLit{} _ <- u = mkTApp v vs
-    simplPrim' (TApp (TPrim PLt) [u, v])
-      | Just (PAdd, k, u) <- constArithView u,
-        Just (PAdd, j, v) <- constArithView v,
-        k == j = tOp PLt u v
-      | Just (PSub, k, u) <- constArithView u,
-        Just (PSub, j, v) <- constArithView v,
-        k == j = tOp PLt v u
-      | Just (PAdd, k, v) <- constArithView v,
-        TApp (TPrim P64ToI) [u] <- u,
-        k >= 2 ^ 64, Just trueCon <- true = TCon trueCon
-      | Just k <- intView u
-      , Just j <- intView v
-      , Just trueCon <- true
-      , Just falseCon <- false = if k < j then TCon trueCon else TCon falseCon
-    simplPrim' (TApp (TPrim PGeq) [u, v])
-      | Just (PAdd, k, u) <- constArithView u,
-        Just (PAdd, j, v) <- constArithView v,
-        k == j = tOp PGeq u v
-      | Just (PSub, k, u) <- constArithView u,
-        Just (PSub, j, v) <- constArithView v,
-        k == j = tOp PGeq v u
-      | Just k <- intView u
-      , Just j <- intView v
-      , Just trueCon <- true
-      , Just falseCon <- false = if k >= j then TCon trueCon else TCon falseCon
-    simplPrim' (TApp (TPrim op) [u, v])
-      | op `elem` [PGeq, PLt, PEqI]
-      , Just (PAdd, k, u) <- constArithView u
-      , Just j <- intView v = TApp (TPrim op) [u, tInt (j - k)]
-    simplPrim' (TApp (TPrim PEqI) [u, v])
-      | Just (op1, k, u) <- constArithView u,
-        Just (op2, j, v) <- constArithView v,
-        op1 == op2, k == j,
-        op1 `elem` [PAdd, PSub] = tOp PEqI u v
-    simplPrim' (TPOp op u v)
-      | zeroL, isMul || isDiv = tInt 0
-      | zeroL, isAdd          = v
-      | zeroR, isMul          = tInt 0
-      | zeroR, isAdd || isSub = u
-      where zeroL = Just 0 == intView u || Just 0 == word64View u
-            zeroR = Just 0 == intView v || Just 0 == word64View v
-            isAdd = op `elem` [PAdd, PAdd64]
-            isSub = op `elem` [PSub, PSub64]
-            isMul = op `elem` [PMul, PMul64]
-            isDiv = op `elem` [PQuot, PQuot64, PRem, PRem64]
-    simplPrim' (TApp (TPrim op) [u, v])
-      | Just u <- negView u,
-        Just v <- negView v,
-        op `elem` [PMul, PQuot] = tOp op u v
-      | Just u <- negView u,
-        op `elem` [PMul, PQuot] = simplArith $ tOp PSub (tInt 0) (tOp op u v)
-      | Just v <- negView v,
-        op `elem` [PMul, PQuot] = simplArith $ tOp PSub (tInt 0) (tOp op u v)
-    simplPrim' (TApp (TPrim PRem) [u, v])
-      | Just u <- negView u  = simplArith $ tOp PSub (tInt 0) (tOp PRem u (unNeg v))
-      | Just v <- negView v  = tOp PRem u v
-
-      -- (fromWord a == fromWord b) = (a ==64 b)
-    simplPrim' (TPOp op (TPFn P64ToI a) (TPFn P64ToI b))
-        | Just op64 <- opTo64 op = tOp op64 a b
-        where
-          opTo64 op = lookup op [(PEqI, PEq64), (PLt, PLt64)]
-
-      -- toWord/fromWord k == fromIntegral k
-    simplPrim' (TPFn PITo64 (TLit (LitNat n)))    = TLit (LitWord64 (fromIntegral n))
-    simplPrim' (TPFn P64ToI (TLit (LitWord64 n))) = TLit (LitNat    (fromIntegral n))
-
-      -- toWord (fromWord a) == a
-    simplPrim' (TPFn PITo64 (TPFn P64ToI a)) = a
-
-    simplPrim' (TApp f@(TPrim op) [u, v]) = simplArith $ TApp f [simplPrim' u, simplPrim' v]
-    simplPrim' u = u
-
-    unNeg u | Just v <- negView u = v
-            | otherwise           = u
-
-    negView (TApp (TPrim PSub) [a, b])
-      | Just 0 <- intView a = Just b
-    negView _ = Nothing
-
-    -- Count arithmetic operations
-    betterThan u v = operations u <= operations v
-      where
-        operations (TApp (TPrim _) [a, b]) = 1 + operations a + operations b
-        operations (TApp (TPrim PSeq) (a : _))
-          | notVar a                       = 1000000  -- only seq on variables!
-        operations (TApp (TPrim _) [a])    = 1 + operations a
-        operations TVar{}                  = 0
-        operations TLit{}                  = 0
-        operations TCon{}                  = 0
-        operations TDef{}                  = 0
-        operations _                       = 1000
-
-        notVar TVar{} = False
-        notVar _      = True
-
-    rewrite' t = rewrite =<< simplPrim t
-
-    constArithView :: TTerm -> Maybe (TPrim, Integer, TTerm)
-    constArithView (TApp (TPrim op) [TLit (LitNat k), u])
-      | op `elem` [PAdd, PSub] = Just (op, k, u)
-    constArithView (TApp (TPrim op) [u, TLit (LitNat k)])
-      | op == PAdd = Just (op, k, u)
-      | op == PSub = Just (PAdd, -k, u)
-    constArithView _ = Nothing
-
-    simplAlt x (TACon c a b) = TACon c a <$> underLams a (maybeAddRewrite (x + a) conTerm $ simpl b)
-      where conTerm = mkTApp (TCon c) $ map TVar $ downFrom a
-    simplAlt x (TALit l b)   = TALit l   <$> maybeAddRewrite x (TLit l) (simpl b)
-    simplAlt x (TAGuard g b) = TAGuard   <$> simpl g <*> simpl b
-
-    -- If x is already bound we add a rewrite, otherwise we bind x to rhs.
-    maybeAddRewrite x rhs cont = do
-      v <- lookupVar x
-      case v of
-        TVar y | x == y -> bindVar x rhs $ cont
-        _ -> addRewrite v rhs cont
-
-    isTrue (TCon c) = Just c == true
-    isTrue _        = False
-
-    isFalse (TCon c) = Just c == false
-    isFalse _        = False
-
-    maybeMinusToPrim f@(TDef minus) es@[a, b]
-      | Just minus == natMinus = do
-      leq  <- checkLeq b a
-      if leq then pure $ tOp PSub a b
-             else tApp f es
-
-    maybeMinusToPrim f es = tApp f es
-
-    tLet (TVar x) b = subst 0 (TVar x) b
-    tLet e (TVar 0) = e
-    tLet e b        = TLet e b
-
-    tCase :: Int -> CaseInfo -> TTerm -> [TAlt] -> S TTerm
-    tCase x t d [] = pure d
-    tCase x t d bs
-      | isUnreachable d =
-        case reverse bs' of
-          [] -> pure d
-          TALit _ b   : as  -> tCase x t b (reverse as)
-          TAGuard _ b : as  -> tCase x t b (reverse as)
-          TACon c a b : _   -> tCase' x t d bs'
-      | otherwise = do
-        d' <- lookupIfVar d
-        case d' of
-          TCase y _ d bs'' | x == y ->
-            tCase x t d (bs' ++ filter (`noOverlap` bs') bs'')
-          _ -> tCase' x t d bs'
-      where
-        bs' = filter (not . isUnreachable) bs
-
-        lookupIfVar (TVar i) = lookupVar i
-        lookupIfVar t = pure t
-
-    noOverlap b bs = not $ any (overlapped b) bs
-
-    overlapped (TACon c _ _)  (TACon c' _ _) = c == c'
-    overlapped (TALit l _)    (TALit l' _)   = l == l'
-    overlapped _              _              = False
-
-    -- Drop unreachable cases for Nat and Int cases.
-    pruneLitCases :: Int -> CaseInfo -> TTerm -> [TAlt] -> S TTerm
-    pruneLitCases x t d bs | CTNat == caseType t =
-      case complete bs [] Nothing of
-        Just bs' -> tCase x t tUnreachable bs'
-        Nothing  -> return $ TCase x t d bs
-      where
-        complete bs small (Just upper)
-          | null $ [0..upper - 1] List.\\ small = Just []
-        complete (b@(TALit (LitNat n) _) : bs) small upper =
-          (b :) <$> complete bs (n : small) upper
-        complete (b@(TAGuard (TApp (TPrim PGeq) [TVar y, TLit (LitNat j)]) _) : bs) small upper | x == y =
-          (b :) <$> complete bs small (Just $ maybe j (min j) upper)
-        complete _ _ _ = Nothing
-
-    pruneLitCases x t d bs
-      | CTInt == caseType t = return $ TCase x t d bs -- TODO
-      | otherwise           = return $ TCase x t d bs
-
-    -- Drop 'false' branches and drop everything after 'true' branches (including the default
-    -- branch)
-    pruneBoolGuards d [] = (d, [])
-    pruneBoolGuards d (b@(TAGuard (TCon c) _) : bs)
-      | Just c == true  = (tUnreachable, [b])
-      | Just c == false = pruneBoolGuards d bs
-    pruneBoolGuards d (b : bs) =
-      second (b :) $ pruneBoolGuards d bs
-
-    tCase' x t d [] = return d
-    tCase' x t d bs = pruneLitCases x t d bs
-
-    tApp :: TTerm -> [TTerm] -> S TTerm
-    tApp (TLet e b) es = TLet e <$> underLet e (tApp b (raise 1 es))
-    tApp (TCase x t d bs) es = do
-      d  <- tApp d es
-      bs <- mapM (`tAppAlt` es) bs
-      simpl $ TCase x t d bs    -- will resimplify branches
-    tApp (TVar x) es = do
-      v <- lookupVar x
-      case v of
-        _ | v /= TVar x && isAtomic v -> tApp v es
-        TLam{} -> tApp v es   -- could blow up the code
-        _      -> pure $ mkTApp (TVar x) es
-    tApp f [] = pure f
-    tApp (TLam b) (TVar i : es) = tApp (subst 0 (TVar i) b) es
-    tApp (TLam b) (e : es) = tApp (TLet e b) es
-    tApp f es = pure $ TApp f es
-
-    tAppAlt (TACon c a b) es = TACon c a <$> underLams a (tApp b (raise a es))
-    tAppAlt (TALit l b) es   = TALit l   <$> tApp b es
-    tAppAlt (TAGuard g b) es = TAGuard g <$> tApp b es
-
-    isAtomic = \case
-      TVar{}    -> True
-      TCon{}    -> True
-      TPrim{}   -> True
-      TDef{}    -> True
-      TLit{}    -> True
-      TSort{}   -> True
-      TErased{} -> True
-      TError{}  -> True
-      _         -> False
-
-    checkLeq a b = do
-      rho  <- asks envSubst
-      rwr  <- asks envRewrite
-      let nf = toArith . applySubst rho
-          less = [ (nf a, nf b) | (TPOp PLt a b, rhs) <- rwr, isTrue  rhs ]
-          leq  = [ (nf b, nf a) | (TPOp PLt a b, rhs) <- rwr, isFalse rhs ]
-
-          match (j, as) (k, bs)
-            | as == bs  = Just (j - k)
-            | otherwise = Nothing
-
-          -- Do we have x ≤ y given x' < y' + d ?
-          matchEqn d x y (x', y') = isJust $ do
-            k <- match x x'     -- x = x' + k
-            j <- match y y'     -- y = y' + j
-            guard (k <= j + d)  -- x ≤ y if k ≤ j + d
-
-          matchLess = matchEqn 1
-          matchLeq  = matchEqn 0
-
-          literal (j, []) (k, []) = j <= k
-          literal _ _ = False
-
-          -- k + fromWord x ≤ y  if  k + 2^64 - 1 ≤ y
-          wordUpperBound (k, [Pos (TApp (TPrim P64ToI) _)]) y = go (k + 2 ^ 64 - 1, []) y
-          wordUpperBound _ _ = False
-
-          -- x ≤ k + fromWord y  if  x ≤ k
-          wordLowerBound a (k, [Pos (TApp (TPrim P64ToI) _)]) = go a (k, [])
-          wordLowerBound _ _ = False
-
-          go x y = or
-            [ literal x y
-            , wordUpperBound x y
-            , wordLowerBound x y
-            , any (matchLess x y) less
-            , any (matchLeq x y) leq ]
-
-      return $ go (nf a) (nf b)
-
-type Arith = (Integer, [Atom])
-
-data Atom = Pos TTerm | Neg TTerm
-  deriving (Show, Eq, Ord)
-
-aNeg :: Atom -> Atom
-aNeg (Pos a) = Neg a
-aNeg (Neg a) = Pos a
-
-aCancel :: [Atom] -> [Atom]
-aCancel (a : as)
-  | (aNeg a) `elem` as = aCancel (List.delete (aNeg a) as)
-  | otherwise          = a : aCancel as
-aCancel [] = []
-
-sortR :: Ord a => [a] -> [a]
-sortR = List.sortBy (flip compare)
-
-aAdd :: Arith -> Arith -> Arith
-aAdd (a, xs) (b, ys) = (a + b, aCancel $ sortR $ xs ++ ys)
-
-aSub :: Arith -> Arith -> Arith
-aSub (a, xs) (b, ys) = (a - b, aCancel $ sortR $ xs ++ map aNeg ys)
-
-fromArith :: Arith -> TTerm
-fromArith (n, []) = tInt n
-fromArith (0, xs)
-  | (ys, Pos a : zs) <- break isPos xs = foldl addAtom a (ys ++ zs)
-fromArith (n, xs)
-  | n < 0, (ys, Pos a : zs) <- break isPos xs =
-    tOp PSub (foldl addAtom a (ys ++ zs)) (tInt (-n))
-fromArith (n, xs) = foldl addAtom (tInt n) xs
-
-isPos :: Atom -> Bool
-isPos Pos{} = True
-isPos Neg{} = False
-
-addAtom :: TTerm -> Atom -> TTerm
-addAtom t (Pos a) = tOp PAdd t a
-addAtom t (Neg a) = tOp PSub t a
-
-toArith :: TTerm -> Arith
-toArith t | Just n <- intView t = (n, [])
-toArith (TApp (TPrim PAdd) [a, b]) = aAdd (toArith a) (toArith b)
-toArith (TApp (TPrim PSub) [a, b]) = aSub (toArith a) (toArith b)
-toArith t = (0, [Pos t])
-
-simplArith :: TTerm -> TTerm
-simplArith = fromArith . toArith
diff --git a/src/Agda/Utils/Treeless.hs b/src/Agda/Utils/Treeless.hs
index b327382..c4f405a 100644
--- a/src/Agda/Utils/Treeless.hs
+++ b/src/Agda/Utils/Treeless.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE NamedFieldPuns, OverloadedStrings #-}
+{-# LANGUAGE OverloadedStrings #-}
 {- NOTE(flupe):
 
 Currently we inline the treeless pipeline from the Agda source.
@@ -45,10 +45,7 @@ import Agda.TypeChecking.Records (getRecordConstructor)
 import Agda.TypeChecking.Reduce
 import Agda.TypeChecking.Substitute
 
-import Agda.Compiler.Treeless.AsPatterns
-import Agda.Compiler.Treeless.Builtin
 import Agda.Compiler.Treeless.Identity
-import Agda.Compiler.Treeless.Simplify
 import Agda.Compiler.Treeless.Uncase
 import Agda.Compiler.Treeless.Unused
 import Agda.Compiler.Treeless.NormalizeNames
@@ -69,7 +66,6 @@ import Agda.Utils.EliminateDefaults
 import Agda.Utils.Erase
 import Agda.Utils.ThunkLets
 import Agda.Utils.EtaExpandConstructors
-import Agda.Utils.Simplify
 
 prettyPure :: P.Pretty a => a -> TCM Doc
 prettyPure = return . P.pretty
diff --git a/src/Agda2Lambox/Compile.hs b/src/Agda2Lambox/Compile.hs
index c812b7a..a76874b 100644
--- a/src/Agda2Lambox/Compile.hs
+++ b/src/Agda2Lambox/Compile.hs
@@ -1,20 +1,13 @@
-{-# LANGUAGE NamedFieldPuns, DataKinds, OverloadedStrings, NondecreasingIndentation #-}
+{-# LANGUAGE OverloadedStrings, NondecreasingIndentation #-}
 module Agda2Lambox.Compile 
   ( compile
   ) where
 
-import Control.Monad.IO.Class ( liftIO )
-import Data.IORef
-
-import Control.Monad.State
-
 import Agda.Compiler.Backend
-import Agda.Syntax.Internal ( QName )
 import Agda.Syntax.Common (Arg(..), IsOpaque (TransparentDef))
 import Agda.Syntax.Common.Pretty ( prettyShow )
-import Agda.TypeChecking.Monad ( liftTCM, getConstInfo )
 import Agda.TypeChecking.Pretty
-import Agda.Utils.Monad ( ifM, ifNotM, orM )
+import Agda.Utils.Monad ( ifM, ifNotM )
 import Agda.Utils.SmallSet qualified as SmallSet
 
 import Agda.Utils ( isDataOrRecDef, isArity, getPragmaInfo )
@@ -22,7 +15,6 @@ import Agda.Utils ( isDataOrRecDef, isArity, getPragmaInfo )
 import Agda2Lambox.Compile.Monad
 import Agda2Lambox.Compile.Target
 import Agda2Lambox.Compile.Utils
-import Agda2Lambox.Compile.Term       ( compileTerm )
 import Agda2Lambox.Compile.Function   ( compileFunction )
 import Agda2Lambox.Compile.Inductive  ( compileInductive )
 import Agda2Lambox.Compile.TypeScheme ( compileTypeScheme )
diff --git a/src/Agda2Lambox/Compile/Function.hs b/src/Agda2Lambox/Compile/Function.hs
index 6f077c8..97297d7 100644
--- a/src/Agda2Lambox/Compile/Function.hs
+++ b/src/Agda2Lambox/Compile/Function.hs
@@ -1,11 +1,10 @@
-{-# LANGUAGE NamedFieldPuns, DataKinds, OverloadedStrings #-}
+{-# LANGUAGE OverloadedStrings #-}
 -- | Convert Agda functions to λ□ constant declarations
 module Agda2Lambox.Compile.Function
   ( compileFunction
   ) where
 
-import Control.Monad ( forM, when, filterM, unless )
-import Control.Monad.IO.Class ( liftIO )
+import Control.Monad ( forM, filterM )
 import Data.Graph ( stronglyConnComp, SCC(..) )
 import Data.List ( elemIndex, find, sort )
 import Data.Map ( Map )
@@ -14,16 +13,16 @@ import Data.Maybe ( fromMaybe )
 import Data.Set ( Set )
 import Data.Set qualified as S
 
-import Agda.Syntax.Abstract.Name ( QName, qnameModule )
+import Agda.Syntax.Abstract.Name ( QName )
 import Agda.TypeChecking.Monad.Base hiding ( None )
 import Agda.TypeChecking.Pretty
 import Agda.Compiler.Backend ( getConstInfo, reportSDoc )
 import Agda.Syntax.Internal.Names ( namesIn )
 import Agda.Syntax.Common ( hasQuantityω )
-import Agda.Utils.Monad (guardWithError, whenM, ifNotM)
+import Agda.Utils.Monad (ifNotM)
 import Agda.Utils.Treeless ( alwaysInline, Erasure )
 
-import Agda.Utils ( treeless, pp, isRecordProjection, isPiTy, etaExpand, isFunction )
+import Agda.Utils ( treeless, isRecordProjection, isPiTy, etaExpand, isFunction )
 import Agda2Lambox.Compile.Target
 import Agda2Lambox.Compile.Utils
 import Agda2Lambox.Compile.Monad
diff --git a/src/Agda2Lambox/Compile/Inductive.hs b/src/Agda2Lambox/Compile/Inductive.hs
index a3d3239..051b266 100644
--- a/src/Agda2Lambox/Compile/Inductive.hs
+++ b/src/Agda2Lambox/Compile/Inductive.hs
@@ -6,12 +6,9 @@ import Control.Monad.Reader ( liftIO )
 import Control.Monad ( forM, unless )
 import Data.Functor ((<&>))
 import Data.Foldable ( toList )
-import Data.List.NonEmpty ( NonEmpty(..) )
 import Data.List.NonEmpty qualified as NEL
 import Data.Maybe ( isJust, fromMaybe )
-import Data.Traversable ( mapM )
 
-import Agda.Syntax.Abstract.Name ( QName )
 import Agda.TypeChecking.Monad.Base hiding ( None )
 import Agda.TypeChecking.Datatypes ( ConstructorInfo(..), getConstructorInfo )
 import Agda.TypeChecking.Pretty
diff --git a/src/Agda2Lambox/Compile/Monad.hs b/src/Agda2Lambox/Compile/Monad.hs
index e47f07c..6196609 100644
--- a/src/Agda2Lambox/Compile/Monad.hs
+++ b/src/Agda2Lambox/Compile/Monad.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE DerivingVia, GeneralizedNewtypeDeriving, OverloadedStrings, DeriveFunctor, DeriveTraversable, NamedFieldPuns #-}
+{-# LANGUAGE DerivingStrategies, GeneralizedNewtypeDeriving, OverloadedStrings, DeriveTraversable #-}
 -- | Compilation monad.
 module Agda2Lambox.Compile.Monad
   ( CompileM
@@ -17,20 +17,17 @@ module Agda2Lambox.Compile.Monad
 import Control.Monad ( unless )
 import Control.Monad.Reader
 import Control.Monad.State
-import Control.Monad.IO.Class ( MonadIO )
 import Data.Bifunctor ( bimap )
 import Data.Set ( Set )
 import Data.Set qualified as Set
-import Data.Set qualified as Set
 import Data.Map qualified as Map
 import Data.Maybe ( catMaybes )
 
 import Agda.Syntax.Abstract (QName)
 import Agda.Compiler.Backend (getConstInfo, PureTCM, HasConstInfo, HasBuiltins, canonicalName)
 import Agda.TypeChecking.Monad (MonadDebug, MonadTrace, MonadAddContext)
-import Agda.TypeChecking.Monad.Debug (MonadDebug, reportSDoc)
+import Agda.TypeChecking.Monad.Debug (reportSDoc)
 import Agda.TypeChecking.Monad.Base hiding (initState)
-import Agda.Utils.List ( mcons )
 import Agda.Utils.Monad ( unlessM )
 import Agda.TypeChecking.Pretty
 import Control.Monad.Error.Class (MonadError)
diff --git a/src/Agda2Lambox/Compile/Target.hs b/src/Agda2Lambox/Compile/Target.hs
index b2f476a..26e3721 100644
--- a/src/Agda2Lambox/Compile/Target.hs
+++ b/src/Agda2Lambox/Compile/Target.hs
@@ -8,7 +8,6 @@ module Agda2Lambox.Compile.Target
   , whenTyped
   ) where
 
-import Data.Foldable (Foldable(foldMap))
 import Control.DeepSeq ( NFData(rnf) )
 import Data.Kind ( Type )
 
diff --git a/src/Agda2Lambox/Compile/Term.hs b/src/Agda2Lambox/Compile/Term.hs
index 1cdffd9..e36fa03 100644
--- a/src/Agda2Lambox/Compile/Term.hs
+++ b/src/Agda2Lambox/Compile/Term.hs
@@ -1,26 +1,19 @@
 module Agda2Lambox.Compile.Term (compileTerm) where
 
-import Control.Monad.Fail ( MonadFail )
-import Control.Monad.IO.Class (MonadIO)
-import Control.Monad.Reader.Class ( MonadReader, ask, asks )
 import Control.Monad.Reader ( ReaderT(runReaderT), local )
 import Control.Monad.Trans
-import Data.List ( elemIndex, foldl', singleton )
-import Data.Maybe ( fromMaybe, listToMaybe )
-import Data.Foldable ( foldrM )
+import Data.List ( elemIndex, singleton )
 import Data.Text qualified as Text ( unpack )
 
-import Agda.Compiler.Backend ( MonadTCState, HasOptions, canonicalName )
-import Agda.Compiler.Backend ( getConstInfo, theDef, pattern Datatype, dataMutual )
-import Agda.Syntax.Abstract.Name ( ModuleName(..), QName(..) )
+import Agda.Compiler.Backend ( canonicalName )
+import Agda.Syntax.Abstract.Name ( QName(..) )
 import Agda.Syntax.Builtin ( builtinNat, builtinZero, builtinSuc )
 import Agda.Syntax.Common ( Erased(..) )
 import Agda.Syntax.Common.Pretty
 import Agda.Syntax.Literal
 import Agda.Syntax.Treeless
   ( TTerm(..), TAlt(..), CaseInfo(..), CaseType(..), TPrim(..) )
-import Agda.TypeChecking.Datatypes ( getConstructorData, getConstructors )
-import Agda.TypeChecking.Monad.Base ( TCM , liftTCM, MonadTCEnv, MonadTCM )
+import Agda.TypeChecking.Monad.Base ( liftTCM )
 import Agda.TypeChecking.Monad.Builtin ( getBuiltinName_ )
 
 import LambdaBox.Names ( Name(..) )
diff --git a/src/Agda2Lambox/Compile/Type.hs b/src/Agda2Lambox/Compile/Type.hs
index 32998c7..535d8e9 100644
--- a/src/Agda2Lambox/Compile/Type.hs
+++ b/src/Agda2Lambox/Compile/Type.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE LambdaCase, FlexibleInstances, MultiWayIf, NamedFieldPuns, OverloadedStrings #-}
+{-# LANGUAGE OverloadedStrings #-}
 module Agda2Lambox.Compile.Type where
 --   ( compileType
 --   , compileTopLevelType
@@ -7,23 +7,16 @@ module Agda2Lambox.Compile.Type where
 --   ) where
 
 
-import Control.Category ((>>>))
 import Control.Monad.Reader
-import Control.Monad ( mapM )
-import Data.List ( foldl' )
-import Data.Function ( (&) )
-import Data.Bifunctor ( second )
 import Data.Maybe ( isJust, mapMaybe )
-import Data.Function ( applyWhen )
 
 import Agda.Syntax.Common ( unArg, Arg (Arg) )
 import Agda.Syntax.Internal
-import Agda.TypeChecking.Substitute ( absBody, TelV (theCore), absApp )
-import Agda.TypeChecking.Telescope (telView, piApplyM)
+import Agda.TypeChecking.Substitute ( absBody, absApp )
 import Agda.TypeChecking.Monad.Base ( TCM, MonadTCM (liftTCM), Definition(..))
 import Agda.TypeChecking.Monad.Debug ( reportSDoc )
 import Agda.TypeChecking.Monad.Signature ( canonicalName )
-import Agda.TypeChecking.Telescope ( mustBePi, shouldBePi )
+import Agda.TypeChecking.Telescope ( shouldBePi )
 import Agda.TypeChecking.Pretty ( prettyTCM, (<+>) )
 import Agda.Utils.Monad ( ifM )
 import Agda.Utils ( unSpine1 )
@@ -31,7 +24,7 @@ import Agda.Utils ( unSpine1 )
 import qualified LambdaBox as LBox
 import Agda2Lambox.Compile.Utils
 import Agda2Lambox.Compile.Monad
-import Agda.Compiler.Backend (HasConstInfo(getConstInfo), Definition(Defn), AddContext (addContext))
+import Agda.Compiler.Backend (HasConstInfo(getConstInfo), AddContext (addContext))
 import Agda.Utils (isDataOrRecDef, getInductiveParams, isArity, maybeUnfoldCopy, isFunDef, isTypeAlias)
 import Agda.TypeChecking.Reduce ( reduce )
 
diff --git a/src/Agda2Lambox/Compile/TypeScheme.hs b/src/Agda2Lambox/Compile/TypeScheme.hs
index a8eb143..5e5a237 100644
--- a/src/Agda2Lambox/Compile/TypeScheme.hs
+++ b/src/Agda2Lambox/Compile/TypeScheme.hs
@@ -1,10 +1,7 @@
-{-# LANGUAGE DataKinds, NoNamedFieldPuns, OverloadedStrings #-}
+{-# LANGUAGE DataKinds, OverloadedStrings #-}
 module Agda2Lambox.Compile.TypeScheme where
 
-import Control.Monad.IO.Class ( liftIO )
-
 import Agda.Syntax.Internal
-import Agda.Syntax.Common
 import Agda.TypeChecking.Pretty
 import Agda.Compiler.Backend
 import Agda.TypeChecking.Telescope ( telView )
@@ -14,7 +11,6 @@ import Agda.TypeChecking.Functions ( etaExpandClause )
 import Agda.Utils ( isTypeAlias )
 import Agda2Lambox.Compile.Monad
 import Agda2Lambox.Compile.Target
-import Agda2Lambox.Compile.Utils
 import Agda2Lambox.Compile.Type
 import LambdaBox.Env
 import LambdaBox.Type qualified as LBox
diff --git a/src/Agda2Lambox/Compile/Utils.hs b/src/Agda2Lambox/Compile/Utils.hs
index 32e0e72..845c5cd 100644
--- a/src/Agda2Lambox/Compile/Utils.hs
+++ b/src/Agda2Lambox/Compile/Utils.hs
@@ -1,21 +1,16 @@
-{-# LANGUAGE NamedFieldPuns, FlexibleInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
 module Agda2Lambox.Compile.Utils where
 
-import Control.Monad.State
-import Control.Monad.IO.Class ( liftIO )
 import Data.Functor ( (<&>) )
-import Data.List ( elemIndex, foldl' )
+import Data.List ( elemIndex )
 import Data.Maybe ( fromMaybe, listToMaybe, isJust )
 
 import Agda.Compiler.Backend
 import Agda.Syntax.Internal
-import Agda.Syntax.Abstract.Name
-import Agda.Syntax.Common.Pretty ( prettyShow, Doc )
+import Agda.Syntax.Common.Pretty ( prettyShow )
 import Agda.Syntax.Common ( usableModality, Arg(..), NameId(..) )
 import Agda.TypeChecking.Datatypes ( getConstructors, getConstructorData )
 import Agda.TypeChecking.Level ( isLevelType )
-import Agda.TypeChecking.Monad.SizedTypes ( isSizeType )
-import Agda.TypeChecking.Monad.Base ( TCM )
 import Agda.TypeChecking.Reduce ( reduce )
 import Agda.TypeChecking.Substitute ( TelV(TelV), theTel )
 import Agda.TypeChecking.Telescope ( telView, telViewUpTo, flattenTel )
diff --git a/src/CodeGen/Rocq.hs b/src/CodeGen/Rocq.hs
index 624351e..4515868 100644
--- a/src/CodeGen/Rocq.hs
+++ b/src/CodeGen/Rocq.hs
@@ -1,10 +1,7 @@
-{-# LANGUAGE FlexibleInstances, FlexibleContexts, OverloadedStrings, DataKinds, MonadComprehensions #-}
+{-# LANGUAGE FlexibleInstances, FlexibleContexts, OverloadedStrings, DataKinds #-}
 -- | Generating Rocq code from our LambdaBox AST
 module CodeGen.Rocq (prettyRocq) where
 
-import Data.Bifunctor(bimap)
-import Data.List(intercalate)
-
 import Agda.Syntax.Common.Pretty
 import LambdaBox
 import Agda.Utils.Function (applyWhen)
diff --git a/src/CodeGen/SExpr.hs b/src/CodeGen/SExpr.hs
index b9b367e..9767847 100644
--- a/src/CodeGen/SExpr.hs
+++ b/src/CodeGen/SExpr.hs
@@ -1,15 +1,10 @@
-{-# LANGUAGE FlexibleInstances, FlexibleContexts, OverloadedStrings #-}
-{-# LANGUAGE DataKinds, MonadComprehensions, GADTs #-}
+{-# LANGUAGE FlexibleInstances, OverloadedStrings, ExistentialQuantification #-}
 -- | Converting the LambdaBox AST to s-expressions
 module CodeGen.SExpr (ToSexp, prettySexp) where
 
-import Data.Bifunctor(bimap)
-import Data.List(intercalate)
 import Data.Maybe(listToMaybe)
 
-import Agda.Syntax.Common.Pretty
 import LambdaBox
-import Agda.Utils.Function (applyWhen)
 import Agda2Lambox.Compile.Target
 import Data.SExpresso.SExpr
 import Data.SExpresso.Print.Lazy
diff --git a/src/LambdaBox.hs b/src/LambdaBox.hs
index 715b851..36edd15 100644
--- a/src/LambdaBox.hs
+++ b/src/LambdaBox.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE OverloadedStrings, DataKinds, GADTs #-}
 -- | Haskell encoding of the LambdaBox syntax.
 module LambdaBox
   ( module LambdaBox.Names
diff --git a/src/LambdaBox/Names.hs b/src/LambdaBox/Names.hs
index aec00af..ab47951 100644
--- a/src/LambdaBox/Names.hs
+++ b/src/LambdaBox/Names.hs
@@ -2,7 +2,6 @@
 -- | Definitions for λ□ identifiers, names and references.
 module LambdaBox.Names where
 
-import Agda.Syntax.Abstract.Name ( ModuleName(..), QName(..) )
 import Agda.Syntax.Common.Pretty
 
 -- | Identifiers.
diff --git a/src/Main.hs b/src/Main.hs
index dcd5c89..210da9e 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -1,12 +1,11 @@
-{-# LANGUAGE DeriveGeneric, DeriveAnyClass, OverloadedStrings, GADTs #-}
+{-# LANGUAGE DeriveGeneric, DeriveAnyClass, OverloadedStrings, ExistentialQuantification #-}
 -- | The agda2lambox Agda backend
 module Main (main) where
 
-import Control.Monad ( unless, filterM, when )
+import Control.Monad ( filterM, when )
 import Control.Monad.IO.Class ( liftIO )
 import Control.DeepSeq ( NFData(rnf) )
 import Data.Function ( (&) )
-import Data.List ( elem )
 import Data.Maybe ( fromMaybe )
 import Data.Version ( showVersion )
 import Data.Text ( pack )
@@ -21,9 +20,7 @@ import Paths_agda2lambox ( version )
 import Agda.Compiler.Common
 import Agda.Compiler.Backend
 import Agda.Main ( runAgda )
-import Agda.Syntax.Internal ( clauseWhereModule )
-import Agda.Syntax.TopLevelModuleName ( TopLevelModuleName, moduleNameToFileName )
-import Agda.Syntax.Common.Pretty ( pretty, prettyShow )
+import Agda.Syntax.Common.Pretty ( prettyShow )
 
 import Agda.Utils ( pp, hasPragma )
 import Agda2Lambox.Compile.Target
diff --git a/test/Main.hs b/test/Main.hs
index 34b1e47..ba8ee7b 100644
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -1,8 +1,7 @@
-{-# LANGUAGE OverloadedStrings #-}
 -- | Test suite for agda2lambox using tasty
 module Main (main) where
 
-import Control.Monad (filterM, unless, when, forM)
+import Control.Monad (unless, when, forM)
 import System.Directory
 import System.FilePath
 import System.Process
@@ -12,7 +11,7 @@ import Data.Char (isSpace)
 import Data.List (sort, isSuffixOf, dropWhileEnd)
 
 import Test.Tasty (defaultMain, testGroup, TestTree)
-import Test.Tasty.HUnit (testCase, assertFailure, (@?=))
+import Test.Tasty.HUnit (testCase, assertFailure)
 
 main :: IO ()
 main = do