use ConstraintSetAssignability for constraint bounds

This commit is contained in:
Douglas Creager 2025-12-04 08:40:28 -05:00
parent 312c4ce5c8
commit db3501bac1
2 changed files with 24 additions and 6 deletions

View File

@ -1911,6 +1911,20 @@ impl<'db> Type<'db> {
.is_always_satisfied(db) .is_always_satisfied(db)
} }
/// Return true if this type is assignable to type `target` using constraint-set assignability.
///
/// This uses `TypeRelation::ConstraintSetAssignability`, which encodes typevar relations into
/// a constraint set and lets `satisfied_by_all_typevars` perform existential vs universal
/// reasoning depending on inferable typevars.
pub fn is_constraint_set_assignable_to(
self,
db: &'db dyn Db,
target: Type<'db>,
) -> bool {
self.when_constraint_set_assignable_to(db, target, InferableTypeVars::None)
.is_always_satisfied(db)
}
fn when_assignable_to( fn when_assignable_to(
self, self,
db: &'db dyn Db, db: &'db dyn Db,

View File

@ -606,7 +606,7 @@ impl<'db> ConstrainedTypeVar<'db> {
// If `lower ≰ upper`, then the constraint cannot be satisfied, since there is no type that // If `lower ≰ upper`, then the constraint cannot be satisfied, since there is no type that
// is both greater than `lower`, and less than `upper`. // is both greater than `lower`, and less than `upper`.
if !lower.is_subtype_of(db, upper) { if !lower.is_constraint_set_assignable_to(db, upper) {
return Node::AlwaysFalse; return Node::AlwaysFalse;
} }
@ -724,8 +724,12 @@ impl<'db> ConstrainedTypeVar<'db> {
if !self.typevar(db).is_same_typevar_as(db, other.typevar(db)) { if !self.typevar(db).is_same_typevar_as(db, other.typevar(db)) {
return false; return false;
} }
other.lower(db).is_subtype_of(db, self.lower(db)) other
&& self.upper(db).is_subtype_of(db, other.upper(db)) .lower(db)
.is_constraint_set_assignable_to(db, self.lower(db))
&& self
.upper(db)
.is_constraint_set_assignable_to(db, other.upper(db))
} }
/// Returns the intersection of two range constraints, or `None` if the intersection is empty. /// Returns the intersection of two range constraints, or `None` if the intersection is empty.
@ -736,7 +740,7 @@ impl<'db> ConstrainedTypeVar<'db> {
// If `lower ≰ upper`, then the intersection is empty, since there is no type that is both // If `lower ≰ upper`, then the intersection is empty, since there is no type that is both
// greater than `lower`, and less than `upper`. // greater than `lower`, and less than `upper`.
if !lower.is_subtype_of(db, upper) { if !lower.is_constraint_set_assignable_to(db, upper) {
return IntersectionResult::Disjoint; return IntersectionResult::Disjoint;
} }
@ -1280,7 +1284,7 @@ impl<'db> Node<'db> {
// process. // process.
debug_assert!(current_bounds.is_none_or( debug_assert!(current_bounds.is_none_or(
|(greatest_lower_bound, least_upper_bound)| { |(greatest_lower_bound, least_upper_bound)| {
greatest_lower_bound.is_subtype_of(db, least_upper_bound) greatest_lower_bound.is_constraint_set_assignable_to(db, least_upper_bound)
} }
)); ));
@ -3485,7 +3489,7 @@ impl<'db> GenericContext<'db> {
// If `lower ≰ upper`, then there is no type that satisfies all of the paths in the // If `lower ≰ upper`, then there is no type that satisfies all of the paths in the
// BDD. That's an ambiguous specialization, as described above. // BDD. That's an ambiguous specialization, as described above.
if !greatest_lower_bound.is_subtype_of(db, least_upper_bound) { if !greatest_lower_bound.is_constraint_set_assignable_to(db, least_upper_bound) {
tracing::debug!( tracing::debug!(
target: "ty_python_semantic::types::constraints::specialize_constrained", target: "ty_python_semantic::types::constraints::specialize_constrained",
bound_typevar = %identity.display(db), bound_typevar = %identity.display(db),