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 <noreply@anthropic.com>

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

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

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