Rename Red Knot (#17820)

crates/ty_python_semantic/resources/mdtest/directives/assert_never.md

@@ -0,0 +1,111 @@
+# `assert_never`
+
+## Basic functionality
+
+`assert_never` makes sure that the type of the argument is `Never`. If it is not, a
+`type-assertion-failure` diagnostic is emitted.
+
+```py
+from typing_extensions import assert_never, Never, Any
+from ty_extensions import Unknown
+
+def _(never: Never, any_: Any, unknown: Unknown, flag: bool):
+    assert_never(never)  # fine
+
+    assert_never(0)  # error: [type-assertion-failure]
+    assert_never("")  # error: [type-assertion-failure]
+    assert_never(None)  # error: [type-assertion-failure]
+    assert_never([])  # error: [type-assertion-failure]
+    assert_never({})  # error: [type-assertion-failure]
+    assert_never(())  # error: [type-assertion-failure]
+    assert_never(1 if flag else never)  # error: [type-assertion-failure]
+
+    assert_never(any_)  # error: [type-assertion-failure]
+    assert_never(unknown)  # error: [type-assertion-failure]
+```
+
+## Use case: Type narrowing and exhaustiveness checking
+
+```toml
+[environment]
+python-version = "3.10"
+```
+
+`assert_never` can be used in combination with type narrowing as a way to make sure that all cases
+are handled in a series of `isinstance` checks or other narrowing patterns that are supported.
+
+```py
+from typing_extensions import assert_never, Literal
+
+class A: ...
+class B: ...
+class C: ...
+
+def if_else_isinstance_success(obj: A | B):
+    if isinstance(obj, A):
+        pass
+    elif isinstance(obj, B):
+        pass
+    elif isinstance(obj, C):
+        pass
+    else:
+        assert_never(obj)
+
+def if_else_isinstance_error(obj: A | B):
+    if isinstance(obj, A):
+        pass
+    # B is missing
+    elif isinstance(obj, C):
+        pass
+    else:
+        # error: [type-assertion-failure] "Expected type `Never`, got `B & ~A & ~C` instead"
+        assert_never(obj)
+
+def if_else_singletons_success(obj: Literal[1, "a"] | None):
+    if obj == 1:
+        pass
+    elif obj == "a":
+        pass
+    elif obj is None:
+        pass
+    else:
+        assert_never(obj)
+
+def if_else_singletons_error(obj: Literal[1, "a"] | None):
+    if obj == 1:
+        pass
+    elif obj is "A":  # "A" instead of "a"
+        pass
+    elif obj is None:
+        pass
+    else:
+        # error: [type-assertion-failure] "Expected type `Never`, got `Literal["a"]` instead"
+        assert_never(obj)
+
+def match_singletons_success(obj: Literal[1, "a"] | None):
+    match obj:
+        case 1:
+            pass
+        case "a":
+            pass
+        case None:
+            pass
+        case _ as obj:
+            # TODO: Ideally, we would not emit an error here
+            # error: [type-assertion-failure] "Expected type `Never`, got `@Todo"
+            assert_never(obj)
+
+def match_singletons_error(obj: Literal[1, "a"] | None):
+    match obj:
+        case 1:
+            pass
+        case "A":  # "A" instead of "a"
+            pass
+        case None:
+            pass
+        case _ as obj:
+            # TODO: We should emit an error here, but the message should
+            # show the type `Literal["a"]` instead of `@Todo(…)`.
+            # error: [type-assertion-failure] "Expected type `Never`, got `@Todo"
+            assert_never(obj)
+```

crates/ty_python_semantic/resources/mdtest/directives/assert_type.md

@@ -0,0 +1,138 @@
+# `assert_type`
+
+## Basic
+
+```py
+from typing_extensions import assert_type
+
+def _(x: int):
+    assert_type(x, int)  # fine
+    assert_type(x, str)  # error: [type-assertion-failure]
+```
+
+## Narrowing
+
+The asserted type is checked against the inferred type, not the declared type.
+
+```toml
+[environment]
+python-version = "3.10"
+```
+
+```py
+from typing_extensions import assert_type
+
+def _(x: int | str):
+    if isinstance(x, int):
+        reveal_type(x)  # revealed: int
+        assert_type(x, int)  # fine
+```
+
+## Equivalence
+
+The actual type must match the asserted type precisely.
+
+```py
+from typing import Any, Type, Union
+from typing_extensions import assert_type
+
+# Subtype does not count
+def _(x: bool):
+    assert_type(x, int)  # error: [type-assertion-failure]
+
+def _(a: type[int], b: type[Any]):
+    assert_type(a, type[Any])  # error: [type-assertion-failure]
+    assert_type(b, type[int])  # error: [type-assertion-failure]
+
+# The expression constructing the type is not taken into account
+def _(a: type[int]):
+    assert_type(a, Type[int])  # fine
+```
+
+## Gradual types
+
+```py
+from typing import Any
+from typing_extensions import Literal, assert_type
+
+from ty_extensions import Unknown
+
+# Any and Unknown are considered equivalent
+def _(a: Unknown, b: Any):
+    reveal_type(a)  # revealed: Unknown
+    assert_type(a, Any)  # fine
+
+    reveal_type(b)  # revealed: Any
+    assert_type(b, Unknown)  # fine
+
+def _(a: type[Unknown], b: type[Any]):
+    reveal_type(a)  # revealed: type[Unknown]
+    assert_type(a, type[Any])  # fine
+
+    reveal_type(b)  # revealed: type[Any]
+    assert_type(b, type[Unknown])  # fine
+```
+
+## Tuples
+
+Tuple types with the same elements are the same.
+
+```py
+from typing_extensions import Any, assert_type
+
+from ty_extensions import Unknown
+
+def _(a: tuple[int, str, bytes]):
+    assert_type(a, tuple[int, str, bytes])  # fine
+
+    assert_type(a, tuple[int, str])  # error: [type-assertion-failure]
+    assert_type(a, tuple[int, str, bytes, None])  # error: [type-assertion-failure]
+    assert_type(a, tuple[int, bytes, str])  # error: [type-assertion-failure]
+
+def _(a: tuple[Any, ...], b: tuple[Unknown, ...]):
+    assert_type(a, tuple[Any, ...])  # fine
+    assert_type(a, tuple[Unknown, ...])  # fine
+
+    assert_type(b, tuple[Unknown, ...])  # fine
+    assert_type(b, tuple[Any, ...])  # fine
+```
+
+## Unions
+
+Unions with the same elements are the same, regardless of order.
+
+```toml
+[environment]
+python-version = "3.10"
+```
+
+```py
+from typing_extensions import assert_type
+
+def _(a: str | int):
+    assert_type(a, str | int)
+    assert_type(a, int | str)
+```
+
+## Intersections
+
+Intersections are the same when their positive and negative parts are respectively the same,
+regardless of order.
+
+```py
+from typing_extensions import assert_type
+
+from ty_extensions import Intersection, Not
+
+class A: ...
+class B: ...
+class C: ...
+class D: ...
+
+def _(a: A):
+    if isinstance(a, B) and not isinstance(a, C) and not isinstance(a, D):
+        reveal_type(a)  # revealed: A & B & ~C & ~D
+
+        assert_type(a, Intersection[A, B, Not[C], Not[D]])
+        assert_type(a, Intersection[B, A, Not[D], Not[C]])
+```

crates/ty_python_semantic/resources/mdtest/directives/cast.md

@@ -0,0 +1,70 @@
+# `cast`
+
+`cast()` takes two arguments, one type and one value, and returns a value of the given type.
+
+The (inferred) type of the value and the given type do not need to have any correlation.
+
+```py
+from typing import Literal, cast, Any
+
+reveal_type(True)  # revealed: Literal[True]
+reveal_type(cast(str, True))  # revealed: str
+reveal_type(cast("str", True))  # revealed: str
+
+reveal_type(cast(int | str, 1))  # revealed: int | str
+
+reveal_type(cast(val="foo", typ=int))  # revealed: int
+
+# error: [invalid-type-form]
+reveal_type(cast(Literal, True))  # revealed: Unknown
+
+# error: [invalid-type-form]
+reveal_type(cast(1, True))  # revealed: Unknown
+
+# error: [missing-argument] "No argument provided for required parameter `val` of function `cast`"
+cast(str)
+# error: [too-many-positional-arguments] "Too many positional arguments to function `cast`: expected 2, got 3"
+cast(str, b"ar", "foo")
+
+def function_returning_int() -> int:
+    return 10
+
+# error: [redundant-cast] "Value is already of type `int`"
+cast(int, function_returning_int())
+
+def function_returning_any() -> Any:
+    return "blah"
+
+# error: [redundant-cast] "Value is already of type `Any`"
+cast(Any, function_returning_any())
+```
+
+Complex type expressions (which may be unsupported) do not lead to spurious `[redundant-cast]`
+diagnostics.
+
+```py
+from typing import Callable
+
+def f(x: Callable[[dict[str, int]], None], y: tuple[dict[str, int]]):
+    a = cast(Callable[[list[bytes]], None], x)
+    b = cast(tuple[list[bytes]], y)
+```
+
+A cast from `Todo` or `Unknown` to `Any` is not considered a "redundant cast": even if these are
+understood as gradually equivalent types by ty, they are understood as different types by human
+readers of ty's output. For `Unknown` in particular, we may consider it differently in the context
+of some opt-in diagnostics, as it indicates that the gradual type has come about due to an invalid
+annotation, missing annotation or missing type argument somewhere.
+
+```py
+from ty_extensions import Unknown
+
+def f(x: Any, y: Unknown, z: Any | str | int):
+    a = cast(dict[str, Any], x)
+    reveal_type(a)  # revealed: dict[str, Any]
+
+    b = cast(Any, y)
+    reveal_type(b)  # revealed: Any
+
+    c = cast(str | int | Any, z)  # error: [redundant-cast]
+```