Better specification for when the presence of typing.Never should be considered a type system error

Typing
43

@carljm here’s an example where both mypy and pyright break the gradual guarantee, but would error consistently if they followed what was here.

I’m using TypeIs to get away from both of the typecheckers special casing isinstance in a way incompatible with the current materialization rules for gradual types:

Code sample in pyright playground

from typing import Any, TypeIs

def is_str(s: Any, /) -> TypeIs[str]:
    return isinstance(s, str)


def breaks_guarantee(s: str, /) -> str:
    if not is_str(s):
        msg = f"Expected a str, got an instance of {type(s):!r}"  # no error
        return TypeError(msg)  # no error
    else:
        return s

def breaking_guarantee_now(s: Any, /) -> str:
    if not is_str(s):
        msg = f"Expected a str, got an instance of {type(s):!r}"  # no error
        return TypeError(msg)  # error
    else:
        return s

mypy playground

What’s proposed here is also consistent with the proposed handling of Never in Intersections and how we are able to distinguish attribute presence from attribute type.

1 Like