From c7983a8c6504a534daf147ccf9829e0e9ef41fb9 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 3 Apr 2026 10:37:20 +0200 Subject: [PATCH] perf: limit counter-example generation in match compiler (#13222) This PR adds a `match.maxCounterExamples` option (default 5) to bound the number of "missing cases" counter-examples the match compiler generates. When the match compiler runs out of alternatives for a variable, it case-splits to explore missing cases. Previously, this would recursively split all inductive-typed fields of each constructor, leading to O(K^fields) counter-examples for types with K constructors per field. For nested incomplete matches on types like `Op w` (20 constructors with `Operand w` fields having 8 constructors each), this produced thousands of counter-examples and took several seconds. The fix checks the counter-example count in `isConstructorTransition`: once the limit is reached and there are no remaining alternatives, the match compiler stops exploring further case splits. The error message notes when output has been truncated and names the option. The existing protection against infinite recursion on recursive types is preserved. Co-authored-by: Claude Opus 4.6 --- src/Lean/Elab/Match.lean | 11 +++- src/Lean/Meta/Match/Match.lean | 22 ++++++-- tests/elab/nested_match_slowdown.lean | 74 +++++++++++++++++++++++++++ 3 files changed, 102 insertions(+), 5 deletions(-) create mode 100644 tests/elab/nested_match_slowdown.lean diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index 935e1a123d..366ae19af6 100644 --- a/src/Lean/Elab/Match.lean +++ b/src/Lean/Elab/Match.lean @@ -1042,7 +1042,16 @@ def mkRedundantAlternativeMsg (altName? : Option Name) (altMsg? : Option Message def reportMatcherResultErrors (altLHSS : List AltLHS) (result : MatcherResult) : TermElabM Unit := do unless result.counterExamples.isEmpty do - withHeadRefOnly <| logError m!"Missing cases:\n{Meta.Match.counterExamplesToMessageData result.counterExamples}" + let maxCEx := Meta.Match.match.maxCounterExamples.get (← getOptions) + let (shown, truncated) := + if result.counterExamples.length > maxCEx then + (result.counterExamples.take maxCEx, true) + else + (result.counterExamples, false) + let mut msg := m!"Missing cases:\n{Meta.Match.counterExamplesToMessageData shown}" + if truncated then + msg := msg ++ m!"\n(further cases omitted, increase `set_option match.maxCounterExamples {maxCEx}` to see more)" + withHeadRefOnly <| logError msg return () unless match.ignoreUnusedAlts.get (← getOptions) || result.unusedAltIdxs.isEmpty do let mut i := 0 diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index 00b8eeec01..66470d9b68 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -78,6 +78,14 @@ register_builtin_option backward.match.rowMajor : Bool := { it splits them from left to right, which can lead to unnecessary code bloat." } +register_builtin_option match.maxCounterExamples : Nat := { + defValue := 5 + descr := "Maximum number of missing-case counter-examples to generate. \ + When this limit is reached, the match compiler stops exploring further \ + case splits for counter-example generation. Increase if you need to see \ + all missing cases." +} + private def mkIncorrectNumberOfPatternsMsg [ToMessageData α] (discrepancyKind : String) (expected actual : Nat) (pats : List α) := let patternsMsg := MessageData.joinSep (pats.map toMessageData) ", " @@ -269,10 +277,16 @@ def isCurrVarInductive (p : Problem) : MetaM Bool := do let val? ← getInductiveVal? x return val?.isSome -private def isConstructorTransition (p : Problem) : MetaM Bool := do - return (← isCurrVarInductive p) - && (hasCtorPattern p || p.alts.isEmpty) - && p.alts.all fun alt => match alt.patterns with +private def isConstructorTransition (p : Problem) : StateRefT State MetaM Bool := do + if !(← isCurrVarInductive p) then return false + if p.alts.isEmpty then + /- When there are no alternatives left and we have already accumulated enough + counter-examples, stop exploring further case splits. This prevents + combinatorial explosion when generating "missing cases" diagnostics. -/ + let maxCEx := match.maxCounterExamples.get (← getOptions) + return (← get).counterExamples.length < maxCEx + else + return hasCtorPattern p && p.alts.all fun alt => match alt.patterns with | .ctor .. :: _ => true | .inaccessible _ :: _ => true -- should be a done pattern by now | _ => false diff --git a/tests/elab/nested_match_slowdown.lean b/tests/elab/nested_match_slowdown.lean new file mode 100644 index 0000000000..a1ac807c0c --- /dev/null +++ b/tests/elab/nested_match_slowdown.lean @@ -0,0 +1,74 @@ +/- +Regression test for slow elaboration of incomplete matches on types with +many constructors and multi-constructor fields. Without the +`match.maxCounterExamples` limit, the match compiler would case-split every +field variable, producing O(K^fields) counter-examples per missing +constructor (where K is the number of constructors of the field type). + +For `Op w` (20 constructors, each with two `Operand w` fields having 8 +constructors), a `nomatch` would try to generate 20 × 8² = 1280 +counter-examples. The limit caps this at 5 (by default). +-/ +set_option autoImplicit false + +-- A field type with many constructors +inductive Operand (w : Nat) where + | r0 : Nat → Operand w + | r1 : Nat → Operand w + | r2 : Nat → Operand w + | r3 : Nat → Operand w + | r4 : Nat → Operand w + | r5 : Nat → Operand w + | r6 : Nat → Operand w + | r7 : Nat → Operand w + +-- A large inductive with multi-constructor field types (20 constructors) +inductive Op (w : Nat) where + | add : Operand w → Operand w → Op w + | or_ : Operand w → Operand w → Op w + | xor : Operand w → Operand w → Op w + | sub : Operand w → Operand w → Op w + | mul : Operand w → Operand w → Op w + | shl : Operand w → Operand w → Op w + | shr : Operand w → Operand w → Op w + | mov : Operand w → Operand w → Op w + | cmp : Operand w → Operand w → Op w + | test : Operand w → Operand w → Op w + | lea : Operand w → Operand w → Op w + | c11 : Operand w → Operand w → Op w + | c12 : Operand w → Operand w → Op w + | c13 : Operand w → Operand w → Op w + | c14 : Operand w → Operand w → Op w + | c15 : Operand w → Operand w → Op w + | c16 : Operand w → Operand w → Op w + | c17 : Operand w → Operand w → Op w + | c18 : Operand w → Operand w → Op w + | c19 : Operand w → Operand w → Op w + +-- Without the counter-example limit, this `nomatch` would generate 1280 +-- counter-examples and take several seconds. With the limit (default 5), +-- it stops early and reports the first 5 missing cases quickly. +/-- +error: Missing cases: +(c19 _ _) +(c18 _ _) +(c17 _ _) +(c16 _ _) +(c15 _ _) +(further cases omitted, increase `set_option match.maxCounterExamples 5` to see more) +-/ +#guard_msgs in +def Op.testNomatch {w : Nat} (op : Op w) : Nat := nomatch op + +-- Regression test: recursive single-constructor types terminate in counter-example +-- generation. The recursive type check in `processConstructor` prevents infinite +-- unfolding. This `nomatch` should fail quickly with "missing cases". +inductive RecStruct where + | mk : Nat → RecStruct → RecStruct + +/-- +error: Missing cases: +_ +-/ +#guard_msgs in +def recTest (x : RecStruct) : Nat := nomatch x