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