NoReturn and Never are underspecified in the spec

Never was added without a PEP as a way to directly indicate that something is uninhabited in 3.11

This brings up something from https://github.com/CarliJoy/intersection_examples/issues/5#issuecomment-1699490563 where we now have a way to express what appears to be an LSP violation that type checks (incorrectly) properly via structural subtyping by mishandling Never as a subtype of other types. Never is not a subtype of all other types. As the bottom type, it is uninhabited and does not follow subtyping rules.

from typing import Never

class A:
    def foo(self, x: int) -> None: ...
    
class B(A):
    foo: Never   # __getattr__(B, "foo") -> raise NotImplementedError
    
x: A = B()  # type checks 
reveal_type(B.foo)

https://mypy-play.net/?mypy=latest&python=3.11&flags=strict&gist=a4279b36d82c1a28d7b17be9a4bbcbdf

I believe under LSP, B is no longer a safe drop-in replacement for A. It's important to note that ongoing work to formalize the type system, including Never does not treat Never as a subtype of all other types, see the ongoing work here: http://bit.ly/python-subtyping

Inizia con l’esempio di Never in questo issue e rivedi la discussione collegata sul sottotipaggio e il lavoro in corso sulla formalizzazione del type checking di Python. Il lavoro è completato quando è stata raggiunta e documentata una specifica chiara per Never e NoReturn, inclusa la loro interazione con il sottotipaggio strutturale e il caso LSP descritto qui.