[spec] overload subtyping rules are too strict.

[randolf-scholz]

The typing spec states that, when A and B are potentially overloaded methods

If a callable B is overloaded with two or more signatures, it is assignable to callable A if at least one of the overloaded signatures in B is assignable to A

If a callable A is overloaded with two or more signatures, callable B is assignable to A if B is assignable to all of the signatures in A

However, this definition seems to be too strict. Consider the following example:

from typing import Protocol, Self, overload

class IntScalarOurs(Protocol):
    def __add__(self, other: int | Self, /) -> Self: ...

class IntScalarTheirs(Protocol):
    @overload
    def __add__(self, other: int, /) -> Self: ...
    @overload
    def __add__(self, other: Self, /) -> Self: ...

These two protocols specify the exact same runtime behavior. Yet, following the rules of the spec, IntScalarOurs is assignable to IntScalarTheirs, but IntScalarTheirs is not assignable to IntScalarOurs.

Case 1: A=IntScalarOurs, B=IntScalarTheirs.

If a callable B is overloaded with two or more signatures, it is assignable to callable A if at least one of the overloaded signatures in B is assignable to A

• Is (self, int) -> Self assignable to (self, int | Self) -> Self? No, because int is not a supertype of int | Self (contravariance)
• Is (self, Self) -> Self assignable to (self, int | Self) -> Self? No, because Self is not a supertype of int | Self (contravariance)

Thus, IntScalarTheirs is not assignable to IntScalarOurs.

Case 2: A=IntScalarTheirs, B=IntScalarOurs.

If a callable A is overloaded with two or more signatures, callable B is assignable to A if B is assignable to all of the signatures in A

• Is (self, int | Self) -> Self assignable to (self, int) -> Self? Yes.
• Is (self, int | Self) -> Self assignable to (self, Self) -> Self? Yes.

Thus, IntScalarOurs is assignable to IntScalarTheirs.

From a pure set-theoretic POV, it seems that subtyping functions should follow a very simply rule based on the domain.

$f <: g$ if and only if $\text{dom}(f) ⊇ \text{dom}(g)$ and $f(x) <: g(x)$ for all $x∈\text{dom}(g)$

What is currently specced appears to be a lemma for a sufficient condition, but not a necessary one. Individual type-checkers can of course use such lemmas if the general case is too difficult to check/implement (and communicate that to their users), but shouldn't the spec be biased towards the theoretically principled point of view, when applicable?

Related Discussions

https://github.com/python/typing/discussions/1782

[JelleZijlstra]

I think the rule you state is correct. I don't know if we can expect type checkers to implement subtyping for overloads fully "correctly"; it seems quite tricky to implement the rule fully. However, the spec should at least allow the full theoretically correct answer, even if type checkers in practice may not implement the full rule.