possibly-undefined rule should respect exhaustive checking

[sjdemartini]

Feature

If assert_never is used for exhaustive checking (per https://typing.readthedocs.io/en/latest/source/unreachable.html#assert-never-and-exhaustiveness-checking), then the possibly-undefined mypy rule should acknowledge that condition is impossible and so recognize when a variable must be defined.

Pitch

Simple example (python 3.11)

# calculate.py
import enum
from typing import assert_never

class Op(enum.Enum):
    ADD = 1
    SUBTRACT = 2

def calculate(left: int, op: Op, right: int) -> int:
    if op is Op.ADD:
        result = left + right
    elif op is Op.SUBTRACT:
        result = left - right
    else:
        assert_never(op)
    
    return result

With mypy 1.0.1, running mypy --enable-error-code=possibly-undefined calculate.py results in:

calculate.py:18: error: Name "result" may be undefined  [possibly-undefined]
Found 1 error in 1 file (checked 1 source file)

Because we asserted that we can never enter the else case, result should not be considered "possibly undefined" in the return statement above.

---

The possibly-undefined rule does behave properly when raising an exception, and should do the same with assert_never. For instance, the following does not result in a mypy violation for possibly-undefined:

def calculate(left: int, op: Op, right: int) -> int:
    if op is Op.ADD:
        result = left + right
    elif op is Op.SUBTRACT:
        result = left - right
    else:
        raise ValueError("Invalid op")
    return result

[sjdemartini]

Or perhaps simpler: even if the else clause is excluded entirely and we don't use assert_never, but we've already exhaustively checked the various conditions, the possibly-undefined violation shouldn't show up then either. With code like:

def calculate(left: int, op: Op, right: int) -> int:
    if op is Op.ADD:
        result = left + right
    elif op is Op.SUBTRACT:
        result = left - right
    return result

[erictraut]

FWIW, I refer to this functionality as narrowing for implied else in pyright. I found the feature to be relatively difficult to implement.

[ilinum]

Thanks for the report!

The narrowing part of this change is #13926. As for the other part, the possibly-undefined check looks at the type inferred by other parts of mypy for the expression and, if it's a Never (or other Bottom type), will declare that branch unreachable.
The problem is that the type checking is skipped on that part (since it is unreachable) and no type is saved for the later possibly-undefined check. Adding a third operation to your enum makes the example work:

class Op(enum.Enum):
    ADD = 1
    SUBTRACT = 2
    DIV = 3

[KotlinIsland]

here is a minified example:

if True:
    b = 1
print(b)  # error: possibly undefined