From 7e5358de2be60ec7ae176e14f451c859dec5a110 Mon Sep 17 00:00:00 2001
From: David Peter <mail@david-peter.de>
Date: Mon, 10 Feb 2025 22:15:47 +0100
Subject: [PATCH] [red-knot] T is disjoint from ~T

---
 .../type_properties/is_disjoint_from.md       | 31 ++++++++++++-
 crates/red_knot_python_semantic/src/types.rs  | 43 ++++++++++++++-----
 2 files changed, 63 insertions(+), 11 deletions(-)

diff --git a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md
index d88100e8b4..274235d8ac 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md
+++ b/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
diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs
index d9d8ac2e9e..133a112281 100644
--- a/crates/red_knot_python_semantic/src/types.rs
+++ b/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)
-            | (other, Type::Intersection(intersection)) => {
-                if intersection
+            (Type::Intersection(inter_left), Type::Intersection(inter_right)) => {
+                // We explicitly make this case a symmetric version of the case below, as there
+                // 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))
-                {
-                    true
-                } else {
-                    // TODO we can do better here. For example:
-                    // X & ~Literal[1] is disjoint from Literal[1]
-                    false
-                }
+                    || inter_right
+                        .positive(db)
+                        .iter()
+                        .any(|p| p.is_disjoint_from(db, self))
+                    || inter_left.negative(db).iter().any(|n| {
+                        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