From 4ec5dad05faa0f21f09e2089aafdb2805bac4f16 Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Sat, 7 Jun 2025 23:20:38 -0700
Subject: [PATCH] fix: only mark single-alt cases discriminant as used if any
 param is used (#8683)

This PR adds an optimization to the LCNF simp pass where the
discriminant of a single-alt cases is only marked as used if any param
is used.
---
 src/Lean/Compiler/LCNF/Simp/Main.lean | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

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