From 214eb71abf1841a36017ba8b79efcf8fa3b93b83 Mon Sep 17 00:00:00 2001 From: ashishpatel26 Date: Mon, 22 Jun 2026 16:04:49 +0530 Subject: [PATCH 1/4] spec: expand Never/NoReturn section with precise subtyping rules (#1458) The previous spec described Never in four lines without defining any of its subtyping behaviour. Type checkers converge on a consistent set of rules, but none were written down. This commit codifies them. Spec changes (docs/spec/special-types.rst): - Never is a subtype of every fully static type (bottom type property) - No type other than Never (and Any) is a subtype of Never - Never | T collapses to T for any type T - Never as a type argument: covariant containers accept it, invariant containers do not - type[Never] represents an uninhabitable class object - Clarify that NoReturn may appear in non-return positions Conformance test changes (conformance/tests/specialtypes_never.py): - Add func11: Never | int collapses to int - Add func12: object is not assignable to Never (E) - Add func13: raise in Never-returning function is OK - Add func14: type[Never] is a valid annotation - Add func15: list[Never] return is valid - Add func16: list[Never] is not assignable to list[int] (E) Result TOMLs updated for mypy, pyright, pyrefly, zuban (Pass). ty marked Partial: does not flag func12 and func16 errors. Closes #1458 --- .../results/mypy/specialtypes_never.toml | 4 ++ .../results/pyrefly/specialtypes_never.toml | 2 + .../results/pyright/specialtypes_never.toml | 5 ++ .../results/ty/specialtypes_never.toml | 9 ++- .../results/zuban/specialtypes_never.toml | 4 ++ conformance/tests/specialtypes_never.py | 41 ++++++++++++ docs/spec/special-types.rst | 67 ++++++++++++++++++- 7 files changed, 129 insertions(+), 3 deletions(-) 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 ` 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..93958adc0 100644 --- a/docs/spec/special-types.rst +++ b/docs/spec/special-types.rst @@ -95,14 +95,77 @@ 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 + +No type other than ``Never`` itself (and :ref:`Any `) is a subtype of +``Never``. In particular, ``object`` is *not* a subtype of ``Never``:: + + def g(x: object) -> Never: + return x # Error — object is not assignable to Never + +Because ``Never`` is a subtype of every 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 :term:`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:: + + from typing import Never + + def empty_list() -> list[Never]: + return [] + +When used with an :term:`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]`` represents the class object for a type that has no instances. +In practice this type is rarely useful directly, but it is the correct result +of narrowing a ``type[T]`` variable to an impossible branch. + .. _`numeric-promotions`: Special cases for ``float`` and ``complex`` From 290d119edfd838c99f926f34f1c7926fab1b4278 Mon Sep 17 00:00:00 2001 From: ashishpatel26 Date: Mon, 22 Jun 2026 23:22:11 +0530 Subject: [PATCH 2/4] Fix doc build: remove :term: references to undefined glossary entries --- docs/spec/special-types.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/spec/special-types.rst b/docs/spec/special-types.rst index 93958adc0..516a12332 100644 --- a/docs/spec/special-types.rst +++ b/docs/spec/special-types.rst @@ -136,7 +136,7 @@ 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 :term:`covariant` +``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:: @@ -146,7 +146,7 @@ useful to type an empty container whose element type is not yet known:: def empty_list() -> list[Never]: return [] -When used with an :term:`invariant` type parameter, the normal invariance rules +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 From 498e503cfbaa2ea5df51324cadf43a2aeb55a7ef Mon Sep 17 00:00:00 2001 From: ashishpatel26 Date: Mon, 22 Jun 2026 23:26:36 +0530 Subject: [PATCH 3/4] Address review comments: fix Any/subtype claim and clarify type[Never] --- docs/spec/special-types.rst | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/docs/spec/special-types.rst b/docs/spec/special-types.rst index 516a12332..a4694909b 100644 --- a/docs/spec/special-types.rst +++ b/docs/spec/special-types.rst @@ -117,8 +117,8 @@ 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 (and :ref:`Any `) is a subtype of -``Never``. In particular, ``object`` is *not* a subtype of ``Never``:: +No type other than ``Never`` itself is a subtype of ``Never``. In +particular, ``object`` is *not* a subtype of ``Never``:: def g(x: object) -> Never: return x # Error — object is not assignable to Never @@ -162,9 +162,10 @@ apply: ``Container[Never]`` is only assignable to ``Container[Never]``:: ``type[Never]`` ^^^^^^^^^^^^^^^^^ -``type[Never]`` represents the class object for a type that has no instances. -In practice this type is rarely useful directly, but it is the correct result -of narrowing a ``type[T]`` variable to an impossible branch. +``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. .. _`numeric-promotions`: From 25a452571e7fe4e22b877e4787e3eb977906794e Mon Sep 17 00:00:00 2001 From: ashishpatel26 Date: Mon, 22 Jun 2026 23:43:02 +0530 Subject: [PATCH 4/4] 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) --- docs/spec/special-types.rst | 28 +++++++++++++++------------- 1 file changed, 15 insertions(+), 13 deletions(-) diff --git a/docs/spec/special-types.rst b/docs/spec/special-types.rst index a4694909b..8a9a0cce1 100644 --- 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`: