new "type system concepts" section (#1743)

Co-authored-by: Jelle Zijlstra <[email protected]>
Co-authored-by: Alex Waygood <[email protected]>

docs/spec/annotations.rst

@@ -16,13 +16,18 @@ hinting is used by filling function annotation slots with classes::
 This states that the expected type of the ``name`` argument is
 ``str``.  Analogically, the expected return type is ``str``.
 
-Expressions whose type is a subtype of a specific argument type are
-also accepted for that argument.
+Expressions whose type is :term:`assignable` to a specific argument type are
+also accepted for that argument. Similarly, an expression whose type is
+assignable to the annotated return type can be returned from the function.
 
 .. _`missing-annotations`:
 
-Any function without annotations should be treated as having the most
-general type possible, or ignored, by any type checker.
+Any function without annotations can be treated as having :ref:`Any`
+annotations on all arguments and the return type. Type checkers may also
+optionally infer more precise types for missing annotations.
+
+Type checkers may choose to entirely ignore (not type check) the bodies of
+functions with no annotations, but this behavior is not required.
 
 It is recommended but not required that checked functions have
 annotations for all arguments and the return type.  For a checked

docs/spec/class-compat.rst

@@ -1,6 +1,6 @@
 .. _`class-compat`:
 
-Class type compatibility
+Class type assignability
 ========================
 
 .. _`classvar`:
@@ -97,8 +97,9 @@ annotated in ``__init__`` or other methods, rather than in the class::
 (Originally specified by :pep:`698`.)
 
 When type checkers encounter a method decorated with ``@typing.override`` they
-should treat it as a type error unless that method is overriding a compatible
-method or attribute in some ancestor class.
+should treat it as a type error unless that method is overriding a method or
+attribute in some ancestor class, and the type of the overriding method is
+:term:`assignable` to the type of the overridden method.
 
 
 .. code-block:: python

docs/spec/constructors.rst

@@ -105,11 +105,11 @@ unrelated class.
 
 If the evaluated return type of ``__new__`` is not the class being constructed
 (or a subclass thereof), a type checker should assume that the ``__init__``
-method will not be called. This is consistent with the runtime behavior of
-the ``type.__call__`` method. If the ``__new__`` method return type is
-a union with one or more subtypes that are not instances of the class being
-constructed (or a subclass thereof), a type checker should likewise assume that
-the ``__init__`` method will not be called.
+method will not be called. This is consistent with the runtime behavior of the
+``type.__call__`` method. If the ``__new__`` method return type is a union with
+one or more members that are not the class being constructed (or a subclass
+thereof), a type checker should likewise assume that the ``__init__`` method
+will not be called.
 
   ::
 
@@ -337,7 +337,7 @@ Consistency of ``__new__`` and ``__init__``
 -------------------------------------------
 
 Type checkers may optionally validate that the ``__new__`` and ``__init__``
-methods for a class have consistent signatures.
+methods for a class have :term:`consistent` signatures.
 
   ::
 
@@ -353,7 +353,8 @@ methods for a class have consistent signatures.
 Converting a Constructor to Callable
 ------------------------------------
 
-Class objects are callable, which means they are compatible with callable types.
+Class objects are callable, which means the type of a class object can be
+:term:`assignable` to a callable type.
 
   ::
 

docs/spec/directives.rst

@@ -86,12 +86,6 @@ At runtime a cast always returns the
 expression unchanged -- it does not check the type, and it does not
 convert or coerce the value.
 
-Casts differ from type comments (see the previous section).  When using
-a type comment, the type checker should still verify that the inferred
-type is consistent with the stated type.  When using a cast, the type
-checker should blindly believe the programmer.  Also, casts can be used
-in expressions, while type comments only apply to assignments.
-
 .. _`if-type-checking`:
 
 ``TYPE_CHECKING``

docs/spec/enums.rst

@@ -350,7 +350,7 @@ literal values during type narrowing and exhaustion detection::
 
 
 Likewise, a type checker should treat a complete union of all literal members
-as compatible with the enum type::
+as :term:`equivalent` to the enum type::
 
     class Answer(Enum):
         Yes = 1

docs/spec/generics.rst

@@ -474,12 +474,12 @@ classes without a metaclass conflict.
 Type variables with an upper bound
 ----------------------------------
 
-A type variable may specify an upper bound using ``bound=<type>`` (when
-using the ``TypeVar`` constructor) or using ``: <type>`` (when using the native
-syntax for generics). The bound itself cannot be parameterized by type variables.
-This means that an
-actual type substituted (explicitly or implicitly) for the type variable must
-be a subtype of the boundary type. Example::
+A type variable may specify an upper bound using ``bound=<type>`` (when using
+the ``TypeVar`` constructor) or using ``: <type>`` (when using the native
+syntax for generics). The bound itself cannot be parameterized by type
+variables. This means that an actual type substituted (explicitly or
+implicitly) for the type variable must be :term:`assignable` to the bound.
+Example::
 
   from typing import TypeVar
   from collections.abc import Sized
@@ -496,11 +496,10 @@ be a subtype of the boundary type. Example::
   longer({1}, {1, 2})  # ok, return type set[int]
   longer([1], {1, 2})  # ok, return type a supertype of list[int] and set[int]
 
-An upper bound cannot be combined with type constraints (as used in
-``AnyStr``, see the example earlier); type constraints cause the
-inferred type to be *exactly* one of the constraint types, while an
-upper bound just requires that the actual type is a subtype of the
-boundary type.
+An upper bound cannot be combined with type constraints (as used in ``AnyStr``,
+see the example earlier); type constraints cause the inferred type to be
+*exactly* one of the constraint types, while an upper bound just requires that
+the actual type is :term:`assignable` to the bound.
 
 .. _`variance`:
 
@@ -523,13 +522,12 @@ introduction to these concepts can be found on `Wikipedia
 <https://en.wikipedia.org/wiki/Covariance_and_contravariance_%28computer_science%29>`_ and in :pep:`483`; here we just show how to control
 a type checker's behavior.
 
-By default generic types declared using the old ``TypeVar`` syntax
-are considered *invariant* in all type variables,
-which means that values for variables annotated with types like
-``list[Employee]`` must exactly match the type annotation -- no subclasses or
-superclasses of the type parameter (in this example ``Employee``) are
-allowed. See below for the behavior when using the built-in generic syntax
-in Python 3.12 and higher.
+By default generic types declared using the old ``TypeVar`` syntax are
+considered *invariant* in all type variables, which means that e.g.
+``list[Manager]`` is neither a supertype nor a subtype of ``list[Employee]``.
+
+See below for the behavior when using the built-in generic syntax in Python
+3.12 and higher.
 
 To facilitate the declaration of container types where covariant or
 contravariant type checking is acceptable, type variables accept keyword
@@ -1926,7 +1924,7 @@ Using a type parameter from an outer scope as a default is not supported.
 Bound Rules
 ^^^^^^^^^^^
 
-``T1``'s bound must be a subtype of ``T2``'s bound.
+``T1``'s bound must be :term:`assignable` to ``T2``'s bound.
 
 ::
 
@@ -2022,8 +2020,8 @@ normal subscription rules, non-overridden defaults should be substituted.
 Using ``bound`` and ``default``
 """""""""""""""""""""""""""""""
 
-If both ``bound`` and ``default`` are passed, ``default`` must be a
-subtype of ``bound``. If not, the type checker should generate an
+If both ``bound`` and ``default`` are passed, ``default`` must be
+:term:`assignable` to ``bound``. If not, the type checker should generate an
 error.
 
 ::
@@ -2268,7 +2266,8 @@ Use in Attribute Annotations
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
 Another use for ``Self`` is to annotate attributes. One example is where we
-have a ``LinkedList`` whose elements must be subclasses of the current class.
+have a ``LinkedList`` whose elements must be :term:`assignable` to the current
+class.
 
 ::
 
@@ -2298,8 +2297,8 @@ constructions with subclasses:
         def ordinal_value(self) -> str:
             return as_ordinal(self.value)
 
-    # Should not be OK because LinkedList[int] is not a subclass of
-    # OrdinalLinkedList, # but the type checker allows it.
+    # Should not be OK because LinkedList[int] is not assignable to
+    # OrdinalLinkedList, but the type checker allows it.
     xs = OrdinalLinkedList(value=1, next=LinkedList[int](value=2))
 
     if xs.next:
@@ -2469,11 +2468,11 @@ See :pep:`PEP 544
 <544#self-types-in-protocols>` for
 details on the behavior of TypeVars bound to protocols.
 
-Checking a class for compatibility with a protocol: If a protocol uses
-``Self`` in methods or attribute annotations, then a class ``Foo`` is
-considered compatible with the protocol if its corresponding methods and
-attribute annotations use either ``Self`` or ``Foo`` or any of ``Foo``’s
-subclasses. See the examples below:
+Checking a class for assignability to a protocol: If a protocol uses ``Self``
+in methods or attribute annotations, then a class ``Foo`` is :term:`assignable`
+to the protocol if its corresponding methods and attribute annotations use
+either ``Self`` or ``Foo`` or any of ``Foo``’s subclasses. See the examples
+below:
 
 ::
 
@@ -2705,16 +2704,15 @@ by the ``TypeVar`` constructor call. No further inference is needed.
 3. Create two specialized versions of the class. We'll refer to these as
 ``upper`` and ``lower`` specializations. In both of these specializations,
 replace all type parameters other than the one being inferred by a dummy type
-instance (a concrete anonymous class that is type compatible with itself and
-assumed to meet the bounds or constraints of the type parameter). In
-the ``upper`` specialized class, specialize the target type parameter with
-an ``object`` instance. This specialization ignores the type parameter's
-upper bound or constraints. In the ``lower`` specialized class, specialize
-the target type parameter with itself (i.e. the corresponding type argument
-is the type parameter itself).
-
-4. Determine whether ``lower`` can be assigned to ``upper`` using normal type
-compatibility rules. If so, the target type parameter is covariant. If not,
+instance (a concrete anonymous class that is assumed to meet the bounds or
+constraints of the type parameter). In the ``upper`` specialized class,
+specialize the target type parameter with an ``object`` instance. This
+specialization ignores the type parameter's upper bound or constraints. In the
+``lower`` specialized class, specialize the target type parameter with itself
+(i.e. the corresponding type argument is the type parameter itself).
+
+4. Determine whether ``lower`` can be assigned to ``upper`` using normal
+assignability rules. If so, the target type parameter is covariant. If not,
 determine whether ``upper`` can be assigned to ``lower``. If so, the target
 type parameter is contravariant. If neither of these combinations are
 assignable, the target type parameter is invariant.
@@ -2737,9 +2735,8 @@ To determine the variance of ``T1``, we specialize ``ClassA`` as follows:
     upper = ClassA[object, Dummy, Dummy]
     lower = ClassA[T1, Dummy, Dummy]
 
-We find that ``upper`` is not assignable to ``lower`` using normal type
-compatibility rules defined in :pep:`484`. Likewise, ``lower`` is not assignable
-to ``upper``, so we conclude that ``T1`` is invariant.
+We find that ``upper`` is not assignable to ``lower``. Likewise, ``lower`` is
+not assignable to ``upper``, so we conclude that ``T1`` is invariant.
 
 To determine the variance of ``T2``, we specialize ``ClassA`` as follows: