From 149fc2173c4f3392a9020246459b9bb02a760088 Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Sat, 5 Jul 2025 12:52:12 -0700
Subject: [PATCH] fix: correctly handle constructor params in elimDeadBranches
 (#9209)

This PR changes the `getLiteral` helper function of `elimDeadBranches`
to correctly handle inductives with constructors. This function is not
used as often as it could be, which makes this issue rare to hit outside
of targeted test cases.
---
 src/Lean/Compiler/LCNF/ElimDeadBranches.lean   | 10 ++++++----
 tests/lean/run/elimDeadBranchesCtorParams.lean | 11 +++++++++++
 2 files changed, 17 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/elimDeadBranchesCtorParams.lean

diff --git a/src/Lean/Compiler/LCNF/ElimDeadBranches.lean b/src/Lean/Compiler/LCNF/ElimDeadBranches.lean
index 5a51d3eeac..3a161abce7 100644
--- a/src/Lean/Compiler/LCNF/ElimDeadBranches.lean
+++ b/src/Lean/Compiler/LCNF/ElimDeadBranches.lean
@@ -216,11 +216,13 @@ where
     let val := getNatConstant val + 1
     let decl ← mkAuxLetDecl <| .lit <| .nat <| val
     return (#[.let decl], decl.fvarId)
-  | .ctor i vs => do
-    let args ← vs.mapM go
+  | .ctor ctorName vs => do
+    let some (.ctorInfo ctorInfo) := (← getEnv).find? ctorName | unreachable!
+    let fields ← vs.mapM go
     let flatten acc := fun (decls, var) => (acc.fst ++ decls, acc.snd.push <| .fvar var)
-    let (decls, params) := args.foldl (init := (#[], Array.mkEmpty args.size)) flatten
-    let letVal : LetValue := .const i [] params
+    let (decls, args) :=
+      fields.foldl (init := (#[], Array.replicate ctorInfo.numParams .erased)) flatten
+    let letVal : LetValue := .const ctorName [] args
     let letDecl ← mkAuxLetDecl letVal
     return (decls.push <| .let letDecl, letDecl.fvarId)
   | _ => unreachable!
diff --git a/tests/lean/run/elimDeadBranchesCtorParams.lean b/tests/lean/run/elimDeadBranchesCtorParams.lean
new file mode 100644
index 0000000000..01d36ba901
--- /dev/null
+++ b/tests/lean/run/elimDeadBranchesCtorParams.lean
@@ -0,0 +1,11 @@
+@[noinline]
+def f (_ : Unit) : Prod Unit Unit :=
+  Prod.mk ⟨⟩ ⟨⟩
+
+@[noinline]
+def g (a : Unit) : Prod (Prod Unit Unit) (Prod Unit Unit) :=
+  Prod.mk (f a) (f a)
+
+def h (a : Unit) : Prod Unit Unit :=
+  match g a with
+  | ⟨_, y⟩ => y