From f759d5dbc1aa18b36bb0affeaeb6ea094fde33db Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Wed, 6 Aug 2025 07:23:28 -0700
Subject: [PATCH] perf: erase all constructor params in the mono phase (#9764)

---
 src/Lean/Compiler/LCNF/ToMono.lean          | 6 +-----
 tests/lean/run/emptyLcnf.lean               | 2 +-
 tests/lean/run/erased.lean                  | 4 ++--
 tests/lean/unhygienicCode.lean.expected.out | 4 ++--
 4 files changed, 6 insertions(+), 10 deletions(-)

diff --git a/src/Lean/Compiler/LCNF/ToMono.lean b/src/Lean/Compiler/LCNF/ToMono.lean
index 34ae148b59..b02ad3c52d 100644
--- a/src/Lean/Compiler/LCNF/ToMono.lean
+++ b/src/Lean/Compiler/LCNF/ToMono.lean
@@ -73,11 +73,7 @@ def argsToMonoWithFnType (resultFVar : FVarId) (args : Array Arg) (type : Expr)
 
 def ctorAppToMono (resultFVar : FVarId) (ctorInfo : ConstructorVal) (args : Array Arg)
     : ToMonoM LetValue := do
-  let argsNewParams : Array Arg ← args[*...ctorInfo.numParams].toArray.mapM fun arg => do
-    -- We only preserve constructor parameters that are types
-    match arg with
-    | .type type => return .type (← toMonoType type)
-    | .fvar .. | .erased => return .erased
+  let argsNewParams : Array Arg := .replicate ctorInfo.numParams .erased
   let argsNewFields ← args[ctorInfo.numParams...*].toArray.mapM (argToMonoDeferredCheck resultFVar)
   let argsNew := argsNewParams ++ argsNewFields
   return .const ctorInfo.name [] argsNew
diff --git a/tests/lean/run/emptyLcnf.lean b/tests/lean/run/emptyLcnf.lean
index ee3adf70af..1c7c57c489 100644
--- a/tests/lean/run/emptyLcnf.lean
+++ b/tests/lean/run/emptyLcnf.lean
@@ -16,7 +16,7 @@ trace: [Compiler.result] size: 5
       let _x.10 := Lean.Compiler.compile _x.1 _y.7 _y.8 _y.9;
       cases _x.10 : EStateM.Result Lean.Exception PUnit PUnit
       | EStateM.Result.ok a.11 a.12 =>
-        let _x.13 := EStateM.Result.ok _ _ _ _x.2 a.12;
+        let _x.13 := EStateM.Result.ok ◾ ◾ ◾ _x.2 a.12;
         return _x.13
       | EStateM.Result.error a.14 a.15 =>
         return _x.10
diff --git a/tests/lean/run/erased.lean b/tests/lean/run/erased.lean
index 165643d7cc..bce3f26a25 100644
--- a/tests/lean/run/erased.lean
+++ b/tests/lean/run/erased.lean
@@ -22,7 +22,7 @@ set_option trace.Compiler.result true
 /--
 trace: [Compiler.result] size: 1
     def Erased.mk (α : lcErased) (a : lcAny) : PSigma lcErased lcAny :=
-      let _x.1 : PSigma lcErased lcAny := PSigma.mk lcErased ◾ ◾ ◾;
+      let _x.1 : PSigma lcErased lcAny := PSigma.mk ◾ ◾ ◾ ◾;
       return _x.1
 ---
 trace: [Compiler.result] size: 5
@@ -32,7 +32,7 @@ trace: [Compiler.result] size: 5
       let _x.10 : EStateM.Result Lean.Exception PUnit PUnit := compile _x.1 _y.7 _y.8 _y.9;
       cases _x.10 : EStateM.Result Lean.Exception PUnit PUnit
       | EStateM.Result.ok (a.11 : PUnit) (a.12 : PUnit) =>
-        let _x.13 : EStateM.Result Lean.Exception PUnit PUnit := EStateM.Result.ok Lean.Exception PUnit PUnit _x.2 a.12;
+        let _x.13 : EStateM.Result Lean.Exception PUnit PUnit := EStateM.Result.ok ◾ ◾ ◾ _x.2 a.12;
         return _x.13
       | EStateM.Result.error (a.14 : Lean.Exception) (a.15 : PUnit) =>
         return _x.10
diff --git a/tests/lean/unhygienicCode.lean.expected.out b/tests/lean/unhygienicCode.lean.expected.out
index 8304bcd105..47928668dc 100644
--- a/tests/lean/unhygienicCode.lean.expected.out
+++ b/tests/lean/unhygienicCode.lean.expected.out
@@ -45,7 +45,7 @@
       return _x.4
 [Compiler.result] size: 5
     def foo._closed_9 : Syntax :=
-      let _x.1 := [] _;
+      let _x.1 := [] ◾;
       let _x.2 := foo._closed_8;
       let _x.3 := foo._closed_6;
       let _x.4 := foo._closed_0;
@@ -75,7 +75,7 @@
       let _x.10 := foo._closed_6;
       let _x.11 := foo._closed_7;
       let _x.12 := foo._closed_8;
-      let _x.13 := [] _;
+      let _x.13 := [] ◾;
       let _x.14 := foo._closed_9;
       let _x.15 := foo._closed_10;
       let _x.16 := foo._closed_11;