Hello,

currently when people want to annotate that a if-elif check should be exhaustive and have a type-checker like mypy verify the exhaustiveness they have to resort to a clever hack that looks like this (This works in mypy. I haven't verified any other type-checkers):

```
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)
```

This works by abusing the fact that mypy doesn't typecheck unreachable code and assert_never can't be called by a valid function call (*except for corner cases I will discuss later).
Mypy also won't report it as unreachable if it is unreachable, as it returns `NoReturn`. If it can be reached mypy will complain about incompatible parameter types.

This has a few problems:
* It can be broken by `Any`. For example if `foo` is of type `Union[int, Any]` and you only check for `int` mypy won't show an error
* According to PEP 484 `NoReturn` is only valid as a return type and should be considered an error if it appears in any other positions.
* Some type-checkers might report the error, even if it is unreachable

This is used in the wild for example by pytest.

Due to python 3.10 introducing the match statement there will probably also be renewed interest in checking exhaustiveness. Therefor I would really like to see an official
way to annotate this. There have already been discussions.
There have already been multiple discussions of this topic on both the mypy github and the typing github:
https://github.com/python/typing/issues/735
https://github.com/python/mypy/issues/5818
(https://github.com/python/mypy/issues/9748)

Discussed solutions/improvements include:
* Changing how `Any` and `NoReturn` interact https://github.com/python/mypy/issues/3194
* Changing PEP 484 to lift restrictions on `NoReturn`
* Introducing `typing.Never` as an alias for `NoReturn` and not holding it to the same restrictions
* Using a self-defined class `Impossible` as parameter type for `assert_never` and just not creating instances of it (Also has the Any problem)
* Reporting reachable `assert False` as error (Might lead to a lot of false positives, where a `assert False` is unreachable but it can't be statically determined)

My suggestion would be adding `assert_exhaustive(x: Any)` 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()`.
They 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.

--
Adrian Freund