Details

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

x:tuple[Literal[1],int]matchx: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 toconditional_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 whereinner_type=int andnew_inner_type=Literal[5]. What this check should do is decide that narrowingint toLiteral[5] produces a positively-narrowed type ofLiteral[5] and the negatively-narrowed type ofint. Instead, it considers narrowingLiteral[5] toint, 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 matchestuple[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:

Matchingint | str againstint is not an unconditional match (the correct rest type isstr). 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 fromall subpatterns match unconditionally toat 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 thematch statements usingm5.

Open Issues

Negative narrowing of variadic tuples also has a similar issue:

fromtypingimportLiteral,Unpackm:tuple[int|str,Unpack[tuple[str, ...]]]matchm: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 tomypy_primer, this change doesn't affect type check results on a corpus of open source code. ✅