From a012e28216e232f39c2bd4ba94249b2cf8f71b57 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Tue, 11 Nov 2025 16:53:09 -0500
Subject: [PATCH] BLAMMO

---
 .../type_properties/implies_subtype_of.md     |  4 ---
 .../src/types/constraints.rs                  | 25 +++++++++++----
 .../src/types/signatures.rs                   | 31 +++++++++++++++++++
 3 files changed, 50 insertions(+), 10 deletions(-)

diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md b/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md
index a3c682917d..054c2115c2 100644
--- a/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md
+++ b/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md
@@ -387,11 +387,7 @@ def unrelated[T]():
     # Note that even though this typevar is also named T, it is not the same typevar as T@identity!
     constraints = ConstraintSet.range(bool, T, int)
 
-    # TODO: no error
-    # error: [static-assert-error]
     static_assert(constraints.implies_subtype_of(TypeOf[identity], Callable[[int], int]))
-    # TODO: no error
-    # error: [static-assert-error]
     static_assert(constraints.implies_subtype_of(TypeOf[identity], Callable[[str], str]))
     static_assert(not constraints.implies_subtype_of(TypeOf[identity], Callable[[str], int]))
 
diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 9fd6af9667..232f66abda 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -296,18 +296,16 @@ impl<'db> ConstraintSet<'db> {
     /// Updates this constraint set to hold the union of itself and another constraint set.
     /// XXX: Document not commutative
     pub(crate) fn union(&mut self, db: &'db dyn Db, other: Self) -> Self {
-        let to_abstract = other.inferable.subtract(db, self.inferable);
-        let other = other.node.exists(db, to_abstract);
-        self.node = self.node.or(db, other);
+        let other = other.reduce_inferable(db, self.inferable);
+        self.node = self.node.or(db, other.node);
         *self
     }
 
     /// Updates this constraint set to hold the intersection of itself and another constraint set.
     /// XXX: Document not commutative
     pub(crate) fn intersect(&mut self, db: &'db dyn Db, other: Self) -> Self {
-        let to_abstract = other.inferable.subtract(db, self.inferable);
-        let other = other.node.exists(db, to_abstract);
-        self.node = self.node.and(db, other);
+        let other = other.reduce_inferable(db, self.inferable);
+        self.node = self.node.and(db, other.node);
         *self
     }
 
@@ -351,6 +349,21 @@ impl<'db> ConstraintSet<'db> {
         }
     }
 
+    /// Reduces the set of inferable typevars for this constraint set. Any typevars that were
+    /// previously inferable but aren't in the new inferable set will be existentially quantified
+    /// away. (That is, those typevars will be removed from the constraint set, and the constraint
+    /// set will return true whenever there was _any_ specialization of those typevars that
+    /// returned true before.)
+    pub(crate) fn reduce_inferable(
+        self,
+        db: &'db dyn Db,
+        inferable: InferableTypeVars<'db>,
+    ) -> Self {
+        let to_abstract = self.inferable.subtract(db, inferable);
+        let node = self.node.exists(db, to_abstract);
+        Self { node, inferable }
+    }
+
     pub(crate) fn range(
         db: &'db dyn Db,
         lower: Type<'db>,
diff --git a/crates/ty_python_semantic/src/types/signatures.rs b/crates/ty_python_semantic/src/types/signatures.rs
index 6fbb7055ce..3161f156d4 100644
--- a/crates/ty_python_semantic/src/types/signatures.rs
+++ b/crates/ty_python_semantic/src/types/signatures.rs
@@ -650,6 +650,17 @@ impl<'db> Signature<'db> {
         other: &Signature<'db>,
         inferable: InferableTypeVars<'db>,
         visitor: &IsEquivalentVisitor<'db>,
+    ) -> ConstraintSet<'db> {
+        self.is_equivalent_to_inner(db, other, inferable, visitor)
+            .reduce_inferable(db, inferable)
+    }
+
+    fn is_equivalent_to_inner(
+        &self,
+        db: &'db dyn Db,
+        other: &Signature<'db>,
+        inferable: InferableTypeVars<'db>,
+        visitor: &IsEquivalentVisitor<'db>,
     ) -> ConstraintSet<'db> {
         // The typevars in self and other should also be considered inferable when checking whether
         // two signatures are equivalent.
@@ -744,6 +755,26 @@ impl<'db> Signature<'db> {
         relation: TypeRelation<'db>,
         relation_visitor: &HasRelationToVisitor<'db>,
         disjointness_visitor: &IsDisjointVisitor<'db>,
+    ) -> ConstraintSet<'db> {
+        self.has_relation_to_inner(
+            db,
+            other,
+            inferable,
+            relation,
+            relation_visitor,
+            disjointness_visitor,
+        )
+        .reduce_inferable(db, inferable)
+    }
+
+    fn has_relation_to_inner(
+        &self,
+        db: &'db dyn Db,
+        other: &Signature<'db>,
+        inferable: InferableTypeVars<'db>,
+        relation: TypeRelation<'db>,
+        relation_visitor: &HasRelationToVisitor<'db>,
+        disjointness_visitor: &IsDisjointVisitor<'db>,
     ) -> ConstraintSet<'db> {
         /// A helper struct to zip two slices of parameters together that provides control over the
         /// two iterators individually. It also keeps track of the current parameter in each