diff --git a/docs/source/literal_types.rst b/docs/source/literal_types.rst
index e449589ddb4d2..a57d7ad9a520b 100644
--- a/docs/source/literal_types.rst
+++ b/docs/source/literal_types.rst
@@ -472,6 +472,29 @@ For match statements specifically, inexhaustive matches can be caught
 without needing to use ``assert_never`` by using
 :option:`--enable-error-code exhaustive-match <mypy --enable-error-code>`.
 
+This also applies to combinations of values in fixed-length tuples:
+
+.. code-block:: python
+
+  def choose_pair(first: Direction, second: Direction) -> int:
+      match first, second:
+          case Direction.up, Direction.up:
+              return 1
+          case Direction.up, Direction.down:
+              return 2
+          case Direction.down, Direction.up:
+              return 3
+          case Direction.down, Direction.down:
+              return 4
+
+Removing a case leaves an unhandled combination that mypy reports with
+``exhaustive-match`` enabled, without requiring ``assert_never``.
+A guarded case only covers the values for which its guard is known to succeed.
+To avoid excessive analysis time, mypy limits the number of remaining tuple
+alternatives it constructs.
+For sufficiently complex products, it may therefore be unable to prove that a
+match is exhaustive; nesting matches over individual components can help.
+
 
 Extra Enum checks
 *****************
diff --git a/mypy/checker.py b/mypy/checker.py
index 3f2a8476ed934..dcda67eedc2b0 100644
--- a/mypy/checker.py
+++ b/mypy/checker.py
@@ -88,7 +88,7 @@ def __init__(self) -> None:
     analyze_member_access,
     is_instance_var,
 )
-from mypy.checkpattern import PatternChecker
+from mypy.checkpattern import PatternChecker, analyze_pattern_bindings
 from mypy.constraints import SUPERTYPE_OF
 from mypy.erasetype import (
     erase_type,
@@ -211,6 +211,7 @@ def __init__(self) -> None:
 )
 from mypy.operators import flip_ops, int_op_to_method, neg_ops
 from mypy.options import PRECISE_TUPLE_TYPES, Options
+from mypy.patterncoverage import is_product_exhaustive
 from mypy.patterns import AsPattern, StarredPattern
 from mypy.plugin import Plugin
 from mypy.plugins import dataclasses as dataclasses_plugin
@@ -6101,22 +6102,30 @@ def visit_match_stmt(self, s: MatchStmt) -> None:
             if isinstance(subject_type, DeletedType):
                 self.msg.deleted_as_rvalue(subject_type, s)
 
+            # Syntax and capture identity are independent of the narrowed subject.
+            # Prepare them once for both inference passes and all union alternatives.
+            pattern_bindings = analyze_pattern_bindings(s.patterns, self.msg)
+
             # We infer types of patterns twice. The first pass is used
             # to infer the types of capture variables. The type of a
             # capture variable may depend on multiple patterns (it
             # will be a union of all capture types). This pass ignores
             # guard expressions.
-            pattern_types = [self.pattern_checker.accept(p, subject_type) for p in s.patterns]
-            type_maps: list[TypeMap] = [t.captures for t in pattern_types]
+            pattern_types = [
+                self.pattern_checker.check_pattern(p, subject_type, pattern_bindings)
+                for p in s.patterns
+            ]
+            type_maps = [t.captures for t in pattern_types]
             inferred_types = self.infer_variable_types_from_type_maps(type_maps)
 
             # The second pass narrows down the types and type checks bodies.
-            unmatched_types: TypeMap = {s.subject: UninhabitedType()}
             for p, g, b in zip(s.patterns, s.guards, s.bodies):
                 current_subject_type = self.expr_checker.narrow_type_from_binder(
                     named_subject, subject_type
                 )
-                pattern_type = self.pattern_checker.accept(p, current_subject_type)
+                pattern_type = self.pattern_checker.check_pattern(
+                    p, current_subject_type, pattern_bindings
+                )
                 with self.binder.frame_context(can_skip=True, fall_through=2):
                     pattern_map, else_map = conditional_types_to_typemaps(
                         named_subject, pattern_type.type, pattern_type.rest_type
@@ -6137,7 +6146,10 @@ def visit_match_stmt(self, s: MatchStmt) -> None:
                                 self._get_recursive_sub_patterns_map(expr, typ),
                                 from_assignment=False,
                             )
-                    self.push_type_map(pattern_type.captures, from_assignment=False)
+                    self.push_type_map(
+                        {expr: typ for expr, typ in pattern_type.captures.items()},
+                        from_assignment=False,
+                    )
                     if g is not None:
                         with self.binder.frame_context(can_skip=False, fall_through=3):
                             gt = get_proper_type(self.expr_checker.accept(g))
@@ -6166,11 +6178,22 @@ def visit_match_stmt(self, s: MatchStmt) -> None:
                     else:
                         self.accept(b)
                 self.push_type_map(else_map, from_assignment=False)
-                unmatched_types = else_map
 
-            if not is_unreachable_map(unmatched_types) and not self.current_node_deferred:
-                for typ in unmatched_types.values():
-                    self.msg.match_statement_inexhaustive_match(typ, s)
+            if not self.binder.is_unreachable() and not self.current_node_deferred:
+                # An opaque guard may leave an empty else_map (no new constraints),
+                # not an empty remainder. Consult the accumulated subject narrowing
+                # rather than the final case's map, which can also contain captures.
+                if all(g is None for g in s.guards) and is_product_exhaustive(
+                    subject_type, s.patterns, self.lookup_type_or_none
+                ):
+                    # This is the path where no case matched.
+                    # The enclosing binder frame merges the exits from case bodies separately.
+                    self.binder.unreachable()
+                else:
+                    remaining_type = self.expr_checker.narrow_type_from_binder(
+                        named_subject, subject_type
+                    )
+                    self.msg.match_statement_inexhaustive_match(remaining_type, s)
 
             # This is needed due to a quirk in frame_context. Without it types will stay narrowed
             # after the match.
@@ -6216,18 +6239,16 @@ def _get_recursive_sub_patterns_map(
         return sub_patterns_map
 
     def infer_variable_types_from_type_maps(
-        self, type_maps: list[TypeMap]
+        self, type_maps: list[dict[NameExpr, Type]]
     ) -> dict[SymbolNode, Type]:
         # Type maps may contain variables inherited from previous code which are not
         # necessary `Var`s (e.g. a function defined earlier with the same name).
         all_captures: dict[SymbolNode, list[tuple[NameExpr, Type]]] = defaultdict(list)
         for tm in type_maps:
-            if not is_unreachable_map(tm):
-                for expr, typ in tm.items():
-                    if isinstance(expr, NameExpr):
-                        node = expr.node
-                        assert node is not None
-                        all_captures[node].append((expr, typ))
+            for expr, typ in tm.items():
+                node = expr.node
+                assert node is not None
+                all_captures[node].append((expr, typ))
 
         inferred_types: dict[SymbolNode, Type] = {}
         for var, captures in all_captures.items():
@@ -6255,13 +6276,9 @@ def infer_variable_types_from_type_maps(
         return inferred_types
 
     def check_and_remove_capture_conflicts(
-        self, type_map: TypeMap, inferred_types: dict[SymbolNode, Type]
+        self, type_map: dict[NameExpr, Type], inferred_types: dict[SymbolNode, Type]
     ) -> None:
-        if is_unreachable_map(type_map):
-            return
         for expr, typ in list(type_map.items()):
-            if not isinstance(expr, NameExpr):
-                continue
             node = expr.node
             if node not in inferred_types or not self.check_subtype(
                 typ,
@@ -8311,6 +8328,7 @@ def conditional_types_with_intersection(
         default: None = None,
         *,
         consider_runtime_isinstance: bool = True,
+        intersection_errors: list[tuple[str, str]] | None = None,
     ) -> tuple[Type | None, Type | None]: ...
 
     @overload
@@ -8322,6 +8340,7 @@ def conditional_types_with_intersection(
         default: Type,
         *,
         consider_runtime_isinstance: bool = True,
+        intersection_errors: list[tuple[str, str]] | None = None,
     ) -> tuple[Type, Type]: ...
 
     def conditional_types_with_intersection(
@@ -8332,6 +8351,7 @@ def conditional_types_with_intersection(
         default: Type | None = None,
         *,
         consider_runtime_isinstance: bool = True,
+        intersection_errors: list[tuple[str, str]] | None = None,
     ) -> tuple[Type | None, Type | None]:
         initial_types = conditional_types(
             expr_type,
@@ -8381,8 +8401,13 @@ def conditional_types_with_intersection(
         if not out:
             # Only report errors if no element in the union worked.
             if self.should_report_unreachable_issues():
-                for types, reason in errors:
-                    self.msg.impossible_intersection(types, reason, ctx)
+                if intersection_errors is not None:
+                    # Pattern analysis decides reachability after combining all
+                    # alternatives. Return the reasons without emitting diagnostics.
+                    intersection_errors.extend(errors)
+                else:
+                    for types, reason in errors:
+                        self.msg.impossible_intersection(types, reason, ctx)
             return UninhabitedType(), expr_type
         new_yes_type = make_simplified_union(out)
         return new_yes_type, expr_type
diff --git a/mypy/checker_shared.py b/mypy/checker_shared.py
index 7ff7d3963431a..00c7da56737fe 100644
--- a/mypy/checker_shared.py
+++ b/mypy/checker_shared.py
@@ -233,12 +233,20 @@ def conditional_types_with_intersection(
         type_ranges: list[TypeRange] | None,
         ctx: Context,
         default: None = None,
+        *,
+        intersection_errors: list[tuple[str, str]] | None = None,
     ) -> tuple[Type | None, Type | None]: ...
 
     @overload
     @abstractmethod
     def conditional_types_with_intersection(
-        self, expr_type: Type, type_ranges: list[TypeRange] | None, ctx: Context, default: Type
+        self,
+        expr_type: Type,
+        type_ranges: list[TypeRange] | None,
+        ctx: Context,
+        default: Type,
+        *,
+        intersection_errors: list[tuple[str, str]] | None = None,
     ) -> tuple[Type, Type]: ...
 
     # Unfortunately, mypyc doesn't support abstract overloads yet.
@@ -249,6 +257,8 @@ def conditional_types_with_intersection(
         type_ranges: list[TypeRange] | None,
         ctx: Context,
         default: Type | None = None,
+        *,
+        intersection_errors: list[tuple[str, str]] | None = None,
     ) -> tuple[Type | None, Type | None]:
         raise NotImplementedError
 
diff --git a/mypy/checkpattern.py b/mypy/checkpattern.py
index 0e4786910e116..4546e96d5b1b3 100644
--- a/mypy/checkpattern.py
+++ b/mypy/checkpattern.py
@@ -3,6 +3,7 @@
 from __future__ import annotations
 
 from collections import defaultdict
+from collections.abc import Sequence
 from typing import Final, NamedTuple
 
 from mypy import message_registry
@@ -28,7 +29,8 @@
     ValuePattern,
 )
 from mypy.plugin import Plugin
-from mypy.subtypes import is_subtype
+from mypy.subtypes import is_same_type, is_subtype
+from mypy.traverser import TraverserVisitor
 from mypy.typeops import (
     coerce_to_literal,
     make_simplified_union,
@@ -43,6 +45,7 @@
     ProperType,
     TupleType,
     Type,
+    TypeAliasType,
     TypedDictType,
     TypeOfAny,
     TypeType,
@@ -82,7 +85,7 @@
 class PatternType(NamedTuple):
     type: Type  # The type the match subject can be narrowed to
     rest_type: Type  # The remaining type if the pattern didn't match
-    captures: dict[Expression, Type]  # The variables captured by the pattern
+    captures: dict[NameExpr, Type]  # The variables captured by the pattern
 
 
 class PatternChecker(PatternVisitor[PatternType]):
@@ -126,12 +129,41 @@ def __init__(
             non_sequence_match_type_names
         )
         self.options = options
+        self.or_bindings: dict[OrPattern, dict[str, NameExpr]] = {}
+        self.reachable_patterns: set[Pattern] = set()
+        self.intersection_errors: dict[Pattern, list[tuple[str, str]]] = {}
+
+    def check_pattern(
+        self, pattern: Pattern, typ: Type, bindings: dict[OrPattern, dict[str, NameExpr]]
+    ) -> PatternType:
+        """Analyze one case, combining reachability before reporting intersections."""
+        self.or_bindings = bindings
+        self.reachable_patterns.clear()
+        self.intersection_errors.clear()
+        result = self.accept(pattern, typ)
+        for node, errors in self.intersection_errors.items():
+            if node not in self.reachable_patterns:
+                for types, reason in errors:
+                    self.msg.impossible_intersection(types, reason, node)
+        return result
 
     def accept(self, o: Pattern, type_context: Type) -> PatternType:
         self.type_context.append(type_context)
         result = o.accept(self)
         self.type_context.pop()
+        if not is_uninhabited(result.type):
+            self.reachable_patterns.add(o)
+        return result
 
+    def narrow_pattern(
+        self, typ: Type, ranges: list[TypeRange], pattern: Pattern, *, default: Type
+    ) -> tuple[Type, Type]:
+        errors: list[tuple[str, str]] = []
+        result = self.chk.conditional_types_with_intersection(
+            typ, ranges, pattern, default=default, intersection_errors=errors
+        )
+        if errors:
+            self.intersection_errors.setdefault(pattern, []).extend(errors)
         return result
 
     def visit_as_pattern(self, o: AsPattern) -> PatternType:
@@ -143,9 +175,15 @@ def visit_as_pattern(self, o: AsPattern) -> PatternType:
             typ, rest_type, type_map = current_type, UninhabitedType(), {}
 
         if not is_uninhabited(typ) and o.name is not None:
-            typ, _ = self.chk.conditional_types_with_intersection(
-                current_type, [get_type_range(typ)], o, default=current_type
-            )
+            proper_type = get_proper_type(typ)
+            if typ is current_type and isinstance(proper_type, UnionType):
+                # This union already describes every captured value. Intersecting
+                # each member with the entire union again adds no information.
+                typ = make_simplified_union(proper_type.items)
+            else:
+                typ, _ = self.narrow_pattern(
+                    current_type, [get_type_range(typ)], o, default=current_type
+                )
             if not is_uninhabited(typ):
                 type_map[o.name] = typ
 
@@ -175,28 +213,30 @@ def visit_or_pattern(self, o: OrPattern) -> PatternType:
         #
         # Check the capture types
         #
-        capture_types: dict[Var, list[tuple[Expression, Type]]] = defaultdict(list)
+        capture_types: dict[Var, list[tuple[NameExpr, Type]]] = defaultdict(list)
         # Collect captures from the first subpattern
         for expr, typ in pattern_types[0].captures.items():
             node = get_var(expr)
             capture_types[node].append((expr, typ))
 
-        # Check if other subpatterns capture the same names
-        for i, pattern_type in enumerate(pattern_types[1:]):
-            vars = {get_var(expr) for expr, _ in pattern_type.captures.items()}
-            if capture_types.keys() != vars:
-                self.msg.fail(message_registry.OR_PATTERN_ALTERNATIVE_NAMES, o.patterns[i])
+        # Syntax has already been validated. Reuse the same capture expressions
+        # regardless of which alternative can match the current subject type.
+        bindings = self.or_bindings[o]
+        for pattern_type in pattern_types[1:]:
             for expr, typ in pattern_type.captures.items():
                 node = get_var(expr)
                 capture_types[node].append((expr, typ))
 
-        captures: dict[Expression, Type] = {}
+        captures: dict[NameExpr, Type] = {}
         for capture_list in capture_types.values():
             typ = UninhabitedType()
             for _, other in capture_list:
                 typ = make_simplified_union([typ, other])
 
-            captures[capture_list[0][0]] = typ
+            capture = capture_list[0][0]
+            # Imported aliases can have a different Var.name. The binding map
+            # uses the name written in the pattern, not the declaration's name.
+            captures[bindings[capture.name]] = typ
 
         union_type = make_simplified_union(types)
         return PatternType(union_type, current_type, captures)
@@ -225,7 +265,7 @@ def visit_singleton_pattern(self, o: SingletonPattern) -> PatternType:
         else:
             assert False
 
-        narrowed_type, rest_type = self.chk.conditional_types_with_intersection(
+        narrowed_type, rest_type = self.narrow_pattern(
             current_type, [get_type_range(typ)], o, default=current_type
         )
         return PatternType(narrowed_type, rest_type, {})
@@ -254,7 +294,7 @@ def visit_sequence_pattern(self, o: SequencePattern) -> PatternType:
         if isinstance(current_type, UnionType):
             match_types: list[Type] = []
             rest_types: list[Type] = []
-            captures_list: dict[Expression, list[Type]] = {}
+            captures_list: dict[NameExpr, list[Type]] = {}
 
             if star_position is not None:
                 star_pattern = o.patterns[star_position]
@@ -284,7 +324,7 @@ def visit_sequence_pattern(self, o: SequencePattern) -> PatternType:
 
             return PatternType(
                 make_simplified_union(match_types),
-                make_simplified_union(rest_types),
+                self.combine_tuple_remainders(rest_types, current_type),
                 {expr: make_simplified_union(types) for expr, types in captures_list.items()},
             )
 
@@ -329,7 +369,7 @@ def visit_sequence_pattern(self, o: SequencePattern) -> PatternType:
         #
         contracted_new_inner_types: list[Type] = []
         contracted_rest_inner_types: list[Type] = []
-        captures = {}  # dict[Expression, Type]
+        captures = {}
 
         contracted_inner_types = self.contract_starred_pattern_types(
             inner_types, star_position, required_patterns
@@ -359,26 +399,38 @@ def visit_sequence_pattern(self, o: SequencePattern) -> PatternType:
             else:
                 new_type = TupleType(new_inner_types, current_type.partial_fallback)
 
-            num_always_match = sum(is_uninhabited(typ) for typ in rest_inner_types)
-            if num_always_match == len(rest_inner_types):
-                # All subpatterns always match, so we can apply negative narrowing
-                rest_type = UninhabitedType()
-            elif num_always_match == len(rest_inner_types) - 1:
-                # Exactly one subpattern may conditionally match, the rest always match.
-                # We can apply negative narrowing to this one position.
-                rest_type = TupleType(
-                    [
-                        curr if is_uninhabited(rest) else rest
-                        for curr, rest in zip(inner_types, rest_inner_types)
-                    ],
-                    current_type.partial_fallback,
-                )
+                # A tuple fails to match at its first failing position. Preserve the
+                # matched prefix and the original suffix in each remaining alternative:
+                # (A, B) - (a, b) = (A - a, B) | (a, B - b).
+                # Irrefutable subpatterns (including starred captures) keep their types.
+                matched_types = [
+                    curr if is_uninhabited(rest) else new
+                    for curr, new, rest in zip(inner_types, new_inner_types, rest_inner_types)
+                ]
+                rest_items: list[Type] = []
+                for i, rest in enumerate(rest_inner_types):
+                    if is_uninhabited(rest):
+                        continue
+                    rest_item = TupleType(
+                        matched_types[:i] + [rest] + inner_types[i + 1 :],
+                        current_type.partial_fallback,
+                    )
+                    # Some complements cannot be expressed (e.g. int minus Literal[1]).
+                    # Avoid redundant expansion when one alternative is already the
+                    # entire original tuple, including when it contains Any.
+                    if is_same_type(rest_item, current_type):
+                        rest_items = [current_type]
+                        break
+                    rest_items.append(rest_item)
+                    if len(rest_items) > self.options.tuple_pattern_narrowing_limit:
+                        break
+                rest_type = self.combine_tuple_remainders(rest_items, current_type)
         elif isinstance(current_type, TupleType):
             # For variadic tuples it is too tricky to match individual items like for fixed
             # tuples, so we instead try to narrow the entire type.
             # TODO: use more precise narrowing when possible (e.g. for identical shapes).
             new_tuple_type = TupleType(new_inner_types, current_type.partial_fallback)
-            new_type, _ = self.chk.conditional_types_with_intersection(
+            new_type, _ = self.narrow_pattern(
                 new_tuple_type, [get_type_range(current_type)], o, default=new_tuple_type
             )
             if (
@@ -392,7 +444,7 @@ def visit_sequence_pattern(self, o: SequencePattern) -> PatternType:
             for typ in new_inner_types:
                 new_inner_type = join_types(new_inner_type, typ)
             new_type = self.construct_sequence_child(current_type, new_inner_type)
-            new_type, possible_rest_type = self.chk.conditional_types_with_intersection(
+            new_type, possible_rest_type = self.narrow_pattern(
                 current_type, [get_type_range(new_type)], o, default=current_type
             )
             if star_position is not None and len(o.patterns) == 1:
@@ -401,6 +453,35 @@ def visit_sequence_pattern(self, o: SequencePattern) -> PatternType:
 
         return PatternType(new_type, rest_type, captures)
 
+    def combine_tuple_remainders(self, items: list[Type], original: Type) -> Type:
+        proper_original = get_proper_type(original)
+        # Bound expansion, not narrowing of a union already supplied by the user.
+        limit = self.options.tuple_pattern_narrowing_limit
+        if isinstance(proper_original, UnionType):
+            limit = max(limit, len(proper_original.items))
+        # Counting only top-level alternatives misses expansion inside nested products.
+        memo: dict[int, tuple[Type, int]] = {}
+        complexity_limit = max(
+            self.options.tuple_pattern_narrowing_limit, tuple_pattern_complexity(original, memo)
+        )
+        complexity = 0
+        flattened: list[Type] = []
+        for item in items:
+            complexity += tuple_pattern_complexity(item, memo, complexity_limit - complexity)
+            if complexity > complexity_limit:
+                return original
+            proper_item = get_proper_type(item)
+            if isinstance(proper_item, UnionType):
+                flattened.extend(proper_item.items)
+            elif not is_uninhabited(proper_item):
+                flattened.append(item)
+            if len(flattened) > limit:
+                return original
+        result = make_simplified_union(flattened)
+        if tuple_pattern_complexity(result, memo, complexity_limit) > complexity_limit:
+            return original
+        return result
+
     def contract_starred_pattern_types(
         self, types: list[Type], star_pos: int | None, num_required_patterns: int
     ) -> list[Type]:
@@ -477,7 +558,7 @@ def expand_starred_pattern_types(
         return new_types
 
     def visit_starred_pattern(self, o: StarredPattern) -> PatternType:
-        captures: dict[Expression, Type] = {}
+        captures: dict[NameExpr, Type] = {}
         if o.capture is not None:
             list_type = self.chk.named_generic_type("builtins.list", [self.type_context[-1]])
             captures[o.capture] = list_type
@@ -486,7 +567,7 @@ def visit_starred_pattern(self, o: StarredPattern) -> PatternType:
     def visit_mapping_pattern(self, o: MappingPattern) -> PatternType:
         current_type = get_proper_type(self.type_context[-1])
         can_match = True
-        captures: dict[Expression, Type] = {}
+        captures: dict[NameExpr, Type] = {}
         for key, value in zip(o.keys, o.values):
             inner_type = self.get_mapping_item_type(o, current_type, key)
             if inner_type is None:
@@ -519,7 +600,7 @@ def visit_mapping_pattern(self, o: MappingPattern) -> PatternType:
             if not o.keys:
                 # Match cannot be refuted, so narrow the remaining type
                 mapping = self.chk.named_type("typing.Mapping")
-                if_type, else_type = self.chk.conditional_types_with_intersection(
+                if_type, else_type = self.narrow_pattern(
                     current_type,
                     [TypeRange(mapping, is_upper_bound=False)],
                     o,
@@ -579,7 +660,7 @@ def visit_class_pattern(self, o: ClassPattern) -> PatternType:
             return self.early_non_match()
         typ = UnionType.make_union([t.item for t in type_ranges])
 
-        new_type, rest_type = self.chk.conditional_types_with_intersection(
+        new_type, rest_type = self.narrow_pattern(
             current_type, type_ranges, o, default=current_type
         )
         if is_uninhabited(new_type):
@@ -593,7 +674,7 @@ def visit_class_pattern(self, o: ClassPattern) -> PatternType:
         keyword_pairs: list[tuple[str | None, Pattern]] = []
         match_arg_set: set[str] = set()
 
-        captures: dict[Expression, Type] = {}
+        captures: dict[NameExpr, Type] = {}
 
         if len(o.positionals) != 0:
             if self.should_self_match(typ):
@@ -792,7 +873,7 @@ def generate_types_from_names(self, type_names: list[str]) -> list[Type]:
         return types
 
     def update_type_map(
-        self, original_type_map: dict[Expression, Type], extra_type_map: dict[Expression, Type]
+        self, original_type_map: dict[NameExpr, Type], extra_type_map: dict[NameExpr, Type]
     ) -> None:
         # Calculating this would not be needed if TypeMap directly used literal hashes instead of
         # expressions, as suggested in the TODO above it's definition
@@ -846,6 +927,84 @@ def early_non_match(self) -> PatternType:
         return PatternType(UninhabitedType(), self.type_context[-1], {})
 
 
+class PatternBindingCollector(TraverserVisitor):
+    def __init__(
+        self, msg: MessageBuilder, or_bindings: dict[OrPattern, dict[str, NameExpr]]
+    ) -> None:
+        self.bindings: dict[str, NameExpr] = {}
+        self.msg = msg
+        self.or_bindings = or_bindings
+
+    def visit_or_pattern(self, o: OrPattern) -> None:
+        first: dict[str, NameExpr] | None = None
+        canonical: dict[str, NameExpr] = {}
+        for i, pattern in enumerate(o.patterns):
+            collector = PatternBindingCollector(self.msg, self.or_bindings)
+            pattern.accept(collector)
+            bindings = collector.bindings
+            if first is None:
+                first = bindings
+            elif first.keys() != bindings.keys():
+                # Invalid nested alternatives must be diagnosed even when type
+                # matching cannot reach them (e.g. inside a wrong-length tuple).
+                self.msg.fail(message_registry.OR_PATTERN_ALTERNATIVE_NAMES, o.patterns[i - 1])
+            for name, expr in bindings.items():
+                canonical.setdefault(name, expr)
+        self.or_bindings[o] = canonical
+        for name, expr in canonical.items():
+            self.bindings.setdefault(name, expr)
+
+    def visit_as_pattern(self, o: AsPattern) -> None:
+        if o.name is not None:
+            self.bindings.setdefault(o.name.name, o.name)
+        super().visit_as_pattern(o)
+
+    def visit_starred_pattern(self, o: StarredPattern) -> None:
+        if o.capture is not None:
+            self.bindings.setdefault(o.capture.name, o.capture)
+        super().visit_starred_pattern(o)
+
+    def visit_mapping_pattern(self, o: MappingPattern) -> None:
+        if o.rest is not None:
+            self.bindings.setdefault(o.rest.name, o.rest)
+        super().visit_mapping_pattern(o)
+
+
+def analyze_pattern_bindings(
+    patterns: Sequence[Pattern], msg: MessageBuilder
+) -> dict[OrPattern, dict[str, NameExpr]]:
+    """Validate OR bindings once, independently of type-based pattern reachability."""
+    bindings: dict[OrPattern, dict[str, NameExpr]] = {}
+    collector = PatternBindingCollector(msg, bindings)
+    for pattern in patterns:
+        pattern.accept(collector)
+    return bindings
+
+
+def tuple_pattern_complexity(
+    typ: Type, memo: dict[int, tuple[Type, int]], limit: int | None = None
+) -> int:
+    """Count represented tuple occurrences without unfolding recursive definitions."""
+    if cached := memo.get(id(typ)):
+        return cached[1]
+    if isinstance(typ, TypeAliasType) and typ.is_recursive:
+        children = typ.args
+        count = 0
+    else:
+        proper_type = get_proper_type(typ)
+        children = proper_type.items if isinstance(proper_type, (TupleType, UnionType)) else []
+        count = int(isinstance(proper_type, TupleType))
+    for child in children:
+        count += tuple_pattern_complexity(child, memo, None if limit is None else limit - count)
+        if limit is not None and count > limit:
+            return limit + 1
+    # Keep the object alive: expanding an alias may allocate temporary types, whose
+    # identities must not be reused while this memo is in use. Count each occurrence
+    # separately even when two positions refer to the same object.
+    memo[id(typ)] = (typ, count)
+    return count
+
+
 def get_match_arg_names(typ: TupleType) -> list[str | None]:
     args: list[str | None] = []
     for item in typ.items:
@@ -857,12 +1016,11 @@ def get_match_arg_names(typ: TupleType) -> list[str | None]:
     return args
 
 
-def get_var(expr: Expression) -> Var:
+def get_var(expr: NameExpr) -> Var:
     """
     Warning: this in only true for expressions captured by a match statement.
     Don't call it from anywhere else
     """
-    assert isinstance(expr, NameExpr), expr
     node = expr.node
     assert isinstance(node, Var), node
     return node
diff --git a/mypy/options.py b/mypy/options.py
index 40fa56bd1b3ba..cff499113dcea 100644
--- a/mypy/options.py
+++ b/mypy/options.py
@@ -81,6 +81,7 @@ class BuildType:
         "untyped_calls_exclude",
         "enable_incomplete_feature",
         "install_types",
+        "tuple_pattern_narrowing_limit",
     }
 ) - {"debug_cache"}
 
@@ -330,6 +331,10 @@ def __init__(self) -> None:
         # Not in the config file or command line.
         self.inspections = False
 
+        # Bound tuple-pattern remainder expansion, retaining the original type if exceeded.
+        # Internal only: tests can lower this independently of the coverage budget.
+        self.tuple_pattern_narrowing_limit = 1024
+
         # Disable the memory optimization of freeing ASTs when
         # possible. This isn't exposed as a command line option
         # because it is intended for software integrating with
diff --git a/mypy/patterncoverage.py b/mypy/patterncoverage.py
new file mode 100644
index 0000000000000..c15b4366b2ee9
--- /dev/null
+++ b/mypy/patterncoverage.py
@@ -0,0 +1,428 @@
+"""Bounded coverage proofs for fixed tuple products.
+
+Input types and AST nodes are treated as read-only.
+"""
+
+from __future__ import annotations
+
+from collections.abc import Callable, Mapping, Sequence
+from dataclasses import dataclass
+from types import MappingProxyType
+from typing import TypeAlias
+
+from mypy.nodes import (
+    BytesExpr,
+    Expression,
+    IntExpr,
+    MemberExpr,
+    RefExpr,
+    StrExpr,
+    TypeInfo,
+    UnaryExpr,
+)
+from mypy.patterns import (
+    AsPattern,
+    ClassPattern,
+    OrPattern,
+    Pattern,
+    SequencePattern,
+    SingletonPattern,
+    ValuePattern,
+)
+from mypy.typeops import literal_values
+from mypy.types import (
+    Instance,
+    LiteralType,
+    NoneType,
+    ProperType,
+    TupleType,
+    Type,
+    TypeAliasType,
+    UnionType,
+    find_unpack_in_list,
+    get_proper_type,
+)
+
+
+@dataclass(frozen=True)
+class ValueDomain:
+    """Type alternatives represented by one coverage-matrix column."""
+
+    alternatives: tuple[ProperType, ...]
+
+
+@dataclass(frozen=True)
+class TupleDomain:
+    """The component domains of a fixed-length tuple."""
+
+    items: tuple[ValueDomain | TupleDomain, ...]
+
+
+Domain: TypeAlias = ValueDomain | TupleDomain
+Row: TypeAlias = tuple[int, ...]
+Matrix: TypeAlias = tuple[Row, ...]
+
+
+@dataclass(frozen=True)
+class _VisitType:
+    typ: Type
+
+
+@dataclass(frozen=True)
+class _FinishTuple:
+    typ: TupleType
+
+
+def build_domain(subject: Type, *, work_limit: int) -> Domain | None:
+    """Build a domain for the subject type.
+
+    Return None if the type is unsupported or the budget runs out.
+    """
+    # Use a stack to handle deeply nested tuple aliases without Python recursion.
+    pending: list[_VisitType | _FinishTuple] = [_VisitType(subject)]
+    built: list[Domain] = []
+    while pending:
+        task = pending.pop()
+        if isinstance(task, _FinishTuple):
+            start = len(built) - len(task.typ.items)
+            built[start:] = [TupleDomain(tuple(built[start:]))]
+            continue
+        typ = task.typ
+        work_limit -= 1
+        if work_limit < 0:
+            return None
+        if isinstance(typ, TypeAliasType) and (typ.alias is None or typ.is_recursive):
+            return None
+        proper = get_proper_type(typ)
+        match proper:
+            case TupleType(items=items, partial_fallback=fallback):
+                if (
+                    fallback.type.fullname != "builtins.tuple"
+                    or find_unpack_in_list(items) is not None
+                ):
+                    return None
+                work_limit -= len(items)
+                if work_limit < 0:
+                    return None
+                pending.append(_FinishTuple(proper))
+                pending.extend(_VisitType(item) for item in reversed(items))
+                continue
+            case UnionType(items=variants):
+                pass
+            case _:
+                variants = [proper]
+        alternatives: list[ProperType] = []
+        for variant in variants:
+            work_limit -= 1
+            if work_limit < 0:
+                return None
+            if isinstance(variant, TypeAliasType) and (
+                variant.alias is None or variant.is_recursive
+            ):
+                return None
+            value = get_proper_type(variant)
+            match value:
+                case Instance(last_known_value=LiteralType() as literal):
+                    alternatives.append(literal)
+                case Instance():
+                    values = literal_values(value)
+                    if values is not None and len(values) <= work_limit:
+                        work_limit -= len(values)
+                        alternatives.extend(LiteralType(item, value) for item in values)
+                    else:
+                        # Keep unavailable or oversized expansions opaque, never partial.
+                        alternatives.append(value)
+                case _:
+                    alternatives.append(value)
+        if not alternatives:
+            return None
+        built.append(ValueDomain(tuple(alternatives)))
+    return built[0]
+
+
+def full_row(domain: Domain) -> Row:
+    """Flatten a bounded domain into a full-coverage bitset for each column."""
+    pending = [domain]
+    masks = []
+    while pending:
+        match pending.pop():
+            case ValueDomain(alternatives=alternatives):
+                masks.append((1 << len(alternatives)) - 1)
+            case TupleDomain(items=items):
+                pending.extend(reversed(items))
+    return tuple(masks)
+
+
+def _resolve_literals(
+    patterns: Sequence[Pattern],
+    lookup_type: Callable[[Expression], Type | None],
+    *,
+    work_limit: int,
+) -> tuple[Mapping[Expression, LiteralType], int] | None:
+    """Read cached types for literal and enum-member patterns.
+
+    The result includes the remaining budget. Return None if it runs out.
+    """
+    work_limit -= len(patterns)
+    if work_limit < 0:
+        return None
+    pending = list(reversed(patterns))
+    literals: dict[Expression, LiteralType] = {}
+    while pending:
+        work_limit -= 1
+        if work_limit < 0:
+            return None
+        match pending.pop():
+            case AsPattern(pattern=inner) if inner is not None:
+                pending.append(inner)
+            case OrPattern(patterns=children) | SequencePattern(patterns=children):
+                work_limit -= len(children)
+                if work_limit < 0:
+                    return None
+                pending.extend(reversed(children))
+            case ValuePattern(expr=expr):
+                # Other dotted values may change between cases.
+                # Only literals and statically resolved enum members are safe to use here.
+                match expr:
+                    case IntExpr() | StrExpr() | BytesExpr():
+                        pass
+                    case UnaryExpr(op="+" | "-", expr=IntExpr()):
+                        pass
+                    case MemberExpr(expr=RefExpr(node=TypeInfo(is_enum=True))):
+                        pass
+                    case _:
+                        continue
+                match get_proper_type(lookup_type(expr)):
+                    case (LiteralType() as literal) | Instance(
+                        last_known_value=LiteralType() as literal
+                    ):
+                        literals[expr] = literal
+    return MappingProxyType(literals), work_limit
+
+
+def _covers_alternative(
+    pattern: Pattern,
+    alternative: ProperType,
+    literals: Mapping[Expression, LiteralType],
+    *,
+    work_limit: int,
+) -> tuple[bool, int] | None:
+    """Check whether the pattern matches every value in this alternative.
+
+    Return the answer and unused budget, or None if the budget runs out.
+    """
+    pending = [pattern]
+    while pending:
+        work_limit -= 1
+        if work_limit < 0:
+            return None
+        match pending.pop(), alternative:
+            case AsPattern(pattern=None), _:
+                return True, work_limit
+            case AsPattern(pattern=inner), _ if inner is not None:
+                pending.append(inner)
+            case OrPattern(patterns=alternatives), _:
+                work_limit -= len(alternatives)
+                if work_limit < 0:
+                    return None
+                pending.extend(reversed(alternatives))
+            case SingletonPattern(value=None), NoneType():
+                return True, work_limit
+            case SingletonPattern(value=expected), LiteralType(value=actual, fallback=fallback):
+                if fallback.type.fullname == "builtins.bool" and actual is expected:
+                    return True, work_limit
+            case (
+                ClassPattern(class_ref=ref, positionals=[], keyword_values=[]),
+                (Instance() as instance) | LiteralType(fallback=instance),
+            ):
+                target = ref.node
+                if (
+                    isinstance(target, TypeInfo)
+                    and not target.is_protocol
+                    and target in instance.type.mro
+                ):
+                    return True, work_limit
+            case ValuePattern(expr=expr), LiteralType():
+                if literals.get(expr) == alternative:
+                    return True, work_limit
+    return False, work_limit
+
+
+def _compile_row(
+    pattern: Pattern,
+    domain: Domain,
+    literals: Mapping[Expression, LiteralType],
+    *,
+    work_limit: int,
+) -> tuple[Matrix, int] | None:
+    """Compile a pattern into a coverage row.
+
+    Unsupported patterns produce no rows; running out of budget returns None.
+    """
+    pending: list[tuple[Pattern | None, Domain]] = [(pattern, domain)]
+    masks: list[int] = []
+    while pending:
+        work_limit -= 1
+        if work_limit < 0:
+            return None
+        current, node = pending.pop()
+        match current:
+            case AsPattern(pattern=inner):
+                pending.append((inner, node))
+                continue
+        match node:
+            case TupleDomain(items=items):
+                work_limit -= len(items)
+                if work_limit < 0:
+                    return None
+                match current:
+                    case None:
+                        pending.extend((None, child) for child in reversed(items))
+                    case SequencePattern(patterns=children) if len(children) == len(items):
+                        pending.extend(zip(reversed(children), reversed(items)))
+                    case _:
+                        return (), work_limit
+            case ValueDomain(alternatives=alternatives):
+                if current is None:
+                    masks.append((1 << len(alternatives)) - 1)
+                    continue
+                mask = 0
+                for i, alternative in enumerate(alternatives):
+                    result = _covers_alternative(
+                        current, alternative, literals, work_limit=work_limit
+                    )
+                    if result is None:
+                        return None
+                    covered, work_limit = result
+                    if covered:
+                        mask |= 1 << i
+                masks.append(mask)
+    return (tuple(masks),), work_limit
+
+
+def compile_patterns(
+    patterns: Sequence[Pattern],
+    domain: Domain,
+    literals: Mapping[Expression, LiteralType],
+    *,
+    work_limit: int,
+) -> tuple[Matrix, int] | None:
+    """Compile patterns into coverage rows, skipping patterns we can't handle.
+
+    Return the rows and unused budget, or None if the budget runs out.
+    """
+    work_limit -= len(patterns)
+    if work_limit < 0:
+        return None
+    pending = list(reversed(patterns))
+    rows: list[Row] = []
+    while pending:
+        work_limit -= 1
+        if work_limit < 0:
+            return None
+        pattern = pending.pop()
+        match pattern:
+            case AsPattern(pattern=inner) if inner is not None:
+                pending.append(inner)
+            case OrPattern(patterns=alternatives):
+                work_limit -= len(alternatives)
+                if work_limit < 0:
+                    return None
+                pending.extend(reversed(alternatives))
+            case _:
+                compiled = _compile_row(pattern, domain, literals, work_limit=work_limit)
+                if compiled is None:
+                    return None
+                compiled_rows, work_limit = compiled
+                rows.extend(compiled_rows)
+    return tuple(rows), work_limit
+
+
+def covers_product(domains: Row, rows: Matrix, *, work_limit: int) -> bool:
+    """Check whether the rows cover every combination of column values.
+
+    Each bit represents a type alternative.
+    Alternatives matched by the same rows are checked together.
+    Each step removes a column; a row covering all remaining columns finishes that branch.
+
+    False can mean there's an uncovered value or that the work budget ran out.
+    """
+    pending = [(domains, rows)]
+    seen: set[tuple[Row, Matrix]] = set()
+    while pending:
+        domain, matrix = pending.pop()
+        work_limit -= max(1, len(matrix) * len(domain))
+        if work_limit < 0:
+            return False
+        matrix = tuple(dict.fromkeys(row for row in matrix if all(row)))
+        if domain in matrix:
+            continue
+        if not matrix:
+            return False
+        key = domain, matrix
+        if key in seen:
+            continue
+        seen.add(key)
+
+        shortest = min(matrix, key=lambda row: sum(a != b for a, b in zip(row, domain)))
+        column = next(i for i, (a, b) in enumerate(zip(shortest, domain)) if a != b)
+        groups = [domain[column]]
+        for mask in dict.fromkeys(row[column] for row in matrix):
+            work_limit -= len(groups)
+            if work_limit < 0:
+                return False
+            split = []
+            for group in groups:
+                yes, no = group & mask, group & ~mask
+                if yes:
+                    split.append(yes)
+                if no:
+                    split.append(no)
+            groups = split
+        reduced_domain = domain[:column] + domain[column + 1 :]
+        for group in groups:
+            if (
+                shortest[column] & group
+                and shortest[:column] + shortest[column + 1 :] == reduced_domain
+            ):
+                continue
+            work_limit -= len(matrix) * max(1, len(domain))
+            if work_limit < 0:
+                return False
+            reduced_rows = tuple(
+                row[:column] + row[column + 1 :] for row in matrix if row[column] & group
+            )
+            if not reduced_rows:
+                return False
+            pending.append((reduced_domain, reduced_rows))
+    return True
+
+
+def is_product_exhaustive(
+    subject: Type,
+    patterns: Sequence[Pattern],
+    lookup_type: Callable[[Expression], Type | None],
+    *,
+    limit: int = 1024,
+) -> bool:
+    """Check whether an unguarded tuple match is exhaustive.
+
+    Alternatives can overlap, so a pattern must cover all values of an alternative for it to count.
+    Guards must be excluded because they can change the values used by later patterns.
+    False means we couldn't prove coverage.
+    """
+    if not isinstance(get_proper_type(subject), TupleType):
+        return False
+    domain = build_domain(subject, work_limit=limit)
+    if domain is None:
+        return False
+    full = full_row(domain)
+    resolved = _resolve_literals(patterns, lookup_type, work_limit=limit * max(1, len(full)))
+    if resolved is None:
+        return False
+    literals, remaining = resolved
+    compiled = compile_patterns(patterns, domain, literals, work_limit=remaining)
+    if compiled is None:
+        return False
+    rows, remaining = compiled
+    return covers_product(full, rows, work_limit=remaining)
diff --git a/mypy/test/testcheck.py b/mypy/test/testcheck.py
index 377b10ad86d24..0aa2d1c7a6fdf 100644
--- a/mypy/test/testcheck.py
+++ b/mypy/test/testcheck.py
@@ -12,6 +12,7 @@
 from mypy import build
 from mypy.errors import CompileError
 from mypy.modulefinder import BuildSource, FindModuleCache, SearchPaths
+from mypy.options import Options
 from mypy.test.config import test_data_prefix, test_temp_dir
 from mypy.test.data import DataDrivenTestCase, DataSuite, FileOperation, module_from_path
 from mypy.test.helpers import (
@@ -107,6 +108,9 @@ def _filename(_msg: str) -> str:
             testcase.output[idx:], key=lambda msg: file_weights.get(_filename(msg), -1)
         )
 
+    def get_options(self, testcase: DataDrivenTestCase, incremental_step: int) -> Options:
+        return parse_options("\n".join(testcase.input), testcase, incremental_step)
+
     def run_case_once(
         self,
         testcase: DataDrivenTestCase,
@@ -136,7 +140,7 @@ def run_case_once(
             perform_file_operations(operations)
 
         # Parse options after moving files (in case mypy.ini is being moved).
-        options = parse_options(original_program_text, testcase, incremental_step)
+        options = self.get_options(testcase, incremental_step)
         options.use_builtins_fixtures = True
         options.show_traceback = True
         options.reveal_verbose_types = not testcase.name.endswith("_no_verbose_reveal")
diff --git a/mypy/test/testpatterncoverage.py b/mypy/test/testpatterncoverage.py
new file mode 100644
index 0000000000000..53ab64c1e3b91
--- /dev/null
+++ b/mypy/test/testpatterncoverage.py
@@ -0,0 +1,132 @@
+"""Independent coverage oracles and checker regressions with bounded narrowing."""
+
+from __future__ import annotations
+
+import itertools
+import random
+from unittest import TestCase
+
+from mypy.options import Options
+from mypy.patterns import AsPattern, OrPattern, SequencePattern, SingletonPattern
+from mypy.test import testcheck
+from mypy.test.data import DataDrivenTestCase
+from mypy.test.typefixture import TypeFixture
+from mypy.types import TupleType
+
+# Import after testcheck to avoid a typeops import cycle.
+from mypy.patterncoverage import (  # ruff: isort: skip
+    build_domain,
+    compile_patterns,
+    covers_product,
+    full_row,
+)
+
+
+class PatternCoverageSuite(TestCase):
+    def test_nested_compilation_and_budget_exhaustion(self) -> None:
+        fx = TypeFixture()
+        subject = TupleType(
+            [
+                fx.bool_type,
+                TupleType([fx.nonet, fx.bool_type], fx.std_tuple),
+                TupleType([], fx.std_tuple),
+            ],
+            fx.std_tuple,
+        )
+        domain = build_domain(subject, work_limit=100)
+        assert domain is not None
+        assert full_row(domain) == (3, 1, 3)
+        patterns = [
+            OrPattern(
+                [
+                    SequencePattern(
+                        [
+                            SingletonPattern(value),
+                            SequencePattern([SingletonPattern(None), AsPattern(None, None)]),
+                            SequencePattern([]),
+                        ]
+                    )
+                    for value in (False, True)
+                ]
+            )
+        ]
+        compiled = compile_patterns(patterns, domain, {}, work_limit=100)
+        assert compiled is not None
+        rows, remaining = compiled
+        assert rows == ((1, 1, 3), (2, 1, 3))
+        assert covers_product(full_row(domain), rows, work_limit=remaining)
+        spent = 100 - remaining
+        assert compile_patterns(patterns, domain, {}, work_limit=spent) == (rows, 0)
+        assert compile_patterns(patterns, domain, {}, work_limit=spent - 1) is None
+        # The wrong tuple length must discard the whole row, even if earlier components match.
+        wrong_shape = SequencePattern(
+            [
+                SingletonPattern(False),
+                AsPattern(None, None),
+                SequencePattern([AsPattern(None, None)]),
+            ]
+        )
+        skipped = compile_patterns([wrong_shape], domain, {}, work_limit=100)
+        assert skipped is not None and skipped[0] == ()
+
+    def test_deep_domains_and_patterns(self) -> None:
+        fx = TypeFixture()
+        subject = TupleType([], fx.std_tuple)
+        pattern = SequencePattern([])
+        for _ in range(1500):
+            subject = TupleType([subject], fx.std_tuple)
+            pattern = SequencePattern([pattern])
+        assert build_domain(subject, work_limit=100) is None
+        domain = build_domain(subject, work_limit=10_000)
+        assert domain is not None
+        assert full_row(domain) == ()
+        assert compile_patterns([pattern], domain, {}, work_limit=100) is None
+        compiled = compile_patterns([pattern], domain, {}, work_limit=10_000)
+        assert compiled is not None
+        rows, remaining = compiled
+        assert rows == ((),)
+        assert covers_product((), rows, work_limit=remaining)
+
+    def test_coverage_matches_enumeration(self) -> None:
+        rng = random.Random(21968)
+        for sizes in [(), (2,), (2, 2), (2, 2, 2), (3, 2, 3), (2,) * 5]:
+            domains = tuple((1 << size) - 1 for size in sizes)
+            points = list(itertools.product(*(range(size) for size in sizes)))
+            for _ in range(1000):
+                rows = tuple(
+                    tuple(rng.randrange(domain + 1) for domain in domains)
+                    for _ in range(rng.randrange(15))
+                )
+                expected = all(
+                    any(
+                        all(mask & (1 << value) for mask, value in zip(row, point)) for row in rows
+                    )
+                    for point in points
+                )
+                assert covers_product(domains, rows, work_limit=1_000_000) == expected
+                assert not covers_product(domains, rows, work_limit=0)
+
+    def test_large_product_and_missing_case(self) -> None:
+        domains = (3,) * 256
+        rows = []
+        for pair in range(128):
+            row = list(domains)
+            row[2 * pair] = row[2 * pair + 1] = 2
+            rows.append(tuple(row))
+        for column in (254, 255):
+            row = list(domains)
+            row[column] = 1
+            rows.append(tuple(row))
+        assert covers_product(domains, tuple(rows), work_limit=1024 * len(domains))
+        assert not covers_product(domains, tuple(rows), work_limit=100)
+        assert not covers_product(domains, tuple(rows[:-1]), work_limit=1_000_000)
+
+
+class PatternCoverageCheckSuite(testcheck.TypeCheckSuite):
+    files = ["patterncoverage.test"]
+
+    def get_options(self, testcase: DataDrivenTestCase, incremental_step: int) -> Options:
+        options = super().get_options(testcase, incremental_step)
+        # Force small examples through the coverage fallback, including in compiled builds.
+        options.tuple_pattern_narrowing_limit = 2
+        return options
diff --git a/mypy/test/testtypes.py b/mypy/test/testtypes.py
index 03b6f1def084d..f43b7cbafe2a1 100644
--- a/mypy/test/testtypes.py
+++ b/mypy/test/testtypes.py
@@ -31,11 +31,12 @@
 from mypy.subtypes import is_more_precise, is_proper_subtype, is_same_type, is_subtype
 from mypy.test.helpers import Suite, assert_equal, assert_type, skip
 from mypy.test.typefixture import InterfaceTypeFixture, TypeFixture
-from mypy.typeops import false_only, make_simplified_union, true_only
+from mypy.typeops import _TupleUnionIndex, false_only, make_simplified_union, true_only
 from mypy.types import (
     LITERAL_TYPE,
     AnyType,
     CallableType,
+    ErasedType,
     Instance,
     LiteralType,
     NoneType,
@@ -657,6 +658,152 @@ def test_simplify_very_large_union(self) -> None:
         # This shouldn't be very slow, even if the union is big.
         self.assert_simplified_union([*literals, fx.str_type], fx.str_type)
 
+    def test_simplified_union_large_tuple_product(self) -> None:
+        literals = [LiteralType(str(i), self.fx.str_type) for i in range(32)]
+        # Keep the correlation between positions: this is a diagonal, not the
+        # Cartesian product of the two columns.
+        rows = [self.tuple(item, item) for item in literals]
+        self.assert_simplified_union([*rows, *rows], UnionType(rows))
+
+    def test_simplified_union_large_tuple_product_subsumption(self) -> None:
+        rows = [self.tuple(LiteralType(str(i), self.fx.str_type), self.fx.b) for i in range(32)]
+        broad = self.tuple(self.fx.str_type, self.fx.a)
+        unrelated = self.tuple(self.fx.str_type, self.fx.d)
+        self.assert_simplified_union([*rows, broad, unrelated], UnionType([broad, unrelated]))
+
+    def test_simplified_union_large_tuple_product_arities(self) -> None:
+        rows: list[Type] = [self.tuple()]
+        rows.extend(
+            self.tuple(*[LiteralType(str(i), self.fx.str_type)] * (1 + i % 3)) for i in range(32)
+        )
+        self.assert_simplified_union(rows, UnionType(rows))
+        # A non-tuple member still participates in ordinary union simplification.
+        self.assert_simplified_union([*rows, self.fx.o], self.fx.o)
+
+    def test_simplified_union_large_nested_tuple_product(self) -> None:
+        rows = [
+            self.tuple(self.tuple(item, item), self.fx.b)
+            for item in (LiteralType(str(i), self.fx.str_type) for i in range(32))
+        ]
+        broad = self.tuple(self.tuple(self.fx.str_type, self.fx.str_type), self.fx.a)
+        self.assert_simplified_union([*rows, broad], broad)
+
+    def test_simplified_union_large_tuple_product_fallbacks(self) -> None:
+        literals = [LiteralType(str(i), self.fx.str_type) for i in range(8)]
+        rows: list[Type] = [
+            TupleType([item], fallback)
+            for item in literals
+            for fallback in (self.fx.a, self.fx.b, self.fx.d)
+        ]
+        # B inherits A, but D is unrelated. Equal items do not imply that two
+        # tuple types with distinct nominal fallbacks are interchangeable.
+        expected = [
+            TupleType([item], fallback) for item in literals for fallback in (self.fx.a, self.fx.d)
+        ]
+        self.assert_simplified_union(rows, UnionType(expected))
+
+    def test_simplified_union_large_tuple_product_any(self) -> None:
+        rows = [self.tuple(LiteralType(str(i), self.fx.str_type), self.fx.a) for i in range(32)]
+        broad = self.tuple(self.fx.str_type, self.fx.anyt)
+        # Proper subtyping must not erase precise alternatives in favor of Any.
+        self.assert_simplified_union([*rows, broad], UnionType([*rows, broad]))
+
+    def test_tuple_union_index_eligibility(self) -> None:
+        fixed = self.tuple(self.fx.a, self.fx.b)
+        assert _TupleUnionIndex.create([fixed], keep_erased=False) is None
+        assert _TupleUnionIndex.create([fixed] * 32, keep_erased=False) is not None
+        assert _TupleUnionIndex.create([fixed] * 32 + [self.fx.a], keep_erased=False) is None
+
+        variadic = self.tuple(UnpackType(self.fx.std_tuple))
+        assert _TupleUnionIndex.create([variadic] * 32, keep_erased=False) is None
+        recursive, _ = self.fx.def_alias_1(self.fx.a)
+        assert _TupleUnionIndex.create([self.tuple(recursive)] * 32, keep_erased=False) is None
+
+    def test_tuple_union_index_preserves_supertypes(self) -> None:
+        components = [
+            self.fx.a,
+            self.fx.b,
+            self.fx.c,
+            self.fx.o,
+            self.fx.anyt,
+            self.fx.nonet,
+            ErasedType(),
+            self.fx.lit1,
+        ]
+        rows = [self.tuple(left, right) for left in components for right in components[:3]]
+        rows.extend([self.tuple(), self.tuple(self.fx.a)])
+        queries = [*rows, self.tuple(self.fx.d, self.fx.d)]
+        queries.extend(
+            self.tuple(LiteralType(str(i), self.fx.str_type), self.fx.a) for i in range(100)
+        )
+
+        for strict_optional in (True, False):
+            with state.strict_optional_set(strict_optional):
+                for keep_erased in (True, False):
+                    index = _TupleUnionIndex.create(rows, keep_erased)
+                    assert index is not None
+                    for row, typ in enumerate(rows):
+                        expected_before_insert = {
+                            i
+                            for i, target in enumerate(rows[:row])
+                            if is_proper_subtype(
+                                typ, target, ignore_promotions=True, keep_erased_types=keep_erased
+                            )
+                        }
+                        assert expected_before_insert <= set(index.candidate_indices(typ))
+                        index.add(typ, row)
+                    for query in queries:
+                        candidates = index.candidate_indices(query)
+                        expected = {
+                            row
+                            for row, target in enumerate(rows)
+                            if is_proper_subtype(
+                                query,
+                                target,
+                                ignore_promotions=True,
+                                keep_erased_types=keep_erased,
+                            )
+                        }
+                        assert expected <= set(candidates)
+                        assert list(candidates) == sorted(set(candidates))
+                        assert all(0 <= row < len(rows) for row in candidates)
+                    assert not index.candidate_indices(self.tuple(self.fx.d, self.fx.d))
+                    # Queries remain correct after a stream of distinct types fills
+                    # the memo, and memoization storage stays bounded by input size.
+                    assert len(index._subtype_cache) <= len(rows)
+
+    def test_tuple_union_index_literal_columns(self) -> None:
+        literal = LiteralType("value", self.fx.a)
+        different_fallback = LiteralType("value", self.fx.d)
+        alias = self.fx.non_rec_alias(literal)
+        literal_union = UnionType([literal, self.fx.lit1])
+        targets = [
+            literal,
+            different_fallback,
+            alias,
+            self.fx.lit1,
+            self.fx.a,
+            self.fx.o,
+            self.fx.anyt,
+            literal_union,
+        ]
+        rows = [self.tuple(target, self.fx.a) for target in targets] * 4
+        index = _TupleUnionIndex.create(rows, keep_erased=False)
+        assert index is not None
+        for row, typ in enumerate(rows):
+            index.add(typ, row)
+
+        # Literal aliases must match both the value and the fallback type.
+        # Other sources still need normal subtype checks against literal targets.
+        for source in [*targets, self.fx.lit1_inst, ErasedType()]:
+            query = self.tuple(source, self.fx.a)
+            expected = [
+                row
+                for row, target in enumerate(rows)
+                if is_proper_subtype(query, target, ignore_promotions=True)
+            ]
+            assert list(index.candidate_indices(query)) == expected
+
     def test_simplified_union_with_str_instance_literals(self) -> None:
         fx = self.fx
 
diff --git a/mypy/typeops.py b/mypy/typeops.py
index eb9d0d1474b8b..c5f57163118a5 100644
--- a/mypy/typeops.py
+++ b/mypy/typeops.py
@@ -9,7 +9,7 @@
 
 import itertools
 from collections.abc import Callable, Iterable, Sequence
-from typing import Any, TypeVar, cast
+from typing import TypeVar, cast
 
 import mypy.subtypes
 from mypy.checker_state import checker_state
@@ -46,6 +46,7 @@
     FunctionLike,
     Instance,
     LiteralType,
+    LiteralValue,
     NoneType,
     NormalizedCallableType,
     Overloaded,
@@ -66,9 +67,11 @@
     UninhabitedType,
     UnionType,
     UnpackType,
+    find_unpack_in_list,
     flatten_nested_unions,
     get_proper_type,
     get_proper_types,
+    has_recursive_types,
     instance_cache,
     remove_dups,
 )
@@ -742,6 +745,7 @@ def _remove_redundant_union_items(items: list[Type], keep_erased: bool) -> list[
     # (by reversing the remaining items)
     for _direction in range(2):
         new_items: list[Type] = []
+        tuple_index = _TupleUnionIndex.create(items, keep_erased)
         # seen is a map from a type to its index in new_items
         seen: dict[ProperType, int] = {}
         unduplicated_literal_fallbacks: set[Instance] | None = None
@@ -770,7 +774,13 @@ def _remove_redundant_union_items(items: list[Type], keep_erased: bool) -> list[
                 pass
             else:
                 # If not, check if we've seen a supertype of this type
-                for j, tj in enumerate(new_items):
+                candidates = (
+                    tuple_index.candidate_indices(proper_ti)
+                    if tuple_index is not None and isinstance(proper_ti, TupleType)
+                    else range(len(new_items))
+                )
+                for j in candidates:
+                    tj = new_items[j]
                     proper_tj = get_proper_type(tj)
                     # If tj is an Instance with a last_known_value, do not remove proper_ti
                     # (unless it's an instance with the same last_known_value)
@@ -799,6 +809,8 @@ def _remove_redundant_union_items(items: list[Type], keep_erased: bool) -> list[
             else:
                 # We have a non-duplicate item, add it to new_items
                 seen[proper_ti] = len(new_items)
+                if tuple_index is not None and isinstance(proper_ti, TupleType):
+                    tuple_index.add(proper_ti, len(new_items))
                 new_items.append(ti)
                 if isinstance(proper_ti, LiteralType):
                     if unduplicated_literal_fallbacks is None:
@@ -813,6 +825,107 @@ def _remove_redundant_union_items(items: list[Type], keep_erased: bool) -> list[
     return items
 
 
+class _TupleUnionColumn:
+    """Separate exact literal targets from targets requiring subtype checks."""
+
+    def __init__(self) -> None:
+        self.literal_rows: dict[LiteralType, set[int]] = {}
+        self.general_rows: dict[Type, set[int]] = {}
+
+
+class _TupleUnionIndex:
+    """Find possible tuple supertypes without repeating whole-tuple comparisons.
+
+    A fixed tuple subtype must have compatible items at every position. Each
+    column maps an item type to the retained rows containing it. Intersecting
+    compatible rows across columns leaves candidates for the ordinary subtype
+    check, which still verifies fallbacks and other tuple-level constraints.
+
+    An index belongs to one simplification pass. Row IDs are append-only positions
+    in the caller's retained-item list. Widening a retained tuple's truthiness is
+    safe because it does not change its items; removing or reordering rows requires
+    a new index. Subtype options and the ambient typing context stay fixed for the
+    lifetime of its bounded memo.
+    """
+
+    def __init__(self, keep_erased: bool, cache_size: int) -> None:
+        self._context = mypy.subtypes.SubtypeContext(
+            keep_erased_types=keep_erased, ignore_promotions=True
+        )
+        self._max_cache_entries = cache_size
+        self._rows: dict[int, set[int]] = {}
+        self._columns: dict[int, list[_TupleUnionColumn]] = {}
+        self._subtype_cache: dict[tuple[Type, Type], bool] = {}
+
+    @classmethod
+    def create(cls, items: Sequence[Type], keep_erased: bool) -> _TupleUnionIndex | None:
+        # Index setup only pays off for larger unions. Other unions retain the
+        # generic scan, including tuples requiring recursive or variadic subtyping.
+        if len(items) < 16:
+            return None
+        for item in items:
+            typ = get_proper_type(item)
+            if isinstance(typ, UninhabitedType):
+                continue
+            if not isinstance(typ, TupleType):
+                return None
+            if find_unpack_in_list(typ.items) is not None or has_recursive_types(typ):
+                return None
+        return cls(keep_erased, cache_size=len(items))
+
+    def add(self, typ: TupleType, row: int) -> None:
+        width = len(typ.items)
+        self._rows.setdefault(width, set()).add(row)
+        if width not in self._columns:
+            self._columns[width] = [_TupleUnionColumn() for _ in typ.items]
+        for item, column in zip(typ.items, self._columns[width]):
+            proper_item = get_proper_type(item)
+            if isinstance(proper_item, LiteralType):
+                column.literal_rows.setdefault(proper_item, set()).add(row)
+            else:
+                column.general_rows.setdefault(item, set()).add(row)
+
+    def candidate_indices(self, typ: TupleType) -> Sequence[int]:
+        """Return ordered retained-row IDs, including every possible supertype."""
+        width = len(typ.items)
+        if width not in self._rows:
+            return ()
+        candidates = self._rows[width].copy()
+        for item, column in zip(typ.items, self._columns[width]):
+            proper_item = get_proper_type(item)
+            compatible: set[int]
+            targets: Iterable[tuple[Type, set[int]]]
+            if isinstance(proper_item, LiteralType):
+                # Literal-to-literal subtyping is equality, including the fallback.
+                # General targets (e.g. str or a union of literals) still need checks.
+                compatible = candidates.intersection(column.literal_rows.get(proper_item, ()))
+                targets = column.general_rows.items()
+            else:
+                compatible = set()
+                targets = itertools.chain(column.literal_rows.items(), column.general_rows.items())
+            for target, rows in targets:
+                if candidates.isdisjoint(rows):
+                    continue
+                if self._is_subtype(item, target):
+                    # Earlier columns have already ruled out the other rows.
+                    compatible.update(candidates.intersection(rows))
+            candidates = compatible
+            if not candidates:
+                return ()
+        # Preserve the generic simplifier's choice of the first retained supertype.
+        return sorted(candidates)
+
+    def _is_subtype(self, item: Type, target: Type) -> bool:
+        key = (item, target)
+        if key in self._subtype_cache:
+            return self._subtype_cache[key]
+        result = mypy.subtypes.is_proper_subtype(item, target, subtype_context=self._context)
+        # High-cardinality columns must not turn memoization into a quadratic cache.
+        if len(self._subtype_cache) < self._max_cache_entries:
+            self._subtype_cache[key] = result
+        return result
+
+
 def _get_type_method_ret_type(t: ProperType, *, name: str) -> Type | None:
     # For Enum literals the ret_type can change based on the Enum
     # we need to check the type of the enum rather than the literal
@@ -1088,6 +1201,18 @@ def is_literal_type_like(t: Type | None) -> bool:
         return False
 
 
+def literal_values(typ: Instance) -> Sequence[LiteralValue] | None:
+    """Return all literal values for the class, or None if unknown.
+
+    Enum literals use member names. Ignores last_known_value.
+    """
+    if typ.type.fullname == "builtins.bool":
+        return (False, True)
+    if typ.type.is_enum and not typ.type.has_base("enum.Flag"):
+        return typ.type.enum_members or None
+    return None
+
+
 def is_singleton_identity_type(typ: ProperType) -> bool:
     """
     Returns True if every value of this type is identical to every other value of this type,
@@ -1098,9 +1223,11 @@ def is_singleton_identity_type(typ: ProperType) -> bool:
     if isinstance(typ, NoneType):
         return True
     if isinstance(typ, Instance):
+        match literal_values(typ):
+            case [value] if is_singleton_identity_type(LiteralType(value, typ)):
+                return True
         return (
-            (typ.type.is_enum and len(typ.type.enum_members) == 1)
-            or (typ.type.fullname in ELLIPSIS_TYPE_NAMES)
+            (typ.type.fullname in ELLIPSIS_TYPE_NAMES)
             or (typ.type.fullname in NOT_IMPLEMENTED_TYPE_NAMES)
             or (typ.type.fullname in SENTINEL_TYPE_NAMES)
         )
@@ -1153,14 +1280,9 @@ class Status(Enum):
     if isinstance(typ, Instance) and (
         target_fullname is None or typ.type.fullname == target_fullname
     ):
-        if typ.type.fullname == "builtins.bool":
-            return UnionType([LiteralType(True, typ), LiteralType(False, typ)])
-
-        if typ.type.is_enum:
-            items = [LiteralType(name, typ) for name in typ.type.enum_members]
-            if not items:
-                return typ
-            return UnionType.make_union(items)
+        values = literal_values(typ)
+        if values is not None:
+            return UnionType.make_union([LiteralType(value, typ) for value in values])
 
     return typ
 
@@ -1179,28 +1301,23 @@ def try_contracting_literals_in_union(types: Sequence[Type]) -> list[ProperType]
     We also treat `Literal[True, False]` as `bool`.
     """
     proper_types = [get_proper_type(typ) for typ in types]
-    sum_types: dict[str, tuple[set[Any], list[int]]] = {}
+    sum_types: dict[str, tuple[set[LiteralValue], list[int]]] = {}
     marked_for_deletion = set()
     for idx, typ in enumerate(proper_types):
         if isinstance(typ, LiteralType):
             fullname = typ.fallback.type.fullname
-            if typ.fallback.type.is_enum or isinstance(typ.value, bool):
-                if fullname not in sum_types:
-                    sum_types[fullname] = (
-                        (
-                            set(typ.fallback.type.enum_members)
-                            if typ.fallback.type.is_enum
-                            else {True, False}
-                        ),
-                        [],
-                    )
-                literals, indexes = sum_types[fullname]
-                literals.discard(typ.value)
-                indexes.append(idx)
-                if not literals:
-                    first, *rest = indexes
-                    proper_types[first] = typ.fallback
-                    marked_for_deletion |= set(rest)
+            if fullname not in sum_types:
+                values = literal_values(typ.fallback)
+                if values is None:
+                    continue
+                sum_types[fullname] = (set(values), [])
+            literals, indexes = sum_types[fullname]
+            literals.discard(typ.value)
+            indexes.append(idx)
+            if not literals:
+                first, *rest = indexes
+                proper_types[first] = typ.fallback
+                marked_for_deletion |= set(rest)
     return list(
         itertools.compress(
             proper_types, [(i not in marked_for_deletion) for i in range(len(proper_types))]
@@ -1220,10 +1337,9 @@ def coerce_to_literal(typ: Type) -> Type:
     elif isinstance(typ, Instance):
         if typ.last_known_value:
             return typ.last_known_value
-        elif typ.type.is_enum:
-            enum_values = typ.type.enum_members
-            if len(enum_values) == 1:
-                return LiteralType(value=enum_values[0], fallback=typ)
+        match literal_values(typ):
+            case [value]:
+                return LiteralType(value, typ)
     return original_type
 
 
diff --git a/test-data/unit/check-python310.test b/test-data/unit/check-python310.test
index 33b952f48f49d..4b069ec23cdf4 100644
--- a/test-data/unit/check-python310.test
+++ b/test-data/unit/check-python310.test
@@ -2097,10 +2097,675 @@ match m6:
     case (1, "a"):
         reveal_type(m6)  # N: Revealed type is "tuple[Literal[1], Literal['a']]"
     case _:
-        reveal_type(m6)  # N: Revealed type is "tuple[Literal[1] | Literal[2], Literal['a'] | Literal['b']]"
+        reveal_type(m6)  # N: Revealed type is "tuple[Literal[2], Literal['a'] | Literal['b']] | tuple[Literal[1], Literal['b']]"
 
 [builtins fixtures/tuple.pyi]
 
+[case testMatchTupleProductBools]
+# flags: --enable-error-code exhaustive-match --warn-unreachable
+from typing import Literal
+
+def complete(a: bool, b: bool) -> int:
+    match a, b:
+        case True, True:
+            return 1
+        case True, False:
+            return 2
+        case False, True:
+            return 3
+        case False, False:
+            return 4
+
+def incomplete(a: bool, b: bool) -> None:
+    match a, b:  # E: Match statement has unhandled case for values of type "tuple[Literal[False], Literal[False]]" \
+                 # N: If match statement is intended to be non-exhaustive, add `case _: pass`
+        case True, True:
+            pass
+        case True, False:
+            pass
+        case False, True:
+            pass
+
+def captures(a: bool, b: bool) -> None:
+    match a, b:
+        case True, True:
+            pass
+        case True, False:
+            reveal_type(a)  # N: Revealed type is "Literal[True]"
+            reveal_type(b)  # N: Revealed type is "Literal[False]"
+        case False, _:
+            reveal_type(a)  # N: Revealed type is "Literal[False]"
+            reveal_type(b)  # N: Revealed type is "builtins.bool"
+        case _:
+            reveal_type(a)  # E: Statement is unreachable
+[builtins fixtures/tuple.pyi]
+
+[case testMatchTupleProductEnums]
+# flags: --enable-error-code exhaustive-match
+from enum import Enum
+from typing import NoReturn
+
+def assert_never(x: NoReturn) -> NoReturn: ...
+
+class A(Enum):
+    ONE = 1
+    TWO = 2
+class B(Enum):
+    ONE = 1
+    TWO = 2
+
+def f(pair: tuple[A, B]) -> int:
+    match pair:
+        case A.ONE, B.ONE:
+            return 1
+        case A.ONE, B.TWO:
+            return 2
+        case A.TWO, B.ONE:
+            return 3
+        case A.TWO, B.TWO:
+            return 4
+        case rest:
+            assert_never(rest)
+
+def g(a: A, b: B) -> int:
+    match a, b:
+        case A.ONE, B.ONE:
+            return 1
+        case A.ONE, B.TWO:
+            return 2
+        case A.TWO, B.ONE:
+            return 3
+        case A.TWO, B.TWO:
+            return 4
+[builtins fixtures/tuple.pyi]
+
+[case testMatchTupleProductResiduals]
+# flags: --strict-equality --warn-unreachable
+from typing import Literal
+
+def f(pair: tuple[Literal[1, 2], Literal["a", "b"]]) -> None:
+    match pair:
+        case 1, "a":
+            pass
+        case rest:
+            reveal_type(rest)  # N: Revealed type is "tuple[Literal[2], Literal['a'] | Literal['b']] | tuple[Literal[1], Literal['b']]"
+
+def g(triple: tuple[bool, int, bool]) -> None:
+    match triple:
+        case True, _, True:
+            pass
+        case rest:
+            reveal_type(rest)  # N: Revealed type is "tuple[Literal[False], builtins.int, builtins.bool] | tuple[Literal[True], builtins.int, Literal[False]]"
+
+def impossible(pair: tuple[Literal[1], Literal[2]]) -> None:
+    match pair:
+        case 1, 3:
+            reveal_type(pair)  # E: Statement is unreachable
+        case rest:
+            reveal_type(rest)  # N: Revealed type is "tuple[Literal[1], Literal[2]]"
+[builtins fixtures/tuple.pyi]
+
+[case testMatchTupleProductOrPatterns]
+# flags: --enable-error-code exhaustive-match --warn-unreachable
+def f(a: bool, b: bool) -> int:
+    match a, b:
+        case (True, True) | (False, False):
+            return 1
+        case (True, False) | (False, True):
+            return 2
+
+def g(a: bool, b: bool) -> None:
+    match a, b:
+        case (True, True) | (False, False):
+            pass
+        case (True, False) as pair:
+            reveal_type(pair)  # N: Revealed type is "tuple[Literal[True], Literal[False]]"
+        case (False, True) as pair:
+            reveal_type(pair)  # N: Revealed type is "tuple[Literal[False], Literal[True]]"
+[builtins fixtures/tuple.pyi]
+
+[case testMatchTupleProductUnionReachability]
+# flags: --warn-unreachable
+from typing import Literal
+
+V: tuple[Literal["a"], None] | tuple[Literal["b"], int] = ("a", None)
+match V:
+    case "a", None:
+        pass
+    case _:
+        pass
+
+def f(value: tuple[Literal["a"], None] | tuple[Literal["b"], int]) -> int:
+    match value:
+        case "a", None:
+            return 0
+        case "b", int(n):
+            return n
+[builtins fixtures/tuple.pyi]
+
+[case testMatchTupleProductClassReachability]
+# flags: --enable-error-code exhaustive-match --warn-unreachable
+class P:
+    def run(self, a: int) -> int: return a
+class Q:
+    def run(self, a: str) -> str: return a
+
+def same_kind(left: P | Q, right: P | Q) -> bool:
+    match left, right:
+        case P(), P():
+            return True
+        case Q(), Q():
+            return True
+        case _:
+            return False
+
+def complete(left: P | Q, right: P | Q) -> int:
+    match left, right:
+        case P(), P():
+            return 1
+        case P(), Q():
+            return 2
+        case Q(), P():
+            return 3
+        case Q(), Q():
+            return 4
+
+def diagonal(left: P | Q, right: P | Q) -> bool:
+    match left, right:
+        case (P(), P()) | (Q(), Q()):
+            return True
+        case _:
+            return False
+[builtins fixtures/tuple.pyi]
+
+[case testMatchTupleProductNestedAndStarred]
+# flags: --enable-error-code exhaustive-match --warn-unreachable
+from typing import NoReturn
+
+def assert_never(x: NoReturn) -> NoReturn: ...
+
+def nested(pair: tuple[bool, tuple[bool, bool]]) -> int:
+    match pair:
+        case True, (True, _):
+            return 1
+        case True, (False, _):
+            return 2
+        case False, (_, True):
+            return 3
+        case False, (_, False):
+            return 4
+
+def starred(value: tuple[bool, int, str, bool]) -> None:
+    match value:
+        case True, *middle, True:
+            reveal_type(middle)  # N: Revealed type is "builtins.list[builtins.int | builtins.str]"
+        case True, *_, False:
+            pass
+        case False, *_, True:
+            pass
+        case False, *_, False:
+            pass
+
+def empty(value: tuple[()]) -> None:
+    match value:
+        case ():
+            pass
+        case rest:
+            assert_never(rest)
+
+def singleton(value: tuple[bool]) -> int:
+    match value:
+        case (True,):
+            return 1
+        case (False,):
+            return 0
+
+def optional(value: tuple[int | None, str | None]) -> int:
+    match value:
+        case None, None:
+            return 0
+        case int(), None:
+            return 1
+        case None, str():
+            return 2
+        case int(), str():
+            return 3
+[builtins fixtures/tuple.pyi]
+
+[case testMatchTupleProductGuards]
+# flags: --enable-error-code exhaustive-match --warn-unreachable
+def guarded(a: bool, b: bool, guard: bool) -> None:
+    match a, b:  # E: Match statement has unhandled case for values of type "tuple[Literal[True], Literal[True]]" \
+                 # N: If match statement is intended to be non-exhaustive, add `case _: pass`
+        case True, True if guard:
+            pass
+        case True, False:
+            pass
+        case False, True:
+            pass
+        case False, False:
+            pass
+
+def fallback(a: bool, b: bool, guard: bool) -> int:
+    match a, b:
+        case True, True if guard:
+            return 1
+        case True, True:
+            return 2
+        case True, False:
+            return 3
+        case False, _:
+            return 4
+
+def always_true(a: bool, b: bool) -> int:
+    match a, b:
+        case True, True if True:
+            return 1
+        case True, False:
+            return 2
+        case False, _:
+            return 3
+
+def always_false(a: bool, b: bool) -> None:
+    match a, b:  # E: Match statement has unhandled case for values of type "tuple[Literal[True], Literal[True]]" \
+                 # N: If match statement is intended to be non-exhaustive, add `case _: pass`
+        case True, True if False:
+            pass  # E: Statement is unreachable
+        case True, False:
+            pass
+        case False, _:
+            pass
+
+def last_guarded(a: bool, b: bool, guard: bool) -> None:
+    match a, b:  # E: Match statement has unhandled case for values of type "tuple[Literal[False], bool] | tuple[Literal[True], Literal[True]]" \
+                 # N: If match statement is intended to be non-exhaustive, add `case _: pass`
+        case True, False:
+            pass
+        case _, False if guard:
+            pass
+
+def unreachable_tail(a: bool, b: bool) -> None:
+    match a, b:
+        case True, _:
+            pass
+        case False, _:
+            pass
+        case True, True:
+            pass  # E: Statement is unreachable
+
+def only_guarded(a: bool, b: bool, guard: bool) -> None:
+    match a, b:  # E: Match statement has unhandled case for values of type "tuple[bool, bool]" \
+                 # N: If match statement is intended to be non-exhaustive, add `case _: pass`
+        case True, True if guard:
+            pass
+
+def unreachable_guard(a: bool, b: bool, guard: bool) -> None:
+    match a, b:
+        case _, _:
+            pass
+        case True, True if guard:
+            pass  # E: Statement is unreachable
+[builtins fixtures/tuple.pyi]
+
+[case testMatchTupleProductConservativeRemainder]
+# flags: --enable-error-code exhaustive-match
+from typing import Any
+
+def unknown(value: tuple[Any, bool]) -> None:
+    match value:  # E: Match statement has unhandled case for values of type "tuple[Any, bool]" \
+                  # N: If match statement is intended to be non-exhaustive, add `case _: pass`
+        case True, True:
+            pass
+        case False, False:
+            pass
+
+def open_type(value: tuple[int, int]) -> None:
+    match value:  # E: Match statement has unhandled case for values of type "tuple[int, int]" \
+                  # N: If match statement is intended to be non-exhaustive, add `case _: pass`
+        case 1, 2:
+            pass
+        case 3, 4:
+            pass
+
+class A: pass
+class B: pass
+class Both(A, B): pass
+
+def overlapping(value: tuple[A | B, A | B]) -> None:
+    match value:
+        case A(), A():
+            pass
+        case A(), B():
+            pass
+        case B(), A():
+            pass
+        case B(), B():
+            pass
+
+def diagonal(value: tuple[A | B, A | B]) -> None:
+    match value:  # E: Match statement has unhandled case for values of type "tuple[B, A] | tuple[A, B]" \
+                  # N: If match statement is intended to be non-exhaustive, add `case _: pass`
+        case A(), A():
+            pass
+        case B(), B():
+            pass
+[builtins fixtures/tuple.pyi]
+
+[case testMatchTupleProductUnreachableAndInvalidPatterns]
+# flags: --warn-unreachable
+from typing import Literal
+
+def unreachable(value: tuple[Literal["a"], int] | tuple[Literal["b"], str]) -> None:
+    match value:
+        case _, None:  # E: Subclass of "int" and "NoneType" cannot exist: "NoneType" is final \
+                       # E: Subclass of "str" and "NoneType" cannot exist: "NoneType" is final
+            reveal_type(value)  # E: Statement is unreachable
+        case _:
+            pass
+
+class P:
+    __match_args__ = ("value",)
+    value: int
+    def run(self, x: int) -> int: return x
+class Q:
+    def run(self, x: str) -> str: return x
+
+def invalid(value: tuple[P, None] | tuple[Q, int]) -> None:
+    match value:
+        case P(first, second), None:  # E: Too many positional patterns for class pattern \
+                                     # E: Subclass of "Q" and "P" cannot exist: would have incompatible method signatures
+            pass  # E: Statement is unreachable
+        case P(missing=field), None:  # E: Class "__main__.P" has no attribute "missing"
+            pass
+        case _:
+            pass
+[builtins fixtures/tuple.pyi]
+
+[case testMatchTupleProductLengths]
+# flags: --enable-error-code exhaustive-match --warn-unreachable
+def f(value: tuple[()] | tuple[bool] | tuple[bool, bool]) -> int:
+    match value:
+        case ():
+            return 0
+        case (True,):
+            return 1
+        case (False,):
+            return 2
+        case True, True:
+            return 3
+        case True, False:
+            return 4
+        case False, True:
+            return 5
+        case False, False:
+            return 6
+[builtins fixtures/tuple.pyi]
+
+[case testMatchTupleProductExpansionLimit]
+# flags: --enable-error-code exhaustive-match --warn-unreachable
+# Each case splits every remaining alternative on a new pair of positions. The
+# all-False tuple still reaches the fallback even when narrowing hits its limit.
+def f(value: tuple[bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool]) -> bool:
+    match value:
+        case True, True, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _:
+            return True
+        case _, _, True, True, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _:
+            return True
+        case _, _, _, _, True, True, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _:
+            return True
+        case _, _, _, _, _, _, True, True, _, _, _, _, _, _, _, _, _, _, _, _, _, _:
+            return True
+        case _, _, _, _, _, _, _, _, True, True, _, _, _, _, _, _, _, _, _, _, _, _:
+            return True
+        case _, _, _, _, _, _, _, _, _, _, True, True, _, _, _, _, _, _, _, _, _, _:
+            return True
+        case _, _, _, _, _, _, _, _, _, _, _, _, True, True, _, _, _, _, _, _, _, _:
+            return True
+        case _, _, _, _, _, _, _, _, _, _, _, _, _, _, True, True, _, _, _, _, _, _:
+            return True
+        case _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, True, True, _, _, _, _:
+            return True
+        case _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, True, True, _, _:
+            return True
+        case _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, True, True:
+            return True
+        case rest:
+            reveal_type(rest[0])  # N: Revealed type is "Literal[False] | Literal[True]"
+            return False
+[builtins fixtures/tuple.pyi]
+
+[case testMatchTupleProductLargeExhaustive]
+# flags: --enable-error-code exhaustive-match --warn-unreachable
+# Narrowing exceeds its 1024-alternative limit here.
+# The coverage check should still prove the match exhaustive.
+def f(value: tuple[bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool]) -> int:
+    match value:
+        case True, True, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _:
+            return 1
+        case _, _, True, True, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _:
+            return 1
+        case _, _, _, _, True, True, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _:
+            return 1
+        case _, _, _, _, _, _, True, True, _, _, _, _, _, _, _, _, _, _, _, _, _, _:
+            return 1
+        case _, _, _, _, _, _, _, _, True, True, _, _, _, _, _, _, _, _, _, _, _, _:
+            return 1
+        case _, _, _, _, _, _, _, _, _, _, True, True, _, _, _, _, _, _, _, _, _, _:
+            return 1
+        case _, _, _, _, _, _, _, _, _, _, _, _, True, True, _, _, _, _, _, _, _, _:
+            return 1
+        case _, _, _, _, _, _, _, _, _, _, _, _, _, _, True, True, _, _, _, _, _, _:
+            return 1
+        case _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, True, True, _, _, _, _:
+            return 1
+        case _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, True, True, _, _:
+            return 1
+        case _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, True, True:
+            return 1
+        case _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, False, _:
+            return 0
+        case _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, False:
+            return 0
+[builtins fixtures/tuple.pyi]
+
+[case testMatchTupleProductOpenEnum]
+# flags: --enable-error-code exhaustive-match
+from enum import Enum
+
+class Open(Enum): pass
+class E(Open):
+    A = 1
+
+def base(x: tuple[Enum | bool, bool]) -> int: # E: Missing return statement
+    match x: # E: Match statement has unhandled case for values of type "tuple[Enum, bool]" \
+             # N: If match statement is intended to be non-exhaustive, add `case _: pass`
+        case True, _: return 1
+        case False, _: return 0
+
+def subclassable(x: tuple[Open | bool, bool]) -> int: # E: Missing return statement
+    match x: # E: Match statement has unhandled case for values of type "tuple[Open, bool]" \
+             # N: If match statement is intended to be non-exhaustive, add `case _: pass`
+        case True, _: return 1
+        case False, _: return 0
+
+base((E.A, True))
+subclassable((E.A, True))
+[builtins fixtures/tuple.pyi]
+
+[case testMatchUnchangedUnionCapture]
+from typing import Any, NewType
+
+class A: pass
+class B: pass
+Tagged = NewType("Tagged", int)
+Alias = A | B
+
+def aliased(value: Alias) -> None:
+    match value:
+        case captured:
+            reveal_type(captured)  # N: Revealed type is "__main__.A | __main__.B"
+
+def dynamic(value: Any | A) -> None:
+    match value:
+        case captured:
+            reveal_type(captured)  # N: Revealed type is "Any | __main__.A"
+
+def tagged(value: Tagged | str) -> None:
+    match value:
+        case captured:
+            reveal_type(captured)  # N: Revealed type is "__main__.Tagged | builtins.str"
+
+match True:
+    case captured_bool:
+        reveal_type(captured_bool)  # N: Revealed type is "Literal[True]"
+[builtins fixtures/tuple.pyi]
+
+[case testMatchTupleProductOrCaptureIdentity]
+# flags: --enable-error-code exhaustive-match --warn-unreachable
+def f(value: tuple[bool, bool]) -> bool:
+    match value:
+        case True, True:
+            return True
+        case ((True as flag) | (False as flag)), _:
+            reveal_type(flag)  # N: Revealed type is "builtins.bool"
+            return flag
+
+class A: pass
+class B: pass
+
+def g(value: tuple[A | B, bool]) -> A | B:
+    match value:
+        case A(), True:
+            return value[0]
+        case ((A() as item) | (B() as item)), _:
+            reveal_type(item)  # N: Revealed type is "__main__.A | __main__.B"
+            return item
+
+def invalid(value: tuple[bool, bool]) -> None:
+    match value:
+        case True, True:
+            pass
+        case ((True as flag) | False), _:  # E: Alternative patterns bind different names
+            pass
+
+def invalid_nested(value: tuple[bool]) -> None:
+    match value:
+        case [((True as x) | (False as y)), _] | [(True as x) as y]:  # E: Alternative patterns bind different names
+            pass
+        case _:
+            pass
+
+def invalid_unvisited(value: tuple[bool]) -> None:
+    match value:
+        case ((True as x) | (False as y)), _:  # E: Alternative patterns bind different names
+            pass  # E: Statement is unreachable
+        case _:
+            pass
+[builtins fixtures/tuple.pyi]
+
+[case testMatchTupleProductAliasedCaptureIdentity]
+# flags: --enable-error-code exhaustive-match --warn-unreachable
+from capture_source import exported as flag
+
+def f(value: tuple[bool, bool]) -> bool:
+    global flag
+    match value:
+        case True, True:
+            return True
+        case ((True as flag) | (False as flag)), _:
+            reveal_type(flag)  # N: Revealed type is "builtins.bool"
+            return flag
+[builtins fixtures/tuple.pyi]
+[file capture_source.py]
+exported: bool
+
+[case testMatchTupleProductImpossibleOrAlternative]
+# flags: --warn-unreachable
+def f(value: tuple[int] | tuple[str]) -> None:
+    match value:
+        case (None | int(),):  # E: Subclass of "int" and "NoneType" cannot exist: "NoneType" is final \
+                              # E: Subclass of "str" and "NoneType" cannot exist: "NoneType" is final
+            pass
+        case _:
+            pass
+
+def g(value: tuple[int] | tuple[str]) -> None:
+    match value:
+        case (int() | str(),):
+            pass
+
+def skipped_alternative(value: tuple[()] | tuple[int] | tuple[str]) -> None:
+    match value:
+        case (None | int(),):  # E: Subclass of "int" and "NoneType" cannot exist: "NoneType" is final \
+                              # E: Subclass of "str" and "NoneType" cannot exist: "NoneType" is final
+            pass
+        case _:
+            pass
+[builtins fixtures/tuple.pyi]
+
+[case testMatchTupleProductNestedMatchBindings]
+# flags: --enable-error-code exhaustive-match --warn-unreachable
+def f(outer: tuple[bool, bool], inner: tuple[int | str, bool]) -> None:
+    match outer:
+        case True, True:
+            match inner:
+                case ((int() as item) | (str() as item)), _:
+                    reveal_type(item)  # N: Revealed type is "builtins.int | builtins.str"
+        case ((True as flag) | (False as flag)), _:
+            reveal_type(flag)  # N: Revealed type is "builtins.bool"
+[builtins fixtures/tuple.pyi]
+
+[case testMatchTupleProductNestedExpansionLimit]
+# flags: --enable-error-code exhaustive-match --warn-unreachable
+Bools = tuple[bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool]
+
+def f(value: tuple[bool, Bools]) -> None:
+    match value:
+        case _, (True, True, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _):
+            pass
+        case _, (_, _, True, True, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _):
+            pass
+        case _, (_, _, _, _, True, True, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _):
+            pass
+        case _, (_, _, _, _, _, _, True, True, _, _, _, _, _, _, _, _, _, _, _, _, _, _):
+            pass
+        case _, (_, _, _, _, _, _, _, _, True, True, _, _, _, _, _, _, _, _, _, _, _, _):
+            pass
+        case _, (_, _, _, _, _, _, _, _, _, _, True, True, _, _, _, _, _, _, _, _, _, _):
+            pass
+        case _, (_, _, _, _, _, _, _, _, _, _, _, _, True, True, _, _, _, _, _, _, _, _):
+            pass
+        case _, (_, _, _, _, _, _, _, _, _, _, _, _, _, _, True, True, _, _, _, _, _, _):
+            pass
+        case _, (_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, True, True, _, _, _, _):
+            pass
+        case _, (_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, True, True, _, _):
+            pass
+        case _, (_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, True, True):
+            pass
+        case _, (False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False):
+            reveal_type(value[1][-1])  # N: Revealed type is "Literal[False]"
+        case rest:
+            reveal_type(rest[1][-2:])  # N: Revealed type is "tuple[builtins.bool, builtins.bool]"
+[builtins fixtures/tuple.pyi]
+
+[case testMatchTupleProductRecursiveAliasBudget]
+# flags: --enable-error-code exhaustive-match --warn-unreachable
+Tree = tuple["Tree", "Tree"] | None
+
+def f(value: tuple[bool, bool, Tree]) -> int:
+    match value:
+        case True, True, _:
+            return 1
+        case True, False, _:
+            return 2
+        case False, True, _:
+            return 3
+        case False, False, tree:
+            reveal_type(tree)  # N: Revealed type is "tuple[tuple[..., ...] | None, tuple[..., ...] | None] | None"
+            return 4
+[builtins fixtures/tuple.pyi]
+
 [case testMatchSequenceWildcardRefutability]
 # flags: --strict-equality --warn-unreachable
 def f1(x: int | list[int]):
@@ -3769,14 +4434,37 @@ class B(TypedDict):
     num: int
 
 d: A | B
-match d["tag"]: # E: Match statement has unhandled case for values of type "B" \
-                # N: If match statement is intended to be non-exhaustive, add `case _: pass` \
-                # E: Match statement has unhandled case for values of type "Literal['b']"
+match d["tag"]: # E: Match statement has unhandled case for values of type "Literal['b']" \
+                # N: If match statement is intended to be non-exhaustive, add `case _: pass`
     case "a":
         reveal_type(d)  # N: Revealed type is "TypedDict('__main__.A', {'tag': Literal['a'], 'name': builtins.str})"
         reveal_type(d["name"])  # N: Revealed type is "builtins.str"
 [typing fixtures/typing-typeddict.pyi]
 
+[case testExhaustiveMatchFinalGuard]
+# flags: --enable-error-code exhaustive-match --warn-unreachable
+def f(value: bool, guard: bool) -> None:
+    match value:  # E: Match statement has unhandled case for values of type "Literal[False]" \
+                  # N: If match statement is intended to be non-exhaustive, add `case _: pass`
+        case True:
+            pass
+        case False if guard:
+            pass
+
+[case testExhaustiveMatchTrailingUnreachableCapture]
+# flags: --enable-error-code exhaustive-match --warn-unreachable
+class A: pass
+class B: pass
+
+def f(x: A | None) -> None:
+    match x:
+        case None:
+            pass
+        case A() as a:
+            pass
+        case B():
+            pass  # E: Statement is unreachable
+
 [case testEnumTypeObjectMember]
 # flags: --strict-equality --warn-unreachable
 import enum
diff --git a/test-data/unit/patterncoverage.test b/test-data/unit/patterncoverage.test
new file mode 100644
index 0000000000000..9be44bb1f18f8
--- /dev/null
+++ b/test-data/unit/patterncoverage.test
@@ -0,0 +1,239 @@
+-- Checker regressions use a narrowing limit of 2 and the production coverage budget.
+
+[case testPatternCoverageReturnAndAssignment]
+# flags: --enable-error-code exhaustive-match
+def returning(x: tuple[bool, bool, bool, bool]) -> int:
+    match x:
+        case True, True, _, _: return 1
+        case _, _, True, True: return 1
+        case _, _, False, _: return 0
+        case _, _, _, False: return 0
+
+def assigned(x: tuple[bool, bool, bool, bool]) -> int:
+    match x:
+        case True, True, _, _: result = 1
+        case _, _, True, True: result = 1
+        case _, _, False, _: result = 0
+        case _, _, _, False: result = 0
+    return result
+[builtins fixtures/tuple.pyi]
+
+[case testPatternCoverageBodyErrors]
+# flags: --enable-error-code exhaustive-match
+def fallthrough(x: tuple[bool, bool, bool, bool]) -> int: # E: Missing return statement
+    match x:
+        case True, True, _, _: pass
+        case _, _, True, True: pass
+        case _, _, False, _: pass
+        case _, _, _, False: pass
+
+def wrong_return(x: tuple[bool, bool, bool, bool]) -> int:
+    match x:
+        case True, True, _, _: return "wrong" # E: Incompatible return value type (got "str", expected "int")
+        case _, _, True, True: return 1
+        case _, _, False, _: return 0
+        case _, _, _, False: return 0
+[builtins fixtures/tuple.pyi]
+
+[case testPatternCoverageIncompleteAndGuarded]
+def missing(x: tuple[bool, bool, bool, bool]) -> int: # E: Missing return statement
+    match x:
+        case True, True, _, _: return 1
+        case _, _, True, True: return 1
+        case _, _, False, _: return 0
+
+def guarded(x: tuple[bool, bool, bool, bool], guard: bool) -> int: # E: Missing return statement
+    match x:
+        case True, True, _, _: return 1
+        case _, _, True, True: return 1
+        case _, _, False, _: return 0
+        case _, _, _, False if guard: return 0
+
+# A true guard disables coverage without changing the remainder. This fails only
+# with the lowered narrowing budget, verifying that the suite reaches the fallback.
+def narrowing_only(x: tuple[bool, bool, bool, bool]) -> int: # E: Missing return statement
+    match x:
+        case True, True, _, _: return 1
+        case _, _, True, True: return 1
+        case _, _, False, _: return 0
+        case _, _, _, False if True: return 0
+[builtins fixtures/tuple.pyi]
+
+[case testPatternCoverageNominalClasses]
+# flags: --enable-error-code exhaustive-match
+from typing import Generic, TypeVar
+T = TypeVar('T')
+class A(Generic[T]): pass
+class B(Generic[T]): pass
+class Both(A[int], B[int]): pass
+
+def f(x: tuple[A[int] | B[int], A[int] | B[int], A[int] | B[int], A[int] | B[int]]) -> int:
+    match x:
+        case A(), A(), _, _: return 1
+        case _, _, A(), A(): return 1
+        case _, _, B(), _: return 0
+        case _, _, _, B(): return 0
+[builtins fixtures/tuple.pyi]
+
+[case testPatternCoverageEnums]
+# flags: --enable-error-code exhaustive-match
+from enum import Enum
+class E(Enum):
+    A = 1
+    B = 2
+
+def f(x: tuple[E, E, E, E]) -> int:
+    match x:
+        case E.A, E.A, _, _: return 1
+        case _, _, E.A, E.A: return 1
+        case _, _, E.B, _: return 0
+        case _, _, _, E.B: return 0
+[builtins fixtures/tuple.pyi]
+
+[case testPatternCoverageMissingEnumAndFlags]
+from enum import Enum, Flag, IntFlag
+class E(Enum):
+    A = 1
+    B = 2
+    C = 3
+class F(Flag):
+    A = 1
+    B = 2
+class I(IntFlag):
+    A = 1
+    B = 2
+
+def missing(x: tuple[E, E, E, E]) -> int: # E: Missing return statement
+    match x:
+        case E.A, E.A, _, _: return 1
+        case _, _, E.A, E.A: return 1
+        case _, _, E.B, _: return 0
+        case _, _, _, E.B: return 0
+
+def flags(x: tuple[F, F, F, F]) -> int: # E: Missing return statement
+    match x:
+        case F.A, F.A, _, _: return 1
+        case _, _, F.A, F.A: return 1
+        case _, _, F.B, _: return 0
+        case _, _, _, F.B: return 0
+
+def intflags(x: tuple[I, I, I, I]) -> int: # E: Missing return statement
+    match x:
+        case I.A, I.A, _, _: return 1
+        case _, _, I.A, I.A: return 1
+        case _, _, I.B, _: return 0
+        case _, _, _, I.B: return 0
+[builtins fixtures/tuple.pyi]
+
+[case testPatternCoverageLiterals]
+# flags: --enable-error-code exhaustive-match
+from typing import Literal
+
+def integers(x: tuple[Literal[-1, 1], Literal[-1, 1], Literal[-1, 1], Literal[-1, 1]]) -> int:
+    match x:
+        case -1, -1, _, _: return 1
+        case _, _, -1, -1: return 1
+        case _, _, 1, _: return 0
+        case _, _, _, 1: return 0
+
+def strings(x: tuple[Literal["a", "b"], Literal["a", "b"], Literal[b"a", b"b"], Literal[b"a", b"b"]]) -> int:
+    match x:
+        case "a", "a", _, _: return 1
+        case _, _, b"a", b"a": return 1
+        case _, _, b"b", _: return 0
+        case _, _, _, b"b": return 0
+[builtins fixtures/tuple.pyi]
+
+[case testPatternCoverageOpaqueAndDistinctAtoms]
+from typing import Any, Literal
+
+def dynamic(x: tuple[Any, Any, Any, Any]) -> int: # E: Missing return statement
+    match x:
+        case True, True, _, _: return 1
+        case _, _, True, True: return 1
+        case _, _, False, _: return 0
+        case _, _, _, False: return 0
+
+def integers(x: tuple[Literal[0, 1], Literal[0, 1], Literal[0, 1], Literal[0, 1]]) -> int: # E: Missing return statement
+    match x:
+        case True, True, _, _: return 1
+        case _, _, True, True: return 1
+        case _, _, False, _: return 0
+        case _, _, _, False: return 0
+[builtins fixtures/tuple.pyi]
+
+[case testPatternCoverageNestedAndOr]
+# flags: --enable-error-code exhaustive-match
+def nested(x: tuple[tuple[bool, bool], tuple[bool, bool]]) -> int:
+    match x:
+        case (True, True), _: return 1
+        case _, (True, True): return 1
+        case _, (False, _): return 0
+        case _, (_, False): return 0
+
+def alternatives(x: tuple[bool, bool, bool, bool]) -> int:
+    match x:
+        case True, True, _, _: return 1
+        case _, _, True, True: return 1
+        case (_, _, False, _) | (_, _, _, False): return 0
+
+def captured(x: tuple[bool, bool, bool, bool]) -> int:
+    match x:
+        case True, True, _, _: return 1
+        case _, _, True, True: return 1
+        case (_, _, False as flag, _) | (_, _, _, False as flag):
+            reveal_type(flag) # N: Revealed type is "Literal[False]"
+            return 0
+[builtins fixtures/tuple.pyi]
+
+[case testPatternCoverageNestedMissing]
+def f(x: tuple[tuple[bool, bool], tuple[bool, bool]]) -> int: # E: Missing return statement
+    match x:
+        case (True, True), _: return 1
+        case _, (True, True): return 1
+        case _, (False, _): return 0
+[builtins fixtures/tuple.pyi]
+
+[case testPatternCoverageSingleMemberFlags]
+from enum import Flag, IntFlag
+F = Flag('F', 'A')
+class I(IntFlag):
+    A = 1
+
+# Zero remains possible even when there is only one named flag.
+def flags(x: tuple[F, bool]) -> int: # E: Missing return statement
+    match x:
+        case F.A, _: return 1
+
+def intflags(x: tuple[I, bool]) -> int: # E: Missing return statement
+    match x:
+        case I.A, _: return 1
+
+def identity(x: F) -> None:
+    if x is F.A:
+        reveal_type(x) # N: Revealed type is "Literal[__main__.F.A]"
+    else:
+        reveal_type(x) # N: Revealed type is "__main__.F"
+[builtins fixtures/tuple.pyi]
+
+[case testPatternCoverageFlagLiteralUnion]
+# flags: --enable-error-code exhaustive-match
+from enum import Flag
+from typing import Literal
+class F(Flag):
+    A = 1
+    B = 2
+
+# Explicit literal unions exclude unnamed combinations and can be exhaustive.
+def flags(x: tuple[Literal[F.A, F.B], bool]) -> int:
+    match x:
+        case F.A, _: return 1
+        case F.B, _: return 0
+
+def alternatives(x: F) -> None:
+    match x:
+        case F.A | F.B:
+            reveal_type(x) # N: Revealed type is "Literal[__main__.F.A] | Literal[__main__.F.B]"
+        case _:
+            reveal_type(x) # N: Revealed type is "__main__.F"
+[builtins fixtures/tuple.pyi]