add more sequents

crates/ty_python_semantic/src/types.rs

@@ -9134,12 +9134,12 @@ impl<'db> BoundTypeVarInstance<'db> {
     /// of synthetic generic functions.
     pub(crate) fn synthetic(
         db: &'db dyn Db,
-        name: &'static str,
+        name: impl Into<Name>,
         variance: TypeVarVariance,
     ) -> Self {
         let identity = TypeVarIdentity::new(
             db,
-            Name::new_static(name),
+            name.into(),
             None, // definition
             TypeVarKind::Pep695,
         );

crates/ty_python_semantic/src/types/constraints.rs

@@ -66,7 +66,7 @@ use crate::types::generics::{GenericContext, InferableTypeVars, Specialization};
 use crate::types::visitor::{TypeCollector, TypeVisitor, walk_type_with_recursion_guard};
 use crate::types::{
     BoundTypeVarIdentity, BoundTypeVarInstance, IntersectionType, Type, TypeRelation,
-    TypeVarBoundOrConstraints, UnionType, walk_bound_type_var_type,
+    TypeVarBoundOrConstraints, TypeVarVariance, UnionType, walk_bound_type_var_type,
 };
 use crate::{Db, FxOrderSet};
 
@@ -1037,59 +1037,56 @@ impl<'db> Node<'db> {
             Node::Interior(_) => {}
         }
 
-        let mut typevars = FxHashSet::default();
+        let q = self.display(db).to_string();
+        eprintln!("==> sat? {q}");
+        let mut inferable_domain = Node::AlwaysTrue;
+        let mut noninferable_domain = Node::AlwaysTrue;
+        let mut gradual_domain = Node::AlwaysTrue;
+        let mut gradual_bounds_typevars = Vec::default();
+        let mut add_typevar = |bound_typevar: BoundTypeVarInstance<'db>| {
+            let valid = bound_typevar.valid_specializations(db, inferable);
+            eprintln!(
+                " -> typevar {} inferable? {}",
+                bound_typevar.identity(db).display(db),
+                bound_typevar.is_inferable(db, inferable)
+            );
+            eprintln!("    valid {}", valid.valid.display(db));
+            eprintln!("    grad  {}", valid.gradual_bounds.display(db));
+            if bound_typevar.is_inferable(db, inferable) {
+                inferable_domain = inferable_domain.and(db, valid.valid);
+            } else {
+                noninferable_domain = noninferable_domain.and(db, valid.valid);
+            }
+            gradual_domain = gradual_domain.and(db, valid.gradual_bounds);
+            gradual_bounds_typevars.extend_from_slice(&valid.gradual_bounds_typevars);
+        };
         self.for_each_constraint(db, &mut |constraint| {
-            typevars.insert(constraint.typevar(db));
+            add_typevar(constraint.typevar(db));
+            if let Type::TypeVar(bound_typevar) = constraint.lower(db) {
+                add_typevar(bound_typevar);
+            }
+            if let Type::TypeVar(bound_typevar) = constraint.upper(db) {
+                add_typevar(bound_typevar);
+            }
         });
 
-        // Returns if some specialization satisfies this constraint set.
-        let some_specialization_satisfies = move |specializations: Node<'db>| {
-            let when_satisfied = specializations.implies(db, self).and(db, specializations);
-            !when_satisfied.is_never_satisfied(db)
-        };
-
-        // Returns if all specializations satisfy this constraint set.
-        let all_specializations_satisfy = move |specializations: Node<'db>| {
-            let when_satisfied = specializations.implies(db, self).and(db, specializations);
-            when_satisfied
-                .iff(db, specializations)
-                .is_always_satisfied(db)
-        };
-
-        for typevar in typevars {
-            if typevar.is_inferable(db, inferable) {
-                // If the typevar is in inferable position, we need to verify that some valid
-                // specialization satisfies the constraint set.
-                let valid_specializations = typevar.valid_specializations(db);
-                if !some_specialization_satisfies(valid_specializations) {
-                    return false;
-                }
-            } else {
-                // If the typevar is in non-inferable position, we need to verify that all required
-                // specializations satisfy the constraint set. Complicating things, the typevar
-                // might have gradual constraints. For those, we need to know the range of valid
-                // materializations, but we only need some materialization to satisfy the
-                // constraint set.
-                //
-                // NB: We could also model this by introducing a synthetic typevar for the gradual
-                // constraint, treating that synthetic typevar as always inferable (so that we only
-                // need to verify for some materialization), and then update this typevar's
-                // constraint to refer to the synthetic typevar instead of the original gradual
-                // constraint.
-                let (static_specializations, gradual_constraints) =
-                    typevar.required_specializations(db);
-                if !all_specializations_satisfy(static_specializations) {
-                    return false;
-                }
-                for gradual_constraint in gradual_constraints {
-                    if !some_specialization_satisfies(gradual_constraint) {
-                        return false;
-                    }
-                }
-            }
-        }
-
-        true
+        eprintln!(" -> dom_inf  {}", inferable_domain.display(db));
+        eprintln!("    dom_non  {}", noninferable_domain.display(db));
+        eprintln!("    dom_grad {}", gradual_domain.display(db));
+        let restricted = self.and(db, inferable_domain);
+        eprintln!(" -> G    {}", restricted.display(db));
+        let inferable_abstracted = restricted.exists(db, inferable.iter());
+        eprintln!(" -> E    {}", inferable_abstracted.display(db));
+        let implies = noninferable_domain.implies(db, inferable_abstracted);
+        eprintln!(" -> imp  {}", implies.display(db));
+        let gradual_abstracted = implies.exists(
+            db,
+            gradual_bounds_typevars
+                .iter()
+                .map(|bound_typevar| bound_typevar.identity(db)),
+        );
+        eprintln!(" -> imp' {}", gradual_abstracted.display(db));
+        gradual_abstracted.is_always_satisfied(db)
     }
 
     /// Returns a new BDD that is the _existential abstraction_ of `self` for a set of typevars.
@@ -2532,6 +2529,22 @@ impl<'db> SequentMap<'db> {
                 (bound_constraint.lower(db), constrained_upper)
             }
 
+            // (CL ≤ C ≤ pivot) ∧ (pivot ≤ B ≤ BU) → (CL ≤ C ≤ B)
+            (constrained_lower, constrained_upper)
+                if !matches!(constrained_upper, Type::TypeVar(_))
+                    && constrained_upper == bound_constraint.lower(db) =>
+            {
+                (constrained_lower, Type::TypeVar(bound_typevar))
+            }
+
+            // (pivot ≤ C ≤ CU) ∧ (BL ≤ B ≤ pivot) → (B ≤ C ≤ CU)
+            (constrained_lower, constrained_upper)
+                if !matches!(constrained_lower, Type::TypeVar(_))
+                    && constrained_lower == bound_constraint.upper(db) =>
+            {
+                (Type::TypeVar(bound_typevar), constrained_upper)
+            }
+
             _ => return,
         };
 
@@ -3026,11 +3039,138 @@ impl<'db> SatisfiedClauses<'db> {
     }
 }
 
+struct ValidSpecializations<'db> {
+    valid: Node<'db>,
+    gradual_bounds: Node<'db>,
+    // XXX: Identity?
+    gradual_bounds_typevars: Vec<BoundTypeVarInstance<'db>>,
+}
+
+impl<'db> ValidSpecializations<'db> {
+    fn for_unbounded(db: &'db dyn Db, bound_typevar: BoundTypeVarInstance<'db>) -> Self {
+        let valid = ConstrainedTypeVar::new_node(db, bound_typevar, Type::Never, Type::object());
+        Self {
+            valid,
+            gradual_bounds: Node::AlwaysTrue,
+            gradual_bounds_typevars: Vec::default(),
+        }
+    }
+
+    fn for_bounded(
+        db: &'db dyn Db,
+        bound_typevar: BoundTypeVarInstance<'db>,
+        bound: Type<'db>,
+    ) -> Self {
+        let bound_lower = bound.bottom_materialization(db);
+        let bound_upper = bound.top_materialization(db);
+        if bound_lower == bound_upper {
+            Self::for_fully_static_bounded(db, bound_typevar, bound_lower)
+        } else {
+            Self::for_gradual_bounded(db, bound_typevar, bound_lower, bound_upper)
+        }
+    }
+
+    fn for_fully_static_bounded(
+        db: &'db dyn Db,
+        bound_typevar: BoundTypeVarInstance<'db>,
+        bound: Type<'db>,
+    ) -> Self {
+        let valid = ConstrainedTypeVar::new_node(db, bound_typevar, Type::Never, bound);
+        Self {
+            valid,
+            gradual_bounds: Node::AlwaysTrue,
+            gradual_bounds_typevars: Vec::default(),
+        }
+    }
+
+    fn for_gradual_bounded(
+        db: &'db dyn Db,
+        bound_typevar: BoundTypeVarInstance<'db>,
+        bound_lower: Type<'db>,
+        bound_upper: Type<'db>,
+    ) -> Self {
+        let gradual_bound_typevar = BoundTypeVarInstance::synthetic(
+            db,
+            format!("{}'bound", bound_typevar.identity(db).display(db)),
+            TypeVarVariance::Invariant,
+        );
+        let gradual_bound_constraints =
+            ConstrainedTypeVar::new_node(db, gradual_bound_typevar, bound_lower, bound_upper);
+        let gradual_bound = ConstrainedTypeVar::new_node(
+            db,
+            bound_typevar,
+            Type::Never,
+            Type::TypeVar(gradual_bound_typevar),
+        );
+        Self {
+            valid: gradual_bound,
+            gradual_bounds: gradual_bound_constraints,
+            gradual_bounds_typevars: vec![gradual_bound_typevar],
+        }
+    }
+
+    fn for_constrained(
+        db: &'db dyn Db,
+        bound_typevar: BoundTypeVarInstance<'db>,
+        constraints: UnionType<'db>,
+    ) -> Self {
+        let mut valid = Node::AlwaysFalse;
+        let mut gradual_bounds = Node::AlwaysTrue;
+        let mut gradual_bounds_typevars = Vec::default();
+
+        for (idx, constraint) in constraints.elements(db).iter().enumerate() {
+            let constraint_lower = constraint.bottom_materialization(db);
+            let constraint_upper = constraint.top_materialization(db);
+            if constraint_lower == constraint_upper {
+                let constraint = ConstrainedTypeVar::new_node(
+                    db,
+                    bound_typevar,
+                    constraint_lower,
+                    constraint_upper,
+                );
+                valid = valid.or(db, constraint);
+            } else {
+                let gradual_constraint_typevar = BoundTypeVarInstance::synthetic(
+                    db,
+                    format!("{}'constraint{idx}", bound_typevar.identity(db).display(db)),
+                    TypeVarVariance::Covariant,
+                );
+                let gradual_constraint_constraints = ConstrainedTypeVar::new_node(
+                    db,
+                    gradual_constraint_typevar,
+                    constraint_lower,
+                    constraint_upper,
+                );
+                let gradual_constraint = ConstrainedTypeVar::new_node(
+                    db,
+                    bound_typevar,
+                    Type::Never,
+                    Type::TypeVar(gradual_constraint_typevar),
+                );
+                valid = valid.or(db, gradual_constraint);
+                gradual_bounds = gradual_bounds.and(db, gradual_constraint_constraints);
+                gradual_bounds_typevars.push(gradual_constraint_typevar);
+            }
+        }
+
+        Self {
+            valid,
+            gradual_bounds,
+            gradual_bounds_typevars,
+        }
+    }
+}
+
 impl<'db> BoundTypeVarInstance<'db> {
     /// Returns the valid specializations of a typevar. This is used when checking a constraint set
     /// when this typevar is in inferable position, where we only need _some_ specialization to
     /// satisfy the constraint set.
-    fn valid_specializations(self, db: &'db dyn Db) -> Node<'db> {
+    fn valid_specializations(
+        self,
+        db: &'db dyn Db,
+        // XXX
+        _inferable: InferableTypeVars<'_, 'db>,
+    ) -> ValidSpecializations<'db> {
         // For gradual upper bounds and constraints, we are free to choose any materialization that
         // makes the check succeed. In inferable positions, it is most helpful to choose a
         // materialization that is as permissive as possible, since that maximizes the number of
@@ -3042,72 +3182,14 @@ impl<'db> BoundTypeVarInstance<'db> {
         // that _some_ valid specialization satisfies the constraint set, it's correct for us to
         // return the range of valid materializations that we can choose from.
         match self.typevar(db).bound_or_constraints(db) {
-            None => Node::AlwaysTrue,
-            Some(TypeVarBoundOrConstraints::UpperBound(bound)) => {
-                let bound = bound.top_materialization(db);
-                ConstrainedTypeVar::new_node(db, self, Type::Never, bound)
-            }
-            Some(TypeVarBoundOrConstraints::Constraints(constraints)) => {
-                let mut specializations = Node::AlwaysFalse;
-                for constraint in constraints.elements(db) {
-                    let constraint_lower = constraint.bottom_materialization(db);
-                    let constraint_upper = constraint.top_materialization(db);
-                    specializations = specializations.or(
-                        db,
-                        ConstrainedTypeVar::new_node(db, self, constraint_lower, constraint_upper),
-                    );
-                }
-                specializations
-            }
-        }
-    }
+            None => ValidSpecializations::for_unbounded(db, self),
 
-    /// Returns the required specializations of a typevar. This is used when checking a constraint
-    /// set when this typevar is in non-inferable position, where we need _all_ specializations to
-    /// satisfy the constraint set.
-    ///
-    /// That causes complications if this is a constrained typevar, where one of the constraints is
-    /// gradual. In that case, we need to return the range of valid materializations, but we don't
-    /// want to require that all of those materializations satisfy the constraint set.
-    ///
-    /// To handle this, we return a "primary" result, and an iterator of any gradual constraints.
-    /// For an unbounded/unconstrained typevar or a bounded typevar, the primary result fully
-    /// specifies the required specializations, and the iterator will be empty. For a constrained
-    /// typevar, the primary result will include the fully static constraints, and the iterator
-    /// will include an entry for each non-fully-static constraint.
-    fn required_specializations(
-        self,
-        db: &'db dyn Db,
-    ) -> (Node<'db>, impl IntoIterator<Item = Node<'db>>) {
-        // For upper bounds and constraints, we are free to choose any materialization that makes
-        // the check succeed. In non-inferable positions, it is most helpful to choose a
-        // materialization that is as restrictive as possible, since that minimizes the number of
-        // valid specializations that must satisfy the check. We therefore take the bottom
-        // materialization of the bound or constraints.
-        match self.typevar(db).bound_or_constraints(db) {
-            None => (Node::AlwaysTrue, Vec::new()),
             Some(TypeVarBoundOrConstraints::UpperBound(bound)) => {
-                let bound = bound.bottom_materialization(db);
-                (
-                    ConstrainedTypeVar::new_node(db, self, Type::Never, bound),
-                    Vec::new(),
-                )
+                ValidSpecializations::for_bounded(db, self, bound)
             }
+
             Some(TypeVarBoundOrConstraints::Constraints(constraints)) => {
-                let mut non_gradual_constraints = Node::AlwaysFalse;
-                let mut gradual_constraints = Vec::new();
-                for constraint in constraints.elements(db) {
-                    let constraint_lower = constraint.bottom_materialization(db);
-                    let constraint_upper = constraint.top_materialization(db);
-                    let constraint =
-                        ConstrainedTypeVar::new_node(db, self, constraint_lower, constraint_upper);
-                    if constraint_lower == constraint_upper {
-                        non_gradual_constraints = non_gradual_constraints.or(db, constraint);
-                    } else {
-                        gradual_constraints.push(constraint);
-                    }
-                }
-                (non_gradual_constraints, gradual_constraints)
+                ValidSpecializations::for_constrained(db, self, constraints)
             }
         }
     }
@@ -3131,7 +3213,9 @@ impl<'db> GenericContext<'db> {
         let abstracted = self
             .variables(db)
             .fold(constraints.node, |constraints, bound_typevar| {
-                constraints.and(db, bound_typevar.valid_specializations(db))
+                let valid_specializations =
+                    bound_typevar.valid_specializations(db, InferableTypeVars::None);
+                constraints.and(db, valid_specializations.valid)
             });
 
         // Then we find all of the "representative types" for each typevar in the constraint set.