constraint implication

Author: dcreager

crates/ty_python_semantic/src/types.rs

@@ -198,7 +198,7 @@ pub(crate) type ApplyTypeMappingVisitor<'db> = TypeTransformer<'db, TypeMapping<
 
 /// A [`PairVisitor`] that is used in `has_relation_to` methods.
 pub(crate) type HasRelationToVisitor<'db> =
-    CycleDetector<TypeRelation, (Type<'db>, Type<'db>, TypeRelation), ConstraintSet<'db>>;
+    CycleDetector<TypeRelation<'db>, (Type<'db>, Type<'db>, TypeRelation<'db>), ConstraintSet<'db>>;
 
 impl Default for HasRelationToVisitor<'_> {
     fn default() -> Self {
@@ -1589,7 +1589,7 @@ impl<'db> Type<'db> {
         db: &'db dyn Db,
         target: Type<'db>,
         inferable: InferableTypeVars<'_, 'db>,
-        relation: TypeRelation,
+        relation: TypeRelation<'db>,
     ) -> ConstraintSet<'db> {
         self.has_relation_to_impl(
             db,
@@ -1606,7 +1606,7 @@ impl<'db> Type<'db> {
         db: &'db dyn Db,
         target: Type<'db>,
         inferable: InferableTypeVars<'_, 'db>,
-        relation: TypeRelation,
+        relation: TypeRelation<'db>,
         relation_visitor: &HasRelationToVisitor<'db>,
         disjointness_visitor: &IsDisjointVisitor<'db>,
     ) -> ConstraintSet<'db> {
@@ -1699,6 +1699,9 @@ impl<'db> Type<'db> {
                     Type::Union(union) => union.elements(db).iter().any(Type::is_dynamic),
                     _ => false,
                 },
+                TypeRelation::ConstraintImplication(_) => {
+                    panic!("constraints should not contain dynamic types")
+                }
             }),
             (_, Type::Dynamic(_)) => ConstraintSet::from(match relation {
                 TypeRelation::Subtyping => false,
@@ -1710,6 +1713,9 @@ impl<'db> Type<'db> {
                     }
                     _ => false,
                 },
+                TypeRelation::ConstraintImplication(_) => {
+                    panic!("constraints should not contain dynamic types")
+                }
             }),
 
             // In general, a TypeVar `T` is not a subtype of a type `S` unless one of the two conditions is satisfied:
@@ -1894,12 +1900,16 @@ impl<'db> Type<'db> {
                     // to non-transitivity (highly undesirable); and pragmatically, a full implementation
                     // of redundancy may not generally lead to simpler types in many situations.
                     let self_ty = match relation {
-                        TypeRelation::Subtyping | TypeRelation::Redundancy => self,
+                        TypeRelation::Subtyping
+                        | TypeRelation::Redundancy
+                        | TypeRelation::ConstraintImplication(_) => self,
                         TypeRelation::Assignability => self.bottom_materialization(db),
                     };
                     intersection.negative(db).iter().when_all(db, |&neg_ty| {
                         let neg_ty = match relation {
-                            TypeRelation::Subtyping | TypeRelation::Redundancy => neg_ty,
+                            TypeRelation::Subtyping
+                            | TypeRelation::Redundancy
+                            | TypeRelation::ConstraintImplication(_) => neg_ty,
                             TypeRelation::Assignability => neg_ty.bottom_materialization(db),
                         };
                         self_ty.is_disjoint_from_impl(
@@ -9715,7 +9725,7 @@ impl<'db> ConstructorCallError<'db> {
 
 /// A non-exhaustive enumeration of relations that can exist between types.
 #[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)]
-pub(crate) enum TypeRelation {
+pub(crate) enum TypeRelation<'db> {
     /// The "subtyping" relation.
     ///
     /// A [fully static] type `B` is a subtype of a fully static type `A` if and only if
@@ -9835,9 +9845,45 @@ pub(crate) enum TypeRelation {
     /// [fully static]: https://typing.python.org/en/latest/spec/glossary.html#term-fully-static-type
     /// [materializations]: https://typing.python.org/en/latest/spec/glossary.html#term-materialize
     Redundancy,
+
+    /// The "constraint implication" relation.
+    ///
+    /// This is used when solving a [`ConstraintSet`], which expresses the conditions under which
+    /// one of the other relationships hold. There are three cases to consider: dynamic types,
+    /// concrete types, and typevars.
+    ///
+    /// The first case is easy; we can ignore it! The upper and lower bounds of a constraint are
+    /// guaranteed to be fully static, so we don't have to define constraint implication for
+    /// dynamic types.
+    ///
+    /// For concrete types, all of the typing relationships (including this one) produce the same
+    /// result. (A concrete type is any fully static type that is not a typevar. It can _contain_ a
+    /// typevar, though — `list[T]` is considered concrete.)
+    ///
+    /// The interesting case is typevars. The other typing relationships all "punt" on the question
+    /// when considering a typevar, by translating the desired relationship into a constraint set.
+    /// That is, we say that `T` is assignable to `int` when `T ≤ int`. (There are interesting
+    /// nuances when comparing a typevar with a dynamic type, but they all end up translating the
+    /// types into a constraint in some way.)
+    ///
+    /// At some point, though, we need to resolve a constraint set; at that point, we can no longer
+    /// punt on the question, and have to determine whether a runtime instance being a member of
+    /// `T` implies that it is also a member of `int`. This will depend on the final constraint set
+    /// that we produced, which might incorporate tighter constraints from other parts of a larger
+    /// type. For instance, `S` implies `int` under each of the following constraint sets:
+    ///
+    ///   - `S ≤ bool`
+    ///   - `S ≤ int`
+    ///   - `S ≤ T ∧ T ≤ int`
+    ///
+    /// Whereas `S` does not imply `int` under the following:
+    ///
+    ///   - `S ≤ str`
+    ///   - `S ≤ T`
+    ConstraintImplication(ConstraintSet<'db>),
 }
 
-impl TypeRelation {
+impl TypeRelation<'_> {
     pub(crate) const fn is_assignability(self) -> bool {
         matches!(self, TypeRelation::Assignability)
     }
@@ -10005,7 +10051,7 @@ impl<'db> BoundMethodType<'db> {
         db: &'db dyn Db,
         other: Self,
         inferable: InferableTypeVars<'_, 'db>,
-        relation: TypeRelation,
+        relation: TypeRelation<'db>,
         relation_visitor: &HasRelationToVisitor<'db>,
         disjointness_visitor: &IsDisjointVisitor<'db>,
     ) -> ConstraintSet<'db> {
@@ -10172,7 +10218,7 @@ impl<'db> CallableType<'db> {
         db: &'db dyn Db,
         other: Self,
         inferable: InferableTypeVars<'_, 'db>,
-        relation: TypeRelation,
+        relation: TypeRelation<'db>,
         relation_visitor: &HasRelationToVisitor<'db>,
         disjointness_visitor: &IsDisjointVisitor<'db>,
     ) -> ConstraintSet<'db> {
@@ -10267,7 +10313,7 @@ impl<'db> KnownBoundMethodType<'db> {
         db: &'db dyn Db,
         other: Self,
         inferable: InferableTypeVars<'_, 'db>,
-        relation: TypeRelation,
+        relation: TypeRelation<'db>,
         relation_visitor: &HasRelationToVisitor<'db>,
         disjointness_visitor: &IsDisjointVisitor<'db>,
     ) -> ConstraintSet<'db> {

crates/ty_python_semantic/src/types/class.rs

@@ -596,14 +596,16 @@ impl<'db> ClassType<'db> {
         db: &'db dyn Db,
         other: Self,
         inferable: InferableTypeVars<'_, 'db>,
-        relation: TypeRelation,
+        relation: TypeRelation<'db>,
         relation_visitor: &HasRelationToVisitor<'db>,
         disjointness_visitor: &IsDisjointVisitor<'db>,
     ) -> ConstraintSet<'db> {
         self.iter_mro(db).when_any(db, |base| {
             match base {
                 ClassBase::Dynamic(_) => match relation {
-                    TypeRelation::Subtyping | TypeRelation::Redundancy => {
+                    TypeRelation::Subtyping
+                    | TypeRelation::Redundancy
+                    | TypeRelation::ConstraintImplication(_) => {
                         ConstraintSet::from(other.is_object(db))
                     }
                     TypeRelation::Assignability => ConstraintSet::from(!other.is_final(db)),

crates/ty_python_semantic/src/types/constraints.rs

@@ -64,7 +64,8 @@ use rustc_hash::FxHashSet;
 use salsa::plumbing::AsId;
 
 use crate::Db;
-use crate::types::{BoundTypeVarIdentity, IntersectionType, Type, UnionType};
+use crate::types::generics::InferableTypeVars;
+use crate::types::{BoundTypeVarIdentity, IntersectionType, Type, TypeRelation, UnionType};
 
 /// An extension trait for building constraint sets from [`Option`] values.
 pub(crate) trait OptionConstraintsExtension<T> {
@@ -185,6 +186,22 @@ impl<'db> ConstraintSet<'db> {
         self.node.is_always_satisfied()
     }
 
+    fn type_implies(
+        self,
+        db: &'db dyn Db,
+        lhs: Type<'db>,
+        rhs: Type<'db>,
+        inferable: InferableTypeVars<'_, 'db>,
+    ) -> bool {
+        lhs.has_relation_to(
+            db,
+            rhs,
+            inferable,
+            TypeRelation::ConstraintImplication(self),
+        )
+        .is_always_satisfied()
+    }
+
     /// Updates this constraint set to hold the union of itself and another constraint set.
     pub(crate) fn union(&mut self, db: &'db dyn Db, other: Self) -> Self {
         self.node = self.node.or(db, other.node);
@@ -247,7 +264,7 @@ impl<'db> ConstraintSet<'db> {
     }
 
     pub(crate) fn display(self, db: &'db dyn Db) -> impl Display {
-        self.node.display(db)
+        self.node.display(db, self)
     }
 }
 
@@ -321,20 +338,34 @@ impl<'db> ConstrainedTypeVar<'db> {
     ///
     /// This is used (among other places) to simplify how we display constraint sets, by removing
     /// redundant constraints from a clause.
-    fn implies(self, db: &'db dyn Db, other: Self) -> bool {
-        other.contains(db, self)
+    fn implies(self, db: &'db dyn Db, other: Self, constraints: ConstraintSet<'db>) -> bool {
+        if self.typevar(db) != other.typevar(db) {
+            return false;
+        }
+        constraints.type_implies(db, other.lower(db), self.lower(db), InferableTypeVars::None)
+            && constraints.type_implies(
+                db,
+                self.upper(db),
+                other.upper(db),
+                InferableTypeVars::None,
+            )
     }
 
     /// Returns the intersection of two range constraints, or `None` if the intersection is empty.
-    fn intersect(self, db: &'db dyn Db, other: Self) -> Option<Self> {
+    fn intersect(
+        self,
+        db: &'db dyn Db,
+        other: Self,
+        constraints: ConstraintSet<'db>,
+    ) -> Option<Self> {
         // (s₁ ≤ α ≤ t₁) ∧ (s₂ ≤ α ≤ t₂) = (s₁ ∪ s₂) ≤ α ≤ (t₁ ∩ t₂))
         let lower = UnionType::from_elements(db, [self.lower(db), other.lower(db)]).normalized(db);
         let upper =
             IntersectionType::from_elements(db, [self.upper(db), other.upper(db)]).normalized(db);
 
         // If `lower ≰ upper`, then the intersection is empty, since there is no type that is both
         // greater than `lower`, and less than `upper`.
-        if !lower.is_subtype_of(db, upper) {
+        if !constraints.type_implies(db, lower, upper, InferableTypeVars::None) {
             return None;
         }
 
@@ -755,10 +786,10 @@ impl<'db> Node<'db> {
     }
 
     /// Simplifies a BDD, replacing constraints with simpler or smaller constraints where possible.
-    fn simplify(self, db: &'db dyn Db) -> Self {
+    fn simplify(self, db: &'db dyn Db, constraints: ConstraintSet<'db>) -> Self {
         match self {
             Node::AlwaysTrue | Node::AlwaysFalse => self,
-            Node::Interior(interior) => interior.simplify(db),
+            Node::Interior(interior) => interior.simplify(db, constraints),
         }
     }
 
@@ -796,14 +827,15 @@ impl<'db> Node<'db> {
         searcher.clauses
     }
 
-    fn display(self, db: &'db dyn Db) -> impl Display {
+    fn display(self, db: &'db dyn Db, constraints: ConstraintSet<'db>) -> impl Display {
         // To render a BDD in DNF form, you perform a depth-first search of the BDD tree, looking
         // for any path that leads to the AlwaysTrue terminal. Each such path represents one of the
         // intersection clauses in the DNF form. The path traverses zero or more interior nodes,
         // and takes either the true or false edge from each one. That gives you the positive or
         // negative individual constraints in the path's clause.
         struct DisplayNode<'db> {
             node: Node<'db>,
+            constraints: ConstraintSet<'db>,
             db: &'db dyn Db,
         }
 
@@ -814,15 +846,16 @@ impl<'db> Node<'db> {
                     Node::AlwaysFalse => f.write_str("never"),
                     Node::Interior(_) => {
                         let mut clauses = self.node.satisfied_clauses(self.db);
-                        clauses.simplify(self.db);
+                        clauses.simplify(self.db, self.constraints);
                         clauses.display(self.db).fmt(f)
                     }
                 }
             }
         }
 
         DisplayNode {
-            node: self.simplify(db),
+            node: self.simplify(db, constraints),
+            constraints,
             db,
         }
     }
@@ -1033,7 +1066,7 @@ impl<'db> InteriorNode<'db> {
     }
 
     #[salsa::tracked(heap_size=ruff_memory_usage::heap_size)]
-    fn simplify(self, db: &'db dyn Db) -> Node<'db> {
+    fn simplify(self, db: &'db dyn Db, constraints: ConstraintSet<'db>) -> Node<'db> {
         // To simplify a non-terminal BDD, we find all pairs of constraints that are mentioned in
         // the BDD. If any of those pairs can be simplified to some other BDD, we perform a
         // substitution to replace the pair with the simplification.
@@ -1117,7 +1150,7 @@ impl<'db> InteriorNode<'db> {
             // There are some simplifications we can make when the intersection of the two
             // constraints is empty, and others that we can make when the intersection is
             // non-empty.
-            match left_constraint.intersect(db, right_constraint) {
+            match left_constraint.intersect(db, right_constraint, constraints) {
                 Some(intersection_constraint) => {
                     // If the intersection is non-empty, we need to create a new constraint to
                     // represent that intersection. We also need to add the new constraint to our
@@ -1274,7 +1307,7 @@ impl<'db> ConstraintAssignment<'db> {
     ///
     /// This is used (among other places) to simplify how we display constraint sets, by removing
     /// redundant constraints from a clause.
-    fn implies(self, db: &'db dyn Db, other: Self) -> bool {
+    fn implies(self, db: &'db dyn Db, other: Self, constraints: ConstraintSet<'db>) -> bool {
         match (self, other) {
             // For two positive constraints, one range has to fully contain the other; the smaller
             // constraint implies the larger.
@@ -1284,7 +1317,7 @@ impl<'db> ConstraintAssignment<'db> {
             (
                 ConstraintAssignment::Positive(self_constraint),
                 ConstraintAssignment::Positive(other_constraint),
-            ) => self_constraint.implies(db, other_constraint),
+            ) => self_constraint.implies(db, other_constraint, constraints),
 
             // For two negative constraints, one range has to fully contain the other; the ranges
             // represent "holes", though, so the constraint with the larger range implies the one
@@ -1295,7 +1328,7 @@ impl<'db> ConstraintAssignment<'db> {
             (
                 ConstraintAssignment::Negative(self_constraint),
                 ConstraintAssignment::Negative(other_constraint),
-            ) => other_constraint.implies(db, self_constraint),
+            ) => other_constraint.implies(db, self_constraint, constraints),
 
             // For a positive and negative constraint, the ranges have to be disjoint, and the
             // positive range implies the negative range.
@@ -1305,7 +1338,9 @@ impl<'db> ConstraintAssignment<'db> {
             (
                 ConstraintAssignment::Positive(self_constraint),
                 ConstraintAssignment::Negative(other_constraint),
-            ) => self_constraint.intersect(db, other_constraint).is_none(),
+            ) => self_constraint
+                .intersect(db, other_constraint, constraints)
+                .is_none(),
 
             // It's theoretically possible for a negative constraint to imply a positive constraint
             // if the positive constraint is always satisfied (`Never ≤ T ≤ object`). But we never
@@ -1391,15 +1426,15 @@ impl<'db> SatisfiedClause<'db> {
     /// want to remove the larger one and keep the smaller one.)
     ///
     /// Returns a boolean that indicates whether any simplifications were made.
-    fn simplify(&mut self, db: &'db dyn Db) -> bool {
+    fn simplify(&mut self, db: &'db dyn Db, constraints: ConstraintSet<'db>) -> bool {
         let mut changes_made = false;
         let mut i = 0;
         // Loop through each constraint, comparing it with any constraints that appear later in the
         // list.
         'outer: while i < self.constraints.len() {
             let mut j = i + 1;
             while j < self.constraints.len() {
-                if self.constraints[j].implies(db, self.constraints[i]) {
+                if self.constraints[j].implies(db, self.constraints[i], constraints) {
                     // If constraint `i` is removed, then we don't need to compare it with any
                     // later constraints in the list. Note that we continue the outer loop, instead
                     // of breaking from the inner loop, so that we don't bump index `i` below.
@@ -1408,7 +1443,7 @@ impl<'db> SatisfiedClause<'db> {
                     self.constraints.swap_remove(i);
                     changes_made = true;
                     continue 'outer;
-                } else if self.constraints[i].implies(db, self.constraints[j]) {
+                } else if self.constraints[i].implies(db, self.constraints[j], constraints) {
                     // If constraint `j` is removed, then we can continue the inner loop. We will
                     // swap a new element into place at index `j`, and will continue comparing the
                     // constraint at index `i` with later constraints.
@@ -1472,11 +1507,11 @@ impl<'db> SatisfiedClauses<'db> {
     /// Simplifies the DNF representation, removing redundancies that do not change the underlying
     /// function. (This is used when displaying a BDD, to make sure that the representation that we
     /// show is as simple as possible while still producing the same results.)
-    fn simplify(&mut self, db: &'db dyn Db) {
+    fn simplify(&mut self, db: &'db dyn Db, constraints: ConstraintSet<'db>) {
         // First simplify each clause individually, by removing constraints that are implied by
         // other constraints in the clause.
         for clause in &mut self.clauses {
-            clause.simplify(db);
+            clause.simplify(db, constraints);
         }
 
         while self.simplify_one_round() {