BLAMMO

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]))
 

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>,

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