Type narrowing to distinct materializations of the same generic protocol

[stevapple]

The Python typing documentation describes structural types as "defines a set of values not by their __class__, but by their properties". It specifically mentions callable types and defines "a callable type is a subtype of another callable type based on their signatures, not a subclass relationship". I believe this rules work should for TypedDict and Protocol too, including generic Protocols.

Here's what I found with Pyright (and mypy, too) and TypeIs-based type narrowing:

from typing import Any, Literal, Protocol, TypeIs

# ==== Basic definitions ====

class MockProtocol[T](Protocol):  # T is inferred to be contravariant
    def __call__(self, t: T) -> None:
        ...

class MockClass():
    def __call__(self, t: int | str) -> None:  # Implements MockProtocol[int | str]
        pass

# ==== Basic static type checking ====

def only_accept_mock_int(obj: MockProtocol[int]) -> None:
    pass

def only_accept_mock_str(obj: MockProtocol[str]) -> None:
    pass

only_accept_mock_int(MockClass())  # MockClass is subtype of MockProtocol[int]
only_accept_mock_str(MockClass())  # MockClass is subtype of MockProtocol[str]

# ==== Runtime type checking involving TypeIs ====

def is_mock_int(obj: Any) -> TypeIs[MockProtocol[int]]:
    return isinstance(obj, MockClass)  # Mock implementation

def is_mock_str(obj: Any) -> TypeIs[MockProtocol[str]]:
    return isinstance(obj, MockClass)  # Mock implementation

def check1(obj: MockClass):  # Inferred to be Literal[True]
    if is_mock_str(obj) and is_mock_int(obj):
        return True
    return False  # Inferred to be unreachable

def check2(obj: MockProtocol[str]):  # Inferred to be Literal[False]
    if is_mock_str(obj) and is_mock_int(obj):
        return True  # Inferred to be unreachable
    return False

result1 = check1(MockClass())  # Inferred to be Literal[True]
result2 = check2(MockClass())  # Inferred to be Literal[False], but the value is True!!!
assert result1 == result2  # Inferred to fail consistently, but it should succeed

I thought this should be a bug? Maybe the current reduction rules are a little bit too aggressive. I would wish the static type checking to at least not conflict with the runtime behavior.

[erictraut]

If you haven't already done so, I recommend reading the details in PEP 742, which introduced TypeIs. It specifies the type-theoretic behavior of TypeIs. Given types A (the argument type) and R (the TypeIs return type), the type theoretic narrowed type is A & R in the positive direction and A & ~R in the negative direction. The & symbol represents a set intersection operator, and ~ represents a set negation operator. The Python type system current doesn't define type intersection or negation, so type checkers like mypy and pyright are not able to accurately represent these theoretic types. They do the best they can with the facilities available in the type system.

With that theory in mind, let's look at what's going on in your example above.

In check1, the call to is_mock_str(obj) narrows obj as follows:
MockClass & MockProtocol[str] in the positive direction; this is equivalent to MockClass
MockClass & ~MockProtocol[str] in the negative direction; this is equivalent to Never

In check1, the call to is_mock_int(obj) narrows obj as follows:
MockClass & MockProtocol[int] in the positive direction; this is equivalent to MockClass
MockClass & ~MockProtocol[int] in the negative direction; this is equivalent to Never

Since the type of obj is narrowed to Never in both negative (fall-through) directions, that means the statement after the if block is not reachable.

In check2, the call to is_mock_str(obj) narrows obj as follows:
MockProtocol[str] & MockProtocol[str] in the positive direction; this is equivalent to MockProtocol[str]
MockProtocol[str] & ~MockProtocol[str] in the negative direction; this is equivalent to Never

In check2, the call to is_mock_int(obj) narrows obj as follows:
MockProtocol[str] & MockProtocol[int] in the positive direction; this cannot be simplified and cannot be represented in today's type system
MockProtocol[str] & ~MockProtocol[int] in the negative direction; this cannot be simplified and cannot be represented in today's type system

The spec says "In practice, the theoretic types for strict type guards cannot be expressed precisely in the Python type system. Type checkers should fall back on practical approximations of these types."

So, I think the behavior you're seeing in check1 is correct and aligned with the spec and type theory. The behavior you're seeing in check2 is pyright's attempt to "fall back to practical approximations".

There's a new type checker under development by Astral called "ty". It is the first major Python type checker that fully supports intersection and negation operations. It's still at the "alpha" stage of development, but once it's complete, it will likely be the first type checker that will be able to accurately represent these types internally. I tried your sample in the ty playground, and you can see that it accurately narrows the narrowed types. It doesn't (yet) correctly infer return types for check1 and check2, but I think the ty team plans to add support for return type inference. So if you want the code in your example to work, the best bet is probably to wait for ty to be completed. There is also work underway to formally add intersections (and maybe negations) to the type system.

[stevapple]

Thanks for your detailed explanation @erictraut ! Type narrowing via TypeIs is new to Python and I noticed that it enabled partial support for type intersections (also mentioned in the WIP intersection proposal). Before the official intersection feature has landed, I would like to play around and see how static type checkers can enable new possibilities by "intersection" via return type inference and type narrowing. The code snippet is an outcome of the experiment.

MockProtocol[str] & MockProtocol[int] in the positive direction; this cannot be simplified and cannot be represented in today's type system

I noticed that Pyright actually has partial support for type intersection. If I didn't check for MockProtocol[int] and introduced an identical MockProtocol2 instead:

class MockProtocol2[T](Protocol):  # T is inferred to be contravariant
    def __call__(self, t: T) -> None:
        ...

def is_mock2_int(obj: Any) -> TypeIs[MockProtocol2[int]]:
    return isinstance(obj, MockClass)  # Mock implementation

def check3(obj: MockProtocol[str]):  # Inferred to be bool
    if is_mock_str(obj) and is_mock2_int(obj):
        reveal_type(obj)  # Outputs: <subclass of MockProtocol[str] and MockProtocol2[int]>
        return True
    reveal_type(obj)  # Outputs: MockProtocol[str]
    return False

The result showed that there might be a bug with the reduction rule, which unexpectedly simplified MockProtocol[str] & MockProtocol[int] to Never.

There's a new type checker under development by Astral called "ty". It is the first major Python type checker that fully supports intersection and negation operations.

Thanks for mentioning ty here! I noticed it earlier but didn't look into how it's different from mypy and Pyright. It's nice to see full gradual type support has been implemented. I would definitely give it a try. Since the intersection PEP proposal is getting done, hopefully an official intersection support in the future will make type narrowing more powerful in Python.