[spec] overload subtyping rules are too strict.

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.

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

Beginne mit den Regeln zur Subtypisierung von Overloads im Callable-Abschnitt der typing-Spezifikation und sieh dir die zugehörige Diskussion unter typing/discussions/1782 an. Vergleiche die dort angegebenen Regeln mit dem Beispiel IntScalarOurs und IntScalarTheirs und bestimme anschließend, ob die Spezifikation eine prinzipielle Überarbeitung oder eine präzisierte Regel für eine hinreichende Bedingung benötigt.