diff --git a/conformance/results/mypy/specialtypes_never.toml b/conformance/results/mypy/specialtypes_never.toml
index d4640eb57..d654a427b 100644
--- a/conformance/results/mypy/specialtypes_never.toml
+++ b/conformance/results/mypy/specialtypes_never.toml
@@ -5,6 +5,10 @@ specialtypes_never.py:85: error: Incompatible types in assignment (expression ha
 specialtypes_never.py:85: note: "list" is invariant -- see https://mypy.readthedocs.io/en/stable/common_issues.html#variance
 specialtypes_never.py:85: note: Consider using "Sequence" instead, which is covariant
 specialtypes_never.py:104: error: Incompatible return value type (got "ClassC[Never]", expected "ClassC[U]")  [return-value]
+specialtypes_never.py:121: error: Return statement in function which does not return  [misc]
+specialtypes_never.py:145: error: Incompatible return value type (got "list[Never]", expected "list[int]")  [return-value]
+specialtypes_never.py:145: note: "list" is invariant -- see https://mypy.readthedocs.io/en/stable/common_issues.html#variance
+specialtypes_never.py:145: note: Consider using "Sequence" instead, which is covariant
 """
 conformance_automated = "Pass"
 errors_diff = """
diff --git a/conformance/results/pyrefly/specialtypes_never.toml b/conformance/results/pyrefly/specialtypes_never.toml
index 251ce6ae0..3e7c60039 100644
--- a/conformance/results/pyrefly/specialtypes_never.toml
+++ b/conformance/results/pyrefly/specialtypes_never.toml
@@ -6,4 +6,6 @@ output = """
 ERROR specialtypes_never.py:19:22-30: Function declared to return `NoReturn` but is missing an explicit `return` [bad-return]
 ERROR specialtypes_never.py:85:21-22: `list[Never]` is not assignable to `list[int]` [bad-assignment]
 ERROR specialtypes_never.py:104:12-27: Returned type `ClassC[Never]` is not assignable to declared return type `ClassC[U]` [bad-return]
+ERROR specialtypes_never.py:121:12-13: Returned type `object` is not assignable to declared return type `Never` [bad-return]
+ERROR specialtypes_never.py:145:12-13: Returned type `list[Never]` is not assignable to declared return type `list[int]` [bad-return]
 """
diff --git a/conformance/results/pyright/specialtypes_never.toml b/conformance/results/pyright/specialtypes_never.toml
index ad3d6a257..19e4e20a9 100644
--- a/conformance/results/pyright/specialtypes_never.toml
+++ b/conformance/results/pyright/specialtypes_never.toml
@@ -8,6 +8,11 @@ specialtypes_never.py:85:21 - error: Type "list[Never]" is not assignable to dec
 specialtypes_never.py:104:12 - error: Type "ClassC[Never]" is not assignable to return type "ClassC[U@func10]"
   "ClassC[Never]" is not assignable to "ClassC[U@func10]"
     Type parameter "T@ClassC" is invariant, but "Never" is not the same as "U@func10" (reportReturnType)
+specialtypes_never.py:121:5 - error: Function with declared return type "NoReturn" cannot include a return statement (reportGeneralTypeIssues)
+specialtypes_never.py:145:12 - error: Type "list[Never]" is not assignable to return type "list[int]"
+  "list[Never]" is not assignable to "list[int]"
+    Type parameter "_T@list" is invariant, but "Never" is not the same as "int"
+    Consider switching from "list" to "Sequence" which is covariant (reportReturnType)
 """
 conformance_automated = "Pass"
 errors_diff = """
diff --git a/conformance/results/ty/specialtypes_never.toml b/conformance/results/ty/specialtypes_never.toml
index 9f528bb43..5ecadda41 100644
--- a/conformance/results/ty/specialtypes_never.toml
+++ b/conformance/results/ty/specialtypes_never.toml
@@ -1,5 +1,12 @@
-conformance_automated = "Pass"
+conformant = "Partial"
+notes = """
+Does not flag `return <object>` in a function declared `-> Never` (line 121).
+Does not flag `return list[Never]` where `list[int]` is expected (line 145).
+"""
+conformance_automated = "Partial"
 errors_diff = """
+Line 121: Expected 1 errors
+Line 145: Expected 1 errors
 """
 output = """
 specialtypes_never.py:19:22: error[invalid-return-type] Function always implicitly returns `None`, which is not assignable to return type `Never`
diff --git a/conformance/results/zuban/specialtypes_never.toml b/conformance/results/zuban/specialtypes_never.toml
index d65bc2c97..894d7d7bf 100644
--- a/conformance/results/zuban/specialtypes_never.toml
+++ b/conformance/results/zuban/specialtypes_never.toml
@@ -7,4 +7,8 @@ specialtypes_never.py:85: error: Incompatible types in assignment (expression ha
 specialtypes_never.py:85: note: "List" is invariant -- see https://mypy.readthedocs.io/en/stable/common_issues.html#variance
 specialtypes_never.py:85: note: Consider using "Sequence" instead, which is covariant
 specialtypes_never.py:104: error: Incompatible return value type (got "ClassC[Never]", expected "ClassC[U]")  [return-value]
+specialtypes_never.py:121: error: Return statement in function which does not return  [misc]
+specialtypes_never.py:145: error: Incompatible return value type (got "list[Never]", expected "list[int]")  [return-value]
+specialtypes_never.py:145: note: "List" is invariant -- see https://mypy.readthedocs.io/en/stable/common_issues.html#variance
+specialtypes_never.py:145: note: Consider using "Sequence" instead, which is covariant
 """
diff --git a/conformance/tests/specialtypes_never.py b/conformance/tests/specialtypes_never.py
index a3ffb4cc1..77f7d0e94 100644
--- a/conformance/tests/specialtypes_never.py
+++ b/conformance/tests/specialtypes_never.py
@@ -102,3 +102,44 @@ class ClassC(Generic[T]):
 def func10(x: U) -> ClassC[U]:
     # Never is not compatible in an invariant context.
     return ClassC[Never]()  # E
+
+
+# Never | T is equivalent to T — the union collapses.
+
+type Alias1 = Never | int   # Equivalent to int
+type Alias2 = int | Never   # Equivalent to int
+
+
+def func11(x: Alias1) -> int:
+    return x  # OK — Alias1 is int
+
+
+# No type other than Never (and Any) is assignable to Never.
+
+
+def func12(x: object) -> Never:
+    return x  # E
+
+
+def func13() -> Never:
+    raise RuntimeError("never")  # OK
+
+
+# type[Never] is valid and represents an uninhabitable class object.
+
+
+def func14(cls: type[Never]) -> None:
+    pass
+
+
+# Empty containers typed as list[Never] are assignable to list[T]
+# only when T is used covariantly; list itself is invariant, so
+# list[Never] is not assignable to list[int].
+
+
+def func15() -> list[Never]:
+    return []  # OK
+
+
+def func16(x: list[Never]) -> list[int]:
+    return x  # E — list is invariant
diff --git a/docs/spec/special-types.rst b/docs/spec/special-types.rst
index eab658b07..8a9a0cce1 100644
--- a/docs/spec/special-types.rst
+++ b/docs/spec/special-types.rst
@@ -95,14 +95,80 @@ is unreachable and will behave accordingly::
 ---------
 
 Since Python 3.11, the ``typing`` module contains a :term:`special form`
-``Never``. It represents the bottom type, a type that represents the empty set
-of Python objects.
+``Never``. It represents the **bottom type**: the type that denotes the empty
+set of Python objects.  No Python object can be a runtime instance of
+``Never``.
 
 The ``Never`` type is equivalent to ``NoReturn``, which is discussed above.
 The ``NoReturn`` type is conventionally used in return annotations of
 functions, and ``Never`` is typically used in other locations, but the two
 types are completely interchangeable.
 
+Subtyping rules for ``Never``
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Because ``Never`` is the bottom type, it is a :term:`subtype` of every fully
+static type.  This means that a value of type ``Never`` is :term:`assignable`
+to a variable of any type ``T``::
+
+  from typing import Never
+
+  def f(x: Never) -> None:
+      v1: int = x   # OK — Never is a subtype of int
+      v2: str = x   # OK — Never is a subtype of str
+
+For ordinary inhabited types such as ``int`` or ``str``, no value is
+assignable to ``Never``::
+
+  def g(x: int) -> Never:
+      return x  # Error — int is not assignable to Never
+
+Because ``Never`` is a subtype of every fully static type ``T``, the union
+``Never | T`` is equivalent to ``T``::
+
+  from typing import Never, Union
+
+  type Alias = Never | int  # Equivalent to int
+
+Code following a call to a function that returns ``Never`` is unreachable.
+Type checkers may suppress errors in unreachable blocks.
+
+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 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_sequence() -> Sequence[Never]:
+      return []
+
+When used with an invariant type parameter, the normal invariance rules
+apply: ``Container[Never]`` is only assignable to ``Container[Never]``::
+
+  from typing import Generic, Never, TypeVar
+
+  T = TypeVar("T")
+
+  class Box(Generic[T]):
+      pass
+
+  def f() -> Box[int]:
+      return Box[Never]()  # Error — Box is invariant in T
+
+``type[Never]``
+^^^^^^^^^^^^^^^^^
+
+``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`:
 
 Special cases for ``float`` and ``complex``