document what the issue is with upstream treeless

Author: flupe

src/Agda/Utils.hs

@@ -82,28 +82,6 @@ isArity typ = do
 -- | Convert compiled clauses to treeless syntax, and return it.
 treeless :: QName -> TCM (Maybe TTerm)
 treeless = CustomTT.toTreeless EagerEvaluation
-  -- TT.toTreelessWith pipeline (EagerEvaluation, TT.EraseUnused)
-  {-
-  where
-    pipeline v q = TT.Sequential []
-    TT.Sequential
-      -- NOTE (flupe): this is the default Agda treeless pipeline
-      --               with the builtin pass removed.
-      -- [ TT.compilerPass "builtin" (30 + v) "builtin translation" $ const TT.translateBuiltins
-      [ TT.FixedPoint 5 $ TT.Sequential
-        [ -- TT.compilerPass "simpl"  (30 + v) "simplification"     $ const TT.simplifyTTerm
-        -- TT.compilerPass "erase"  (30 + v) "erasure"            $ TT.eraseTerms q
-        -- , TT.compilerPass "uncase" (30 + v) "uncase"             $ const TT.caseToSeq
-        -- , TT.compilerPass "aspat"  (30 + v) "@-pattern recovery" $ const TT.recoverAsPatterns
-        ]
-      -- , TT.compilerPass "id" (30 + v) "identity function detection" $ const (TT.detectIdentityFunctions q)
-
-      -- NOTE(flupe): actually, we also remove case defaults to add a branch for all constructors
-      -- , TT.compilerPass "defaults" (30 + v) "eliminate case defaults" $ const TT.eliminateCaseDefaults
-      ]
-      -}
-
-
 
 -- * projections
 

src/Agda/Utils/EliminateDefaults.hs

@@ -17,6 +17,7 @@ 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
@@ -25,7 +26,9 @@ import Agda.Compiler.Treeless.Subst () --instance only
 
 
 eliminateCaseDefaults :: TTerm -> TCM TTerm
-eliminateCaseDefaults = tr
+eliminateCaseDefaults term = do
+  liftIO $ putStrLn "hello"
+  tr term
   where
     tr :: TTerm -> TCM TTerm
     tr = \case

src/Agda/Utils/EtaExpandConstructors.hs

@@ -36,7 +36,6 @@ etaExpandConstructors t | Just (q, args) <- unSpineCon t = do
     let nlam = arity - nargs
     exargs <- mapM (etaExpandConstructors . raise nlam) args
     let vars = TVar <$> reverse [0 .. nlam - 1]
-    liftIO $ putStrLn $ show vars
     pure $ iterate TLam (TApp (TCon q) $ exargs ++ vars) !! nlam
 
 etaExpandConstructors t = case t of

src/Agda/Utils/Treeless.hs

@@ -1,4 +1,12 @@
 {-# LANGUAGE NamedFieldPuns, OverloadedStrings #-}
+{- NOTE(flupe):
+
+Currently we inline the treeless pipeline from the Agda source.
+The reason is simple: there is a bug in the pipeline that makes
+the compiler ignore the user-provided pipeline in recursive calls to treeless.
+Since the treeless compilation is cached (?), it is never recomputed with the right pipeline.
+
+-}
 module Agda.Utils.Treeless
   ( toTreeless
   , toTreelessWith
@@ -174,11 +182,6 @@ compilerPass tag v name code = SinglePass (CompilerPass tag v name code)
 compilerPipeline :: BuildPipeline
 compilerPipeline v q =
   Sequential
-    -- Issue #4967: No simplification step before builtin translation! Simplification relies
-    --              on either all or no builtins being translated. Since we might have inlined
-    --              functions that have had the builtin translation applied, we need to apply it
-    --              first.
-    -- [ compilerPass "simpl"   (35 + v) "simplification"      $ const simplifyTTerm
 
     -- [ compilerPass "builtin" (30 + v) "builtin translation" $ const translateBuiltins
     [ FixedPoint 5 $ Sequential