diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index 093f43096fabd..0c394fbfa9f9f 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -88,7 +88,6 @@ use std::cell::{Cell, RefCell}; use std::cmp::Ordering; -use std::collections::VecDeque; use std::convert::Infallible; use std::fmt::{Debug, Display}; use std::iter; @@ -96,7 +95,6 @@ use std::marker::PhantomData; use std::ops::{ControlFlow, Range}; use std::sync::{Arc, LazyLock}; -use indexmap::map::Entry; use itertools::Itertools; use ruff_index::{Idx, IndexVec, newtype_index}; use rustc_hash::{FxHashMap, FxHashSet}; @@ -109,10 +107,8 @@ use crate::types::class::GenericAlias; use crate::types::constraints::projection::{ProjectionError, SolutionBudget}; use crate::types::constraints::support::{Support, SupportId}; use crate::types::typevar::{BoundTypeVarIdentity, TypeVarInstance, TypeVarSet}; -use crate::types::variance::VarianceInferable; use crate::types::visitor::{ - TypeCollector, TypeKind, TypeVisitor, any_over_type, walk_non_atomic_type, - walk_type_with_recursion_guard, + TypeCollector, TypeKind, TypeVisitor, walk_non_atomic_type, walk_type_with_recursion_guard, }; use crate::types::{ ApplyTypeMappingVisitor, BoundTypeVarInstance, IntersectionType, Type, TypeContext, @@ -120,10 +116,14 @@ use crate::types::{ }; use crate::{Db, FxIndexMap, FxIndexSet, FxOrderSet, ProgramEnvironment}; +pub(crate) mod paths; pub(crate) mod projection; +mod sequents; mod solutions; mod support; +use paths::PathAssignments; +use sequents::SequentMap; use solutions::SolutionWalker; /// An extension trait for building constraint sets from [`Option`] values. @@ -1426,32 +1426,6 @@ impl<'db> ConstraintSetStorage<'db> { depth } - /// Returns how much sequent fuel is needed to derive this constraint. - /// - /// This cost is driven by two factors. - /// - /// First, nested types containing typevars can produce increasingly complex families of - /// derived constraints. Charge more fuel for those constraints so that each additional level - /// of typevar depth shortens the remaining derivation chain. - /// - /// Second, even without considering typevars, the lower and upper bounds can become more - /// structurally complex. We consider a type to be more complex if it has deeper nesting of - /// type constructors. Each sequent is charged the _increase_ in that complexity between its - /// antecedents and its consequent. (Measuring growth rather than absolute depth avoids - /// penalizing a complex concrete bound that is merely propagated unchanged.) - fn sequent_fuel_cost( - &mut self, - db: &'db dyn Db, - env: &ProgramEnvironment<'db>, - constraint: ConstraintId, - antecedent_constructor_depth: u16, - ) -> u16 { - let (constructor_depth, typevar_depth) = - self.cached_constraint_bound_depth(db, env, constraint); - let constructor_growth = constructor_depth.saturating_sub(antecedent_constructor_depth); - typevar_depth.max(constructor_growth).saturating_add(1) - } - fn cached_constraint_implies( &mut self, db: &'db dyn Db, @@ -1945,52 +1919,6 @@ pub(crate) struct ConstraintBounds<'db> { pub(crate) upper: Option>, } -impl<'db> Type<'db> { - /// Returns whether this type can participate in a transitive sequent proof. - /// - /// Gradual assignability is not transitive, so constraints with dynamic bounds are ineligible. - /// Note that we can't use [`is_fully_static`][Type::is_fully_static] here, since that - /// considers the declared bounds/constraints of typevars. In the context of a sequent map, - /// typevars are opaque symbolic atoms: considering their bounds or defaults could incorrectly - /// make their eligibility depend on a specialization that the sequent is meant to constrain. - fn is_static_sequent_eligible(self, db: &'db dyn Db, env: &ProgramEnvironment<'db>) -> bool { - struct EligibilityVisitor<'a, 'db> { - env: &'a ProgramEnvironment<'db>, - seen: TypeCollector<'db>, - eligible: Cell, - } - - impl<'db> TypeVisitor<'db> for EligibilityVisitor<'_, 'db> { - fn program_environment(&self) -> &ProgramEnvironment<'db> { - self.env - } - - fn should_visit_lazy_type_attributes(&self) -> bool { - false - } - - fn visit_type(&self, db: &'db dyn Db, ty: Type<'db>) { - if !self.eligible.get() || ty.is_type_var() { - return; - } - if ty.is_dynamic() { - self.eligible.set(false); - return; - } - walk_type_with_recursion_guard(db, ty, self, &self.seen); - } - } - - let visitor = EligibilityVisitor { - env, - seen: TypeCollector::default(), - eligible: Cell::new(true), - }; - visitor.visit_type(db, self); - visitor.eligible.get() - } -} - impl<'db> ConstraintBounds<'db> { pub(crate) fn new( lower: Option>, @@ -5105,2334 +5033,280 @@ impl ConstraintAssignment { } } -/// A collection of _sequents_ that describe how the constraints mentioned in a BDD relate to each -/// other. These are used in several BDD operations that need to know about "derived facts" even if -/// they are not mentioned in the BDD directly. These operations involve walking one or more paths -/// from the root node to a terminal node. Each sequent describes paths that are invalid (which are -/// pruned from the search), and new constraints that we can assume to be true even if we haven't -/// seen them directly. +/// A visitor for walking the paths of a BDD. /// -/// Sequent maps are primarily used when walking a BDD path with a [`PathAssignments`]. The -/// `PathAssignments` will hold a sequent map containing all of the constraints that are -/// encountered during the walk. It builds up its sequent map lazily, so that it only has to -/// include sequents for the constraints that are actually encountered. However, we also don't want -/// to perform duplicate work if we perform multiple BDD walks on the same constraint set. The -/// [`for_constraint`][Self::for_constraint] and [`for_constraint_pair`][Self::for_constraint_pair] -/// methods are salsa-tracked, to ensure that we only perform them once for any particular -/// constraint or pair of constraints. `PathAssignments` invokes these methods when it encounters a -/// new constraint, and then merges those cached sequents into its own sequent map. (That means we -/// also share the work of calculating the sequent map across `PathAssignments` for _different_ -/// constraint sets.) -#[derive(Debug, Default)] -struct SequentMap { - sequents: Vec, -} +/// **NOTE**: This trait gives you full control over the walking process: in particular, you have +/// more opportunities to abort the walk early. If you want to perform a simple "fold" over all of +/// the paths, the [`PathFold`] trait is easier to implement, and can also be used as a +/// `PathVisitor`. +/// +/// Each path starts at the root node and ends at a terminal node, and represents one family of +/// typevar assignments described by the BDD. Each path can be either _satisfied_, meaning that +/// this family of assignments is accepted by the constraint set; _unsatisfied_, meaning that this +/// family of assignments is _not_ accepted by the constraint set; or _impossible_, meaning that +/// this family of assignments contains a contradiction, and cannot possibly ever occur. +/// +/// To visit the BDD paths: +/// +/// - We start at the root node. +/// +/// - Each time we encounter an interior node, we call the visitor's `enter_interior` method. We +/// then process walk the interior node's `true`, `uncertain`, and `false` outgoing edges. +/// +/// - To process an edge, we recursively visit the node that the edge points to (getting a `Result` +/// for that subtree), and then call the visitor's `visit_edge` method. This lets you modify the +/// subtree's value based on the assignments that were added to the path by this edge. (This +/// includes at least the constraint checked by the interior node containing this edge, and can +/// also include any additional derived facts that we learn based on whatever other assignments +/// currently hold on the path.) +/// +/// - Once we have processed all of the edges for an interior node, we call the visitor's +/// `leave_interior` method. This lets you combine the `Result`s from each outgoing edge into a +/// single `Result` that represents the subtree rooted at this interior node. +/// +/// Throughout this process, if any of your methods return [`ControlFlow::Break`], we will abort +/// the path walk and immediately return that value. +trait PathVisitor { + type Result; + type Interior; + type Break; -/// Describes one rule for deriving new implicit constraints from existing constraints in a BDD -/// path. -#[derive(Clone, Copy, Debug)] -enum Sequent { - /// Sequent of the form `¬C → false` - /// - /// This indicates that `C` is always true. Any path that assumes it is false is impossible and - /// can be pruned. - SingleTautology { ante: ConstraintId }, + /// Called before visiting any interior or terminal node. Returning `Break` prevents the + /// traversal from entering the node or deriving facts from its outgoing edges. + fn visit_node(&mut self) -> ControlFlow { + ControlFlow::Continue(()) + } - /// Sequent of the form `C₁ ∧ C₂ → false` - /// - /// This indicates that `C₁` and `C₂` are disjoint: it is not possible for both to hold. Any - /// path that assumes both is impossible and can be pruned. - PairImpossibility { - ante1: ConstraintId, - ante2: ConstraintId, - }, + /// Called when we reach the end of a satisfied path. `path` will contain all of the + /// assignments on this path. The `Result` value that you return will be propagated back up as + /// we "unwind" this path. + fn visit_satisfied<'db>( + &mut self, + db: &'db dyn Db, + storage: &mut ConstraintSetStorage<'db>, + path: &PathAssignments, + ) -> ControlFlow; - /// Sequent of the form `C → D` - /// - /// This indicates that `C` on its own is enough to imply `D`. For any path that assumes `C` - /// holds, we can add `D` to the path even if it doesn't appear in the BDD. - SingleImplication { - ante: ConstraintId, - post: ConstraintId, - }, + /// Called when we reach the end of an unsatisfied path. `path` will contain all of the + /// assignments on this path. The `Result` value that you return will be propagated back up as + /// we "unwind" this path. + fn visit_unsatisfied<'db>( + &mut self, + db: &'db dyn Db, + storage: &mut ConstraintSetStorage<'db>, + path: &PathAssignments, + ) -> ControlFlow; - /// Sequent of the form `C₁ ∧ C₂ → D` - /// - /// This indicates that if `C₁` and `C₂` are both true, then `D` is guaranteed to be true as - /// well. For any path that assumes both `C₁` and `C₂` hold, we can add `D` to the path even if - /// it doesn't appear in the BDD. - PairImplication { - ante1: ConstraintId, - ante2: ConstraintId, - post: ConstraintId, - }, -} + /// Called when we determine that a path is impossible, either because its assignments + /// contradict each other, or because an edge is structurally absent (such as the uncertain + /// edge when visiting a negated BDD). The `Result` value that you return will be propagated + /// back up as we "unwind" this path. + fn visit_impossible<'db>( + &mut self, + db: &'db dyn Db, + storage: &mut ConstraintSetStorage<'db>, + path: &PathAssignments, + ) -> ControlFlow; -impl SequentMap { - /// Returns a sequent map containing the sequents that we can infer from a single constraint in - /// isolation. This method is salsa-tracked so that we only perform this work once per - /// constraint. - fn for_constraint<'db, 'c>( + /// Called on the way down as we enter each interior node. You can create a + /// [`Interior`][Self::Interior] value that will be passed to the + /// [`visit_edge`][Self::visit_edge] and [`leave_interior`][Self::leave_interior] methods + /// when we call them for this node. + fn enter_interior<'db>( + &mut self, db: &'db dyn Db, - env: &ProgramEnvironment<'db>, - storage: &'c mut ConstraintSetStorage<'db>, - constraint: ConstraintId, - ) -> &'c Self { - let key = constraint; - if !storage.single_sequent_cache.contains_key(&key) { - tracing::trace!( - target: "ty_python_semantic::types::constraints::SequentMap", - constraint = %constraint.display(db, env, storage), - "add sequents for constraint", - ); - let mut map = SequentMap::default(); - map.add_sequents_for_single(db, env, storage, constraint); - storage.single_sequent_cache.insert(key, map); - } - &storage.single_sequent_cache[&key] - } + storage: &mut ConstraintSetStorage<'db>, + interior_node: InteriorNode, + ) -> ControlFlow; - /// Returns a sequent map containing the sequents that we can infer from a pair of constraints. - /// This method is salsa-tracked so that we only perform this work once per constraint pair. - /// - /// (Note that this method is _not_ commutative; you should provide `left` and `right` in the - /// order that they appear in the source code, so that we can construct derived constraints - /// that retain that ordering.) - fn for_constraint_pair<'db, 'c>( + /// Called once for each edge in the BDD. You are given the [`Result`][Self::Result] value + /// of the subtree that the edge points to, as well as the origin and derived assignments that + /// are added by the edge. + fn visit_edge<'db>( + &mut self, db: &'db dyn Db, - env: &ProgramEnvironment<'db>, - storage: &'c mut ConstraintSetStorage<'db>, - left: ConstraintId, - right: ConstraintId, - ) -> &'c Self { - let key = (left, right); - if !storage.pair_sequent_cache.contains_key(&key) { - tracing::trace!( - target: "ty_python_semantic::types::constraints::SequentMap", - left = %left.display(db, env, storage), - right = %right.display(db, env, storage), - "add sequents for constraint pair", - ); - let mut map = SequentMap::default(); - map.add_sequents_for_pair(db, env, storage, left, right); - storage.pair_sequent_cache.insert(key, map); - } - &storage.pair_sequent_cache[&key] - } + storage: &mut ConstraintSetStorage<'db>, + interior_value: &Self::Interior, + subtree: Self::Result, + path: &PathAssignments, + new_range: Range, + ) -> ControlFlow; - /// Quickly determines whether two constraints cannot possibly produce any sequents when passed - /// to [`for_constraint_pair`][Self::for_constraint_pair]. If this returns `true`, it is safe - /// to skip calling `for_constraint_pair` for this pair of constraints. - fn pair_cannot_produce_sequents<'db>( + /// Called on the way back up as we leave each interior node in the BDD. Combines the + /// [`Result`][Self::Result] values for each of the interior node's subtrees. + fn leave_interior<'db>( + &mut self, db: &'db dyn Db, - env: &ProgramEnvironment<'db>, storage: &mut ConstraintSetStorage<'db>, - left: ConstraintId, - right: ConstraintId, - ) -> bool { - // Currently, the only pattern we look for is when two constraints that have _only_ lower - // bounds, where those lower bounds are disjoint. Given `l₁ ≤ T ∧ l₂ ≤ T`, the only - // sequent we could theoretically produce is `(l₁ | l₂) ≤ T`. But we don't store that as a - // single constraint; we always break that apart into the two smaller constraints that we - // started with. - - let left = storage.constraint_data(left); - let right = storage.constraint_data(right); - if !left.typevar.is_same_typevar_as(db, right.typevar) { - return false; - } + interior_value: &Self::Interior, + if_true: Self::Result, + if_uncertain: Self::Result, + if_false: Self::Result, + ) -> ControlFlow; +} - let (Some(left_lower), Some(right_lower)) = (left.bounds.lower, right.bounds.lower) else { - return false; - }; - if left.bounds.upper.is_some() || right.bounds.upper.is_some() { - return false; - } - let left_lower = left_lower.ty(); - let right_lower = right_lower.ty(); +/// A visitor for "folding" over the paths in a BDD, producing a single value that summarizes all +/// of them. +/// +/// This is a simpler trait to implement when you don't need as much control over the path walk. +/// Any type that implements this trait can also be used as a [`PathVisitor`]. +trait PathFold { + type Result; + type Break; - // This call might need its own borrow of the builder's storage, so create a new builder - // that it can use. - let builder = ConstraintSetBuilder::new(); - left_lower - .when_trivially_disjoint_from(db, env, right_lower, &builder, TypeVarSet::None) - .is_trivially_always_satisfied() - } + /// Returns the base case value that represents a satisfied path. + fn satisfied<'db>( + &mut self, + db: &'db dyn Db, + storage: &mut ConstraintSetStorage<'db>, + path: &PathAssignments, + ) -> ControlFlow; - fn add_single_tautology(&mut self, ante: ConstraintId) { - self.sequents.push(Sequent::SingleTautology { ante }); - } + /// Returns the base case value that represents an unsatisfied path. + fn unsatisfied<'db>( + &mut self, + db: &'db dyn Db, + storage: &mut ConstraintSetStorage<'db>, + path: &PathAssignments, + ) -> ControlFlow; - fn add_pair_impossibility(&mut self, ante1: ConstraintId, ante2: ConstraintId) { - self.sequents - .push(Sequent::PairImpossibility { ante1, ante2 }); - } + /// Returns the base case value that represents an impossible path. + fn impossible<'db>( + &mut self, + db: &'db dyn Db, + storage: &mut ConstraintSetStorage<'db>, + path: &PathAssignments, + ) -> ControlFlow; - fn add_pair_implication<'db>( + /// Combines the values for each subtree of an interior node, returning a value that represents + /// the subtree rooted at that node. + fn combine<'db>( &mut self, db: &'db dyn Db, - env: &ProgramEnvironment<'db>, storage: &mut ConstraintSetStorage<'db>, - ante1: ConstraintId, - ante2: ConstraintId, - post: ConstraintId, - ) { - // If the post constraint is unsatisfiable, then the antecedents contradict each other. - let post_data = storage.constraint_data(post); - let post_lower = post_data.bounds.lower_bound().ty(); - let post_upper = post_data.bounds.upper_bound().ty(); - let (when, source_order) = storage.load( - db, - env, - &post_lower.when_constraint_set_assignable_to_owned(db, env, post_upper), - ); - if when.is_never_satisfied(db, env, storage, source_order) { - self.add_pair_impossibility(ante1, ante2); - return; - } + if_true: Self::Result, + if_uncertain: Self::Result, + if_false: Self::Result, + ) -> ControlFlow; +} - // If either antecedent implies the consequent on its own, this new sequent is redundant. - if ante1.implies(db, env, storage, post) || ante2.implies(db, env, storage, post) { - return; - } +impl PathVisitor for T +where + T: PathFold, +{ + type Result = ::Result; + type Interior = (); + type Break = ::Break; - self.sequents - .push(Sequent::PairImplication { ante1, ante2, post }); + fn visit_satisfied<'db>( + &mut self, + db: &'db dyn Db, + storage: &mut ConstraintSetStorage<'db>, + path: &PathAssignments, + ) -> ControlFlow { + PathFold::satisfied(self, db, storage, path) } - fn add_single_implication(&mut self, ante: ConstraintId, post: ConstraintId) { - if ante == post { - return; - } - - self.sequents - .push(Sequent::SingleImplication { ante, post }); + fn visit_unsatisfied<'db>( + &mut self, + db: &'db dyn Db, + storage: &mut ConstraintSetStorage<'db>, + path: &PathAssignments, + ) -> ControlFlow { + PathFold::unsatisfied(self, db, storage, path) } - fn add_sequents_for_single<'db>( + fn visit_impossible<'db>( &mut self, db: &'db dyn Db, - env: &ProgramEnvironment<'db>, storage: &mut ConstraintSetStorage<'db>, - constraint: ConstraintId, - ) { - // If this constraint binds its typevar to `Never ≤ T ≤ object`, then the typevar can take - // on any type, and the constraint is always satisfied. - let constraint_data = storage.constraint_data(constraint); - let lower = constraint_data.bounds.lower_bound().ty(); - let upper = constraint_data.bounds.upper_bound().ty(); - if lower.is_never() && upper.is_object() { - self.add_single_tautology(constraint); - return; - } + path: &PathAssignments, + ) -> ControlFlow { + PathFold::impossible(self, db, storage, path) + } - // Given a constraint `L ≤ T ≤ U`, `L ≤ U` must also hold. If those bounds contain other - // typevars, we can infer additional constraints. This is easiest to see when the bounds - // _are_ typevars: - // - // 1. `(S ≤ T ≤ U) → (S ≤ U)` - // 2. `(S ≤ T ≤ τ) → (S ≤ τ)` - // 3. `(τ ≤ T ≤ U) → (τ ≤ U)` - // - // but it also holds when the bounds _contain_ typevars: - // - // 4. `(Covariant[S] ≤ T ≤ Covariant[U]) → (S ≤ U)` - // `(Covariant[S] ≤ T ≤ Covariant[τ]) → (S ≤ τ)` - // `(Covariant[τ] ≤ T ≤ Covariant[U]) → (τ ≤ U)` - // - // 5. `(Contravariant[S] ≤ T ≤ Contravariant[U]) → (U ≤ S)` - // `(Contravariant[S] ≤ T ≤ Contravariant[τ]) → (τ ≤ S)` - // `(Contravariant[τ] ≤ T ≤ Contravariant[U]) → (U ≤ τ)` - // - // 6. `(Invariant[S] ≤ T ≤ Invariant[U]) → (S = U)` - // `(Invariant[S] ≤ T ≤ Invariant[τ]) → (S = τ)` - // `(Invariant[τ] ≤ T ≤ Invariant[U]) → (τ = U)` - // - // and whenever the bounds are assignable, even if they don't mention exactly the same - // types: - // - // class Sub(Covariant[int]): ... - // - // 7. `(Covariant[S] ≤ T ≤ Sub) → (S ≤ int)` - // `(Sub ≤ T ≤ Covariant[U]) → (int ≤ U)` - // - // To handle all of these cases, we perform a constraint set assignability check to see - // when `L ≤ U`. This gives us a constraint set, which should be the rhs of the sequent - // implication. (That is, this check directly encodes `(L ≤ T ≤ U) → (L ≤ U)` as an - // implication.) - - // Skip trivial cases where the assignability check won't produce useful results. - if lower.is_never() || upper.is_object() { - return; - } - - let (when, source_order) = storage.load( - db, - env, - &lower.when_constraint_set_assignable_to_owned(db, env, upper), - ); - - // If L is _never_ assignable to U, this constraint would violate transitivity, and should - // never have been added. - #[expect(clippy::debug_assert_with_mut_call)] - { - debug_assert!(!when.is_never_satisfied(db, env, storage, source_order)); - } - - // Fast path: If L is trivially always assignable to U, there are no derived constraints - // that we can infer. This would be handled correctly by the logic below, but this is a - // useful early return. Since we only use this check as an early return happy path, we can - // accept false negatives. That lets us use the simpler and cheaper check against - // ALWAYS_TRUE, rather than a more expensive is_always_satisfiable call. - if when == ALWAYS_TRUE { - return; - } - - // Technically, we've just calculated a _constraint set_ as the rhs of this implication. - // Unfortunately, our sequent map can currently only store implications where the rhs is a - // single constraint. - // - // If the constraint set that we get represents a single conjunction, we can still shoehorn - // it into this shape, since we can "break apart" a conjunction on the rhs of an - // implication: - // - // a → b ∧ c ∧ d - // - // becomes - // - // a → b - // a → c - // a → d - // - // That takes care of breaking apart the rhs conjunction: we can add each positive - // constraint as a separate single_implication. - // - // We can also handle _negative_ constraints, because those turn into impossibilities: - // - // a → ¬b - // - // becomes - // - // a ∧ b → false - // - // TODO: This should handle the most common cases. In the future, we could handle arbitrary - // rhs constraint sets by moving this logic into PathAssignments::walk_path, and performing - // it once for _every_ root→always path in the BDD. (That would require resetting the - // PathAssignments state for each of those paths, which is why the logic would have to - // move.) - let mut node = when; - if !node.is_single_conjunction(storage) { - return; - } - - loop { - match node.node() { - Node::AlwaysTrue | Node::AlwaysFalse => break, - Node::Interior(interior) => { - let interior = storage.interior_node_data(interior.node()); - let derived = storage.constraint_data(interior.constraint); - let derived = ConstraintId::new_with_bounds( - db, - env, - storage, - derived.typevar, - derived - .bounds - .lower - .map(|bound| bound.with_source_provenance(constraint_data.bounds)), - derived - .bounds - .upper - .map(|bound| bound.with_source_provenance(constraint_data.bounds)), - ); - if interior.if_true != ALWAYS_FALSE { - self.add_single_implication(constraint, derived); - node = interior.if_true; - } else { - self.add_pair_impossibility(constraint, derived); - node = interior.if_false; - } - } - } - } - } - - fn add_sequents_for_pair<'db>( - &mut self, - db: &'db dyn Db, - env: &ProgramEnvironment<'db>, - storage: &mut ConstraintSetStorage<'db>, - left_constraint: ConstraintId, - right_constraint: ConstraintId, - ) { - // If either of the constraints has another typevar as a lower/upper bound, the only - // sequents we can add are for the transitive closure. For instance, if we have - // `(S ≤ T) ∧ (T ≤ int)`, then `(S ≤ int)` will also hold, and we should add a sequent for - // this implication. These are the `mutual_sequents` mentioned below — sequents that come - // about because two typevars are mutually constrained. - // - // Complicating things is that `(S ≤ T)` will be encoded differently depending on how `S` - // and `T` compare in our arbitrary BDD variable ordering. - // - // When `S` comes before `T`, `(S ≤ T)` will be encoded as `(Never ≤ S ≤ T)`, and the - // overall antecedent will be `(Never ≤ S ≤ T) ∧ (T ≤ int)`. Those two individual - // constraints constrain different typevars (`S` and `T`, respectively), and are handled by - // `add_mutual_sequents_for_different_typevars`. - // - // When `T` comes before `S`, `(S ≤ T)` will be encoded as `(S ≤ T ≤ object)`, and the - // overall antecedent will be `(S ≤ T ≤ object) ∧ (T ≤ int)`. Those two individual - // constraints both constrain `T`, and are handled by - // `add_mutual_sequents_for_same_typevars`. - // - // If all of the lower and upper bounds are concrete (i.e., not typevars), then there - // several _other_ sequents that we can add, as handled by `add_concrete_sequents`. - let left_constraint_data = storage.constraint_data(left_constraint); - let left_typevar = left_constraint_data.typevar; - let right_constraint_data = storage.constraint_data(right_constraint); - let right_typevar = right_constraint_data.typevar; - - if !left_typevar.is_same_typevar_as(db, right_typevar) { - self.add_mutual_sequents_for_different_typevars( - db, - env, - storage, - left_constraint, - right_constraint, - ); - self.add_nested_typevar_sequents(db, env, storage, left_constraint, right_constraint); - } else if left_constraint_data.bounds.lower_bound().ty().is_type_var() - || left_constraint_data.bounds.upper_bound().ty().is_type_var() - || right_constraint_data - .bounds - .lower_bound() - .ty() - .is_type_var() - || right_constraint_data - .bounds - .upper_bound() - .ty() - .is_type_var() - { - self.add_mutual_sequents_for_same_typevars( - db, - env, - storage, - left_constraint, - right_constraint, - ); - } else { - self.add_concrete_sequents(db, env, storage, left_constraint, right_constraint); - } - } - - fn add_mutual_sequents_for_different_typevars<'db>( - &mut self, - db: &'db dyn Db, - env: &ProgramEnvironment<'db>, - storage: &mut ConstraintSetStorage<'db>, - left_constraint: ConstraintId, - right_constraint: ConstraintId, - ) { - // We've structured our constraints so that a typevar's upper/lower bound can only - // be another typevar if the bound is "later" in our arbitrary ordering. That means - // we only have to check this pair of constraints in one direction — though we do - // have to figure out which of the two typevars is constrained, and which one is - // the upper/lower bound. - let left_constraint_data = storage.constraint_data(left_constraint); - let left_typevar = left_constraint_data.typevar; - let right_constraint_data = storage.constraint_data(right_constraint); - let right_typevar = right_constraint_data.typevar; - let (bound_constraint, constrained_constraint) = - if left_typevar.can_be_bound_for(db, storage, right_typevar) { - (left_constraint, right_constraint) - } else { - (right_constraint, left_constraint) - }; - - // We then look for cases where the "constrained" typevar's upper and/or lower bound - // matches the "bound" typevar. If so, we're going to add an implication sequent that - // replaces the upper/lower bound that matched with the bound constraint's corresponding - // bound. - let bound_constraint_data = storage.constraint_data(bound_constraint); - let bound_typevar = bound_constraint_data.typevar; - let constrained_constraint_data = storage.constraint_data(constrained_constraint); - let constrained_typevar = constrained_constraint_data.typevar; - let constrained_lower_bound = constrained_constraint_data.bounds.lower_bound(); - let constrained_upper_bound = constrained_constraint_data.bounds.upper_bound(); - let bound_lower_bound = bound_constraint_data.bounds.lower_bound(); - let bound_upper_bound = bound_constraint_data.bounds.upper_bound(); - - // Transitive pivots require subtyping; classes with dynamic bases can be assignable to - // unrelated types without being subtypes. - let (new_lower, new_upper) = match ( - constrained_lower_bound.ty(), - constrained_upper_bound.ty(), - bound_lower_bound.ty(), - bound_upper_bound.ty(), - ) { - // (B ≤ C ≤ B) ∧ (BL ≤ B ≤ BU) → (BL ≤ C ≤ BU) - (Type::TypeVar(constrained_lower), Type::TypeVar(constrained_upper), _, _) - if constrained_lower.is_same_typevar_as(db, bound_typevar) - && constrained_upper.is_same_typevar_as(db, bound_typevar) => - { - ( - ConstraintBound::from_transitive_derivation( - bound_lower_bound.ty(), - constrained_lower_bound, - bound_lower_bound, - ), - ConstraintBound::from_transitive_derivation( - bound_upper_bound.ty(), - constrained_upper_bound, - bound_upper_bound, - ), - ) - } - - // (CL ≤ C ≤ B) ∧ (BL ≤ B ≤ BU) → (CL ≤ C ≤ BU) - (_, Type::TypeVar(constrained_upper), _, _) - if constrained_upper.is_same_typevar_as(db, bound_typevar) => - { - ( - constrained_lower_bound, - ConstraintBound::from_transitive_derivation( - bound_upper_bound.ty(), - constrained_upper_bound, - bound_upper_bound, - ), - ) - } - - // (B ≤ C ≤ CU) ∧ (BL ≤ B ≤ BU) → (BL ≤ C ≤ CU) - (Type::TypeVar(constrained_lower), _, _, _) - if constrained_lower.is_same_typevar_as(db, bound_typevar) => - { - ( - ConstraintBound::from_transitive_derivation( - bound_lower_bound.ty(), - constrained_lower_bound, - bound_lower_bound, - ), - constrained_upper_bound, - ) - } - - // (CL ≤ C ≤ pivot) ∧ (pivot ≤ B ≤ BU) → (CL ≤ C ≤ B) - (_, constrained_upper, bound_lower, _) - if !constrained_upper.is_never() - && !constrained_upper.is_object() - && storage.cached_is_constraint_set_subtype_of( - db, - env, - constrained_upper.top_materialization(db, env), - bound_lower.bottom_materialization(db, env), - ) => - { - ( - constrained_lower_bound, - ConstraintBound::from_transitive_derivation( - Type::TypeVar(bound_typevar), - constrained_upper_bound, - bound_lower_bound, - ), - ) - } - - // (pivot ≤ C ≤ CU) ∧ (BL ≤ B ≤ pivot) → (B ≤ C ≤ CU) - (constrained_lower, _, _, bound_upper) - if !constrained_lower.is_never() - && !constrained_lower.is_object() - && storage.cached_is_constraint_set_subtype_of( - db, - env, - bound_upper.top_materialization(db, env), - constrained_lower.bottom_materialization(db, env), - ) => - { - ( - ConstraintBound::from_transitive_derivation( - Type::TypeVar(bound_typevar), - constrained_lower_bound, - bound_upper_bound, - ), - constrained_upper_bound, - ) - } - - _ => return, - }; - - let mut post_constraints: SmallVec<[ConstraintId; 3]> = SmallVec::new(); - // These are derived logical constraints, not direct inference evidence. Avoid preserving - // explicit bounds that are equivalent to missing lower/upper bounds, so a derived - // `T ≤ U ≤ object` can satisfy a later query for `T ≤ U` without requiring a separate - // materialized-default implication. - let mut constrained_lower = (!new_lower.ty().is_never()).then_some(new_lower); - let mut constrained_upper = (!new_upper.ty().is_object()).then_some(new_upper); - - // The transitive rule above gives us an intended post-condition - // `new_lower ≤ [constrained] ≤ new_upper`. - // - // If a top-level bound typevar is "earlier" than `constrained`, we cannot represent that - // directly as a bound on `constrained` without violating our canonical ordering. - // Instead, split it into equivalent canonical constraints by "moving" that bound onto the - // other typevar: - // - // invalid lower `L ≤ [C]` -> `(Never ≤ [L] ≤ C)` and drop `L` from C's lower bound - // invalid upper `[C] ≤ U` -> `(C ≤ [U] ≤ object)` and drop `U` from C's upper bound - // - // Example: if we derive `[A] ≤ T ≤ [B]` but `A`/`B` are not valid top-level bounds for - // `T` in this ordering, we emit two pair implications: - // `(Never ≤ [A] ≤ T)` and `(T ≤ [B] ≤ object)`. - // This preserves the relationship while keeping all derived constraints canonical. - if let Type::TypeVar(lower_bound_typevar) = new_lower.ty() - && !lower_bound_typevar.can_be_bound_for(db, storage, constrained_typevar) - { - post_constraints.push(ConstraintId::new_with_bounds( - db, - env, - storage, - lower_bound_typevar, - None, - Some(new_lower.with_type(Type::TypeVar(constrained_typevar))), - )); - constrained_lower = None; - } - - if let Type::TypeVar(upper_bound_typevar) = new_upper.ty() - && !upper_bound_typevar.can_be_bound_for(db, storage, constrained_typevar) - { - post_constraints.push(ConstraintId::new_with_bounds( - db, - env, - storage, - upper_bound_typevar, - Some(new_upper.with_type(Type::TypeVar(constrained_typevar))), - None, - )); - constrained_upper = None; - } - - if constrained_lower.is_some() || constrained_upper.is_some() { - post_constraints.push(ConstraintId::new_with_bounds( - db, - env, - storage, - constrained_typevar, - constrained_lower, - constrained_upper, - )); - } - - for post_constraint in post_constraints { - self.add_pair_implication( - db, - env, - storage, - left_constraint, - right_constraint, - post_constraint, - ); - } - } - - /// Adds sequents for the case where one constraint's lower or upper bound contains another - /// constraint's typevar nested inside a parameterized type (e.g., `U ≤ Covariant[T]`). - /// - /// This is distinct from `add_mutual_sequents_for_different_typevars`, which handles the case - /// where a typevar appears _directly_ as a top-level lower/upper bound (e.g., `U ≤ T`). A - /// bare `Type::TypeVar` is technically a special case of covariant nesting (since the variance - /// of `T` in `T` itself is covariant), but the existing direct-typevar logic handles it - /// separately because it requires careful canonical ordering of typevar-to-typevar constraints - /// that the generic nested-typevar logic here does not need to worry about. - fn add_nested_typevar_sequents<'db>( - &mut self, - db: &'db dyn Db, - env: &ProgramEnvironment<'db>, - storage: &mut ConstraintSetStorage<'db>, - left_constraint: ConstraintId, - right_constraint: ConstraintId, - ) { - // Keep this precheck aligned with `variance_of`, which visits lazy types. - let has_typevar_bound = |bounds: ConstraintBounds<'db>| { - bounds - .lower - .is_some_and(|lower| any_over_type(db, env, lower.ty(), true, Type::is_type_var)) - || bounds.upper.is_some_and(|upper| { - any_over_type(db, env, upper.ty(), true, Type::is_type_var) - }) - }; - if !has_typevar_bound(storage.constraint_data(left_constraint).bounds) - && !has_typevar_bound(storage.constraint_data(right_constraint).bounds) - { - return; - } - - let mut try_tightening = - |bound_constraint: ConstraintId, constrained_constraint: ConstraintId| { - let bound_data = storage.constraint_data(bound_constraint); - let bound_typevar = bound_data.typevar; - let bound_identity = bound_typevar.identity(db); - let bound_lower_bound = bound_data.bounds.lower_bound(); - let bound_upper_bound = bound_data.bounds.upper_bound(); - let constrained_data = storage.constraint_data(constrained_constraint); - let constrained_typevar = constrained_data.typevar; - let constrained_identity = constrained_typevar.identity(db); - let constrained_lower_bound = constrained_data.bounds.lower_bound(); - let constrained_upper_bound = constrained_data.bounds.upper_bound(); - let constrained_lower = constrained_lower_bound.ty(); - let constrained_upper = constrained_upper_bound.ty(); - - // If the replacement contains the bound typevar itself (e.g., the bound - // constraint is `_V ≤ G[_V]`), or the constrained typevar (e.g., the bound - // constraint is `_T ≤ G[_V]` and we're about to substitute into `_V ≤ G[_T]`), - // substituting would create a deeper nesting of the same recursive pattern - // that triggers the same substitution again ad infinitum. Skip in both cases. - // - // Fast-path bare typevar replacements (`Type::TypeVar`) using equality checks - // instead of calling `variance_of` on them. This avoids a large number of tiny - // tracked `variance_of` queries in hot paths. - let replacement_mentions_bound_or_constrained = |replacement: Type<'db>| { - replacement.variance_of(db, env, bound_identity) != TypeVarVariance::Bivariant - || replacement.variance_of(db, env, constrained_identity) - != TypeVarVariance::Bivariant - }; - - // Check the upper bound of the constrained constraint for nested occurrences of - // the bound typevar. We use `variance_of` as our combined presence + variance - // check: `Bivariant` means the typevar doesn't appear in the type (or is genuinely - // bivariant, which is semantically equivalent — no implication is needed in either - // case). - // - // Note: if `Bivariant` is ever removed from the `TypeVarVariance` enum, we would - // need an alternative representation for "typevar not present" - // (e.g., `Option`). - let upper_replacement = match ( - constrained_upper.variance_of(db, env, bound_identity), - bound_lower_bound.ty(), - bound_upper_bound.ty(), - ) { - (TypeVarVariance::Bivariant, _, _) => None, - // Skip bare typevars — those are handled by - // `add_mutual_sequents_for_different_typevars`. - _ if constrained_upper.is_type_var() => None, - // Covariance preserves direction: upper bound on T substitutes into upper - // bound. A ≤ B → G[A] ≤ G[B], so (T ≤ u_B) gives G[T] ≤ G[u_B]. - (TypeVarVariance::Covariant, _, bound_upper) if !bound_upper.is_object() => { - Some(bound_upper_bound) - } - // Contravariance flips direction: lower bound on T substitutes into upper - // bound. A ≤ B → G[B] ≤ G[A], so (l_B ≤ T) gives G[T] ≤ G[l_B]. - (TypeVarVariance::Contravariant, bound_lower, _) if !bound_lower.is_never() => { - Some(bound_lower_bound) - } - // Invariance requires equality: only substitute if l_B = u_B. - (TypeVarVariance::Invariant, bound_lower, bound_upper) - if bound_lower == bound_upper && !bound_lower.is_never() => - { - Some(ConstraintBound::from_combination( - bound_lower, - bound_lower_bound, - bound_upper_bound, - )) - } - _ => None, - }; - let upper_replacement = upper_replacement.filter(|replacement| { - // Substituting one typevar for another into large unions can generate many - // very-weak derived constraints and cause severe performance regressions. - // Keep the common/non-union case enabled; skip union upper bounds for this - // specific typevar-to-typevar replacement shape. - if replacement.ty().is_type_var() && constrained_upper.is_union() { - return false; - } - !replacement_mentions_bound_or_constrained(replacement.ty()) - }); - if let Some(replacement) = upper_replacement { - let new_upper = constrained_upper.substitute_one_typevar( - db, - env, - bound_typevar, - replacement.ty(), - ); - if new_upper != constrained_upper { - let post = ConstraintId::new_with_bounds( - db, - env, - storage, - constrained_typevar, - constrained_data.bounds.lower, - Some(ConstraintBound::from_transitive_derivation( - new_upper, - constrained_upper_bound, - replacement, - )), - ); - self.add_pair_implication( - db, - env, - storage, - bound_constraint, - constrained_constraint, - post, - ); - } - } - - // Check the lower bound of the constrained constraint for nested occurrences. - let lower_replacement = match ( - constrained_lower.variance_of(db, env, bound_identity), - bound_lower_bound.ty(), - bound_upper_bound.ty(), - ) { - (TypeVarVariance::Bivariant, _, _) => None, - _ if constrained_lower.is_type_var() => None, - // Covariance preserves direction: lower bound on T substitutes into lower - // bound. A ≤ B → G[A] ≤ G[B], so (l_B ≤ T) gives G[l_B] ≤ G[T]. - (TypeVarVariance::Covariant, bound_lower, _) if !bound_lower.is_never() => { - Some(bound_lower_bound) - } - // Contravariance flips direction: upper bound on T substitutes into lower - // bound. A ≤ B → G[B] ≤ G[A], so (T ≤ u_B) gives G[u_B] ≤ G[T]. - (TypeVarVariance::Contravariant, _, bound_upper) - if !bound_upper.is_object() => - { - Some(bound_upper_bound) - } - // Invariance requires equality: only substitute if l_B = u_B. - (TypeVarVariance::Invariant, bound_lower, bound_upper) - if bound_lower == bound_upper && !bound_lower.is_never() => - { - Some(ConstraintBound::from_combination( - bound_lower, - bound_lower_bound, - bound_upper_bound, - )) - } - _ => None, - }; - let lower_replacement = lower_replacement.filter(|replacement| { - // Substituting one typevar for another into large intersections can generate - // many very-weak derived constraints and cause severe performance regressions. - // Keep the common/non-intersection case enabled; skip intersection lower - // bounds for this specific typevar-to-typevar replacement shape. - if replacement.ty().is_type_var() && constrained_lower.is_intersection() { - return false; - } - !replacement_mentions_bound_or_constrained(replacement.ty()) - }); - if let Some(replacement) = lower_replacement { - let new_lower = constrained_lower.substitute_one_typevar( - db, - env, - bound_typevar, - replacement.ty(), - ); - if new_lower != constrained_lower { - let post = ConstraintId::new_with_bounds( - db, - env, - storage, - constrained_typevar, - Some(ConstraintBound::from_transitive_derivation( - new_lower, - constrained_lower_bound, - replacement, - )), - constrained_data.bounds.upper, - ); - self.add_pair_implication( - db, - env, - storage, - bound_constraint, - constrained_constraint, - post, - ); - } - } - }; - - try_tightening(left_constraint, right_constraint); - try_tightening(right_constraint, left_constraint); - - // Additionally, check if one constraint's bare typevar *bound* appears nested in the other - // constraint's bounds. This handles the "dual" direction: instead of substituting a - // typevar's concrete bounds into another constraint (tightening), we substitute the - // typevar itself for one of its bare typevar bounds (weakening), creating a cross-typevar - // link. - // - // For example, given `(Covariant[S] ≤ C) ∧ (Never ≤ B ≤ S)`, S is B's upper bound and - // appears covariantly in C's lower bound. Since `B ≤ S`, covariance tells us that - // `Covariant[B] ≤ Covariant[S]`. Transitivity then lets us derive `Covariant[B] ≤ C`. - // - // The derived constraint is weaker than the original, but it introduces a relationship - // between B and C that we need to remember and propagate if we ever existentially quantify - // away S. - // - // TODO: This only handles the case where the bound (in this case, S) is a bare typevar. A - // future extension could handle arbitrary types by pattern-matching on generic alias - // structure. - // - // This is defined as a separate closure because it iterates over the bound constraint's - // bare typevar bounds, which is a different axis than `try_tightening`'s check on the - // bound constraint's typevar. - let mut try_weakening = - |bound_constraint: ConstraintId, constrained_constraint: ConstraintId| { - let bound_data = storage.constraint_data(bound_constraint); - let bound_typevar = bound_data.typevar; - let bound_lower_bound = bound_data.bounds.lower_bound(); - let bound_upper_bound = bound_data.bounds.upper_bound(); - let bound_lower = bound_lower_bound.ty(); - let constrained_data = storage.constraint_data(constrained_constraint); - let constrained_typevar = constrained_data.typevar; - let constrained_lower_bound = constrained_data.bounds.lower_bound(); - let constrained_upper_bound = constrained_data.bounds.upper_bound(); - let constrained_lower = constrained_lower_bound.ty(); - let constrained_upper = constrained_upper_bound.ty(); - - let mut try_one_bound = |bound: ConstraintBound<'db>, is_upper_bound: bool| { - let Some(nested_typevar) = bound.ty().as_typevar() else { - return; - }; - - // Skip if the nested typevar is the same as the constrained typevar — that - // case is handled by `add_mutual_sequents_for_different_typevars`. - if nested_typevar.is_same_typevar_as(db, constrained_typevar) - || nested_typevar.is_same_typevar_as(db, bound_typevar) - { - return; - } - - let replacement = Type::TypeVar(bound_typevar); - - // Check the constrained constraint's upper bound for nested occurrences of - // nested_typevar (S). We want to *weaken* (relax) the upper bound by making it - // larger: - // - Covariant + S is B's lower bound (S ≤ B): G[S] ≤ G[B] → weaker. Emit. - // - Contravariant + S is B's upper bound (B ≤ S): G[S] ≤ G[B] → weaker. Emit. - // - Other combinations tighten rather than weaken. Skip. - let should_weaken_upper = !constrained_upper.is_type_var() - && !constrained_upper.is_never() - && !constrained_upper.is_object() - && !constrained_upper.is_dynamic() - && match constrained_upper.variance_of(db, env, nested_typevar.identity(db)) - { - TypeVarVariance::Bivariant => false, - TypeVarVariance::Covariant => !is_upper_bound, - TypeVarVariance::Contravariant => is_upper_bound, - TypeVarVariance::Invariant => { - bound_lower_bound.ty() == bound_upper_bound.ty() - && !bound_lower.is_never() - } - }; - if should_weaken_upper { - let new_upper = constrained_upper.substitute_one_typevar( - db, - env, - nested_typevar, - replacement, - ); - if new_upper != constrained_upper { - let post = ConstraintId::new_with_bounds( - db, - env, - storage, - constrained_typevar, - constrained_data.bounds.lower, - Some(ConstraintBound::from_transitive_derivation( - new_upper, - constrained_upper_bound, - bound, - )), - ); - self.add_pair_implication( - db, - env, - storage, - bound_constraint, - constrained_constraint, - post, - ); - } - } - - // Ditto for the lower bound. - let should_weaken_lower = !constrained_lower.is_type_var() - && !constrained_lower.is_never() - && !constrained_lower.is_object() - && !constrained_lower.is_dynamic() - && match constrained_lower.variance_of(db, env, nested_typevar.identity(db)) - { - TypeVarVariance::Bivariant => false, - TypeVarVariance::Covariant => is_upper_bound, - TypeVarVariance::Contravariant => !is_upper_bound, - TypeVarVariance::Invariant => { - bound_lower_bound.ty() == bound_upper_bound.ty() - && !bound_lower.is_never() - } - }; - if should_weaken_lower { - let new_lower = constrained_lower.substitute_one_typevar( - db, - env, - nested_typevar, - replacement, - ); - if new_lower != constrained_lower { - let post = ConstraintId::new_with_bounds( - db, - env, - storage, - constrained_typevar, - Some(ConstraintBound::from_transitive_derivation( - new_lower, - constrained_lower_bound, - bound, - )), - constrained_data.bounds.upper, - ); - self.add_pair_implication( - db, - env, - storage, - bound_constraint, - constrained_constraint, - post, - ); - } - } - }; - - // For each bare typevar bound S of the bound constraint, check if S appears - // nested in the constrained constraint's bounds. If so, we can substitute B - // (the bound constraint's typevar) for S, producing a weaker but useful - // constraint. - if let Some(upper) = bound_data.bounds.upper { - try_one_bound(upper, true); - } - if let Some(lower) = bound_data.bounds.lower { - try_one_bound(lower, false); - } - }; - - try_weakening(left_constraint, right_constraint); - try_weakening(right_constraint, left_constraint); - } - - fn add_mutual_sequents_for_same_typevars<'db>( - &mut self, - db: &'db dyn Db, - env: &ProgramEnvironment<'db>, - storage: &mut ConstraintSetStorage<'db>, - left_constraint: ConstraintId, - right_constraint: ConstraintId, - ) { - let mut try_one_direction = - |left_constraint: ConstraintId, right_constraint: ConstraintId| { - let left_constraint_data = storage.constraint_data(left_constraint); - let left_lower = left_constraint_data.bounds.lower_bound(); - let left_upper = left_constraint_data.bounds.upper_bound(); - let right_constraint_data = storage.constraint_data(right_constraint); - let right_lower = right_constraint_data.bounds.lower_bound(); - let right_upper = right_constraint_data.bounds.upper_bound(); - let mut new_constraints = - |bound_typevar: BoundTypeVarInstance<'db>, - mut right_lower: Option>, - mut right_upper: Option>| { - if let Some(right_lower_bound) = right_lower - && let Type::TypeVar(other_bound_typevar) = right_lower_bound.ty() - && bound_typevar.is_same_typevar_as(db, other_bound_typevar) - { - right_lower = None; - } - if let Some(right_upper_bound) = right_upper - && let Type::TypeVar(other_bound_typevar) = right_upper_bound.ty() - && bound_typevar.is_same_typevar_as(db, other_bound_typevar) - { - right_upper = None; - } - - // Same idea as `add_mutual_sequents_for_different_typevars`: if a derived - // post-condition for `[bound]` has top-level typevar bounds in the wrong - // orientation, split it into equivalent canonical constraints instead of - // dropping it. - let mut post_constraints: SmallVec<[ConstraintId; 3]> = SmallVec::new(); - // These are derived logical constraints, not direct inference evidence. - // Avoid preserving explicit bounds that are equivalent to missing - // lower/upper bounds; direct constraints still retain their explicit - // bound presence. - let mut constrained_lower = - right_lower.filter(|bound| !bound.ty().is_never()); - let mut constrained_upper = - right_upper.filter(|bound| !bound.ty().is_object()); - - if let Some(right_lower_bound) = right_lower - && let Type::TypeVar(lower_bound_typevar) = right_lower_bound.ty() - && !lower_bound_typevar.can_be_bound_for(db, storage, bound_typevar) - { - post_constraints.push(ConstraintId::new_with_bounds( - db, - env, - storage, - lower_bound_typevar, - None, - Some(right_lower_bound.with_type(Type::TypeVar(bound_typevar))), - )); - constrained_lower = None; - } - - if let Some(right_upper_bound) = right_upper - && let Type::TypeVar(upper_bound_typevar) = right_upper_bound.ty() - && !upper_bound_typevar.can_be_bound_for(db, storage, bound_typevar) - { - post_constraints.push(ConstraintId::new_with_bounds( - db, - env, - storage, - upper_bound_typevar, - Some(right_upper_bound.with_type(Type::TypeVar(bound_typevar))), - None, - )); - constrained_upper = None; - } - - if constrained_lower.is_some() || constrained_upper.is_some() { - post_constraints.push(ConstraintId::new_with_bounds( - db, - env, - storage, - bound_typevar, - constrained_lower, - constrained_upper, - )); - } - - post_constraints - }; - let post_constraints = match (left_lower.ty(), left_upper.ty()) { - (Type::TypeVar(bound_typevar), Type::TypeVar(other_bound_typevar)) - if bound_typevar.is_same_typevar_as(db, other_bound_typevar) => - { - new_constraints( - bound_typevar, - Some(ConstraintBound::from_transitive_derivation( - right_lower.ty(), - left_lower, - right_lower, - )), - Some(ConstraintBound::from_transitive_derivation( - right_upper.ty(), - left_upper, - right_upper, - )), - ) - } - (Type::TypeVar(bound_typevar), _) => new_constraints( - bound_typevar, - None, - Some(ConstraintBound::from_transitive_derivation( - right_upper.ty(), - left_lower, - right_upper, - )), - ), - (_, Type::TypeVar(bound_typevar)) => new_constraints( - bound_typevar, - Some(ConstraintBound::from_transitive_derivation( - right_lower.ty(), - left_upper, - right_lower, - )), - None, - ), - _ => return, - }; - for post_constraint in post_constraints { - self.add_pair_implication( - db, - env, - storage, - left_constraint, - right_constraint, - post_constraint, - ); - } - }; - - try_one_direction(left_constraint, right_constraint); - try_one_direction(right_constraint, left_constraint); - } - - fn add_concrete_sequents<'db>( - &mut self, - db: &'db dyn Db, - env: &ProgramEnvironment<'db>, - storage: &mut ConstraintSetStorage<'db>, - left_constraint: ConstraintId, - right_constraint: ConstraintId, - ) { - // These might seem redundant with the intersection check below, since `a → b` means that - // `a ∧ b = a`. But we are not normalizing constraint bounds, and these clauses help us - // identify constraints that are identical besides e.g. ordering of union/intersection - // elements. (For instance, when processing `T ≤ τ₁ & τ₂` and `T ≤ τ₂ & τ₁`, these clauses - // would add sequents for `(T ≤ τ₁ & τ₂) → (T ≤ τ₂ & τ₁)` and vice versa.) - if storage.cached_constraint_implies(db, env, left_constraint, right_constraint) { - tracing::trace!( - target: "ty_python_semantic::types::constraints::SequentMap", - left = %left_constraint.display(db, env, storage), - right = %right_constraint.display(db, env, storage), - "left implies right", - ); - self.add_single_implication(left_constraint, right_constraint); - } - if storage.cached_constraint_implies(db, env, right_constraint, left_constraint) { - tracing::trace!( - target: "ty_python_semantic::types::constraints::SequentMap", - left = %left_constraint.display(db, env, storage), - right = %right_constraint.display(db, env, storage), - "right implies left", - ); - self.add_single_implication(right_constraint, left_constraint); - } - - match left_constraint.intersect(db, env, storage, right_constraint) { - IntersectionResult::Simplified(intersection_constraint_data) => { - let intersection_constraint = - storage.intern_constraint(db, env, intersection_constraint_data); - tracing::trace!( - target: "ty_python_semantic::types::constraints::SequentMap", - left = %left_constraint.display(db, env, storage), - right = %right_constraint.display(db, env, storage), - intersection = %intersection_constraint.display(db, env, storage), - "left and right overlap", - ); - self.add_pair_implication( - db, - env, - storage, - left_constraint, - right_constraint, - intersection_constraint, - ); - self.add_single_implication(intersection_constraint, left_constraint); - self.add_single_implication(intersection_constraint, right_constraint); - } - - // The sequent map only needs to include constraints that might appear in a BDD. If the - // intersection does not collapse to a single constraint, then there's no new - // constraint that we need to add to the sequent map. - IntersectionResult::CannotSimplify => {} - - IntersectionResult::Disjoint => { - tracing::trace!( - target: "ty_python_semantic::types::constraints::SequentMap", - left = %left_constraint.display(db, env, storage), - right = %right_constraint.display(db, env, storage), - "left and right are disjoint", - ); - self.add_pair_impossibility(left_constraint, right_constraint); - } - } - } - - #[expect(dead_code)] // Keep this around for debugging purposes - fn display<'db, 'a>( - &'a self, - db: &'db dyn Db, - env: &'a ProgramEnvironment<'db>, - storage: &'a ConstraintSetStorage<'db>, - prefix: &'a dyn Display, - ) -> impl Display + 'a { - std::fmt::from_fn(move |f| { - let mut first = true; - let mut maybe_write_prefix = |f: &mut std::fmt::Formatter<'_>| { - if first { - first = false; - Ok(()) - } else { - write!(f, "\n{prefix}") - } - }; - - for sequent in &self.sequents { - match sequent { - Sequent::SingleTautology { .. } => {} - - Sequent::PairImpossibility { ante1, ante2 } => { - maybe_write_prefix(f)?; - write!( - f, - "{} ∧ {} → false", - ante1.display(db, env, storage), - ante2.display(db, env, storage), - )?; - } - - Sequent::PairImplication { ante1, ante2, post } => { - maybe_write_prefix(f)?; - write!( - f, - "{} ∧ {} → {}", - ante1.display(db, env, storage), - ante2.display(db, env, storage), - post.display(db, env, storage), - )?; - } - - Sequent::SingleImplication { ante, post } => { - maybe_write_prefix(f)?; - write!( - f, - "{} → {}", - ante.display(db, env, storage), - post.display(db, env, storage) - )?; - } - } - } - - if first { - f.write_str("[no sequents]")?; - } - Ok(()) - }) - } -} - -/// A visitor for walking the paths of a BDD. -/// -/// **NOTE**: This trait gives you full control over the walking process: in particular, you have -/// more opportunities to abort the walk early. If you want to perform a simple "fold" over all of -/// the paths, the [`PathFold`] trait is easier to implement, and can also be used as a -/// `PathVisitor`. -/// -/// Each path starts at the root node and ends at a terminal node, and represents one family of -/// typevar assignments described by the BDD. Each path can be either _satisfied_, meaning that -/// this family of assignments is accepted by the constraint set; _unsatisfied_, meaning that this -/// family of assignments is _not_ accepted by the constraint set; or _impossible_, meaning that -/// this family of assignments contains a contradiction, and cannot possibly ever occur. -/// -/// To visit the BDD paths: -/// -/// - We start at the root node. -/// -/// - Each time we encounter an interior node, we call the visitor's `enter_interior` method. We -/// then process walk the interior node's `true`, `uncertain`, and `false` outgoing edges. -/// -/// - To process an edge, we recursively visit the node that the edge points to (getting a `Result` -/// for that subtree), and then call the visitor's `visit_edge` method. This lets you modify the -/// subtree's value based on the assignments that were added to the path by this edge. (This -/// includes at least the constraint checked by the interior node containing this edge, and can -/// also include any additional derived facts that we learn based on whatever other assignments -/// currently hold on the path.) -/// -/// - Once we have processed all of the edges for an interior node, we call the visitor's -/// `leave_interior` method. This lets you combine the `Result`s from each outgoing edge into a -/// single `Result` that represents the subtree rooted at this interior node. -/// -/// Throughout this process, if any of your methods return [`ControlFlow::Break`], we will abort -/// the path walk and immediately return that value. -trait PathVisitor { - type Result; - type Interior; - type Break; - - /// Called before visiting any interior or terminal node. Returning `Break` prevents the - /// traversal from entering the node or deriving facts from its outgoing edges. - fn visit_node(&mut self) -> ControlFlow { - ControlFlow::Continue(()) - } - - /// Called when we reach the end of a satisfied path. `path` will contain all of the - /// assignments on this path. The `Result` value that you return will be propagated back up as - /// we "unwind" this path. - fn visit_satisfied<'db>( - &mut self, - db: &'db dyn Db, - storage: &mut ConstraintSetStorage<'db>, - path: &PathAssignments, - ) -> ControlFlow; - - /// Called when we reach the end of an unsatisfied path. `path` will contain all of the - /// assignments on this path. The `Result` value that you return will be propagated back up as - /// we "unwind" this path. - fn visit_unsatisfied<'db>( - &mut self, - db: &'db dyn Db, - storage: &mut ConstraintSetStorage<'db>, - path: &PathAssignments, - ) -> ControlFlow; - - /// Called when we determine that a path is impossible, either because its assignments - /// contradict each other, or because an edge is structurally absent (such as the uncertain - /// edge when visiting a negated BDD). The `Result` value that you return will be propagated - /// back up as we "unwind" this path. - fn visit_impossible<'db>( - &mut self, - db: &'db dyn Db, - storage: &mut ConstraintSetStorage<'db>, - path: &PathAssignments, - ) -> ControlFlow; - - /// Called on the way down as we enter each interior node. You can create a - /// [`Interior`][Self::Interior] value that will be passed to the - /// [`visit_edge`][Self::visit_edge] and [`leave_interior`][Self::leave_interior] methods - /// when we call them for this node. - fn enter_interior<'db>( - &mut self, - db: &'db dyn Db, - storage: &mut ConstraintSetStorage<'db>, - interior_node: InteriorNode, - ) -> ControlFlow; - - /// Called once for each edge in the BDD. You are given the [`Result`][Self::Result] value - /// of the subtree that the edge points to, as well as the origin and derived assignments that - /// are added by the edge. - fn visit_edge<'db>( - &mut self, - db: &'db dyn Db, - storage: &mut ConstraintSetStorage<'db>, - interior_value: &Self::Interior, - subtree: Self::Result, - path: &PathAssignments, - new_range: Range, - ) -> ControlFlow; - - /// Called on the way back up as we leave each interior node in the BDD. Combines the - /// [`Result`][Self::Result] values for each of the interior node's subtrees. - fn leave_interior<'db>( - &mut self, - db: &'db dyn Db, - storage: &mut ConstraintSetStorage<'db>, - interior_value: &Self::Interior, - if_true: Self::Result, - if_uncertain: Self::Result, - if_false: Self::Result, - ) -> ControlFlow; -} - -/// A visitor for "folding" over the paths in a BDD, producing a single value that summarizes all -/// of them. -/// -/// This is a simpler trait to implement when you don't need as much control over the path walk. -/// Any type that implements this trait can also be used as a [`PathVisitor`]. -trait PathFold { - type Result; - type Break; - - /// Returns the base case value that represents a satisfied path. - fn satisfied<'db>( - &mut self, - db: &'db dyn Db, - storage: &mut ConstraintSetStorage<'db>, - path: &PathAssignments, - ) -> ControlFlow; - - /// Returns the base case value that represents an unsatisfied path. - fn unsatisfied<'db>( - &mut self, - db: &'db dyn Db, - storage: &mut ConstraintSetStorage<'db>, - path: &PathAssignments, - ) -> ControlFlow; - - /// Returns the base case value that represents an impossible path. - fn impossible<'db>( - &mut self, - db: &'db dyn Db, - storage: &mut ConstraintSetStorage<'db>, - path: &PathAssignments, - ) -> ControlFlow; - - /// Combines the values for each subtree of an interior node, returning a value that represents - /// the subtree rooted at that node. - fn combine<'db>( - &mut self, - db: &'db dyn Db, - storage: &mut ConstraintSetStorage<'db>, - if_true: Self::Result, - if_uncertain: Self::Result, - if_false: Self::Result, - ) -> ControlFlow; -} - -impl PathVisitor for T -where - T: PathFold, -{ - type Result = ::Result; - type Interior = (); - type Break = ::Break; - - fn visit_satisfied<'db>( - &mut self, - db: &'db dyn Db, - storage: &mut ConstraintSetStorage<'db>, - path: &PathAssignments, - ) -> ControlFlow { - PathFold::satisfied(self, db, storage, path) - } - - fn visit_unsatisfied<'db>( - &mut self, - db: &'db dyn Db, - storage: &mut ConstraintSetStorage<'db>, - path: &PathAssignments, - ) -> ControlFlow { - PathFold::unsatisfied(self, db, storage, path) - } - - fn visit_impossible<'db>( - &mut self, - db: &'db dyn Db, - storage: &mut ConstraintSetStorage<'db>, - path: &PathAssignments, - ) -> ControlFlow { - PathFold::impossible(self, db, storage, path) - } - - fn enter_interior<'db>( - &mut self, - _db: &'db dyn Db, - _storage: &mut ConstraintSetStorage<'db>, - _interior_node: InteriorNode, - ) -> ControlFlow { - ControlFlow::Continue(()) - } - - fn visit_edge<'db>( - &mut self, - _db: &'db dyn Db, - _storage: &mut ConstraintSetStorage<'db>, - _interior_value: &Self::Interior, - subtree: Self::Result, - _path: &PathAssignments, - _new_range: Range, - ) -> ControlFlow { - ControlFlow::Continue(subtree) - } - - fn leave_interior<'db>( - &mut self, - db: &'db dyn Db, - storage: &mut ConstraintSetStorage<'db>, - _interior_value: &Self::Interior, - if_true: Self::Result, - if_uncertain: Self::Result, - if_false: Self::Result, - ) -> ControlFlow { - PathFold::combine(self, db, storage, if_true, if_uncertain, if_false) - } -} - -/// A path visitor that breaks early if it encounters a satisfied path. When applying this visitor, -/// a `Continue` result indicates that no satisfied path was found, and the BDD was therefore -/// unsatisfiable. A `Break` result indicates the opposite. -struct IsNeverSatisfiedVisitor; - -impl PathFold for IsNeverSatisfiedVisitor { - type Result = (); - type Break = (); - - fn satisfied<'db>( - &mut self, - _db: &'db dyn Db, - _storage: &mut ConstraintSetStorage<'db>, - _path: &PathAssignments, - ) -> ControlFlow { - ControlFlow::Break(()) - } - - fn unsatisfied<'db>( - &mut self, - _db: &'db dyn Db, - _storage: &mut ConstraintSetStorage<'db>, - _path: &PathAssignments, - ) -> ControlFlow { - ControlFlow::Continue(()) - } - - fn impossible<'db>( - &mut self, - _db: &'db dyn Db, - _storage: &mut ConstraintSetStorage<'db>, - _path: &PathAssignments, - ) -> ControlFlow { - ControlFlow::Continue(()) - } - - fn combine<'db>( - &mut self, - _db: &'db dyn Db, - _storage: &mut ConstraintSetStorage<'db>, - _if_true: Self::Result, - _if_uncertain: Self::Result, - _if_false: Self::Result, - ) -> ControlFlow { - ControlFlow::Continue(()) - } -} - -/// The collection of constraints that we know to be true or false at a certain point when -/// traversing a BDD. -/// -/// An important part of this traversal is that not all of those constraints come directly from the -/// BDD, since constraints are not independent. In particular, there can be "implications", which -/// record e.g. when two constraints both being true imply another: -/// `A ≤ list[B] ∧ B ≤ int → A ≤ list[int]`. If we see `A ≤ list[B]` and `B ≤ int` in a BDD path, -/// we can _assume_ that `A ≤ list[int]` also holds, even if it doesn't actually appear in the BDD. -/// -/// Unfortunately, there are certain implications that are technically true, but not helpful; -/// for instance, because they cause us to endlessly expand a constraint by substituting a bound -/// into itself. -/// -/// We use a "fuel" mechanism to prevent these kinds of situations, without having to play -/// whack-a-mole to implement detection patterns for all of the pathological patterns. Each -/// derived constraint costs at least one unit of fuel. Nested typevars increase that cost according -/// to their depth, as does any constructor depth introduced relative to the antecedents. Measuring -/// structural growth instead of absolute depth ensures that propagating an existing complex -/// concrete bound remains cheap, while repeatedly wrapping that bound continues to consume path -/// fuel after no nested typevars remain. -/// -/// We track this fuel in two ways: First, there is a global limit on the total amount of work we -/// are willing to do for a particular BDD path traversal. Second, there is a more focused -/// "per-path" limit, which records how far removed a derived constraint is from a constraint that -/// actually appears in the BDD. If either of those limits are exceeded, we ignore the derived -/// constraint that we are currently considering. -#[derive(Debug)] -pub(crate) struct PathAssignments { - /// All of the rules that we know for inferring derived constraints on the current path. - sequents: Vec, - /// Each assignment's source constraint and the first per-path fuel value with which it was - /// derived. - assignments: FxIndexMap, - /// Additional per-path fuel values that can derive an assignment, keyed by its index in - /// `assignments`. These are stored separately so that branch-local additions can be rolled - /// back by truncating the set. Only the greatest fuel value participates in further - /// derivation. - additional_fuels: Vec<(usize, u16)>, - /// The amount of global fuel that remains across all assignments and paths. - remaining_overall_fuel: u16, - /// Constraints that we have discovered, mapped to whether we have processed them yet. (This - /// ensures a stable order for all of the derived constraints that we create, while still - /// letting us create them lazily.) - discovered: FxIndexMap, - /// Constraint pairs that we have already checked and added to `sequents`. - elaborated_pairs: FxHashSet<(ConstraintId, ConstraintId)>, - - /// Type variables that only involve concrete constraints and so do not participate in sequent - /// discovery. - independent_typevars: FxHashSet, - - /// Derived assignments that have been queued up to be added to the current path. - assignment_queue: VecDeque<(ConstraintAssignment, AssignmentFuel)>, - - /// The next chunk of derived assignments that have been queued up to add to the current path. - /// If we derive the same assignment multiple times, we keep the derivation that lets us make - /// the most additional progress (more remaining fuel for this derivation chain, less overall - /// fuel consumed). - new_assignments: FxIndexMap, -} - -/// The total amount of fuel that we are willing to spend for this path traversal. This was -/// chosen empirically, to balance performance with accurate ecosystem diagnostics. -const OVERALL_FUEL_BUDGET: u16 = 256; - -/// The maximum number of "trips through the sequent map" that we are willing to take for a -/// derived constraint. This records how far removed we are from a constraint that comes -/// directly from the BDD. -const PATH_FUEL_BUDGET: u16 = 8; - -/// The fuel cost of deriving a particular assignment during BDD path walking. -#[derive(Clone, Copy, Debug, Eq, PartialEq)] -struct AssignmentFuel { - /// The amount of fuel consumed when deriving the assignment, or None if this assignment came - /// directly from the BDD - consumed: Option, - /// The amount of fuel remaining on the derivation path after deriving this assignment - remaining: u16, -} - -impl AssignmentFuel { - fn origin() -> AssignmentFuel { - AssignmentFuel { - consumed: None, - remaining: PATH_FUEL_BUDGET, - } - } - - fn derived(consumed: u16, remaining: u16) -> AssignmentFuel { - AssignmentFuel { - consumed: Some(consumed), - remaining, - } - } - - fn is_derived(self) -> bool { - self.consumed.is_some() - } -} - -impl PartialOrd for AssignmentFuel { - fn partial_cmp(&self, other: &Self) -> Option { - Some(self.cmp(other)) - } -} - -impl Ord for AssignmentFuel { - fn cmp(&self, other: &Self) -> Ordering { - let self_key = (self.remaining, std::cmp::Reverse(self.consumed)); - let other_key = (other.remaining, std::cmp::Reverse(other.consumed)); - self_key.cmp(&other_key) - } -} - -impl PathAssignments { - fn new( - constraints: impl IntoIterator, - independent_typevars: FxHashSet, - ) -> Self { - let discovered = constraints - .into_iter() - .map(|constraint| (constraint, false)) - .collect(); - Self { - sequents: Vec::default(), - assignments: FxIndexMap::default(), - additional_fuels: Vec::default(), - discovered, - elaborated_pairs: FxHashSet::default(), - independent_typevars, - remaining_overall_fuel: OVERALL_FUEL_BUDGET, - assignment_queue: VecDeque::default(), - new_assignments: FxIndexMap::default(), - } - } - - fn visit<'db, V>( - &mut self, - db: &'db dyn Db, - env: &ProgramEnvironment<'db>, - storage: &mut ConstraintSetStorage<'db>, - node: NodeId, - visitor: &mut V, - ) -> ControlFlow - where - V: PathVisitor, - { - self.visit_inner(db, env, storage, node, visitor, false) - } - - /// Visits the paths of the negation of `node`, without constructing that negation eagerly. - fn visit_negated<'db, V>( - &mut self, - db: &'db dyn Db, - env: &ProgramEnvironment<'db>, - storage: &mut ConstraintSetStorage<'db>, - node: NodeId, - visitor: &mut V, - ) -> ControlFlow - where - V: PathVisitor, - { - self.visit_inner(db, env, storage, node, visitor, true) - } - - fn visit_inner<'db, V>( - &mut self, - db: &'db dyn Db, - env: &ProgramEnvironment<'db>, - storage: &mut ConstraintSetStorage<'db>, - node: NodeId, - visitor: &mut V, - negated: bool, - ) -> ControlFlow - where - V: PathVisitor, - { - visitor.visit_node()?; - match node.node() { - Node::AlwaysTrue if negated => visitor.visit_unsatisfied(db, storage, self), - Node::AlwaysTrue => visitor.visit_satisfied(db, storage, self), - - Node::AlwaysFalse if negated => visitor.visit_satisfied(db, storage, self), - Node::AlwaysFalse => visitor.visit_unsatisfied(db, storage, self), - - Node::Interior(interior) => { - let interior_value = visitor.enter_interior(db, storage, interior)?; - let interior = storage.interior_node_data(node); - - let true_subtree = if negated { - interior.if_true.or(storage, interior.if_uncertain) - } else { - interior.if_true - }; - let if_true = self.walk_edge( - db, - env, - storage, - interior.constraint.when_true(), - |storage, path, new_range, found_conflict| { - let subtree = if found_conflict { - visitor.visit_impossible(db, storage, path) - } else { - path.visit_inner(db, env, storage, true_subtree, visitor, negated) - }; - match subtree { - ControlFlow::Continue(subtree) => visitor.visit_edge( - db, - storage, - &interior_value, - subtree, - path, - new_range, - ), - ControlFlow::Break(b) => ControlFlow::Break(b), - } - }, - )?; - - let if_uncertain = if negated { - let subtree = visitor.visit_impossible(db, storage, self)?; - visitor.visit_edge(db, storage, &interior_value, subtree, self, 0..0)? - } else { - self.walk_edge( - db, - env, - storage, - interior.constraint.when_unconstrained(), - |storage, path, new_range, found_conflict| { - let subtree = if found_conflict { - visitor.visit_impossible(db, storage, path) - } else { - path.visit_inner( - db, - env, - storage, - interior.if_uncertain, - visitor, - false, - ) - }; - match subtree { - ControlFlow::Continue(subtree) => visitor.visit_edge( - db, - storage, - &interior_value, - subtree, - path, - new_range, - ), - ControlFlow::Break(b) => ControlFlow::Break(b), - } - }, - )? - }; - - let false_subtree = if negated { - interior.if_false.or(storage, interior.if_uncertain) - } else { - interior.if_false - }; - let if_false = self.walk_edge( - db, - env, - storage, - interior.constraint.when_false(), - |storage, path, new_range, found_conflict| { - let subtree = if found_conflict { - visitor.visit_impossible(db, storage, path) - } else { - path.visit_inner(db, env, storage, false_subtree, visitor, negated) - }; - match subtree { - ControlFlow::Continue(subtree) => visitor.visit_edge( - db, - storage, - &interior_value, - subtree, - path, - new_range, - ), - ControlFlow::Break(b) => ControlFlow::Break(b), - } - }, - )?; - - visitor.leave_interior( - db, - storage, - &interior_value, - if_true, - if_uncertain, - if_false, - ) - } - } - } - - /// Walks one of the outgoing edges of an internal BDD node. `assignment` describes the - /// constraint that the BDD node checks, and whether we are following the `if_true` or - /// `if_false` edge. - /// - /// This new assignment might cause this path to become impossible — for instance, if we were - /// already assuming (from an earlier edge in the path) a constraint that is disjoint with this - /// one. We might also be able to infer _other_ assignments that do not appear in the BDD - /// directly, but which are implied from a combination of constraints that we _have_ seen. - /// - /// To handle all of this, you provide a callback. If the path has become impossible, we will - /// return `None` _without invoking the callback_. If the path does not contain any - /// contradictions, we will invoke the callback and return its result (wrapped in `Some`). - /// - /// Your callback will also be provided a slice of all of the constraints that we were able to - /// infer from `assignment` combined with the information we already knew. (For borrow-check - /// reasons, we provide this as a [`Range`]; use that range to index into `self.assignments` to - /// get the list of all of the assignments that we learned from this edge.) - /// - /// You will presumably end up making a recursive call of some kind to keep progressing through - /// the BDD. You should make this call from inside of your callback, so that as you get further - /// down into the BDD structure, we remember all of the information that we have learned from - /// the path we're on. - fn walk_edge<'db, R>( - &mut self, - db: &'db dyn Db, - env: &ProgramEnvironment<'db>, - storage: &mut ConstraintSetStorage<'db>, - assignment: ConstraintAssignment, - f: impl FnOnce(&mut ConstraintSetStorage<'db>, &mut Self, Range, bool) -> R, - ) -> R { - // Record a snapshot of the assignments that we already knew held — both so that we can - // pass along the range of which assignments are new, and so that we can reset back to this - // point before returning. - let start = self.assignments.len(); - let additional_fuels_start = self.additional_fuels.len(); - let previous_remaining_overall_fuel = self.remaining_overall_fuel; - - // Add the new assignment and anything we can derive from it. - tracing::trace!( - target: "ty_python_semantic::types::constraints::PathAssignment", - before = %format_args!( - "[{}]", - self.assignments[..start].iter().map(|(assignment, _)| { - assignment.display(db, env, storage) - }).format(", "), - ), - edge = %assignment.display(db, env, storage), - "walk edge", - ); - debug_assert!(self.assignment_queue.is_empty()); - self.assignment_queue - .push_back((assignment, AssignmentFuel::origin())); - let source_constraint = assignment.constraint(); - let found_conflict = self - .drain_assignment_queue(db, env, storage, source_constraint) - .is_err(); - if !found_conflict { - tracing::trace!( - target: "ty_python_semantic::types::constraints::PathAssignment", - new = %format_args!( - "[{}]", - self.assignments[start..].iter().map(|(assignment, _)| { - assignment.display(db, env, storage) - }).format(", "), - ), - "new assignments", - ); - } - // Otherwise invoke the callback to keep traversing the BDD. The callback will likely - // traverse additional edges, which might add more to our `assignments` set. But even - // if that happens, `start..end` will mark the assignments that were added by the - // `add_assignment` call above — that is, the new assignment for this edge along with - // the derived information we inferred from it. - let end = self.assignments.len(); - let result = f(storage, self, start..end, found_conflict); - - // Reset back to where we were before following this edge, so that the caller can reuse a - // single instance for the entire BDD traversal. - self.assignment_queue.clear(); - self.assignments.truncate(start); - self.additional_fuels.truncate(additional_fuels_start); - self.remaining_overall_fuel = previous_remaining_overall_fuel; - result - } - - fn positive_constraints(&self) -> impl Iterator + '_ { - self.assignments.iter().filter_map( - |(assignment, (source_constraint, _))| match assignment { - ConstraintAssignment::Positive(constraint) => { - Some((*constraint, *source_constraint)) - } - ConstraintAssignment::Negative(_) | ConstraintAssignment::Unconstrained(_) => None, - }, - ) - } - - fn assignment_holds(&self, assignment: ConstraintAssignment) -> bool { - self.assignments.contains_key(&assignment) - } - - fn contains_constraint(&self, constraint: ConstraintId) -> bool { - self.assignment_holds(constraint.when_true()) - || self.assignment_holds(constraint.when_false()) - || self.assignment_holds(constraint.when_unconstrained()) - } - - /// Returns the greatest remaining fuel for any derivation of `assignment` on this path. - fn max_remaining_fuel_for(&self, assignment: ConstraintAssignment) -> Option { - let (index, _, (_, first_fuel)) = self.assignments.get_full(&assignment)?; - let max_fuel = self - .additional_fuels - .iter() - .filter(|(fuel_index, _)| *fuel_index == index) - .map(|(_, fuel)| *fuel) - .fold(*first_fuel, u16::max); - Some(max_fuel) - } - - /// Update our sequent map to ensure that it holds all of the sequents that involve the given - /// constraint. We do not calculate the new sequents directly. Instead, we call - /// [`SequentMap::for_constraint`] and [`for_constraint_pair`][SequentMap::for_constraint_pair] - /// to calculate _and cache_ the constraints, so that if we walk another constraint set - /// containing this constraint, we reuse the work to calculate its sequents. - fn discover_constraint<'db>( + fn enter_interior<'db>( &mut self, - db: &'db dyn Db, - env: &ProgramEnvironment<'db>, - storage: &mut ConstraintSetStorage<'db>, - constraint: ConstraintId, - ) { - // If we've already processed this constraint, we can skip it. - let (constraint_index, existing) = self.discovered.insert_full(constraint, true); - let already_processed = existing.is_some_and(|existing| existing); - if already_processed { - return; - } - - let single_map = SequentMap::for_constraint(db, env, storage, constraint); - self.sequents.extend_from_slice(&single_map.sequents); - - for (existing_index, (existing, _)) in self.discovered.iter().enumerate() { - if *existing == constraint { - continue; - } - - let existing_support = storage.constraint_support(*existing); - let constraint_support = storage.constraint_support(constraint); - - // Independent typevars must be checked for disjoint or invalid constraints, but are - // otherwise already constrained and do not participate in sequent discovery. - if !existing_support.overlaps_with(constraint_support) - && existing_support - .iter() - .chain(constraint_support.iter()) - .any(|typevar| self.independent_typevars.contains(&typevar)) - && existing_support.is_complete() - && constraint_support.is_complete() - { - continue; - } - - if SequentMap::pair_cannot_produce_sequents(db, env, storage, *existing, constraint) { - continue; - } - - let (a, b) = if existing_index < constraint_index { - (*existing, constraint) - } else { - (constraint, *existing) - }; - if !self.elaborated_pairs.insert((a, b)) { - // We've already elaborated this pair of constraints. - continue; - } - - let pair_map = SequentMap::for_constraint_pair(db, env, storage, a, b); - self.sequents.extend_from_slice(&pair_map.sequents); - } + _db: &'db dyn Db, + _storage: &mut ConstraintSetStorage<'db>, + _interior_node: InteriorNode, + ) -> ControlFlow { + ControlFlow::Continue(()) } - fn drain_assignment_queue<'db>( + fn visit_edge<'db>( &mut self, - db: &'db dyn Db, - env: &ProgramEnvironment<'db>, - storage: &mut ConstraintSetStorage<'db>, - source_constraint: ConstraintId, - ) -> Result<(), PathAssignmentConflict> { - while let Some((assignment, fuel)) = self.assignment_queue.pop_front() { - self.add_assignment(db, env, storage, assignment, source_constraint, fuel)?; - } - Ok(()) + _db: &'db dyn Db, + _storage: &mut ConstraintSetStorage<'db>, + _interior_value: &Self::Interior, + subtree: Self::Result, + _path: &PathAssignments, + _new_range: Range, + ) -> ControlFlow { + ControlFlow::Continue(subtree) } - /// Adds a new assignment, along with any derived information that we can infer from the new - /// assignment combined with the assignments we've already seen. If any of this causes the path - /// to become invalid, due to a contradiction, returns a [`PathAssignmentConflict`] error. - fn add_assignment<'db>( + fn leave_interior<'db>( &mut self, db: &'db dyn Db, - env: &ProgramEnvironment<'db>, storage: &mut ConstraintSetStorage<'db>, - assignment: ConstraintAssignment, - source_constraint: ConstraintId, - fuel: AssignmentFuel, - ) -> Result<(), PathAssignmentConflict> { - if matches!(assignment, ConstraintAssignment::Unconstrained(_)) { - // An `Unconstrained` assignment means "this constraint can go either way". If there is - // already any assignment for this constraint (positive, negative, or unconstrained), - // the existing assignment is at least as informative, and we skip. - if self.contains_constraint(assignment.constraint()) { - return Ok(()); - } - - // Since we don't know whether the assignment's constraint holds or not, we cannot - // derive any additional information from the sequent map. We still want to record the - // assignment, but as an optimization we can return early without actually querying the - // sequent map. - self.assignments - .insert(assignment, (source_constraint, fuel.remaining)); - return Ok(()); - } - - // First add this assignment. If it causes a conflict, return that as an error. - if self.assignments.contains_key(&assignment.negated()) { - tracing::trace!( - target: "ty_python_semantic::types::constraints::PathAssignment", - assignment = %assignment.display(db, env, storage), - facts = %format_args!( - "[{}]", - self.assignments.iter().map(|(assignment, _)| { - assignment.display(db, env, storage) - }).format(", "), - ), - "found contradiction", - ); - return Err(PathAssignmentConflict); - } - - match self.assignments.entry(assignment) { - Entry::Vacant(entry) => { - if let Some(fuel_cost) = fuel.consumed { - self.remaining_overall_fuel = - match self.remaining_overall_fuel.checked_sub(fuel_cost) { - Some(updated_fuel) => updated_fuel, - None => return Ok(()), - }; - } - entry.insert((source_constraint, fuel.remaining)); - } - - Entry::Occupied(mut entry) => { - let index = entry.index(); - let (existing_source_constraint, existing_fuel) = entry.get_mut(); - - // If a constraint appears both as an "origin" constraint (it actually appears in - // the BDD structure) and as a "derived" constraint (we infer it from other - // constraints), we should prefer the origin source constraint, regardless of which - // order we encounter the various constraints in the BDD. - if !fuel.is_derived() { - *existing_source_constraint = source_constraint; - } - - // We've already seen this assignment, and in theory have already queried the - // sequent map for its consequents, which should let us return early. - // - // However, a new derivation chain can replenish the fuel for this assignment, - // giving it more chances to participate in multi-step sequent chains. That means - // there might be some consequents that were skipped previously due to a lack of - // fuel, that can be added now because of the replinished fuel budget. - - // There is another derivation of this assignment that already provides at least as - // much fuel as this constraint. That means replenishing the fuel won't have any - // effect. - if *existing_fuel >= fuel.remaining - || self - .additional_fuels - .iter() - .any(|(fuel_index, existing_fuel)| { - *fuel_index == index && *existing_fuel >= fuel.remaining - }) - { - return Ok(()); - } - - // Record the replenished fuel separately so that `walk_edge` can restore the - // parent branch by truncating `additional_fuels`. - self.additional_fuels.push((index, fuel.remaining)); - } - } - - // Then use our sequents to add additional facts that we know to be true. - // - // TODO: This is very naive at the moment, partly for expediency, and partly because we - // don't anticipate the sequent maps to be very large. We might consider avoiding the - // brute-force search. - - self.new_assignments.clear(); - self.discover_constraint(db, env, storage, assignment.constraint()); - - for i in 0..self.sequents.len() { - let sequent = self.sequents[i]; - self.check_sequent(db, env, storage, sequent)?; - } - - // If we were able to derive any new assignments from this one, add them to the processing - // queue. - self.assignment_queue.extend(self.new_assignments.drain(..)); - - Ok(()) + _interior_value: &Self::Interior, + if_true: Self::Result, + if_uncertain: Self::Result, + if_false: Self::Result, + ) -> ControlFlow { + PathFold::combine(self, db, storage, if_true, if_uncertain, if_false) } +} - fn enqueue_assignment(&mut self, assignment: ConstraintAssignment, new_fuel: AssignmentFuel) { - self.new_assignments - .entry(assignment) - .and_modify(|existing_fuel| { - *existing_fuel = std::cmp::max(*existing_fuel, new_fuel); - }) - .or_insert(new_fuel); - } +/// A path visitor that breaks early if it encounters a satisfied path. When applying this visitor, +/// a `Continue` result indicates that no satisfied path was found, and the BDD was therefore +/// unsatisfiable. A `Break` result indicates the opposite. +struct IsNeverSatisfiedVisitor; - fn check_sequent<'db>( - &mut self, - db: &'db dyn Db, - env: &ProgramEnvironment<'db>, - storage: &mut ConstraintSetStorage<'db>, - sequent: Sequent, - ) -> Result<(), PathAssignmentConflict> { - match sequent { - Sequent::SingleTautology { ante } => { - self.check_single_tautology(db, env, storage, ante) - } - Sequent::PairImpossibility { ante1, ante2 } => { - self.check_pair_impossibility(db, env, storage, ante1, ante2) - } - Sequent::PairImplication { ante1, ante2, post } => { - self.check_pair_implication(db, env, storage, ante1, ante2, post); - Ok(()) - } - Sequent::SingleImplication { ante, post } => { - self.check_single_implication(db, env, storage, ante, post); - Ok(()) - } - } - } +impl PathFold for IsNeverSatisfiedVisitor { + type Result = (); + type Break = (); - fn check_single_tautology<'db>( + fn satisfied<'db>( &mut self, - db: &'db dyn Db, - env: &ProgramEnvironment<'db>, - storage: &mut ConstraintSetStorage<'db>, - ante: ConstraintId, - ) -> Result<(), PathAssignmentConflict> { - if self.assignment_holds(ante.when_false()) { - // The sequent map says (ante1) is always true, and the current path asserts that - // it's false. - tracing::trace!( - target: "ty_python_semantic::types::constraints::PathAssignment", - ante = %ante.display(db, env, storage), - facts = %format_args!( - "[{}]", - self.assignments.iter().map(|(assignment, _)| { - assignment.display(db, env, storage) - }).format(", "), - ), - "found contradiction", - ); - return Err(PathAssignmentConflict); - } - - Ok(()) + _db: &'db dyn Db, + _storage: &mut ConstraintSetStorage<'db>, + _path: &PathAssignments, + ) -> ControlFlow { + ControlFlow::Break(()) } - fn check_pair_impossibility<'db>( + fn unsatisfied<'db>( &mut self, - db: &'db dyn Db, - env: &ProgramEnvironment<'db>, - storage: &mut ConstraintSetStorage<'db>, - ante1: ConstraintId, - ante2: ConstraintId, - ) -> Result<(), PathAssignmentConflict> { - if self.assignment_holds(ante1.when_true()) && self.assignment_holds(ante2.when_true()) { - // The sequent map says (ante1 ∧ ante2) is an impossible combination, and the - // current path asserts that both are true. - tracing::trace!( - target: "ty_python_semantic::types::constraints::PathAssignment", - ante1 = %ante1.display(db, env, storage), - ante2 = %ante2.display(db, env, storage), - facts = %format_args!( - "[{}]", - self.assignments.iter().map(|(assignment, _)| { - assignment.display(db, env, storage) - }).format(", "), - ), - "found contradiction", - ); - return Err(PathAssignmentConflict); - } - - Ok(()) + _db: &'db dyn Db, + _storage: &mut ConstraintSetStorage<'db>, + _path: &PathAssignments, + ) -> ControlFlow { + ControlFlow::Continue(()) } - fn check_pair_implication<'db>( + fn impossible<'db>( &mut self, - db: &'db dyn Db, - env: &ProgramEnvironment<'db>, - storage: &mut ConstraintSetStorage<'db>, - ante1: ConstraintId, - ante2: ConstraintId, - post: ConstraintId, - ) { - let Some(ante1_fuel) = self.max_remaining_fuel_for(ante1.when_true()) else { - return; - }; - let Some(ante2_fuel) = self.max_remaining_fuel_for(ante2.when_true()) else { - return; - }; - let available_fuel = ante1_fuel.min(ante2_fuel); - let (ante1_constructor_depth, _) = storage.cached_constraint_bound_depth(db, env, ante1); - let (ante2_constructor_depth, _) = storage.cached_constraint_bound_depth(db, env, ante2); - let antecedent_constructor_depth = ante1_constructor_depth.max(ante2_constructor_depth); - let fuel_cost = storage.sequent_fuel_cost(db, env, post, antecedent_constructor_depth); - if let Some(post_fuel) = available_fuel.checked_sub(fuel_cost) { - self.enqueue_assignment( - post.when_true(), - AssignmentFuel::derived(fuel_cost, post_fuel), - ); - } + _db: &'db dyn Db, + _storage: &mut ConstraintSetStorage<'db>, + _path: &PathAssignments, + ) -> ControlFlow { + ControlFlow::Continue(()) } - fn check_single_implication<'db>( + fn combine<'db>( &mut self, - db: &'db dyn Db, - env: &ProgramEnvironment<'db>, - storage: &mut ConstraintSetStorage<'db>, - ante: ConstraintId, - post: ConstraintId, - ) { - let Some(available_fuel) = self.max_remaining_fuel_for(ante.when_true()) else { - return; - }; - let ante_data = storage.constraint_data(ante); - let (antecedent_constructor_depth, _) = - storage.cached_constraint_bound_depth(db, env, ante); - let post_data = storage.constraint_data(post); - let fuel_cost = if post_data.is_bound_projection_of(db, ante_data) { - 1 - } else { - storage.sequent_fuel_cost(db, env, post, antecedent_constructor_depth) - }; - if let Some(post_fuel) = available_fuel.checked_sub(fuel_cost) { - self.enqueue_assignment( - post.when_true(), - AssignmentFuel::derived(fuel_cost, post_fuel), - ); - } + _db: &'db dyn Db, + _storage: &mut ConstraintSetStorage<'db>, + _if_true: Self::Result, + _if_uncertain: Self::Result, + _if_false: Self::Result, + ) -> ControlFlow { + ControlFlow::Continue(()) } } -#[derive(Debug)] -struct PathAssignmentConflict; - /// A single clause in the DNF representation of a BDD #[derive(Clone, Debug, Default, Eq, PartialEq)] struct SatisfiedClause { @@ -7954,55 +5828,6 @@ mod tests { assert!(positive_results > 0); } - #[test] - fn overlapping_lower_bounds_do_not_skip_nonempty_sequent_map() { - let db = setup_db(); - let db = &db; - let env = db.program_environment(); - let builder = ConstraintSetBuilder::new(); - let t = create_typevar(db, "T"); - let bool = known_instance(db, KnownClass::Bool); - let u = create_typevar(db, "U") - .map_bound_or_constraints(db, |_| Some(TypeVarBoundOrConstraints::UpperBound(bool))); - let type_of_u = SubclassOfType::from(db, &env, u); - let bool_class = KnownClass::Bool.to_class_literal(db, &env); - let mut storage = builder.storage.borrow_mut(); - let left = ConstraintId::new_with_bounds( - db, - &env, - &mut storage, - t, - Some(ConstraintBound::Evidence(type_of_u)), - None, - ); - let right = ConstraintId::new_with_bounds( - db, - &env, - &mut storage, - t, - Some(ConstraintBound::Evidence(bool_class)), - None, - ); - - for (left, right) in [(left, right), (right, left)] { - let sequents = SequentMap::for_constraint_pair(db, &env, &mut storage, left, right); - - assert!( - sequents - .sequents - .iter() - .any(|sequent| matches!(sequent, Sequent::SingleImplication { .. })) - ); - assert!(!SequentMap::pair_cannot_produce_sequents( - db, - &env, - &mut storage, - left, - right - )); - } - } - #[test] fn bounded_path_fast_paths_respect_limits() { let db = setup_db(); @@ -8497,57 +6322,6 @@ class E: ... ); } - #[test] - fn constraint_implications_are_cached() { - let db = setup_db(); - let db = &db; - let env = db.program_environment(); - let t = create_typevar(db, "T"); - let builder = ConstraintSetBuilder::new(); - let mut storage = builder.storage.borrow_mut(); - let t_int = ConstraintId::new( - db, - &env, - &mut storage, - t, - Type::Never, - KnownClass::Int.to_instance(db, &env), - ); - let t_bool = ConstraintId::new( - db, - &env, - &mut storage, - t, - Type::Never, - KnownClass::Bool.to_instance(db, &env), - ); - - assert!(storage.cached_constraint_implies(db, &env, t_bool, t_int)); - assert!(storage.cached_constraint_implies(db, &env, t_bool, t_int)); - drop(storage); - - { - let storage = builder.storage.borrow(); - assert_eq!( - storage.constraint_implication_cache.get(&(t_bool, t_int)), - Some(&true) - ); - assert_eq!(storage.constraint_implication_cache.len(), 1); - } - - let mut storage = builder.storage.borrow_mut(); - assert!(!storage.cached_constraint_implies(db, &env, t_int, t_bool)); - assert!(!storage.cached_constraint_implies(db, &env, t_int, t_bool)); - drop(storage); - - let storage = builder.storage.borrow(); - assert_eq!( - storage.constraint_implication_cache.get(&(t_int, t_bool)), - Some(&false) - ); - assert_eq!(storage.constraint_implication_cache.len(), 2); - } - #[test] fn trivial_satisfaction_only_recognizes_terminals() { let db = setup_db(); @@ -9391,342 +7165,6 @@ class E: ... ); } - #[test] - fn eager_and_lazy_negation_are_equivalent() { - let db = setup_db(); - let db = &db; - let env = db.program_environment(); - let t = create_typevar(db, "T"); - let u = create_typevar(db, "U"); - let builder = ConstraintSetBuilder::new(); - - let t_int = create_constraint(db, &builder, t, KnownClass::Int); - let t_bool = create_constraint(db, &builder, t, KnownClass::Bool); - let u_str = create_constraint(db, &builder, u, KnownClass::Str); - let u_int = create_constraint(db, &builder, u, KnownClass::Int); - - let lhs = t_int.or(db, &builder, || u_str); - let rhs = t_bool.or(db, &builder, || u_int); - let intersection = lhs.and(db, &builder, || rhs); - let tautology = lhs.or(db, &builder, || lhs.negate(db, &builder)); - - let t_bool_upper = ConstraintSet::constrain_typevar_upper_bound( - db, - &env, - &builder, - t, - KnownClass::Bool.to_instance(db, &env), - ); - let t_int_upper = ConstraintSet::constrain_typevar_upper_bound( - db, - &env, - &builder, - t, - KnownClass::Int.to_instance(db, &env), - ); - let implication = t_bool_upper - .negate(db, &builder) - .or(db, &builder, || t_int_upper); - - for set in [lhs, rhs, intersection, tautology, implication] { - assert_eq!( - set.is_always_satisfied(db, &env), - set.negate(db, &builder).is_never_satisfied(db, &env) - ); - } - } - - #[derive(Clone, Copy, Debug, Eq, PartialEq)] - enum PathFoldBreak { - Satisfied, - Unsatisfied, - Impossible, - Combine, - } - - /// A path fold that reconstructs a constraint set from its satisfied paths and can abort at - /// a specified callback. - struct ReconstructPathFold { - break_at: Option, - } - - impl ReconstructPathFold { - fn result( - &self, - at: PathFoldBreak, - result: (NodeId, Option), - ) -> ControlFlow)> { - if self.break_at == Some(at) { - ControlFlow::Break(at) - } else { - ControlFlow::Continue(result) - } - } - } - - impl PathFold for ReconstructPathFold { - type Result = (NodeId, Option); - type Break = PathFoldBreak; - - fn satisfied<'db>( - &mut self, - _db: &'db dyn Db, - storage: &mut ConstraintSetStorage<'db>, - path: &PathAssignments, - ) -> ControlFlow { - let result = - path.assignments - .iter() - .fold((ALWAYS_TRUE, None), |result, (assignment, _)| { - let (node, source_order) = result; - let (assignment, assignment_source_order) = - Node::new_satisfied_constraint(storage, *assignment); - ( - node.and(storage, assignment), - storage.ordered_source_order(source_order, assignment_source_order), - ) - }); - self.result(PathFoldBreak::Satisfied, result) - } - - fn unsatisfied<'db>( - &mut self, - _db: &'db dyn Db, - _storage: &mut ConstraintSetStorage<'db>, - _path: &PathAssignments, - ) -> ControlFlow { - self.result(PathFoldBreak::Unsatisfied, (ALWAYS_FALSE, None)) - } - - fn impossible<'db>( - &mut self, - _db: &'db dyn Db, - _storage: &mut ConstraintSetStorage<'db>, - _path: &PathAssignments, - ) -> ControlFlow { - self.result(PathFoldBreak::Impossible, (ALWAYS_FALSE, None)) - } - - fn combine<'db>( - &mut self, - _db: &'db dyn Db, - storage: &mut ConstraintSetStorage<'db>, - if_true: Self::Result, - if_uncertain: Self::Result, - if_false: Self::Result, - ) -> ControlFlow { - let (if_true, if_true_source_order) = if_true; - let (if_uncertain, if_uncertain_source_order) = if_uncertain; - let (if_false, if_false_source_order) = if_false; - let node = if_true.or(storage, if_uncertain).or(storage, if_false); - let source_order = - storage.ordered_source_order(if_true_source_order, if_uncertain_source_order); - let source_order = storage.ordered_source_order(source_order, if_false_source_order); - self.result(PathFoldBreak::Combine, (node, source_order)) - } - } - - fn path_assignments_for<'db>( - db: &'db dyn Db, - env: &ProgramEnvironment<'db>, - builder: &ConstraintSetBuilder<'db>, - node: NodeId, - source_order: Option, - ) -> PathAssignments { - let mut storage = builder.storage.borrow_mut(); - match node.node() { - Node::AlwaysTrue | Node::AlwaysFalse => PathAssignments::new([], FxHashSet::default()), - Node::Interior(interior) => { - interior.path_assignments(db, env, &mut storage, source_order) - } - } - } - - #[test] - fn path_assignments_follow_constraint_source_order() { - let db = setup_db(); - let db = &db; - let env = db.program_environment(); - let t = create_typevar(db, "T"); - let u = create_typevar(db, "U"); - let builder = ConstraintSetBuilder::new(); - let t_int = create_constraint(db, &builder, t, KnownClass::Int); - let u_str = create_constraint(db, &builder, u, KnownClass::Str); - - // Construct the set in the opposite order from constraint creation. This ensures the - // initializer follows the sidecar rather than either TDD traversal or constraint IDs. - let set = u_str.and(db, &builder, || t_int); - let path = path_assignments_for(db, &env, &builder, set.node, set.source_order); - let storage = builder.storage.borrow(); - let expected = - [u_str.node, t_int.node].map(|node| storage.interior_node_data(node).constraint); - let actual: Vec<_> = path.discovered.keys().copied().collect(); - - assert_eq!(actual, expected); - } - - #[test] - fn path_fold_reconstructs_constraint_sets() { - let db = setup_db(); - let db = &db; - let env = db.program_environment(); - let t = create_typevar(db, "T"); - let u = create_typevar(db, "U"); - let v = create_typevar(db, "V"); - let builder = ConstraintSetBuilder::new(); - - let t_int = create_constraint(db, &builder, t, KnownClass::Int); - let t_str = create_constraint(db, &builder, t, KnownClass::Str); - let u_int = create_constraint(db, &builder, u, KnownClass::Int); - let v_bytes = create_constraint(db, &builder, v, KnownClass::Bytes); - let union = t_int.or(db, &builder, || u_int); - let intersection = union.and(db, &builder, || t_str.or(db, &builder, || v_bytes)); - let contradiction = t_int.and(db, &builder, || t_str); - let tautology = union.or(db, &builder, || union.negate(db, &builder)); - - let t_u = - ConstraintSet::constrain_typevar_upper_bound(db, &env, &builder, t, Type::TypeVar(u)); - let u_int_upper = ConstraintSet::constrain_typevar_upper_bound( - db, - &env, - &builder, - u, - KnownClass::Int.to_instance(db, &env), - ); - let int_t = ConstraintSet::constrain_typevar_lower_bound( - db, - &env, - &builder, - t, - KnownClass::Int.to_instance(db, &env), - ); - let transitive = t_u - .and(db, &builder, || u_int_upper) - .and(db, &builder, || int_t) - .or(db, &builder, || v_bytes); - - for set in [ - ConstraintSet::always(&builder), - ConstraintSet::never(&builder), - union, - intersection, - contradiction, - tautology, - transitive, - ] { - let mut path = path_assignments_for(db, &env, &builder, set.node, set.source_order); - let mut fold = ReconstructPathFold { break_at: None }; - let mut storage = builder.storage.borrow_mut(); - let ControlFlow::Continue((reconstructed, reconstructed_source_order)) = - path.visit(db, &env, &mut storage, set.node, &mut fold) - else { - panic!("reconstruction unexpectedly aborted"); - }; - drop(storage); - let reconstructed = - ConstraintSet::from_node(&builder, reconstructed, reconstructed_source_order); - assert!( - set.iff(db, &builder, reconstructed) - .is_always_satisfied(db, &env) - ); - } - } - - #[test] - fn path_fold_break_restores_path_assignments() { - let db = setup_db(); - let db = &db; - let env = db.program_environment(); - let t = create_typevar(db, "T"); - let u = create_typevar(db, "U"); - let builder = ConstraintSetBuilder::new(); - let t_int = create_constraint(db, &builder, t, KnownClass::Int); - let t_str = create_constraint(db, &builder, t, KnownClass::Str); - let u_int = create_constraint(db, &builder, u, KnownClass::Int); - let set = t_int.and(db, &builder, || t_str).or(db, &builder, || u_int); - - for break_at in [ - PathFoldBreak::Satisfied, - PathFoldBreak::Unsatisfied, - PathFoldBreak::Impossible, - PathFoldBreak::Combine, - ] { - let mut path = path_assignments_for(db, &env, &builder, set.node, set.source_order); - let mut aborting_fold = ReconstructPathFold { - break_at: Some(break_at), - }; - let mut storage = builder.storage.borrow_mut(); - assert_eq!( - path.visit(db, &env, &mut storage, set.node, &mut aborting_fold), - ControlFlow::Break(break_at) - ); - - let mut completing_fold = ReconstructPathFold { break_at: None }; - let ControlFlow::Continue((reconstructed, reconstructed_source_order)) = - path.visit(db, &env, &mut storage, set.node, &mut completing_fold) - else { - panic!("reconstruction unexpectedly aborted after {break_at:?}"); - }; - drop(storage); - let reconstructed = - ConstraintSet::from_node(&builder, reconstructed, reconstructed_source_order); - assert!( - set.iff(db, &builder, reconstructed) - .is_always_satisfied(db, &env) - ); - } - } - - #[test] - fn solution_walker_break_restores_path_assignments() { - let db = setup_db(); - let db = &db; - let env = db.program_environment(); - let t = create_typevar(db, "T"); - let builder = ConstraintSetBuilder::new(); - let t_int = create_constraint(db, &builder, t, KnownClass::Int); - let t_str = create_constraint(db, &builder, t, KnownClass::Str); - let set = t_int.or(db, &builder, || t_str); - let source_orders = builder - .storage - .borrow() - .calculate_source_orders(set.source_order); - let expected = PathBounds::compute( - db, - &env, - &mut builder.storage.borrow_mut(), - set.node, - TypeVarSet::from_typevars(db, [t]), - set.source_order, - ); - - // Both limits interrupt an edge with path-local assignments: the visit limit stops - // below the root, and the path limit stops after collecting the first alternative. - for (remaining_paths, remaining_visits, error) in [ - (usize::MAX, 1, ProjectionError::TraversalBudgetExceeded), - (1, usize::MAX, ProjectionError::PathBudgetExceeded), - ] { - let mut path = path_assignments_for(db, &env, &builder, set.node, set.source_order); - let mut storage = builder.storage.borrow_mut(); - let mut limits = BoundedSolutionLimits { - remaining_paths, - remaining_visits, - }; - let mut walker = SolutionWalker::new(source_orders.clone()); - assert_eq!( - walker.visit_node(db, &env, &mut storage, &mut path, set.node, &mut limits), - ControlFlow::Break(error) - ); - drop(walker); - - let mut limits = UnboundedSolutionLimits; - let mut walker = SolutionWalker::new(source_orders.clone()); - let ControlFlow::Continue(()) = - walker.visit_node(db, &env, &mut storage, &mut path, set.node, &mut limits); - assert_eq!(walker.finish(db, &env, &mut storage), expected); - } - } - /// Double negation of a TDD with uncertain branches is semantically equivalent to the /// original (though the structure may differ since negation produces flat TDDs). #[test] diff --git a/crates/ty_python_semantic/src/types/constraints/paths.rs b/crates/ty_python_semantic/src/types/constraints/paths.rs new file mode 100644 index 0000000000000..ee9c7b3be3b2e --- /dev/null +++ b/crates/ty_python_semantic/src/types/constraints/paths.rs @@ -0,0 +1,1143 @@ +//! [`PathAssignments`] and friends + +use std::cmp::Ordering; +use std::collections::VecDeque; +use std::fmt::Debug; +use std::ops::{ControlFlow, Range}; + +use indexmap::map::Entry; +use itertools::Itertools; +use rustc_hash::FxHashSet; + +use crate::types::constraints::sequents::{Sequent, SequentMap}; +use crate::types::constraints::{ + ConstraintAssignment, ConstraintId, ConstraintSetStorage, Node, NodeId, PathVisitor, TypeVarId, +}; +use crate::{Db, FxIndexMap, ProgramEnvironment}; + +/// The collection of constraints that we know to be true or false at a certain point when +/// traversing a BDD. +/// +/// An important part of this traversal is that not all of those constraints come directly from the +/// BDD, since constraints are not independent. In particular, there can be "implications", which +/// record e.g. when two constraints both being true imply another: +/// `A ≤ list[B] ∧ B ≤ int → A ≤ list[int]`. If we see `A ≤ list[B]` and `B ≤ int` in a BDD path, +/// we can _assume_ that `A ≤ list[int]` also holds, even if it doesn't actually appear in the BDD. +/// +/// Unfortunately, there are certain implications that are technically true, but not helpful; +/// for instance, because they cause us to endlessly expand a constraint by substituting a bound +/// into itself. +/// +/// We use a "fuel" mechanism to prevent these kinds of situations, without having to play +/// whack-a-mole to implement detection patterns for all of the pathological patterns. Each +/// derived constraint costs at least one unit of fuel. Nested typevars increase that cost according +/// to their depth, as does any constructor depth introduced relative to the antecedents. Measuring +/// structural growth instead of absolute depth ensures that propagating an existing complex +/// concrete bound remains cheap, while repeatedly wrapping that bound continues to consume path +/// fuel after no nested typevars remain. +/// +/// We track this fuel in two ways: First, there is a global limit on the total amount of work we +/// are willing to do for a particular BDD path traversal. Second, there is a more focused +/// "per-path" limit, which records how far removed a derived constraint is from a constraint that +/// actually appears in the BDD. If either of those limits are exceeded, we ignore the derived +/// constraint that we are currently considering. +#[derive(Debug)] +pub(crate) struct PathAssignments { + /// All of the rules that we know for inferring derived constraints on the current path. + sequents: Vec, + /// Each assignment's source constraint and the first per-path fuel value with which it was + /// derived. + pub(super) assignments: FxIndexMap, + /// Additional per-path fuel values that can derive an assignment, keyed by its index in + /// `assignments`. These are stored separately so that branch-local additions can be rolled + /// back by truncating the set. Only the greatest fuel value participates in further + /// derivation. + additional_fuels: Vec<(usize, u16)>, + /// The amount of global fuel that remains across all assignments and paths. + remaining_overall_fuel: u16, + /// Constraints that we have discovered, mapped to whether we have processed them yet. (This + /// ensures a stable order for all of the derived constraints that we create, while still + /// letting us create them lazily.) + discovered: FxIndexMap, + /// Constraint pairs that we have already checked and added to `sequents`. + elaborated_pairs: FxHashSet<(ConstraintId, ConstraintId)>, + + /// Type variables that only involve concrete constraints and so do not participate in sequent + /// discovery. + independent_typevars: FxHashSet, + + /// Derived assignments that have been queued up to be added to the current path. + assignment_queue: VecDeque<(ConstraintAssignment, AssignmentFuel)>, + + /// The next chunk of derived assignments that have been queued up to add to the current path. + /// If we derive the same assignment multiple times, we keep the derivation that lets us make + /// the most additional progress (more remaining fuel for this derivation chain, less overall + /// fuel consumed). + new_assignments: FxIndexMap, +} + +/// The total amount of fuel that we are willing to spend for this path traversal. This was +/// chosen empirically, to balance performance with accurate ecosystem diagnostics. +const OVERALL_FUEL_BUDGET: u16 = 256; + +/// The maximum number of "trips through the sequent map" that we are willing to take for a +/// derived constraint. This records how far removed we are from a constraint that comes +/// directly from the BDD. +const PATH_FUEL_BUDGET: u16 = 8; + +/// The fuel cost of deriving a particular assignment during BDD path walking. +#[derive(Clone, Copy, Debug, Eq, PartialEq)] +struct AssignmentFuel { + /// The amount of fuel consumed when deriving the assignment, or None if this assignment came + /// directly from the BDD + consumed: Option, + /// The amount of fuel remaining on the derivation path after deriving this assignment + remaining: u16, +} + +impl AssignmentFuel { + fn origin() -> AssignmentFuel { + AssignmentFuel { + consumed: None, + remaining: PATH_FUEL_BUDGET, + } + } + + fn derived(consumed: u16, remaining: u16) -> AssignmentFuel { + AssignmentFuel { + consumed: Some(consumed), + remaining, + } + } + + fn is_derived(self) -> bool { + self.consumed.is_some() + } +} + +impl PartialOrd for AssignmentFuel { + fn partial_cmp(&self, other: &Self) -> Option { + Some(self.cmp(other)) + } +} + +impl Ord for AssignmentFuel { + fn cmp(&self, other: &Self) -> Ordering { + let self_key = (self.remaining, std::cmp::Reverse(self.consumed)); + let other_key = (other.remaining, std::cmp::Reverse(other.consumed)); + self_key.cmp(&other_key) + } +} + +impl PathAssignments { + pub(super) fn new( + constraints: impl IntoIterator, + independent_typevars: FxHashSet, + ) -> Self { + let discovered = constraints + .into_iter() + .map(|constraint| (constraint, false)) + .collect(); + Self { + sequents: Vec::default(), + assignments: FxIndexMap::default(), + additional_fuels: Vec::default(), + discovered, + elaborated_pairs: FxHashSet::default(), + independent_typevars, + remaining_overall_fuel: OVERALL_FUEL_BUDGET, + assignment_queue: VecDeque::default(), + new_assignments: FxIndexMap::default(), + } + } + + pub(super) fn visit<'db, V>( + &mut self, + db: &'db dyn Db, + env: &ProgramEnvironment<'db>, + storage: &mut ConstraintSetStorage<'db>, + node: NodeId, + visitor: &mut V, + ) -> ControlFlow + where + V: PathVisitor, + { + self.visit_inner(db, env, storage, node, visitor, false) + } + + /// Visits the paths of the negation of `node`, without constructing that negation eagerly. + pub(super) fn visit_negated<'db, V>( + &mut self, + db: &'db dyn Db, + env: &ProgramEnvironment<'db>, + storage: &mut ConstraintSetStorage<'db>, + node: NodeId, + visitor: &mut V, + ) -> ControlFlow + where + V: PathVisitor, + { + self.visit_inner(db, env, storage, node, visitor, true) + } + + fn visit_inner<'db, V>( + &mut self, + db: &'db dyn Db, + env: &ProgramEnvironment<'db>, + storage: &mut ConstraintSetStorage<'db>, + node: NodeId, + visitor: &mut V, + negated: bool, + ) -> ControlFlow + where + V: PathVisitor, + { + visitor.visit_node()?; + match node.node() { + Node::AlwaysTrue if negated => visitor.visit_unsatisfied(db, storage, self), + Node::AlwaysTrue => visitor.visit_satisfied(db, storage, self), + + Node::AlwaysFalse if negated => visitor.visit_satisfied(db, storage, self), + Node::AlwaysFalse => visitor.visit_unsatisfied(db, storage, self), + + Node::Interior(interior) => { + let interior_value = visitor.enter_interior(db, storage, interior)?; + let interior = storage.interior_node_data(node); + + let true_subtree = if negated { + interior.if_true.or(storage, interior.if_uncertain) + } else { + interior.if_true + }; + let if_true = self.walk_edge( + db, + env, + storage, + interior.constraint.when_true(), + |storage, path, new_range, found_conflict| { + let subtree = if found_conflict { + visitor.visit_impossible(db, storage, path) + } else { + path.visit_inner(db, env, storage, true_subtree, visitor, negated) + }; + match subtree { + ControlFlow::Continue(subtree) => visitor.visit_edge( + db, + storage, + &interior_value, + subtree, + path, + new_range, + ), + ControlFlow::Break(b) => ControlFlow::Break(b), + } + }, + )?; + + let if_uncertain = if negated { + let subtree = visitor.visit_impossible(db, storage, self)?; + visitor.visit_edge(db, storage, &interior_value, subtree, self, 0..0)? + } else { + self.walk_edge( + db, + env, + storage, + interior.constraint.when_unconstrained(), + |storage, path, new_range, found_conflict| { + let subtree = if found_conflict { + visitor.visit_impossible(db, storage, path) + } else { + path.visit_inner( + db, + env, + storage, + interior.if_uncertain, + visitor, + false, + ) + }; + match subtree { + ControlFlow::Continue(subtree) => visitor.visit_edge( + db, + storage, + &interior_value, + subtree, + path, + new_range, + ), + ControlFlow::Break(b) => ControlFlow::Break(b), + } + }, + )? + }; + + let false_subtree = if negated { + interior.if_false.or(storage, interior.if_uncertain) + } else { + interior.if_false + }; + let if_false = self.walk_edge( + db, + env, + storage, + interior.constraint.when_false(), + |storage, path, new_range, found_conflict| { + let subtree = if found_conflict { + visitor.visit_impossible(db, storage, path) + } else { + path.visit_inner(db, env, storage, false_subtree, visitor, negated) + }; + match subtree { + ControlFlow::Continue(subtree) => visitor.visit_edge( + db, + storage, + &interior_value, + subtree, + path, + new_range, + ), + ControlFlow::Break(b) => ControlFlow::Break(b), + } + }, + )?; + + visitor.leave_interior( + db, + storage, + &interior_value, + if_true, + if_uncertain, + if_false, + ) + } + } + } + + /// Walks one of the outgoing edges of an internal BDD node. `assignment` describes the + /// constraint that the BDD node checks, and whether we are following the `if_true` or + /// `if_false` edge. + /// + /// This new assignment might cause this path to become impossible — for instance, if we were + /// already assuming (from an earlier edge in the path) a constraint that is disjoint with this + /// one. We might also be able to infer _other_ assignments that do not appear in the BDD + /// directly, but which are implied from a combination of constraints that we _have_ seen. + /// + /// To handle all of this, you provide a callback. If the path has become impossible, we will + /// return `None` _without invoking the callback_. If the path does not contain any + /// contradictions, we will invoke the callback and return its result (wrapped in `Some`). + /// + /// Your callback will also be provided a slice of all of the constraints that we were able to + /// infer from `assignment` combined with the information we already knew. (For borrow-check + /// reasons, we provide this as a [`Range`]; use that range to index into `self.assignments` to + /// get the list of all of the assignments that we learned from this edge.) + /// + /// You will presumably end up making a recursive call of some kind to keep progressing through + /// the BDD. You should make this call from inside of your callback, so that as you get further + /// down into the BDD structure, we remember all of the information that we have learned from + /// the path we're on. + pub(super) fn walk_edge<'db, R>( + &mut self, + db: &'db dyn Db, + env: &ProgramEnvironment<'db>, + storage: &mut ConstraintSetStorage<'db>, + assignment: ConstraintAssignment, + f: impl FnOnce(&mut ConstraintSetStorage<'db>, &mut Self, Range, bool) -> R, + ) -> R { + // Record a snapshot of the assignments that we already knew held — both so that we can + // pass along the range of which assignments are new, and so that we can reset back to this + // point before returning. + let start = self.assignments.len(); + let additional_fuels_start = self.additional_fuels.len(); + let previous_remaining_overall_fuel = self.remaining_overall_fuel; + + // Add the new assignment and anything we can derive from it. + tracing::trace!( + target: "ty_python_semantic::types::constraints::PathAssignment", + before = %format_args!( + "[{}]", + self.assignments[..start].iter().map(|(assignment, _)| { + assignment.display(db, env, storage) + }).format(", "), + ), + edge = %assignment.display(db, env, storage), + "walk edge", + ); + debug_assert!(self.assignment_queue.is_empty()); + self.assignment_queue + .push_back((assignment, AssignmentFuel::origin())); + let source_constraint = assignment.constraint(); + let found_conflict = self + .drain_assignment_queue(db, env, storage, source_constraint) + .is_err(); + if !found_conflict { + tracing::trace!( + target: "ty_python_semantic::types::constraints::PathAssignment", + new = %format_args!( + "[{}]", + self.assignments[start..].iter().map(|(assignment, _)| { + assignment.display(db, env, storage) + }).format(", "), + ), + "new assignments", + ); + } + // Otherwise invoke the callback to keep traversing the BDD. The callback will likely + // traverse additional edges, which might add more to our `assignments` set. But even + // if that happens, `start..end` will mark the assignments that were added by the + // `add_assignment` call above — that is, the new assignment for this edge along with + // the derived information we inferred from it. + let end = self.assignments.len(); + let result = f(storage, self, start..end, found_conflict); + + // Reset back to where we were before following this edge, so that the caller can reuse a + // single instance for the entire BDD traversal. + self.assignment_queue.clear(); + self.assignments.truncate(start); + self.additional_fuels.truncate(additional_fuels_start); + self.remaining_overall_fuel = previous_remaining_overall_fuel; + result + } + + pub(super) fn positive_constraints( + &self, + ) -> impl Iterator + '_ { + self.assignments.iter().filter_map( + |(assignment, (source_constraint, _))| match assignment { + ConstraintAssignment::Positive(constraint) => { + Some((*constraint, *source_constraint)) + } + ConstraintAssignment::Negative(_) | ConstraintAssignment::Unconstrained(_) => None, + }, + ) + } + + fn assignment_holds(&self, assignment: ConstraintAssignment) -> bool { + self.assignments.contains_key(&assignment) + } + + fn contains_constraint(&self, constraint: ConstraintId) -> bool { + self.assignment_holds(constraint.when_true()) + || self.assignment_holds(constraint.when_false()) + || self.assignment_holds(constraint.when_unconstrained()) + } + + /// Returns the greatest remaining fuel for any derivation of `assignment` on this path. + fn max_remaining_fuel_for(&self, assignment: ConstraintAssignment) -> Option { + let (index, _, (_, first_fuel)) = self.assignments.get_full(&assignment)?; + let max_fuel = self + .additional_fuels + .iter() + .filter(|(fuel_index, _)| *fuel_index == index) + .map(|(_, fuel)| *fuel) + .fold(*first_fuel, u16::max); + Some(max_fuel) + } + + /// Update our sequent map to ensure that it holds all of the sequents that involve the given + /// constraint. We do not calculate the new sequents directly. Instead, we call + /// [`SequentMap::for_constraint`] and [`for_constraint_pair`][SequentMap::for_constraint_pair] + /// to calculate _and cache_ the constraints, so that if we walk another constraint set + /// containing this constraint, we reuse the work to calculate its sequents. + fn discover_constraint<'db>( + &mut self, + db: &'db dyn Db, + env: &ProgramEnvironment<'db>, + storage: &mut ConstraintSetStorage<'db>, + constraint: ConstraintId, + ) { + // If we've already processed this constraint, we can skip it. + let (constraint_index, existing) = self.discovered.insert_full(constraint, true); + let already_processed = existing.is_some_and(|existing| existing); + if already_processed { + return; + } + + let single_map = SequentMap::for_constraint(db, env, storage, constraint); + self.sequents.extend_from_slice(&single_map.sequents); + + for (existing_index, (existing, _)) in self.discovered.iter().enumerate() { + if *existing == constraint { + continue; + } + + let existing_support = storage.constraint_support(*existing); + let constraint_support = storage.constraint_support(constraint); + + // Independent typevars must be checked for disjoint or invalid constraints, but are + // otherwise already constrained and do not participate in sequent discovery. + if !existing_support.overlaps_with(constraint_support) + && existing_support + .iter() + .chain(constraint_support.iter()) + .any(|typevar| self.independent_typevars.contains(&typevar)) + && existing_support.is_complete() + && constraint_support.is_complete() + { + continue; + } + + if SequentMap::pair_cannot_produce_sequents(db, env, storage, *existing, constraint) { + continue; + } + + let (a, b) = if existing_index < constraint_index { + (*existing, constraint) + } else { + (constraint, *existing) + }; + if !self.elaborated_pairs.insert((a, b)) { + // We've already elaborated this pair of constraints. + continue; + } + + let pair_map = SequentMap::for_constraint_pair(db, env, storage, a, b); + self.sequents.extend_from_slice(&pair_map.sequents); + } + } + + fn drain_assignment_queue<'db>( + &mut self, + db: &'db dyn Db, + env: &ProgramEnvironment<'db>, + storage: &mut ConstraintSetStorage<'db>, + source_constraint: ConstraintId, + ) -> Result<(), PathAssignmentConflict> { + while let Some((assignment, fuel)) = self.assignment_queue.pop_front() { + self.add_assignment(db, env, storage, assignment, source_constraint, fuel)?; + } + Ok(()) + } + + /// Adds a new assignment, along with any derived information that we can infer from the new + /// assignment combined with the assignments we've already seen. If any of this causes the path + /// to become invalid, due to a contradiction, returns a [`PathAssignmentConflict`] error. + fn add_assignment<'db>( + &mut self, + db: &'db dyn Db, + env: &ProgramEnvironment<'db>, + storage: &mut ConstraintSetStorage<'db>, + assignment: ConstraintAssignment, + source_constraint: ConstraintId, + fuel: AssignmentFuel, + ) -> Result<(), PathAssignmentConflict> { + if matches!(assignment, ConstraintAssignment::Unconstrained(_)) { + // An `Unconstrained` assignment means "this constraint can go either way". If there is + // already any assignment for this constraint (positive, negative, or unconstrained), + // the existing assignment is at least as informative, and we skip. + if self.contains_constraint(assignment.constraint()) { + return Ok(()); + } + + // Since we don't know whether the assignment's constraint holds or not, we cannot + // derive any additional information from the sequent map. We still want to record the + // assignment, but as an optimization we can return early without actually querying the + // sequent map. + self.assignments + .insert(assignment, (source_constraint, fuel.remaining)); + return Ok(()); + } + + // First add this assignment. If it causes a conflict, return that as an error. + if self.assignments.contains_key(&assignment.negated()) { + tracing::trace!( + target: "ty_python_semantic::types::constraints::PathAssignment", + assignment = %assignment.display(db, env, storage), + facts = %format_args!( + "[{}]", + self.assignments.iter().map(|(assignment, _)| { + assignment.display(db, env, storage) + }).format(", "), + ), + "found contradiction", + ); + return Err(PathAssignmentConflict); + } + + match self.assignments.entry(assignment) { + Entry::Vacant(entry) => { + if let Some(fuel_cost) = fuel.consumed { + self.remaining_overall_fuel = + match self.remaining_overall_fuel.checked_sub(fuel_cost) { + Some(updated_fuel) => updated_fuel, + None => return Ok(()), + }; + } + entry.insert((source_constraint, fuel.remaining)); + } + + Entry::Occupied(mut entry) => { + let index = entry.index(); + let (existing_source_constraint, existing_fuel) = entry.get_mut(); + + // If a constraint appears both as an "origin" constraint (it actually appears in + // the BDD structure) and as a "derived" constraint (we infer it from other + // constraints), we should prefer the origin source constraint, regardless of which + // order we encounter the various constraints in the BDD. + if !fuel.is_derived() { + *existing_source_constraint = source_constraint; + } + + // We've already seen this assignment, and in theory have already queried the + // sequent map for its consequents, which should let us return early. + // + // However, a new derivation chain can replenish the fuel for this assignment, + // giving it more chances to participate in multi-step sequent chains. That means + // there might be some consequents that were skipped previously due to a lack of + // fuel, that can be added now because of the replinished fuel budget. + + // There is another derivation of this assignment that already provides at least as + // much fuel as this constraint. That means replenishing the fuel won't have any + // effect. + if *existing_fuel >= fuel.remaining + || self + .additional_fuels + .iter() + .any(|(fuel_index, existing_fuel)| { + *fuel_index == index && *existing_fuel >= fuel.remaining + }) + { + return Ok(()); + } + + // Record the replenished fuel separately so that `walk_edge` can restore the + // parent branch by truncating `additional_fuels`. + self.additional_fuels.push((index, fuel.remaining)); + } + } + + // Then use our sequents to add additional facts that we know to be true. + // + // TODO: This is very naive at the moment, partly for expediency, and partly because we + // don't anticipate the sequent maps to be very large. We might consider avoiding the + // brute-force search. + + self.new_assignments.clear(); + self.discover_constraint(db, env, storage, assignment.constraint()); + + for i in 0..self.sequents.len() { + let sequent = self.sequents[i]; + self.check_sequent(db, env, storage, sequent)?; + } + + // If we were able to derive any new assignments from this one, add them to the processing + // queue. + self.assignment_queue.extend(self.new_assignments.drain(..)); + + Ok(()) + } + + fn enqueue_assignment(&mut self, assignment: ConstraintAssignment, new_fuel: AssignmentFuel) { + self.new_assignments + .entry(assignment) + .and_modify(|existing_fuel| { + *existing_fuel = std::cmp::max(*existing_fuel, new_fuel); + }) + .or_insert(new_fuel); + } + + fn check_sequent<'db>( + &mut self, + db: &'db dyn Db, + env: &ProgramEnvironment<'db>, + storage: &mut ConstraintSetStorage<'db>, + sequent: Sequent, + ) -> Result<(), PathAssignmentConflict> { + match sequent { + Sequent::SingleTautology { ante } => { + self.check_single_tautology(db, env, storage, ante) + } + Sequent::PairImpossibility { ante1, ante2 } => { + self.check_pair_impossibility(db, env, storage, ante1, ante2) + } + Sequent::PairImplication { ante1, ante2, post } => { + self.check_pair_implication(db, env, storage, ante1, ante2, post); + Ok(()) + } + Sequent::SingleImplication { ante, post } => { + self.check_single_implication(db, env, storage, ante, post); + Ok(()) + } + } + } + + fn check_single_tautology<'db>( + &mut self, + db: &'db dyn Db, + env: &ProgramEnvironment<'db>, + storage: &mut ConstraintSetStorage<'db>, + ante: ConstraintId, + ) -> Result<(), PathAssignmentConflict> { + if self.assignment_holds(ante.when_false()) { + // The sequent map says (ante1) is always true, and the current path asserts that + // it's false. + tracing::trace!( + target: "ty_python_semantic::types::constraints::PathAssignment", + ante = %ante.display(db, env, storage), + facts = %format_args!( + "[{}]", + self.assignments.iter().map(|(assignment, _)| { + assignment.display(db, env, storage) + }).format(", "), + ), + "found contradiction", + ); + return Err(PathAssignmentConflict); + } + + Ok(()) + } + + fn check_pair_impossibility<'db>( + &mut self, + db: &'db dyn Db, + env: &ProgramEnvironment<'db>, + storage: &mut ConstraintSetStorage<'db>, + ante1: ConstraintId, + ante2: ConstraintId, + ) -> Result<(), PathAssignmentConflict> { + if self.assignment_holds(ante1.when_true()) && self.assignment_holds(ante2.when_true()) { + // The sequent map says (ante1 ∧ ante2) is an impossible combination, and the + // current path asserts that both are true. + tracing::trace!( + target: "ty_python_semantic::types::constraints::PathAssignment", + ante1 = %ante1.display(db, env, storage), + ante2 = %ante2.display(db, env, storage), + facts = %format_args!( + "[{}]", + self.assignments.iter().map(|(assignment, _)| { + assignment.display(db, env, storage) + }).format(", "), + ), + "found contradiction", + ); + return Err(PathAssignmentConflict); + } + + Ok(()) + } + + fn check_pair_implication<'db>( + &mut self, + db: &'db dyn Db, + env: &ProgramEnvironment<'db>, + storage: &mut ConstraintSetStorage<'db>, + ante1: ConstraintId, + ante2: ConstraintId, + post: ConstraintId, + ) { + let Some(ante1_fuel) = self.max_remaining_fuel_for(ante1.when_true()) else { + return; + }; + let Some(ante2_fuel) = self.max_remaining_fuel_for(ante2.when_true()) else { + return; + }; + let available_fuel = ante1_fuel.min(ante2_fuel); + let (ante1_constructor_depth, _) = storage.cached_constraint_bound_depth(db, env, ante1); + let (ante2_constructor_depth, _) = storage.cached_constraint_bound_depth(db, env, ante2); + let antecedent_constructor_depth = ante1_constructor_depth.max(ante2_constructor_depth); + let fuel_cost = storage.sequent_fuel_cost(db, env, post, antecedent_constructor_depth); + if let Some(post_fuel) = available_fuel.checked_sub(fuel_cost) { + self.enqueue_assignment( + post.when_true(), + AssignmentFuel::derived(fuel_cost, post_fuel), + ); + } + } + + fn check_single_implication<'db>( + &mut self, + db: &'db dyn Db, + env: &ProgramEnvironment<'db>, + storage: &mut ConstraintSetStorage<'db>, + ante: ConstraintId, + post: ConstraintId, + ) { + let Some(available_fuel) = self.max_remaining_fuel_for(ante.when_true()) else { + return; + }; + let ante_data = storage.constraint_data(ante); + let (antecedent_constructor_depth, _) = + storage.cached_constraint_bound_depth(db, env, ante); + let post_data = storage.constraint_data(post); + let fuel_cost = if post_data.is_bound_projection_of(db, ante_data) { + 1 + } else { + storage.sequent_fuel_cost(db, env, post, antecedent_constructor_depth) + }; + if let Some(post_fuel) = available_fuel.checked_sub(fuel_cost) { + self.enqueue_assignment( + post.when_true(), + AssignmentFuel::derived(fuel_cost, post_fuel), + ); + } + } +} + +#[derive(Debug)] +struct PathAssignmentConflict; + +#[cfg(test)] +mod tests { + use super::super::solutions::SolutionWalker; + use super::super::*; + + use crate::db::tests::{TestDb, setup_db}; + use crate::types::{BoundTypeVarInstance, KnownClass, TypeVarVariance}; + use ruff_python_ast::name::Name; + + fn create_typevar<'db>(db: &'db TestDb, name: &'static str) -> BoundTypeVarInstance<'db> { + BoundTypeVarInstance::synthetic( + db, + &db.program_environment(), + Name::new_static(name), + TypeVarVariance::Invariant, + ) + } + + fn create_constraint<'db, 'c>( + db: &'db TestDb, + builder: &'c ConstraintSetBuilder<'db>, + bound_typevar: BoundTypeVarInstance<'db>, + bound: KnownClass, + ) -> ConstraintSet<'db, 'c> { + let env = db.program_environment(); + let ty = bound.to_instance(db, &env); + ConstraintSet::constrain_typevar(db, &env, builder, bound_typevar, ty, ty) + } + + #[test] + fn eager_and_lazy_negation_are_equivalent() { + let db = setup_db(); + let db = &db; + let env = db.program_environment(); + let t = create_typevar(db, "T"); + let u = create_typevar(db, "U"); + let builder = ConstraintSetBuilder::new(); + + let t_int = create_constraint(db, &builder, t, KnownClass::Int); + let t_bool = create_constraint(db, &builder, t, KnownClass::Bool); + let u_str = create_constraint(db, &builder, u, KnownClass::Str); + let u_int = create_constraint(db, &builder, u, KnownClass::Int); + + let lhs = t_int.or(db, &builder, || u_str); + let rhs = t_bool.or(db, &builder, || u_int); + let intersection = lhs.and(db, &builder, || rhs); + let tautology = lhs.or(db, &builder, || lhs.negate(db, &builder)); + + let t_bool_upper = ConstraintSet::constrain_typevar_upper_bound( + db, + &env, + &builder, + t, + KnownClass::Bool.to_instance(db, &env), + ); + let t_int_upper = ConstraintSet::constrain_typevar_upper_bound( + db, + &env, + &builder, + t, + KnownClass::Int.to_instance(db, &env), + ); + let implication = t_bool_upper + .negate(db, &builder) + .or(db, &builder, || t_int_upper); + + for set in [lhs, rhs, intersection, tautology, implication] { + assert_eq!( + set.is_always_satisfied(db, &env), + set.negate(db, &builder).is_never_satisfied(db, &env) + ); + } + } + + #[derive(Clone, Copy, Debug, Eq, PartialEq)] + enum PathFoldBreak { + Satisfied, + Unsatisfied, + Impossible, + Combine, + } + + /// A path fold that reconstructs a constraint set from its satisfied paths and can abort at + /// a specified callback. + struct ReconstructPathFold { + break_at: Option, + } + + impl ReconstructPathFold { + fn result( + &self, + at: PathFoldBreak, + result: (NodeId, Option), + ) -> ControlFlow)> { + if self.break_at == Some(at) { + ControlFlow::Break(at) + } else { + ControlFlow::Continue(result) + } + } + } + + impl PathFold for ReconstructPathFold { + type Result = (NodeId, Option); + type Break = PathFoldBreak; + + fn satisfied<'db>( + &mut self, + _db: &'db dyn Db, + storage: &mut ConstraintSetStorage<'db>, + path: &PathAssignments, + ) -> ControlFlow { + let result = + path.assignments + .iter() + .fold((ALWAYS_TRUE, None), |result, (assignment, _)| { + let (node, source_order) = result; + let (assignment, assignment_source_order) = + Node::new_satisfied_constraint(storage, *assignment); + ( + node.and(storage, assignment), + storage.ordered_source_order(source_order, assignment_source_order), + ) + }); + self.result(PathFoldBreak::Satisfied, result) + } + + fn unsatisfied<'db>( + &mut self, + _db: &'db dyn Db, + _storage: &mut ConstraintSetStorage<'db>, + _path: &PathAssignments, + ) -> ControlFlow { + self.result(PathFoldBreak::Unsatisfied, (ALWAYS_FALSE, None)) + } + + fn impossible<'db>( + &mut self, + _db: &'db dyn Db, + _storage: &mut ConstraintSetStorage<'db>, + _path: &PathAssignments, + ) -> ControlFlow { + self.result(PathFoldBreak::Impossible, (ALWAYS_FALSE, None)) + } + + fn combine<'db>( + &mut self, + _db: &'db dyn Db, + storage: &mut ConstraintSetStorage<'db>, + if_true: Self::Result, + if_uncertain: Self::Result, + if_false: Self::Result, + ) -> ControlFlow { + let (if_true, if_true_source_order) = if_true; + let (if_uncertain, if_uncertain_source_order) = if_uncertain; + let (if_false, if_false_source_order) = if_false; + let node = if_true.or(storage, if_uncertain).or(storage, if_false); + let source_order = + storage.ordered_source_order(if_true_source_order, if_uncertain_source_order); + let source_order = storage.ordered_source_order(source_order, if_false_source_order); + self.result(PathFoldBreak::Combine, (node, source_order)) + } + } + + fn path_assignments_for<'db>( + db: &'db dyn Db, + env: &ProgramEnvironment<'db>, + builder: &ConstraintSetBuilder<'db>, + node: NodeId, + source_order: Option, + ) -> PathAssignments { + let mut storage = builder.storage.borrow_mut(); + match node.node() { + Node::AlwaysTrue | Node::AlwaysFalse => PathAssignments::new([], FxHashSet::default()), + Node::Interior(interior) => { + interior.path_assignments(db, env, &mut storage, source_order) + } + } + } + + #[test] + fn path_assignments_follow_constraint_source_order() { + let db = setup_db(); + let db = &db; + let env = db.program_environment(); + let t = create_typevar(db, "T"); + let u = create_typevar(db, "U"); + let builder = ConstraintSetBuilder::new(); + let t_int = create_constraint(db, &builder, t, KnownClass::Int); + let u_str = create_constraint(db, &builder, u, KnownClass::Str); + + // Construct the set in the opposite order from constraint creation. This ensures the + // initializer follows the sidecar rather than either TDD traversal or constraint IDs. + let set = u_str.and(db, &builder, || t_int); + let path = path_assignments_for(db, &env, &builder, set.node, set.source_order); + let storage = builder.storage.borrow(); + let expected = + [u_str.node, t_int.node].map(|node| storage.interior_node_data(node).constraint); + let actual: Vec<_> = path.discovered.keys().copied().collect(); + + assert_eq!(actual, expected); + } + + #[test] + fn path_fold_reconstructs_constraint_sets() { + let db = setup_db(); + let db = &db; + let env = db.program_environment(); + let t = create_typevar(db, "T"); + let u = create_typevar(db, "U"); + let v = create_typevar(db, "V"); + let builder = ConstraintSetBuilder::new(); + + let t_int = create_constraint(db, &builder, t, KnownClass::Int); + let t_str = create_constraint(db, &builder, t, KnownClass::Str); + let u_int = create_constraint(db, &builder, u, KnownClass::Int); + let v_bytes = create_constraint(db, &builder, v, KnownClass::Bytes); + let union = t_int.or(db, &builder, || u_int); + let intersection = union.and(db, &builder, || t_str.or(db, &builder, || v_bytes)); + let contradiction = t_int.and(db, &builder, || t_str); + let tautology = union.or(db, &builder, || union.negate(db, &builder)); + + let t_u = + ConstraintSet::constrain_typevar_upper_bound(db, &env, &builder, t, Type::TypeVar(u)); + let u_int_upper = ConstraintSet::constrain_typevar_upper_bound( + db, + &env, + &builder, + u, + KnownClass::Int.to_instance(db, &env), + ); + let int_t = ConstraintSet::constrain_typevar_lower_bound( + db, + &env, + &builder, + t, + KnownClass::Int.to_instance(db, &env), + ); + let transitive = t_u + .and(db, &builder, || u_int_upper) + .and(db, &builder, || int_t) + .or(db, &builder, || v_bytes); + + for set in [ + ConstraintSet::always(&builder), + ConstraintSet::never(&builder), + union, + intersection, + contradiction, + tautology, + transitive, + ] { + let mut path = path_assignments_for(db, &env, &builder, set.node, set.source_order); + let mut fold = ReconstructPathFold { break_at: None }; + let mut storage = builder.storage.borrow_mut(); + let ControlFlow::Continue((reconstructed, reconstructed_source_order)) = + path.visit(db, &env, &mut storage, set.node, &mut fold) + else { + panic!("reconstruction unexpectedly aborted"); + }; + drop(storage); + let reconstructed = + ConstraintSet::from_node(&builder, reconstructed, reconstructed_source_order); + assert!( + set.iff(db, &builder, reconstructed) + .is_always_satisfied(db, &env) + ); + } + } + + #[test] + fn path_fold_break_restores_path_assignments() { + let db = setup_db(); + let db = &db; + let env = db.program_environment(); + let t = create_typevar(db, "T"); + let u = create_typevar(db, "U"); + let builder = ConstraintSetBuilder::new(); + let t_int = create_constraint(db, &builder, t, KnownClass::Int); + let t_str = create_constraint(db, &builder, t, KnownClass::Str); + let u_int = create_constraint(db, &builder, u, KnownClass::Int); + let set = t_int.and(db, &builder, || t_str).or(db, &builder, || u_int); + + for break_at in [ + PathFoldBreak::Satisfied, + PathFoldBreak::Unsatisfied, + PathFoldBreak::Impossible, + PathFoldBreak::Combine, + ] { + let mut path = path_assignments_for(db, &env, &builder, set.node, set.source_order); + let mut aborting_fold = ReconstructPathFold { + break_at: Some(break_at), + }; + let mut storage = builder.storage.borrow_mut(); + assert_eq!( + path.visit(db, &env, &mut storage, set.node, &mut aborting_fold), + ControlFlow::Break(break_at) + ); + + let mut completing_fold = ReconstructPathFold { break_at: None }; + let ControlFlow::Continue((reconstructed, reconstructed_source_order)) = + path.visit(db, &env, &mut storage, set.node, &mut completing_fold) + else { + panic!("reconstruction unexpectedly aborted after {break_at:?}"); + }; + drop(storage); + let reconstructed = + ConstraintSet::from_node(&builder, reconstructed, reconstructed_source_order); + assert!( + set.iff(db, &builder, reconstructed) + .is_always_satisfied(db, &env) + ); + } + } + + #[test] + fn solution_walker_break_restores_path_assignments() { + let db = setup_db(); + let db = &db; + let env = db.program_environment(); + let t = create_typevar(db, "T"); + let builder = ConstraintSetBuilder::new(); + let t_int = create_constraint(db, &builder, t, KnownClass::Int); + let t_str = create_constraint(db, &builder, t, KnownClass::Str); + let set = t_int.or(db, &builder, || t_str); + let source_orders = builder + .storage + .borrow() + .calculate_source_orders(set.source_order); + let expected = PathBounds::compute( + db, + &env, + &mut builder.storage.borrow_mut(), + set.node, + TypeVarSet::from_typevars(db, [t]), + set.source_order, + ); + + // Both limits interrupt an edge with path-local assignments: the visit limit stops + // below the root, and the path limit stops after collecting the first alternative. + for (remaining_paths, remaining_visits, error) in [ + (usize::MAX, 1, ProjectionError::TraversalBudgetExceeded), + (1, usize::MAX, ProjectionError::PathBudgetExceeded), + ] { + let mut path = path_assignments_for(db, &env, &builder, set.node, set.source_order); + let mut storage = builder.storage.borrow_mut(); + let mut limits = BoundedSolutionLimits { + remaining_paths, + remaining_visits, + }; + let mut walker = SolutionWalker::new(source_orders.clone()); + assert_eq!( + walker.visit_node(db, &env, &mut storage, &mut path, set.node, &mut limits), + ControlFlow::Break(error) + ); + drop(walker); + + let mut limits = UnboundedSolutionLimits; + let mut walker = SolutionWalker::new(source_orders.clone()); + let ControlFlow::Continue(()) = + walker.visit_node(db, &env, &mut storage, &mut path, set.node, &mut limits); + assert_eq!(walker.finish(db, &env, &mut storage), expected); + } + } +} diff --git a/crates/ty_python_semantic/src/types/constraints/sequents.rs b/crates/ty_python_semantic/src/types/constraints/sequents.rs new file mode 100644 index 0000000000000..ea5bb4962ab58 --- /dev/null +++ b/crates/ty_python_semantic/src/types/constraints/sequents.rs @@ -0,0 +1,1515 @@ +//! The [`SequentMap`] and related functionality + +use std::cell::Cell; +use std::fmt::{Debug, Display}; + +use smallvec::SmallVec; + +use crate::types::constraints::{ + ALWAYS_FALSE, ALWAYS_TRUE, ConstraintBound, ConstraintBounds, ConstraintId, + ConstraintSetBuilder, ConstraintSetStorage, IntersectionResult, Node, +}; +use crate::types::typevar::TypeVarSet; +use crate::types::variance::VarianceInferable; +use crate::types::visitor::{ + TypeCollector, TypeVisitor, any_over_type, walk_type_with_recursion_guard, +}; +use crate::types::{BoundTypeVarInstance, Type, TypeVarVariance}; +use crate::{Db, ProgramEnvironment}; + +/// A collection of _sequents_ that describe how the constraints mentioned in a BDD relate to each +/// other. These are used in several BDD operations that need to know about "derived facts" even if +/// they are not mentioned in the BDD directly. These operations involve walking one or more paths +/// from the root node to a terminal node. Each sequent describes paths that are invalid (which are +/// pruned from the search), and new constraints that we can assume to be true even if we haven't +/// seen them directly. +/// +/// Sequent maps are primarily used when walking a BDD path with a +/// [`PathAssignments`][super::paths::PathAssignments]. The +/// `PathAssignments` will hold a sequent map containing all of the constraints that are +/// encountered during the walk. It builds up its sequent map lazily, so that it only has to +/// include sequents for the constraints that are actually encountered. However, we also don't want +/// to perform duplicate work if we perform multiple BDD walks on the same constraint set. The +/// [`for_constraint`][Self::for_constraint] and [`for_constraint_pair`][Self::for_constraint_pair] +/// methods are salsa-tracked, to ensure that we only perform them once for any particular +/// constraint or pair of constraints. `PathAssignments` invokes these methods when it encounters a +/// new constraint, and then merges those cached sequents into its own sequent map. (That means we +/// also share the work of calculating the sequent map across `PathAssignments` for _different_ +/// constraint sets.) +#[derive(Debug, Default)] +pub(super) struct SequentMap { + pub(super) sequents: Vec, +} + +/// Describes one rule for deriving new implicit constraints from existing constraints in a BDD +/// path. +#[derive(Clone, Copy, Debug)] +pub(super) enum Sequent { + /// Sequent of the form `¬C → false` + /// + /// This indicates that `C` is always true. Any path that assumes it is false is impossible and + /// can be pruned. + SingleTautology { ante: ConstraintId }, + + /// Sequent of the form `C₁ ∧ C₂ → false` + /// + /// This indicates that `C₁` and `C₂` are disjoint: it is not possible for both to hold. Any + /// path that assumes both is impossible and can be pruned. + PairImpossibility { + ante1: ConstraintId, + ante2: ConstraintId, + }, + + /// Sequent of the form `C → D` + /// + /// This indicates that `C` on its own is enough to imply `D`. For any path that assumes `C` + /// holds, we can add `D` to the path even if it doesn't appear in the BDD. + SingleImplication { + ante: ConstraintId, + post: ConstraintId, + }, + + /// Sequent of the form `C₁ ∧ C₂ → D` + /// + /// This indicates that if `C₁` and `C₂` are both true, then `D` is guaranteed to be true as + /// well. For any path that assumes both `C₁` and `C₂` hold, we can add `D` to the path even if + /// it doesn't appear in the BDD. + PairImplication { + ante1: ConstraintId, + ante2: ConstraintId, + post: ConstraintId, + }, +} + +impl SequentMap { + /// Returns a sequent map containing the sequents that we can infer from a single constraint in + /// isolation. This method is salsa-tracked so that we only perform this work once per + /// constraint. + pub(super) fn for_constraint<'db, 'c>( + db: &'db dyn Db, + env: &ProgramEnvironment<'db>, + storage: &'c mut ConstraintSetStorage<'db>, + constraint: ConstraintId, + ) -> &'c Self { + let key = constraint; + if !storage.single_sequent_cache.contains_key(&key) { + tracing::trace!( + target: "ty_python_semantic::types::constraints::SequentMap", + constraint = %constraint.display(db, env, storage), + "add sequents for constraint", + ); + let mut map = SequentMap::default(); + map.add_sequents_for_single(db, env, storage, constraint); + storage.single_sequent_cache.insert(key, map); + } + &storage.single_sequent_cache[&key] + } + + /// Returns a sequent map containing the sequents that we can infer from a pair of constraints. + /// This method is salsa-tracked so that we only perform this work once per constraint pair. + /// + /// (Note that this method is _not_ commutative; you should provide `left` and `right` in the + /// order that they appear in the source code, so that we can construct derived constraints + /// that retain that ordering.) + pub(super) fn for_constraint_pair<'db, 'c>( + db: &'db dyn Db, + env: &ProgramEnvironment<'db>, + storage: &'c mut ConstraintSetStorage<'db>, + left: ConstraintId, + right: ConstraintId, + ) -> &'c Self { + let key = (left, right); + if !storage.pair_sequent_cache.contains_key(&key) { + tracing::trace!( + target: "ty_python_semantic::types::constraints::SequentMap", + left = %left.display(db, env, storage), + right = %right.display(db, env, storage), + "add sequents for constraint pair", + ); + let mut map = SequentMap::default(); + map.add_sequents_for_pair(db, env, storage, left, right); + storage.pair_sequent_cache.insert(key, map); + } + &storage.pair_sequent_cache[&key] + } + + /// Quickly determines whether two constraints cannot possibly produce any sequents when passed + /// to [`for_constraint_pair`][Self::for_constraint_pair]. If this returns `true`, it is safe + /// to skip calling `for_constraint_pair` for this pair of constraints. + pub(super) fn pair_cannot_produce_sequents<'db>( + db: &'db dyn Db, + env: &ProgramEnvironment<'db>, + storage: &mut ConstraintSetStorage<'db>, + left: ConstraintId, + right: ConstraintId, + ) -> bool { + // Currently, the only pattern we look for is when two constraints that have _only_ lower + // bounds, where those lower bounds are disjoint. Given `l₁ ≤ T ∧ l₂ ≤ T`, the only + // sequent we could theoretically produce is `(l₁ | l₂) ≤ T`. But we don't store that as a + // single constraint; we always break that apart into the two smaller constraints that we + // started with. + + let left = storage.constraint_data(left); + let right = storage.constraint_data(right); + if !left.typevar.is_same_typevar_as(db, right.typevar) { + return false; + } + + let (Some(left_lower), Some(right_lower)) = (left.bounds.lower, right.bounds.lower) else { + return false; + }; + if left.bounds.upper.is_some() || right.bounds.upper.is_some() { + return false; + } + let left_lower = left_lower.ty(); + let right_lower = right_lower.ty(); + + // This call might need its own borrow of the builder's storage, so create a new builder + // that it can use. + let builder = ConstraintSetBuilder::new(); + left_lower + .when_trivially_disjoint_from(db, env, right_lower, &builder, TypeVarSet::None) + .is_trivially_always_satisfied() + } + + fn add_single_tautology(&mut self, ante: ConstraintId) { + self.sequents.push(Sequent::SingleTautology { ante }); + } + + fn add_pair_impossibility(&mut self, ante1: ConstraintId, ante2: ConstraintId) { + self.sequents + .push(Sequent::PairImpossibility { ante1, ante2 }); + } + + fn add_pair_implication<'db>( + &mut self, + db: &'db dyn Db, + env: &ProgramEnvironment<'db>, + storage: &mut ConstraintSetStorage<'db>, + ante1: ConstraintId, + ante2: ConstraintId, + post: ConstraintId, + ) { + // If the post constraint is unsatisfiable, then the antecedents contradict each other. + let post_data = storage.constraint_data(post); + let post_lower = post_data.bounds.lower_bound().ty(); + let post_upper = post_data.bounds.upper_bound().ty(); + let (when, source_order) = storage.load( + db, + env, + &post_lower.when_constraint_set_assignable_to_owned(db, env, post_upper), + ); + if when.is_never_satisfied(db, env, storage, source_order) { + self.add_pair_impossibility(ante1, ante2); + return; + } + + // If either antecedent implies the consequent on its own, this new sequent is redundant. + if ante1.implies(db, env, storage, post) || ante2.implies(db, env, storage, post) { + return; + } + + self.sequents + .push(Sequent::PairImplication { ante1, ante2, post }); + } + + fn add_single_implication(&mut self, ante: ConstraintId, post: ConstraintId) { + if ante == post { + return; + } + + self.sequents + .push(Sequent::SingleImplication { ante, post }); + } + + fn add_sequents_for_single<'db>( + &mut self, + db: &'db dyn Db, + env: &ProgramEnvironment<'db>, + storage: &mut ConstraintSetStorage<'db>, + constraint: ConstraintId, + ) { + // If this constraint binds its typevar to `Never ≤ T ≤ object`, then the typevar can take + // on any type, and the constraint is always satisfied. + let constraint_data = storage.constraint_data(constraint); + let lower = constraint_data.bounds.lower_bound().ty(); + let upper = constraint_data.bounds.upper_bound().ty(); + if lower.is_never() && upper.is_object() { + self.add_single_tautology(constraint); + return; + } + + // Given a constraint `L ≤ T ≤ U`, `L ≤ U` must also hold. If those bounds contain other + // typevars, we can infer additional constraints. This is easiest to see when the bounds + // _are_ typevars: + // + // 1. `(S ≤ T ≤ U) → (S ≤ U)` + // 2. `(S ≤ T ≤ τ) → (S ≤ τ)` + // 3. `(τ ≤ T ≤ U) → (τ ≤ U)` + // + // but it also holds when the bounds _contain_ typevars: + // + // 4. `(Covariant[S] ≤ T ≤ Covariant[U]) → (S ≤ U)` + // `(Covariant[S] ≤ T ≤ Covariant[τ]) → (S ≤ τ)` + // `(Covariant[τ] ≤ T ≤ Covariant[U]) → (τ ≤ U)` + // + // 5. `(Contravariant[S] ≤ T ≤ Contravariant[U]) → (U ≤ S)` + // `(Contravariant[S] ≤ T ≤ Contravariant[τ]) → (τ ≤ S)` + // `(Contravariant[τ] ≤ T ≤ Contravariant[U]) → (U ≤ τ)` + // + // 6. `(Invariant[S] ≤ T ≤ Invariant[U]) → (S = U)` + // `(Invariant[S] ≤ T ≤ Invariant[τ]) → (S = τ)` + // `(Invariant[τ] ≤ T ≤ Invariant[U]) → (τ = U)` + // + // and whenever the bounds are assignable, even if they don't mention exactly the same + // types: + // + // class Sub(Covariant[int]): ... + // + // 7. `(Covariant[S] ≤ T ≤ Sub) → (S ≤ int)` + // `(Sub ≤ T ≤ Covariant[U]) → (int ≤ U)` + // + // To handle all of these cases, we perform a constraint set assignability check to see + // when `L ≤ U`. This gives us a constraint set, which should be the rhs of the sequent + // implication. (That is, this check directly encodes `(L ≤ T ≤ U) → (L ≤ U)` as an + // implication.) + + // Skip trivial cases where the assignability check won't produce useful results. + if lower.is_never() || upper.is_object() { + return; + } + + let (when, source_order) = storage.load( + db, + env, + &lower.when_constraint_set_assignable_to_owned(db, env, upper), + ); + + // If L is _never_ assignable to U, this constraint would violate transitivity, and should + // never have been added. + #[expect(clippy::debug_assert_with_mut_call)] + { + debug_assert!(!when.is_never_satisfied(db, env, storage, source_order)); + } + + // Fast path: If L is trivially always assignable to U, there are no derived constraints + // that we can infer. This would be handled correctly by the logic below, but this is a + // useful early return. Since we only use this check as an early return happy path, we can + // accept false negatives. That lets us use the simpler and cheaper check against + // ALWAYS_TRUE, rather than a more expensive is_always_satisfiable call. + if when == ALWAYS_TRUE { + return; + } + + // Technically, we've just calculated a _constraint set_ as the rhs of this implication. + // Unfortunately, our sequent map can currently only store implications where the rhs is a + // single constraint. + // + // If the constraint set that we get represents a single conjunction, we can still shoehorn + // it into this shape, since we can "break apart" a conjunction on the rhs of an + // implication: + // + // a → b ∧ c ∧ d + // + // becomes + // + // a → b + // a → c + // a → d + // + // That takes care of breaking apart the rhs conjunction: we can add each positive + // constraint as a separate single_implication. + // + // We can also handle _negative_ constraints, because those turn into impossibilities: + // + // a → ¬b + // + // becomes + // + // a ∧ b → false + // + // TODO: This should handle the most common cases. In the future, we could handle arbitrary + // rhs constraint sets by moving this logic into PathAssignments::walk_path, and performing + // it once for _every_ root→always path in the BDD. (That would require resetting the + // PathAssignments state for each of those paths, which is why the logic would have to + // move.) + let mut node = when; + if !node.is_single_conjunction(storage) { + return; + } + + loop { + match node.node() { + Node::AlwaysTrue | Node::AlwaysFalse => break, + Node::Interior(interior) => { + let interior = storage.interior_node_data(interior.node()); + let derived = storage.constraint_data(interior.constraint); + let derived = ConstraintId::new_with_bounds( + db, + env, + storage, + derived.typevar, + derived + .bounds + .lower + .map(|bound| bound.with_source_provenance(constraint_data.bounds)), + derived + .bounds + .upper + .map(|bound| bound.with_source_provenance(constraint_data.bounds)), + ); + if interior.if_true != ALWAYS_FALSE { + self.add_single_implication(constraint, derived); + node = interior.if_true; + } else { + self.add_pair_impossibility(constraint, derived); + node = interior.if_false; + } + } + } + } + } + + fn add_sequents_for_pair<'db>( + &mut self, + db: &'db dyn Db, + env: &ProgramEnvironment<'db>, + storage: &mut ConstraintSetStorage<'db>, + left_constraint: ConstraintId, + right_constraint: ConstraintId, + ) { + // If either of the constraints has another typevar as a lower/upper bound, the only + // sequents we can add are for the transitive closure. For instance, if we have + // `(S ≤ T) ∧ (T ≤ int)`, then `(S ≤ int)` will also hold, and we should add a sequent for + // this implication. These are the `mutual_sequents` mentioned below — sequents that come + // about because two typevars are mutually constrained. + // + // Complicating things is that `(S ≤ T)` will be encoded differently depending on how `S` + // and `T` compare in our arbitrary BDD variable ordering. + // + // When `S` comes before `T`, `(S ≤ T)` will be encoded as `(Never ≤ S ≤ T)`, and the + // overall antecedent will be `(Never ≤ S ≤ T) ∧ (T ≤ int)`. Those two individual + // constraints constrain different typevars (`S` and `T`, respectively), and are handled by + // `add_mutual_sequents_for_different_typevars`. + // + // When `T` comes before `S`, `(S ≤ T)` will be encoded as `(S ≤ T ≤ object)`, and the + // overall antecedent will be `(S ≤ T ≤ object) ∧ (T ≤ int)`. Those two individual + // constraints both constrain `T`, and are handled by + // `add_mutual_sequents_for_same_typevars`. + // + // If all of the lower and upper bounds are concrete (i.e., not typevars), then there + // several _other_ sequents that we can add, as handled by `add_concrete_sequents`. + let left_constraint_data = storage.constraint_data(left_constraint); + let left_typevar = left_constraint_data.typevar; + let right_constraint_data = storage.constraint_data(right_constraint); + let right_typevar = right_constraint_data.typevar; + + if !left_typevar.is_same_typevar_as(db, right_typevar) { + self.add_mutual_sequents_for_different_typevars( + db, + env, + storage, + left_constraint, + right_constraint, + ); + self.add_nested_typevar_sequents(db, env, storage, left_constraint, right_constraint); + } else if left_constraint_data.bounds.lower_bound().ty().is_type_var() + || left_constraint_data.bounds.upper_bound().ty().is_type_var() + || right_constraint_data + .bounds + .lower_bound() + .ty() + .is_type_var() + || right_constraint_data + .bounds + .upper_bound() + .ty() + .is_type_var() + { + self.add_mutual_sequents_for_same_typevars( + db, + env, + storage, + left_constraint, + right_constraint, + ); + } else { + self.add_concrete_sequents(db, env, storage, left_constraint, right_constraint); + } + } + + fn add_mutual_sequents_for_different_typevars<'db>( + &mut self, + db: &'db dyn Db, + env: &ProgramEnvironment<'db>, + storage: &mut ConstraintSetStorage<'db>, + left_constraint: ConstraintId, + right_constraint: ConstraintId, + ) { + // We've structured our constraints so that a typevar's upper/lower bound can only + // be another typevar if the bound is "later" in our arbitrary ordering. That means + // we only have to check this pair of constraints in one direction — though we do + // have to figure out which of the two typevars is constrained, and which one is + // the upper/lower bound. + let left_constraint_data = storage.constraint_data(left_constraint); + let left_typevar = left_constraint_data.typevar; + let right_constraint_data = storage.constraint_data(right_constraint); + let right_typevar = right_constraint_data.typevar; + let (bound_constraint, constrained_constraint) = + if left_typevar.can_be_bound_for(db, storage, right_typevar) { + (left_constraint, right_constraint) + } else { + (right_constraint, left_constraint) + }; + + // We then look for cases where the "constrained" typevar's upper and/or lower bound + // matches the "bound" typevar. If so, we're going to add an implication sequent that + // replaces the upper/lower bound that matched with the bound constraint's corresponding + // bound. + let bound_constraint_data = storage.constraint_data(bound_constraint); + let bound_typevar = bound_constraint_data.typevar; + let constrained_constraint_data = storage.constraint_data(constrained_constraint); + let constrained_typevar = constrained_constraint_data.typevar; + let constrained_lower_bound = constrained_constraint_data.bounds.lower_bound(); + let constrained_upper_bound = constrained_constraint_data.bounds.upper_bound(); + let bound_lower_bound = bound_constraint_data.bounds.lower_bound(); + let bound_upper_bound = bound_constraint_data.bounds.upper_bound(); + + // Transitive pivots require subtyping; classes with dynamic bases can be assignable to + // unrelated types without being subtypes. + let (new_lower, new_upper) = match ( + constrained_lower_bound.ty(), + constrained_upper_bound.ty(), + bound_lower_bound.ty(), + bound_upper_bound.ty(), + ) { + // (B ≤ C ≤ B) ∧ (BL ≤ B ≤ BU) → (BL ≤ C ≤ BU) + (Type::TypeVar(constrained_lower), Type::TypeVar(constrained_upper), _, _) + if constrained_lower.is_same_typevar_as(db, bound_typevar) + && constrained_upper.is_same_typevar_as(db, bound_typevar) => + { + ( + ConstraintBound::from_transitive_derivation( + bound_lower_bound.ty(), + constrained_lower_bound, + bound_lower_bound, + ), + ConstraintBound::from_transitive_derivation( + bound_upper_bound.ty(), + constrained_upper_bound, + bound_upper_bound, + ), + ) + } + + // (CL ≤ C ≤ B) ∧ (BL ≤ B ≤ BU) → (CL ≤ C ≤ BU) + (_, Type::TypeVar(constrained_upper), _, _) + if constrained_upper.is_same_typevar_as(db, bound_typevar) => + { + ( + constrained_lower_bound, + ConstraintBound::from_transitive_derivation( + bound_upper_bound.ty(), + constrained_upper_bound, + bound_upper_bound, + ), + ) + } + + // (B ≤ C ≤ CU) ∧ (BL ≤ B ≤ BU) → (BL ≤ C ≤ CU) + (Type::TypeVar(constrained_lower), _, _, _) + if constrained_lower.is_same_typevar_as(db, bound_typevar) => + { + ( + ConstraintBound::from_transitive_derivation( + bound_lower_bound.ty(), + constrained_lower_bound, + bound_lower_bound, + ), + constrained_upper_bound, + ) + } + + // (CL ≤ C ≤ pivot) ∧ (pivot ≤ B ≤ BU) → (CL ≤ C ≤ B) + (_, constrained_upper, bound_lower, _) + if !constrained_upper.is_never() + && !constrained_upper.is_object() + && storage.cached_is_constraint_set_subtype_of( + db, + env, + constrained_upper.top_materialization(db, env), + bound_lower.bottom_materialization(db, env), + ) => + { + ( + constrained_lower_bound, + ConstraintBound::from_transitive_derivation( + Type::TypeVar(bound_typevar), + constrained_upper_bound, + bound_lower_bound, + ), + ) + } + + // (pivot ≤ C ≤ CU) ∧ (BL ≤ B ≤ pivot) → (B ≤ C ≤ CU) + (constrained_lower, _, _, bound_upper) + if !constrained_lower.is_never() + && !constrained_lower.is_object() + && storage.cached_is_constraint_set_subtype_of( + db, + env, + bound_upper.top_materialization(db, env), + constrained_lower.bottom_materialization(db, env), + ) => + { + ( + ConstraintBound::from_transitive_derivation( + Type::TypeVar(bound_typevar), + constrained_lower_bound, + bound_upper_bound, + ), + constrained_upper_bound, + ) + } + + _ => return, + }; + + let mut post_constraints: SmallVec<[ConstraintId; 3]> = SmallVec::new(); + // These are derived logical constraints, not direct inference evidence. Avoid preserving + // explicit bounds that are equivalent to missing lower/upper bounds, so a derived + // `T ≤ U ≤ object` can satisfy a later query for `T ≤ U` without requiring a separate + // materialized-default implication. + let mut constrained_lower = (!new_lower.ty().is_never()).then_some(new_lower); + let mut constrained_upper = (!new_upper.ty().is_object()).then_some(new_upper); + + // The transitive rule above gives us an intended post-condition + // `new_lower ≤ [constrained] ≤ new_upper`. + // + // If a top-level bound typevar is "earlier" than `constrained`, we cannot represent that + // directly as a bound on `constrained` without violating our canonical ordering. + // Instead, split it into equivalent canonical constraints by "moving" that bound onto the + // other typevar: + // + // invalid lower `L ≤ [C]` -> `(Never ≤ [L] ≤ C)` and drop `L` from C's lower bound + // invalid upper `[C] ≤ U` -> `(C ≤ [U] ≤ object)` and drop `U` from C's upper bound + // + // Example: if we derive `[A] ≤ T ≤ [B]` but `A`/`B` are not valid top-level bounds for + // `T` in this ordering, we emit two pair implications: + // `(Never ≤ [A] ≤ T)` and `(T ≤ [B] ≤ object)`. + // This preserves the relationship while keeping all derived constraints canonical. + if let Type::TypeVar(lower_bound_typevar) = new_lower.ty() + && !lower_bound_typevar.can_be_bound_for(db, storage, constrained_typevar) + { + post_constraints.push(ConstraintId::new_with_bounds( + db, + env, + storage, + lower_bound_typevar, + None, + Some(new_lower.with_type(Type::TypeVar(constrained_typevar))), + )); + constrained_lower = None; + } + + if let Type::TypeVar(upper_bound_typevar) = new_upper.ty() + && !upper_bound_typevar.can_be_bound_for(db, storage, constrained_typevar) + { + post_constraints.push(ConstraintId::new_with_bounds( + db, + env, + storage, + upper_bound_typevar, + Some(new_upper.with_type(Type::TypeVar(constrained_typevar))), + None, + )); + constrained_upper = None; + } + + if constrained_lower.is_some() || constrained_upper.is_some() { + post_constraints.push(ConstraintId::new_with_bounds( + db, + env, + storage, + constrained_typevar, + constrained_lower, + constrained_upper, + )); + } + + for post_constraint in post_constraints { + self.add_pair_implication( + db, + env, + storage, + left_constraint, + right_constraint, + post_constraint, + ); + } + } + + /// Adds sequents for the case where one constraint's lower or upper bound contains another + /// constraint's typevar nested inside a parameterized type (e.g., `U ≤ Covariant[T]`). + /// + /// This is distinct from `add_mutual_sequents_for_different_typevars`, which handles the case + /// where a typevar appears _directly_ as a top-level lower/upper bound (e.g., `U ≤ T`). A + /// bare `Type::TypeVar` is technically a special case of covariant nesting (since the variance + /// of `T` in `T` itself is covariant), but the existing direct-typevar logic handles it + /// separately because it requires careful canonical ordering of typevar-to-typevar constraints + /// that the generic nested-typevar logic here does not need to worry about. + fn add_nested_typevar_sequents<'db>( + &mut self, + db: &'db dyn Db, + env: &ProgramEnvironment<'db>, + storage: &mut ConstraintSetStorage<'db>, + left_constraint: ConstraintId, + right_constraint: ConstraintId, + ) { + // Keep this precheck aligned with `variance_of`, which visits lazy types. + let has_typevar_bound = |bounds: ConstraintBounds<'db>| { + bounds + .lower + .is_some_and(|lower| any_over_type(db, env, lower.ty(), true, Type::is_type_var)) + || bounds.upper.is_some_and(|upper| { + any_over_type(db, env, upper.ty(), true, Type::is_type_var) + }) + }; + if !has_typevar_bound(storage.constraint_data(left_constraint).bounds) + && !has_typevar_bound(storage.constraint_data(right_constraint).bounds) + { + return; + } + + let mut try_tightening = + |bound_constraint: ConstraintId, constrained_constraint: ConstraintId| { + let bound_data = storage.constraint_data(bound_constraint); + let bound_typevar = bound_data.typevar; + let bound_identity = bound_typevar.identity(db); + let bound_lower_bound = bound_data.bounds.lower_bound(); + let bound_upper_bound = bound_data.bounds.upper_bound(); + let constrained_data = storage.constraint_data(constrained_constraint); + let constrained_typevar = constrained_data.typevar; + let constrained_identity = constrained_typevar.identity(db); + let constrained_lower_bound = constrained_data.bounds.lower_bound(); + let constrained_upper_bound = constrained_data.bounds.upper_bound(); + let constrained_lower = constrained_lower_bound.ty(); + let constrained_upper = constrained_upper_bound.ty(); + + // If the replacement contains the bound typevar itself (e.g., the bound + // constraint is `_V ≤ G[_V]`), or the constrained typevar (e.g., the bound + // constraint is `_T ≤ G[_V]` and we're about to substitute into `_V ≤ G[_T]`), + // substituting would create a deeper nesting of the same recursive pattern + // that triggers the same substitution again ad infinitum. Skip in both cases. + // + // Fast-path bare typevar replacements (`Type::TypeVar`) using equality checks + // instead of calling `variance_of` on them. This avoids a large number of tiny + // tracked `variance_of` queries in hot paths. + let replacement_mentions_bound_or_constrained = |replacement: Type<'db>| { + replacement.variance_of(db, env, bound_identity) != TypeVarVariance::Bivariant + || replacement.variance_of(db, env, constrained_identity) + != TypeVarVariance::Bivariant + }; + + // Check the upper bound of the constrained constraint for nested occurrences of + // the bound typevar. We use `variance_of` as our combined presence + variance + // check: `Bivariant` means the typevar doesn't appear in the type (or is genuinely + // bivariant, which is semantically equivalent — no implication is needed in either + // case). + // + // Note: if `Bivariant` is ever removed from the `TypeVarVariance` enum, we would + // need an alternative representation for "typevar not present" + // (e.g., `Option`). + let upper_replacement = match ( + constrained_upper.variance_of(db, env, bound_identity), + bound_lower_bound.ty(), + bound_upper_bound.ty(), + ) { + (TypeVarVariance::Bivariant, _, _) => None, + // Skip bare typevars — those are handled by + // `add_mutual_sequents_for_different_typevars`. + _ if constrained_upper.is_type_var() => None, + // Covariance preserves direction: upper bound on T substitutes into upper + // bound. A ≤ B → G[A] ≤ G[B], so (T ≤ u_B) gives G[T] ≤ G[u_B]. + (TypeVarVariance::Covariant, _, bound_upper) if !bound_upper.is_object() => { + Some(bound_upper_bound) + } + // Contravariance flips direction: lower bound on T substitutes into upper + // bound. A ≤ B → G[B] ≤ G[A], so (l_B ≤ T) gives G[T] ≤ G[l_B]. + (TypeVarVariance::Contravariant, bound_lower, _) if !bound_lower.is_never() => { + Some(bound_lower_bound) + } + // Invariance requires equality: only substitute if l_B = u_B. + (TypeVarVariance::Invariant, bound_lower, bound_upper) + if bound_lower == bound_upper && !bound_lower.is_never() => + { + Some(ConstraintBound::from_combination( + bound_lower, + bound_lower_bound, + bound_upper_bound, + )) + } + _ => None, + }; + let upper_replacement = upper_replacement.filter(|replacement| { + // Substituting one typevar for another into large unions can generate many + // very-weak derived constraints and cause severe performance regressions. + // Keep the common/non-union case enabled; skip union upper bounds for this + // specific typevar-to-typevar replacement shape. + if replacement.ty().is_type_var() && constrained_upper.is_union() { + return false; + } + !replacement_mentions_bound_or_constrained(replacement.ty()) + }); + if let Some(replacement) = upper_replacement { + let new_upper = constrained_upper.substitute_one_typevar( + db, + env, + bound_typevar, + replacement.ty(), + ); + if new_upper != constrained_upper { + let post = ConstraintId::new_with_bounds( + db, + env, + storage, + constrained_typevar, + constrained_data.bounds.lower, + Some(ConstraintBound::from_transitive_derivation( + new_upper, + constrained_upper_bound, + replacement, + )), + ); + self.add_pair_implication( + db, + env, + storage, + bound_constraint, + constrained_constraint, + post, + ); + } + } + + // Check the lower bound of the constrained constraint for nested occurrences. + let lower_replacement = match ( + constrained_lower.variance_of(db, env, bound_identity), + bound_lower_bound.ty(), + bound_upper_bound.ty(), + ) { + (TypeVarVariance::Bivariant, _, _) => None, + _ if constrained_lower.is_type_var() => None, + // Covariance preserves direction: lower bound on T substitutes into lower + // bound. A ≤ B → G[A] ≤ G[B], so (l_B ≤ T) gives G[l_B] ≤ G[T]. + (TypeVarVariance::Covariant, bound_lower, _) if !bound_lower.is_never() => { + Some(bound_lower_bound) + } + // Contravariance flips direction: upper bound on T substitutes into lower + // bound. A ≤ B → G[B] ≤ G[A], so (T ≤ u_B) gives G[u_B] ≤ G[T]. + (TypeVarVariance::Contravariant, _, bound_upper) + if !bound_upper.is_object() => + { + Some(bound_upper_bound) + } + // Invariance requires equality: only substitute if l_B = u_B. + (TypeVarVariance::Invariant, bound_lower, bound_upper) + if bound_lower == bound_upper && !bound_lower.is_never() => + { + Some(ConstraintBound::from_combination( + bound_lower, + bound_lower_bound, + bound_upper_bound, + )) + } + _ => None, + }; + let lower_replacement = lower_replacement.filter(|replacement| { + // Substituting one typevar for another into large intersections can generate + // many very-weak derived constraints and cause severe performance regressions. + // Keep the common/non-intersection case enabled; skip intersection lower + // bounds for this specific typevar-to-typevar replacement shape. + if replacement.ty().is_type_var() && constrained_lower.is_intersection() { + return false; + } + !replacement_mentions_bound_or_constrained(replacement.ty()) + }); + if let Some(replacement) = lower_replacement { + let new_lower = constrained_lower.substitute_one_typevar( + db, + env, + bound_typevar, + replacement.ty(), + ); + if new_lower != constrained_lower { + let post = ConstraintId::new_with_bounds( + db, + env, + storage, + constrained_typevar, + Some(ConstraintBound::from_transitive_derivation( + new_lower, + constrained_lower_bound, + replacement, + )), + constrained_data.bounds.upper, + ); + self.add_pair_implication( + db, + env, + storage, + bound_constraint, + constrained_constraint, + post, + ); + } + } + }; + + try_tightening(left_constraint, right_constraint); + try_tightening(right_constraint, left_constraint); + + // Additionally, check if one constraint's bare typevar *bound* appears nested in the other + // constraint's bounds. This handles the "dual" direction: instead of substituting a + // typevar's concrete bounds into another constraint (tightening), we substitute the + // typevar itself for one of its bare typevar bounds (weakening), creating a cross-typevar + // link. + // + // For example, given `(Covariant[S] ≤ C) ∧ (Never ≤ B ≤ S)`, S is B's upper bound and + // appears covariantly in C's lower bound. Since `B ≤ S`, covariance tells us that + // `Covariant[B] ≤ Covariant[S]`. Transitivity then lets us derive `Covariant[B] ≤ C`. + // + // The derived constraint is weaker than the original, but it introduces a relationship + // between B and C that we need to remember and propagate if we ever existentially quantify + // away S. + // + // TODO: This only handles the case where the bound (in this case, S) is a bare typevar. A + // future extension could handle arbitrary types by pattern-matching on generic alias + // structure. + // + // This is defined as a separate closure because it iterates over the bound constraint's + // bare typevar bounds, which is a different axis than `try_tightening`'s check on the + // bound constraint's typevar. + let mut try_weakening = + |bound_constraint: ConstraintId, constrained_constraint: ConstraintId| { + let bound_data = storage.constraint_data(bound_constraint); + let bound_typevar = bound_data.typevar; + let bound_lower_bound = bound_data.bounds.lower_bound(); + let bound_upper_bound = bound_data.bounds.upper_bound(); + let bound_lower = bound_lower_bound.ty(); + let constrained_data = storage.constraint_data(constrained_constraint); + let constrained_typevar = constrained_data.typevar; + let constrained_lower_bound = constrained_data.bounds.lower_bound(); + let constrained_upper_bound = constrained_data.bounds.upper_bound(); + let constrained_lower = constrained_lower_bound.ty(); + let constrained_upper = constrained_upper_bound.ty(); + + let mut try_one_bound = |bound: ConstraintBound<'db>, is_upper_bound: bool| { + let Some(nested_typevar) = bound.ty().as_typevar() else { + return; + }; + + // Skip if the nested typevar is the same as the constrained typevar — that + // case is handled by `add_mutual_sequents_for_different_typevars`. + if nested_typevar.is_same_typevar_as(db, constrained_typevar) + || nested_typevar.is_same_typevar_as(db, bound_typevar) + { + return; + } + + let replacement = Type::TypeVar(bound_typevar); + + // Check the constrained constraint's upper bound for nested occurrences of + // nested_typevar (S). We want to *weaken* (relax) the upper bound by making it + // larger: + // - Covariant + S is B's lower bound (S ≤ B): G[S] ≤ G[B] → weaker. Emit. + // - Contravariant + S is B's upper bound (B ≤ S): G[S] ≤ G[B] → weaker. Emit. + // - Other combinations tighten rather than weaken. Skip. + let should_weaken_upper = !constrained_upper.is_type_var() + && !constrained_upper.is_never() + && !constrained_upper.is_object() + && !constrained_upper.is_dynamic() + && match constrained_upper.variance_of(db, env, nested_typevar.identity(db)) + { + TypeVarVariance::Bivariant => false, + TypeVarVariance::Covariant => !is_upper_bound, + TypeVarVariance::Contravariant => is_upper_bound, + TypeVarVariance::Invariant => { + bound_lower_bound.ty() == bound_upper_bound.ty() + && !bound_lower.is_never() + } + }; + if should_weaken_upper { + let new_upper = constrained_upper.substitute_one_typevar( + db, + env, + nested_typevar, + replacement, + ); + if new_upper != constrained_upper { + let post = ConstraintId::new_with_bounds( + db, + env, + storage, + constrained_typevar, + constrained_data.bounds.lower, + Some(ConstraintBound::from_transitive_derivation( + new_upper, + constrained_upper_bound, + bound, + )), + ); + self.add_pair_implication( + db, + env, + storage, + bound_constraint, + constrained_constraint, + post, + ); + } + } + + // Ditto for the lower bound. + let should_weaken_lower = !constrained_lower.is_type_var() + && !constrained_lower.is_never() + && !constrained_lower.is_object() + && !constrained_lower.is_dynamic() + && match constrained_lower.variance_of(db, env, nested_typevar.identity(db)) + { + TypeVarVariance::Bivariant => false, + TypeVarVariance::Covariant => is_upper_bound, + TypeVarVariance::Contravariant => !is_upper_bound, + TypeVarVariance::Invariant => { + bound_lower_bound.ty() == bound_upper_bound.ty() + && !bound_lower.is_never() + } + }; + if should_weaken_lower { + let new_lower = constrained_lower.substitute_one_typevar( + db, + env, + nested_typevar, + replacement, + ); + if new_lower != constrained_lower { + let post = ConstraintId::new_with_bounds( + db, + env, + storage, + constrained_typevar, + Some(ConstraintBound::from_transitive_derivation( + new_lower, + constrained_lower_bound, + bound, + )), + constrained_data.bounds.upper, + ); + self.add_pair_implication( + db, + env, + storage, + bound_constraint, + constrained_constraint, + post, + ); + } + } + }; + + // For each bare typevar bound S of the bound constraint, check if S appears + // nested in the constrained constraint's bounds. If so, we can substitute B + // (the bound constraint's typevar) for S, producing a weaker but useful + // constraint. + if let Some(upper) = bound_data.bounds.upper { + try_one_bound(upper, true); + } + if let Some(lower) = bound_data.bounds.lower { + try_one_bound(lower, false); + } + }; + + try_weakening(left_constraint, right_constraint); + try_weakening(right_constraint, left_constraint); + } + + fn add_mutual_sequents_for_same_typevars<'db>( + &mut self, + db: &'db dyn Db, + env: &ProgramEnvironment<'db>, + storage: &mut ConstraintSetStorage<'db>, + left_constraint: ConstraintId, + right_constraint: ConstraintId, + ) { + let mut try_one_direction = + |left_constraint: ConstraintId, right_constraint: ConstraintId| { + let left_constraint_data = storage.constraint_data(left_constraint); + let left_lower = left_constraint_data.bounds.lower_bound(); + let left_upper = left_constraint_data.bounds.upper_bound(); + let right_constraint_data = storage.constraint_data(right_constraint); + let right_lower = right_constraint_data.bounds.lower_bound(); + let right_upper = right_constraint_data.bounds.upper_bound(); + let mut new_constraints = + |bound_typevar: BoundTypeVarInstance<'db>, + mut right_lower: Option>, + mut right_upper: Option>| { + if let Some(right_lower_bound) = right_lower + && let Type::TypeVar(other_bound_typevar) = right_lower_bound.ty() + && bound_typevar.is_same_typevar_as(db, other_bound_typevar) + { + right_lower = None; + } + if let Some(right_upper_bound) = right_upper + && let Type::TypeVar(other_bound_typevar) = right_upper_bound.ty() + && bound_typevar.is_same_typevar_as(db, other_bound_typevar) + { + right_upper = None; + } + + // Same idea as `add_mutual_sequents_for_different_typevars`: if a derived + // post-condition for `[bound]` has top-level typevar bounds in the wrong + // orientation, split it into equivalent canonical constraints instead of + // dropping it. + let mut post_constraints: SmallVec<[ConstraintId; 3]> = SmallVec::new(); + // These are derived logical constraints, not direct inference evidence. + // Avoid preserving explicit bounds that are equivalent to missing + // lower/upper bounds; direct constraints still retain their explicit + // bound presence. + let mut constrained_lower = + right_lower.filter(|bound| !bound.ty().is_never()); + let mut constrained_upper = + right_upper.filter(|bound| !bound.ty().is_object()); + + if let Some(right_lower_bound) = right_lower + && let Type::TypeVar(lower_bound_typevar) = right_lower_bound.ty() + && !lower_bound_typevar.can_be_bound_for(db, storage, bound_typevar) + { + post_constraints.push(ConstraintId::new_with_bounds( + db, + env, + storage, + lower_bound_typevar, + None, + Some(right_lower_bound.with_type(Type::TypeVar(bound_typevar))), + )); + constrained_lower = None; + } + + if let Some(right_upper_bound) = right_upper + && let Type::TypeVar(upper_bound_typevar) = right_upper_bound.ty() + && !upper_bound_typevar.can_be_bound_for(db, storage, bound_typevar) + { + post_constraints.push(ConstraintId::new_with_bounds( + db, + env, + storage, + upper_bound_typevar, + Some(right_upper_bound.with_type(Type::TypeVar(bound_typevar))), + None, + )); + constrained_upper = None; + } + + if constrained_lower.is_some() || constrained_upper.is_some() { + post_constraints.push(ConstraintId::new_with_bounds( + db, + env, + storage, + bound_typevar, + constrained_lower, + constrained_upper, + )); + } + + post_constraints + }; + let post_constraints = match (left_lower.ty(), left_upper.ty()) { + (Type::TypeVar(bound_typevar), Type::TypeVar(other_bound_typevar)) + if bound_typevar.is_same_typevar_as(db, other_bound_typevar) => + { + new_constraints( + bound_typevar, + Some(ConstraintBound::from_transitive_derivation( + right_lower.ty(), + left_lower, + right_lower, + )), + Some(ConstraintBound::from_transitive_derivation( + right_upper.ty(), + left_upper, + right_upper, + )), + ) + } + (Type::TypeVar(bound_typevar), _) => new_constraints( + bound_typevar, + None, + Some(ConstraintBound::from_transitive_derivation( + right_upper.ty(), + left_lower, + right_upper, + )), + ), + (_, Type::TypeVar(bound_typevar)) => new_constraints( + bound_typevar, + Some(ConstraintBound::from_transitive_derivation( + right_lower.ty(), + left_upper, + right_lower, + )), + None, + ), + _ => return, + }; + for post_constraint in post_constraints { + self.add_pair_implication( + db, + env, + storage, + left_constraint, + right_constraint, + post_constraint, + ); + } + }; + + try_one_direction(left_constraint, right_constraint); + try_one_direction(right_constraint, left_constraint); + } + + fn add_concrete_sequents<'db>( + &mut self, + db: &'db dyn Db, + env: &ProgramEnvironment<'db>, + storage: &mut ConstraintSetStorage<'db>, + left_constraint: ConstraintId, + right_constraint: ConstraintId, + ) { + // These might seem redundant with the intersection check below, since `a → b` means that + // `a ∧ b = a`. But we are not normalizing constraint bounds, and these clauses help us + // identify constraints that are identical besides e.g. ordering of union/intersection + // elements. (For instance, when processing `T ≤ τ₁ & τ₂` and `T ≤ τ₂ & τ₁`, these clauses + // would add sequents for `(T ≤ τ₁ & τ₂) → (T ≤ τ₂ & τ₁)` and vice versa.) + if storage.cached_constraint_implies(db, env, left_constraint, right_constraint) { + tracing::trace!( + target: "ty_python_semantic::types::constraints::SequentMap", + left = %left_constraint.display(db, env, storage), + right = %right_constraint.display(db, env, storage), + "left implies right", + ); + self.add_single_implication(left_constraint, right_constraint); + } + if storage.cached_constraint_implies(db, env, right_constraint, left_constraint) { + tracing::trace!( + target: "ty_python_semantic::types::constraints::SequentMap", + left = %left_constraint.display(db, env, storage), + right = %right_constraint.display(db, env, storage), + "right implies left", + ); + self.add_single_implication(right_constraint, left_constraint); + } + + match left_constraint.intersect(db, env, storage, right_constraint) { + IntersectionResult::Simplified(intersection_constraint_data) => { + let intersection_constraint = + storage.intern_constraint(db, env, intersection_constraint_data); + tracing::trace!( + target: "ty_python_semantic::types::constraints::SequentMap", + left = %left_constraint.display(db, env, storage), + right = %right_constraint.display(db, env, storage), + intersection = %intersection_constraint.display(db, env, storage), + "left and right overlap", + ); + self.add_pair_implication( + db, + env, + storage, + left_constraint, + right_constraint, + intersection_constraint, + ); + self.add_single_implication(intersection_constraint, left_constraint); + self.add_single_implication(intersection_constraint, right_constraint); + } + + // The sequent map only needs to include constraints that might appear in a BDD. If the + // intersection does not collapse to a single constraint, then there's no new + // constraint that we need to add to the sequent map. + IntersectionResult::CannotSimplify => {} + + IntersectionResult::Disjoint => { + tracing::trace!( + target: "ty_python_semantic::types::constraints::SequentMap", + left = %left_constraint.display(db, env, storage), + right = %right_constraint.display(db, env, storage), + "left and right are disjoint", + ); + self.add_pair_impossibility(left_constraint, right_constraint); + } + } + } + + #[expect(dead_code)] // Keep this around for debugging purposes + fn display<'db, 'a>( + &'a self, + db: &'db dyn Db, + env: &'a ProgramEnvironment<'db>, + storage: &'a ConstraintSetStorage<'db>, + prefix: &'a dyn Display, + ) -> impl Display + 'a { + std::fmt::from_fn(move |f| { + let mut first = true; + let mut maybe_write_prefix = |f: &mut std::fmt::Formatter<'_>| { + if first { + first = false; + Ok(()) + } else { + write!(f, "\n{prefix}") + } + }; + + for sequent in &self.sequents { + match sequent { + Sequent::SingleTautology { .. } => {} + + Sequent::PairImpossibility { ante1, ante2 } => { + maybe_write_prefix(f)?; + write!( + f, + "{} ∧ {} → false", + ante1.display(db, env, storage), + ante2.display(db, env, storage), + )?; + } + + Sequent::PairImplication { ante1, ante2, post } => { + maybe_write_prefix(f)?; + write!( + f, + "{} ∧ {} → {}", + ante1.display(db, env, storage), + ante2.display(db, env, storage), + post.display(db, env, storage), + )?; + } + + Sequent::SingleImplication { ante, post } => { + maybe_write_prefix(f)?; + write!( + f, + "{} → {}", + ante.display(db, env, storage), + post.display(db, env, storage) + )?; + } + } + } + + if first { + f.write_str("[no sequents]")?; + } + Ok(()) + }) + } +} + +impl<'db> Type<'db> { + /// Returns whether this type can participate in a transitive sequent proof. + /// + /// Gradual assignability is not transitive, so constraints with dynamic bounds are ineligible. + /// Note that we can't use [`is_fully_static`][Type::is_fully_static] here, since that + /// considers the declared bounds/constraints of typevars. In the context of a sequent map, + /// typevars are opaque symbolic atoms: considering their bounds or defaults could incorrectly + /// make their eligibility depend on a specialization that the sequent is meant to constrain. + pub(super) fn is_static_sequent_eligible( + self, + db: &'db dyn Db, + env: &ProgramEnvironment<'db>, + ) -> bool { + struct EligibilityVisitor<'a, 'db> { + env: &'a ProgramEnvironment<'db>, + seen: TypeCollector<'db>, + eligible: Cell, + } + + impl<'db> TypeVisitor<'db> for EligibilityVisitor<'_, 'db> { + fn program_environment(&self) -> &ProgramEnvironment<'db> { + self.env + } + + fn should_visit_lazy_type_attributes(&self) -> bool { + false + } + + fn visit_type(&self, db: &'db dyn Db, ty: Type<'db>) { + if !self.eligible.get() || ty.is_type_var() { + return; + } + if ty.is_dynamic() { + self.eligible.set(false); + return; + } + walk_type_with_recursion_guard(db, ty, self, &self.seen); + } + } + + let visitor = EligibilityVisitor { + env, + seen: TypeCollector::default(), + eligible: Cell::new(true), + }; + visitor.visit_type(db, self); + visitor.eligible.get() + } +} + +impl<'db> ConstraintSetStorage<'db> { + /// Returns how much sequent fuel is needed to derive this constraint. + /// + /// This cost is driven by two factors. + /// + /// First, nested types containing typevars can produce increasingly complex families of + /// derived constraints. Charge more fuel for those constraints so that each additional level + /// of typevar depth shortens the remaining derivation chain. + /// + /// Second, even without considering typevars, the lower and upper bounds can become more + /// structurally complex. We consider a type to be more complex if it has deeper nesting of + /// type constructors. Each sequent is charged the _increase_ in that complexity between its + /// antecedents and its consequent. (Measuring growth rather than absolute depth avoids + /// penalizing a complex concrete bound that is merely propagated unchanged.) + pub(super) fn sequent_fuel_cost( + &mut self, + db: &'db dyn Db, + env: &ProgramEnvironment<'db>, + constraint: ConstraintId, + antecedent_constructor_depth: u16, + ) -> u16 { + let (constructor_depth, typevar_depth) = + self.cached_constraint_bound_depth(db, env, constraint); + let constructor_growth = constructor_depth.saturating_sub(antecedent_constructor_depth); + typevar_depth.max(constructor_growth).saturating_add(1) + } +} + +#[cfg(test)] +mod tests { + use super::*; + + use crate::db::tests::{TestDb, setup_db}; + use crate::types::typevar::TypeVarBoundOrConstraints; + use crate::types::{BoundTypeVarInstance, KnownClass, SubclassOfType, TypeVarVariance}; + use ruff_python_ast::name::Name; + + fn create_typevar<'db>(db: &'db TestDb, name: &'static str) -> BoundTypeVarInstance<'db> { + BoundTypeVarInstance::synthetic( + db, + &db.program_environment(), + Name::new_static(name), + TypeVarVariance::Invariant, + ) + } + + fn known_instance(db: &TestDb, class: KnownClass) -> Type<'_> { + class.to_instance(db, &db.program_environment()) + } + + #[test] + fn overlapping_lower_bounds_do_not_skip_nonempty_sequent_map() { + let db = setup_db(); + let db = &db; + let env = db.program_environment(); + let builder = ConstraintSetBuilder::new(); + let t = create_typevar(db, "T"); + let bool = known_instance(db, KnownClass::Bool); + let u = create_typevar(db, "U") + .map_bound_or_constraints(db, |_| Some(TypeVarBoundOrConstraints::UpperBound(bool))); + let type_of_u = SubclassOfType::from(db, &env, u); + let bool_class = KnownClass::Bool.to_class_literal(db, &env); + let mut storage = builder.storage.borrow_mut(); + let left = ConstraintId::new_with_bounds( + db, + &env, + &mut storage, + t, + Some(ConstraintBound::Evidence(type_of_u)), + None, + ); + let right = ConstraintId::new_with_bounds( + db, + &env, + &mut storage, + t, + Some(ConstraintBound::Evidence(bool_class)), + None, + ); + + for (left, right) in [(left, right), (right, left)] { + let sequents = SequentMap::for_constraint_pair(db, &env, &mut storage, left, right); + + assert!( + sequents + .sequents + .iter() + .any(|sequent| matches!(sequent, Sequent::SingleImplication { .. })) + ); + assert!(!SequentMap::pair_cannot_produce_sequents( + db, + &env, + &mut storage, + left, + right + )); + } + } + + #[test] + fn constraint_implications_are_cached() { + let db = setup_db(); + let db = &db; + let env = db.program_environment(); + let t = create_typevar(db, "T"); + let builder = ConstraintSetBuilder::new(); + let mut storage = builder.storage.borrow_mut(); + let t_int = ConstraintId::new( + db, + &env, + &mut storage, + t, + Type::Never, + KnownClass::Int.to_instance(db, &env), + ); + let t_bool = ConstraintId::new( + db, + &env, + &mut storage, + t, + Type::Never, + KnownClass::Bool.to_instance(db, &env), + ); + + assert!(storage.cached_constraint_implies(db, &env, t_bool, t_int)); + assert!(storage.cached_constraint_implies(db, &env, t_bool, t_int)); + drop(storage); + + { + let storage = builder.storage.borrow(); + assert_eq!( + storage.constraint_implication_cache.get(&(t_bool, t_int)), + Some(&true) + ); + assert_eq!(storage.constraint_implication_cache.len(), 1); + } + + let mut storage = builder.storage.borrow_mut(); + assert!(!storage.cached_constraint_implies(db, &env, t_int, t_bool)); + assert!(!storage.cached_constraint_implies(db, &env, t_int, t_bool)); + drop(storage); + + let storage = builder.storage.borrow(); + assert_eq!( + storage.constraint_implication_cache.get(&(t_int, t_bool)), + Some(&false) + ); + assert_eq!(storage.constraint_implication_cache.len(), 2); + } +} diff --git a/crates/ty_python_semantic/src/types/constraints/solutions.rs b/crates/ty_python_semantic/src/types/constraints/solutions.rs index b4f6d269d90d2..851062d6ae4ab 100644 --- a/crates/ty_python_semantic/src/types/constraints/solutions.rs +++ b/crates/ty_python_semantic/src/types/constraints/solutions.rs @@ -1,9 +1,10 @@ use std::marker::PhantomData; use std::ops::ControlFlow; +use crate::types::constraints::paths::PathAssignments; use crate::types::constraints::{ ALWAYS_FALSE, ALWAYS_TRUE, ConstraintBoundsBuilder, ConstraintId, ConstraintSetStorage, NodeId, - PathAssignments, PathBounds, SolutionLimits, + PathBounds, SolutionLimits, }; use crate::types::{BoundTypeVarInstance, Type}; use crate::{Db, FxIndexMap, FxIndexSet, ProgramEnvironment};