Address grievejia review comments on Never/NoReturn spec

- Use int instead of object as the non-Never witness (object is already expected to not be a subtype of most things; int is more illuminating) - Rephrase to avoid the too-strong 'No type other than Never' claim (uninhabitable types like tuple[Never, int] are also subtypes of Never) - Qualify all 'every type T' as 'every fully static type T' throughout (the subtype relation is undefined for gradual types like Any) - Replace list[Never] with Sequence[Never] in the covariant example (list is invariant, so list[Never] is not assignable to list[int]; Sequence is covariant and correctly demonstrates the bottom-type behaviour)
ashishpatel26 · Jun 22, 2026 · Jun 22, 2026 · Jun 22, 2026 · Jun 22, 2026 · Jun 22, 2026
commit 25a452571e7fe4e22b877e4787e3eb977906794e
diff --git a/docs/spec/special-types.rst b/docs/spec/special-types.rst
@@ -117,14 +117,14 @@ to a variable of any type ``T``::
       v1: int = x   # OK — Never is a subtype of int
       v2: str = x   # OK — Never is a subtype of str
 
-No type other than ``Never`` itself is a subtype of ``Never``.  In
-particular, ``object`` is *not* a subtype of ``Never``::
+For ordinary inhabited types such as ``int`` or ``str``, no value is
+assignable to ``Never``::
 
-  def g(x: object) -> Never:
-      return x  # Error — object is not assignable to Never
+  def g(x: int) -> Never:
+      return x  # Error — int is not assignable to Never
 
-Because ``Never`` is a subtype of every type ``T``, the union ``Never | T`` is
-equivalent to ``T``::
+Because ``Never`` is a subtype of every fully static type ``T``, the union
+``Never | T`` is equivalent to ``T``::
 
   from typing import Never, Union
 
@@ -138,12 +138,14 @@ Using ``Never`` as a type argument
 
 ``Never`` may appear as a type argument.  When used with a covariant
 type parameter, ``Container[Never]`` is a subtype of ``Container[T]`` for
-every type ``T``, because ``Never`` is a subtype of every type.  This is
-useful to type an empty container whose element type is not yet known::
+every fully static type ``T``, because ``Never`` is a subtype of every fully
+static type.  This is useful to type an empty container whose element type is
+not yet known::
 
+  from collections.abc import Sequence
   from typing import Never
 
-  def empty_list() -> list[Never]:
+  def empty_sequence() -> Sequence[Never]:
       return []
 
 When used with an invariant type parameter, the normal invariance rules
@@ -162,10 +164,10 @@ apply: ``Container[Never]`` is only assignable to ``Container[Never]``::
 ``type[Never]``
 ^^^^^^^^^^^^^^^^^
 
-``type[Never]`` is a subtype of ``type[T]`` for every type ``T``, just as
-``Never`` is a subtype of every type ``T``.  In practice a variable receives
-this type only in provably unreachable code — for example, when narrowing a
-``type[int] | type[str]`` through all possible branches.
+``type[Never]`` is a subtype of ``type[T]`` for every fully static type ``T``,
+just as ``Never`` is a subtype of every fully static type ``T``.  In practice
+a variable receives this type only in provably unreachable code — for example,
+when narrowing a ``type[int] | type[str]`` through all possible branches.
 
 .. _`numeric-promotions`: