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

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