Signal unreachability when narrowing with TypeGuard[Never] or TypeIs[Never]

[brianschubert]

Closes #16160

Before

from typing_extensions import Never, TypeGuard

def guard(x: object) -> TypeGuard[Never]:
    ...

a: object

if guard(a):
    reveal_type(a)  # N: Revealed type is "Never"
else:
    reveal_type(a)  # N: Revealed type is "builtins.object"

assert guard(a)
b = 0  # reachable

After

from typing_extensions import Never, TypeGuard

def guard(x: object) -> TypeGuard[Never]:
    ...

a: object

if guard(a):
    reveal_type(a)  # E: Statement is unreachable
else:
    reveal_type(a)  # N: Revealed type is "builtins.object"

assert guard(a)
b = 0  # E: Statement is unreachable

[github-actions]

According to mypy_primer, this change doesn't affect type check results on a corpus of open source code. ✅

[hauntsaninja]

Hm, shouldn't the TypeIs case already work?

(Is there a valid use case for this?)

[brianschubert]

Hm, shouldn't the TypeIs case already work?

D'oh! It does. Or at least mostly works. It does detect unreachability in the basic case, but looking a little closer, it has some funny behavior in the edge case where the prior type involves Never:

def guard(x: object) -> TypeIs[Never]: ...

a: Never

if guard(a):
    reveal_type(a)  # Considered reachable, N: Revealed type is "Never"    
else:
    reveal_type(a)  # Curiously, no note or error!

assert guard(a)
reveal_type(a)      # Considered reachable, N: Revealed type is "Never"    

Likewise, it will also let you narrow Never | object to object. A little weird, but I'm not sure that these cases are something worth caring about on their own.

(Is there a valid use case for this?)

Honestly, I don't know. I can speculate ways it could be used, but I doubt any of them would pass a code review :)

I mainly see this as nice from a consistency perspective. This makes Type{Guard,Is}[Never] behave exactly the same as Literal[False], even in the edge cases with Never.

Maybe this would be useful in a second-order case, where the argument to Type{Guard,Is} comes from something more complicated (think conditionally defined type aliases, or generated code), and where having unusual behavior for Never could be an extra source of confusion?

Please feel free to close if you don't think this is worth pursing :)