Consider the following code snippet:
class Base:
def foo(self, x: "Base") -> None:
pass
class Derived(Base):
def foo(self, x: "Derived") -> None:
x.bar()
def bar(self) -> None:
pass
def test(a: Base, b: Base) -> None:
a.foo(b)
test(Derived(), Base())
It’s easy to see that this program is not type-safe: the foo() method on the Base class is declared to be able to consume any subclasses of Base as argument, but the overriding foo() method on the Derived class can only consume one specific subclass of Base (namely Derived). This breaks Liskov substitution principle, and if we run the program it’ll result in a runtime crash because in the run, Derived.foo() would unexpectedly get a Base object as argument via dynamic dispatching, while it only expected a Derived object. Type checkers today are in universal agreement that this kind of code is problematic and will reject it typically via some kind of “incompatible override” check (mypy, pyright, pyre1).
But what happens if I change 2 type annotations in this example, and keep everything else (including the program logic) the same as follows?
from typing import Self
class Base:
def foo(self, x: Self) -> None:
pass
class Derived(Base):
def foo(self, x: Self) -> None:
x.bar()
def bar(self) -> None:
pass
def test(a: Base, b: Base) -> None:
a.foo(b)
test(Derived(), Base())
This change should not affect whether the program is type-safe or not – it’s exactly the same code that breaks substitution principle before, and exactly the same crash we’ll run into at runtime as before. So I would expect that this version of the program will be rejected by type checkers as well. However that’s not the case: mypy, pyright and pyre1 (the sandbox version) would accept this program. The only type checker I know of that is willing to reject the program is the internally deployed version (more up-to-date than sandbox version) of Pyre1, albeit with a terrible error message:
8,4: Inconsistent override [14]: `Derived.foo` overrides method defined in `Base` inconsistently. Parameter of type `Variable[_Self_Derived__ (bound to Derived)]` is not a supertype of the overridden parameter `Variable[_Self_Base__ (bound to Base)]`.
If we look at the typing spec, both PEP 673 and the typing spec site dictates that the Self type should be semantically equivalent to a typevar with the declaring class as its bound. One consequence of this is that type checkers are supposed to make the same accept/reject decision on both the previous example that uses Self annotation, and the following example that uses bounded typevar:
class Base:
def foo[T: Base](self: T, x: T) -> None:
pass
class Derived(Base):
def foo[T: Derived](self: T, x: T) -> None:
x.bar()
def bar(self) -> None:
pass
def test(a: Base, b: Base) -> None:
a.foo(b)
test(Derived(), Base())
Interestingly, mypy still accepts this version of the program, whereas pyright starts to reject it. Pyre1 (the internal version) would reject the program, with similar-looking error message as mentioned above.
Note that from a soundness perspective, none of the examples above is type-safe since they all cause runtime crashes. So it’s interesting to see that 3 different type checkers made 3 different choices on what to do here: mypy chose to be unsound but spec-conforming; pyright choose to be unsound and non-spec-conforming, and pyre1 (internal) is both sound and spec-conforming (but emits incomprehensible error messages). Normally such divergence may not be a big issue if uses of the Self type in similar manners are uncommon in practice. But a quick search in typeshed brings back more hits than I expected, which may indicate that the problem might not be that rare. So I figured it might be useful to at least raise the issue here and get some opinions (hopefully a consensus) about what to do with it.
If we take a step from the examples back and take a more general perspective, my understanding is that if the PEP 673 semantics (i.e. self type = typevar bounded by the containing class) is to be respected, then the use of Self annotation can only be covariant if we still want to maintain the substitution principle. In other words, if the Self annotation appears in a contravariant position (e.g. as type annotation of an argument), the theoretically sound way to handle it should be to either emit a type error, or treat the Self as exactly the same as the containing class (i.e. make it invariant – this is more lenient than erroring immediately on contravariant Self usage, since it could still accepts the safe case where even though contravariant Self appears, the method never gets overridden).
Another approach we could take here is to modify the spec to give up PEP 673 semantics, and just declare that Self always behaves covariantly even if it’s put at contravariant positions (i.e. aligning the spec with what mypy’s implementation today). Soundness will be unavoidably broken if we take this option so I hope we would take extra care of documenting this decision well. But it might be the path of least resistance.
