Self type from 673 and soundness holes

[Tomaz-Vieira]

Is there a standard way of handling soundness holes emerging from Self type? I would open some bug reports, but I'm not sure if there's even a stance on whether those should be checked by the type checker at all. An example that is even listed as valid usage in PEP 673 itself is this:

# pyright: strict

from typing import List
from typing_extensions import Self, reveal_type


class Animal:
    def to_list(self) -> List[Self]:
        return [Cat(), Dog()]

class Dog(Animal):
    pass

class Cat(Animal):
    pass

dogs: List[Dog] = Dog().to_list() # but dogs is [Cat(), Dog()]

Because Self changes its meaning down the inheritance tree, every time Self is used to compose an invariant type in a return value we either get an uninheritable class (should the type checker enforce @final then?) or a method that is impossible to define. I'm sure there are other ways to break the type system by using Self.

Are these bugs that should be reported? I for one would like to be warned in these situations, but type hinting in python can be more lenient than other typing systems, and Self is recent enough that there might not be any standards on how to handle its corner cases yet.

[erictraut]

I recommend raising these questions in the python/typing forums. The authors of PEP 673 (who are part of the pyre team) will likely be monitoring those discussions, and they can weigh in. I suspect that the answer will be that this these type holes are acceptable and pragmatic compromises.

Then again, you might be able to make a persuasive argument. The same hole would not exist with the more traditional method of using a TypeVar.

S = TypeVar("S")

class Animal:
    def to_list(self: S) -> List[S]:
        return [Cat(), Dog()] # Type error: TypeVar _T@list is invariant

The example you give above bends over backward to exploit the hole. After all, using subclasses within a class implementation is something you should not do in well-written object-oriented code. If you want to argue that these holes should be plugged, you might want to find a better example where the code is not so contorted. There are always ways that a poorly-written piece of code can find ways to defeat the type system. The tools are not meant to be bullet-proof; they're meant to provide a means for well-intentioned programmers to make their code more robust and maintainable.