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

从此 issue 中的 Never 示例开始，查看链接的子类型关系讨论以及正在进行的 Python 类型系统形式化工作。完成的标准是为 Never 和 NoReturn 达成并记录一份明确的规范，其中包括它们与结构化子类型关系的交互，以及此处描述的 LSP 情况。