[red-knot] add test cases result in false positive errors (#16856)

## Summary

From #16641

The previous PR attempted to fix the errors presented in this PR, but as
discussed in the conversation, it was concluded that the approach was
undesirable and that further work would be needed to fix the errors with
a correct general solution.

In this PR, I instead add the test cases from the previous PR as TODOs,
as a starting point for future work.

## Test Plan

---------

Co-authored-by: Carl Meyer <[email protected]>

Author: mtshiba

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,19 @@ 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],
+):
+    # TODO: This should be `Never`
+    reveal_type(a)  # revealed: Literal[True]
+    # TODO: This should be `Never`
+    reveal_type(b)  # revealed: Literal[False]
+    reveal_type(c)  # revealed: Never
+    reveal_type(d)  # revealed: Never
 ```
 
 ## Simplification of `LiteralString`, `AlwaysTruthy` and `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,22 @@ 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))
+
+# TODO: No errors
+# error: [static-assert-error]
+static_assert(is_assignable_to(bool, Literal[False] | AlwaysTruthy))
+# error: [static-assert-error]
+static_assert(is_assignable_to(bool, Literal[True] | AlwaysFalsy))
+# error: [static-assert-error]
+static_assert(is_assignable_to(LiteralString, Literal[""] | AlwaysTruthy))
+static_assert(not is_assignable_to(Literal[True] | AlwaysFalsy, Literal[False] | 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 +305,19 @@ 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]]))
+
+# TODO: No errors
+# The condition `is_assignable_to(T & U, U)` should still be satisfied after the following transformations:
+# `LiteralString & AlwaysTruthy` -> `LiteralString & ~Literal[""]`
+# error: [static-assert-error]
+static_assert(is_assignable_to(Intersection[LiteralString, Not[Literal[""]]], AlwaysTruthy))
+# error: [static-assert-error]
+static_assert(is_assignable_to(Intersection[LiteralString, Not[Literal["", "a"]]], AlwaysTruthy))
+# `LiteralString & ~AlwaysFalsy`  -> `LiteralString & ~Literal[""]`
+# error: [static-assert-error]
+static_assert(is_assignable_to(Intersection[LiteralString, Not[Literal[""]]], Not[AlwaysFalsy]))
+# error: [static-assert-error]
+static_assert(is_assignable_to(Intersection[LiteralString, Not[Literal["", "a"]]], Not[AlwaysFalsy]))
 ```
 
 ## General properties

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

@@ -196,7 +196,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 +223,25 @@ 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))
+
+# TODO: No errors
+# error: [static-assert-error]
+static_assert(is_disjoint_from(AlwaysFalsy, Intersection[LiteralString, Not[Literal[""]]]))
+# error: [static-assert-error]
+static_assert(is_disjoint_from(Intersection[Not[Literal[True]], Not[Literal[False]]], bool))
+# error: [static-assert-error]
+static_assert(is_disjoint_from(Intersection[AlwaysFalsy, Not[Literal[False]]], bool))
+# error: [static-assert-error]
+static_assert(is_disjoint_from(Intersection[AlwaysTruthy, Not[Literal[True]]], bool))
+
+# TODO: No errors
+# The condition `is_disjoint(T, Not[T])` must still be satisfied after the following transformations:
+# `LiteralString & AlwaysTruthy` -> `LiteralString & ~Literal[""]`
+# error: [static-assert-error]
+static_assert(is_disjoint_from(Intersection[LiteralString, AlwaysTruthy], Not[LiteralString] | AlwaysFalsy))
+# `LiteralString & ~AlwaysFalsy`  -> `LiteralString & ~Literal[""]`
+# error: [static-assert-error]
+static_assert(is_disjoint_from(Intersection[LiteralString, Not[AlwaysFalsy]], Not[LiteralString] | AlwaysFalsy))
 ```
 
 ### Class, module and function literals

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

@@ -46,6 +46,12 @@ static_assert(is_gradual_equivalent_to(Intersection[str | int, Not[type[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))
+
+# TODO: No errors
+# error: [static-assert-error]
+static_assert(is_gradual_equivalent_to(Unknown, Unknown | Any))
+# error: [static-assert-error]
+static_assert(is_gradual_equivalent_to(Unknown, Intersection[Unknown, Any]))
 ```
 
 ## Tuples

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

@@ -276,8 +276,8 @@ static_assert(is_subtype_of(Never, AlwaysFalsy))
 ### `AlwaysTruthy` and `AlwaysFalsy`
 
 ```py
-from knot_extensions import AlwaysTruthy, AlwaysFalsy, is_subtype_of, static_assert
-from typing import Literal
+from knot_extensions import AlwaysTruthy, AlwaysFalsy, Intersection, Not, is_subtype_of, static_assert
+from typing_extensions import Literal, LiteralString
 
 static_assert(is_subtype_of(Literal[1], AlwaysTruthy))
 static_assert(is_subtype_of(Literal[0], AlwaysFalsy))
@@ -290,6 +290,28 @@ 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))
+
+# TODO: No errors
+# error: [static-assert-error]
+static_assert(is_subtype_of(bool, Literal[False] | AlwaysTruthy))
+# error: [static-assert-error]
+static_assert(is_subtype_of(bool, Literal[True] | AlwaysFalsy))
+# error: [static-assert-error]
+static_assert(is_subtype_of(LiteralString, Literal[""] | AlwaysTruthy))
+static_assert(not is_subtype_of(Literal[True] | AlwaysFalsy, Literal[False] | AlwaysTruthy))
+
+# TODO: No errors
+# The condition `is_subtype_of(T & U, U)` must still be satisfied after the following transformations:
+# `LiteralString & AlwaysTruthy` -> `LiteralString & ~Literal[""]`
+# error: [static-assert-error]
+static_assert(is_subtype_of(Intersection[LiteralString, Not[Literal[""]]], AlwaysTruthy))
+# error: [static-assert-error]
+static_assert(is_subtype_of(Intersection[LiteralString, Not[Literal["", "a"]]], AlwaysTruthy))
+# `LiteralString & ~AlwaysFalsy` -> `LiteralString & ~Literal[""]`
+# error: [static-assert-error]
+static_assert(is_subtype_of(Intersection[LiteralString, Not[Literal[""]]], Not[AlwaysFalsy]))
+# error: [static-assert-error]
+static_assert(is_subtype_of(Intersection[LiteralString, Not[Literal["", "a"]]], Not[AlwaysFalsy]))
 ```
 
 ### Module literals