diff --git a/src/Lean/Compiler/LCNF/Simp/Main.lean b/src/Lean/Compiler/LCNF/Simp/Main.lean index 5631cfa440..8c0ba865be 100644 --- a/src/Lean/Compiler/LCNF/Simp/Main.lean +++ b/src/Lean/Compiler/LCNF/Simp/Main.lean @@ -327,9 +327,14 @@ partial def simp (code : Code) : SimpM Code := withIncRecDepth do return alt.updateCode (← simp k) | .default k => return alt.updateCode (← simp k) let alts ← addDefaultAlt alts - if alts.size == 1 && alts[0]! matches .default .. then - return alts[0]!.getCode - else - markUsedFVar discr - return code.updateCases! resultType discr alts + if let #[alt] := alts then + match alt with + | .default k => return k + | .alt _ params k => + if !(← params.anyM (isUsed ·.fvarId)) then + params.forM (eraseParam ·) + markSimplified + return k + markUsedFVar discr + return code.updateCases! resultType discr alts end