Exhaustiveness checking fails on non-trivial use of pattern matching

[ajasmin]

Code using assert_never() to ensure exhaustive use of match-case yields a type error on many non-trivial cases.

mypy can only verify exhaustiveness when matching directly against a Union type or Enum value.

Though, proving the exhaustiveness of non-trivial matches may be beyond mypy domain. Here are a couple of examples for the sake of argument:

Matching on both [] and [x, *xs] on Sequence will not narrow the type

from collections.abc import Sequence
from typing import assert_never

def my_sum(s: Sequence[float]) -> float:
    match s:
        case []:
            return 0
        case [num, *rest]:
            return num + my_sum(rest)
        case _ as u:
            # error: Argument 1 to "assert_never" has incompatible type "Sequence[float]"; expected "NoReturn"
            return assert_never(u)

Matching against all Enum values that a single-member wrapper class may contain

import dataclasses, enum
from typing import assert_never, final

class E(enum.Enum):
    A = enum.auto()
    B = enum.auto()

@final
@dataclasses.dataclass(frozen=True)
class Foo:
    x: E

def match_enum_attribute(f: Foo) -> None:
    match f:
        case Foo(E.A):
            pass
        case Foo(E.B):
            pass
        case _ as r:
            # error: Argument 1 to "assert_never" has incompatible type "Foo"; expected "NoReturn"  [arg-type]
            assert_never(r)

[erictraut]

I think mypy is working as intended here. Exhaustiveness checking is based on type narrowing.

In your top example, the initial type of s is Sequence[float]. The type cannot be further narrowed by the first case statement because the length of the sequence cannot be determined statically. For the same reason, the type cannot be further narrowed by the second case statement. If you were to add a third case statement that uses the pattern [*x], mypy should be able to narrow the type to Never. (It doesn't do this currently, so that looks to me like a missing feature. Pyright is able to narrow to Never in this case.)

In your second example, the initial type of f is Foo. Neither of the case statements can further narrow the type. It remains Foo. There is no type in the Python type system that represents "an instance of Foo where the x attribute does not contain E.A". If you want mypy to check for exhaustiveness in this case, you could modify your code as follows:

def match_enum_attribute(f: Foo) -> None:
    match f:
        case Foo():
            match f.x:
                case E.A:
                    pass
                case E.B:
                    pass
                case _ as r:
                    assert_never(r)
        case _ as r:
            assert_never(r)

[ajasmin]

When rewriting the second example to match on tuple[E], mypy correctly narrows the type of the Enum E but still fails on assert_never(r):

import enum
from typing_extensions import assert_never

class E(enum.Enum):
    A = enum.auto()
    B = enum.auto()

def match_enum_attribute(f: tuple[E]) -> None:
    match f:
        case (E.A,):
            pass
        case (E.B,):
            pass
        case _ as r:
            assert_never(r)

error: Argument 1 to "assert_never" has incompatible type "Tuple[<nothing>]"; expected "NoReturn"  [arg-type]

[AlexWaygood]

When rewriting the second example to match on tuple[E], mypy correctly narrows the type of the Enum E but still fails on assert_never(r):

There's a bug in your code here. You want to call assert_never on the first element of f in the fallback case, rather than f itself (since f is known to be a tuple). If you correct your code to the following, mypy is fine with it:

import enum
from typing_extensions import assert_never

class E(enum.Enum):
    A = enum.auto()
    B = enum.auto()

def match_enum_attribute(f: tuple[E]) -> None:
    match f:
        case (E.A,):
            pass
        case (E.B,):
            pass
        case (_,) as r:
            assert_never(r)

https://mypy-play.net/?mypy=latest&python=3.11&gist=502599bec6b2cd6a24be96939a45c34b

[ajasmin]

When matching on tuples of two enums, it's also possible for enum values to be narrowed too aggressively.

import enum
from typing_extensions import assert_never

class E(enum.Enum):
    A = enum.auto()
    B = enum.auto()

def do_match(t: tuple[E,E]) -> None:
    match t:
        case (E.A,E.A):
            pass
        case (E.B,_):
            pass
        case (x,y):
            # no type error there
            assert_never(x)
            assert_never(y)

# Fails at runtime
do_match((E.A,E.B))

From my understanding, we'd need a broad match like (E.A, _) or (E.A, *rest) to narrow out E.A from the first element. Though, mypy narrows on (E.A, E.A) and doesn't reach assert_never(x).

With (E.A, *rest), we can check exhaustiveness on rest by nesting match statements and calling assert_never() in each branch though this is more verbose.

[juliancoffee]

I stumbled upon this issue with a similar code

def f(xs: Optional[tuple[str, bool]]) -> None:
    match xs:
        case None:
            print("None")
        case [msg, flag]:
            print(f"{msg} and {flag}")
        case rest:
            # fails with `rest` is of type tuple[Never, Never]
            assert_never(rest)

Technically you could workaround with something like this (or import assert_type from typing extensions)

from typing import TypeVar, Generic, Optional, Never, assert_never

T = TypeVar("T")
class assert_type(Generic[T]):
    def __init__(self, x: T) -> None:
        pass

def f(xs: Optional[tuple[str, bool]]) -> None:
    match xs:
        case None:
            print("None")
        case [msg, flag]:
            print(f"{msg} and {flag}")
        case other:
            # ideally wouldn't be needed
            assert_type[tuple[Never, Never]](other)

But this third step looks quite redundant, especially considering that in most languages with pattern matching even case rest is redundant, but that's another thing.
Why can't we "roll" tuple[Never*] into Never?

from collections.abc import Sequence
from typing import Never, assert_never, overload

@overload
def assert_never_seq(rest: Never) -> Never: pass

@overload
def assert_never_seq(rest: Sequence[Never]) -> Sequence[Never]: pass

def assert_never_seq(rest):
    raise RuntimeError(rest)

It doesn't help with the issue above though, but that looks more like a bug in mypy.