check valid specializations

crates/ty_python_semantic/resources/mdtest/generics/pep695/variables.md

@@ -173,14 +173,16 @@ from typing_extensions import final
 def bounded[T: Super](t: T) -> None:
     reveal_type(is_assignable_to(T, Any))  # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(Any, T))  # revealed: ty_extensions.ConstraintSet[always]
-    reveal_type(is_assignable_to(T, Super))  # revealed: ty_extensions.ConstraintSet[always]
+    # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@bounded ≤ Super)]
+    reveal_type(is_assignable_to(T, Super))
     reveal_type(is_assignable_to(T, Sub))  # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_assignable_to(Super, T))  # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_assignable_to(Sub, T))  # revealed: ty_extensions.ConstraintSet[never]
 
     reveal_type(is_subtype_of(T, Any))  # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(Any, T))  # revealed: ty_extensions.ConstraintSet[never]
-    reveal_type(is_subtype_of(T, Super))  # revealed: ty_extensions.ConstraintSet[always]
+    # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@bounded ≤ Super)]
+    reveal_type(is_subtype_of(T, Super))
     reveal_type(is_subtype_of(T, Sub))  # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(Super, T))  # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(Sub, T))  # revealed: ty_extensions.ConstraintSet[never]
@@ -206,12 +208,14 @@ class FinalClass: ...
 def bounded_final[T: FinalClass](t: T) -> None:
     reveal_type(is_assignable_to(T, Any))  # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(Any, T))  # revealed: ty_extensions.ConstraintSet[always]
-    reveal_type(is_assignable_to(T, FinalClass))  # revealed: ty_extensions.ConstraintSet[always]
+    # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@bounded_final ≤ FinalClass)]
+    reveal_type(is_assignable_to(T, FinalClass))
     reveal_type(is_assignable_to(FinalClass, T))  # revealed: ty_extensions.ConstraintSet[never]
 
     reveal_type(is_subtype_of(T, Any))  # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(Any, T))  # revealed: ty_extensions.ConstraintSet[never]
-    reveal_type(is_subtype_of(T, FinalClass))  # revealed: ty_extensions.ConstraintSet[always]
+    # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@bounded_final ≤ FinalClass)]
+    reveal_type(is_subtype_of(T, FinalClass))
     reveal_type(is_subtype_of(FinalClass, T))  # revealed: ty_extensions.ConstraintSet[never]
 ```
 
@@ -244,49 +248,71 @@ intersection of all of its constraints is a subtype of the typevar.
 from ty_extensions import Intersection
 
 def constrained[T: (Base, Unrelated)](t: T) -> None:
-    reveal_type(is_assignable_to(T, Super))  # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained = Base)]
-    reveal_type(is_assignable_to(T, Base))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(T, Super))
+    # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained = Base)]
+    reveal_type(is_assignable_to(T, Base))
     reveal_type(is_assignable_to(T, Sub))  # revealed: ty_extensions.ConstraintSet[never]
-    reveal_type(is_assignable_to(T, Unrelated))  # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained = Unrelated)]
+    reveal_type(is_assignable_to(T, Unrelated))
     reveal_type(is_assignable_to(T, Any))  # revealed: ty_extensions.ConstraintSet[always]
-    reveal_type(is_assignable_to(T, Super | Unrelated))  # revealed: ty_extensions.ConstraintSet[always]
+    # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@constrained = Base) ∨ (T@constrained = Unrelated)]
-    reveal_type(is_assignable_to(T, Base | Unrelated))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(T, Super | Unrelated))
-    reveal_type(is_assignable_to(T, Sub | Unrelated))  # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@constrained = Base) ∨ (T@constrained = Unrelated)]
+    reveal_type(is_assignable_to(T, Base | Unrelated))
+    # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained = Unrelated)]
+    reveal_type(is_assignable_to(T, Sub | Unrelated))
     reveal_type(is_assignable_to(Any, T))  # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(Super, T))  # revealed: ty_extensions.ConstraintSet[never]
-    reveal_type(is_assignable_to(Unrelated, T))  # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained = Unrelated)]
+    reveal_type(is_assignable_to(Unrelated, T))
     reveal_type(is_assignable_to(Super | Unrelated, T))  # revealed: ty_extensions.ConstraintSet[never]
-    reveal_type(is_assignable_to(Intersection[Base, Unrelated], T))  # revealed: ty_extensions.ConstraintSet[always]
+    # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@constrained = Base) ∨ (T@constrained = Unrelated)]
+    reveal_type(is_assignable_to(Intersection[Base, Unrelated], T))
 
-    reveal_type(is_subtype_of(T, Super))  # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained = Base)]
-    reveal_type(is_subtype_of(T, Base))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(T, Super))
+    # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained = Base)]
+    reveal_type(is_subtype_of(T, Base))
     reveal_type(is_subtype_of(T, Sub))  # revealed: ty_extensions.ConstraintSet[never]
-    reveal_type(is_subtype_of(T, Unrelated))  # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained = Unrelated)]
+    reveal_type(is_subtype_of(T, Unrelated))
     reveal_type(is_subtype_of(T, Any))  # revealed: ty_extensions.ConstraintSet[never]
-    reveal_type(is_subtype_of(T, Super | Unrelated))  # revealed: ty_extensions.ConstraintSet[always]
+    # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@constrained = Base) ∨ (T@constrained = Unrelated)]
-    reveal_type(is_subtype_of(T, Base | Unrelated))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_subtype_of(T, Super | Unrelated))
-    reveal_type(is_subtype_of(T, Sub | Unrelated))  # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@constrained = Base) ∨ (T@constrained = Unrelated)]
+    reveal_type(is_subtype_of(T, Base | Unrelated))
+    # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained = Unrelated)]
+    reveal_type(is_subtype_of(T, Sub | Unrelated))
     reveal_type(is_subtype_of(Any, T))  # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(Super, T))  # revealed: ty_extensions.ConstraintSet[never]
-    reveal_type(is_subtype_of(Unrelated, T))  # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained = Unrelated)]
+    reveal_type(is_subtype_of(Unrelated, T))
     reveal_type(is_subtype_of(Super | Unrelated, T))  # revealed: ty_extensions.ConstraintSet[never]
-    reveal_type(is_subtype_of(Intersection[Base, Unrelated], T))  # revealed: ty_extensions.ConstraintSet[always]
+    # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@constrained = Base) ∨ (T@constrained = Unrelated)]
+    reveal_type(is_subtype_of(Intersection[Base, Unrelated], T))
 
 def constrained_by_gradual[T: (Base, Any)](t: T) -> None:
     reveal_type(is_assignable_to(T, Super))  # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(T, Base))  # revealed: ty_extensions.ConstraintSet[always]
-    reveal_type(is_assignable_to(T, Sub))  # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained_by_gradual ≠ Base)]
-    reveal_type(is_assignable_to(T, Unrelated))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(T, Sub))
+    # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained_by_gradual ≠ Base)]
+    reveal_type(is_assignable_to(T, Unrelated))
     reveal_type(is_assignable_to(T, Any))  # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(T, Super | Any))  # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(T, Super | Unrelated))  # revealed: ty_extensions.ConstraintSet[always]
-    reveal_type(is_assignable_to(Super, T))  # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained_by_gradual ≠ Base)]
+    reveal_type(is_assignable_to(Super, T))
     reveal_type(is_assignable_to(Base, T))  # revealed: ty_extensions.ConstraintSet[always]
-    reveal_type(is_assignable_to(Unrelated, T))  # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained_by_gradual ≠ Base)]
+    reveal_type(is_assignable_to(Unrelated, T))
     reveal_type(is_assignable_to(Any, T))  # revealed: ty_extensions.ConstraintSet[always]
-    reveal_type(is_assignable_to(Super | Any, T))  # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained_by_gradual ≠ Base)]
+    reveal_type(is_assignable_to(Super | Any, T))
     reveal_type(is_assignable_to(Base | Any, T))  # revealed: ty_extensions.ConstraintSet[always]
-    reveal_type(is_assignable_to(Super | Unrelated, T))  # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained_by_gradual ≠ Base)]
+    reveal_type(is_assignable_to(Super | Unrelated, T))
     reveal_type(is_assignable_to(Intersection[Base, Unrelated], T))  # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(Intersection[Base, Any], T))  # revealed: ty_extensions.ConstraintSet[always]
 
@@ -315,40 +341,54 @@ the same type.
 
 ```py
 def two_constrained[T: (int, str), U: (int, str)](t: T, u: U) -> None:
-    reveal_type(is_assignable_to(T, U))  # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[some valid specializations: ((T@two_constrained = str) ∧ (U@two_constrained = str)) ∨ ((T@two_constrained = int) ∧ (U@two_constrained = int))]
-    reveal_type(is_assignable_to(U, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(T, U))
+    # revealed: ty_extensions.ConstraintSet[some valid specializations: ((U@two_constrained = str) ∧ (T@two_constrained = str)) ∨ ((U@two_constrained = int) ∧ (T@two_constrained = int))]
+    reveal_type(is_assignable_to(U, T))
 
-    reveal_type(is_subtype_of(T, U))  # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[some valid specializations: ((T@two_constrained = str) ∧ (U@two_constrained = str)) ∨ ((T@two_constrained = int) ∧ (U@two_constrained = int))]
-    reveal_type(is_subtype_of(U, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(T, U))
+    # revealed: ty_extensions.ConstraintSet[some valid specializations: ((U@two_constrained = str) ∧ (T@two_constrained = str)) ∨ ((U@two_constrained = int) ∧ (T@two_constrained = int))]
+    reveal_type(is_subtype_of(U, T))
 
 @final
 class AnotherFinalClass: ...
 
 def two_final_constrained[T: (FinalClass, AnotherFinalClass), U: (FinalClass, AnotherFinalClass)](t: T, u: U) -> None:
-    reveal_type(is_assignable_to(T, U))  # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[some valid specializations: ((T@two_final_constrained = AnotherFinalClass) ∧ (U@two_final_constrained = AnotherFinalClass)) ∨ ((T@two_final_constrained = FinalClass) ∧ (U@two_final_constrained = FinalClass))]
-    reveal_type(is_assignable_to(U, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(T, U))
+    # revealed: ty_extensions.ConstraintSet[some valid specializations: ((U@two_final_constrained = AnotherFinalClass) ∧ (T@two_final_constrained = AnotherFinalClass)) ∨ ((U@two_final_constrained = FinalClass) ∧ (T@two_final_constrained = FinalClass))]
+    reveal_type(is_assignable_to(U, T))
 
-    reveal_type(is_subtype_of(T, U))  # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[some valid specializations: ((T@two_final_constrained = AnotherFinalClass) ∧ (U@two_final_constrained = AnotherFinalClass)) ∨ ((T@two_final_constrained = FinalClass) ∧ (U@two_final_constrained = FinalClass))]
-    reveal_type(is_subtype_of(U, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(T, U))
+    # revealed: ty_extensions.ConstraintSet[some valid specializations: ((U@two_final_constrained = AnotherFinalClass) ∧ (T@two_final_constrained = AnotherFinalClass)) ∨ ((U@two_final_constrained = FinalClass) ∧ (T@two_final_constrained = FinalClass))]
+    reveal_type(is_subtype_of(U, T))
 ```
 
 A bound or constrained typevar is a subtype of itself in a union:
 
 ```py
 def union[T: Base, U: (Base, Unrelated)](t: T, u: U) -> None:
-    reveal_type(is_assignable_to(T, T | None))  # revealed: ty_extensions.ConstraintSet[always]
+    # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@union ≤ Base)]
-    reveal_type(is_assignable_to(U, U | None))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(T, T | None))
+    # revealed: ty_extensions.ConstraintSet[all valid specializations: (U@union = Base) ∨ (U@union = Unrelated)]
+    reveal_type(is_assignable_to(U, U | None))
 
-    reveal_type(is_subtype_of(T, T | None))  # revealed: ty_extensions.ConstraintSet[always]
+    # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@union ≤ Base)]
-    reveal_type(is_subtype_of(U, U | None))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_subtype_of(T, T | None))
+    # revealed: ty_extensions.ConstraintSet[all valid specializations: (U@union = Base) ∨ (U@union = Unrelated)]
+    reveal_type(is_subtype_of(U, U | None))
 ```
 
 A bound or constrained typevar in a union with a dynamic type is assignable to the typevar:
 
 ```py
 def union_with_dynamic[T: Base, U: (Base, Unrelated)](t: T, u: U) -> None:
-    reveal_type(is_assignable_to(T | Any, T))  # revealed: ty_extensions.ConstraintSet[always]
+    # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@union_with_dynamic ≤ Base)]
-    reveal_type(is_assignable_to(U | Any, U))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(T | Any, T))
+    # revealed: ty_extensions.ConstraintSet[all valid specializations: (U@union_with_dynamic = Base) ∨ (U@union_with_dynamic = Unrelated)]
+    reveal_type(is_assignable_to(U | Any, U))
 
     reveal_type(is_subtype_of(T | Any, T))  # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(U | Any, U))  # revealed: ty_extensions.ConstraintSet[never]
@@ -362,11 +402,15 @@ from ty_extensions import Intersection, Not, is_disjoint_from, static_assert
 class A: ...
 
 def inter[T: Base, U: (Base, Unrelated)](t: T, u: U) -> None:
-    reveal_type(is_assignable_to(Intersection[T, Unrelated], T))  # revealed: ty_extensions.ConstraintSet[always]
+    # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@inter ≤ Base)]
-    reveal_type(is_subtype_of(Intersection[T, Unrelated], T))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(Intersection[T, Unrelated], T))
+    # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@inter ≤ Base)]
+    reveal_type(is_subtype_of(Intersection[T, Unrelated], T))
 
-    reveal_type(is_assignable_to(Intersection[U, A], U))  # revealed: ty_extensions.ConstraintSet[always]
+    # revealed: ty_extensions.ConstraintSet[all valid specializations: (U@inter = Base) ∨ (U@inter = Unrelated)]
-    reveal_type(is_subtype_of(Intersection[U, A], U))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(Intersection[U, A], U))
+    # revealed: ty_extensions.ConstraintSet[all valid specializations: (U@inter = Base) ∨ (U@inter = Unrelated)]
+    reveal_type(is_subtype_of(Intersection[U, A], U))
 
     static_assert(is_disjoint_from(Not[T], T))
     static_assert(is_disjoint_from(T, Not[T]))

crates/ty_python_semantic/src/types.rs

@@ -1449,6 +1449,19 @@ impl<'db> Type<'db> {
         self.when_subtype_of(db, target).is_always_satisfied()
     }
 
+    /// Return the constraints under which this type is a [subtype of] type `target`. (See
+    /// [`is_subtype_of`][Self::is_subtype_of] for more details on how we calculate subtyping.)
+    ///
+    /// If neither type contains any bound typevars (inferable or not), the result will either be
+    /// [always][ConstraintSet::is_always_satisfied] or [never][ConstraintSet::is_never_satisfied].
+    /// Otherwise, the result will describe which types those typevars must be specialized to for
+    /// subtyping to hold. Note that the result will not enforce that the typevars can only be
+    /// specialized to _valid_ specializations (those that satisfy the typevar's upper bound or
+    /// constraints), nor will it ensure that subtyping holds for _all_ valid specializations. We
+    /// leave that up to the caller to check, so that you can use this method to obtain "partial"
+    /// results and build up a more complete constraint set over several subtyping checks.
+    ///
+    /// [subtype of]: https://typing.python.org/en/latest/spec/concepts.html#subtype-supertype-and-type-equivalence
     fn when_subtype_of(self, db: &'db dyn Db, target: Type<'db>) -> ConstraintSet<'db> {
         self.has_relation_to(db, target, TypeRelation::Subtyping)
     }
@@ -1460,6 +1473,19 @@ impl<'db> Type<'db> {
         self.when_assignable_to(db, target).is_always_satisfied()
     }
 
+    /// Returns the constraints under which this type is [assignable to] type `target`.
+    ///
+    /// If neither type contains any bound typevars (inferable or not), the result will either be
+    /// [always][ConstraintSet::is_always_satisfied] or [never][ConstraintSet::is_never_satisfied].
+    /// Otherwise, the result will describe which types those typevars must be specialized to for
+    /// assignability to hold. Note that the result will not enforce that the typevars can only be
+    /// specialized to _valid_ specializations (those that satisfy the typevar's upper bound or
+    /// constraints), nor will it ensure that assignability holds for _all_ valid specializations.
+    /// We leave that up to the caller to check, so that you can use this method to obtain
+    /// "partial" results and build up a more complete constraint set over several assignability
+    /// checks.
+    ///
+    /// [assignable to]: https://typing.python.org/en/latest/spec/concepts.html#the-assignable-to-or-consistent-subtyping-relation
     fn when_assignable_to(self, db: &'db dyn Db, target: Type<'db>) -> ConstraintSet<'db> {
         self.has_relation_to(db, target, TypeRelation::Assignability)
     }
@@ -3946,9 +3972,8 @@ impl<'db> Type<'db> {
                 Truthiness::Ambiguous
             }
 
-            Type::KnownInstance(KnownInstanceType::ConstraintSet(tracked_set)) => {
+            Type::KnownInstance(KnownInstanceType::ConstraintSet(constraints)) => {
-                let constraints = tracked_set.constraints(db);
+                Truthiness::from(constraints.holds_for_all_valid_specializations(db))
-                Truthiness::from(constraints.is_always_satisfied())
             }
 
             Type::FunctionLiteral(_)
@@ -6902,19 +6927,39 @@ impl<'db> TypeMapping<'_, 'db> {
     }
 }
 
-/// A Salsa-tracked constraint set. This is only needed to have something appropriately small to
+/// A constraint set, along with the valid specializations of a list of typevars.
-/// put in a [`KnownInstance::ConstraintSet`]. We don't actually manipulate these as part of using
-/// constraint sets to check things like assignability; they're only used as a debugging aid in
-/// mdtests. That means there's no need for this to be interned; being tracked is sufficient.
 #[salsa::tracked(debug, heap_size=ruff_memory_usage::heap_size)]
 #[derive(PartialOrd, Ord)]
-pub struct TrackedConstraintSet<'db> {
+pub struct ValidSpecializationsConstraintSet<'db> {
+    #[returns(as_ref)]
+    valid_specializations: Option<ConstraintSet<'db>>,
+
     #[returns(ref)]
     constraints: ConstraintSet<'db>,
 }
 
 // The Salsa heap is tracked separately.
-impl get_size2::GetSize for TrackedConstraintSet<'_> {}
+impl get_size2::GetSize for ValidSpecializationsConstraintSet<'_> {}
+
+impl<'db> ValidSpecializationsConstraintSet<'db> {
+    fn limit_to_valid_specializations(self, db: &'db dyn Db) -> ConstraintSet<'db> {
+        let constraints = self.constraints(db).clone();
+        let Some(valid_specializations) = self.valid_specializations(db) else {
+            return constraints;
+        };
+        constraints.and(db, || valid_specializations.clone())
+    }
+
+    fn holds_for_all_valid_specializations(self, db: &'db dyn Db) -> bool {
+        let constraints = self.constraints(db);
+        match self.valid_specializations(db) {
+            Some(valid_specializations) => (valid_specializations.clone())
+                .implies(db, || self.constraints(db).clone())
+                .is_always_satisfied(),
+            _ => constraints.is_always_satisfied(),
+        }
+    }
+}
 
 /// Singleton types that are heavily special-cased by ty. Despite its name,
 /// quite a different type to [`NominalInstanceType`].
@@ -6961,7 +7006,7 @@ pub enum KnownInstanceType<'db> {
 
     /// A constraint set, which is exposed in mdtests as an instance of
     /// `ty_extensions.ConstraintSet`.
-    ConstraintSet(TrackedConstraintSet<'db>),
+    ConstraintSet(ValidSpecializationsConstraintSet<'db>),
 }
 
 fn walk_known_instance_type<'db, V: visitor::TypeVisitor<'db> + ?Sized>(
@@ -7085,11 +7130,19 @@ impl<'db> KnownInstanceType<'db> {
                         f.write_str("]")
                     }
                     KnownInstanceType::ConstraintSet(tracked_set) => {
-                        let constraints = tracked_set.constraints(self.db);
+                        let constraints = tracked_set.limit_to_valid_specializations(self.db);
                         if constraints.is_always_satisfied() {
                             f.write_str("ty_extensions.ConstraintSet[always]")
                         } else if constraints.is_never_satisfied() {
                             f.write_str("ty_extensions.ConstraintSet[never]")
+                        } else if tracked_set.valid_specializations(self.db).is_some() {
+                            let is_valid = tracked_set.holds_for_all_valid_specializations(self.db);
+                            write!(
+                                f,
+                                "ty_extensions.ConstraintSet[{} valid specializations: {}]",
+                                if is_valid { "all" } else { "some" },
+                                constraints.display(self.db)
+                            )
                         } else {
                             write!(
                                 f,

crates/ty_python_semantic/src/types/call/bind.rs

@@ -32,7 +32,7 @@ use crate::types::tuple::{TupleLength, TupleType};
 use crate::types::{
     BoundMethodType, ClassLiteral, DataclassParams, FieldInstance, KnownBoundMethodType,
     KnownClass, KnownInstanceType, MemberLookupPolicy, PropertyInstanceType, SpecialFormType,
-    TrackedConstraintSet, TypeAliasType, TypeContext, TypeMapping, UnionType,
+    TypeAliasType, TypeContext, TypeMapping, UnionType, ValidSpecializationsConstraintSet,
     WrapperDescriptorKind, enums, ide_support, todo_type,
 };
 use ruff_db::diagnostic::{Annotation, Diagnostic, SubDiagnostic, SubDiagnosticSeverity};
@@ -598,9 +598,15 @@ impl<'db> Bindings<'db> {
                         Some(KnownFunction::IsEquivalentTo) => {
                             if let [Some(ty_a), Some(ty_b)] = overload.parameter_types() {
                                 let constraints = ty_a.when_equivalent_to(db, *ty_b);
-                                let tracked = TrackedConstraintSet::new(db, constraints);
+                                let valid_specializations = (ty_a.valid_specializations(db))
+                                    .and(db, || ty_b.valid_specializations(db));
+                                let result = ValidSpecializationsConstraintSet::new(
+                                    db,
+                                    Some(valid_specializations),
+                                    constraints,
+                                );
                                 overload.set_return_type(Type::KnownInstance(
-                                    KnownInstanceType::ConstraintSet(tracked),
+                                    KnownInstanceType::ConstraintSet(result),
                                 ));
                             }
                         }
@@ -608,9 +614,15 @@ impl<'db> Bindings<'db> {
                         Some(KnownFunction::IsSubtypeOf) => {
                             if let [Some(ty_a), Some(ty_b)] = overload.parameter_types() {
                                 let constraints = ty_a.when_subtype_of(db, *ty_b);
-                                let tracked = TrackedConstraintSet::new(db, constraints);
+                                let valid_specializations = (ty_a.valid_specializations(db))
+                                    .and(db, || ty_b.valid_specializations(db));
+                                let result = ValidSpecializationsConstraintSet::new(
+                                    db,
+                                    Some(valid_specializations),
+                                    constraints,
+                                );
                                 overload.set_return_type(Type::KnownInstance(
-                                    KnownInstanceType::ConstraintSet(tracked),
+                                    KnownInstanceType::ConstraintSet(result),
                                 ));
                             }
                         }
@@ -618,9 +630,15 @@ impl<'db> Bindings<'db> {
                         Some(KnownFunction::IsAssignableTo) => {
                             if let [Some(ty_a), Some(ty_b)] = overload.parameter_types() {
                                 let constraints = ty_a.when_assignable_to(db, *ty_b);
-                                let tracked = TrackedConstraintSet::new(db, constraints);
+                                let valid_specializations = (ty_a.valid_specializations(db))
+                                    .and(db, || ty_b.valid_specializations(db));
+                                let result = ValidSpecializationsConstraintSet::new(
+                                    db,
+                                    Some(valid_specializations),
+                                    constraints,
+                                );
                                 overload.set_return_type(Type::KnownInstance(
-                                    KnownInstanceType::ConstraintSet(tracked),
+                                    KnownInstanceType::ConstraintSet(result),
                                 ));
                             }
                         }
@@ -628,9 +646,15 @@ impl<'db> Bindings<'db> {
                         Some(KnownFunction::IsDisjointFrom) => {
                             if let [Some(ty_a), Some(ty_b)] = overload.parameter_types() {
                                 let constraints = ty_a.when_disjoint_from(db, *ty_b);
-                                let tracked = TrackedConstraintSet::new(db, constraints);
+                                let valid_specializations = (ty_a.valid_specializations(db))
+                                    .and(db, || ty_b.valid_specializations(db));
+                                let result = ValidSpecializationsConstraintSet::new(
+                                    db,
+                                    Some(valid_specializations),
+                                    constraints,
+                                );
                                 overload.set_return_type(Type::KnownInstance(
-                                    KnownInstanceType::ConstraintSet(tracked),
+                                    KnownInstanceType::ConstraintSet(result),
                                 ));
                             }
                         }

crates/ty_python_semantic/src/types/constraints.rs

@@ -1412,7 +1412,7 @@ impl<'db> Type<'db> {
                         let valid_specializations = bound_typevar.valid_specializations(db);
                         self.result
                             .borrow_mut()
-                            .intersect(db, &valid_specializations);
+                            .intersect(db, valid_specializations);
                     }
                     _ => {}
                 }

crates/ty_python_semantic/src/types/function.rs

@@ -80,8 +80,8 @@ use crate::types::{
     BoundMethodType, BoundTypeVarInstance, CallableType, ClassBase, ClassLiteral, ClassType,
     DeprecatedInstance, DynamicType, FindLegacyTypeVarsVisitor, HasRelationToVisitor,
     IsEquivalentVisitor, KnownClass, KnownInstanceType, NormalizedVisitor, SpecialFormType,
-    TrackedConstraintSet, Truthiness, Type, TypeMapping, TypeRelation, UnionBuilder, all_members,
+    Truthiness, Type, TypeMapping, TypeRelation, UnionBuilder, ValidSpecializationsConstraintSet,
-    binding_type, todo_type, walk_type_mapping,
+    all_members, binding_type, todo_type, walk_type_mapping,
 };
 use crate::{Db, FxOrderSet, ModuleName, resolve_module};
 
@@ -1702,34 +1702,34 @@ impl KnownFunction {
             KnownFunction::RangeConstraint => {
                 let [
                     Some(lower),
-                    Some(Type::NonInferableTypeVar(typevar)),
+                    Some(Type::NonInferableTypeVar(bound_typevar)),
                     Some(upper),
                 ] = parameter_types
                 else {
                     return;
                 };
 
-                let constraints = ConstraintSet::range(db, *lower, *typevar, *upper);
+                let constraints = ConstraintSet::range(db, *lower, *bound_typevar, *upper);
-                let tracked = TrackedConstraintSet::new(db, constraints);
+                let result = ValidSpecializationsConstraintSet::new(db, None, constraints);
                 overload.set_return_type(Type::KnownInstance(KnownInstanceType::ConstraintSet(
-                    tracked,
+                    result,
                 )));
             }
 
             KnownFunction::NegatedRangeConstraint => {
                 let [
                     Some(lower),
-                    Some(Type::NonInferableTypeVar(typevar)),
+                    Some(Type::NonInferableTypeVar(bound_typevar)),
                     Some(upper),
                 ] = parameter_types
                 else {
                     return;
                 };
 
-                let constraints = ConstraintSet::negated_range(db, *lower, *typevar, *upper);
+                let constraints = ConstraintSet::negated_range(db, *lower, *bound_typevar, *upper);
-                let tracked = TrackedConstraintSet::new(db, constraints);
+                let result = ValidSpecializationsConstraintSet::new(db, None, constraints);
                 overload.set_return_type(Type::KnownInstance(KnownInstanceType::ConstraintSet(
-                    tracked,
+                    result,
                 )));
             }
 

crates/ty_python_semantic/src/types/generics.rs

@@ -1131,7 +1131,7 @@ impl<'db> SpecializationBuilder<'db> {
                                     }
                                 }
                             }
-                            when_all_assignable.intersect(self.db, &when_assignable);
+                            when_all_assignable.intersect(self.db, when_assignable);
                         }
 
                         if when_all_assignable.is_always_satisfied() {

crates/ty_python_semantic/src/types/infer/builder.rs

@@ -91,10 +91,10 @@ use crate::types::{
     BoundTypeVarInstance, CallDunderError, CallableType, ClassLiteral, ClassType, DataclassParams,
     DynamicType, IntersectionBuilder, IntersectionType, KnownClass, KnownInstanceType,
     MemberLookupPolicy, MetaclassCandidate, PEP695TypeAliasType, Parameter, ParameterForm,
-    Parameters, SpecialFormType, SubclassOfType, TrackedConstraintSet, Truthiness, Type,
+    Parameters, SpecialFormType, SubclassOfType, Truthiness, Type, TypeAliasType,
-    TypeAliasType, TypeAndQualifiers, TypeContext, TypeMapping, TypeQualifiers,
+    TypeAndQualifiers, TypeContext, TypeMapping, TypeQualifiers,
     TypeVarBoundOrConstraintsEvaluation, TypeVarDefaultEvaluation, TypeVarInstance, TypeVarKind,
-    UnionBuilder, UnionType, binding_type, todo_type,
+    UnionBuilder, UnionType, ValidSpecializationsConstraintSet, binding_type, todo_type,
 };
 use crate::types::{ClassBase, add_inferred_python_version_hint_to_diagnostic};
 use crate::unpack::{EvaluationMode, UnpackPosition};
@@ -6947,12 +6947,16 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
                 ast::UnaryOp::Invert,
                 Type::KnownInstance(KnownInstanceType::ConstraintSet(constraints)),
             ) => {
+                let valid_specializations = constraints.valid_specializations(self.db()).cloned();
                 let constraints = constraints.constraints(self.db());
                 let result = constraints.negate(self.db());
-                Type::KnownInstance(KnownInstanceType::ConstraintSet(TrackedConstraintSet::new(
+                Type::KnownInstance(KnownInstanceType::ConstraintSet(
-                    self.db(),
+                    ValidSpecializationsConstraintSet::new(
-                    result,
+                        self.db(),
-                )))
+                        valid_specializations,
+                        result,
+                    ),
+                ))
             }
 
             (ast::UnaryOp::Not, ty) => ty
@@ -7309,26 +7313,29 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
             (
                 Type::KnownInstance(KnownInstanceType::ConstraintSet(left)),
                 Type::KnownInstance(KnownInstanceType::ConstraintSet(right)),
-                ast::Operator::BitAnd,
+                ast::Operator::BitAnd | ast::Operator::BitOr,
             ) => {
+                let valid_specializations = match (
+                    left.valid_specializations(self.db()),
+                    right.valid_specializations(self.db()),
+                ) {
+                    (Some(left), Some(right)) => Some(left.and(self.db(), || *right)),
+                    (Some(single), None) | (None, Some(single)) => Some(*single),
+                    (None, None) => None,
+                };
                 let left = left.constraints(self.db());
                 let right = right.constraints(self.db());
-                let result = left.and(self.db(), || *right);
+                let result = match op {
+                    ast::Operator::BitAnd => left.and(self.db(), || *right),
+                    ast::Operator::BitOr => left.or(self.db(), || *right),
+                    _ => unreachable!("operator should only be BitAnd or BitOr"),
+                };
                 Some(Type::KnownInstance(KnownInstanceType::ConstraintSet(
-                    TrackedConstraintSet::new(self.db(), result),
+                    ValidSpecializationsConstraintSet::new(
-                )))
+                        self.db(),
-            }
+                        valid_specializations,
-
+                        result,
-            (
+                    ),
-                Type::KnownInstance(KnownInstanceType::ConstraintSet(left)),
-                Type::KnownInstance(KnownInstanceType::ConstraintSet(right)),
-                ast::Operator::BitOr,
-            ) => {
-                let left = left.constraints(self.db());
-                let right = right.constraints(self.db());
-                let result = left.or(self.db(), || *right);
-                Some(Type::KnownInstance(KnownInstanceType::ConstraintSet(
-                    TrackedConstraintSet::new(self.db(), result),
                 )))
             }