Details

For the sake of explanation, consider the setup from the linked issue:

x: tuple[Literal[1], int]
match x:
    case (1, 5):
        ...

The root cause of this issue comes from this snippet:

This loop iterates of the current types of the tuple positions (inner_types = [Literal[1], int]) and the proposed new types from the match subpatterns (new_inner_tuples = [Literal[1], Literal[5]]). For each tuple position, it computes the positive-narrowed type if the subpattern matches (narrowed_inner_type) and the negative-narrowed type if the subpattern fails to match (inner_rest_type).

The problem appears to be that the arguments being passed to conditional_types_with_intersection are flipped. Instead of asking the question "what happens when I narrow the old type to the new type?", it's asking the question "what happens when I narrow the new type to the old type?". As a specific example, consider the second iteration where inner_type=int and new_inner_type=Literal[5]. What this check should do is decide that narrowing int to Literal[5] produces a positively-narrowed type of Literal[5] and the negatively-narrowed type of int. Instead, it considers narrowing Literal[5] to int, and decides that the negatively-narrowed type uninhabited/Never (bad).

In the setup above, this causes mypy to deduce that the pattern (1, 5) unconditionally matches tuple[Literal[1], int] (bad), which leads subsequent patterns being considered unreachable (bad).

The fix is to swap the arguments, so that it correctly considers the case of narrowing old-type to new-type. This fixes the linked issue.

However, only applying the fix above leads to a test regression; specifically, this test case will fail:

To my understanding, this test is included erroneously, since this sort of narrowing is not technically implemented (yet). Currently, mypy only applies negative narrowing if all subpatterns unconditionally match:

Matching int | str against int is not an unconditional match (the correct rest type is str). However, due to the issue above, the rest type was computed as uninhabited/Never and this pattern was considered to be an unconditional match; hence negative narrowing was inappropriately (but ultimately accidentally correctly) applied.

This can be behavior can be preserved by relaxing the negative-narrowing criteria from all subpatterns match unconditionally to at most one subpattern may match conditionally, and the rest match unconditionally. We can then safely negatively-narrow the single position that conditionally matches. This behavior is demonstrated in the before/after example above with the match statements using m5.

Open Issues

Negative narrowing of variadic tuples also has a similar issue:

from typing import Literal, Unpack

m: tuple[int | str, Unpack[tuple[str, ...]]]
match m:
    case (int(), *_):
        reveal_type(m)  # N: Revealed type is "tuple[builtins.int, Unpack[builtins.tuple[builtins.str, ...]]]"
    case _:
        reveal_type(m)  # E: Statement is unreachable

However, the fix is more complicated, so I'm leaving it for a separate PR.

CC @freundTech as original author in #10191.

According to mypy_primer, this change doesn't affect type check results on a corpus of open source code. ✅