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