From 504d71f268e9cfadf81c91b5f6777c0ed0b7cbfa Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Thu, 21 Aug 2025 14:55:10 -0700
Subject: [PATCH] chore: remove unnecessary code handling `cases` of an erased
 value (#10035)

This is now all handled in `toLCNF`.
---
 src/Lean/Compiler/IR/ToIR.lean | 20 ++++++--------------
 1 file changed, 6 insertions(+), 14 deletions(-)

diff --git a/src/Lean/Compiler/IR/ToIR.lean b/src/Lean/Compiler/IR/ToIR.lean
index 003c0fdc13..feb54c6b2b 100644
--- a/src/Lean/Compiler/IR/ToIR.lean
+++ b/src/Lean/Compiler/IR/ToIR.lean
@@ -117,20 +117,12 @@ partial def lowerCode (c : LCNF.Code) : M FnBody := do
     let joinPointId ← getJoinPointValue fvarId
     return .jmp joinPointId (← args.mapM lowerArg)
   | .cases cases =>
-    match (← getFVarValue cases.discr) with
-    | .var varId =>
-      return .case cases.typeName
-                   varId
-                   (← nameToIRType cases.typeName)
-                   (← cases.alts.mapM (lowerAlt varId))
-    | .erased =>
-      let #[alt] := cases.alts | panic! "erased inductive should only have one case"
-      match alt with
-      | .alt _ params code =>
-        params.forM (bindErased ·.fvarId)
-        lowerCode code
-      | .default code =>
-        lowerCode code
+    -- `casesOn` for inductive predicates should have already been expanded.
+    let .var varId := (← getFVarValue cases.discr) | unreachable!
+    return .case cases.typeName
+                 varId
+                 (← nameToIRType cases.typeName)
+                 (← cases.alts.mapM (lowerAlt varId))
   | .return fvarId =>
     return .ret (← getFVarValue fvarId)
   | .unreach .. => return .unreachable