From 892475dcacd75f3b409954f269fdba016d21e491 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Mon, 9 Feb 2026 13:44:01 +0100 Subject: [PATCH] fix: LCNF casesOnCtor can only act if type correct (#12387) This PR fixes an issue in LCNF simp where it would attempt to act on type incorrect `cases` statements and look for a branch, otherwise panic. This issue did not yet manifest in production as various other invariants upheld by LCNF simp help mask it but will start to become an issue with the upcoming changes. This is the proper fix for #6957. --- src/Lean/Compiler/LCNF/Simp/Main.lean | 3 +++ 1 file changed, 3 insertions(+) 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