ruff/crates/ty_python_semantic/resources/mdtest/directives/assert_never.md
David Peter 2a00eca66b
[ty] Exhaustiveness checking & reachability for match statements (#19508)
## Summary

Implements proper reachability analysis and — in effect — exhaustiveness
checking for `match` statements. This allows us to check the following
code without any errors (leads to *"can implicitly return `None`"* on
`main`):

```py
from enum import Enum, auto

class Color(Enum):
    RED = auto()
    GREEN = auto()
    BLUE = auto()

def hex(color: Color) -> str:
    match color:
        case Color.RED:
            return "#ff0000"
        case Color.GREEN:
            return "#00ff00"
        case Color.BLUE:
            return "#0000ff"
```

Note that code like this already worked fine if there was a
`assert_never(color)` statement in a catch-all case, because we would
then consider that `assert_never` call terminal. But now this also works
without the wildcard case. Adding a member to the enum would still lead
to an error here, if that case would not be handled in `hex`.

What needed to happen to support this is a new way of evaluating match
pattern constraints. Previously, we would simply compare the type of the
subject expression against the patterns. For the last case here, the
subject type would still be `Color` and the value type would be
`Literal[Color.BLUE]`, so we would infer an ambiguous truthiness.

Now, before we compare the subject type against the pattern, we first
generate a union type that corresponds to the set of all values that
would have *definitely been matched* by previous patterns. Then, we
build a "narrowed" subject type by computing `subject_type &
~already_matched_type`, and compare *that* against the pattern type. For
the example here, `already_matched_type = Literal[Color.RED] |
Literal[Color.GREEN]`, and so we have a narrowed subject type of `Color
& ~(Literal[Color.RED] | Literal[Color.GREEN]) = Literal[Color.BLUE]`,
which allows us to infer a reachability of `AlwaysTrue`.

<details>

<summary>A note on negated reachability constraints</summary>

It might seem that we now perform duplicate work, because we also record
*negated* reachability constraints. But that is still important for
cases like the following (and possibly also for more realistic
scenarios):

```py
from typing import Literal

def _(x: int | str):
    match x:
        case None:
            pass # never reachable
        case _:
            y = 1

    y
```

</details>

closes https://github.com/astral-sh/ty/issues/99

## Test Plan

* I verified that this solves all examples from the linked ticket (the
first example needs a PEP 695 type alias, because we don't support
legacy type aliases yet)
* Verified that the ecosystem changes are all because of removed false
positives
* Updated tests
2025-07-23 22:45:45 +02:00

3.2 KiB

assert_never

Basic functionality

assert_never makes sure that the type of the argument is Never.

Correct usage

from typing_extensions import assert_never, Never, Any
from ty_extensions import Unknown

def _(never: Never):
    assert_never(never)  # fine

Diagnostics

If it is not, a type-assertion-failure diagnostic is emitted.

from typing_extensions import assert_never, Never, Any
from ty_extensions import Unknown

def _():
    assert_never(0)  # error: [type-assertion-failure]

def _():
    assert_never("")  # error: [type-assertion-failure]

def _():
    assert_never(None)  # error: [type-assertion-failure]

def _():
    assert_never([])  # error: [type-assertion-failure]

def _():
    assert_never({})  # error: [type-assertion-failure]

def _():
    assert_never(())  # error: [type-assertion-failure]

def _(flag: bool, never: Never):
    assert_never(1 if flag else never)  # error: [type-assertion-failure]

def _(any_: Any):
    assert_never(any_)  # error: [type-assertion-failure]

def _(unknown: Unknown):
    assert_never(unknown)  # error: [type-assertion-failure]

Use case: Type narrowing and exhaustiveness checking

[environment]
python-version = "3.10"

assert_never can be used in combination with type narrowing as a way to make sure that all cases are handled in a series of isinstance checks or other narrowing patterns that are supported.

from typing_extensions import assert_never, Literal

class A: ...
class B: ...
class C: ...

def if_else_isinstance_success(obj: A | B):
    if isinstance(obj, A):
        pass
    elif isinstance(obj, B):
        pass
    elif isinstance(obj, C):
        pass
    else:
        assert_never(obj)

def if_else_isinstance_error(obj: A | B):
    if isinstance(obj, A):
        pass
    # B is missing
    elif isinstance(obj, C):
        pass
    else:
        # error: [type-assertion-failure] "Argument does not have asserted type `Never`"
        assert_never(obj)

def if_else_singletons_success(obj: Literal[1, "a"] | None):
    if obj == 1:
        pass
    elif obj == "a":
        pass
    elif obj is None:
        pass
    else:
        assert_never(obj)

def if_else_singletons_error(obj: Literal[1, "a"] | None):
    if obj == 1:
        pass
    elif obj is "A":  # "A" instead of "a"
        pass
    elif obj is None:
        pass
    else:
        # error: [type-assertion-failure] "Argument does not have asserted type `Never`"
        assert_never(obj)

def match_singletons_success(obj: Literal[1, "a"] | None):
    match obj:
        case 1:
            pass
        case "a":
            pass
        case None:
            pass
        case _ as obj:
            assert_never(obj)

def match_singletons_error(obj: Literal[1, "a"] | None):
    match obj:
        case 1:
            pass
        case "A":  # "A" instead of "a"
            pass
        case None:
            pass
        case _ as obj:
            # TODO: We should emit an error here, but the message should
            # show the type `Literal["a"]` instead of `@Todo(…)`.
            # error: [type-assertion-failure] "Argument does not have asserted type `Never`"
            assert_never(obj)