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)

Author: ashishpatel26

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`: