Open jgarvin opened 10 months ago
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''`
@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.
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.
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.
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]
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 #12364To Reproduce
Playground link: https://mypy-play.net/?mypy=latest&python=3.12&gist=0d21d288fce8aa13d3cc60f4e418960a
Actual Behavior
Your Environment
mypy.ini
(and other config files): n/a