constrain typevar

This commit is contained in:
Douglas Creager 2025-08-25 15:53:51 -04:00
parent 836a9ea441
commit c6f5bca2a8
2 changed files with 40 additions and 2 deletions

View file

@ -1576,12 +1576,28 @@ impl<'db> Type<'db> {
{
match bound_typevar.typevar(db).bound_or_constraints(db) {
None => unreachable!(),
// Verify that the upper bound satisfies the relation. (If it does, than any
// subtype of the upper bound will too.) Also add a safety constraint that
// ensures that the typevar specializes to a subtype of the upper bound.
Some(TypeVarBoundOrConstraints::UpperBound(bound)) => {
bound.has_relation_to_impl(db, target, relation, visitor)
ConstraintSet::constrain_typevar(db, bound_typevar, Type::Never, bound)
.implies(db, || {
bound.has_relation_to_impl(db, target, relation, visitor)
})
}
Some(TypeVarBoundOrConstraints::Constraints(constraints)) => {
constraints.elements(db).iter().when_all(db, |constraint| {
constraint.has_relation_to_impl(db, target, relation, visitor)
// Note that constrained typevars must specialize to _exactly_ one of the
// constraints, not to a _subtype_ of one.
ConstraintSet::constrain_typevar(
db,
bound_typevar,
*constraint,
*constraint,
)
.implies(db, || {
constraint.has_relation_to_impl(db, target, relation, visitor)
})
})
}
}

View file

@ -171,6 +171,19 @@ impl<'db> ConstraintSet<'db> {
}
}
/// Returns a constraint set that constraints a typevar to a particular range of types.
pub(crate) fn constrain_typevar(
db: &'db dyn Db,
typevar: BoundTypeVarInstance<'db>,
lower: Type<'db>,
upper: Type<'db>,
) -> Self {
let lower = lower.bottom_materialization(db);
let upper = upper.top_materialization(db);
let node = RangeConstraint::new_node(db, lower, typevar, upper);
Self { node }
}
/// Returns whether this constraint set never holds
pub(crate) fn is_never_satisfied(self) -> bool {
self.node.is_never_satisfied()
@ -220,6 +233,15 @@ impl<'db> ConstraintSet<'db> {
self
}
/// Returns a constraint set encoding that this constraint set implies another.
///
/// In Boolean logic, `p → q` is usually translated into `¬p q`. However, we translate it
/// into the equivalent `¬p (p ∧ q)`. This ensures that the constraints under which `q` is
/// true are compatible with the assumptions introduced by `p`.
pub(crate) fn implies(self, db: &'db dyn Db, other: impl FnOnce() -> Self) -> Self {
self.clone().negate(db).or(db, || self.and(db, other))
}
pub(crate) fn range(
db: &'db dyn Db,
lower: Type<'db>,