Exhaustiveness checks (assert_never) don't work with 2-tuple of enums

[jgarvin]

Bug Report

The code below fails to type check, but should succeed because it's exhaustive.

There are some possibly related issues, but I don't know if they are all the same bug, the other tickets tend to depend on Union which this does not: #16650 #15426 #12364

To Reproduce

Playground link: https://mypy-play.net/?mypy=latest&python=3.12&gist=0d21d288fce8aa13d3cc60f4e418960a

#!/usr/bin/env python
# -*- coding: utf-8 -*-

from enum import Enum
from typing import assert_never

class A(Enum):
    A0 = 0
    A1 = 1

class B(Enum):
    B0 = 0
    B1 = 1

def test(a: A, b: B) -> bool:
    match (a, b):
        case (A.A0, B.B0):
            return True
        case (A.A0, B.B1):
            return True
        case (A.A1, B.B0):
            return True
        case (A.A1, B.B1):
            return True
        case _ as never:
            assert_never(never)

    return False

Actual Behavior

typecheck_test.py:26: error: Argument 1 to "assert_never" has incompatible type "tuple[A, B]"; expected "NoReturn"  [arg-type]

Your Environment

• Mypy version used: 1.8.0
• Mypy command-line flags: n/a
• Mypy configuration options from mypy.ini (and other config files): n/a
• Python version used: 3.11 (but also happens with 3.12 in playground link)

[sidddhesh100]

Insted of using asser_never function you can directly raise an AssertionError exception like mentioned in the below code `
from enum import Enum
from typing import Any

class A(Enum):
A0 = 0
A1 = 1

class B(Enum):
B0 = 0
B1 = 1

def test(a: A, b: B) -> bool:
match (a, b):
case (A.A0, B.B0):
return True
case (A.A0, B.B1):
return True
case (A.A1, B.B0):
return True
case (A.A1, B.B1):
return True
case _ as never:
raise AssertionError(f"Expected code to be unreachable, but got: {never}")
return False''`

[jgarvin]

@sidddhesh100 I just did an assert False for now, but that's a workaround not a fix because it moves the error from type checking time to runtime. The point of using assert_never is for mypy to tell you about being non-exhaustive before you really run.

[erictraut]

Exhaustiveness checks are based on type narrowing.

The original type of the subject expression ((a, b)) is tuple[A, B]. That type is equivalent to tuple[Literal[A.A0, A.A1], Literal[B.B0, B.B1]] (via "enum expansion").

Narrowing this type based on the specified patterns requires "tuple expansion", which is not something mypy currently does, at least to my knowledge. The tuple expansion of the above type is tuple[Literal[A.A0], Literal[B.B0]] | tuple[Literal[A.A0], Literal[B.B1]] | tuple[Literal[A.A1], Literal[B.B0]] | tuple[Literal[A.A1, Literal[B.B1]]. This expanded type can now be further narrowed based on the patterns in the match statement.

As you can see, this technique can lead to a union with a very large number of subtypes. Type checkers generally try to avoid such combinatoric explosions, so even if mypy were to add support for this technique, it would likely need to place limits on the expansion.

FWIW, pyright does tuple expansion but only for one dimension of a tuple at a time. That means pyright also doesn't detect exhaustiveness in the code sample above, since it requires expansion of two tuple dimensions.

If you restructure your code to avoid the need for tuple expansion, mypy will then be able to perform exhaustiveness checks.

[jgarvin]

Other langs with pattern matching (Rust, Haskell etc) don't seem to have an issue with this, but I've never tried for anything bigger than ~4-tuples with 2-3 variants. I don't know how other langs avoid the explosion or if they just tolerate it, but this is a totally standard use of tuples and pattern matching and I think anybody coming from those langs (which AFAICT inspired the feature in Python) would expect it to work.

[antonio-antuan]

two cases with different, but wrong results (mypy 1.111):

import typing
from enum import StrEnum


class F(StrEnum):
    A = "a"
    B = "b"


class Z(StrEnum):
    Q = "q"
    X = "x"


def foo(z: Z, f: F) -> None:
    match (z, f):
        case (Z.Q, F.A):
            pass
        case (Z.X, F.A):
            pass
        case (Z.Q, F.B):
            pass
        case (Z.X, F.B):
            pass
        case _:
            typing.assert_never((z, f))  #  error: Argument 1 to "assert_never" has incompatible type "tuple[Z, F]"; expected "NoReturn"  [arg-type]

def bar(z: Z, f: F) -> None:
    comb = (z, f)
    match comb:
        case (Z.Q, F.A):
            pass
        case (Z.X, F.A):
            pass
        case (Z.Q, F.B):
            pass
        case (Z.X, F.B):
            pass
        case _:
            typing.assert_never(comb)  # error: Argument 1 to "assert_never" has incompatible type "tuple[Never, Never]"; expected "NoReturn"  [arg-type]

[antoniogamizbadger]

Any updates on this? It would be a nice to have. Not sure if the type explosion is really a problem. For most of the cases, we do not use type matching so big that this becomes a problem (I think, I have not got any data to back that statement).