[ty] Use existential quantification to only consider inferable typevars (astral-sh#24383)

The `ConstraintSet::solutions` method returns a (set of) solutions for a
constraint set — assignments of specific types to each typevar in
question. astral-sh#23848 introduced two variants of this method. One of them
(`solutions_with_inferable`) would take in the set of `inferable`
typevars. This was used in a cycle check at the beginning of the method,
to make sure that we only considered the typevars we're actually solving
for when detecting a cyclic constraint set. More importantly, it was
also used to limit the result, so that we would only get solutions for
ther inferable typevars (i.e., the ones that we're using the constraint
set to solve for).

A cleaner approach is to use _extensional quantification_ to _remove_
the non-inferable typevars from the constraint set before calculating
solutions. We already had this available as a lower-level TDD method
(`abstract_one_inner`), which lets us provide an arbitrary
`should_remove` callback to determine which constraints to keep and
which to remove. We just need to add a new public API method that
provides a `should_remove` callback that keeps only the constraints
involving inferable typevars.

Given this change we can actually remove the cyclic checks completely,
since `SequentMap` and `PathAssignments` will already bottom out if they
encounter a cycle in the constraints. (Specifically, while we're walking
TDD paths, `PathAssignments` will only add constraints that aren't
already present in the current path.)

Author: dcreager

crates/ty_python_semantic/resources/mdtest/regression/2799_constraint_correlation.md

@@ -0,0 +1,52 @@
+# Regressions for correlated constraints
+
+This test exercises several regressions that stem from how our specialization inference does not
+always currently combine multiple constraints that we infer when calling a generic function.
+
+## Generic protocol overloads
+
+The generic protocol overload for `Series.mul` can infer multiple correlated specializations for
+`(T_contra, S2)`.
+
+TODO: We currently collapse those disjunctive solutions into independent unions in
+`SpecializationBuilder.types`, which can produce an impossible pair and reject the overload. This
+should be fixed once we are using a constraint set for our internal state.
+
+```toml
+[environment]
+python-version = "3.13"
+```
+
+```py
+from typing import Generic, Protocol, TypeVar, overload
+
+T = TypeVar("T")
+T_contra = TypeVar("T_contra")
+S2 = TypeVar("S2")
+
+class ElementOpsMixin(Generic[S2]):
+    @overload
+    def _proto_mul(self: "ElementOpsMixin[bool]", other: bool) -> "ElementOpsMixin[bool]": ...
+    @overload
+    def _proto_mul(self: "ElementOpsMixin[str]", other: str) -> "ElementOpsMixin[str]": ...
+    def _proto_mul(self, other):
+        raise NotImplementedError
+
+class Supports_ProtoMul(Protocol[T_contra, S2]):
+    def _proto_mul(self, other: T_contra, /) -> ElementOpsMixin[S2]: ...
+
+class Series(ElementOpsMixin[T], Generic[T]):
+    @overload
+    def mul(self: Supports_ProtoMul[T_contra, S2], other: T_contra) -> "Series[S2]": ...
+    @overload
+    def mul(self: "Series[int]", other: int) -> "Series[int]": ...
+    def mul(self, other):
+        raise NotImplementedError
+
+def _(left: Series[bool]):
+    # TODO: no error
+    # TODO: revealed: Series[bool]
+    # error: [no-matching-overload]
+    # revealed: Unknown
+    reveal_type(left.mul(True))
+```

crates/ty_python_semantic/src/types/call/bind.rs

@@ -4340,29 +4340,23 @@ impl<'a, 'db> ArgumentTypeChecker<'a, '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);
+                let set = return_ty
+                    .when_constraint_set_assignable_to(self.db, tcx, constraints)
+                    .remove_noninferable(self.db, 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, variance, lower, upper| {
-                        if !typevar.is_inferable(self.db, self.inferable_typevars) {
-                            return Ok(None);
-                        }
-
+                let solutions =
+                    set.solutions_with(self.db, constraints, |typevar, variance, lower, upper| {
                         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, lower, upper)
-                    },
-                );
+                        PathBounds::default_solve(self.db, constraints, typevar, lower, upper)
+                    });
 
                 let Solutions::Constrained(solutions) = solutions else {
                     return None;