diff --git a/src/Lean/Compiler/LCNF/Simp/Main.lean b/src/Lean/Compiler/LCNF/Simp/Main.lean
index a9d9a6169f..078e035b45 100644
--- a/src/Lean/Compiler/LCNF/Simp/Main.lean
+++ b/src/Lean/Compiler/LCNF/Simp/Main.lean
@@ -187,6 +187,9 @@ partial def simpCasesOnCtor? (cases : Cases .pure) : SimpM (Option (Code .pure))
     return some ret
   | .fvar discr =>
     let some ctorInfo ← findCtor? discr | return none
+    let some (.ctorInfo ctorVal) := (← getEnv).find? ctorInfo.getName | return none
+    unless cases.typeName == ctorVal.induct do
+      return none
     let (alt, cases) := cases.extractAlt! ctorInfo.getName
     eraseCode (.cases cases)
     markSimplified