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

Bắt đầu với ví dụ về Never trong issue này và xem xét thảo luận được liên kết về subtyping cũng như công việc đang diễn ra nhằm hình thức hóa hệ thống typing của Python. Được xem là hoàn thành khi đạt được và ghi lại một đặc tả rõ ràng cho Never và NoReturn, bao gồm tương tác của chúng với structural subtyping và trường hợp LSP được mô tả ở đây.