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

@@ -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!

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