Is it type-safe for a subclass to annotate an attribute as Never?

[randolf-scholz]

Consider this example ①:

from typing import Never

class A:
    foo: int
class B(A):
    foo: Never

Is B a proper subtype of A? Both mypy and pyright do not flag this code as wrong, but there is a heated debate in the intersection-pep discussion whether this is allowed. I would appreciate it if people could comment on what they think whether in the examples ①, ②, ③, ④ B is a proper subtype of A. (all examples validate in mypy and pyright).

Example ②

from typing import Never

class A:
    def foo(self) -> int: return 0
class B(A):
    def foo(self) -> Never: raise NotImplementedError

Example ③

from typing import Never

class A:
    @property
    def foo(self) -> int: return 0
class B(A):
    @property
    def foo(self) -> Never: raise NotImplementedError

Example ④

from typing import Never

class A:
    foo: int

    def __getattr__(self, name):
        if name == "foo":
            return 42
        raise AttributeError


class B(A):
    foo: Never

    def __getattr__(self, name):
        if name == "foo":
            raise NotImplementedError("B.foo is not implemented!")
        raise AttributeError

[randolf-scholz]

What all parties agree on is:

1. No instances of Never can exist at runtime.
2. It is therefore impossible to populate B.foo

Disagreement is about whether if A defines foo, B can choose to not populate foo, in the sense of leaving it with type Never. Here are the main arguments:

Pro: B is a subtype of A

This follows from strictly following the rule: B is a (structural) subtype of A if B.x is a subtype of A.x for all x defined for A. Since Never is the bottom type, B.foo is a subtype of A.foo and therefore B is a subtype of A.

Contra: B is not a subtype of A

Specifying a field is a promise that the field exists. However, as mentioned above, B.foo cannot be populated. A subclass must populate all fields that its parent class populates.

---

So in some regards, the question is whether a field existing, and a field being populated are the same thing or not.

[hauntsaninja]

Speaking to the general case:

Covariant overriding of mutable attributes is something that is definitely unsound.

However, most type checkers allow it in cases involving nominal subtyping, see e.g. python/mypy#3208. This is a decision made for pragmatic reasons.

With Protocols and substructural typing, we got an opportunity to be stricter, and I believe most type checkers disallow covariant overriding of mutable attributes in substructural types.

from typing import Never, Protocol

class A(Protocol):
    foo: int
class B:
    foo: Never

def takes_A(a: A): ...
takes_A(B()) # error

I haven't followed the intersection discussion closely since it was too noisy. My advice would be to first focus on intersections of structural types. This would cover a lot of the usage, and you choose soundness on things like covariant overrides of mutable attributes.

[randolf-scholz]

Yes, for mutable attributes it is definitely different. Unfortunately, the current typing system makes it difficult to be precise in this regard. Sometimes I wish there was typing.Attribute and typing.MutableAttribute for this very reason.

[randolf-scholz]

My advice would be to first focus on intersections of structural types.

Well, the discussion kind of got hung up on the point about what should happen when A.foo and B.foo are incompatible. Is then only (A&B).foo equal to Never or is A&B itself equal to Never?

[hauntsaninja]

(without having thought too much about it)

If an attribute is immutable / Final / method / property, I'd say (A&B).foo should be of type A.foo & B.foo.

So when A.foo and B.foo are incompatible, this is Never. In such a case, I'd say type checkers should issue a warning where the intersection is defined, but nevertheless give you a type that mostly matches what you ask for. This matches what type checkers do for Liskov incompatibilities in subclasses, which is conceptually quite close to an incompatible intersection.