Deep interactions between Protocols and overloads

[RBerga06]

Let's say I have a generic Protocol and a class that implements that protocol multiple times (for different arguments) via overloads:

class Proto[T](Protocol):
    @type_check_only
    def proto(self, _: T, /) -> None: ...

type One = Literal[1]
type Two = Literal[2]

@final
class Impl[N: int]:
    # ensure `N` is invariant
    def __init__(self, n: N, /) -> None: ...
    @type_check_only
    def get_n(self, /) -> N: ...

    # implement Proto[N] for Impl[N] and Proto[M] for Impl[One] (for all integers N, M)
    @overload
    def proto(self, _: "Impl[N]", /) -> None: ...
    @overload
    def proto[M: int](self: "Impl[One]", _: "Impl[M]", /) -> None: ...

I can easily verify that Impl really does implement Proto the way I intended:

class check1[T]:
    def __init__(self, x: Proto[T], /) -> None: ...

# Here it all works as expected
impl1 = Impl[One](1)
impl2 = Impl[Two](2)
impl_ = Impl[int](3)
_ = check1[Impl[One]](impl1)  # ok (first overload applies)
_ = check1[Impl[Two]](impl1)  # ok (second overload applies)
_ = check1[Impl[One]](impl2)  # error (second overload doesn't apply because One != Two)
_ = check1[Impl[Two]](impl2)  # ok (first overload applies)
_ = check1[Impl[One]](impl_)  # error (second overload doesn't apply because N is invariant)
_ = check1[Impl[Two]](impl_)  # error (second overload doesn't apply because N is invariant)
_ = check1[Impl[int]](impl_)  # ok (first overload applies)

Now, let's say we wanted to write a function func that takes T and Proto[T], in any order, and just applies .proto(...) on them. Here, I'll model it as a generic class:

class func[T]:
    @overload
    def __init__(self, x: T, y: Proto[T], /) -> None: ...
    @overload
    def __init__(self, x: Proto[T], y: T, /) -> None: ...
	# implementation not important

If I don't specify T manually, sometimes Pyright complains:

_ = func[Impl[One]](impl2, impl1)  # error (correct)
_ = func[Impl[One]](impl1, impl2)  # error (correct)
_ = func[Impl[int]](impl_, impl1)  # ok
_ = func[Impl[int]](impl1, impl_)  # ok
_ = func[Impl[Two]](impl2, impl1)  # ok
_ = func[Impl[Two]](impl1, impl2)  # ok
reveal_type(func(impl2, impl1))  # ok, type is `func[Impl[Two]]`
reveal_type(func(impl1, impl2))  # error, but why?

Code sample in pyright playground

The error message says I cannot assign impl2: Impl[Two] to y: T, because Impl[Two] is not assignable to Impl[One]: it looks like Pyright has chosen the first overload in Impl's implementation of Proto and has resolved T to be One because impl1: Impl[One] indeed implements Proto[One]. However, since this leads to an error, why has Pyright not tried the other implementation?

Side note

If I don't manually enforce the type parameter of check1, Pyright infers Impl[One]:

reveal_type(check1(impl1))  # type is `check1[Impl[One]]`  # first overload applies

Is this:

• a hard limitation of Pyright (and type checker implementations in general),
• a hole (unspecified behaviour) in the typing spec,
• or the expected behaviour (and I just don't understand what's going on)?

If it is indeed a hard limitation, can I type func in a different way (without changing Impl and Proto)?

Thank you for your time and dedication to improve the soundness and expressiveness of the Python type system (and to answer all these questions from the community).

Best regards,
Riccardo Bergamaschi.

[antoninche]

Hi! What you’re running into here isn’t a special “typing bug” in your code, it’s a consequence of how overload resolution and structural subtyping interact in current Python type checkers.

The key points are:

• Static type checkers like Pyright and mypy match overloads based on the call signature alone. They don’t re-solve type variables based on deeper protocol conformance after the fact — once a candidate overload is chosen, they stick with it. This is why in your second call example Pyright picks the first overload branch and doesn’t try the other: there isn’t a mechanism in the spec that says “if this overload leads to a constraint contradiction, try another” — overload resolution isn’t backtracking.

• Protocol conformance is structural, but it doesn’t drive overload resolution. That is, knowing that Impl[Two] conforms to Proto[Two] and that Impl[One] also implements the protocol isn’t enough for the type checker to reorder overload matching at call time. Once a type variable T is fixed by an overload match, the checker doesn’t go look for alternate matches when later constraints fail.

• Different type checkers have subtle differences here, but none currently implement a full “overload resolution with backtracking” mechanism; most simply test the overloads in declaration order and stop at the first plausible match.

So in short:

• It’s not a missing feature you’re supposed to use — it’s an inherent limitation of current overload resolution strategies in Python type checkers.
• There isn’t an alternative typing of func that magically makes Pyright choose the “better” overload, aside from writing more explicit overloads that guide the checker.
• This is a well-known complexity with overloads + protocols — type checkers err on the side of determinism and performance rather than complete search.
  Hope that clarifies what’s happening under the hood!

[RBerga06]

Thank you!