Python type-checking: Literal[False], overload, and NoReturn

user_1244455 0
Viewed 281

I have the following (typed) Python function:

from typing import overload, Literal, NoReturn

@overload
def check(condition: Literal[False], msg: str) -> NoReturn:
    pass

@overload
def check(condition: Literal[True], msg: str) -> None:
    pass

def check(condition, msg):
    if not condition:
        raise Exception(msg)

Pyright type-checker complains:

Overloaded function implementation is not consistent with signature of overload 1
  Function return type "NoReturn" is incompatible with type "None"
    Type cannot be assigned to type "None"

I'm confused by this-- Pyright apparently can't determine that check will always throw an error if condition is False. How can I massage this to make it work?

pyright python
1 Answers

I posted this to the Pyright issue tracker and was informed that I had to add a Union[NoReturn, None] annotation to the check implementation to resolve the error:

[This] falls out of pyright's rules for return type inference. Pyright will infer a NoReturn type only in the case that all code paths raise an exception. It's quite common for some code paths raise an exception, and it would produce many false positives if pyright were to include NoReturn in the union in that case, so NoReturn is always elided from a union in an inferred return type.

Mypy doesn't have any support for return type inference, so that explains why this doesn't occur for mypy.

The correct way to annotate this is to include an explicit None | NoReturn return type for the implementation.

Unfortunately, this defeats the purpose of the overloads in the first place, which is to allow PyRight to infer from the arguments when NoReturn is the return type. I asked whether it is possible to use overloads to conditionally express NoReturn to the type checker. Apparently it is not:

Unfortunately, pyright cannot make this determination because of its core architecture. The "reachability" of nodes within a code flow graph cannot rely on type evaluations because type evaluations depend on reachability of code flow nodes. To work around this chicken-and-egg problem, the logic that determines reachability does some basic checks to determine if the called function is potentially a "NoReturn" function, but these basic checks are not sophisticated enough to handle overload evaluation. Evaluating overloads requires the full type evaluator, and that depends on reachability.

user_12444550
Related