Pyright has an internal type called `Never` that is effectively an alias for `NoReturn` (and is semantically equivalent to an empty union). Pyright supports `NoReturn` for input parameter annotations to allow for functions like `assert_never`. I can't speak for pyre or pytest, but I'm guessing that they also ignore the restriction in PEP 484 to allow for this mechanism. That said, I'd be in favor of introducing a `typing.Never` alias as you've suggested. I think it would add clarity with little or no additional complexity. Your note is timely. I just finished implementing a new feature in the latest version of Pyright that I refer to as "implied else narrowing". It's used in cases where an "if" or "elif" clause is missing a corresponding "else" clause and the conditional expression in the "if" or "elif" can be narrowed to a "Never" type in the negative (else) case. It allows for automatic exhaustiveness checking without the introduction of an explicit `asser_never` call. See here for [documentation and samples](https://github.com/microsoft/pyright/blob/master/docs/type-concepts.md#narro...). This feature was relatively straightforward to implement once I worked out the rules, but I don't know enough about mypy's architecture to say whether it will be similarly straightforward to implement there. The rules can get a little complicated if you want to support composite conditional expressions — those that include `and`, `or`, and `not` modifiers. For reference, here's [the commit that introduces the feature in Pyright](https://github.com/microsoft/pyright/commit/c53cadf07039bb3911ff7dc9c42cae62...). My initial implementation had a measurable impact on pyright's analysis performance (about a 15% perf regression in typical code, and significantly more in the worst case) because of the additional code flow nodes it introduced to the graph. I've made some subsequent changes (heuristics) to claw back most of that perf loss. -- Eric Traut Contributor to Pyright & Pylance Microsoft Corp.