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