Stabilize all_type_pairs_can_be_assigned_from_their_intersection

crates/red_knot_python_semantic/resources/mdtest/intersection_types.md

@@ -663,6 +663,7 @@ to the fact that `bool` is a `@final` class at runtime that cannot be subclassed
 
 ```py
 from knot_extensions import Intersection, Not, AlwaysTruthy, AlwaysFalsy
+from typing_extensions import Literal
 
 class P: ...
 
@@ -686,6 +687,17 @@ def f(
     reveal_type(f)  # revealed: Never
     reveal_type(g)  # revealed: Never
     reveal_type(h)  # revealed: Never
+
+def never(
+    a: Intersection[Intersection[AlwaysFalsy, Not[Literal[False]]], bool],
+    b: Intersection[Intersection[AlwaysTruthy, Not[Literal[True]]], bool],
+    c: Intersection[Intersection[Literal[True], Not[AlwaysTruthy]], bool],
+    d: Intersection[Intersection[Literal[False], Not[AlwaysFalsy]], bool],
+):
+    reveal_type(a)  # revealed: Never
+    reveal_type(b)  # revealed: Never
+    reveal_type(c)  # revealed: Never
+    reveal_type(d)  # revealed: Never
 ```
 
 ## Simplification of `LiteralString`, `AlwaysTruthy` and `AlwaysFalsy`

crates/red_knot_python_semantic/resources/mdtest/type_api.md

@@ -111,7 +111,11 @@ from typing_extensions import Literal
 from knot_extensions import AlwaysFalsy, AlwaysTruthy, is_subtype_of, static_assert
 
 static_assert(is_subtype_of(Literal[True], AlwaysTruthy))
+static_assert(is_subtype_of(Literal["a"], AlwaysTruthy))
+static_assert(is_subtype_of(Literal[1], AlwaysTruthy))
 static_assert(is_subtype_of(Literal[False], AlwaysFalsy))
+static_assert(is_subtype_of(Literal[""], AlwaysFalsy))
+static_assert(is_subtype_of(Literal[0], AlwaysFalsy))
 
 static_assert(not is_subtype_of(int, AlwaysFalsy))
 static_assert(not is_subtype_of(str, AlwaysFalsy))

crates/red_knot_python_semantic/resources/mdtest/type_properties/is_assignable_to.md

@@ -206,8 +206,8 @@ static_assert(not is_assignable_to(tuple[Any, Literal[2]], tuple[int, str]))
 ## Union types
 
 ```py
-from knot_extensions import static_assert, is_assignable_to, Unknown
-from typing import Literal, Any
+from knot_extensions import AlwaysTruthy, AlwaysFalsy, static_assert, is_assignable_to, Unknown
+from typing_extensions import Literal, Any, LiteralString
 
 static_assert(is_assignable_to(int, int | str))
 static_assert(is_assignable_to(str, int | str))
@@ -227,13 +227,18 @@ static_assert(not is_assignable_to(int | None, str | None))
 static_assert(not is_assignable_to(Literal[1] | None, int))
 static_assert(not is_assignable_to(Literal[1] | None, str | None))
 static_assert(not is_assignable_to(Any | int | str, int))
+
+static_assert(is_assignable_to(bool, Literal[False] | AlwaysTruthy))
+static_assert(is_assignable_to(bool, Literal[True] | AlwaysFalsy))
+static_assert(not is_assignable_to(Literal[True] | AlwaysFalsy, Literal[False] | AlwaysTruthy))
+static_assert(is_assignable_to(LiteralString, Literal[""] | AlwaysTruthy))
 ```
 
 ## Intersection types
 
 ```py
-from knot_extensions import static_assert, is_assignable_to, Intersection, Not
-from typing_extensions import Any, Literal
+from knot_extensions import static_assert, is_assignable_to, Intersection, Not, AlwaysTruthy, AlwaysFalsy
+from typing_extensions import Any, Literal, final, LiteralString
 
 class Parent: ...
 class Child1(Parent): ...
@@ -296,6 +301,30 @@ static_assert(is_assignable_to(Intersection[Any, Unrelated], Intersection[Any, P
 static_assert(is_assignable_to(Intersection[Any, Parent, Unrelated], Intersection[Any, Parent, Unrelated]))
 static_assert(is_assignable_to(Intersection[Unrelated, Any], Intersection[Unrelated, Not[Any]]))
 static_assert(is_assignable_to(Intersection[Literal[1], Any], Intersection[Unrelated, Not[Any]]))
+
+static_assert(is_assignable_to(Intersection[Unrelated, Not[int]], Not[int]))
+static_assert(is_assignable_to(Intersection[Intersection[str, Not[Literal[""]]], int], Intersection[str, Not[Literal[""]]]))
+static_assert(is_assignable_to(Intersection[Intersection[Any, Not[int]], Not[str]], Intersection[Any, Not[int]]))
+
+# The condition `is_assignable_to(T & U, U)` should still be satisfied after the following transformations:
+# `LiteralString & AlwaysTruthy` -> `LiteralString & ~Literal[""]`
+static_assert(is_assignable_to(Intersection[LiteralString, Not[Literal[""]]], AlwaysTruthy))
+static_assert(is_assignable_to(Intersection[LiteralString, Not[Literal["", "a"]]], AlwaysTruthy))
+# `LiteralString & ~AlwaysTruthy` -> `Literal[""]`
+static_assert(is_assignable_to(Literal[""], Not[AlwaysTruthy]))
+static_assert(not is_assignable_to(Literal["", "a"], Not[AlwaysTruthy]))
+# `LiteralString & AlwaysFalsy` -> `Literal[""]`
+static_assert(is_assignable_to(Literal[""], AlwaysFalsy))
+static_assert(not is_assignable_to(Literal["", "a"], AlwaysFalsy))
+# `LiteralString & ~AlwaysFalsy`  -> `LiteralString & ~Literal[""]`
+static_assert(is_assignable_to(Intersection[LiteralString, Not[Literal[""]]], Not[AlwaysFalsy]))
+static_assert(is_assignable_to(Intersection[LiteralString, Not[Literal["", "a"]]], Not[AlwaysFalsy]))
+# `bool & ~AlwaysTruthy`, `bool & ~Literal[True]` -> `Literal[False]`
+static_assert(is_assignable_to(Literal[False], Not[AlwaysTruthy]))
+static_assert(is_assignable_to(Literal[False], Not[Literal[True]]))
+# `bool & ~AlwaysFalsy`, `bool & ~Literal[False]` -> `Literal[True]`
+static_assert(is_assignable_to(Literal[True], Not[AlwaysFalsy]))
+static_assert(is_assignable_to(Literal[True], Not[Literal[False]]))
 ```
 
 ## General properties

crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md

@@ -27,7 +27,7 @@ static_assert(not is_disjoint_from(str, type[Any]))
 ## Class hierarchies
 
 ```py
-from knot_extensions import is_disjoint_from, static_assert, Intersection, is_subtype_of
+from knot_extensions import Intersection, Not, is_disjoint_from, static_assert, is_subtype_of
 from typing import final
 
 class A: ...
@@ -56,6 +56,10 @@ static_assert(not is_disjoint_from(FinalSubclass, A))
 # ... which makes it disjoint from B1, B2:
 static_assert(is_disjoint_from(B1, FinalSubclass))
 static_assert(is_disjoint_from(B2, FinalSubclass))
+
+static_assert(is_disjoint_from(B1, Not[B1]))
+static_assert(is_disjoint_from(C, Intersection[A, Not[B1]]))
+static_assert(is_disjoint_from(Intersection[A, Not[B1]], C))
 ```
 
 ## Tuple types
@@ -196,7 +200,7 @@ static_assert(is_disjoint_from(None, Intersection[int, Not[str]]))
 
 ```py
 from typing_extensions import Literal, LiteralString
-from knot_extensions import TypeOf, is_disjoint_from, static_assert
+from knot_extensions import Intersection, Not, TypeOf, is_disjoint_from, static_assert, AlwaysFalsy, AlwaysTruthy
 
 static_assert(is_disjoint_from(Literal[True], Literal[False]))
 static_assert(is_disjoint_from(Literal[True], Literal[1]))
@@ -223,6 +227,35 @@ static_assert(not is_disjoint_from(Literal[1], Literal[1]))
 static_assert(not is_disjoint_from(Literal["a"], Literal["a"]))
 static_assert(not is_disjoint_from(Literal["a"], LiteralString))
 static_assert(not is_disjoint_from(Literal["a"], str))
+
+static_assert(is_disjoint_from(Intersection[str, Not[Literal["a"]]], Literal["a"]))
+static_assert(is_disjoint_from(Intersection[str, Not[Literal["a", "b"]]], Literal["a"]))
+static_assert(not is_disjoint_from(Intersection[str, Not[Literal["a"]]], Literal["b"]))
+
+static_assert(is_disjoint_from(AlwaysFalsy, Intersection[LiteralString, Not[Literal[""]]]))
+static_assert(is_disjoint_from(AlwaysTruthy, Literal[""]))
+
+static_assert(is_disjoint_from(Intersection[Not[Literal[True]], Not[Literal[False]]], bool))
+static_assert(is_disjoint_from(Intersection[AlwaysFalsy, Not[Literal[False]]], bool))
+static_assert(is_disjoint_from(Intersection[AlwaysTruthy, Not[Literal[True]]], bool))
+static_assert(is_disjoint_from(Intersection[Literal[True], Not[AlwaysTruthy]], bool))
+static_assert(is_disjoint_from(Intersection[Literal[False], Not[AlwaysFalsy]], bool))
+
+# The condition `is_disjoint(T, Not[T])` must still be satisfied after the following transformations:
+# `LiteralString & AlwaysTruthy` -> `LiteralString & ~Literal[""]`
+static_assert(is_disjoint_from(Intersection[LiteralString, AlwaysTruthy], Not[LiteralString] | AlwaysFalsy))
+# `LiteralString & ~AlwaysTruthy` -> `LiteralString & Literal[""]`
+static_assert(is_disjoint_from(Intersection[LiteralString, Not[AlwaysTruthy]], Not[LiteralString] | AlwaysTruthy))
+# `bool & ~AlwaysTruthy`, `bool & ~Literal[True]` -> `bool & Literal[False]`
+static_assert(is_disjoint_from(Intersection[bool, Not[AlwaysTruthy]], Not[bool] | AlwaysTruthy))
+static_assert(is_disjoint_from(Intersection[bool, Not[Literal[True]]], Not[bool] | Literal[True]))
+# `LiteralString & AlwaysFalsy` -> `LiteralString & Literal[""]`
+static_assert(is_disjoint_from(Intersection[LiteralString, AlwaysFalsy], Not[LiteralString] | AlwaysTruthy))
+# `LiteralString & ~AlwaysFalsy`  -> `LiteralString & ~Literal[""]`
+static_assert(is_disjoint_from(Intersection[LiteralString, Not[AlwaysFalsy]], Not[LiteralString] | AlwaysFalsy))
+# `bool & ~AlwaysFalsy`, `bool & ~Literal[False]` -> `bool & Literal[True]`
+static_assert(is_disjoint_from(Intersection[bool, Not[AlwaysFalsy]], Not[bool] | AlwaysFalsy))
+static_assert(is_disjoint_from(Intersection[bool, Not[Literal[False]]], Not[bool] | Literal[False]))
 ```
 
 ### Class, module and function literals

crates/red_knot_python_semantic/resources/mdtest/type_properties/is_equivalent_to.md

@@ -118,4 +118,26 @@ class R: ...
 static_assert(is_equivalent_to(Intersection[tuple[P | Q], R], Intersection[tuple[Q | P], R]))
 ```
 
+## Transformation by intersection
+
+```py
+from knot_extensions import Intersection, Not, AlwaysTruthy, AlwaysFalsy, static_assert, is_equivalent_to
+from typing_extensions import Literal, LiteralString
+
+# `LiteralString & AlwaysTruthy` -> `LiteralString & ~Literal[""]`
+static_assert(is_equivalent_to(Intersection[LiteralString, AlwaysTruthy], Intersection[LiteralString, Not[Literal[""]]]))
+# `LiteralString & ~AlwaysTruthy` -> `Literal[""]`
+static_assert(is_equivalent_to(Intersection[LiteralString, Not[AlwaysTruthy]], Literal[""]))
+# `LiteralString & AlwaysFalsy` -> `Literal[""]`
+static_assert(is_equivalent_to(Intersection[LiteralString, AlwaysFalsy], Literal[""]))
+# `LiteralString & ~AlwaysFalsy`  -> `LiteralString & ~Literal[""]`
+static_assert(is_equivalent_to(Intersection[LiteralString, Not[AlwaysFalsy]], Intersection[LiteralString, Not[Literal[""]]]))
+# `bool & ~AlwaysFalsy`, `bool & ~Literal[False]` -> `bool & Literal[True]`
+static_assert(is_equivalent_to(Intersection[bool, Not[AlwaysFalsy]], Literal[True]))
+static_assert(is_equivalent_to(Intersection[bool, Not[Literal[False]]], Literal[True]))
+# `bool & ~AlwaysTruthy`, `bool & ~Literal[True]` -> `bool & Literal[False]`
+static_assert(is_equivalent_to(Intersection[bool, Not[AlwaysTruthy]], Literal[False]))
+static_assert(is_equivalent_to(Intersection[bool, Not[Literal[True]]], Literal[False]))
+```
+
 [the equivalence relation]: https://typing.readthedocs.io/en/latest/spec/glossary.html#term-equivalent

crates/red_knot_python_semantic/resources/mdtest/type_properties/is_gradual_equivalent_to.md

@@ -42,9 +42,9 @@ static_assert(is_gradual_equivalent_to(str | int, int | str))
 static_assert(
     is_gradual_equivalent_to(Intersection[str, int, Not[bytes], Not[None]], Intersection[int, str, Not[None], Not[bytes]])
 )
-# TODO: `~type[Any]` shoudld be gradually equivalent to `~type[Unknown]`
-# error: [static-assert-error]
 static_assert(is_gradual_equivalent_to(Intersection[str | int, Not[type[Any]]], Intersection[int | str, Not[type[Unknown]]]))
+static_assert(is_gradual_equivalent_to(Unknown, Unknown | Any))
+static_assert(is_gradual_equivalent_to(Unknown, Intersection[Unknown, Any]))
 
 static_assert(not is_gradual_equivalent_to(str | int, int | str | bytes))
 static_assert(not is_gradual_equivalent_to(str | int | bytes, int | str | dict))

crates/red_knot_python_semantic/resources/mdtest/type_properties/is_subtype_of.md

@@ -276,8 +276,9 @@ static_assert(is_subtype_of(Never, AlwaysFalsy))
 ### `AlwaysTruthy` and `AlwaysFalsy`
 
 ```py
-from knot_extensions import AlwaysTruthy, AlwaysFalsy, is_subtype_of, static_assert
+from knot_extensions import AlwaysTruthy, AlwaysFalsy, Intersection, Not, is_subtype_of, static_assert
 from typing import Literal
+from typing_extensions import LiteralString
 
 static_assert(is_subtype_of(Literal[1], AlwaysTruthy))
 static_assert(is_subtype_of(Literal[0], AlwaysFalsy))
@@ -290,6 +291,31 @@ static_assert(not is_subtype_of(Literal[0], AlwaysTruthy))
 
 static_assert(not is_subtype_of(str, AlwaysTruthy))
 static_assert(not is_subtype_of(str, AlwaysFalsy))
+
+static_assert(is_subtype_of(bool, Literal[False] | AlwaysTruthy))
+static_assert(is_subtype_of(bool, Literal[True] | AlwaysFalsy))
+static_assert(not is_subtype_of(Literal[True] | AlwaysFalsy, Literal[False] | AlwaysTruthy))
+static_assert(is_subtype_of(LiteralString, Literal[""] | AlwaysTruthy))
+
+# The condition `is_subtype_of(T & U, U)` must still be satisfied after the following transformations:
+# `LiteralString & AlwaysTruthy` -> `LiteralString & ~Literal[""]`
+static_assert(is_subtype_of(Intersection[LiteralString, Not[Literal[""]]], AlwaysTruthy))
+static_assert(is_subtype_of(Intersection[LiteralString, Not[Literal["", "a"]]], AlwaysTruthy))
+# `LiteralString & ~AlwaysTruthy` -> `Literal[""]`
+static_assert(is_subtype_of(Literal[""], Not[AlwaysTruthy]))
+static_assert(not is_subtype_of(Literal["", "a"], Not[AlwaysTruthy]))
+# `LiteralString & AlwaysFalsy` -> `Literal[""]`
+static_assert(is_subtype_of(Literal[""], AlwaysFalsy))
+static_assert(not is_subtype_of(Literal["", "a"], AlwaysFalsy))
+# `LiteralString & ~AlwaysFalsy` -> `LiteralString & ~Literal[""]`
+static_assert(is_subtype_of(Intersection[LiteralString, Not[Literal[""]]], Not[AlwaysFalsy]))
+static_assert(is_subtype_of(Intersection[LiteralString, Not[Literal["", "a"]]], Not[AlwaysFalsy]))
+# `bool & ~AlwaysTruthy`, `bool & ~Literal[True]` -> `Literal[False]`
+static_assert(is_subtype_of(Literal[False], Not[AlwaysTruthy]))
+static_assert(is_subtype_of(Literal[False], Not[Literal[True]]))
+# `bool & ~AlwaysFalsy`, `bool & ~Literal[False]` -> `Literal[True]`
+static_assert(is_subtype_of(Literal[True], Not[AlwaysFalsy]))
+static_assert(is_subtype_of(Literal[True], Not[Literal[False]]))
 ```
 
 ### Module literals