A type can be consistent subtype of distinct materializations of a generic protocol

[stevapple]

Bug Report

When using TypeIs to narrow a type down to two different fully static materializations of the same generic Protocol, MyPy will infer the result to be Never, thus producing false assertions.

To Reproduce

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) -> Literal[True]:  # Won't complain because `return False` is unreachable
    if is_mock_str(obj) and is_mock_int(obj):
        return True
    return False  # Inferred to be unreachable

def check2(obj: MockProtocol[str]) -> Literal[False]:  # Won't complain because `return True` is unreachable, which is incorrect!
    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

Expected Behavior

check2 should be inferred as Callable[..., bool] because a fully static type can be subtype of both MockProtocol[str] and MockProtocol[int].

Actual Behavior

Literal[False] is recognized as a compatible return type of check2 due to false reachability assumption, causing the type of result2 to be wrong.

Your Environment

• Mypy version used: 1.18.1
• Mypy command-line flags: mypy --strict
• Mypy configuration options from mypy.ini (and other config files): (default)
• Python version used: Python 3.13.8

[sterliakov]

What exactly do you mean when you say "Inferred to be Literal[True]"? Mypy does not infer function return types, they are Any unless explicitly annotated. Are you using some IDE extension? Are you running dmypy suggest (which should never suggest Literal types IIRC)? Where do you get the "inferred" type from? Inferring return types sounds more like annoying pyright behavior to me.

(but the issue is valid for mypy, repro's with --warn-unreachable - we do not consider such protocol intersections)

https://mypy-play.net/?mypy=master&python=3.13&flags=strict%2Cwarn-unreachable&gist=8e3e74989cc0ab6a5c9bb4646167928c

[stevapple]

Are you running dmypy suggest (which should never suggest Literal types IIRC)?

Sorry for the confusion! I rechecked the command line and I was running with mypy repro.py --strict. Updated the issue body.

Where do you get the "inferred" type from? Inferring return types sounds more like annoying pyright behavior to me.

You're correct that mypy don't proactively infer the result type. What it did is to check return type compatibility based on false assumption. eg. if you annotate check1 like this:

def check1(obj: MockClass) -> Literal[False]

Then mypy will raise the following error:

repro.py:37: error: Incompatible return value type (got "Literal[True]", expected "Literal[False]")  [return-value]

And if you annotate with def check1(obj: MockClass) -> Literal[True], it did not warn. I believe this is a misword by me so let me slightly change the wordings.