PEP 724: Stricter TypeGuard

.github/CODEOWNERS

@@ -601,6 +601,7 @@ pep-0719.rst  @Yhg1s
 pep-0720.rst  @FFY00
 pep-0721.rst  @encukou
 pep-0722.rst  @pfmoore
+pep-0724.rst  @jellezijlstra
 # ...
 # pep-0754.txt
 # ...

pep-0724.rst

@@ -0,0 +1,238 @@
+PEP: 724
+Title: Stricter Type Guards
+Author: Rich Chiodo <rchiodo at microsoft.com>, 
+        Eric Traut <erictr at microsoft.com>, 
+        Erik De Bonte <erikd at microsoft.com>
+Sponsor: Jelle Zijlstra <[email protected]>
+Discussions-To: https://mail.python.org/archives/list/[email protected]/thread/EMUD2D424OI53DCWQ4H5L6SJD2IXBHUL/
+Status: Draft
+Type: Standards Track
+Topic: Typing
+Content-Type: text/x-rst
+Created: 28-Jul-2023
+Python-Version: 3.13
+Post-History: 
+
+
+Abstract
+========
+
+:pep:`647` introduced the concept of ``TypeGuard`` functions which return
+``True`` if their input parameter matches their target type. For example, a
+function that returns ``TypeGuard[str]`` is assumed to return ``True`` if and
+only if its input parameter is a ``str``. This allows type checkers to narrow
+types when a ``TypeGuard`` function returns ``True``.
+
+This PEP further refines :pep:`647` by allowing type checkers to also narrow
+types when a ``TypeGuard`` function returns ``False``.
+
+Motivation
+==========
+
+``TypeGuards`` are used throughout Python libraries to allow a type checker to
+narrow the type of something when the ``TypeGuard`` returns ``True``.
+
+However, in the ``False`` case, :pep:`647` doesn't prescribe what the type
+might be:
+
+.. code-block:: python
+
+    def is_str(val: str | int) -> TypeGuard[str]:
+        return isinstance(val, str)
+
+    def func(val: str | int):
+        if is_str(val):
+            # Type checkers can assume val is a 'str' in this branch
+        else:
+            # Type here is not narrowed. It is still 'str | int' 
+
+
+Specification
+=============
+
+This PEP proposes some modifications to :pep:`647` in order to allow a type
+checker to further narrow what a ``TypeGuard`` is indicating when it returns
+``False``.
+
+* When the output type of a ``TypeGuard`` is consistent [#isconsistent]_ with
+  the type of its first input parameter, type checkers will apply stricter type
+  semantics:
+
+.. code-block:: python
+
+    # Stricter TypeGuard possible (Kangaroo | Koala is consistent with Animal)
+    def is_marsupial(val: Animal) -> TypeGuard[Kangaroo | Koala]: 
+        return isinstance(val, Kangaroo | Koala)
+
+    # Stricter TypeGuard not possible (list[T] is not consistent with 
+    # list[T | None])
+    def has_no_nones(val: list[T | None]) -> TypeGuard[list[T]]: 
+        return None not in val
+
+* When stricter semantics are possible, the output type for the ``False`` case
+  can be determined:
+
+.. code-block:: python
+
+    def is_str(val: str | int) -> TypeGuard[str]: # Stricter mode possible
+        return isinstance(val, str)
+
+    def func(val: str | int):
+        if is_str(val):
+            # Type checkers can assume val is a 'str' in this branch
+        else:
+            # Type checkers can assume val is an 'int' in this branch
+
+* When the output type of the ``TypeGuard`` is a union, the type checker can
+  apply additional type narrowing based on the type of the first input
+  argument, eliminating union elements that are impossible given the input
+  argument type:
+
+.. code-block:: python
+
+    def is_cardinal_direction(val: str) -> TypeGuard[Literal["N", "S", "E", "W"]]:
+        return val in ("N", "S", "E", "W")
+
+    def func(direction: Literal["NW", "E"]):
+        if is_cardinal_direction(direction):
+            # Literal["E"] The type cannot be "N", "S" or "W" here because of
+            # argument type
+        else:
+            # Literal["NW"]
+
+Additional Examples
+===================
+
+Any
+---
+
+``Any`` is consistent [#isconsistent]_ with any other type, which means
+stricter semantics can be applied. 
+
+.. code-block:: python
+
+    def is_a(x: Any) -> TypeGuard[A]: # Stricter TypeGuard possible
+        return isinstance(x, A)
+
+    def test(x: A | B):
+        if is_a(x):
+            # x is of type A here
+        else:
+            # x is of type B here
+
+Covariance
+----------
+
+Covariance is not the same thing as being consistent [#isconsistent]_:
+
+.. code-block:: python
+
+    def is_str_seq(val: Sequence[str | int]) -> TypeGuard[Sequence[str]]:
+        return all(isinstance(x, str) for x in val)
+
+    def func3(val: Sequence[str | int]):
+        if is_str_seq(val):
+            # val is Sequence[str]
+        else:
+            # val is Sequence[str | int]
+
+Type ``B`` is consistent [#isconsistent]_ with type ``A`` if
+
+* ``B`` is a subtype of ``A``
+* ``A`` is Any
+* ``B`` is Any
+
+``Sequence[str]`` is not a subtype of ``Sequence[str | int]`` so the special
+semantics cannot be applied and only the ``True`` case is narrowed. 
+
+Degenerate case
+---------------
+
+It is possible to break the type checker by making a ``TypeGuard`` that is
+incorrect:
+
+.. code-block:: python
+
+    def is_positive_int(val: int | str) -> TypeGuard[int]:
+        return isinstance(val, int) and val > 0
+
+    def func(val: int | str):
+        if is_positive_int(val):
+            # Type checker assumes int here
+        else:
+            # Type checker assumes str incorrectly here
+
+As :pep:`647 <647#enforcing-strict-narrowing>` stated, users can create invalid
+``TypeGuards``. The same thing applies to this PEP. If the user is not careful
+the type checker may flag things incorrectly.
+
+Backwards Compatibility
+=======================
+
+The new ``False`` case for a ``TypeGuard`` breaks backwards compatibility.
+
+.. code-block:: python
+
+    def is_int(val: int | str) -> TypeGuard[int]:
+        return isinstance(val, int)
+
+    def func(val: int | str):
+        if is_int(val):
+            # Type checker assumes int here
+        else:
+            # Type checker assumes str here
+
+A type checker will assume in the ``False`` case that the value is ``str``.
+
+This is a change in behavior from :pep:`647`.
+
+TBD: Not sure what the resolution of this should be yet. I want to say
+something like - Code that already exists would not be harmed by this change as
+existing code would have more checks to validate the type on the else case. For
+new code, the assumption is that users will expect this behavior anyway.
+
+
+How to Teach This
+=================
+
+We assert that users unfamiliar with ``TypeGuard`` will expect the behavior
+outlined in this PEP, therefore making ``TypeGuard`` easier to teach and
+explain.
+
+
+Reference Implementation
+========================
+
+A reference `implementation`__ of this idea exists in Pyright.
+
+__ https://github.com/microsoft/pyright/commit/9a5af798d726bd0612cebee7223676c39cf0b9b0
+
+
+Rejected Ideas
+==============
+
+Originally a new ``StrictTypeGuard`` construct was proposed. A
+``StrictTypeGuard`` would be similar to to a ``TypeGuard`` except it would
+explicitly state that output type was consistent [#isconsistent]_ with the
+input type. Type checkers would validate that the output type was consistent
+[#isconsistent]_ with the input type.
+
+See this comment: `StrictTypeGuard proposal`__
+
+__ https://github.com/python/typing/discussions/1013#discussioncomment-1966238
+
+This was rejected because for most cases it's not necessary. Most people assume
+when the ``TypeGuard`` returns ``False``, that the input type has been narrowed
+to its other type. Why not just change the specification to match their
+assumptions?
+
+Footnotes
+=========
+
+.. [#isconsistent] :pep:`PEP 483's discussion of is-consistent <483#summary-of-gradual-typing>`
+
+Copyright
+=========
+
+This document is placed in the public domain or under the CC0-1.0-Universal
+license, whichever is more permissive.