From 3ef117ed95f24d581028f0076c6e44180fbaba51 Mon Sep 17 00:00:00 2001
From: Alex Waygood <alex.waygood@gmail.com>
Date: Tue, 30 Sep 2025 17:44:34 +0100
Subject: [PATCH] [ty] Fix simplification of `T & ~T` for non-fully-static
 types

---
 .../resources/mdtest/intersection_types.md    | 49 +++++++++++++++++++
 .../ty_python_semantic/src/types/builder.rs   | 11 +++++
 2 files changed, 60 insertions(+)

diff --git a/crates/ty_python_semantic/resources/mdtest/intersection_types.md b/crates/ty_python_semantic/resources/mdtest/intersection_types.md
index 0f5b37eb88..f124bd973d 100644
--- a/crates/ty_python_semantic/resources/mdtest/intersection_types.md
+++ b/crates/ty_python_semantic/resources/mdtest/intersection_types.md
@@ -907,6 +907,11 @@ def unknown(
 Dynamic types do not cancel each other out. Intersecting an unknown set of values with the negation
 of another unknown set of values is not necessarily empty, so we keep the positive contribution:
 
+```toml
+[environment]
+python-version = "3.12"
+```
+
 ```py
 from typing import Any
 from ty_extensions import Intersection, Not, Unknown
@@ -924,6 +929,50 @@ def unknown(
 ) -> None:
     reveal_type(i1)  # revealed: Unknown
     reveal_type(i2)  # revealed: Unknown
+
+class Covariant[T]:
+    def get(self) -> T:
+        raise NotImplementedError
+
+def covariant(
+    i1: Intersection[Covariant[Any], Not[Covariant[Any]]],
+    i2: Intersection[Not[Covariant[Any]], Covariant[Any]],
+) -> None:
+    reveal_type(i1)  # revealed: Covariant[Any]
+    reveal_type(i2)  # revealed: Covariant[Any]
+
+class Contravariant[T]:
+    def receive(self, input: T): ...
+
+def contravariant(
+    i1: Intersection[Contravariant[Any], Not[Contravariant[Any]]],
+    i2: Intersection[Not[Contravariant[Any]], Contravariant[Any]],
+) -> None:
+    reveal_type(i1)  # revealed: Contravariant[Any]
+    reveal_type(i2)  # revealed: Contravariant[Any]
+
+class Invariant[T]:
+    mutable_attribute: T
+
+def invariant(
+    i1: Intersection[Invariant[Any], Not[Invariant[Any]]],
+    i2: Intersection[Not[Invariant[Any]], Invariant[Any]],
+) -> None:
+    reveal_type(i1)  # revealed: Invariant[Any]
+    reveal_type(i2)  # revealed: Invariant[Any]
+
+class Bivariant[T]: ...
+
+# Because of bivariance, the specialisation here is meaningless;
+# `Bivariant[Any]` is arguably still a fully static type, even
+# though it is specialised with a gradual form! Thus self-cancellation
+# here is fine:
+def bivariant(
+    i1: Intersection[Bivariant[Any], Not[Bivariant[Any]]],
+    i2: Intersection[Not[Bivariant[Any]], Bivariant[Any]],
+) -> None:
+    reveal_type(i1)  # revealed: Never
+    reveal_type(i2)  # revealed: Never
 ```
 
 ### Mixed dynamic types
diff --git a/crates/ty_python_semantic/src/types/builder.rs b/crates/ty_python_semantic/src/types/builder.rs
index 556edcb368..7b53a75b40 100644
--- a/crates/ty_python_semantic/src/types/builder.rs
+++ b/crates/ty_python_semantic/src/types/builder.rs
@@ -958,6 +958,12 @@ impl<'db> InnerIntersectionBuilder<'db> {
                         self.positive.insert(Type::Never);
                         return;
                     }
+                    // `T & ~T` = `T` if `T` is not a subtype of `T`
+                    // (this can only be true if `T` is a non-fully-static type)
+                    if existing_negative.is_equivalent_to(db, new_positive) {
+                        to_remove.push(index);
+                        continue;
+                    }
                     // A & ~B = A    if A and B are disjoint
                     if existing_negative.is_disjoint_from(db, new_positive) {
                         to_remove.push(index);
@@ -1048,6 +1054,11 @@ impl<'db> InnerIntersectionBuilder<'db> {
                         self.positive.insert(Type::Never);
                         return;
                     }
+                    // `T & ~T` = `T` if `T` is not a subtype of `T`
+                    // (this can only be true if `T` is a non-fully-static type)
+                    if existing_positive.is_equivalent_to(db, new_negative) {
+                        return;
+                    }
                     // A & ~B = A    if A and B are disjoint
                     if existing_positive.is_disjoint_from(db, new_negative) {
                         return;