[red-knot] T is disjoint from ~T

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

@@ -132,6 +132,27 @@ static_assert(not is_disjoint_from(Intersection[X, Z], Y))
 static_assert(not is_disjoint_from(Intersection[Y, Z], X))
 ```
 
+## Negation / complement
+
+The complement of a type `T` is disjoint from `T`. In fact, it is disjoint from every subtype of
+`T`:
+
+```py
+from knot_extensions import Not, Intersection, is_disjoint_from, static_assert
+
+class T: ...
+class S(T): ...
+
+static_assert(is_disjoint_from(Not[T], T))
+static_assert(is_disjoint_from(Not[T], S))
+
+static_assert(is_disjoint_from(Intersection[T, Any], Not[T]))
+static_assert(is_disjoint_from(Not[T], Intersection[T, Any]))
+
+static_assert(is_disjoint_from(Intersection[S, Any], Not[T]))
+static_assert(is_disjoint_from(Not[T], Intersection[S, Any]))
+```
+
 ## Special types
 
 ### `Never`
@@ -244,7 +265,7 @@ static_assert(not is_disjoint_from(TypeOf[f], object))
 ### `AlwaysTruthy` and `AlwaysFalsy`
 
 ```py
-from knot_extensions import AlwaysFalsy, AlwaysTruthy, is_disjoint_from, static_assert
+from knot_extensions import AlwaysFalsy, AlwaysTruthy, Intersection, Not, is_disjoint_from, static_assert
 from typing import Literal
 
 static_assert(is_disjoint_from(None, AlwaysTruthy))
@@ -256,6 +277,14 @@ static_assert(not is_disjoint_from(str, AlwaysTruthy))
 
 static_assert(is_disjoint_from(Literal[1, 2], AlwaysFalsy))
 static_assert(not is_disjoint_from(Literal[0, 1], AlwaysTruthy))
+
+type Truthy = Not[AlwaysFalsy]
+type Falsy = Not[AlwaysTruthy]
+
+type AmbiguousTruthiness = Intersection[Truthy, Falsy]
+
+static_assert(is_disjoint_from(AlwaysTruthy, AmbiguousTruthiness))
+static_assert(is_disjoint_from(AlwaysFalsy, AmbiguousTruthiness))
 ```
 
 ### Instance types versus `type[T]` types

crates/red_knot_python_semantic/src/types.rs

@@ -1261,19 +1261,42 @@ impl<'db> Type<'db> {
                 .iter()
                 .all(|e| e.is_disjoint_from(db, other)),
 
-            (Type::Intersection(intersection), other)
+            (Type::Intersection(inter_left), Type::Intersection(inter_right)) => {
-            | (other, Type::Intersection(intersection)) => {
+                // We explicitly make this case a symmetric version of the case below, as there
-                if intersection
+                // are some type pairs like `Any & T` and `~T` that would otherwise lead to non-
+                // symmetric results.
+                inter_left
                     .positive(db)
                     .iter()
                     .any(|p| p.is_disjoint_from(db, other))
-                {
+                    || inter_right
-                    true
+                        .positive(db)
-                } else {
+                        .iter()
-                    // TODO we can do better here. For example:
+                        .any(|p| p.is_disjoint_from(db, self))
-                    // X & ~Literal[1] is disjoint from Literal[1]
+                    || inter_left.negative(db).iter().any(|n| {
-                    false
+                        other.is_subtype_of(db, *n)
-                }
+                            && self.is_fully_static(db)
+                            && other.is_fully_static(db)
+                    })
+                    || inter_right.negative(db).iter().any(|n| {
+                        self.is_subtype_of(db, *n)
+                            && self.is_fully_static(db)
+                            && other.is_fully_static(db)
+                    })
+            }
+            (Type::Intersection(intersection), t) | (t, Type::Intersection(intersection)) => {
+                // TODO: There are certainly more cases that could be handled here. For example,
+                // it is possible that both A and B overlap with C, but the intersection A & B
+                // does not overlap with C.
+                intersection
+                    .positive(db)
+                    .iter()
+                    .any(|p| p.is_disjoint_from(db, t))
+                    || intersection.negative(db).iter().any(|n| {
+                        t.is_subtype_of(db, *n)
+                            && self.is_fully_static(db)
+                            && other.is_fully_static(db)
+                    })
             }
 
             // any single-valued type is disjoint from another single-valued type