[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.

Details

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

#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.

[randolf-scholz]

I want to highlight a problem that arises from this issue: generic Protocols that describe that a type supports some interface (e.g. CanX[T] type Protocols like you find them in @jorenham's optype library) seem to be fundamentally broken with all type checkers.

Consider a Protocol like:

class CanOP[T](Protocol):
    # types supporting 'self.op(other) -> Self' when other is of type 'T'.
    def op(self, other: T, /) -> Self: ...

Now, imagine a class that supports self.op(other) -> Self when other is Self, int or X.

But, combinatorially, there are 13 different — but from a typing POV equivalent — ways of annotating op on the class, considering trading unions for overloads and overload order.

Consequently, neither does any single type-checker consistently solve for the same value of T when given one of the 13 possible types, nor do any of the type checkers agree on what T should solve to on a case-by-case basis.

I compiled a test suite that demonstrates the issue on several CanX protocols

from typing import Protocol, Self, overload, reveal_type, assert_type
# mypy: disable-error-code="arg-type"


class X: ...


class CanOP[T](Protocol):
    # Protocol for types that supports 'op(self, other) -> Self' when
    # other is of type 'T'.
    def op(self, other: T, /) -> Self: ...


class CanIntOP[T](Protocol):
    # Protocol for types that support 'op(self, other) -> Self' when
    # other is of type 'int' or 'T'.
    @overload
    def op(self, other: int, /) -> Self: ...
    @overload
    def op(self, other: T, /) -> Self: ...


class CanIntOP_union[T](Protocol):
    # Protocol for types that support 'op(self, other) -> Self' when
    # other is of type 'int | T'.
    def op(self, other: int | T, /) -> Self: ...


class CanSelfOP[T](Protocol):
    # Protocol for types that support 'op(self, other) -> Self' when
    # other is of type 'Self' or 'T'.
    @overload
    def op(self, other: Self, /) -> Self: ...
    @overload
    def op(self, other: T, /) -> Self: ...


class CanSelfOP_union[T](Protocol):
    # Protocol for types that support 'op(self, other) -> Self' when
    # other is of type 'Self | T'.
    def op(self, other: Self | T, /) -> Self: ...


class CanBothOP[T](Protocol):
    # Protocol for types that support 'op(self, other) -> Self' when
    # other is of type 'Self', 'int' or 'T'.
    @overload
    def op(self, other: Self, /) -> Self: ...
    @overload
    def op(self, other: int, /) -> Self: ...
    @overload
    def op(self, other: T, /) -> Self: ...


class CanBothOP_union[T](Protocol):
    # Protocol for types that support 'op(self, other) -> Self' when
    # other is of type 'Self | int | T'.
    def op(self, other: Self | T | int, /) -> Self: ...


def _view1[T](x: CanOP[T], /) -> T: ...  # type: ignore[empty-body]
def _view2[T](x: CanIntOP[T], /) -> T: ...  # type: ignore[empty-body]
def _view3[T](x: CanSelfOP[T], /) -> T: ...  # type: ignore[empty-body]
def _view4[T](x: CanBothOP[T], /) -> T: ...  # type: ignore[empty-body]
def _view2_union[T](x: CanIntOP_union[T], /) -> T: ...  # type: ignore[empty-body]
def _view3_union[T](x: CanSelfOP_union[T], /) -> T: ...  # type: ignore[empty-body]
def _view4_union[T](x: CanBothOP_union[T], /) -> T: ...  # type: ignore[empty-body]


# We give a type that supports op with Self | int
# There are 3 ways to define it:
# 1. A1_1: one overload with union
# 2. A2_1: two overloads, int first
# 3. A2_2: two overloads, Self first
class A1_1:
    def op(self, other: Self | int, /) -> Self:
        return self


class A2_1:
    @overload
    def op(self, other: int, /) -> Self: ...
    @overload
    def op(self, other: Self, /) -> Self: ...
    def op(self, other: Self | int, /) -> Self:
        return self


class A2_2:
    @overload
    def op(self, other: Self, /) -> Self: ...
    @overload
    def op(self, other: int, /) -> Self: ...
    def op(self, other: Self | int, /) -> Self:
        return self


# We give a type that supports op with Self | int | X
# There are 13 equivalent ways to define it:
# 1. B1_1: one overload with (Self | X | int)
# 2. with two overloads, there are 6 ways to arrange them:
#   - B2_1: (X | int, Self)
#   - B2_2: (Self, X | int)
#   - B2_3: (Self | int, X)
#   - B2_4: (X, Self | int)
#   - B2_5: (Self | X, int)
#   - B2_6: (int, Self | X)
# 3. with three overloads, there are 6 ways to arrange them:
#   - B3_1: (Self, X, int)
#   - B3_2: (Self, int, X)
#   - B3_3: (X, Self, int)
#   - B3_4: (X, int, Self)
#   - B3_5: (int, Self, X)
#   - B3_6: (int, X, Self)
class B1_1:
    def op(self, other: Self | X | int, /) -> Self:
        return self


class B2_1:
    @overload
    def op(self, other: X | int, /) -> Self: ...
    @overload
    def op(self, other: Self, /) -> Self: ...
    def op(self, other: X | int | Self, /) -> Self:
        return self


class B2_2:
    @overload
    def op(self, other: Self, /) -> Self: ...
    @overload
    def op(self, other: X | int, /) -> Self: ...
    def op(self, other: int | X | Self, /) -> Self:
        return self


class B2_3:
    @overload
    def op(self, other: Self | int, /) -> Self: ...
    @overload
    def op(self, other: X, /) -> Self: ...
    def op(self, other: Self | X | int, /) -> Self:
        return self


class B2_4:
    @overload
    def op(self, other: X, /) -> Self: ...
    @overload
    def op(self, other: Self | int, /) -> Self: ...
    def op(self, other: X | Self | int, /) -> Self:
        return self


class B2_5:
    @overload
    def op(self, other: Self | X, /) -> Self: ...
    @overload
    def op(self, other: int, /) -> Self: ...
    def op(self, other: Self | X | int, /) -> Self:
        return self


class B2_6:
    @overload
    def op(self, other: int, /) -> Self: ...
    @overload
    def op(self, other: Self | X, /) -> Self: ...
    def op(self, other: int | Self | X, /) -> Self:
        return self


class B3_1:
    @overload
    def op(self, other: Self, /) -> Self: ...
    @overload
    def op(self, other: X, /) -> Self: ...
    @overload
    def op(self, other: int, /) -> Self: ...
    def op(self, other: Self | X | int, /) -> Self:
        return self


class B3_2:
    @overload
    def op(self, other: Self, /) -> Self: ...
    @overload
    def op(self, other: int, /) -> Self: ...
    @overload
    def op(self, other: X, /) -> Self: ...
    def op(self, other: Self | int | X, /) -> Self:
        return self


class B3_3:
    @overload
    def op(self, other: X, /) -> Self: ...
    @overload
    def op(self, other: Self, /) -> Self: ...
    @overload
    def op(self, other: int, /) -> Self: ...
    def op(self, other: X | Self | int, /) -> Self:
        return self


class B3_4:
    @overload
    def op(self, other: X, /) -> Self: ...
    @overload
    def op(self, other: int, /) -> Self: ...
    @overload
    def op(self, other: Self, /) -> Self: ...
    def op(self, other: X | int | Self, /) -> Self:
        return self


class B3_5:
    @overload
    def op(self, other: int, /) -> Self: ...
    @overload
    def op(self, other: Self, /) -> Self: ...
    @overload
    def op(self, other: X, /) -> Self: ...
    def op(self, other: int | Self | X, /) -> Self:
        return self


class B3_6:
    @overload
    def op(self, other: int, /) -> Self: ...
    @overload
    def op(self, other: X, /) -> Self: ...
    @overload
    def op(self, other: Self, /) -> Self: ...
    def op(self, other: int | X | Self, /) -> Self:
        return self


def test_CanOP(
    a1_1: A1_1, a2_1: A2_1, a2_2: A2_2,
    b1_1: B1_1,
    b2_1: B2_1, b2_2: B2_2, b2_3: B2_3, b2_4: B2_4, b2_5: B2_5, b2_6: B2_6,
    b3_1: B3_1, b3_2: B3_2, b3_3: B3_3, b3_4: B3_4, b3_5: B3_5, b3_6: B3_6,
) -> None:  # fmt: skip
    reveal_type(_view1(a1_1))
    reveal_type(_view1(a2_1))
    reveal_type(_view1(a2_2))
    reveal_type(_view1(b1_1))
    reveal_type(_view1(b2_1))
    reveal_type(_view1(b2_2))
    reveal_type(_view1(b2_3))
    reveal_type(_view1(b2_4))
    reveal_type(_view1(b2_5))
    reveal_type(_view1(b2_6))
    reveal_type(_view1(b3_1))
    reveal_type(_view1(b3_2))
    reveal_type(_view1(b3_3))
    reveal_type(_view1(b3_4))
    reveal_type(_view1(b3_5))
    reveal_type(_view1(b3_6))


assert_type(1, str)  # line separator


def test_CanIntOP(
    a1_1: A1_1, a2_1: A2_1, a2_2: A2_2,
    b1_1: B1_1,
    b2_1: B2_1, b2_2: B2_2, b2_3: B2_3, b2_4: B2_4, b2_5: B2_5, b2_6: B2_6,
    b3_1: B3_1, b3_2: B3_2, b3_3: B3_3, b3_4: B3_4, b3_5: B3_5, b3_6: B3_6,
) -> None:  # fmt: skip
    reveal_type(_view2(a1_1))
    reveal_type(_view2(a2_1))
    reveal_type(_view2(a2_2))
    reveal_type(_view2(b1_1))
    reveal_type(_view2(b2_1))
    reveal_type(_view2(b2_2))
    reveal_type(_view2(b2_3))
    reveal_type(_view2(b2_4))
    reveal_type(_view2(b2_5))
    reveal_type(_view2(b2_6))
    reveal_type(_view2(b3_1))
    reveal_type(_view2(b3_2))
    reveal_type(_view2(b3_3))
    reveal_type(_view2(b3_4))
    reveal_type(_view2(b3_5))
    reveal_type(_view2(b3_6))


assert_type(1, str)  # line separator


def test_CanSelfOP(
    a1_1: A1_1, a2_1: A2_1, a2_2: A2_2,
    b1_1: B1_1,
    b2_1: B2_1, b2_2: B2_2, b2_3: B2_3, b2_4: B2_4, b2_5: B2_5, b2_6: B2_6,
    b3_1: B3_1, b3_2: B3_2, b3_3: B3_3, b3_4: B3_4, b3_5: B3_5, b3_6: B3_6,
) -> None:  # fmt: skip
    reveal_type(_view3(a1_1))
    reveal_type(_view3(a2_1))
    reveal_type(_view3(a2_2))
    reveal_type(_view3(b1_1))
    reveal_type(_view3(b2_1))
    reveal_type(_view3(b2_2))
    reveal_type(_view3(b2_3))
    reveal_type(_view3(b2_4))
    reveal_type(_view3(b2_5))
    reveal_type(_view3(b2_6))
    reveal_type(_view3(b3_1))
    reveal_type(_view3(b3_2))
    reveal_type(_view3(b3_3))
    reveal_type(_view3(b3_4))
    reveal_type(_view3(b3_5))
    reveal_type(_view3(b3_6))


assert_type(1, str)  # line separator


def test_CanBothOP(
    a1_1: A1_1, a2_1: A2_1, a2_2: A2_2,
    b1_1: B1_1,
    b2_1: B2_1, b2_2: B2_2, b2_3: B2_3, b2_4: B2_4, b2_5: B2_5, b2_6: B2_6,
    b3_1: B3_1, b3_2: B3_2, b3_3: B3_3, b3_4: B3_4, b3_5: B3_5, b3_6: B3_6,
) -> None:  # fmt: skip
    reveal_type(_view4(a1_1))
    reveal_type(_view4(a2_1))
    reveal_type(_view4(a2_2))
    reveal_type(_view4(b1_1))
    reveal_type(_view4(b2_1))
    reveal_type(_view4(b2_2))
    reveal_type(_view4(b2_3))
    reveal_type(_view4(b2_4))
    reveal_type(_view4(b2_5))
    reveal_type(_view4(b2_6))
    reveal_type(_view4(b3_1))
    reveal_type(_view4(b3_2))
    reveal_type(_view4(b3_3))
    reveal_type(_view4(b3_4))
    reveal_type(_view4(b3_5))
    reveal_type(_view4(b3_6))


assert_type(1, str)  # line separator


def test_CanIntOP_union(
    a1_1: A1_1, a2_1: A2_1, a2_2: A2_2,
    b1_1: B1_1,
    b2_1: B2_1, b2_2: B2_2, b2_3: B2_3, b2_4: B2_4, b2_5: B2_5, b2_6: B2_6,
    b3_1: B3_1, b3_2: B3_2, b3_3: B3_3, b3_4: B3_4, b3_5: B3_5, b3_6: B3_6,
) -> None:  # fmt: skip
    reveal_type(_view2_union(a1_1))
    reveal_type(_view2_union(a2_1))
    reveal_type(_view2_union(a2_2))
    reveal_type(_view2_union(b1_1))
    reveal_type(_view2_union(b2_1))
    reveal_type(_view2_union(b2_2))
    reveal_type(_view2_union(b2_3))
    reveal_type(_view2_union(b2_4))
    reveal_type(_view2_union(b2_5))
    reveal_type(_view2_union(b2_6))
    reveal_type(_view2_union(b3_1))
    reveal_type(_view2_union(b3_2))
    reveal_type(_view2_union(b3_3))
    reveal_type(_view2_union(b3_4))
    reveal_type(_view2_union(b3_5))
    reveal_type(_view2_union(b3_6))


assert_type(1, str)  # line separator


def test_CanSelfOP_union(
    a1_1: A1_1, a2_1: A2_1, a2_2: A2_2,
    b1_1: B1_1,
    b2_1: B2_1, b2_2: B2_2, b2_3: B2_3, b2_4: B2_4, b2_5: B2_5, b2_6: B2_6,
    b3_1: B3_1, b3_2: B3_2, b3_3: B3_3, b3_4: B3_4, b3_5: B3_5, b3_6: B3_6,
) -> None:  # fmt: skip
    reveal_type(_view3_union(a1_1))
    reveal_type(_view3_union(a2_1))
    reveal_type(_view3_union(a2_2))
    reveal_type(_view3_union(b1_1))
    reveal_type(_view3_union(b2_1))
    reveal_type(_view3_union(b2_2))
    reveal_type(_view3_union(b2_3))
    reveal_type(_view3_union(b2_4))
    reveal_type(_view3_union(b2_5))
    reveal_type(_view3_union(b2_6))
    reveal_type(_view3_union(b3_1))
    reveal_type(_view3_union(b3_2))
    reveal_type(_view3_union(b3_3))
    reveal_type(_view3_union(b3_4))
    reveal_type(_view3_union(b3_5))
    reveal_type(_view3_union(b3_6))


assert_type(1, str)  # line separator


def test_CanBothOP_union(
    a1_1: A1_1, a2_1: A2_1, a2_2: A2_2,
    b1_1: B1_1,
    b2_1: B2_1, b2_2: B2_2, b2_3: B2_3, b2_4: B2_4, b2_5: B2_5, b2_6: B2_6,
    b3_1: B3_1, b3_2: B3_2, b3_3: B3_3, b3_4: B3_4, b3_5: B3_5, b3_6: B3_6,
) -> None:  # fmt: skip
    reveal_type(_view4_union(a1_1))
    reveal_type(_view4_union(a2_1))
    reveal_type(_view4_union(a2_2))
    reveal_type(_view4_union(b1_1))
    reveal_type(_view4_union(b2_1))
    reveal_type(_view4_union(b2_2))
    reveal_type(_view4_union(b2_3))
    reveal_type(_view4_union(b2_4))
    reveal_type(_view4_union(b2_5))
    reveal_type(_view4_union(b2_6))
    reveal_type(_view4_union(b3_1))
    reveal_type(_view4_union(b3_2))
    reveal_type(_view4_union(b3_3))
    reveal_type(_view4_union(b3_4))
    reveal_type(_view4_union(b3_5))
    reveal_type(_view4_union(b3_6))

• mypy-playground
• pyright playground
• pyrefly sandbox
• ty playground (ty seems to have the most trouble)

[randolf-scholz]

Here are 3 concrete situations when overloads are guaranteed to be commutative that type checkers could seek to support:

1. Mutually exclusive call signatures:

   class Foo(Protocol):
       @overload
       def f(self, *, a: A) -> B: ...
       @overload
       def f(self, *, x: X) -> Y: ...
   
   class Bar(Protocol):
       @overload
       def f(self, *, x: X) -> Y: ...
       @overload
       def f(self, *, a: A) -> B: ...

   because the call-signatures are mutually exclusive, swapping the order is safe. Subclasses shouldn't be able to violate this, e.g. via **kwargs), without triggering "Overloaded function signature 2 will never be matched" type errors.

2. Mutually exclusive argument types:

   class Foo(Protocol):
       @overload
       def f(self, a: int, /) -> A: ...
       @overload
       def f(self, x: str, /) -> B: ...
   
   class Bar(Protocol):
       @overload
       def f(self, x: str, /) -> B: ...
       @overload
       def f(self, a: int, /) -> A: ...

   because int and str use @disjoint_base, their intersection is empty, so swapping the order is safe.

3. Identical signatures and return types.

   class Foo(Protocol):
       @overload
       def f(self, a: A, /) -> C: ...
       @overload
       def f(self, b: B, /) -> C: ...
   
   class Bar(Protocol):
       @overload
       def f(self, b: B, /) -> C: ...
       @overload
       def f(self, a: A, /) -> C: ...
   
   class Baz(Protocol):
       def f(self, z: A | B, /) -> C: ...

   these are all equivalent types according to the set based criterion.