From 848cbb1ddaf93e78ae5df0e8f01130e1b024d6d1 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Thu, 5 Mar 2026 15:17:12 -0500
Subject: [PATCH 01/20] put constraint builder in spec builder too

---
 crates/ty_python_semantic/src/types.rs        |   4 +-
 .../ty_python_semantic/src/types/call/bind.rs |  63 ++++----
 .../ty_python_semantic/src/types/generics.rs  | 135 ++++++------------
 .../src/types/infer/builder.rs                |  24 ++--
 4 files changed, 83 insertions(+), 143 deletions(-)

diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs
index e4846954c09b6..2b8580173ad0e 100644
--- a/crates/ty_python_semantic/src/types.rs
+++ b/crates/ty_python_semantic/src/types.rs
@@ -1885,11 +1885,11 @@ impl<'db> Type<'db> {
         // Collect the type mappings used to narrow the type context.
         let tcx_mappings = {
             let mut builder =
-                SpecializationBuilder::new(db, generic_context.inferable_typevars(db));
+                SpecializationBuilder::new(db, constraints, generic_context.inferable_typevars(db));
 
             if let Some(tcx) = tcx.annotation {
                 let alias_instance = Type::instance(db, class_literal.identity_specialization(db));
-                let _ = builder.infer_reverse(constraints, tcx, alias_instance);
+                let _ = builder.infer_reverse(tcx, alias_instance);
             }
 
             builder.into_type_mappings()
diff --git a/crates/ty_python_semantic/src/types/call/bind.rs b/crates/ty_python_semantic/src/types/call/bind.rs
index f6afce5a5dbcf..b00bc5467bb91 100644
--- a/crates/ty_python_semantic/src/types/call/bind.rs
+++ b/crates/ty_python_semantic/src/types/call/bind.rs
@@ -3723,7 +3723,7 @@ impl<'a, 'db> ArgumentTypeChecker<'a, 'db> {
             .zip(self.call_expression_tcx.annotation);
 
         self.inferable_typevars = generic_context.inferable_typevars(self.db);
-        let mut builder = SpecializationBuilder::new(self.db, self.inferable_typevars);
+        let mut builder = SpecializationBuilder::new(self.db, constraints, self.inferable_typevars);
 
         // Type variables for which we inferred a declared type based on a partially specialized
         // type from an outer generic context. For these type variables, we may infer types that
@@ -3740,37 +3740,32 @@ impl<'a, 'db> ArgumentTypeChecker<'a, 'db> {
                     .class_specialization(self.db)?;
 
                 builder
-                    .infer_reverse_map(
-                        constraints,
-                        tcx,
-                        return_ty,
-                        |(identity, variance, inferred_ty)| {
-                            // Avoid unnecessarily widening the return type based on a covariant
-                            // type parameter from the type context, as it can lead to argument
-                            // assignability errors if the type variable is constrained by a narrower
-                            // parameter type.
-                            if variance.is_covariant() {
-                                return None;
-                            }
+                    .infer_reverse_map(tcx, return_ty, |(identity, variance, inferred_ty)| {
+                        // Avoid unnecessarily widening the return type based on a covariant
+                        // type parameter from the type context, as it can lead to argument
+                        // assignability errors if the type variable is constrained by a narrower
+                        // parameter type.
+                        if variance.is_covariant() {
+                            return None;
+                        }
 
-                            // Avoid inferring a preferred type based on partially specialized type context
-                            // from an outer generic call. If the type context is a union, we try to keep
-                            // any concrete elements.
-                            let inferred_ty = inferred_ty.filter_union(self.db, |ty| {
-                                if ty.has_unspecialized_type_var(self.db) {
-                                    partially_specialized_declared_type.insert(identity);
-                                    false
-                                } else {
-                                    true
-                                }
-                            });
-                            if inferred_ty.has_unspecialized_type_var(self.db) {
-                                return None;
+                        // Avoid inferring a preferred type based on partially specialized type context
+                        // from an outer generic call. If the type context is a union, we try to keep
+                        // any concrete elements.
+                        let inferred_ty = inferred_ty.filter_union(self.db, |ty| {
+                            if ty.has_unspecialized_type_var(self.db) {
+                                partially_specialized_declared_type.insert(identity);
+                                false
+                            } else {
+                                true
                             }
+                        });
+                        if inferred_ty.has_unspecialized_type_var(self.db) {
+                            return None;
+                        }
 
-                            Some(inferred_ty)
-                        },
-                    )
+                        Some(inferred_ty)
+                    })
                     .ok()?;
 
                 Some(builder.type_mappings().clone())
@@ -3779,7 +3774,6 @@ impl<'a, 'db> ArgumentTypeChecker<'a, 'db> {
 
         let mut specialization_errors = Vec::new();
         let assignable_to_declared_type = self.infer_argument_types(
-            constraints,
             &mut builder,
             &preferred_type_mappings,
             &partially_specialized_declared_type,
@@ -3792,11 +3786,10 @@ impl<'a, 'db> ArgumentTypeChecker<'a, 'db> {
         // Note that this will still lead to an invalid specialization, but may
         // produce more precise diagnostics.
         if !assignable_to_declared_type {
-            builder = SpecializationBuilder::new(self.db, self.inferable_typevars);
+            builder = SpecializationBuilder::new(self.db, constraints, self.inferable_typevars);
             specialization_errors.clear();
 
             self.infer_argument_types(
-                constraints,
                 &mut builder,
                 &FxHashMap::default(),
                 &FxHashSet::default(),
@@ -3861,10 +3854,9 @@ impl<'a, 'db> ArgumentTypeChecker<'a, 'db> {
         self.specialization = Some(specialization);
     }
 
-    fn infer_argument_types(
+    fn infer_argument_types<'c>(
         &mut self,
-        constraints: &ConstraintSetBuilder<'db>,
-        builder: &mut SpecializationBuilder<'db>,
+        builder: &mut SpecializationBuilder<'db, 'c>,
         preferred_type_mappings: &FxHashMap<BoundTypeVarIdentity<'db>, Type<'db>>,
         partially_specialized_declared_type: &FxHashSet<BoundTypeVarIdentity<'_>>,
         specialization_errors: &mut Vec<BindingError<'db>>,
@@ -3879,7 +3871,6 @@ impl<'a, 'db> ArgumentTypeChecker<'a, 'db> {
                 self.argument_matches[argument_index].iter()
             {
                 let specialization_result = builder.infer_map(
-                    constraints,
                     parameters[parameter_index].annotated_type(),
                     variadic_argument_type.unwrap_or(argument_type),
                     |(identity, _, inferred_ty)| {
diff --git a/crates/ty_python_semantic/src/types/generics.rs b/crates/ty_python_semantic/src/types/generics.rs
index cf8cf1ddb9bd2..73cc955f3e911 100644
--- a/crates/ty_python_semantic/src/types/generics.rs
+++ b/crates/ty_python_semantic/src/types/generics.rs
@@ -1639,8 +1639,9 @@ impl<'db> ApplySpecialization<'_, 'db> {
 
 /// Performs type inference between parameter annotations and argument types, producing a
 /// specialization of a generic function.
-pub(crate) struct SpecializationBuilder<'db> {
+pub(crate) struct SpecializationBuilder<'db, 'c> {
     db: &'db dyn Db,
+    constraints: &'c ConstraintSetBuilder<'db>,
     inferable: InferableTypeVars<'db, 'db>,
     types: FxHashMap<BoundTypeVarIdentity<'db>, Type<'db>>,
 }
@@ -1649,10 +1650,15 @@ pub(crate) struct SpecializationBuilder<'db> {
 /// type with respect to the type variable.
 pub(crate) type TypeVarAssignment<'db> = (BoundTypeVarIdentity<'db>, TypeVarVariance, Type<'db>);
 
-impl<'db> SpecializationBuilder<'db> {
-    pub(crate) fn new(db: &'db dyn Db, inferable: InferableTypeVars<'db, 'db>) -> Self {
+impl<'db, 'c> SpecializationBuilder<'db, 'c> {
+    pub(crate) fn new(
+        db: &'db dyn Db,
+        constraints: &'c ConstraintSetBuilder<'db>,
+        inferable: InferableTypeVars<'db, 'db>,
+    ) -> Self {
         Self {
             db,
+            constraints,
             inferable,
             types: FxHashMap::default(),
         }
@@ -1683,6 +1689,7 @@ impl<'db> SpecializationBuilder<'db> {
 
         Self {
             db: self.db,
+            constraints: self.constraints,
             inferable: self.inferable,
             types,
         }
@@ -1702,6 +1709,7 @@ impl<'db> SpecializationBuilder<'db> {
 
         Self {
             db: self.db,
+            constraints: self.constraints,
             inferable: self.inferable,
             types,
         }
@@ -1768,14 +1776,13 @@ impl<'db> SpecializationBuilder<'db> {
     /// specialization directly from that constraint set. This method lets us migrate to that brave
     /// new world incrementally, by using the new constraint set mechanism piecemeal for certain
     /// type comparisons.
-    fn add_type_mappings_from_constraint_set<'c>(
+    fn add_type_mappings_from_constraint_set(
         &mut self,
         formal: Type<'db>,
         set: ConstraintSet<'db, 'c>,
-        constraints: &'c ConstraintSetBuilder<'db>,
         mut f: impl FnMut(TypeVarAssignment<'db>) -> Option<Type<'db>>,
     ) -> Result<(), ()> {
-        let solutions = match set.solutions(self.db, constraints) {
+        let solutions = match set.solutions(self.db, self.constraints) {
             Solutions::Unsatisfiable => return Err(()),
             Solutions::Unconstrained => return Ok(()),
             Solutions::Constrained(solutions) => solutions,
@@ -1800,17 +1807,16 @@ impl<'db> SpecializationBuilder<'db> {
         let formal_is_single_paramspec = formal_signature.is_single_paramspec().is_some();
 
         for actual_callable in actual_callables.as_slice() {
-            let constraints = ConstraintSetBuilder::new();
             if formal_is_single_paramspec {
                 let when = actual_callable
                     .signatures(self.db)
                     .when_constraint_set_assignable_to(
                         self.db,
                         formal_signature,
-                        &constraints,
+                        self.constraints,
                         self.inferable,
                     );
-                self.add_type_mappings_from_constraint_set(formal, when, &constraints, &mut *f)?;
+                self.add_type_mappings_from_constraint_set(formal, when, &mut *f)?;
             } else {
                 // An overloaded actual callable is compatible with the formal signature if at
                 // least one of its overloads is. We collect type mappings from all satisfiable
@@ -1820,11 +1826,11 @@ impl<'db> SpecializationBuilder<'db> {
                     let when = actual_signature.when_constraint_set_assignable_to_signatures(
                         self.db,
                         formal_signature,
-                        &constraints,
+                        self.constraints,
                         self.inferable,
                     );
                     if self
-                        .add_type_mappings_from_constraint_set(formal, when, &constraints, &mut *f)
+                        .add_type_mappings_from_constraint_set(formal, when, &mut *f)
                         .is_ok()
                     {
                         any_satisfiable = true;
@@ -1841,11 +1847,10 @@ impl<'db> SpecializationBuilder<'db> {
     /// Infer type mappings for the specialization based on a given type and its declared type.
     pub(crate) fn infer(
         &mut self,
-        constraints: &ConstraintSetBuilder<'db>,
         formal: Type<'db>,
         actual: Type<'db>,
     ) -> Result<(), SpecializationError<'db>> {
-        self.infer_map(constraints, formal, actual, |(_, _, ty)| Some(ty))
+        self.infer_map(formal, actual, |(_, _, ty)| Some(ty))
     }
 
     /// Infer type mappings for the specialization based on a given type and its declared type.
@@ -1854,13 +1859,11 @@ impl<'db> SpecializationBuilder<'db> {
     /// optionally modify the inferred type, or filter out the type mapping entirely.
     pub(crate) fn infer_map(
         &mut self,
-        constraints: &ConstraintSetBuilder<'db>,
         formal: Type<'db>,
         actual: Type<'db>,
         mut f: impl FnMut(TypeVarAssignment<'db>) -> Option<Type<'db>>,
     ) -> Result<(), SpecializationError<'db>> {
         self.infer_map_impl(
-            constraints,
             formal,
             actual,
             TypeVarVariance::Covariant,
@@ -1871,7 +1874,6 @@ impl<'db> SpecializationBuilder<'db> {
 
     fn infer_map_impl(
         &mut self,
-        constraints: &ConstraintSetBuilder<'db>,
         formal: Type<'db>,
         actual: Type<'db>,
         polarity: TypeVarVariance,
@@ -1908,14 +1910,7 @@ impl<'db> SpecializationBuilder<'db> {
             // Expand PEP 695 type aliases in the formal type.
             // This is necessary for solving generics like `def head[T](my_list: MyList[T]) -> T`.
             (Type::TypeAlias(alias), _) => {
-                return self.infer_map_impl(
-                    constraints,
-                    alias.value_type(self.db),
-                    actual,
-                    polarity,
-                    f,
-                    seen,
-                );
+                return self.infer_map_impl(alias.value_type(self.db), actual, polarity, f, seen);
             }
 
             // TODO: We haven't implemented a full unification solver yet. If typevars appear in
@@ -1981,7 +1976,7 @@ impl<'db> SpecializationBuilder<'db> {
                 if !actual.is_never() {
                     let assignable_elements = union_formal.elements(self.db).iter().filter(|ty| {
                         actual
-                            .when_subtype_of(self.db, **ty, constraints, self.inferable)
+                            .when_subtype_of(self.db, **ty, self.constraints, self.inferable)
                             .is_always_satisfied(self.db)
                     });
                     if assignable_elements.exactly_one().is_ok() {
@@ -2011,14 +2006,8 @@ impl<'db> SpecializationBuilder<'db> {
                 let mut first_error = None;
                 let mut found_matching_element = false;
                 for formal_element in union_formal.elements(self.db) {
-                    let result = self.infer_map_impl(
-                        constraints,
-                        *formal_element,
-                        actual,
-                        polarity,
-                        &mut f,
-                        seen,
-                    );
+                    let result =
+                        self.infer_map_impl(*formal_element, actual, polarity, &mut f, seen);
                     if let Err(err) = result {
                         first_error.get_or_insert(err);
                     } else {
@@ -2028,7 +2017,7 @@ impl<'db> SpecializationBuilder<'db> {
                             .when_assignable_to(
                                 self.db,
                                 *formal_element,
-                                constraints,
+                                self.constraints,
                                 self.inferable,
                             )
                             .is_never_satisfied(self.db)
@@ -2064,7 +2053,7 @@ impl<'db> SpecializationBuilder<'db> {
                             return Ok(());
                         }
                         if !ty
-                            .when_assignable_to(self.db, bound, constraints, self.inferable)
+                            .when_assignable_to(self.db, bound, self.constraints, self.inferable)
                             .is_always_satisfied(self.db)
                         {
                             return Err(SpecializationError::MismatchedBound {
@@ -2117,13 +2106,18 @@ impl<'db> SpecializationBuilder<'db> {
                         for constraint in typevar_constraints.elements(self.db) {
                             let is_satisfied = if polarity.is_contravariant() {
                                 constraint
-                                    .when_assignable_to(self.db, ty, constraints, self.inferable)
+                                    .when_assignable_to(
+                                        self.db,
+                                        ty,
+                                        self.constraints,
+                                        self.inferable,
+                                    )
                                     .is_always_satisfied(self.db)
                             } else {
                                 ty.when_assignable_to(
                                     self.db,
                                     *constraint,
-                                    constraints,
+                                    self.constraints,
                                     self.inferable,
                                 )
                                 .is_always_satisfied(self.db)
@@ -2149,7 +2143,7 @@ impl<'db> SpecializationBuilder<'db> {
                 // actual type must also be disjoint from every negative element of the
                 // intersection, but that doesn't help us infer any type mappings.)
                 for positive in formal_intersection.iter_positive(self.db) {
-                    self.infer_map_impl(constraints, positive, actual, polarity, f, seen)?;
+                    self.infer_map_impl(positive, actual, polarity, f, seen)?;
                 }
             }
             (_, Type::Intersection(actual_intersection)) => {
@@ -2171,8 +2165,7 @@ impl<'db> SpecializationBuilder<'db> {
                 let mut first_error = None;
                 let mut found_matching_element = false;
                 for positive in actual_intersection.iter_positive(self.db) {
-                    let result =
-                        self.infer_map_impl(constraints, formal, positive, polarity, f, seen);
+                    let result = self.infer_map_impl(formal, positive, polarity, f, seen);
                     if let Err(err) = result {
                         // TODO: `infer_map_impl` can have side effects even in the error case, so
                         // to be fully correct here we'd need to snapshot `self.types` before each
@@ -2183,7 +2176,7 @@ impl<'db> SpecializationBuilder<'db> {
                         // The recursive call to `infer_map_impl` may succeed even if the actual
                         // type is not assignable to the formal element.
                         if !positive
-                            .when_assignable_to(self.db, formal, constraints, self.inferable)
+                            .when_assignable_to(self.db, formal, self.constraints, self.inferable)
                             .is_never_satisfied(self.db)
                         {
                             found_matching_element = true;
@@ -2201,7 +2194,6 @@ impl<'db> SpecializationBuilder<'db> {
                 let formal_instance = Type::TypeVar(subclass_of.into_type_var().unwrap());
                 if let Some(actual_instance) = ty.to_instance(self.db) {
                     return self.infer_map_impl(
-                        constraints,
                         formal_instance,
                         actual_instance,
                         polarity,
@@ -2218,14 +2210,7 @@ impl<'db> SpecializationBuilder<'db> {
                 // Retry specialization with the literal's fallback instance so literals can
                 // contribute to generic inference for nominal and protocol formals.
                 let actual_instance = literal.fallback_instance(self.db);
-                return self.infer_map_impl(
-                    constraints,
-                    formal,
-                    actual_instance,
-                    polarity,
-                    f,
-                    seen,
-                );
+                return self.infer_map_impl(formal, actual_instance, polarity, f, seen);
             }
 
             (formal, Type::ProtocolInstance(actual_protocol)) => {
@@ -2236,7 +2221,6 @@ impl<'db> SpecializationBuilder<'db> {
                 // infer the specialization of the protocol that the class implements.
                 if let Some(actual_nominal) = actual_protocol.to_nominal_instance() {
                     return self.infer_map_impl(
-                        constraints,
                         formal,
                         Type::NominalInstance(actual_nominal),
                         polarity,
@@ -2270,7 +2254,6 @@ impl<'db> SpecializationBuilder<'db> {
                     {
                         let variance = TypeVarVariance::Covariant.compose(polarity);
                         self.infer_map_impl(
-                            constraints,
                             *formal_element,
                             *actual_element,
                             variance,
@@ -2295,7 +2278,7 @@ impl<'db> SpecializationBuilder<'db> {
                         let when = actual.when_constraint_set_assignable_to(
                             self.db,
                             formal,
-                            constraints,
+                            self.constraints,
                             self.inferable,
                         );
                         // For protocol inference via constraint sets, we currently treat
@@ -2304,12 +2287,7 @@ impl<'db> SpecializationBuilder<'db> {
                         // unsatisfied comparisons simply produced no type mappings), and avoids
                         // false positives for callable-wrapper patterns while this path is still
                         // a hybrid of old and new solver logic.
-                        let _ = self.add_type_mappings_from_constraint_set(
-                            formal,
-                            when,
-                            constraints,
-                            &mut f,
-                        );
+                        let _ = self.add_type_mappings_from_constraint_set(formal, when, &mut f);
                         return Ok(());
                     }
 
@@ -2338,14 +2316,7 @@ impl<'db> SpecializationBuilder<'db> {
                             base_specialization
                         ) {
                             let variance = typevar.variance_with_polarity(self.db, polarity);
-                            self.infer_map_impl(
-                                constraints,
-                                *formal_ty,
-                                *base_ty,
-                                variance,
-                                &mut f,
-                                seen,
-                            )?;
+                            self.infer_map_impl(*formal_ty, *base_ty, variance, &mut f, seen)?;
                         }
                         return Ok(());
                     }
@@ -2404,14 +2375,7 @@ impl<'db> SpecializationBuilder<'db> {
             // when it can be matched directly against a type variable in the formal type,
             // e.g., `reveal_type(alias)` should reveal the type alias, not its value type.
             (formal, Type::TypeAlias(alias)) => {
-                return self.infer_map_impl(
-                    constraints,
-                    formal,
-                    alias.value_type(self.db),
-                    polarity,
-                    f,
-                    seen,
-                );
+                return self.infer_map_impl(formal, alias.value_type(self.db), polarity, f, seen);
             }
 
             // TODO: Add more forms that we can structurally induct into: type[C], callables
@@ -2425,11 +2389,10 @@ impl<'db> SpecializationBuilder<'db> {
     /// actual type, not the formal type, contains inferable type variables.
     pub(crate) fn infer_reverse(
         &mut self,
-        constraints: &ConstraintSetBuilder<'db>,
         formal: Type<'db>,
         actual: Type<'db>,
     ) -> Result<(), SpecializationError<'db>> {
-        self.infer_reverse_map(constraints, formal, actual, |(_, _, ty)| Some(ty))
+        self.infer_reverse_map(formal, actual, |(_, _, ty)| Some(ty))
     }
 
     /// Infer type mappings for the specialization in the reverse direction, i.e., where the
@@ -2439,13 +2402,11 @@ impl<'db> SpecializationBuilder<'db> {
     /// optionally modify the inferred type, or filter out the type mapping entirely.
     pub(crate) fn infer_reverse_map(
         &mut self,
-        constraints: &ConstraintSetBuilder<'db>,
         formal: Type<'db>,
         actual: Type<'db>,
         mut f: impl FnMut(TypeVarAssignment<'db>) -> Option<Type<'db>>,
     ) -> Result<(), SpecializationError<'db>> {
         self.infer_reverse_map_impl(
-            constraints,
             formal,
             actual,
             TypeVarVariance::Covariant,
@@ -2456,7 +2417,6 @@ impl<'db> SpecializationBuilder<'db> {
 
     fn infer_reverse_map_impl(
         &mut self,
-        constraints: &ConstraintSetBuilder<'db>,
         formal: Type<'db>,
         actual: Type<'db>,
         polarity: TypeVarVariance,
@@ -2489,8 +2449,8 @@ impl<'db> SpecializationBuilder<'db> {
 
         // Collect the actual type to which each synthetic type variable is mapped.
         let forward_type_mappings = {
-            let mut builder = SpecializationBuilder::new(self.db, inferable);
-            builder.infer(constraints, synthetic_formal, actual)?;
+            let mut builder = SpecializationBuilder::new(self.db, self.constraints, inferable);
+            builder.infer(synthetic_formal, actual)?;
             builder.into_type_mappings()
         };
 
@@ -2498,7 +2458,7 @@ impl<'db> SpecializationBuilder<'db> {
         //
         // This is the base case for when `actual` is an inferable type variable.
         if forward_type_mappings.is_empty() {
-            return self.infer_map_impl(constraints, actual, formal, polarity, f, seen);
+            return self.infer_map_impl(actual, formal, polarity, f, seen);
         }
 
         // Consider the reverse inference of `Sequence[int]` given `list[T]`.
@@ -2513,14 +2473,7 @@ impl<'db> SpecializationBuilder<'db> {
 
                 // Note that it is possible that we need to recurse deeper, so we continue
                 // to perform a reverse inference on the nested types.
-                self.infer_reverse_map_impl(
-                    constraints,
-                    formal_type,
-                    *actual_type,
-                    variance,
-                    f,
-                    seen,
-                )?;
+                self.infer_reverse_map_impl(formal_type, *actual_type, variance, f, seen)?;
             }
         }
 
diff --git a/crates/ty_python_semantic/src/types/infer/builder.rs b/crates/ty_python_semantic/src/types/infer/builder.rs
index 7bdc1adf47e6d..05c585eb20dce 100644
--- a/crates/ty_python_semantic/src/types/infer/builder.rs
+++ b/crates/ty_python_semantic/src/types/infer/builder.rs
@@ -5172,12 +5172,14 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
                 // If this is a generic call, attempt to specialize the parameter type using the
                 // declared type context, if provided.
                 if let Some(generic_context) = overload.signature.generic_context {
-                    let mut builder =
-                        SpecializationBuilder::new(db, generic_context.inferable_typevars(db));
+                    let mut builder = SpecializationBuilder::new(
+                        db,
+                        &constraints,
+                        generic_context.inferable_typevars(db),
+                    );
 
                     if let Some(declared_return_ty) = call_expression_tcx.annotation {
                         let _ = builder.infer_reverse(
-                            &constraints,
                             declared_return_ty,
                             overload
                                 .constructor_instance_type
@@ -6035,7 +6037,7 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
 
         // Collect type constraints from the declared element types.
         let (elt_tcx_constraints, elt_tcx_variance) = {
-            let mut builder = SpecializationBuilder::new(self.db(), inferable);
+            let mut builder = SpecializationBuilder::new(self.db(), &constraints, inferable);
 
             // For a given type variable, we keep track of the variance of any assignments to
             // that type variable in the type context.
@@ -6050,7 +6052,6 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
 
                 builder
                     .infer_reverse_map(
-                        &constraints,
                         tcx,
                         collection_instance,
                         |(typevar, variance, inferred_ty)| {
@@ -6079,7 +6080,7 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
         };
 
         // Create a set of constraints to infer a precise type for `T`.
-        let mut builder = SpecializationBuilder::new(self.db(), inferable);
+        let mut builder = SpecializationBuilder::new(self.db(), &constraints, inferable);
 
         for elt_ty in elt_tys.clone() {
             let elt_ty_identity = elt_ty.identity(self.db());
@@ -6108,9 +6109,7 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
             // our inference is compatible with subsequent additions to the collection), but it
             // matches the behavior of other type checkers and is usually the desired behavior.
             if let Some(elt_tcx) = elt_tcx {
-                builder
-                    .infer(&constraints, Type::TypeVar(elt_ty), elt_tcx)
-                    .ok()?;
+                builder.infer(Type::TypeVar(elt_ty), elt_tcx).ok()?;
             }
         }
 
@@ -6139,12 +6138,10 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
 
                 let mut elt_tys = elt_tys.clone();
                 if let Some((key_ty, value_ty)) = elt_tys.next_tuple() {
-                    builder
-                        .infer(&constraints, Type::TypeVar(key_ty), unpacked_key_ty)
-                        .ok()?;
+                    builder.infer(Type::TypeVar(key_ty), unpacked_key_ty).ok()?;
 
                     builder
-                        .infer(&constraints, Type::TypeVar(value_ty), unpacked_value_ty)
+                        .infer(Type::TypeVar(value_ty), unpacked_value_ty)
                         .ok()?;
                 }
 
@@ -6191,7 +6188,6 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
 
                 builder
                     .infer(
-                        &constraints,
                         Type::TypeVar(elt_ty),
                         if elt.is_starred_expr() {
                             inferred_elt_ty

From 8a6bdd5b27229a988f7785218dabd9df5697790c Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Thu, 5 Mar 2026 18:56:33 -0500
Subject: [PATCH 02/20] [phase 1] allow hook to choose specific typevar
 solution

---
 .../src/types/constraints.rs                  | 466 ++++++++++++------
 .../ty_python_semantic/src/types/generics.rs  |  43 ++
 2 files changed, 350 insertions(+), 159 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 2250b5bf12e9f..92e5ae1408b5e 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -597,7 +597,7 @@ impl<'db, 'c> ConstraintSet<'db, 'c> {
         self,
         db: &'db dyn Db,
         builder: &'c ConstraintSetBuilder<'db>,
-    ) -> Solutions<'db, 'c> {
+    ) -> Solutions<Ref<'c, Vec<Solution<'db>>>> {
         self.verify_builder(builder);
 
         // If the constraint set is cyclic, we'll hit an infinite expansion when trying to add type
@@ -609,6 +609,34 @@ impl<'db, 'c> ConstraintSet<'db, 'c> {
         self.node.solutions(db, builder)
     }
 
+    /// Computes solutions for each BDD path, using a caller-provided hook to select solutions.
+    ///
+    /// The `choose` hook is called for each typevar on each BDD path with the typevar's
+    /// materialized lower and upper bounds. It returns:
+    /// - `Some(ty)` to use `ty` as the solution for this typevar on this path
+    /// - `None` to fall back to the default solution selection logic
+    ///
+    /// For multi-path BDDs, the hook is called per-path. The caller is responsible for combining
+    /// results across paths (typically via union), matching the behavior of
+    /// [`add_type_mappings_from_constraint_set`][super::generics::SpecializationBuilder::add_type_mappings_from_constraint_set].
+    ///
+    /// Returns owned solutions (not cached), since the hook makes results non-deterministic.
+    #[expect(dead_code)] // Will be used in Phase 2 of the constraint set migration
+    pub(crate) fn solutions_with(
+        self,
+        db: &'db dyn Db,
+        builder: &'c ConstraintSetBuilder<'db>,
+        choose: impl FnMut(BoundTypeVarInstance<'db>, Type<'db>, Type<'db>) -> Option<Type<'db>>,
+    ) -> Solutions<Vec<Solution<'db>>> {
+        self.verify_builder(builder);
+
+        if self.is_cyclic(db) {
+            return Solutions::Unsatisfiable;
+        }
+
+        self.node.solutions_with(db, builder, choose)
+    }
+
     #[expect(dead_code)] // Keep this around for debugging purposes
     pub(crate) fn display(self, db: &'db dyn Db) -> impl Display {
         self.node
@@ -1724,7 +1752,7 @@ impl NodeId {
         self,
         db: &'db dyn Db,
         builder: &'c ConstraintSetBuilder<'db>,
-    ) -> Solutions<'db, 'c> {
+    ) -> Solutions<Ref<'c, Vec<Solution<'db>>>> {
         match self.node() {
             Node::AlwaysTrue => Solutions::Unconstrained,
             Node::AlwaysFalse => Solutions::Unsatisfiable,
@@ -1732,6 +1760,19 @@ impl NodeId {
         }
     }
 
+    fn solutions_with<'db>(
+        self,
+        db: &'db dyn Db,
+        builder: &ConstraintSetBuilder<'db>,
+        choose: impl FnMut(BoundTypeVarInstance<'db>, Type<'db>, Type<'db>) -> Option<Type<'db>>,
+    ) -> Solutions<Vec<Solution<'db>>> {
+        match self.node() {
+            Node::AlwaysTrue => Solutions::Unconstrained,
+            Node::AlwaysFalse => Solutions::Unsatisfiable,
+            Node::Interior(interior) => interior.solutions_with(db, builder, choose),
+        }
+    }
+
     /// Returns the negation of this BDD.
     fn negate(self, builder: &ConstraintSetBuilder<'_>) -> Self {
         match self.node() {
@@ -2598,6 +2639,237 @@ struct InteriorNodeData {
     max_source_order: usize,
 }
 
+/// Accumulated lower and upper bounds for a single typevar on a single BDD path.
+///
+/// Lower bounds are collected into a union (they are alternatives for the minimum type the
+/// typevar can specialize to). Upper bounds are collected into an intersection (the typevar
+/// must satisfy all of them simultaneously).
+#[derive(Default)]
+struct Bounds<'db> {
+    lower: FxIndexSet<Type<'db>>,
+    upper: FxIndexSet<Type<'db>>,
+}
+
+impl<'db> Bounds<'db> {
+    fn add_lower(&mut self, _db: &'db dyn Db, ty: Type<'db>) {
+        // Lower bounds are unioned. Our type representation is in DNF, so unioning a new
+        // element is typically cheap (in that it does not involve a combinatorial
+        // explosion from distributing the clause through an existing disjunction). So we
+        // don't need to be as clever here as in `add_upper`.
+        self.lower.insert(ty);
+    }
+
+    fn add_upper(&mut self, db: &'db dyn Db, ty: Type<'db>) {
+        // Upper bounds are intersectioned. If `ty` is a union, that involves distributing
+        // the union elements through the existing type. That makes it worth checking first
+        // whether any of the types in the upper bound are redundant.
+
+        // First check if there's an existing upper bound clause that is a subtype of the
+        // new type. If so, adding the new type does nothing to the intersection.
+        if self
+            .upper
+            .iter()
+            .any(|existing| existing.is_redundant_with(db, ty))
+        {
+            return;
+        }
+
+        // Otherwise remove any existing clauses that are a supertype of the new type,
+        // since the intersection will clip them to the new type.
+        self.upper
+            .retain(|existing| !ty.is_redundant_with(db, *existing));
+        self.upper.insert(ty);
+    }
+}
+
+/// Materialized lower and upper bounds for a single typevar on a single BDD path.
+struct TypeVarBounds<'db> {
+    bound_typevar: BoundTypeVarInstance<'db>,
+    /// The union of all lower bounds on this path.
+    lower: Type<'db>,
+    /// The intersection of all upper bounds on this path (NOT including the typevar's declared
+    /// upper bound).
+    upper: Type<'db>,
+}
+
+/// Per-path bounds for all typevars. Each element is the set of typevar bounds for one BDD path.
+type PathBounds<'db> = Vec<Vec<TypeVarBounds<'db>>>;
+
+/// Computes sorted BDD paths and accumulates per-typevar lower/upper bounds for each path.
+///
+/// Returns a list of paths, where each path contains the materialized lower/upper bounds for
+/// each typevar that appears in the path's constraints.
+fn compute_path_bounds<'db>(
+    db: &'db dyn Db,
+    builder: &ConstraintSetBuilder<'db>,
+    node: NodeId,
+) -> PathBounds<'db> {
+    // Sort the constraints in each path by their `source_order`s, to ensure that we construct
+    // any unions or intersections in our type mappings in a stable order. Constraints might
+    // come out of `PathAssignment`s with identical `source_order`s, but if they do, those
+    // "tied" constraints will still be ordered in a stable way. So we need a stable sort to
+    // retain that stable per-tie ordering.
+    let mut sorted_paths = Vec::new();
+    node.for_each_path(db, builder, |path| {
+        let mut path: Vec<_> = path.positive_constraints().collect();
+        path.sort_by_key(|(_, source_order)| *source_order);
+        sorted_paths.push(path);
+    });
+    sorted_paths.sort_by(|path1, path2| {
+        let source_orders1 = path1.iter().map(|(_, source_order)| *source_order);
+        let source_orders2 = path2.iter().map(|(_, source_order)| *source_order);
+        source_orders1.cmp(source_orders2)
+    });
+
+    let mut result = Vec::with_capacity(sorted_paths.len());
+    let mut mappings: FxHashMap<BoundTypeVarInstance<'db>, Bounds<'db>> = FxHashMap::default();
+
+    for path in sorted_paths {
+        mappings.clear();
+        for (constraint, _) in path {
+            let constraint = builder.constraint_data(constraint);
+            let typevar = constraint.typevar;
+            let lower = constraint.lower;
+            let upper = constraint.upper;
+            let bounds = mappings.entry(typevar).or_default();
+            bounds.add_lower(db, lower);
+            bounds.add_upper(db, upper);
+
+            if let Type::TypeVar(lower_bound_typevar) = lower {
+                let bounds = mappings.entry(lower_bound_typevar).or_default();
+                bounds.add_upper(db, Type::TypeVar(typevar));
+            }
+
+            if let Type::TypeVar(upper_bound_typevar) = upper {
+                let bounds = mappings.entry(upper_bound_typevar).or_default();
+                bounds.add_lower(db, Type::TypeVar(typevar));
+            }
+        }
+
+        let path_bounds = mappings
+            .drain()
+            .map(|(bound_typevar, bounds)| TypeVarBounds {
+                bound_typevar,
+                lower: UnionType::from_elements(db, bounds.lower),
+                upper: IntersectionType::from_elements(db, bounds.upper),
+            })
+            .collect();
+        result.push(path_bounds);
+    }
+
+    result
+}
+
+/// The default solution selection logic for a single typevar on a single BDD path.
+///
+/// Given the materialized lower and upper bounds for a typevar, selects the solution type.
+/// Returns:
+/// - `Ok(Some(solution))` if the typevar is solved on this path
+/// - `Ok(None)` if the typevar is unsolved (no solution added)
+/// - `Err(())` if the path is invalid (bounds violate the typevar's declared constraints)
+fn default_solve<'db>(
+    db: &'db dyn Db,
+    bound_typevar: BoundTypeVarInstance<'db>,
+    lower: Type<'db>,
+    upper: Type<'db>,
+) -> Result<Option<TypeVarSolution<'db>>, ()> {
+    match bound_typevar.typevar(db).require_bound_or_constraints(db) {
+        TypeVarBoundOrConstraints::UpperBound(bound) => {
+            let bound = bound.top_materialization(db);
+            if !lower.is_assignable_to(db, bound) {
+                // This path does not satisfy the typevar's upper bound, and is
+                // therefore not a valid specialization.
+                return Err(());
+            }
+
+            // Prefer the lower bound (often the concrete actual type seen) over the
+            // upper bound (which may include TypeVar bounds/constraints). The upper bound
+            // should only be used as a fallback when no concrete type was inferred.
+            if !lower.is_never() {
+                return Ok(Some(TypeVarSolution {
+                    bound_typevar,
+                    solution: lower,
+                }));
+            }
+
+            let upper = IntersectionType::from_elements(
+                db,
+                std::iter::once(upper).chain(std::iter::once(bound)),
+            );
+            if upper != bound {
+                Ok(Some(TypeVarSolution {
+                    bound_typevar,
+                    solution: upper,
+                }))
+            } else {
+                Ok(None)
+            }
+        }
+
+        TypeVarBoundOrConstraints::Constraints(constraints) => {
+            // Filter out the typevar constraints that aren't satisfied by this path.
+            let compatible_constraints = constraints.elements(db).iter().filter(|constraint| {
+                let constraint_lower = constraint.bottom_materialization(db);
+                let constraint_upper = constraint.top_materialization(db);
+                lower.is_assignable_to(db, constraint_lower)
+                    && constraint_upper.is_assignable_to(db, upper)
+            });
+
+            // If only one constraint remains, that's our specialization for this path.
+            match compatible_constraints.at_most_one() {
+                Ok(None) => {
+                    // This path does not satisfy any of the constraints, and is
+                    // therefore not a valid specialization.
+                    Err(())
+                }
+
+                Ok(Some(compatible_constraint)) => Ok(Some(TypeVarSolution {
+                    bound_typevar,
+                    solution: *compatible_constraint,
+                })),
+
+                Err(_) => {
+                    // This path satisfies multiple constraints. For now, don't
+                    // prefer any of them, and fall back on the default
+                    // specialization for this typevar.
+                    Ok(None)
+                }
+            }
+        }
+    }
+}
+
+/// Solves each path by applying a per-typevar solver function, collecting valid solutions.
+///
+/// The solver receives the typevar and its materialized lower/upper bounds, and returns:
+/// - `Ok(Some(solution))` to add a solution for this typevar on this path
+/// - `Ok(None)` to leave this typevar unsolved on this path
+/// - `Err(())` to invalidate the entire path
+fn solve_paths<'db>(
+    db: &'db dyn Db,
+    path_bounds: &PathBounds<'db>,
+    mut solver: impl FnMut(
+        &'db dyn Db,
+        BoundTypeVarInstance<'db>,
+        Type<'db>,
+        Type<'db>,
+    ) -> Result<Option<TypeVarSolution<'db>>, ()>,
+) -> Vec<Solution<'db>> {
+    let mut solutions = Vec::with_capacity(path_bounds.len());
+    'paths: for path in path_bounds {
+        let mut solution = Vec::with_capacity(path.len());
+        for tvb in path {
+            match solver(db, tvb.bound_typevar, tvb.lower, tvb.upper) {
+                Ok(Some(s)) => solution.push(s),
+                Ok(None) => {}
+                Err(()) => continue 'paths,
+            }
+        }
+        solutions.push(solution);
+    }
+    solutions
+}
+
 impl InteriorNode {
     fn node(self) -> NodeId {
         self.0
@@ -3112,45 +3384,7 @@ impl InteriorNode {
         self,
         db: &'db dyn Db,
         builder: &'c ConstraintSetBuilder<'db>,
-    ) -> Solutions<'db, 'c> {
-        #[derive(Default)]
-        struct Bounds<'db> {
-            lower: FxIndexSet<Type<'db>>,
-            upper: FxIndexSet<Type<'db>>,
-        }
-
-        impl<'db> Bounds<'db> {
-            fn add_lower(&mut self, _db: &'db dyn Db, ty: Type<'db>) {
-                // Lower bounds are unioned. Our type representation is in DNF, so unioning a new
-                // element is typically cheap (in that it does not involve a combinatorial
-                // explosion from distributing the clause through an existing disjunction). So we
-                // don't need to be as clever here as in `add_upper`.
-                self.lower.insert(ty);
-            }
-
-            fn add_upper(&mut self, db: &'db dyn Db, ty: Type<'db>) {
-                // Upper bounds are intersectioned. If `ty` is a union, that involves distributing
-                // the union elements through the existing type. That makes it worth checking first
-                // whether any of the types in the upper bound are redundant.
-
-                // First check if there's an existing upper bound clause that is a subtype of the
-                // new type. If so, adding the new type does nothing to the intersection.
-                if self
-                    .upper
-                    .iter()
-                    .any(|existing| existing.is_redundant_with(db, ty))
-                {
-                    return;
-                }
-
-                // Otherwise remove any existing clauses that are a supertype of the new type,
-                // since the intersection will clip them to the new type.
-                self.upper
-                    .retain(|existing| !ty.is_redundant_with(db, *existing));
-                self.upper.insert(ty);
-            }
-        }
-
+    ) -> Solutions<Ref<'c, Vec<Solution<'db>>>> {
         fn solutions_inner<'db, 'c>(
             db: &'db dyn Db,
             builder: &'c ConstraintSetBuilder<'db>,
@@ -3164,122 +3398,8 @@ impl InteriorNode {
                 return solutions;
             }
 
-            // Sort the constraints in each path by their `source_order`s, to ensure that we construct
-            // any unions or intersections in our type mappings in a stable order. Constraints might
-            // come out of `PathAssignment`s with identical `source_order`s, but if they do, those
-            // "tied" constraints will still be ordered in a stable way. So we need a stable sort to
-            // retain that stable per-tie ordering.
-            let mut sorted_paths = Vec::new();
-            interior.for_each_path(db, builder, |path| {
-                let mut path: Vec<_> = path.positive_constraints().collect();
-                path.sort_by_key(|(_, source_order)| *source_order);
-                sorted_paths.push(path);
-            });
-            sorted_paths.sort_by(|path1, path2| {
-                let source_orders1 = path1.iter().map(|(_, source_order)| *source_order);
-                let source_orders2 = path2.iter().map(|(_, source_order)| *source_order);
-                source_orders1.cmp(source_orders2)
-            });
-
-            let mut solutions = Vec::with_capacity(sorted_paths.len());
-            let mut mappings: FxHashMap<BoundTypeVarInstance<'db>, Bounds<'db>> =
-                FxHashMap::default();
-            'paths: for path in sorted_paths {
-                mappings.clear();
-                for (constraint, _) in path {
-                    let constraint = builder.constraint_data(constraint);
-                    let typevar = constraint.typevar;
-                    let lower = constraint.lower;
-                    let upper = constraint.upper;
-                    let bounds = mappings.entry(typevar).or_default();
-                    bounds.add_lower(db, lower);
-                    bounds.add_upper(db, upper);
-
-                    if let Type::TypeVar(lower_bound_typevar) = lower {
-                        let bounds = mappings.entry(lower_bound_typevar).or_default();
-                        bounds.add_upper(db, Type::TypeVar(typevar));
-                    }
-
-                    if let Type::TypeVar(upper_bound_typevar) = upper {
-                        let bounds = mappings.entry(upper_bound_typevar).or_default();
-                        bounds.add_lower(db, Type::TypeVar(typevar));
-                    }
-                }
-
-                let mut solution = Vec::with_capacity(mappings.len());
-                for (bound_typevar, bounds) in mappings.drain() {
-                    match bound_typevar.typevar(db).require_bound_or_constraints(db) {
-                        TypeVarBoundOrConstraints::UpperBound(bound) => {
-                            let bound = bound.top_materialization(db);
-                            let lower = UnionType::from_elements(db, bounds.lower);
-                            if !lower.is_assignable_to(db, bound) {
-                                // This path does not satisfy the typevar's upper bound, and is
-                                // therefore not a valid specialization.
-                                continue 'paths;
-                            }
-
-                            // Prefer the lower bound (often the concrete actual type seen) over the
-                            // upper bound (which may include TypeVar bounds/constraints). The upper bound
-                            // should only be used as a fallback when no concrete type was inferred.
-                            if !lower.is_never() {
-                                solution.push(TypeVarSolution {
-                                    bound_typevar,
-                                    solution: lower,
-                                });
-                                continue;
-                            }
-
-                            let upper = IntersectionType::from_elements(
-                                db,
-                                std::iter::chain(bounds.upper, [bound]),
-                            );
-                            if upper != bound {
-                                solution.push(TypeVarSolution {
-                                    bound_typevar,
-                                    solution: upper,
-                                });
-                            }
-                        }
-
-                        TypeVarBoundOrConstraints::Constraints(constraints) => {
-                            // Filter out the typevar constraints that aren't satisfied by this path.
-                            let lower = UnionType::from_elements(db, bounds.lower);
-                            let upper = IntersectionType::from_elements(db, bounds.upper);
-                            let compatible_constraints =
-                                constraints.elements(db).iter().filter(|constraint| {
-                                    let constraint_lower = constraint.bottom_materialization(db);
-                                    let constraint_upper = constraint.top_materialization(db);
-                                    lower.is_assignable_to(db, constraint_lower)
-                                        && constraint_upper.is_assignable_to(db, upper)
-                                });
-
-                            // If only one constraint remains, that's our specialization for this path.
-                            match compatible_constraints.at_most_one() {
-                                Ok(None) => {
-                                    // This path does not satisfy any of the constraints, and is
-                                    // therefore not a valid specialization.
-                                    continue 'paths;
-                                }
-
-                                Ok(Some(compatible_constraint)) => {
-                                    solution.push(TypeVarSolution {
-                                        bound_typevar,
-                                        solution: *compatible_constraint,
-                                    });
-                                }
-
-                                Err(_) => {
-                                    // This path satisfies multiple constraints. For now, don't
-                                    // prefer any of them, and fall back on the default
-                                    // specialization for this typevar.
-                                }
-                            }
-                        }
-                    }
-                }
-
-                solutions.push(solution);
-            }
+            let path_bounds = compute_path_bounds(db, builder, interior);
+            let solutions = solve_paths(db, &path_bounds, default_solve);
 
             let mut storage = builder.storage.borrow_mut();
             storage.solutions_cache.insert(key, solutions);
@@ -3296,6 +3416,28 @@ impl InteriorNode {
         Solutions::Constrained(solutions)
     }
 
+    fn solutions_with<'db>(
+        self,
+        db: &'db dyn Db,
+        builder: &ConstraintSetBuilder<'db>,
+        mut choose: impl FnMut(BoundTypeVarInstance<'db>, Type<'db>, Type<'db>) -> Option<Type<'db>>,
+    ) -> Solutions<Vec<Solution<'db>>> {
+        let path_bounds = compute_path_bounds(db, builder, self.node());
+        let solutions = solve_paths(db, &path_bounds, |db, bound_typevar, lower, upper| {
+            if let Some(ty) = choose(bound_typevar, lower, upper) {
+                return Ok(Some(TypeVarSolution {
+                    bound_typevar,
+                    solution: ty,
+                }));
+            }
+            default_solve(db, bound_typevar, lower, upper)
+        });
+        if solutions.is_empty() {
+            return Solutions::Unsatisfiable;
+        }
+        Solutions::Constrained(solutions)
+    }
+
     fn path_assignments(self, builder: &ConstraintSetBuilder<'_>) -> PathAssignments {
         // Sort the constraints in this BDD by their `source_order`s before adding them to the
         // sequent map. This ensures that constraints appear in the sequent map in a stable order.
@@ -3738,11 +3880,17 @@ impl InteriorNode {
     }
 }
 
+/// The result of solving a constraint set for per-typevar specializations.
+///
+/// Generic over the container type `S`: cached solutions use
+/// `Ref<'c, Vec<Solution<'db>>>` (borrowed from the builder's cache), while
+/// hook-based solutions use `Vec<Solution<'db>>` (owned, since the hook makes
+/// caching inappropriate).
 #[derive(Debug)]
-pub(crate) enum Solutions<'db, 'c> {
+pub(crate) enum Solutions<S> {
     Unsatisfiable,
     Unconstrained,
-    Constrained(Ref<'c, Vec<Solution<'db>>>),
+    Constrained(S),
 }
 
 pub(crate) type Solution<'db> = Vec<TypeVarSolution<'db>>;
diff --git a/crates/ty_python_semantic/src/types/generics.rs b/crates/ty_python_semantic/src/types/generics.rs
index 73cc955f3e911..786ac95abac0b 100644
--- a/crates/ty_python_semantic/src/types/generics.rs
+++ b/crates/ty_python_semantic/src/types/generics.rs
@@ -1732,6 +1732,49 @@ impl<'db, 'c> SpecializationBuilder<'db, 'c> {
         generic_context.specialize_recursive(self.db, types)
     }
 
+    /// Build a specialization, using a caller-provided hook to select the solution for each
+    /// typevar.
+    ///
+    /// The `choose` hook is called for each typevar in the generic context with the typevar's
+    /// materialized lower and upper bounds:
+    /// - For typevars that were inferred (present in the type mappings), both bounds are set to
+    ///   the inferred type (representing an equality constraint).
+    /// - For typevars that were not inferred, `lower` is `Never` and `upper` is `object`
+    ///   (representing an unconstrained typevar).
+    ///
+    /// The hook returns:
+    /// - `Some(ty)` to use `ty` as the specialization for this typevar
+    /// - `None` to use the default (the inferred type for mapped typevars, or the typevar's
+    ///   default for unmapped typevars)
+    ///
+    /// This method replaces the pattern of `mapped(...).build(...)`, allowing callers to
+    /// transform inferred types (e.g., literal promotion) in a single step. In the future,
+    /// when the builder's internal representation switches from a `HashMap` to a `ConstraintSet`,
+    /// the hook will receive actual lower/upper bounds from the constraint set instead of
+    /// synthetic equality bounds.
+    #[expect(dead_code)] // Will be used in Phase 2 of the constraint set migration
+    pub(crate) fn build_with(
+        &mut self,
+        generic_context: GenericContext<'db>,
+        mut choose: impl FnMut(BoundTypeVarInstance<'db>, Type<'db>, Type<'db>) -> Option<Type<'db>>,
+    ) -> Specialization<'db> {
+        let types = generic_context
+            .variables_inner(self.db)
+            .iter()
+            .map(|(identity, variable)| {
+                if let Some(&mapped_ty) = self.types.get(identity) {
+                    // The typevar was inferred — present both bounds as the inferred type.
+                    let chosen = choose(*variable, mapped_ty, mapped_ty);
+                    Some(chosen.unwrap_or(mapped_ty))
+                } else {
+                    // The typevar was not inferred — present open bounds.
+                    choose(*variable, Type::Never, Type::object())
+                }
+            });
+
+        generic_context.specialize_recursive(self.db, types)
+    }
+
     fn add_type_mapping(
         &mut self,
         bound_typevar: BoundTypeVarInstance<'db>,

From 9ee3251018bc3706084a10e24165c7b6cdc32529 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Thu, 5 Mar 2026 20:44:54 -0500
Subject: [PATCH 03/20] [phase 2] use solutions hook to promote literals

---
 .../ty_python_semantic/src/types/call/bind.rs | 79 ++++++++++---------
 .../ty_python_semantic/src/types/generics.rs  | 47 +++--------
 2 files changed, 49 insertions(+), 77 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/call/bind.rs b/crates/ty_python_semantic/src/types/call/bind.rs
index b00bc5467bb91..082140412440e 100644
--- a/crates/ty_python_semantic/src/types/call/bind.rs
+++ b/crates/ty_python_semantic/src/types/call/bind.rs
@@ -3800,55 +3800,56 @@ impl<'a, 'db> ArgumentTypeChecker<'a, 'db> {
         self.errors.extend(specialization_errors);
 
         // Attempt to promote any promotable types assigned to the specialization.
-        let maybe_promote = |typevar: BoundTypeVarInstance<'db>, ty: Type<'db>| {
-            let bound_or_constraints = typevar.typevar(self.db).bound_or_constraints(self.db);
-
-            // For constrained TypeVars, the inferred type is already one of the
-            // constraints. Promoting literals would produce a type that doesn't
-            // match any constraint.
-            if matches!(
-                bound_or_constraints,
-                Some(TypeVarBoundOrConstraints::Constraints(_))
-            ) {
-                return ty;
-            }
+        // The hook receives (typevar, lower_bound, upper_bound) and returns Some(ty) to
+        // override the default solution, or None to keep it.
+        let maybe_promote =
+            |typevar: BoundTypeVarInstance<'db>, lower: Type<'db>, _upper: Type<'db>| {
+                let bound_or_constraints = typevar.typevar(self.db).bound_or_constraints(self.db);
+
+                // For constrained TypeVars, the inferred type is already one of the
+                // constraints. Promoting literals would produce a type that doesn't
+                // match any constraint.
+                if matches!(
+                    bound_or_constraints,
+                    Some(TypeVarBoundOrConstraints::Constraints(_))
+                ) {
+                    return None;
+                }
 
-            let return_ty = self.constructor_instance_type.unwrap_or(self.return_ty);
-            let mut variance_in_return = TypeVarVariance::Bivariant;
+                let return_ty = self.constructor_instance_type.unwrap_or(self.return_ty);
+                let mut variance_in_return = TypeVarVariance::Bivariant;
 
-            // Find all occurrences of the type variable in the return type.
-            let visit_return_ty = |_, ty, variance, _| {
-                if ty != Type::TypeVar(typevar) {
-                    return;
-                }
+                // Find all occurrences of the type variable in the return type.
+                let visit_return_ty = |_, ty, variance, _| {
+                    if ty != Type::TypeVar(typevar) {
+                        return;
+                    }
 
-                variance_in_return = variance_in_return.join(variance);
-            };
+                    variance_in_return = variance_in_return.join(variance);
+                };
 
-            return_ty.visit_specialization(self.db, self.call_expression_tcx, visit_return_ty);
+                return_ty.visit_specialization(self.db, self.call_expression_tcx, visit_return_ty);
 
-            // Promotion is only useful if the type variable is in invariant or contravariant
-            // position in the return type.
-            if variance_in_return.is_covariant() {
-                return ty;
-            }
+                // Promotion is only useful if the type variable is in invariant or contravariant
+                // position in the return type.
+                if variance_in_return.is_covariant() {
+                    return None;
+                }
 
-            let promoted = ty.promote(self.db);
+                let promoted = lower.promote(self.db);
 
-            // If the TypeVar has an upper bound, only use the promoted type if it
-            // still satisfies the bound.
-            if let Some(TypeVarBoundOrConstraints::UpperBound(bound)) = bound_or_constraints {
-                if !promoted.is_assignable_to(self.db, bound) {
-                    return ty;
+                // If the TypeVar has an upper bound, only use the promoted type if it
+                // still satisfies the bound.
+                if let Some(TypeVarBoundOrConstraints::UpperBound(bound)) = bound_or_constraints {
+                    if !promoted.is_assignable_to(self.db, bound) {
+                        return None;
+                    }
                 }
-            }
 
-            promoted
-        };
+                Some(promoted)
+            };
 
-        let specialization = builder
-            .mapped(generic_context, maybe_promote)
-            .build(generic_context);
+        let specialization = builder.build_with(generic_context, maybe_promote);
 
         self.return_ty = self.return_ty.apply_specialization(self.db, specialization);
         self.specialization = Some(specialization);
diff --git a/crates/ty_python_semantic/src/types/generics.rs b/crates/ty_python_semantic/src/types/generics.rs
index 786ac95abac0b..521e21876df63 100644
--- a/crates/ty_python_semantic/src/types/generics.rs
+++ b/crates/ty_python_semantic/src/types/generics.rs
@@ -1674,27 +1674,6 @@ impl<'db, 'c> SpecializationBuilder<'db, 'c> {
         self.types
     }
 
-    /// Map the types that have been assigned in this specialization.
-    pub(crate) fn mapped(
-        &self,
-        generic_context: GenericContext<'db>,
-        f: impl Fn(BoundTypeVarInstance<'db>, Type<'db>) -> Type<'db>,
-    ) -> Self {
-        let mut types = self.types.clone();
-        for (identity, variable) in generic_context.variables_inner(self.db) {
-            if let Some(ty) = types.get_mut(identity) {
-                *ty = f(*variable, *ty);
-            }
-        }
-
-        Self {
-            db: self.db,
-            constraints: self.constraints,
-            inferable: self.inferable,
-            types,
-        }
-    }
-
     pub(crate) fn with_default(
         &self,
         generic_context: GenericContext<'db>,
@@ -1735,24 +1714,20 @@ impl<'db, 'c> SpecializationBuilder<'db, 'c> {
     /// Build a specialization, using a caller-provided hook to select the solution for each
     /// typevar.
     ///
-    /// The `choose` hook is called for each typevar in the generic context with the typevar's
-    /// materialized lower and upper bounds:
-    /// - For typevars that were inferred (present in the type mappings), both bounds are set to
-    ///   the inferred type (representing an equality constraint).
-    /// - For typevars that were not inferred, `lower` is `Never` and `upper` is `object`
-    ///   (representing an unconstrained typevar).
+    /// The `choose` hook is called for each *inferred* typevar (those with entries in the type
+    /// mappings) with the typevar's materialized lower and upper bounds. Currently, both bounds
+    /// are set to the inferred type (representing an equality constraint). Unmapped typevars
+    /// are left to `specialize_recursive` to fill in with defaults.
     ///
     /// The hook returns:
     /// - `Some(ty)` to use `ty` as the specialization for this typevar
-    /// - `None` to use the default (the inferred type for mapped typevars, or the typevar's
-    ///   default for unmapped typevars)
+    /// - `None` to use the inferred type unchanged
     ///
     /// This method replaces the pattern of `mapped(...).build(...)`, allowing callers to
     /// transform inferred types (e.g., literal promotion) in a single step. In the future,
     /// when the builder's internal representation switches from a `HashMap` to a `ConstraintSet`,
     /// the hook will receive actual lower/upper bounds from the constraint set instead of
     /// synthetic equality bounds.
-    #[expect(dead_code)] // Will be used in Phase 2 of the constraint set migration
     pub(crate) fn build_with(
         &mut self,
         generic_context: GenericContext<'db>,
@@ -1762,14 +1737,10 @@ impl<'db, 'c> SpecializationBuilder<'db, 'c> {
             .variables_inner(self.db)
             .iter()
             .map(|(identity, variable)| {
-                if let Some(&mapped_ty) = self.types.get(identity) {
-                    // The typevar was inferred — present both bounds as the inferred type.
-                    let chosen = choose(*variable, mapped_ty, mapped_ty);
-                    Some(chosen.unwrap_or(mapped_ty))
-                } else {
-                    // The typevar was not inferred — present open bounds.
-                    choose(*variable, Type::Never, Type::object())
-                }
+                let mapped_ty = self.types.get(identity).copied()?;
+                // The typevar was inferred — present both bounds as the inferred type.
+                let chosen = choose(*variable, mapped_ty, mapped_ty);
+                Some(chosen.unwrap_or(mapped_ty))
             });
 
         generic_context.specialize_recursive(self.db, types)

From 889002c6c6f258b6911d281753c6af1eb3e9da1f Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Thu, 5 Mar 2026 21:13:02 -0500
Subject: [PATCH 04/20] [phase 3] replace most infer_reverse calls with
 constraint set checks

---
 .../resources/mdtest/promotion.md             |   2 +-
 crates/ty_python_semantic/src/types.rs        |  51 +++--
 .../src/types/constraints.rs                  |   1 -
 .../ty_python_semantic/src/types/generics.rs  |   2 +
 .../src/types/infer/builder.rs                | 195 +++++++++++++-----
 5 files changed, 183 insertions(+), 68 deletions(-)

diff --git a/crates/ty_python_semantic/resources/mdtest/promotion.md b/crates/ty_python_semantic/resources/mdtest/promotion.md
index c0987d7613234..1ddedb2c5b832 100644
--- a/crates/ty_python_semantic/resources/mdtest/promotion.md
+++ b/crates/ty_python_semantic/resources/mdtest/promotion.md
@@ -238,7 +238,7 @@ x11: list[Literal[1] | Literal[2] | Literal[3]] = [1, 2, 3]
 reveal_type(x11)  # revealed: list[Literal[1, 2, 3]]
 
 x12: Y[Y[Literal[1]]] = [[1]]
-reveal_type(x12)  # revealed: list[Y[Literal[1]]]
+reveal_type(x12)  # revealed: list[list[Literal[1]]]
 
 x13: list[tuple[Literal[1], Literal[2], Literal[3]]] = [(1, 2, 3)]
 reveal_type(x13)  # revealed: list[tuple[Literal[1], Literal[2], Literal[3]]]
diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs
index 2b8580173ad0e..c7d4c7eed391d 100644
--- a/crates/ty_python_semantic/src/types.rs
+++ b/crates/ty_python_semantic/src/types.rs
@@ -51,7 +51,7 @@ use crate::types::bound_super::BoundSuperType;
 use crate::types::call::{Binding, Bindings, CallArguments, CallableBinding};
 pub(crate) use crate::types::callable::{CallableType, CallableTypes};
 pub(crate) use crate::types::class_base::ClassBase;
-use crate::types::constraints::ConstraintSetBuilder;
+use crate::types::constraints::{ConstraintSetBuilder, Solutions};
 use crate::types::context::{LintDiagnosticGuard, LintDiagnosticGuardBuilder};
 use crate::types::diagnostic::{INVALID_AWAIT, INVALID_TYPE_FORM};
 pub use crate::types::display::{DisplaySettings, TypeDetail, TypeDisplayDetails};
@@ -60,10 +60,10 @@ use crate::types::function::{
     DataclassTransformerFlags, DataclassTransformerParams, FunctionDecorators, FunctionSpans,
     FunctionType, KnownFunction,
 };
+pub(crate) use crate::types::generics::GenericContext;
 use crate::types::generics::{
     ApplySpecialization, InferableTypeVars, Specialization, bind_typevar,
 };
-pub(crate) use crate::types::generics::{GenericContext, SpecializationBuilder};
 use crate::types::infer::InferenceFlags;
 use crate::types::known_instance::{InternedConstraintSet, InternedType, UnionTypeInstance};
 pub use crate::types::method::{BoundMethodType, KnownBoundMethodType, WrapperDescriptorKind};
@@ -1883,17 +1883,44 @@ impl<'db> Type<'db> {
         let generic_context = specialization.generic_context(db);
 
         // Collect the type mappings used to narrow the type context.
-        let tcx_mappings = {
-            let mut builder =
-                SpecializationBuilder::new(db, constraints, generic_context.inferable_typevars(db));
-
-            if let Some(tcx) = tcx.annotation {
+        //
+        // We use a forward CSA check (`alias_instance ≤ tcx`) to infer what each typevar
+        // in the identity specialization maps to in the type context. For example, if
+        // `tcx = list[int]` and `alias_instance = list[T]`, the CSA produces `T = int`.
+        let tcx_mappings: FxHashMap<_, _> = tcx
+            .annotation
+            .and_then(|tcx| {
                 let alias_instance = Type::instance(db, class_literal.identity_specialization(db));
-                let _ = builder.infer_reverse(tcx, alias_instance);
-            }
-
-            builder.into_type_mappings()
-        };
+                let inferable = generic_context.inferable_typevars(db);
+                let set = alias_instance.when_constraint_set_assignable_to(
+                    db,
+                    tcx,
+                    constraints,
+                    inferable,
+                );
+                match set.solutions(db, constraints) {
+                    Solutions::Constrained(solutions) => {
+                        let mut mappings = FxHashMap::default();
+                        for solution in solutions.iter() {
+                            for binding in solution {
+                                mappings
+                                    .entry(binding.bound_typevar.identity(db))
+                                    .and_modify(|existing| {
+                                        *existing = UnionType::from_two_elements(
+                                            db,
+                                            *existing,
+                                            binding.solution,
+                                        );
+                                    })
+                                    .or_insert(binding.solution);
+                            }
+                        }
+                        Some(mappings)
+                    }
+                    _ => None,
+                }
+            })
+            .unwrap_or_default();
 
         for (type_var, ty) in generic_context.variables(db).zip(specialization.types(db)) {
             let variance = type_var.variance_with_polarity(db, polarity);
diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 92e5ae1408b5e..2ad7c7a3ee1f8 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -621,7 +621,6 @@ impl<'db, 'c> ConstraintSet<'db, 'c> {
     /// [`add_type_mappings_from_constraint_set`][super::generics::SpecializationBuilder::add_type_mappings_from_constraint_set].
     ///
     /// Returns owned solutions (not cached), since the hook makes results non-deterministic.
-    #[expect(dead_code)] // Will be used in Phase 2 of the constraint set migration
     pub(crate) fn solutions_with(
         self,
         db: &'db dyn Db,
diff --git a/crates/ty_python_semantic/src/types/generics.rs b/crates/ty_python_semantic/src/types/generics.rs
index 521e21876df63..d97a4fd7af748 100644
--- a/crates/ty_python_semantic/src/types/generics.rs
+++ b/crates/ty_python_semantic/src/types/generics.rs
@@ -1674,6 +1674,7 @@ impl<'db, 'c> SpecializationBuilder<'db, 'c> {
         self.types
     }
 
+    #[expect(dead_code)] // Will be removed in Phase 4
     pub(crate) fn with_default(
         &self,
         generic_context: GenericContext<'db>,
@@ -2401,6 +2402,7 @@ impl<'db, 'c> SpecializationBuilder<'db, 'c> {
 
     /// Infer type mappings for the specialization in the reverse direction, i.e., where the
     /// actual type, not the formal type, contains inferable type variables.
+    #[expect(dead_code)] // Will be removed in Phase 4
     pub(crate) fn infer_reverse(
         &mut self,
         formal: Type<'db>,
diff --git a/crates/ty_python_semantic/src/types/infer/builder.rs b/crates/ty_python_semantic/src/types/infer/builder.rs
index 05c585eb20dce..46cc2cfd49816 100644
--- a/crates/ty_python_semantic/src/types/infer/builder.rs
+++ b/crates/ty_python_semantic/src/types/infer/builder.rs
@@ -58,7 +58,7 @@ use crate::types::class::{
     ClassLiteral, CodeGeneratorKind, DynamicClassAnchor, DynamicClassLiteral,
     DynamicMetaclassConflict, MethodDecorator,
 };
-use crate::types::constraints::ConstraintSetBuilder;
+use crate::types::constraints::{ConstraintSetBuilder, Solutions};
 use crate::types::context::InferContext;
 use crate::types::diagnostic::{
     self, CALL_NON_CALLABLE, CONFLICTING_DECLARATIONS, CYCLIC_CLASS_DEFINITION,
@@ -5172,35 +5172,59 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
                 // If this is a generic call, attempt to specialize the parameter type using the
                 // declared type context, if provided.
                 if let Some(generic_context) = overload.signature.generic_context {
-                    let mut builder = SpecializationBuilder::new(
-                        db,
-                        &constraints,
-                        generic_context.inferable_typevars(db),
-                    );
-
+                    // Use a forward CSA check to infer typevar specializations from the
+                    // declared type context. For example, if the return type is `list[T]`
+                    // and the declared type context is `list[int]`, CSA produces `T = int`.
+                    let mut tcx_mappings = FxHashMap::default();
                     if let Some(declared_return_ty) = call_expression_tcx.annotation {
-                        let _ = builder.infer_reverse(
+                        let return_ty = overload
+                            .constructor_instance_type
+                            .unwrap_or(overload.signature.return_ty);
+                        let inferable = generic_context.inferable_typevars(db);
+                        let set = return_ty.when_constraint_set_assignable_to(
+                            db,
                             declared_return_ty,
-                            overload
-                                .constructor_instance_type
-                                .unwrap_or(overload.signature.return_ty),
+                            &constraints,
+                            inferable,
                         );
+                        if let Solutions::Constrained(solutions) = set.solutions(db, &constraints) {
+                            for solution in solutions.iter() {
+                                for binding in solution {
+                                    tcx_mappings
+                                        .entry(binding.bound_typevar.identity(db))
+                                        .and_modify(|existing| {
+                                            *existing = UnionType::from_two_elements(
+                                                db,
+                                                *existing,
+                                                binding.solution,
+                                            );
+                                        })
+                                        .or_insert(binding.solution);
+                                }
+                            }
+                        }
                     }
 
-                    let specialization = builder
-                        // Default specialize any type variables to a marker type, which will be ignored
-                        // during argument inference, allowing the concrete subset of the parameter
-                        // type to still affect argument inference.
-                        //
-                        // TODO: Eventually, we want to "tie together" the typevars of the two calls
-                        // so that we can infer their specializations at the same time — or at least, for
-                        // the specialization of one to influence the specialization of the other. It's
-                        // not yet clear how we're going to do that. (We might have to start inferring
-                        // constraint sets for each expression, instead of simple types?)
-                        .with_default(generic_context, |_| {
-                            Type::Dynamic(DynamicType::UnspecializedTypeVar)
-                        })
-                        .build(generic_context);
+                    // Default specialize any type variables to a marker type, which will be ignored
+                    // during argument inference, allowing the concrete subset of the parameter
+                    // type to still affect argument inference.
+                    //
+                    // TODO: Eventually, we want to "tie together" the typevars of the two calls
+                    // so that we can infer their specializations at the same time — or at least, for
+                    // the specialization of one to influence the specialization of the other. It's
+                    // not yet clear how we're going to do that. (We might have to start inferring
+                    // constraint sets for each expression, instead of simple types?)
+                    let specialization = generic_context.specialize_recursive(
+                        db,
+                        generic_context.variables(db).map(|typevar| {
+                            Some(
+                                tcx_mappings
+                                    .get(&typevar.identity(db))
+                                    .copied()
+                                    .unwrap_or(Type::Dynamic(DynamicType::UnspecializedTypeVar)),
+                            )
+                        }),
+                    );
 
                     parameter_type = parameter_type.apply_specialization(db, specialization);
                 }
@@ -6036,47 +6060,110 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
         });
 
         // Collect type constraints from the declared element types.
+        //
+        // We use a forward CSA check (`collection_instance ≤ tcx`) to infer what each
+        // typevar maps to in the type context. For example, if `tcx = list[int]` and
+        // `collection_instance = list[T]`, the CSA produces `T = int`.
+        //
+        // Variance is determined from the constraint bounds: a constraint with only an
+        // upper bound (`lower = Never`) indicates a covariant position, while a constraint
+        // with only a lower bound (`upper = object`) indicates contravariant. This correctly
+        // handles cases where the TCX type is a covariant superclass of the collection
+        // (e.g., `Sequence[Any]` as TCX for `list[T]`).
         let (elt_tcx_constraints, elt_tcx_variance) = {
-            let mut builder = SpecializationBuilder::new(self.db(), &constraints, inferable);
-
-            // For a given type variable, we keep track of the variance of any assignments to
-            // that type variable in the type context.
+            let mut elt_tcx_constraints: FxHashMap<BoundTypeVarIdentity<'_>, Type<'db>> =
+                FxHashMap::default();
             let mut elt_tcx_variance: FxHashMap<BoundTypeVarIdentity<'_>, TypeVarVariance> =
                 FxHashMap::default();
 
             if let Some(tcx) = tcx.annotation
                 && tcx.class_specialization(self.db()).is_some()
             {
-                let collection_instance =
-                    Type::instance(self.db(), ClassType::Generic(collection_alias));
+                let db = self.db();
+                let collection_instance = Type::instance(db, ClassType::Generic(collection_alias));
 
-                builder
-                    .infer_reverse_map(
-                        tcx,
-                        collection_instance,
-                        |(typevar, variance, inferred_ty)| {
-                            // Avoid inferring a preferred type based on partially specialized type context
-                            // from an outer generic call. If the type context is a union, we try to keep
-                            // any concrete elements.
-                            let inferred_ty = inferred_ty.filter_union(self.db(), |ty| {
-                                !ty.has_unspecialized_type_var(self.db())
-                            });
-                            if inferred_ty.has_unspecialized_type_var(self.db()) {
-                                return None;
-                            }
+                let set = collection_instance.when_constraint_set_assignable_to(
+                    db,
+                    tcx,
+                    &constraints,
+                    inferable,
+                );
 
-                            elt_tcx_variance
-                                .entry(typevar)
-                                .and_modify(|current| *current = current.join(variance))
-                                .or_insert(variance);
+                // Use `solutions_with` to capture per-typevar variance from the raw
+                // lower/upper bounds on each BDD path.
+                let solutions = set.solutions_with(db, &constraints, |typevar, lower, upper| {
+                    // Determine variance from the constraint bounds:
+                    // - Only upper bound (lower = Never) → covariant position
+                    // - Only lower bound (upper = object) → contravariant position
+                    // - Both bounds set → invariant position
+                    let variance = if lower.is_never() {
+                        TypeVarVariance::Covariant
+                    } else if upper == Type::object() {
+                        TypeVarVariance::Contravariant
+                    } else {
+                        TypeVarVariance::Invariant
+                    };
+                    let identity = typevar.identity(db);
+                    elt_tcx_variance
+                        .entry(identity)
+                        .and_modify(|current| *current = current.join(variance))
+                        .or_insert(variance);
+                    None // Use default solution selection
+                });
 
-                            Some(inferred_ty)
-                        },
-                    )
-                    .ok()?;
+                match solutions {
+                    // If the TCX type context is not compatible with the collection type
+                    // (e.g., a `list` literal where a `tuple` is expected), the CSA produces
+                    // an unsatisfiable result. In that case, we simply proceed without TCX
+                    // constraints rather than aborting the entire collection literal inference.
+                    Solutions::Unsatisfiable | Solutions::Unconstrained => {}
+                    Solutions::Constrained(solutions) => {
+                        for solution in &solutions {
+                            for binding in solution {
+                                // The SequentMap's transitivity reasoning can inject
+                                // cross-typevar references into the solution bounds.
+                                // For example, `_KT ≤ str ∧ str ≤ _VT` derives `_KT ≤ _VT`,
+                                // which adds `_KT` to `_VT`'s lower bound. Filter out any
+                                // inferable typevars from the solution, since they represent
+                                // cross-typevar relationships that are resolved independently.
+                                let inferred_ty = binding.solution.filter_union(db, |ty| {
+                                    !ty.as_typevar()
+                                        .is_some_and(|tv| tv.is_inferable(db, inferable))
+                                });
+
+                                // Avoid inferring a preferred type based on partially specialized
+                                // type context from an outer generic call. If the type context is
+                                // a union, we try to keep any concrete elements.
+                                let inferred_ty = inferred_ty
+                                    .filter_union(db, |ty| !ty.has_unspecialized_type_var(db));
+                                if inferred_ty.has_unspecialized_type_var(db) {
+                                    continue;
+                                }
+
+                                let identity = binding.bound_typevar.identity(db);
+                                elt_tcx_constraints
+                                    .entry(identity)
+                                    .and_modify(|existing| {
+                                        *existing = UnionType::from_two_elements(
+                                            db,
+                                            *existing,
+                                            inferred_ty,
+                                        );
+                                    })
+                                    .or_insert(inferred_ty);
+                            }
+                        }
+
+                        // Remove variance entries for typevars whose solutions were
+                        // filtered out (e.g., due to unspecialized typevars). Variance
+                        // should only be tracked for typevars with actual TCX constraints.
+                        elt_tcx_variance
+                            .retain(|identity, _| elt_tcx_constraints.contains_key(identity));
+                    }
+                }
             }
 
-            (builder.into_type_mappings(), elt_tcx_variance)
+            (elt_tcx_constraints, elt_tcx_variance)
         };
 
         // Create a set of constraints to infer a precise type for `T`.

From b1d0265f5779960bc60b358458853393f54f45f4 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Fri, 6 Mar 2026 10:36:18 -0500
Subject: [PATCH 05/20] [phase 4.2] migrate preferred_type_mappings to not use
 infer_reverse

---
 .../mdtest/assignment/annotations.md          |   3 +-
 .../ty_python_semantic/src/types/call/bind.rs | 127 +++++++++++++++---
 .../src/types/constraints.rs                  |  70 ++++++++--
 .../ty_python_semantic/src/types/generics.rs  |  48 +++++--
 4 files changed, 207 insertions(+), 41 deletions(-)

diff --git a/crates/ty_python_semantic/resources/mdtest/assignment/annotations.md b/crates/ty_python_semantic/resources/mdtest/assignment/annotations.md
index b9e37b651811b..18f185f351fb1 100644
--- a/crates/ty_python_semantic/resources/mdtest/assignment/annotations.md
+++ b/crates/ty_python_semantic/resources/mdtest/assignment/annotations.md
@@ -615,8 +615,7 @@ e: list[Any] | None = [1]
 reveal_type(e)  # revealed: list[Any]
 
 f: list[Any] | None = f2(1)
-# TODO: Better constraint solver.
-reveal_type(f)  # revealed: list[int] | None
+reveal_type(f)  # revealed: list[Any] | None
 
 g: list[Any] | dict[Any, Any] = f3(1)
 # TODO: Better constraint solver.
diff --git a/crates/ty_python_semantic/src/types/call/bind.rs b/crates/ty_python_semantic/src/types/call/bind.rs
index 082140412440e..5133131e777a2 100644
--- a/crates/ty_python_semantic/src/types/call/bind.rs
+++ b/crates/ty_python_semantic/src/types/call/bind.rs
@@ -27,7 +27,7 @@ use crate::place::{DefinedPlace, Definedness, Place, known_module_symbol};
 use crate::subscript::PyIndex;
 use crate::types::call::arguments::{Expansion, is_expandable_type};
 use crate::types::callable::CallableTypeKind;
-use crate::types::constraints::{ConstraintSet, ConstraintSetBuilder};
+use crate::types::constraints::{ConstraintSet, ConstraintSetBuilder, Solutions};
 use crate::types::diagnostic::{
     CALL_NON_CALLABLE, CALL_TOP_CALLABLE, CONFLICTING_ARGUMENT_FORMS, INVALID_ARGUMENT_TYPE,
     INVALID_DATACLASS, MISSING_ARGUMENT, NO_MATCHING_OVERLOAD, PARAMETER_ALREADY_ASSIGNED,
@@ -3732,43 +3732,134 @@ impl<'a, 'db> ArgumentTypeChecker<'a, 'db> {
         let mut partially_specialized_declared_type: FxHashSet<BoundTypeVarIdentity<'_>> =
             FxHashSet::default();
 
-        // Attempt to to solve the specialization while preferring the declared type of non-covariant
+        // Attempt to solve the specialization while preferring the declared type of non-covariant
         // type parameters from generic classes.
+        //
+        // We use a forward CSA check (`return_ty ≤ tcx`) to infer what each typevar in the
+        // function's return type maps to in the type context. For example, if the return type is
+        // `list[T]` and the type context is `list[int]`, the CSA produces `T ≤ int`, from which
+        // we extract the preferred type `int`.
+        //
+        // TODO: This two-phase approach (extract preferred types from TCX, then check argument
+        // compatibility) should eventually be replaced by conjoining the TCX constraint set
+        // directly with the argument constraint sets in the builder. The current solution-level
+        // filtering (variance, inferable typevars, concrete content) works around extracting
+        // solutions too early. When the builder maintains a single constraint set, the combined
+        // set `(return_ty ≤ tcx) ∧ (∧ᵢ actual_i ≤ formal_i)` would naturally resolve the tension
+        // between TCX preferences and argument constraints. If the combined set is unsatisfiable,
+        // we fall back to argument constraints alone (which the current code already does via
+        // `assignable_to_declared_type`).
         let preferred_type_mappings = return_with_tcx
             .and_then(|(return_ty, tcx)| {
                 tcx.filter_union(self.db, |ty| ty.class_specialization(self.db).is_some())
                     .class_specialization(self.db)?;
 
-                builder
-                    .infer_reverse_map(tcx, return_ty, |(identity, variance, inferred_ty)| {
+                let set = return_ty.when_constraint_set_assignable_to(
+                    self.db,
+                    tcx,
+                    constraints,
+                    self.inferable_typevars,
+                );
+
+                // Use `solutions_with` to determine per-typevar variance from the raw
+                // lower/upper bounds on each BDD path.
+                let mut variance_map: FxHashMap<BoundTypeVarIdentity<'_>, TypeVarVariance> =
+                    FxHashMap::default();
+                let solutions = set.solutions_with_inferable(
+                    self.db,
+                    constraints,
+                    self.inferable_typevars,
+                    |typevar, lower, upper| {
+                        let variance = if lower.is_never() {
+                            TypeVarVariance::Covariant
+                        } else if upper == Type::object() {
+                            TypeVarVariance::Contravariant
+                        } else {
+                            TypeVarVariance::Invariant
+                        };
+                        let identity = typevar.identity(self.db);
+                        variance_map
+                            .entry(identity)
+                            .and_modify(|current| *current = current.join(variance))
+                            .or_insert(variance);
+                        None // Use default solution selection
+                    },
+                );
+
+                let Solutions::Constrained(solutions) = solutions else {
+                    return None;
+                };
+
+                let mut preferred: FxHashMap<BoundTypeVarIdentity<'db>, Type<'db>> =
+                    FxHashMap::default();
+
+                for solution in &solutions {
+                    for binding in solution {
+                        let identity = binding.bound_typevar.identity(self.db);
+
                         // Avoid unnecessarily widening the return type based on a covariant
                         // type parameter from the type context, as it can lead to argument
                         // assignability errors if the type variable is constrained by a narrower
                         // parameter type.
-                        if variance.is_covariant() {
-                            return None;
+                        if variance_map
+                            .get(&identity)
+                            .is_some_and(|v| v.is_covariant())
+                        {
+                            continue;
                         }
 
-                        // Avoid inferring a preferred type based on partially specialized type context
-                        // from an outer generic call. If the type context is a union, we try to keep
-                        // any concrete elements.
-                        let inferred_ty = inferred_ty.filter_union(self.db, |ty| {
+                        // Filter out inferable typevars (cross-typevar references from
+                        // SequentMap transitivity) and unspecialized typevars (from partially
+                        // specialized contexts).
+                        let inferred_ty = binding.solution.filter_union(self.db, |ty| {
+                            if ty
+                                .as_typevar()
+                                .is_some_and(|tv| tv.is_inferable(self.db, self.inferable_typevars))
+                            {
+                                return false;
+                            }
                             if ty.has_unspecialized_type_var(self.db) {
                                 partially_specialized_declared_type.insert(identity);
-                                false
-                            } else {
-                                true
+                                return false;
                             }
+                            true
                         });
                         if inferred_ty.has_unspecialized_type_var(self.db) {
-                            return None;
+                            continue;
                         }
 
-                        Some(inferred_ty)
-                    })
-                    .ok()?;
+                        // Skip preferred types where every non-TypeVar union element still
+                        // deeply contains non-inferable typevars. Such types (e.g.,
+                        // `T@h | list[T@h]` from an outer generic scope) don't provide
+                        // useful concrete information and would cause over-expansion.
+                        let concrete_content =
+                            inferred_ty.filter_union(self.db, |ty| !ty.has_typevar(self.db));
+                        if concrete_content.is_never() && inferred_ty.has_typevar(self.db) {
+                            continue;
+                        }
+
+                        preferred
+                            .entry(identity)
+                            .and_modify(|existing| {
+                                *existing =
+                                    UnionType::from_two_elements(self.db, *existing, inferred_ty);
+                            })
+                            .or_insert(inferred_ty);
+                    }
+                }
+
+                // Add preferred types to the builder so they serve as the base mapping
+                // when argument inference adds more types.
+                for solution in &solutions {
+                    for binding in solution {
+                        let identity = binding.bound_typevar.identity(self.db);
+                        if let Some(&ty) = preferred.get(&identity) {
+                            builder.insert_type_mapping(binding.bound_typevar, ty);
+                        }
+                    }
+                }
 
-                Some(builder.type_mappings().clone())
+                Some(preferred)
             })
             .unwrap_or_default();
 
diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 2ad7c7a3ee1f8..6f9671489ce53 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -337,6 +337,14 @@ impl<'db, 'c> ConstraintSet<'db, 'c> {
     /// neither bound _is_ a typevar. And it's not something we can create a specialization from,
     /// since we would endlessly substitute until we stack overflow.
     pub(crate) fn is_cyclic(self, db: &'db dyn Db) -> bool {
+        self.is_cyclic_impl(db, None)
+    }
+
+    fn is_cyclic_impl(
+        self,
+        db: &'db dyn Db,
+        inferable: Option<InferableTypeVars<'_, 'db>>,
+    ) -> bool {
         #[derive(Default)]
         struct CollectReachability<'db> {
             reachable_typevars: RefCell<FxHashSet<BoundTypeVarIdentity<'db>>>,
@@ -403,21 +411,33 @@ impl<'db, 'c> ConstraintSet<'db, 'c> {
             false
         }
 
-        // First find all of the typevars that each constraint directly mentions.
+        // First find all of the typevars that each constraint directly mentions. When `inferable`
+        // is provided, only include inferable typevars as sources and targets in the graph.
         let mut reachable_typevars: FxHashMap<
             BoundTypeVarIdentity<'db>,
             FxHashSet<BoundTypeVarIdentity<'db>>,
         > = FxHashMap::default();
         self.node
             .for_each_constraint(self.builder, &mut |constraint, _| {
-                let visitor = CollectReachability::default();
                 let constraint = self.builder.constraint_data(constraint);
+                let identity = constraint.typevar.identity(db);
+                if inferable.is_some_and(|inferable| !identity.is_inferable(inferable)) {
+                    return;
+                }
+                let visitor = CollectReachability::default();
                 visitor.visit_type(db, constraint.lower);
                 visitor.visit_type(db, constraint.upper);
-                reachable_typevars
-                    .entry(constraint.typevar.identity(db))
-                    .or_default()
-                    .extend(visitor.reachable_typevars.into_inner());
+                let reachable = visitor.reachable_typevars.into_inner();
+                let entry = reachable_typevars.entry(identity).or_default();
+                if let Some(inferable) = inferable {
+                    entry.extend(
+                        reachable
+                            .into_iter()
+                            .filter(|tv| tv.is_inferable(inferable)),
+                    );
+                } else {
+                    entry.extend(reachable);
+                }
             });
 
         // Then perform a depth-first search to see if there are any cycles.
@@ -626,14 +646,37 @@ impl<'db, 'c> ConstraintSet<'db, 'c> {
         db: &'db dyn Db,
         builder: &'c ConstraintSetBuilder<'db>,
         choose: impl FnMut(BoundTypeVarInstance<'db>, Type<'db>, Type<'db>) -> Option<Type<'db>>,
+    ) -> Solutions<Vec<Solution<'db>>> {
+        self.solutions_with_impl(db, builder, None, choose)
+    }
+
+    /// Like [`solutions_with`][Self::solutions_with], but only considers cycles among inferable
+    /// typevars. Non-inferable typevars (e.g., from outer scopes that appear due to BDD
+    /// constraint reordering) are skipped during both cycle detection and solution extraction.
+    pub(crate) fn solutions_with_inferable(
+        self,
+        db: &'db dyn Db,
+        builder: &'c ConstraintSetBuilder<'db>,
+        inferable: InferableTypeVars<'_, 'db>,
+        choose: impl FnMut(BoundTypeVarInstance<'db>, Type<'db>, Type<'db>) -> Option<Type<'db>>,
+    ) -> Solutions<Vec<Solution<'db>>> {
+        self.solutions_with_impl(db, builder, Some(inferable), choose)
+    }
+
+    fn solutions_with_impl(
+        self,
+        db: &'db dyn Db,
+        builder: &'c ConstraintSetBuilder<'db>,
+        inferable: Option<InferableTypeVars<'_, 'db>>,
+        choose: impl FnMut(BoundTypeVarInstance<'db>, Type<'db>, Type<'db>) -> Option<Type<'db>>,
     ) -> Solutions<Vec<Solution<'db>>> {
         self.verify_builder(builder);
 
-        if self.is_cyclic(db) {
+        if self.is_cyclic_impl(db, inferable) {
             return Solutions::Unsatisfiable;
         }
 
-        self.node.solutions_with(db, builder, choose)
+        self.node.solutions_with(db, builder, inferable, choose)
     }
 
     #[expect(dead_code)] // Keep this around for debugging purposes
@@ -1763,12 +1806,13 @@ impl NodeId {
         self,
         db: &'db dyn Db,
         builder: &ConstraintSetBuilder<'db>,
+        inferable: Option<InferableTypeVars<'_, 'db>>,
         choose: impl FnMut(BoundTypeVarInstance<'db>, Type<'db>, Type<'db>) -> Option<Type<'db>>,
     ) -> Solutions<Vec<Solution<'db>>> {
         match self.node() {
             Node::AlwaysTrue => Solutions::Unconstrained,
             Node::AlwaysFalse => Solutions::Unsatisfiable,
-            Node::Interior(interior) => interior.solutions_with(db, builder, choose),
+            Node::Interior(interior) => interior.solutions_with(db, builder, inferable, choose),
         }
     }
 
@@ -3419,10 +3463,18 @@ impl InteriorNode {
         self,
         db: &'db dyn Db,
         builder: &ConstraintSetBuilder<'db>,
+        inferable: Option<InferableTypeVars<'_, 'db>>,
         mut choose: impl FnMut(BoundTypeVarInstance<'db>, Type<'db>, Type<'db>) -> Option<Type<'db>>,
     ) -> Solutions<Vec<Solution<'db>>> {
         let path_bounds = compute_path_bounds(db, builder, self.node());
         let solutions = solve_paths(db, &path_bounds, |db, bound_typevar, lower, upper| {
+            // When filtering by inferable typevars, skip non-inferable ones — they appear
+            // due to BDD constraint reordering and should not be solved.
+            if let Some(inferable) = inferable {
+                if !bound_typevar.is_inferable(db, inferable) {
+                    return Ok(None);
+                }
+            }
             if let Some(ty) = choose(bound_typevar, lower, upper) {
                 return Ok(Some(TypeVarSolution {
                     bound_typevar,
diff --git a/crates/ty_python_semantic/src/types/generics.rs b/crates/ty_python_semantic/src/types/generics.rs
index d97a4fd7af748..54244432a4686 100644
--- a/crates/ty_python_semantic/src/types/generics.rs
+++ b/crates/ty_python_semantic/src/types/generics.rs
@@ -218,19 +218,25 @@ pub(crate) enum InferableTypeVars<'a, 'db> {
     ),
 }
 
+impl<'db> BoundTypeVarIdentity<'db> {
+    pub(crate) fn is_inferable(self, inferable: InferableTypeVars<'_, 'db>) -> bool {
+        match inferable {
+            InferableTypeVars::None => false,
+            InferableTypeVars::One(typevars) => typevars.contains(&self),
+            InferableTypeVars::Two(left, right) => {
+                self.is_inferable(*left) || self.is_inferable(*right)
+            }
+        }
+    }
+}
+
 impl<'db> BoundTypeVarInstance<'db> {
     pub(crate) fn is_inferable(
         self,
         db: &'db dyn Db,
         inferable: InferableTypeVars<'_, 'db>,
     ) -> bool {
-        match inferable {
-            InferableTypeVars::None => false,
-            InferableTypeVars::One(typevars) => typevars.contains(&self.identity(db)),
-            InferableTypeVars::Two(left, right) => {
-                self.is_inferable(db, *left) || self.is_inferable(db, *right)
-            }
-        }
+        self.identity(db).is_inferable(inferable)
     }
 }
 
@@ -1664,11 +1670,6 @@ impl<'db, 'c> SpecializationBuilder<'db, 'c> {
         }
     }
 
-    /// Returns the current set of type mappings for this specialization.
-    pub(crate) fn type_mappings(&self) -> &FxHashMap<BoundTypeVarIdentity<'db>, Type<'db>> {
-        &self.types
-    }
-
     /// Returns the current set of type mappings for this specialization.
     pub(crate) fn into_type_mappings(self) -> FxHashMap<BoundTypeVarIdentity<'db>, Type<'db>> {
         self.types
@@ -1747,6 +1748,29 @@ impl<'db, 'c> SpecializationBuilder<'db, 'c> {
         generic_context.specialize_recursive(self.db, types)
     }
 
+    /// Insert a type mapping for a bound typevar.
+    ///
+    /// If a mapping already exists for this typevar, the new type is unioned with the existing
+    /// one.
+    pub(crate) fn insert_type_mapping(
+        &mut self,
+        bound_typevar: BoundTypeVarInstance<'db>,
+        ty: Type<'db>,
+    ) {
+        let identity = bound_typevar.identity(self.db);
+        match self.types.entry(identity) {
+            Entry::Occupied(mut entry) => {
+                if bound_typevar.is_paramspec(self.db) {
+                    return;
+                }
+                *entry.get_mut() = UnionType::from_two_elements(self.db, *entry.get(), ty);
+            }
+            Entry::Vacant(entry) => {
+                entry.insert(ty);
+            }
+        }
+    }
+
     fn add_type_mapping(
         &mut self,
         bound_typevar: BoundTypeVarInstance<'db>,

From 715c2793952ea765a95381a148adffe49d06a7e7 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Fri, 6 Mar 2026 17:55:57 -0500
Subject: [PATCH 06/20] [phase 4] update remaining infer_reverse calls

---
 crates/ty_python_semantic/src/types.rs        |  18 +-
 .../ty_python_semantic/src/types/generics.rs  | 170 ++----------------
 .../src/types/infer/builder.rs                |   2 +-
 .../src/types/known_instance.rs               |   1 -
 .../ty_python_semantic/src/types/typevar.rs   |   3 +-
 5 files changed, 17 insertions(+), 177 deletions(-)

diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs
index c7d4c7eed391d..4cdbb0c726e42 100644
--- a/crates/ty_python_semantic/src/types.rs
+++ b/crates/ty_python_semantic/src/types.rs
@@ -4,7 +4,6 @@ use ruff_diagnostics::{Edit, Fix};
 use rustc_hash::FxHashMap;
 
 use std::borrow::Cow;
-use std::cell::RefCell;
 use std::time::Duration;
 
 use bitflags::bitflags;
@@ -5402,12 +5401,6 @@ impl<'db> Type<'db> {
                     match type_mapping {
                         TypeMapping::EagerExpansion => unreachable!("handled above"),
 
-                        // For UniqueSpecialization, get raw value type, apply specialization, then apply mapping.
-                        TypeMapping::UniqueSpecialization { .. } => {
-                            let value_type = alias.raw_value_type(db);
-                            alias.apply_function_specialization(db, value_type).apply_type_mapping_impl(db, type_mapping, tcx, visitor)
-                        }
-
                         _ => {
                             let value_type = alias.raw_value_type(db).apply_type_mapping_impl(db, type_mapping, tcx, visitor);
                             alias.apply_function_specialization(db, value_type).apply_type_mapping_impl(db, type_mapping, tcx, visitor)
@@ -5432,7 +5425,6 @@ impl<'db> Type<'db> {
             Type::LiteralValue(_) => match type_mapping {
                 TypeMapping::ApplySpecialization(_) |
                 TypeMapping::ApplySpecializationWithMaterialization { .. } |
-                TypeMapping::UniqueSpecialization { .. } |
                 TypeMapping::BindLegacyTypevars(_) |
                 TypeMapping::BindSelf { .. } |
                 TypeMapping::ReplaceSelf { .. } |
@@ -5448,7 +5440,6 @@ impl<'db> Type<'db> {
             Type::Dynamic(_) => match type_mapping {
                 TypeMapping::ApplySpecialization(_) |
                 TypeMapping::ApplySpecializationWithMaterialization { .. } |
-                TypeMapping::UniqueSpecialization { .. } |
                 TypeMapping::BindLegacyTypevars(_) |
                 TypeMapping::BindSelf(..) |
                 TypeMapping::ReplaceSelf { .. } |
@@ -6229,11 +6220,6 @@ pub enum TypeMapping<'a, 'db> {
         specialization: ApplySpecialization<'a, 'db>,
         materialization_kind: MaterializationKind,
     },
-    /// Resets any specializations to contain unique synthetic type variables.
-    UniqueSpecialization {
-        // A list of synthetic type variables, and the types they replaced.
-        specialization: RefCell<Vec<(BoundTypeVarInstance<'db>, Type<'db>)>>,
-    },
     /// Replaces any literal types with their corresponding promoted type form (e.g. `Literal["string"]`
     /// to `str`, or `def _() -> int` to `Callable[[], int]`).
     Promote(PromotionMode, PromotionKind),
@@ -6285,8 +6271,7 @@ impl<'db> TypeMapping<'_, 'db> {
                     }),
                 )
             }
-            TypeMapping::UniqueSpecialization { .. }
-            | TypeMapping::Promote(..)
+            TypeMapping::Promote(..)
             | TypeMapping::BindLegacyTypevars(_)
             | TypeMapping::Materialize(_)
             | TypeMapping::ReplaceParameterDefaults
@@ -6331,7 +6316,6 @@ impl<'db> TypeMapping<'_, 'db> {
             },
             TypeMapping::Promote(mode, kind) => TypeMapping::Promote(mode.flip(), *kind),
             TypeMapping::ApplySpecialization(_)
-            | TypeMapping::UniqueSpecialization { .. }
             | TypeMapping::BindLegacyTypevars(_)
             | TypeMapping::BindSelf(..)
             | TypeMapping::ReplaceSelf { .. }
diff --git a/crates/ty_python_semantic/src/types/generics.rs b/crates/ty_python_semantic/src/types/generics.rs
index 54244432a4686..165b7529f3f2e 100644
--- a/crates/ty_python_semantic/src/types/generics.rs
+++ b/crates/ty_python_semantic/src/types/generics.rs
@@ -5,7 +5,6 @@ use std::fmt::Display;
 
 use itertools::{Either, Itertools};
 use ruff_python_ast as ast;
-use ruff_python_ast::name::Name;
 use rustc_hash::{FxHashMap, FxHashSet};
 
 use crate::node_key::NodeKey;
@@ -1105,39 +1104,20 @@ impl<'db> Specialization<'db> {
             return self.materialize_impl(db, *materialization_kind, visitor);
         }
 
-        let types: Box<[_]> = if let TypeMapping::UniqueSpecialization { specialization } =
-            type_mapping
-        {
-            let mut specialization = specialization.borrow_mut();
-
-            self.types(db)
-                .iter()
-                .zip(self.generic_context(db).variables(db))
-                .map(|(ty, typevar)| {
-                    // Create a unique synthetic type variable.
-                    let name = format!("_T{}", specialization.len());
-                    let synthetic =
-                        BoundTypeVarInstance::synthetic(db, Name::new(name), typevar.variance(db));
-
-                    specialization.push((synthetic, *ty));
-                    Type::TypeVar(synthetic)
-                })
-                .collect()
-        } else {
-            self.types(db)
-                .iter()
-                .zip(self.generic_context(db).variables(db))
-                .enumerate()
-                .map(|(i, (ty, typevar))| {
-                    let tcx = TypeContext::new(tcx.get(i).copied());
-                    if typevar.variance(db).is_covariant() {
-                        ty.apply_type_mapping_impl(db, type_mapping, tcx, visitor)
-                    } else {
-                        ty.apply_type_mapping_impl(db, &type_mapping.flip(), tcx, visitor)
-                    }
-                })
-                .collect()
-        };
+        let types: Box<[_]> = self
+            .types(db)
+            .iter()
+            .zip(self.generic_context(db).variables(db))
+            .enumerate()
+            .map(|(i, (ty, typevar))| {
+                let tcx = TypeContext::new(tcx.get(i).copied());
+                if typevar.variance(db).is_covariant() {
+                    ty.apply_type_mapping_impl(db, type_mapping, tcx, visitor)
+                } else {
+                    ty.apply_type_mapping_impl(db, &type_mapping.flip(), tcx, visitor)
+                }
+            })
+            .collect();
 
         let tuple_inner = self.tuple_inner(db).and_then(|tuple| {
             tuple.apply_type_mapping_impl(db, type_mapping, TypeContext::default(), visitor)
@@ -1670,32 +1650,6 @@ impl<'db, 'c> SpecializationBuilder<'db, 'c> {
         }
     }
 
-    /// Returns the current set of type mappings for this specialization.
-    pub(crate) fn into_type_mappings(self) -> FxHashMap<BoundTypeVarIdentity<'db>, Type<'db>> {
-        self.types
-    }
-
-    #[expect(dead_code)] // Will be removed in Phase 4
-    pub(crate) fn with_default(
-        &self,
-        generic_context: GenericContext<'db>,
-        default_ty: impl Fn(BoundTypeVarInstance<'db>) -> Type<'db>,
-    ) -> Self {
-        let mut types = self.types.clone();
-        for (identity, variable) in generic_context.variables_inner(self.db) {
-            if let Entry::Vacant(entry) = types.entry(*identity) {
-                entry.insert(default_ty(*variable));
-            }
-        }
-
-        Self {
-            db: self.db,
-            constraints: self.constraints,
-            inferable: self.inferable,
-            types,
-        }
-    }
-
     /// Apply a transformation to all accumulated type variable assignments.
     pub(crate) fn map_types(&mut self, mut f: impl FnMut(Type<'db>) -> Type<'db>) {
         for ty in self.types.values_mut() {
@@ -2423,102 +2377,6 @@ impl<'db, 'c> SpecializationBuilder<'db, 'c> {
 
         Ok(())
     }
-
-    /// Infer type mappings for the specialization in the reverse direction, i.e., where the
-    /// actual type, not the formal type, contains inferable type variables.
-    #[expect(dead_code)] // Will be removed in Phase 4
-    pub(crate) fn infer_reverse(
-        &mut self,
-        formal: Type<'db>,
-        actual: Type<'db>,
-    ) -> Result<(), SpecializationError<'db>> {
-        self.infer_reverse_map(formal, actual, |(_, _, ty)| Some(ty))
-    }
-
-    /// Infer type mappings for the specialization in the reverse direction, i.e., where the
-    /// actual type, not the formal type, contains inferable type variables.
-    ///
-    /// The provided function will be called before any type mappings are created, and can
-    /// optionally modify the inferred type, or filter out the type mapping entirely.
-    pub(crate) fn infer_reverse_map(
-        &mut self,
-        formal: Type<'db>,
-        actual: Type<'db>,
-        mut f: impl FnMut(TypeVarAssignment<'db>) -> Option<Type<'db>>,
-    ) -> Result<(), SpecializationError<'db>> {
-        self.infer_reverse_map_impl(
-            formal,
-            actual,
-            TypeVarVariance::Covariant,
-            &mut f,
-            &mut FxHashSet::default(),
-        )
-    }
-
-    fn infer_reverse_map_impl(
-        &mut self,
-        formal: Type<'db>,
-        actual: Type<'db>,
-        polarity: TypeVarVariance,
-        f: &mut dyn FnMut(TypeVarAssignment<'db>) -> Option<Type<'db>>,
-        seen: &mut FxHashSet<(Type<'db>, Type<'db>)>,
-    ) -> Result<(), SpecializationError<'db>> {
-        // Avoid infinite recursion
-        if !seen.insert((formal, actual)) {
-            return Ok(());
-        }
-
-        // Assign each type variable on the formal type to a unique synthetic type variable.
-        let type_mapping = TypeMapping::UniqueSpecialization {
-            specialization: RefCell::new(Vec::new()),
-        };
-        let synthetic_formal =
-            formal.apply_type_mapping(self.db, &type_mapping, TypeContext::default());
-
-        // Recover the synthetic type variables.
-        let synthetic_specialization = match type_mapping {
-            TypeMapping::UniqueSpecialization { specialization } => specialization.into_inner(),
-            _ => unreachable!(),
-        };
-
-        let inferable = GenericContext::from_typevar_instances(
-            self.db,
-            synthetic_specialization.iter().map(|(typevar, _)| *typevar),
-        )
-        .inferable_typevars(self.db);
-
-        // Collect the actual type to which each synthetic type variable is mapped.
-        let forward_type_mappings = {
-            let mut builder = SpecializationBuilder::new(self.db, self.constraints, inferable);
-            builder.infer(synthetic_formal, actual)?;
-            builder.into_type_mappings()
-        };
-
-        // If there are no forward type mappings, try the other direction.
-        //
-        // This is the base case for when `actual` is an inferable type variable.
-        if forward_type_mappings.is_empty() {
-            return self.infer_map_impl(actual, formal, polarity, f, seen);
-        }
-
-        // Consider the reverse inference of `Sequence[int]` given `list[T]`.
-        //
-        // Given a forward type mapping of `T@Sequence` -> `T@list`, and a synthetic type mapping of
-        // `T@Sequence` -> `int`, we want to infer the reverse type mapping `T@list` -> `int`.
-        for (synthetic_type_var, formal_type) in synthetic_specialization {
-            if let Some(actual_type) =
-                forward_type_mappings.get(&synthetic_type_var.identity(self.db))
-            {
-                let variance = synthetic_type_var.variance_with_polarity(self.db, polarity);
-
-                // Note that it is possible that we need to recurse deeper, so we continue
-                // to perform a reverse inference on the nested types.
-                self.infer_reverse_map_impl(formal_type, *actual_type, variance, f, seen)?;
-            }
-        }
-
-        Ok(())
-    }
 }
 
 #[derive(Clone, Debug, Eq, PartialEq)]
diff --git a/crates/ty_python_semantic/src/types/infer/builder.rs b/crates/ty_python_semantic/src/types/infer/builder.rs
index 46cc2cfd49816..9d2a67d43c178 100644
--- a/crates/ty_python_semantic/src/types/infer/builder.rs
+++ b/crates/ty_python_semantic/src/types/infer/builder.rs
@@ -6196,7 +6196,7 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
             // our inference is compatible with subsequent additions to the collection), but it
             // matches the behavior of other type checkers and is usually the desired behavior.
             if let Some(elt_tcx) = elt_tcx {
-                builder.infer(Type::TypeVar(elt_ty), elt_tcx).ok()?;
+                builder.insert_type_mapping(elt_ty, elt_tcx);
             }
         }
 
diff --git a/crates/ty_python_semantic/src/types/known_instance.rs b/crates/ty_python_semantic/src/types/known_instance.rs
index 8ecee6c599d96..29ae40a70ee67 100644
--- a/crates/ty_python_semantic/src/types/known_instance.rs
+++ b/crates/ty_python_semantic/src/types/known_instance.rs
@@ -284,7 +284,6 @@ impl<'db> KnownInstanceType<'db> {
                 ),
                 TypeMapping::ApplySpecialization(_)
                 | TypeMapping::ApplySpecializationWithMaterialization { .. }
-                | TypeMapping::UniqueSpecialization { .. }
                 | TypeMapping::Promote(..)
                 | TypeMapping::BindSelf(..)
                 | TypeMapping::ReplaceSelf { .. }
diff --git a/crates/ty_python_semantic/src/types/typevar.rs b/crates/ty_python_semantic/src/types/typevar.rs
index 5f3e9fee7d727..e02b52e8e4dc9 100644
--- a/crates/ty_python_semantic/src/types/typevar.rs
+++ b/crates/ty_python_semantic/src/types/typevar.rs
@@ -903,8 +903,7 @@ impl<'db> BoundTypeVarInstance<'db> {
                     Type::TypeVar(self)
                 }
             }
-            TypeMapping::UniqueSpecialization { .. }
-            | TypeMapping::Promote(..)
+            TypeMapping::Promote(..)
             | TypeMapping::ReplaceParameterDefaults
             | TypeMapping::BindLegacyTypevars(_)
             | TypeMapping::EagerExpansion

From f93d643ed67b05cc8300d2bd2f3bcb18391cd942 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Mon, 9 Mar 2026 21:11:00 -0400
Subject: [PATCH 07/20] clean up comments

---
 .../ty_python_semantic/src/types/call/bind.rs | 27 +++++++-------
 .../src/types/infer/builder.rs                | 37 ++++++++++---------
 2 files changed, 33 insertions(+), 31 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/call/bind.rs b/crates/ty_python_semantic/src/types/call/bind.rs
index 5133131e777a2..a07e4fab65ada 100644
--- a/crates/ty_python_semantic/src/types/call/bind.rs
+++ b/crates/ty_python_semantic/src/types/call/bind.rs
@@ -3735,20 +3735,21 @@ impl<'a, 'db> ArgumentTypeChecker<'a, 'db> {
         // Attempt to solve the specialization while preferring the declared type of non-covariant
         // type parameters from generic classes.
         //
-        // We use a forward CSA check (`return_ty ≤ tcx`) to infer what each typevar in the
-        // function's return type maps to in the type context. For example, if the return type is
-        // `list[T]` and the type context is `list[int]`, the CSA produces `T ≤ int`, from which
-        // we extract the preferred type `int`.
+        // We use a forward assignability check (`return_ty ≤ tcx`) to infer what each typevar in
+        // the function's return type maps to in the type context. (We use _constraint set_
+        // assignability so that we get a constraint set describing the typevars.) For example, if
+        // the return type is `list[T]` and the type context is `list[int]`, the check produces
+        // `T ≤ int`, from which we extract the preferred type `int`.
         //
-        // TODO: This two-phase approach (extract preferred types from TCX, then check argument
-        // compatibility) should eventually be replaced by conjoining the TCX constraint set
-        // directly with the argument constraint sets in the builder. The current solution-level
-        // filtering (variance, inferable typevars, concrete content) works around extracting
-        // solutions too early. When the builder maintains a single constraint set, the combined
-        // set `(return_ty ≤ tcx) ∧ (∧ᵢ actual_i ≤ formal_i)` would naturally resolve the tension
-        // between TCX preferences and argument constraints. If the combined set is unsatisfiable,
-        // we fall back to argument constraints alone (which the current code already does via
-        // `assignable_to_declared_type`).
+        // TODO: This two-phase approach (extract preferred types from the type context, then check
+        // argument compatibility) should eventually be replaced by conjoining the type context
+        // constraint set directly with the argument constraint sets in the builder. The current
+        // solution-level filtering (variance, inferable typevars, concrete content) works around
+        // extracting solutions too early. When the builder maintains a single constraint set, the
+        // combined set `(return_ty ≤ tcx) ∧ (∧ᵢ actual_i ≤ formal_i)` will naturally resolve the
+        // tension between type context preferences and argument constraints. If the combined set
+        // is unsatisfiable, we will fall back to argument constraints alone (which the current
+        // code does via `assignable_to_declared_type`).
         let preferred_type_mappings = return_with_tcx
             .and_then(|(return_ty, tcx)| {
                 tcx.filter_union(self.db, |ty| ty.class_specialization(self.db).is_some())
diff --git a/crates/ty_python_semantic/src/types/infer/builder.rs b/crates/ty_python_semantic/src/types/infer/builder.rs
index 9d2a67d43c178..9ff822084f416 100644
--- a/crates/ty_python_semantic/src/types/infer/builder.rs
+++ b/crates/ty_python_semantic/src/types/infer/builder.rs
@@ -5172,9 +5172,9 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
                 // If this is a generic call, attempt to specialize the parameter type using the
                 // declared type context, if provided.
                 if let Some(generic_context) = overload.signature.generic_context {
-                    // Use a forward CSA check to infer typevar specializations from the
-                    // declared type context. For example, if the return type is `list[T]`
-                    // and the declared type context is `list[int]`, CSA produces `T = int`.
+                    // Use a forward assignability check to infer typevar specializations from the
+                    // declared type context. For example, if the return type is `list[T]` and the
+                    // declared type context is `list[int]`, the check produces `T = int`.
                     let mut tcx_mappings = FxHashMap::default();
                     if let Some(declared_return_ty) = call_expression_tcx.annotation {
                         let return_ty = overload
@@ -6061,15 +6061,15 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
 
         // Collect type constraints from the declared element types.
         //
-        // We use a forward CSA check (`collection_instance ≤ tcx`) to infer what each
-        // typevar maps to in the type context. For example, if `tcx = list[int]` and
-        // `collection_instance = list[T]`, the CSA produces `T = int`.
+        // We use a forward assignability check (`collection_instance ≤ tcx`) to infer what each
+        // typevar maps to in the type context. For example, if the type context is `list[int]` and
+        // `collection_instance` is `list[T]`, the check produces `T = int`.
         //
-        // Variance is determined from the constraint bounds: a constraint with only an
-        // upper bound (`lower = Never`) indicates a covariant position, while a constraint
-        // with only a lower bound (`upper = object`) indicates contravariant. This correctly
-        // handles cases where the TCX type is a covariant superclass of the collection
-        // (e.g., `Sequence[Any]` as TCX for `list[T]`).
+        // Variance is determined from the constraint bounds: a constraint with only an upper bound
+        // (`lower = Never`) indicates a covariant position, while a constraint with only a lower
+        // bound (`upper = object`) indicates contravariant. This correctly handles cases where the
+        // type context is a covariant superclass of the collection (e.g., `Sequence[Any]` as type
+        // context for `list[T]`).
         let (elt_tcx_constraints, elt_tcx_variance) = {
             let mut elt_tcx_constraints: FxHashMap<BoundTypeVarIdentity<'_>, Type<'db>> =
                 FxHashMap::default();
@@ -6112,10 +6112,11 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
                 });
 
                 match solutions {
-                    // If the TCX type context is not compatible with the collection type
-                    // (e.g., a `list` literal where a `tuple` is expected), the CSA produces
-                    // an unsatisfiable result. In that case, we simply proceed without TCX
-                    // constraints rather than aborting the entire collection literal inference.
+                    // If the type context is not compatible with the collection type (e.g., a
+                    // `list` literal where a `tuple` is expected), the assignability check
+                    // produces an unsatisfiable result. In that case, we simply proceed without
+                    // type context constraints rather than aborting the entire collection literal
+                    // inference.
                     Solutions::Unsatisfiable | Solutions::Unconstrained => {}
                     Solutions::Constrained(solutions) => {
                         for solution in &solutions {
@@ -6154,9 +6155,9 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
                             }
                         }
 
-                        // Remove variance entries for typevars whose solutions were
-                        // filtered out (e.g., due to unspecialized typevars). Variance
-                        // should only be tracked for typevars with actual TCX constraints.
+                        // Remove variance entries for typevars whose solutions were filtered out
+                        // (e.g., due to unspecialized typevars). Variance should only be tracked
+                        // for typevars with actual type context constraints.
                         elt_tcx_variance
                             .retain(|identity, _| elt_tcx_constraints.contains_key(identity));
                     }

From bd9efd39bcb3bd8f1c057855d1aa2d350f5dc6f9 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Mon, 9 Mar 2026 21:16:15 -0400
Subject: [PATCH 08/20] remove some redundancy

---
 .../ty_python_semantic/src/types/generics.rs  | 27 ++++++-------------
 1 file changed, 8 insertions(+), 19 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/generics.rs b/crates/ty_python_semantic/src/types/generics.rs
index 165b7529f3f2e..a4c90a244e52b 100644
--- a/crates/ty_python_semantic/src/types/generics.rs
+++ b/crates/ty_python_semantic/src/types/generics.rs
@@ -1714,9 +1714,16 @@ impl<'db, 'c> SpecializationBuilder<'db, 'c> {
         let identity = bound_typevar.identity(self.db);
         match self.types.entry(identity) {
             Entry::Occupied(mut entry) => {
+                // TODO: The spec says that when a ParamSpec is used multiple times in a signature,
+                // the type checker can solve it to a common behavioral supertype. We don't
+                // implement that yet so in case there are multiple ParamSpecs, use the
+                // specialization from the first occurrence.
+                // https://github.com/astral-sh/ty/issues/1778
+                // https://github.com/astral-sh/ruff/pull/21445#discussion_r2591510145
                 if bound_typevar.is_paramspec(self.db) {
                     return;
                 }
+
                 *entry.get_mut() = UnionType::from_two_elements(self.db, *entry.get(), ty);
             }
             Entry::Vacant(entry) => {
@@ -1736,25 +1743,7 @@ impl<'db, 'c> SpecializationBuilder<'db, 'c> {
         let Some(ty) = f((identity, variance, ty)) else {
             return;
         };
-
-        match self.types.entry(identity) {
-            Entry::Occupied(mut entry) => {
-                // TODO: The spec says that when a ParamSpec is used multiple times in a signature,
-                // the type checker can solve it to a common behavioral supertype. We don't
-                // implement that yet so in case there are multiple ParamSpecs, use the
-                // specialization from the first occurrence.
-                // https://github.com/astral-sh/ty/issues/1778
-                // https://github.com/astral-sh/ruff/pull/21445#discussion_r2591510145
-                if bound_typevar.is_paramspec(self.db) {
-                    return;
-                }
-
-                *entry.get_mut() = UnionType::from_two_elements(self.db, *entry.get(), ty);
-            }
-            Entry::Vacant(entry) => {
-                entry.insert(ty);
-            }
-        }
+        self.insert_type_mapping(bound_typevar, ty);
     }
 
     /// Finds all of the valid specializations of a constraint set, and adds their type mappings to

From 2ba73734fe7871ed6014609eaeeeef03d9b0b0b6 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Tue, 10 Mar 2026 12:16:23 -0400
Subject: [PATCH 09/20] use inferable variant

---
 .../src/types/constraints.rs                  | 36 +++----------
 .../src/types/infer/builder.rs                | 53 +++++++++++--------
 2 files changed, 40 insertions(+), 49 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 6f9671489ce53..4fcfbb71c4c5e 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -631,52 +631,32 @@ impl<'db, 'c> ConstraintSet<'db, 'c> {
 
     /// Computes solutions for each BDD path, using a caller-provided hook to select solutions.
     ///
+    /// We only consider cycles among inferable typevars. Non-inferable typevars (e.g., from outer
+    /// scopes that appear due to BDD constraint reordering) are skipped during both cycle
+    /// detection and solution extraction.
+    ///
     /// The `choose` hook is called for each typevar on each BDD path with the typevar's
     /// materialized lower and upper bounds. It returns:
     /// - `Some(ty)` to use `ty` as the solution for this typevar on this path
     /// - `None` to fall back to the default solution selection logic
     ///
     /// For multi-path BDDs, the hook is called per-path. The caller is responsible for combining
-    /// results across paths (typically via union), matching the behavior of
-    /// [`add_type_mappings_from_constraint_set`][super::generics::SpecializationBuilder::add_type_mappings_from_constraint_set].
-    ///
-    /// Returns owned solutions (not cached), since the hook makes results non-deterministic.
-    pub(crate) fn solutions_with(
-        self,
-        db: &'db dyn Db,
-        builder: &'c ConstraintSetBuilder<'db>,
-        choose: impl FnMut(BoundTypeVarInstance<'db>, Type<'db>, Type<'db>) -> Option<Type<'db>>,
-    ) -> Solutions<Vec<Solution<'db>>> {
-        self.solutions_with_impl(db, builder, None, choose)
-    }
-
-    /// Like [`solutions_with`][Self::solutions_with], but only considers cycles among inferable
-    /// typevars. Non-inferable typevars (e.g., from outer scopes that appear due to BDD
-    /// constraint reordering) are skipped during both cycle detection and solution extraction.
+    /// results across paths (typically via union).
     pub(crate) fn solutions_with_inferable(
         self,
         db: &'db dyn Db,
         builder: &'c ConstraintSetBuilder<'db>,
         inferable: InferableTypeVars<'_, 'db>,
         choose: impl FnMut(BoundTypeVarInstance<'db>, Type<'db>, Type<'db>) -> Option<Type<'db>>,
-    ) -> Solutions<Vec<Solution<'db>>> {
-        self.solutions_with_impl(db, builder, Some(inferable), choose)
-    }
-
-    fn solutions_with_impl(
-        self,
-        db: &'db dyn Db,
-        builder: &'c ConstraintSetBuilder<'db>,
-        inferable: Option<InferableTypeVars<'_, 'db>>,
-        choose: impl FnMut(BoundTypeVarInstance<'db>, Type<'db>, Type<'db>) -> Option<Type<'db>>,
     ) -> Solutions<Vec<Solution<'db>>> {
         self.verify_builder(builder);
 
-        if self.is_cyclic_impl(db, inferable) {
+        if self.is_cyclic_impl(db, Some(inferable)) {
             return Solutions::Unsatisfiable;
         }
 
-        self.node.solutions_with(db, builder, inferable, choose)
+        self.node
+            .solutions_with(db, builder, Some(inferable), choose)
     }
 
     #[expect(dead_code)] // Keep this around for debugging purposes
diff --git a/crates/ty_python_semantic/src/types/infer/builder.rs b/crates/ty_python_semantic/src/types/infer/builder.rs
index 9ff822084f416..30731d276c3e3 100644
--- a/crates/ty_python_semantic/src/types/infer/builder.rs
+++ b/crates/ty_python_semantic/src/types/infer/builder.rs
@@ -6089,27 +6089,38 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
                     inferable,
                 );
 
-                // Use `solutions_with` to capture per-typevar variance from the raw
-                // lower/upper bounds on each BDD path.
-                let solutions = set.solutions_with(db, &constraints, |typevar, lower, upper| {
-                    // Determine variance from the constraint bounds:
-                    // - Only upper bound (lower = Never) → covariant position
-                    // - Only lower bound (upper = object) → contravariant position
-                    // - Both bounds set → invariant position
-                    let variance = if lower.is_never() {
-                        TypeVarVariance::Covariant
-                    } else if upper == Type::object() {
-                        TypeVarVariance::Contravariant
-                    } else {
-                        TypeVarVariance::Invariant
-                    };
-                    let identity = typevar.identity(db);
-                    elt_tcx_variance
-                        .entry(identity)
-                        .and_modify(|current| *current = current.join(variance))
-                        .or_insert(variance);
-                    None // Use default solution selection
-                });
+                // Use `solutions_with_inferable` to capture per-typevar variance from the raw
+                // lower/upper bounds on each BDD path. We must use the inferable-aware variant so
+                // that non-inferable typevars from outer scopes (which the assignability check
+                // constrains alongside the collection's own typevars) are excluded from cycle
+                // detection and solution extraction. Without this, a type context like
+                // `list[T@MyClass]` would create mutual constraints between `_T` (list's typevar)
+                // and `T@MyClass`, which `is_cyclic` would flag as a cycle, returning
+                // `Unsatisfiable` and losing the type context information entirely.
+                let solutions = set.solutions_with_inferable(
+                    db,
+                    &constraints,
+                    inferable,
+                    |typevar, lower, upper| {
+                        // Determine variance from the constraint bounds:
+                        // - Only upper bound (lower = Never) → covariant position
+                        // - Only lower bound (upper = object) → contravariant position
+                        // - Both bounds set → invariant position
+                        let variance = if lower.is_never() {
+                            TypeVarVariance::Covariant
+                        } else if upper == Type::object() {
+                            TypeVarVariance::Contravariant
+                        } else {
+                            TypeVarVariance::Invariant
+                        };
+                        let identity = typevar.identity(db);
+                        elt_tcx_variance
+                            .entry(identity)
+                            .and_modify(|current| *current = current.join(variance))
+                            .or_insert(variance);
+                        None // Use default solution selection
+                    },
+                );
 
                 match solutions {
                     // If the type context is not compatible with the collection type (e.g., a

From fa57c421443d05b8a1c8b7c74a64da09ce4f6e29 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Mon, 16 Mar 2026 22:23:51 -0400
Subject: [PATCH 10/20] remove map_types

---
 crates/ty_python_semantic/src/types/generics.rs | 17 -----------------
 .../src/types/infer/builder.rs                  | 17 ++++++++++-------
 2 files changed, 10 insertions(+), 24 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/generics.rs b/crates/ty_python_semantic/src/types/generics.rs
index a4c90a244e52b..3818cd75ae3c5 100644
--- a/crates/ty_python_semantic/src/types/generics.rs
+++ b/crates/ty_python_semantic/src/types/generics.rs
@@ -1650,23 +1650,6 @@ impl<'db, 'c> SpecializationBuilder<'db, 'c> {
         }
     }
 
-    /// Apply a transformation to all accumulated type variable assignments.
-    pub(crate) fn map_types(&mut self, mut f: impl FnMut(Type<'db>) -> Type<'db>) {
-        for ty in self.types.values_mut() {
-            *ty = f(*ty);
-        }
-    }
-
-    pub(crate) fn build(&mut self, generic_context: GenericContext<'db>) -> Specialization<'db> {
-        let types = generic_context
-            .variables_inner(self.db)
-            .iter()
-            .map(|(identity, _)| self.types.get(identity).copied());
-
-        // TODO Infer the tuple spec for a tuple type
-        generic_context.specialize_recursive(self.db, types)
-    }
-
     /// Build a specialization, using a caller-provided hook to select the solution for each
     /// typevar.
     ///
diff --git a/crates/ty_python_semantic/src/types/infer/builder.rs b/crates/ty_python_semantic/src/types/infer/builder.rs
index 30731d276c3e3..4249abf09bc0c 100644
--- a/crates/ty_python_semantic/src/types/infer/builder.rs
+++ b/crates/ty_python_semantic/src/types/infer/builder.rs
@@ -6300,15 +6300,18 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
             }
         }
 
-        // Promote singleton types to `T | Unknown` in inferred type parameters,
-        // so that e.g. `[None]` is inferred as `list[None | Unknown]`.
-        if elt_tcx_constraints.is_empty() {
-            builder.map_types(|ty| ty.promote_singletons(self.db()));
-        }
-
         let class_type = collection_alias
             .origin(self.db())
-            .apply_specialization(self.db(), |_| builder.build(generic_context));
+            .apply_specialization(self.db(), |_| {
+                builder.build_with(generic_context, |_, lower, _| {
+                    // Promote singleton types to `T | Unknown` in inferred type parameters,
+                    // so that e.g. `[None]` is inferred as `list[None | Unknown]`.
+                    if elt_tcx_constraints.is_empty() {
+                        return Some(lower.promote_singletons(self.db()));
+                    }
+                    None
+                })
+            });
 
         Type::from(class_type).to_instance(self.db())
     }

From 83892d6c561a65e2758696846ab82d6fedfa8aa3 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Tue, 17 Mar 2026 10:02:47 -0400
Subject: [PATCH 11/20] fix numpy failure

---
 .../ty_python_semantic/src/types/infer/builder.rs   | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/crates/ty_python_semantic/src/types/infer/builder.rs b/crates/ty_python_semantic/src/types/infer/builder.rs
index 4249abf09bc0c..a9f31797e958d 100644
--- a/crates/ty_python_semantic/src/types/infer/builder.rs
+++ b/crates/ty_python_semantic/src/types/infer/builder.rs
@@ -6078,6 +6078,19 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
 
             if let Some(tcx) = tcx.annotation
                 && tcx.class_specialization(self.db()).is_some()
+                // Skip constraint extraction when the type context contains
+                // UnspecializedTypeVar placeholders (from partially-specialized
+                // parameter types during multi-inference for overloaded calls).
+                // The CSA would walk through protocol supertypes and produce
+                // constraints contaminated by the placeholder, which collapse to
+                // `Any` during solution extraction and bypass downstream filters.
+                //
+                // TODO: UnspecializedTypeVar should be removed entirely once the
+                // SpecializationBuilder uses constraint sets internally, at which
+                // point the typevars that it currently replaces can instead be
+                // existentially quantified away (as is already done for generic
+                // callable assignability in `check_signature_pair`).
+                && !tcx.has_unspecialized_type_var(self.db())
             {
                 let db = self.db();
                 let collection_instance = Type::instance(db, ClassType::Generic(collection_alias));

From 00bd6c409ebf8804401eb8ae2a09e810e654c732 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Tue, 17 Mar 2026 13:43:26 -0400
Subject: [PATCH 12/20] constraint set assignability does not use `inferable`

---
 crates/ty_python_semantic/src/types.rs               |  8 +-------
 crates/ty_python_semantic/src/types/call/bind.rs     |  7 +------
 crates/ty_python_semantic/src/types/generics.rs      |  9 +--------
 crates/ty_python_semantic/src/types/infer/builder.rs | 10 ++--------
 crates/ty_python_semantic/src/types/relation.rs      |  8 +++-----
 crates/ty_python_semantic/src/types/signatures.rs    |  8 +-------
 6 files changed, 9 insertions(+), 41 deletions(-)

diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs
index 4cdbb0c726e42..24dbdaa7d41b6 100644
--- a/crates/ty_python_semantic/src/types.rs
+++ b/crates/ty_python_semantic/src/types.rs
@@ -1890,13 +1890,7 @@ impl<'db> Type<'db> {
             .annotation
             .and_then(|tcx| {
                 let alias_instance = Type::instance(db, class_literal.identity_specialization(db));
-                let inferable = generic_context.inferable_typevars(db);
-                let set = alias_instance.when_constraint_set_assignable_to(
-                    db,
-                    tcx,
-                    constraints,
-                    inferable,
-                );
+                let set = alias_instance.when_constraint_set_assignable_to(db, tcx, constraints);
                 match set.solutions(db, constraints) {
                     Solutions::Constrained(solutions) => {
                         let mut mappings = FxHashMap::default();
diff --git a/crates/ty_python_semantic/src/types/call/bind.rs b/crates/ty_python_semantic/src/types/call/bind.rs
index a07e4fab65ada..81d7b18e26126 100644
--- a/crates/ty_python_semantic/src/types/call/bind.rs
+++ b/crates/ty_python_semantic/src/types/call/bind.rs
@@ -3755,12 +3755,7 @@ impl<'a, 'db> ArgumentTypeChecker<'a, 'db> {
                 tcx.filter_union(self.db, |ty| ty.class_specialization(self.db).is_some())
                     .class_specialization(self.db)?;
 
-                let set = return_ty.when_constraint_set_assignable_to(
-                    self.db,
-                    tcx,
-                    constraints,
-                    self.inferable_typevars,
-                );
+                let set = return_ty.when_constraint_set_assignable_to(self.db, tcx, constraints);
 
                 // Use `solutions_with` to determine per-typevar variance from the raw
                 // lower/upper bounds on each BDD path.
diff --git a/crates/ty_python_semantic/src/types/generics.rs b/crates/ty_python_semantic/src/types/generics.rs
index 3818cd75ae3c5..c3d6f7711ef4d 100644
--- a/crates/ty_python_semantic/src/types/generics.rs
+++ b/crates/ty_python_semantic/src/types/generics.rs
@@ -1775,12 +1775,7 @@ impl<'db, 'c> SpecializationBuilder<'db, 'c> {
             if formal_is_single_paramspec {
                 let when = actual_callable
                     .signatures(self.db)
-                    .when_constraint_set_assignable_to(
-                        self.db,
-                        formal_signature,
-                        self.constraints,
-                        self.inferable,
-                    );
+                    .when_constraint_set_assignable_to(self.db, formal_signature, self.constraints);
                 self.add_type_mappings_from_constraint_set(formal, when, &mut *f)?;
             } else {
                 // An overloaded actual callable is compatible with the formal signature if at
@@ -1792,7 +1787,6 @@ impl<'db, 'c> SpecializationBuilder<'db, 'c> {
                         self.db,
                         formal_signature,
                         self.constraints,
-                        self.inferable,
                     );
                     if self
                         .add_type_mappings_from_constraint_set(formal, when, &mut *f)
@@ -2244,7 +2238,6 @@ impl<'db, 'c> SpecializationBuilder<'db, 'c> {
                             self.db,
                             formal,
                             self.constraints,
-                            self.inferable,
                         );
                         // For protocol inference via constraint sets, we currently treat
                         // unsatisfiable results as "no inference" instead of an immediate
diff --git a/crates/ty_python_semantic/src/types/infer/builder.rs b/crates/ty_python_semantic/src/types/infer/builder.rs
index a9f31797e958d..c46d9ada24210 100644
--- a/crates/ty_python_semantic/src/types/infer/builder.rs
+++ b/crates/ty_python_semantic/src/types/infer/builder.rs
@@ -5180,12 +5180,10 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
                         let return_ty = overload
                             .constructor_instance_type
                             .unwrap_or(overload.signature.return_ty);
-                        let inferable = generic_context.inferable_typevars(db);
                         let set = return_ty.when_constraint_set_assignable_to(
                             db,
                             declared_return_ty,
                             &constraints,
-                            inferable,
                         );
                         if let Solutions::Constrained(solutions) = set.solutions(db, &constraints) {
                             for solution in solutions.iter() {
@@ -6095,12 +6093,8 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
                 let db = self.db();
                 let collection_instance = Type::instance(db, ClassType::Generic(collection_alias));
 
-                let set = collection_instance.when_constraint_set_assignable_to(
-                    db,
-                    tcx,
-                    &constraints,
-                    inferable,
-                );
+                let set =
+                    collection_instance.when_constraint_set_assignable_to(db, tcx, &constraints);
 
                 // Use `solutions_with_inferable` to capture per-typevar variance from the raw
                 // lower/upper bounds on each BDD path. We must use the inferable-aware variant so
diff --git a/crates/ty_python_semantic/src/types/relation.rs b/crates/ty_python_semantic/src/types/relation.rs
index f21a7a33535b5..a3a3cfd0688da 100644
--- a/crates/ty_python_semantic/src/types/relation.rs
+++ b/crates/ty_python_semantic/src/types/relation.rs
@@ -346,7 +346,7 @@ impl<'db> Type<'db> {
     /// reasoning depending on inferable typevars.
     pub fn is_constraint_set_assignable_to(self, db: &'db dyn Db, target: Type<'db>) -> bool {
         let constraints = ConstraintSetBuilder::new();
-        self.when_constraint_set_assignable_to(db, target, &constraints, InferableTypeVars::None)
+        self.when_constraint_set_assignable_to(db, target, &constraints)
             .is_always_satisfied(db)
     }
 
@@ -371,13 +371,12 @@ impl<'db> Type<'db> {
         db: &'db dyn Db,
         target: Type<'db>,
         constraints: &'c ConstraintSetBuilder<'db>,
-        inferable: InferableTypeVars<'_, 'db>,
     ) -> ConstraintSet<'db, 'c> {
         self.has_relation_to(
             db,
             target,
             constraints,
-            inferable,
+            InferableTypeVars::None,
             TypeRelation::ConstraintSetAssignability,
         )
     }
@@ -558,13 +557,12 @@ impl<'a, 'c, 'db> TypeRelationChecker<'a, 'c, 'db> {
 
     pub(super) fn constraint_set_assignability(
         constraints: &'c ConstraintSetBuilder<'db>,
-        inferable: InferableTypeVars<'a, 'db>,
         relation_visitor: &'a HasRelationToVisitor<'db, 'c>,
         disjointness_visitor: &'a IsDisjointVisitor<'db, 'c>,
     ) -> Self {
         Self {
             constraints,
-            inferable,
+            inferable: InferableTypeVars::None,
             relation: TypeRelation::ConstraintSetAssignability,
             given: ConstraintSet::from_bool(constraints, false),
             relation_visitor,
diff --git a/crates/ty_python_semantic/src/types/signatures.rs b/crates/ty_python_semantic/src/types/signatures.rs
index ec1754fba48b8..c3c0c0c99dee5 100644
--- a/crates/ty_python_semantic/src/types/signatures.rs
+++ b/crates/ty_python_semantic/src/types/signatures.rs
@@ -319,13 +319,11 @@ impl<'db> CallableSignature<'db> {
         db: &'db dyn Db,
         other: &Self,
         constraints: &'c ConstraintSetBuilder<'db>,
-        inferable: InferableTypeVars<'_, 'db>,
     ) -> ConstraintSet<'db, 'c> {
         let relation_visitor = HasRelationToVisitor::default(constraints);
         let disjointness_visitor = IsDisjointVisitor::default(constraints);
         let checker = TypeRelationChecker::constraint_set_assignability(
             constraints,
-            inferable,
             &relation_visitor,
             &disjointness_visitor,
         );
@@ -729,7 +727,6 @@ impl<'db> Signature<'db> {
         db: &'db dyn Db,
         other: &CallableSignature<'db>,
         constraints: &'c ConstraintSetBuilder<'db>,
-        inferable: InferableTypeVars<'_, 'db>,
     ) -> ConstraintSet<'db, 'c> {
         // If this signature is a paramspec, bind it to the entire overloaded other callable.
         if let Some(self_bound_typevar) = self.parameters.as_paramspec()
@@ -762,7 +759,6 @@ impl<'db> Signature<'db> {
                         db,
                         other_return_type,
                         constraints,
-                        inferable,
                     )
                 });
             return param_spec_matches.and(db, constraints, || return_types_match);
@@ -772,7 +768,7 @@ impl<'db> Signature<'db> {
             .overloads
             .iter()
             .when_all(db, constraints, |other_signature| {
-                self.when_constraint_set_assignable_to(db, other_signature, constraints, inferable)
+                self.when_constraint_set_assignable_to(db, other_signature, constraints)
             })
     }
 
@@ -781,13 +777,11 @@ impl<'db> Signature<'db> {
         db: &'db dyn Db,
         other: &Self,
         constraints: &'c ConstraintSetBuilder<'db>,
-        inferable: InferableTypeVars<'_, 'db>,
     ) -> ConstraintSet<'db, 'c> {
         let relation_visitor = HasRelationToVisitor::default(constraints);
         let disjointness_visitor = IsDisjointVisitor::default(constraints);
         let checker = TypeRelationChecker::constraint_set_assignability(
             constraints,
-            inferable,
             &relation_visitor,
             &disjointness_visitor,
         );

From fb6c3f04096ec70f3f5cb658482dd75785b2405d Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Tue, 17 Mar 2026 14:21:19 -0400
Subject: [PATCH 13/20] add fast path for instances of same class

---
 crates/ty_python_semantic/src/types/class.rs | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/crates/ty_python_semantic/src/types/class.rs b/crates/ty_python_semantic/src/types/class.rs
index d435ebcf02d0e..d6e76197b01b6 100644
--- a/crates/ty_python_semantic/src/types/class.rs
+++ b/crates/ty_python_semantic/src/types/class.rs
@@ -1842,6 +1842,24 @@ impl<'c, 'db> TypeRelationChecker<'_, 'c, 'db> {
         source: ClassType<'db>,
         target: ClassType<'db>,
     ) -> ConstraintSet<'db, 'c> {
+        // Fast path: if source and target are the same class (possibly with different
+        // specializations), we can compare them directly without walking the MRO.
+        match (source, target) {
+            (ClassType::NonGeneric(source), ClassType::NonGeneric(target)) if source == target => {
+                return self.always();
+            }
+            (ClassType::Generic(source_alias), ClassType::Generic(target_alias))
+                if source_alias.origin(db) == target_alias.origin(db) =>
+            {
+                return self.check_specialization_pair(
+                    db,
+                    source_alias.specialization(db),
+                    target_alias.specialization(db),
+                );
+            }
+            _ => {}
+        }
+
         source.iter_mro(db).when_any(db, self.constraints, |base| {
             match base {
                 ClassBase::Dynamic(_) => match self.relation {

From d74d703e7864b7116e0e2961a83be725c0ed0c27 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Tue, 17 Mar 2026 14:37:56 -0400
Subject: [PATCH 14/20] fix doc link

---
 crates/ty_python_semantic/src/types/generics.rs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/generics.rs b/crates/ty_python_semantic/src/types/generics.rs
index c3d6f7711ef4d..abbb8e5797ec9 100644
--- a/crates/ty_python_semantic/src/types/generics.rs
+++ b/crates/ty_python_semantic/src/types/generics.rs
@@ -1737,10 +1737,10 @@ impl<'db, 'c> SpecializationBuilder<'db, 'c> {
     /// argument, and the variance of those typevars in the corresponding parameter.
     ///
     /// TODO: This is a stopgap! Eventually, the builder will maintain a single constraint set for
-    /// the main specialization that we are building, and [`build`][Self::build] will build the
-    /// specialization directly from that constraint set. This method lets us migrate to that brave
-    /// new world incrementally, by using the new constraint set mechanism piecemeal for certain
-    /// type comparisons.
+    /// the main specialization that we are building, and [`build_with`][Self::build_with] will
+    /// build the specialization directly from that constraint set. This method lets us migrate to
+    /// that brave new world incrementally, by using the new constraint set mechanism piecemeal for
+    /// certain type comparisons.
     fn add_type_mappings_from_constraint_set(
         &mut self,
         formal: Type<'db>,

From f6d32b58686d6da385469ef9c72eb424cfab77f6 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Mon, 23 Mar 2026 16:13:04 -0400
Subject: [PATCH 15/20] fix failing test

---
 crates/ty_python_semantic/src/types/call/bind.rs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/crates/ty_python_semantic/src/types/call/bind.rs b/crates/ty_python_semantic/src/types/call/bind.rs
index 01c495db91c13..0dbc36537dfc2 100644
--- a/crates/ty_python_semantic/src/types/call/bind.rs
+++ b/crates/ty_python_semantic/src/types/call/bind.rs
@@ -3786,6 +3786,9 @@ impl<'a, 'db> ArgumentTypeChecker<'a, 'db> {
                 tcx.filter_union(self.db, |ty| ty.class_specialization(self.db).is_some())
                     .class_specialization(self.db)?;
 
+                let return_ty =
+                    return_ty.filter_disjoint_elements(self.db, tcx, self.inferable_typevars);
+                let tcx = tcx.filter_disjoint_elements(self.db, return_ty, self.inferable_typevars);
                 let set = return_ty.when_constraint_set_assignable_to(self.db, tcx, constraints);
 
                 // Use `solutions_with` to determine per-typevar variance from the raw

From e02ef4c91a630d2e3f21f792e3ff93711569131a Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Mon, 23 Mar 2026 16:27:59 -0400
Subject: [PATCH 16/20] docs fixes

---
 .../ty_python_semantic/src/types/call/bind.rs |  6 +++---
 .../ty_python_semantic/src/types/generics.rs  | 11 ++---------
 .../src/types/infer/builder.rs                | 19 +++++++++----------
 3 files changed, 14 insertions(+), 22 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/call/bind.rs b/crates/ty_python_semantic/src/types/call/bind.rs
index 0dbc36537dfc2..1fddc57e51272 100644
--- a/crates/ty_python_semantic/src/types/call/bind.rs
+++ b/crates/ty_python_semantic/src/types/call/bind.rs
@@ -3766,11 +3766,11 @@ impl<'a, 'db> ArgumentTypeChecker<'a, 'db> {
         // Attempt to solve the specialization while preferring the declared type of non-covariant
         // type parameters from generic classes.
         //
-        // We use a forward assignability check (`return_ty ≤ tcx`) to infer what each typevar in
-        // the function's return type maps to in the type context. (We use _constraint set_
+        // We use an assignability check (`return_ty ≤ tcx`) to infer what each typevar in the
+        // function's return type maps to in the type context. (We use _constraint set_
         // assignability so that we get a constraint set describing the typevars.) For example, if
         // the return type is `list[T]` and the type context is `list[int]`, the check produces
-        // `T ≤ int`, from which we extract the preferred type `int`.
+        // `T = int`, from which we extract the preferred type `int`.
         //
         // TODO: This two-phase approach (extract preferred types from the type context, then check
         // argument compatibility) should eventually be replaced by conjoining the type context
diff --git a/crates/ty_python_semantic/src/types/generics.rs b/crates/ty_python_semantic/src/types/generics.rs
index abbb8e5797ec9..b6cdd3f17be1e 100644
--- a/crates/ty_python_semantic/src/types/generics.rs
+++ b/crates/ty_python_semantic/src/types/generics.rs
@@ -1658,15 +1658,8 @@ impl<'db, 'c> SpecializationBuilder<'db, 'c> {
     /// are set to the inferred type (representing an equality constraint). Unmapped typevars
     /// are left to `specialize_recursive` to fill in with defaults.
     ///
-    /// The hook returns:
-    /// - `Some(ty)` to use `ty` as the specialization for this typevar
-    /// - `None` to use the inferred type unchanged
-    ///
-    /// This method replaces the pattern of `mapped(...).build(...)`, allowing callers to
-    /// transform inferred types (e.g., literal promotion) in a single step. In the future,
-    /// when the builder's internal representation switches from a `HashMap` to a `ConstraintSet`,
-    /// the hook will receive actual lower/upper bounds from the constraint set instead of
-    /// synthetic equality bounds.
+    /// The hook should return `Some(ty)` to use `ty` as the specialization for this typevar, or
+    /// `None` to use the inferred type unchanged.
     pub(crate) fn build_with(
         &mut self,
         generic_context: GenericContext<'db>,
diff --git a/crates/ty_python_semantic/src/types/infer/builder.rs b/crates/ty_python_semantic/src/types/infer/builder.rs
index d94334bde21fe..892fb8d73c7aa 100644
--- a/crates/ty_python_semantic/src/types/infer/builder.rs
+++ b/crates/ty_python_semantic/src/types/infer/builder.rs
@@ -6056,18 +6056,17 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
 
             if let Some(tcx) = tcx.annotation
                 && tcx.class_specialization(self.db()).is_some()
-                // Skip constraint extraction when the type context contains
-                // UnspecializedTypeVar placeholders (from partially-specialized
-                // parameter types during multi-inference for overloaded calls).
-                // The CSA would walk through protocol supertypes and produce
-                // constraints contaminated by the placeholder, which collapse to
-                // `Any` during solution extraction and bypass downstream filters.
+                // Skip constraint extraction when the type context contains UnspecializedTypeVar
+                // placeholders (from partially-specialized parameter types during multi-inference
+                // for overloaded calls). The assignability check would walk through protocol
+                // supertypes and produce constraints contaminated by the placeholder, which
+                // collapse to `Any` during solution extraction and bypass downstream filters.
                 //
                 // TODO: UnspecializedTypeVar should be removed entirely once the
-                // SpecializationBuilder uses constraint sets internally, at which
-                // point the typevars that it currently replaces can instead be
-                // existentially quantified away (as is already done for generic
-                // callable assignability in `check_signature_pair`).
+                // SpecializationBuilder uses constraint sets internally, at which point the
+                // typevars that it currently replaces can instead be existentially quantified away
+                // (as is already done for generic callable assignability in
+                // `check_signature_pair`).
                 && !tcx.has_unspecialized_type_var(self.db())
             {
                 let db = self.db();

From 767f30dc5a5a1fc997da040220bd2c809f6f1112 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Mon, 23 Mar 2026 16:32:29 -0400
Subject: [PATCH 17/20] DRY variance calculation

---
 .../ty_python_semantic/src/types/call/bind.rs |  9 +----
 .../src/types/constraints.rs                  | 39 ++++++++++++++++---
 .../src/types/infer/builder.rs                | 13 +------
 3 files changed, 36 insertions(+), 25 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/call/bind.rs b/crates/ty_python_semantic/src/types/call/bind.rs
index 1fddc57e51272..4b3be4a46c826 100644
--- a/crates/ty_python_semantic/src/types/call/bind.rs
+++ b/crates/ty_python_semantic/src/types/call/bind.rs
@@ -3799,14 +3799,7 @@ impl<'a, 'db> ArgumentTypeChecker<'a, 'db> {
                     self.db,
                     constraints,
                     self.inferable_typevars,
-                    |typevar, lower, upper| {
-                        let variance = if lower.is_never() {
-                            TypeVarVariance::Covariant
-                        } else if upper == Type::object() {
-                            TypeVarVariance::Contravariant
-                        } else {
-                            TypeVarVariance::Invariant
-                        };
+                    |typevar, variance, _lower, _upper| {
                         let identity = typevar.identity(self.db);
                         variance_map
                             .entry(identity)
diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 4fcfbb71c4c5e..98654704b1aaf 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -106,7 +106,8 @@ use crate::types::visitor::{
     TypeCollector, TypeVisitor, any_over_type, walk_type_with_recursion_guard,
 };
 use crate::types::{
-    BoundTypeVarInstance, IntersectionType, Type, TypeVarBoundOrConstraints, UnionType,
+    BoundTypeVarInstance, IntersectionType, Type, TypeVarBoundOrConstraints, TypeVarVariance,
+    UnionType,
 };
 use crate::{Db, FxIndexMap, FxIndexSet};
 
@@ -647,7 +648,12 @@ impl<'db, 'c> ConstraintSet<'db, 'c> {
         db: &'db dyn Db,
         builder: &'c ConstraintSetBuilder<'db>,
         inferable: InferableTypeVars<'_, 'db>,
-        choose: impl FnMut(BoundTypeVarInstance<'db>, Type<'db>, Type<'db>) -> Option<Type<'db>>,
+        choose: impl FnMut(
+            BoundTypeVarInstance<'db>,
+            TypeVarVariance,
+            Type<'db>,
+            Type<'db>,
+        ) -> Option<Type<'db>>,
     ) -> Solutions<Vec<Solution<'db>>> {
         self.verify_builder(builder);
 
@@ -1787,7 +1793,12 @@ impl NodeId {
         db: &'db dyn Db,
         builder: &ConstraintSetBuilder<'db>,
         inferable: Option<InferableTypeVars<'_, 'db>>,
-        choose: impl FnMut(BoundTypeVarInstance<'db>, Type<'db>, Type<'db>) -> Option<Type<'db>>,
+        choose: impl FnMut(
+            BoundTypeVarInstance<'db>,
+            TypeVarVariance,
+            Type<'db>,
+            Type<'db>,
+        ) -> Option<Type<'db>>,
     ) -> Solutions<Vec<Solution<'db>>> {
         match self.node() {
             Node::AlwaysTrue => Solutions::Unconstrained,
@@ -3444,7 +3455,12 @@ impl InteriorNode {
         db: &'db dyn Db,
         builder: &ConstraintSetBuilder<'db>,
         inferable: Option<InferableTypeVars<'_, 'db>>,
-        mut choose: impl FnMut(BoundTypeVarInstance<'db>, Type<'db>, Type<'db>) -> Option<Type<'db>>,
+        mut choose: impl FnMut(
+            BoundTypeVarInstance<'db>,
+            TypeVarVariance,
+            Type<'db>,
+            Type<'db>,
+        ) -> Option<Type<'db>>,
     ) -> Solutions<Vec<Solution<'db>>> {
         let path_bounds = compute_path_bounds(db, builder, self.node());
         let solutions = solve_paths(db, &path_bounds, |db, bound_typevar, lower, upper| {
@@ -3455,7 +3471,20 @@ impl InteriorNode {
                     return Ok(None);
                 }
             }
-            if let Some(ty) = choose(bound_typevar, lower, upper) {
+
+            // Determine variance from the constraint bounds:
+            // - Only upper bound (lower = Never) → covariant position
+            // - Only lower bound (upper = object) → contravariant position
+            // - Both bounds set → invariant position
+            let variance = if lower.is_never() {
+                TypeVarVariance::Covariant
+            } else if upper == Type::object() {
+                TypeVarVariance::Contravariant
+            } else {
+                TypeVarVariance::Invariant
+            };
+
+            if let Some(ty) = choose(bound_typevar, variance, lower, upper) {
                 return Ok(Some(TypeVarSolution {
                     bound_typevar,
                     solution: ty,
diff --git a/crates/ty_python_semantic/src/types/infer/builder.rs b/crates/ty_python_semantic/src/types/infer/builder.rs
index 892fb8d73c7aa..df3f600cfa9d9 100644
--- a/crates/ty_python_semantic/src/types/infer/builder.rs
+++ b/crates/ty_python_semantic/src/types/infer/builder.rs
@@ -6087,18 +6087,7 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
                     db,
                     &constraints,
                     inferable,
-                    |typevar, lower, upper| {
-                        // Determine variance from the constraint bounds:
-                        // - Only upper bound (lower = Never) → covariant position
-                        // - Only lower bound (upper = object) → contravariant position
-                        // - Both bounds set → invariant position
-                        let variance = if lower.is_never() {
-                            TypeVarVariance::Covariant
-                        } else if upper == Type::object() {
-                            TypeVarVariance::Contravariant
-                        } else {
-                            TypeVarVariance::Invariant
-                        };
+                    |typevar, variance, _lower, _upper| {
                         let identity = typevar.identity(db);
                         elt_tcx_variance
                             .entry(identity)

From 74277740c2e22342b6d3c9d88b3d042e0f38e2ce Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Mon, 23 Mar 2026 16:55:55 -0400
Subject: [PATCH 18/20] remove unneeded check

---
 crates/ty_python_semantic/src/types/call/bind.rs | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/call/bind.rs b/crates/ty_python_semantic/src/types/call/bind.rs
index 4b3be4a46c826..f08e07106b6c9 100644
--- a/crates/ty_python_semantic/src/types/call/bind.rs
+++ b/crates/ty_python_semantic/src/types/call/bind.rs
@@ -3835,12 +3835,6 @@ impl<'a, 'db> ArgumentTypeChecker<'a, 'db> {
                         // SequentMap transitivity) and unspecialized typevars (from partially
                         // specialized contexts).
                         let inferred_ty = binding.solution.filter_union(self.db, |ty| {
-                            if ty
-                                .as_typevar()
-                                .is_some_and(|tv| tv.is_inferable(self.db, self.inferable_typevars))
-                            {
-                                return false;
-                            }
                             if ty.has_unspecialized_type_var(self.db) {
                                 partially_specialized_declared_type.insert(identity);
                                 return false;

From a5cb24d2279f324fd772bf837c307065dccf6371 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Mon, 23 Mar 2026 18:08:29 -0400
Subject: [PATCH 19/20] move some things around

---
 .../ty_python_semantic/src/types/call/bind.rs |   6 +-
 .../src/types/constraints.rs                  | 352 +++++++++---------
 .../src/types/infer/builder.rs                |   6 +-
 3 files changed, 181 insertions(+), 183 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/call/bind.rs b/crates/ty_python_semantic/src/types/call/bind.rs
index f08e07106b6c9..99977b1580b05 100644
--- a/crates/ty_python_semantic/src/types/call/bind.rs
+++ b/crates/ty_python_semantic/src/types/call/bind.rs
@@ -27,7 +27,7 @@ use crate::place::{DefinedPlace, Definedness, Place, known_module_symbol};
 use crate::subscript::PyIndex;
 use crate::types::call::arguments::{CallArgumentTypes, Expansion, is_expandable_type};
 use crate::types::callable::CallableTypeKind;
-use crate::types::constraints::{ConstraintSet, ConstraintSetBuilder, Solutions};
+use crate::types::constraints::{ConstraintSet, ConstraintSetBuilder, PathBounds, Solutions};
 use crate::types::diagnostic::{
     CALL_NON_CALLABLE, CALL_TOP_CALLABLE, CONFLICTING_ARGUMENT_FORMS, INVALID_ARGUMENT_TYPE,
     INVALID_DATACLASS, MISSING_ARGUMENT, NO_MATCHING_OVERLOAD, PARAMETER_ALREADY_ASSIGNED,
@@ -3799,13 +3799,13 @@ impl<'a, 'db> ArgumentTypeChecker<'a, 'db> {
                     self.db,
                     constraints,
                     self.inferable_typevars,
-                    |typevar, variance, _lower, _upper| {
+                    |typevar, variance, lower, upper| {
                         let identity = typevar.identity(self.db);
                         variance_map
                             .entry(identity)
                             .and_modify(|current| *current = current.join(variance))
                             .or_insert(variance);
-                        None // Use default solution selection
+                        PathBounds::default_solve(self.db, typevar, variance, lower, upper)
                     },
                 );
 
diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 98654704b1aaf..0bb695362acc1 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -653,7 +653,7 @@ impl<'db, 'c> ConstraintSet<'db, 'c> {
             TypeVarVariance,
             Type<'db>,
             Type<'db>,
-        ) -> Option<Type<'db>>,
+        ) -> Result<Option<Type<'db>>, ()>,
     ) -> Solutions<Vec<Solution<'db>>> {
         self.verify_builder(builder);
 
@@ -1798,7 +1798,7 @@ impl NodeId {
             TypeVarVariance,
             Type<'db>,
             Type<'db>,
-        ) -> Option<Type<'db>>,
+        ) -> Result<Option<Type<'db>>, ()>,
     ) -> Solutions<Vec<Solution<'db>>> {
         match self.node() {
             Node::AlwaysTrue => Solutions::Unconstrained,
@@ -2727,181 +2727,197 @@ struct TypeVarBounds<'db> {
 }
 
 /// Per-path bounds for all typevars. Each element is the set of typevar bounds for one BDD path.
-type PathBounds<'db> = Vec<Vec<TypeVarBounds<'db>>>;
+pub(crate) struct PathBounds<'db>(Vec<Vec<TypeVarBounds<'db>>>);
 
-/// Computes sorted BDD paths and accumulates per-typevar lower/upper bounds for each path.
-///
-/// Returns a list of paths, where each path contains the materialized lower/upper bounds for
-/// each typevar that appears in the path's constraints.
-fn compute_path_bounds<'db>(
-    db: &'db dyn Db,
-    builder: &ConstraintSetBuilder<'db>,
-    node: NodeId,
-) -> PathBounds<'db> {
-    // Sort the constraints in each path by their `source_order`s, to ensure that we construct
-    // any unions or intersections in our type mappings in a stable order. Constraints might
-    // come out of `PathAssignment`s with identical `source_order`s, but if they do, those
-    // "tied" constraints will still be ordered in a stable way. So we need a stable sort to
-    // retain that stable per-tie ordering.
-    let mut sorted_paths = Vec::new();
-    node.for_each_path(db, builder, |path| {
-        let mut path: Vec<_> = path.positive_constraints().collect();
-        path.sort_by_key(|(_, source_order)| *source_order);
-        sorted_paths.push(path);
-    });
-    sorted_paths.sort_by(|path1, path2| {
-        let source_orders1 = path1.iter().map(|(_, source_order)| *source_order);
-        let source_orders2 = path2.iter().map(|(_, source_order)| *source_order);
-        source_orders1.cmp(source_orders2)
-    });
-
-    let mut result = Vec::with_capacity(sorted_paths.len());
-    let mut mappings: FxHashMap<BoundTypeVarInstance<'db>, Bounds<'db>> = FxHashMap::default();
-
-    for path in sorted_paths {
-        mappings.clear();
-        for (constraint, _) in path {
-            let constraint = builder.constraint_data(constraint);
-            let typevar = constraint.typevar;
-            let lower = constraint.lower;
-            let upper = constraint.upper;
-            let bounds = mappings.entry(typevar).or_default();
-            bounds.add_lower(db, lower);
-            bounds.add_upper(db, upper);
-
-            if let Type::TypeVar(lower_bound_typevar) = lower {
-                let bounds = mappings.entry(lower_bound_typevar).or_default();
-                bounds.add_upper(db, Type::TypeVar(typevar));
-            }
+impl<'db> PathBounds<'db> {
+    /// Computes sorted BDD paths and accumulates per-typevar lower/upper bounds for each path.
+    ///
+    /// Returns a list of paths, where each path contains the materialized lower/upper bounds for
+    /// each typevar that appears in the path's constraints.
+    fn compute(db: &'db dyn Db, builder: &ConstraintSetBuilder<'db>, node: NodeId) -> Self {
+        // Sort the constraints in each path by their `source_order`s, to ensure that we construct
+        // any unions or intersections in our type mappings in a stable order. Constraints might
+        // come out of `PathAssignment`s with identical `source_order`s, but if they do, those
+        // "tied" constraints will still be ordered in a stable way. So we need a stable sort to
+        // retain that stable per-tie ordering.
+        let mut sorted_paths = Vec::new();
+        node.for_each_path(db, builder, |path| {
+            let mut path: Vec<_> = path.positive_constraints().collect();
+            path.sort_by_key(|(_, source_order)| *source_order);
+            sorted_paths.push(path);
+        });
+        sorted_paths.sort_by(|path1, path2| {
+            let source_orders1 = path1.iter().map(|(_, source_order)| *source_order);
+            let source_orders2 = path2.iter().map(|(_, source_order)| *source_order);
+            source_orders1.cmp(source_orders2)
+        });
+
+        let mut result = Vec::with_capacity(sorted_paths.len());
+        let mut mappings: FxHashMap<BoundTypeVarInstance<'db>, Bounds<'db>> = FxHashMap::default();
+
+        for path in sorted_paths {
+            mappings.clear();
+            for (constraint, _) in path {
+                let constraint = builder.constraint_data(constraint);
+                let typevar = constraint.typevar;
+                let lower = constraint.lower;
+                let upper = constraint.upper;
+                let bounds = mappings.entry(typevar).or_default();
+                bounds.add_lower(db, lower);
+                bounds.add_upper(db, upper);
+
+                if let Type::TypeVar(lower_bound_typevar) = lower {
+                    let bounds = mappings.entry(lower_bound_typevar).or_default();
+                    bounds.add_upper(db, Type::TypeVar(typevar));
+                }
 
-            if let Type::TypeVar(upper_bound_typevar) = upper {
-                let bounds = mappings.entry(upper_bound_typevar).or_default();
-                bounds.add_lower(db, Type::TypeVar(typevar));
+                if let Type::TypeVar(upper_bound_typevar) = upper {
+                    let bounds = mappings.entry(upper_bound_typevar).or_default();
+                    bounds.add_lower(db, Type::TypeVar(typevar));
+                }
             }
+
+            let path_bounds = mappings
+                .drain()
+                .map(|(bound_typevar, bounds)| TypeVarBounds {
+                    bound_typevar,
+                    lower: UnionType::from_elements(db, bounds.lower),
+                    upper: IntersectionType::from_elements(db, bounds.upper),
+                })
+                .collect();
+            result.push(path_bounds);
         }
 
-        let path_bounds = mappings
-            .drain()
-            .map(|(bound_typevar, bounds)| TypeVarBounds {
-                bound_typevar,
-                lower: UnionType::from_elements(db, bounds.lower),
-                upper: IntersectionType::from_elements(db, bounds.upper),
-            })
-            .collect();
-        result.push(path_bounds);
+        Self(result)
     }
 
-    result
-}
-
-/// The default solution selection logic for a single typevar on a single BDD path.
-///
-/// Given the materialized lower and upper bounds for a typevar, selects the solution type.
-/// Returns:
-/// - `Ok(Some(solution))` if the typevar is solved on this path
-/// - `Ok(None)` if the typevar is unsolved (no solution added)
-/// - `Err(())` if the path is invalid (bounds violate the typevar's declared constraints)
-fn default_solve<'db>(
-    db: &'db dyn Db,
-    bound_typevar: BoundTypeVarInstance<'db>,
-    lower: Type<'db>,
-    upper: Type<'db>,
-) -> Result<Option<TypeVarSolution<'db>>, ()> {
-    match bound_typevar.typevar(db).require_bound_or_constraints(db) {
-        TypeVarBoundOrConstraints::UpperBound(bound) => {
-            let bound = bound.top_materialization(db);
-            if !lower.is_assignable_to(db, bound) {
-                // This path does not satisfy the typevar's upper bound, and is
-                // therefore not a valid specialization.
-                return Err(());
-            }
+    fn solve(&self, db: &'db dyn Db) -> Vec<Solution<'db>> {
+        self.solve_with(db, Self::default_solve)
+    }
 
-            // Prefer the lower bound (often the concrete actual type seen) over the
-            // upper bound (which may include TypeVar bounds/constraints). The upper bound
-            // should only be used as a fallback when no concrete type was inferred.
-            if !lower.is_never() {
-                return Ok(Some(TypeVarSolution {
+    /// Solves each path by applying a per-typevar solver function, collecting valid solutions.
+    ///
+    /// The solver receives the typevar and its materialized lower/upper bounds, and returns:
+    /// - `Ok(Some(solution))` to add a solution for this typevar on this path
+    /// - `Ok(None)` to leave this typevar unsolved on this path
+    /// - `Err(())` to invalidate the entire path
+    fn solve_with(
+        &self,
+        db: &'db dyn Db,
+        mut solver: impl FnMut(
+            &'db dyn Db,
+            BoundTypeVarInstance<'db>,
+            TypeVarVariance,
+            Type<'db>,
+            Type<'db>,
+        ) -> Result<Option<Type<'db>>, ()>,
+    ) -> Vec<Solution<'db>> {
+        let mut solutions = Vec::with_capacity(self.0.len());
+        'paths: for path in &self.0 {
+            let mut solution = Vec::with_capacity(path.len());
+            for bounds in path {
+                let TypeVarBounds {
                     bound_typevar,
-                    solution: lower,
-                }));
-            }
+                    lower,
+                    upper,
+                } = *bounds;
+
+                // Determine variance from the constraint bounds:
+                // - Only upper bound (lower = Never) → covariant position
+                // - Only lower bound (upper = object) → contravariant position
+                // - Both bounds set → invariant position
+                let variance = if lower.is_never() {
+                    TypeVarVariance::Covariant
+                } else if upper == Type::object() {
+                    TypeVarVariance::Contravariant
+                } else {
+                    TypeVarVariance::Invariant
+                };
 
-            let upper = IntersectionType::from_elements(
-                db,
-                std::iter::once(upper).chain(std::iter::once(bound)),
-            );
-            if upper != bound {
-                Ok(Some(TypeVarSolution {
-                    bound_typevar,
-                    solution: upper,
-                }))
-            } else {
-                Ok(None)
+                match solver(db, bound_typevar, variance, lower, upper) {
+                    Ok(Some(ty)) => solution.push(TypeVarSolution {
+                        bound_typevar,
+                        solution: ty,
+                    }),
+                    Ok(None) => {}
+                    Err(()) => continue 'paths,
+                }
             }
+            solutions.push(solution);
         }
+        solutions
+    }
 
-        TypeVarBoundOrConstraints::Constraints(constraints) => {
-            // Filter out the typevar constraints that aren't satisfied by this path.
-            let compatible_constraints = constraints.elements(db).iter().filter(|constraint| {
-                let constraint_lower = constraint.bottom_materialization(db);
-                let constraint_upper = constraint.top_materialization(db);
-                lower.is_assignable_to(db, constraint_lower)
-                    && constraint_upper.is_assignable_to(db, upper)
-            });
-
-            // If only one constraint remains, that's our specialization for this path.
-            match compatible_constraints.at_most_one() {
-                Ok(None) => {
-                    // This path does not satisfy any of the constraints, and is
+    /// The default solution selection logic for a single typevar on a single BDD path.
+    ///
+    /// Given the materialized lower and upper bounds for a typevar, selects the solution type.
+    /// Returns:
+    /// - `Ok(Some(solution))` if the typevar is solved on this path
+    /// - `Ok(None)` if the typevar is unsolved (no solution added)
+    /// - `Err(())` if the path is invalid (bounds violate the typevar's declared constraints)
+    pub(crate) fn default_solve(
+        db: &'db dyn Db,
+        bound_typevar: BoundTypeVarInstance<'db>,
+        _variance: TypeVarVariance,
+        lower: Type<'db>,
+        upper: Type<'db>,
+    ) -> Result<Option<Type<'db>>, ()> {
+        match bound_typevar.typevar(db).require_bound_or_constraints(db) {
+            TypeVarBoundOrConstraints::UpperBound(bound) => {
+                let bound = bound.top_materialization(db);
+                if !lower.is_assignable_to(db, bound) {
+                    // This path does not satisfy the typevar's upper bound, and is
                     // therefore not a valid specialization.
-                    Err(())
+                    return Err(());
                 }
 
-                Ok(Some(compatible_constraint)) => Ok(Some(TypeVarSolution {
-                    bound_typevar,
-                    solution: *compatible_constraint,
-                })),
+                // Prefer the lower bound (often the concrete actual type seen) over the
+                // upper bound (which may include TypeVar bounds/constraints). The upper bound
+                // should only be used as a fallback when no concrete type was inferred.
+                if !lower.is_never() {
+                    return Ok(Some(lower));
+                }
 
-                Err(_) => {
-                    // This path satisfies multiple constraints. For now, don't
-                    // prefer any of them, and fall back on the default
-                    // specialization for this typevar.
+                let upper = IntersectionType::from_elements(
+                    db,
+                    std::iter::once(upper).chain(std::iter::once(bound)),
+                );
+                if upper != bound {
+                    Ok(Some(upper))
+                } else {
                     Ok(None)
                 }
             }
-        }
-    }
-}
 
-/// Solves each path by applying a per-typevar solver function, collecting valid solutions.
-///
-/// The solver receives the typevar and its materialized lower/upper bounds, and returns:
-/// - `Ok(Some(solution))` to add a solution for this typevar on this path
-/// - `Ok(None)` to leave this typevar unsolved on this path
-/// - `Err(())` to invalidate the entire path
-fn solve_paths<'db>(
-    db: &'db dyn Db,
-    path_bounds: &PathBounds<'db>,
-    mut solver: impl FnMut(
-        &'db dyn Db,
-        BoundTypeVarInstance<'db>,
-        Type<'db>,
-        Type<'db>,
-    ) -> Result<Option<TypeVarSolution<'db>>, ()>,
-) -> Vec<Solution<'db>> {
-    let mut solutions = Vec::with_capacity(path_bounds.len());
-    'paths: for path in path_bounds {
-        let mut solution = Vec::with_capacity(path.len());
-        for tvb in path {
-            match solver(db, tvb.bound_typevar, tvb.lower, tvb.upper) {
-                Ok(Some(s)) => solution.push(s),
-                Ok(None) => {}
-                Err(()) => continue 'paths,
+            TypeVarBoundOrConstraints::Constraints(constraints) => {
+                // Filter out the typevar constraints that aren't satisfied by this path.
+                let compatible_constraints = constraints.elements(db).iter().filter(|constraint| {
+                    let constraint_lower = constraint.bottom_materialization(db);
+                    let constraint_upper = constraint.top_materialization(db);
+                    lower.is_assignable_to(db, constraint_lower)
+                        && constraint_upper.is_assignable_to(db, upper)
+                });
+
+                // If only one constraint remains, that's our specialization for this path.
+                match compatible_constraints.at_most_one() {
+                    Ok(None) => {
+                        // This path does not satisfy any of the constraints, and is
+                        // therefore not a valid specialization.
+                        Err(())
+                    }
+
+                    Ok(Some(compatible_constraint)) => Ok(Some(*compatible_constraint)),
+
+                    Err(_) => {
+                        // This path satisfies multiple constraints. For now, don't
+                        // prefer any of them, and fall back on the default
+                        // specialization for this typevar.
+                        Ok(None)
+                    }
+                }
             }
         }
-        solutions.push(solution);
     }
-    solutions
 }
 
 impl InteriorNode {
@@ -3432,8 +3448,8 @@ impl InteriorNode {
                 return solutions;
             }
 
-            let path_bounds = compute_path_bounds(db, builder, interior);
-            let solutions = solve_paths(db, &path_bounds, default_solve);
+            let path_bounds = PathBounds::compute(db, builder, interior);
+            let solutions = path_bounds.solve(db);
 
             let mut storage = builder.storage.borrow_mut();
             storage.solutions_cache.insert(key, solutions);
@@ -3460,10 +3476,10 @@ impl InteriorNode {
             TypeVarVariance,
             Type<'db>,
             Type<'db>,
-        ) -> Option<Type<'db>>,
+        ) -> Result<Option<Type<'db>>, ()>,
     ) -> Solutions<Vec<Solution<'db>>> {
-        let path_bounds = compute_path_bounds(db, builder, self.node());
-        let solutions = solve_paths(db, &path_bounds, |db, bound_typevar, lower, upper| {
+        let path_bounds = PathBounds::compute(db, builder, self.node());
+        let solutions = path_bounds.solve_with(db, |db, bound_typevar, variance, lower, upper| {
             // When filtering by inferable typevars, skip non-inferable ones — they appear
             // due to BDD constraint reordering and should not be solved.
             if let Some(inferable) = inferable {
@@ -3472,25 +3488,7 @@ impl InteriorNode {
                 }
             }
 
-            // Determine variance from the constraint bounds:
-            // - Only upper bound (lower = Never) → covariant position
-            // - Only lower bound (upper = object) → contravariant position
-            // - Both bounds set → invariant position
-            let variance = if lower.is_never() {
-                TypeVarVariance::Covariant
-            } else if upper == Type::object() {
-                TypeVarVariance::Contravariant
-            } else {
-                TypeVarVariance::Invariant
-            };
-
-            if let Some(ty) = choose(bound_typevar, variance, lower, upper) {
-                return Ok(Some(TypeVarSolution {
-                    bound_typevar,
-                    solution: ty,
-                }));
-            }
-            default_solve(db, bound_typevar, lower, upper)
+            choose(bound_typevar, variance, lower, upper)
         });
         if solutions.is_empty() {
             return Solutions::Unsatisfiable;
diff --git a/crates/ty_python_semantic/src/types/infer/builder.rs b/crates/ty_python_semantic/src/types/infer/builder.rs
index df3f600cfa9d9..58c1d0cfc7516 100644
--- a/crates/ty_python_semantic/src/types/infer/builder.rs
+++ b/crates/ty_python_semantic/src/types/infer/builder.rs
@@ -57,7 +57,7 @@ use crate::types::class::{
     ClassLiteral, CodeGeneratorKind, DynamicClassAnchor, DynamicClassLiteral,
     DynamicMetaclassConflict, MethodDecorator,
 };
-use crate::types::constraints::{ConstraintSetBuilder, Solutions};
+use crate::types::constraints::{ConstraintSetBuilder, PathBounds, Solutions};
 use crate::types::context::InferContext;
 use crate::types::diagnostic::{
     self, CALL_NON_CALLABLE, CONFLICTING_DECLARATIONS, CYCLIC_CLASS_DEFINITION,
@@ -6087,13 +6087,13 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
                     db,
                     &constraints,
                     inferable,
-                    |typevar, variance, _lower, _upper| {
+                    |typevar, variance, lower, upper| {
                         let identity = typevar.identity(db);
                         elt_tcx_variance
                             .entry(identity)
                             .and_modify(|current| *current = current.join(variance))
                             .or_insert(variance);
-                        None // Use default solution selection
+                        PathBounds::default_solve(db, typevar, variance, lower, upper)
                     },
                 );
 

From 135b27a28bfc4a5f67d37e9cdf4dacb5ec21766f Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Mon, 23 Mar 2026 18:16:02 -0400
Subject: [PATCH 20/20] remove inferable parameter

---
 .../ty_python_semantic/src/types/call/bind.rs |  6 +++-
 .../src/types/constraints.rs                  | 32 ++++++-------------
 .../src/types/infer/builder.rs                |  6 +++-
 3 files changed, 19 insertions(+), 25 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/call/bind.rs b/crates/ty_python_semantic/src/types/call/bind.rs
index 99977b1580b05..d3f7e61f601bc 100644
--- a/crates/ty_python_semantic/src/types/call/bind.rs
+++ b/crates/ty_python_semantic/src/types/call/bind.rs
@@ -3800,12 +3800,16 @@ impl<'a, 'db> ArgumentTypeChecker<'a, 'db> {
                     constraints,
                     self.inferable_typevars,
                     |typevar, variance, lower, upper| {
+                        if !typevar.is_inferable(self.db, self.inferable_typevars) {
+                            return Ok(None);
+                        }
+
                         let identity = typevar.identity(self.db);
                         variance_map
                             .entry(identity)
                             .and_modify(|current| *current = current.join(variance))
                             .or_insert(variance);
-                        PathBounds::default_solve(self.db, typevar, variance, lower, upper)
+                        PathBounds::default_solve(self.db, typevar, lower, upper)
                     },
                 );
 
diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 0bb695362acc1..308bd1479ad52 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -661,8 +661,7 @@ impl<'db, 'c> ConstraintSet<'db, 'c> {
             return Solutions::Unsatisfiable;
         }
 
-        self.node
-            .solutions_with(db, builder, Some(inferable), choose)
+        self.node.solutions_with(db, builder, choose)
     }
 
     #[expect(dead_code)] // Keep this around for debugging purposes
@@ -1792,7 +1791,6 @@ impl NodeId {
         self,
         db: &'db dyn Db,
         builder: &ConstraintSetBuilder<'db>,
-        inferable: Option<InferableTypeVars<'_, 'db>>,
         choose: impl FnMut(
             BoundTypeVarInstance<'db>,
             TypeVarVariance,
@@ -1803,7 +1801,7 @@ impl NodeId {
         match self.node() {
             Node::AlwaysTrue => Solutions::Unconstrained,
             Node::AlwaysFalse => Solutions::Unsatisfiable,
-            Node::Interior(interior) => interior.solutions_with(db, builder, inferable, choose),
+            Node::Interior(interior) => interior.solutions_with(db, builder, choose),
         }
     }
 
@@ -2792,7 +2790,9 @@ impl<'db> PathBounds<'db> {
     }
 
     fn solve(&self, db: &'db dyn Db) -> Vec<Solution<'db>> {
-        self.solve_with(db, Self::default_solve)
+        self.solve_with(|bound_typevar, _variance, lower, upper| {
+            Self::default_solve(db, bound_typevar, lower, upper)
+        })
     }
 
     /// Solves each path by applying a per-typevar solver function, collecting valid solutions.
@@ -2803,9 +2803,7 @@ impl<'db> PathBounds<'db> {
     /// - `Err(())` to invalidate the entire path
     fn solve_with(
         &self,
-        db: &'db dyn Db,
-        mut solver: impl FnMut(
-            &'db dyn Db,
+        mut choose: impl FnMut(
             BoundTypeVarInstance<'db>,
             TypeVarVariance,
             Type<'db>,
@@ -2834,7 +2832,7 @@ impl<'db> PathBounds<'db> {
                     TypeVarVariance::Invariant
                 };
 
-                match solver(db, bound_typevar, variance, lower, upper) {
+                match choose(bound_typevar, variance, lower, upper) {
                     Ok(Some(ty)) => solution.push(TypeVarSolution {
                         bound_typevar,
                         solution: ty,
@@ -2858,7 +2856,6 @@ impl<'db> PathBounds<'db> {
     pub(crate) fn default_solve(
         db: &'db dyn Db,
         bound_typevar: BoundTypeVarInstance<'db>,
-        _variance: TypeVarVariance,
         lower: Type<'db>,
         upper: Type<'db>,
     ) -> Result<Option<Type<'db>>, ()> {
@@ -3470,8 +3467,7 @@ impl InteriorNode {
         self,
         db: &'db dyn Db,
         builder: &ConstraintSetBuilder<'db>,
-        inferable: Option<InferableTypeVars<'_, 'db>>,
-        mut choose: impl FnMut(
+        choose: impl FnMut(
             BoundTypeVarInstance<'db>,
             TypeVarVariance,
             Type<'db>,
@@ -3479,17 +3475,7 @@ impl InteriorNode {
         ) -> Result<Option<Type<'db>>, ()>,
     ) -> Solutions<Vec<Solution<'db>>> {
         let path_bounds = PathBounds::compute(db, builder, self.node());
-        let solutions = path_bounds.solve_with(db, |db, bound_typevar, variance, lower, upper| {
-            // When filtering by inferable typevars, skip non-inferable ones — they appear
-            // due to BDD constraint reordering and should not be solved.
-            if let Some(inferable) = inferable {
-                if !bound_typevar.is_inferable(db, inferable) {
-                    return Ok(None);
-                }
-            }
-
-            choose(bound_typevar, variance, lower, upper)
-        });
+        let solutions = path_bounds.solve_with(choose);
         if solutions.is_empty() {
             return Solutions::Unsatisfiable;
         }
diff --git a/crates/ty_python_semantic/src/types/infer/builder.rs b/crates/ty_python_semantic/src/types/infer/builder.rs
index 58c1d0cfc7516..4ee988aa9cad8 100644
--- a/crates/ty_python_semantic/src/types/infer/builder.rs
+++ b/crates/ty_python_semantic/src/types/infer/builder.rs
@@ -6088,12 +6088,16 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
                     &constraints,
                     inferable,
                     |typevar, variance, lower, upper| {
+                        if !typevar.is_inferable(db, inferable) {
+                            return Ok(None);
+                        }
+
                         let identity = typevar.identity(db);
                         elt_tcx_variance
                             .entry(identity)
                             .and_modify(|current| *current = current.join(variance))
                             .or_insert(variance);
-                        PathBounds::default_solve(db, typevar, variance, lower, upper)
+                        PathBounds::default_solve(db, typevar, lower, upper)
                     },
                 );