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.
This commit is contained in:
Henrik Böving 2026-02-09 13:44:01 +01:00 committed by GitHub
parent b4a254de69
commit 892475dcac
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

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