Fix reachability in nested match sequence patterns

[cdce8p]

The rest type can't be inferred to be uninhabited if the inner pattern matched a Mapping or Sequence.

Fixes #19981
Fixes #19995

[github-actions]

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

[A5rocks]

I... don't really follow. I don't know anything about the pattern matching checker, so I'm just going off inference/comments elsewhere, but isn't it right to say the rest is uninhabited? If I were to guess the problem is more with the | rather than the (_, {...})?

(sorry, you'll probably just have to explain why this is right when this comment does that. I just don't get it...)

[cdce8p]

The rest type is calculated from the intersection of the subject inner type and the matched inner type. Let's consider an example. Say the subject type is int | str and the matched type is int, the rest type will then be str.

For dict and list this is a bit more complicated as those are match patterns itself. So if the subject is {"a": 1, "b": 2} inferred to dict[str, int] and the case {"a": 2} the pattern would not actually match. However the inferred matched type is still dict[str, int] and the intersection would be Never which isn't correct. A similar issue happens with list. So we have to ignore the intersection rest type for Mapping and Sequence sub-patterns for those.

--
I'm not sure if it might even affect other generic classes as well. So far though I haven't been able to trigger the issue with any other examples so I'd leave it at these two for now.

[A5rocks]

OK thanks that makes more sense. In that case I'm surprised about the check that rest is uninhabited! But more importantly, it seems like we already have machinery already doing this? (or did I misunderstand your explanation):

x: dict[str, int] = {"b": 0}

match x:
    case {"a": 5}:
        pass
    case b:
        reveal_type(b)  # N: Revealed type is "builtins.dict[builtins.str, builtins.int]"

[cdce8p]

But more importantly, it seems like we already have machinery already doing this? [...]

x: dict[str, int] = {"b": 0}

match x:
    case {"a": 5}:
        pass
    case b:
        reveal_type(b)  # N: Revealed type is "builtins.dict[builtins.str, builtins.int]"

The issue only happens for Mapping or Sequence patterns inside a Sequence pattern. Furthermore you'll need a wildcard match. With that mypy currently thinks "oh it's a wildcard so it always matches, thus the rest should be never". That's only true though if the parent sequence pattern itself matches, so we shouldn't infer rest in those cases.

[A5rocks]

I see. Is there a reason why this doesn't narrow the 2nd tuple element to Never?: (in comparison to if x is a dict, which I can see now and is I think what you are talking about)

x: str = "blah"

match (x, 4):
    case ("a", _):
        pass
    case b:
        reveal_type(b)  # N: Revealed type is "tuple[builtins.str, Literal[4]?]"

[cdce8p]

The rest type for x is inferred as str whereas with the dict example it's inferred as Never since technically both the subject and inner match types are identical dict[str, str].

m7: dict[str, str]

match (m7, m7):
    case ({"a": "1"}, _):
        ...
    case (_, {"a": "2"}):
        ...

[A5rocks]

Sorry I forgot to respond. I'm concerned that the logic here is incomplete, does this PR fix this too?: (I'm specifically concerned about the comparison of rest to Never.)

x: dict[str, str] | str = {"blah": "blah"}

match (x, 4):
    case ({"b": "a"}, _):
        pass
    case b:
        reveal_type(b)  # N: Revealed type is "tuple[builtins.dict[builtins.str, builtins.str] | builtins.str, Never]"

Do you think it would be possible to instead have a marker that actually, if we specify a literal dict literal, it might not actually match? (unless it's empty) Otherwise maybe this is the best we can get...

[ilevkivskyi]

Just to add my 5 cents to the discussion: IMO the whole pattern match checking looks quite ad-hoc, we already have extensive logic for if statements (e.g. all the things in find_isinstance_check()), and we may need to re-implement pattern matching so that they share as much of the logic as possible.

[sterliakov]

I'm feeling stupid now, but won't this patch immediately cause reachability false negatives? You check for list or dict unconditionally, so

foo: dict[str, str]
bar: dict[str, str]

match (foo, bar):
    case dict(), _:
        1
    case _, dict():
        2

will not report the case with 2 as unreachable? And it clearly is...

[sterliakov]

I imagine something like (sorry for inline diff, either github UI doesn't work well with multiline changes or I don't know where the magic button is)

diff --git a/mypy/checkpattern.py b/mypy/checkpattern.py
index 9d4c00b6c..4ecc8878f 100644
--- a/mypy/checkpattern.py
+++ b/mypy/checkpattern.py
@@ -306,7 +306,7 @@ class PatternChecker(PatternVisitor[PatternType]):
         if isinstance(current_type, TupleType) and unpack_index is None:
             narrowed_inner_types = []
             inner_rest_types = []
-            for inner_type, new_inner_type in zip(inner_types, new_inner_types):
+            for pat, inner_type, new_inner_type in zip(o.patterns, inner_types, new_inner_types):
                 (narrowed_inner_type, inner_rest_type) = (
                     self.chk.conditional_types_with_intersection(
                         inner_type, [get_type_range(new_inner_type)], o, default=inner_type
@@ -318,8 +318,14 @@ class PatternChecker(PatternVisitor[PatternType]):
                     is_uninhabited(inner_rest_type)
                     and isinstance(narrowed_ptype, Instance)
                     and (
-                        narrowed_ptype.type.fullname == "builtins.dict"
-                        or narrowed_ptype.type.fullname == "builtins.list"
+                        (
+                            narrowed_ptype.type.fullname == "builtins.dict"
+                            and isinstance(pat, MappingPattern)
+                        )
+                        or (
+                            narrowed_ptype.type.fullname == "builtins.list"
+                            and isinstance(pat, SequencePattern)
+                        )
                     )
                 ):
                     # Can't narrow rest type to uninhabited
diff --git a/test-data/unit/check-python310.test b/test-data/unit/check-python310.test
index b08560103..d2ce60e5d 100644
--- a/test-data/unit/check-python310.test
+++ b/test-data/unit/check-python310.test
@@ -1586,6 +1586,14 @@ match (m7, m7):
     case (_, {"a": "2"}):
         reveal_type(m7)  # N: Revealed type is "builtins.dict[builtins.str, builtins.str]"
 
+match (m7, m7):
+    case (dict(), _):
+        reveal_type(m7)  # N: Revealed type is "builtins.dict[builtins.str, builtins.str]"
+    case (_, dict()):
+        reveal_type(m7)  # E: Statement is unreachable
+    case (_, _):
+        reveal_type(m7)  # E: Statement is unreachable
+
 m8: list[int]
 
 match (m8, m8):
@@ -1593,6 +1601,12 @@ match (m8, m8):
         reveal_type(m8)  # N: Revealed type is "builtins.list[builtins.int]"
     case (_, [2]):
         reveal_type(m8)  # N: Revealed type is "builtins.list[builtins.int]"
+
+match (m8, m8):
+    case (list(), _):
+        reveal_type(m8)  # N: Revealed type is "builtins.list[builtins.int]"
+    case (_, [2]):
+        reveal_type(m8)  # E: Statement is unreachable
 [builtins fixtures/dict.pyi]
 
 [case testMatchEnumSingleChoice]

could fix the introduced false negatives. Could you also add a test with nested mapping/sequence patterns and their dict()/list() counterparts? This pattern checker part is recursive, but TBH I'm personally unable to trace through all branches and make sure that another unexpected Never does not slip through when a mapping pattern is nested somewhere.