diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs index b2cb2d61f1..5dc0e4e9b0 100644 --- a/crates/ty_python_semantic/src/types.rs +++ b/crates/ty_python_semantic/src/types.rs @@ -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) + }) }) } } diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index cb4e504196..7e62695426 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -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>,