Typing: Exhaustiveness checking util

[Phlogistique]

There is a known idiom for ensuring exhaustiveness of an if chain:
https://github.com/python/mypy/issues/5818

from typing import NoReturn

def assert_never(x: NoReturn) -> NoReturn:
    raise AssertionError(f"Invalid value: {x!r}")

from typing import Union

def type_checking_ok(foo: Union[str, int]) -> None:
    if isinstance(foo, str):
        print("str")
    elif isinstance(foo, int):
        print("int")
    else:
        assert_never(foo)

def type_checking_ko(foo: Union[str, int]) -> None:
    if isinstance(foo, str):
        print("str")
    else:
        assert_never(foo)

It works with mypy but I have not tested it with other type checkers.

Because it is not in the standard library, it has to be implemented or imported in many projects that use typing. At my workplace, we have this util under the name assert_exhaustivity

It would be helpful to document this idiom and have it in the standard library. Would a pull request to this repository be the right way to make it happen? Or does it need a PEP?

[gvanrossum]

Maybe static type checkers could add support for assert False directly in this place? Then you wouldn't need the dummy function. Surely a static checker can deduce that assert False is intended to be unreachable?

[Phlogistique]

One added advantage of the assert_never approach is that the type checker can print the type for the missing branch.

For example with mypy:

test.py:12: error: Argument 1 to "assert_never" has incompatible type "int"; expected "NoReturn"

[bluetech]

I think commandeering assert False would be really nice, however I suspect it wouldn't work well because there is a lot of code out there which uses assert False for unreachable sections which are not statically known to be unreachable.

[freundTech]

With Pattern Matching now being accepted into python there might be renewed interest in this topic.

I would suggest adding assert_exhaustive(x) to typing. The implementation could raise a fitting exception (Just assert False would of course also work, but I would argue that it's helpful to also give more details if it fails at runtime. Not only if it fails during type-checking).

Type-checkers can then just be hardcoded to handle assert_exhaustive(), which removes the problem with NoReturn only being allowed as a return type.

Type-checkers could also make sure that assert_exhaustive() is only used within else blocks (and maybe case _ blocks in the future.

PS: Starting in April I will be writing my bachelors thesis on the topic of "Exhaustiveness check for Structural Pattern Matching in Python 3.10". My work will most likely be based on mypy and I'm planing to contribute the code back to upstream. Having an "official" way to annotate exhaustiveness would be really useful for me.