[π] Preserve main-compatible relevant non-inferable solution bindings
diff --git a/crates/ty_python_semantic/resources/mdtest/bidirectional.md b/crates/ty_python_semantic/resources/mdtest/bidirectional.md
index 0c762ae..327eb94 100644
--- a/crates/ty_python_semantic/resources/mdtest/bidirectional.md
+++ b/crates/ty_python_semantic/resources/mdtest/bidirectional.md
@@ -832,9 +832,7 @@
 ## Covariant constructors with outer return contexts
 
 A bounded, defaulted, covariant constructor should use its outer return context instead of falling
-back to its declared default. These false positives are pending
-[#26680](https://github.com/astral-sh/ruff/pull/26680), which will conjoin contextual return
-constraints with argument constraints before solving.
+back to its declared default.
 
 ```py
 from __future__ import annotations
@@ -844,8 +842,6 @@
 
 class Client:
     def no_argument(self) -> EmptyBox[Self]:
-        # TODO(#26680): no error
-        # error: [invalid-return-type] "expected `EmptyBox[Self@no_argument]`, found `EmptyBox[Client]`"
         return EmptyBox()
 
 T = TypeVar("T", bound=Client, default=Client, covariant=True)
@@ -856,8 +852,6 @@
 
 class Holder(Generic[T]):
     def related(self) -> RelatedBox[T]:
-        # TODO(#26680): no error
-        # error: [invalid-return-type] "expected `RelatedBox[T@Holder]`, found `RelatedBox[Client]`"
         return RelatedBox(self)
 
 class RelatedBox(Generic[T]):
@@ -868,8 +862,7 @@
 ## Dataclass constructors with outer return contexts
 
 A covariant dataclass argument referring to outer `Self` should not specialize to its declared
-default. The resulting return and argument false positives are pending
-[#26680](https://github.com/astral-sh/ruff/pull/26680).
+default.
 
 ```py
 from __future__ import annotations
@@ -880,11 +873,7 @@
 
 class PartialUser:
     def equipped(self, present: bool) -> Equipped[Self]:
-        # TODO(#26680): no error
-        # error: [invalid-return-type]
         return Equipped(
-            # TODO(#26680): no error
-            # error: [invalid-argument-type] "Expected `Item[User] | None`, found `Item[Self@equipped] | None`"
             first=Item(self) if present else None,
         )
 
@@ -929,8 +918,7 @@
 ## Iterable constructors retain contextual outer element types
 
 After narrowing `Iterable[T] | T`, a `list` constructor should retain the outer `T` instead of
-inferring `object`. This false-positive return diagnostic is also pending
-[#26680](https://github.com/astral-sh/ruff/pull/26680).
+inferring `object`.
 
 ```py
 from collections.abc import Collection, Iterable, Sized
@@ -938,8 +926,6 @@
 
 def maybe_iterable_to_list[T](value: Iterable[T] | T) -> Collection[T] | T:
     if isinstance(value, Iterable) and not isinstance(value, Sized):
-        # TODO(#26680): no error
-        # error: [invalid-return-type] "found `list[object]`"
         return list(value)
     value = cast(Collection[T], value)
     return value
@@ -949,8 +935,7 @@
 
 A constrained outer return type should remain visible in an invalid callback diagnostic. The
 callback itself is still invalid, but replacing its expected result with `Unknown` loses useful
-information. Restoring the outer result is pending
-[#26680](https://github.com/astral-sh/ruff/pull/26680).
+information.
 
 ```py
 from collections.abc import Callable
@@ -968,19 +953,15 @@
         self.callback = callback
 
     def view(self) -> CallbackView[C]:
-        # TODO(#26680): no [invalid-return-type] error
-        # TODO(#26680): error: [invalid-argument-type] "Expected `(int, /) -> C@CallbackInterface`, found `Selector@__init__`"
-        # error: [invalid-return-type]
-        # error: [invalid-argument-type] "Expected `(int, /) -> Unknown`, found `Selector@__init__`"
+        # error: [invalid-argument-type] "Expected `(int, /) -> C@CallbackInterface`, found `Selector@__init__`"
         return CallbackView(self.callback)
 ```
 
 ## Callable factories retain contextual outer element types
 
 Narrowing a union to a callable should not replace its outer iterable element type with `Unknown`.
-The factory argument remains invalid, but its expected result should preserve the outer `CT`. Its
-correct diagnostic is pending [#26680](https://github.com/astral-sh/ruff/pull/26680); the separate
-narrowed-sequence constructor must remain valid.
+The factory argument remains invalid, but its expected result should preserve the outer `CT`. The
+narrowed sequence should also retain its outer element type.
 
 ```py
 from collections.abc import Callable, Iterable, Iterator, Sequence
@@ -1005,10 +986,7 @@
 
 def build_iter_view(matches: Iterable[CT] | Callable[[], Iterable[CT]]) -> Iterable[CT]:
     if callable(matches):
-        # TODO(#26680): no [invalid-return-type] error
-        # TODO(#26680): error: [invalid-argument-type] "Expected `() -> Iterable[CT@built_iter_view]`"
-        # error: [invalid-return-type]
-        # error: [invalid-argument-type] "Expected `() -> Iterable[Unknown]`"
+        # error: [invalid-argument-type] "Expected `() -> Iterable[CT@build_iter_view]`"
         return FactoryView(matches)
     if not isinstance(matches, Sequence):
         matches = list(matches)
diff --git a/crates/ty_python_semantic/resources/mdtest/generics/legacy/callables.md b/crates/ty_python_semantic/resources/mdtest/generics/legacy/callables.md
index 31ea3b6..13abc38 100644
--- a/crates/ty_python_semantic/resources/mdtest/generics/legacy/callables.md
+++ b/crates/ty_python_semantic/resources/mdtest/generics/legacy/callables.md
@@ -423,16 +423,15 @@
 assert_type(infer_return(callback), object)
 ```
 
-## Generic inference after projection budget exhaustion
+## Generic inference with many partially annotated overloads
 
-The literal-specific overloads below produce more alternative bindings than generic inference can
-project within its limits. The precise type of `default=0` does not replace the missing callback
-evidence: we recover with `Unknown` in either argument order.
+The literal-specific overloads below do not require enumerating irrelevant combinations of bindings.
+Generic inference retains the catch-all overload's `object` return type even when the default has a
+more precise type, regardless of argument order.
 
 ```py
 from typing import Callable, Literal, TypeVar, overload
 from typing_extensions import assert_type
-from ty_extensions._internal import Unknown
 
 R = TypeVar("R")
 T = TypeVar("T")
@@ -471,8 +470,8 @@
 def callback(value):
     raise NotImplementedError
 
-assert_type(infer_return(callback, 0), Unknown)
-assert_type(infer_return(default=0, callback=callback), Unknown)
+assert_type(infer_return(callback, 0), object)
+assert_type(infer_return(default=0, callback=callback), object)
 ```
 
 ## Multiple occurrences of a higher-order generic callable
diff --git a/crates/ty_python_semantic/resources/mdtest/regression/constraint_set_ordering.md b/crates/ty_python_semantic/resources/mdtest/regression/constraint_set_ordering.md
index 4ecc307..52aedc6 100644
--- a/crates/ty_python_semantic/resources/mdtest/regression/constraint_set_ordering.md
+++ b/crates/ty_python_semantic/resources/mdtest/regression/constraint_set_ordering.md
@@ -221,8 +221,8 @@
 ## Non-inferable constraint source order and typevar orientation
 
 A non-inferable constraint can appear before or after inferable constraints, and a bare relationship
-can be encoded with either variable as its subject. None of those representation choices should
-change which type variables are returned.
+can be encoded with either variable as its subject. Unrelated non-inferable variables are omitted,
+but a directly related non-inferable variable must be retained regardless of its orientation.
 
 ```py
 from ty_extensions._internal import ConstraintSet
@@ -239,20 +239,20 @@
 
 def inferable_subject[I, N]() -> None:
     constraints = ConstraintSet.range(N, I, N)
-    # revealed: tuple[Solution[I=N@inferable_subject]]
+    # revealed: tuple[Solution[N=I@inferable_subject, I=N@inferable_subject]]
     reveal_type(constraints.solutions(inferable=tuple[I]))
 
 def noninferable_subject[N, I]() -> None:
     constraints = ConstraintSet.range(I, N, I)
-    # revealed: tuple[Solution[I=N@noninferable_subject]]
+    # revealed: tuple[Solution[I=N@noninferable_subject, N=I@noninferable_subject]]
     reveal_type(constraints.solutions(inferable=tuple[I]))
 ```
 
 ## Abstraction and non-inferable typevars
 
-Non-inferable typevars must not appear in reported solution bindings, and irrelevant positive
-decisions must not leak onto independent alternatives. Universal abstraction of an alternative must
-likewise leave only the unrelated branch.
+Irrelevant non-inferable typevars must not appear in reported solution bindings, and irrelevant
+positive decisions must not leak onto independent alternatives. Universal abstraction of an
+alternative must likewise leave only the unrelated branch.
 
 ```py
 from ty_extensions import static_assert
diff --git a/crates/ty_python_semantic/resources/mdtest/regression/noninferable_projection_to_terminal.md b/crates/ty_python_semantic/resources/mdtest/regression/noninferable_projection_to_terminal.md
index 6d54bad..a496268 100644
--- a/crates/ty_python_semantic/resources/mdtest/regression/noninferable_projection_to_terminal.md
+++ b/crates/ty_python_semantic/resources/mdtest/regression/noninferable_projection_to_terminal.md
@@ -141,7 +141,7 @@
     async def __aenter__(self) -> T:
         # TODO(#26680): Keep the return error, but report `Response | (T@Manager & Socket)`.
         # TODO(#26680): Remove both invalid-argument-type errors.
-        # error: [invalid-return-type] "expected `T@Manager`, found `Response | Unknown`"
+        # error: [invalid-return-type] "expected `T@Manager`, found `Response | T@Manager`"
         # error: [invalid-argument-type]
         # error: [invalid-argument-type]
         return await self.response.__aenter__()
diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md b/crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md
index 87ac6b5..38dcd22 100644
--- a/crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md
+++ b/crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md
@@ -1043,8 +1043,9 @@
 ### Symbolic relationships and fixed non-inferable bindings
 
 A bare relationship must have the same meaning regardless of which type variable the TDD chooses as
-its constraint subject. An explicit exact constraint fixes a non-inferable variable to a concrete
-type; a one-sided bound does not.
+its constraint subject. Directly related non-inferable variables retain their reverse bindings,
+while unrelated non-inferable constraints do not. An explicit exact constraint fixes a non-inferable
+variable to a concrete type; a one-sided bound does not.
 
 ```py
 from typing import Any, Never
@@ -1052,18 +1053,18 @@
 
 def symbolic_relationship[I, N]() -> None:
     constraints = ConstraintSet.range(N, I, N)
-    # revealed: tuple[Solution[I=N@symbolic_relationship]]
+    # revealed: tuple[Solution[N=I@symbolic_relationship, I=N@symbolic_relationship]]
     reveal_type(constraints.solutions(inferable=tuple[I]))
 
 def symbolic_relationship_reversed[N, I]() -> None:
     constraints = ConstraintSet.range(N, I, N)
-    # revealed: tuple[Solution[I=N@symbolic_relationship_reversed]]
+    # revealed: tuple[Solution[N=I@symbolic_relationship_reversed, I=N@symbolic_relationship_reversed]]
     reveal_type(constraints.solutions(inferable=tuple[I]))
 
 def fixed_noninferable[I, N]() -> None:
     constraints = ConstraintSet.range(int, N, int) & ConstraintSet.range(N, I, N)
     # TODO: revealed: tuple[Solution[I=int]]
-    # revealed: tuple[Solution[I=int | N@fixed_noninferable]]
+    # revealed: tuple[Solution[I=int | N@fixed_noninferable, N=I@fixed_noninferable]]
     reveal_type(constraints.solutions(inferable=tuple[I]))
 
 def fixed_nested_noninferable[I, N]() -> None:
@@ -1074,12 +1075,12 @@
 
 def gradual_noninferable_any[I, N]() -> None:
     constraints = ConstraintSet.range(Any, N, Any) & ConstraintSet.range(N, I, N)
-    # revealed: tuple[Solution[I=Any | N@gradual_noninferable_any]]
+    # revealed: tuple[Solution[I=Any | N@gradual_noninferable_any, N=I@gradual_noninferable_any]]
     reveal_type(constraints.solutions(inferable=tuple[I]))
 
 def gradual_noninferable_unknown[I, N]() -> None:
     constraints = ConstraintSet.range(Unknown, N, Unknown) & ConstraintSet.range(N, I, N)
-    # revealed: tuple[Solution[I=Unknown | N@gradual_noninferable_unknown]]
+    # revealed: tuple[Solution[I=Unknown | N@gradual_noninferable_unknown, N=I@gradual_noninferable_unknown]]
     reveal_type(constraints.solutions(inferable=tuple[I]))
 
 def lower_bounded_noninferable[I, N]() -> None:
@@ -1090,7 +1091,7 @@
 
 def upper_bounded_noninferable[I, N]() -> None:
     constraints = ConstraintSet.range(Never, N, int) & ConstraintSet.range(N, I, N)
-    # revealed: tuple[Solution[I=N@upper_bounded_noninferable]]
+    # revealed: tuple[Solution[I=N@upper_bounded_noninferable, N=I@upper_bounded_noninferable]]
     reveal_type(constraints.solutions(inferable=tuple[I]))
 ```
 
diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 461e6ac..4665144 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -4871,7 +4871,16 @@
                 .expect("every BDD constraint should have a source-order entry")
         });
 
-        if !self.node().is_single_conjunction(storage) {
+        // Concrete alternatives cannot introduce relationships between distinct typevars, so
+        // they can use the same independence optimization as a single conjunction.
+        if !self.node().is_single_conjunction(storage)
+            && constraints.iter().any(|constraint| {
+                !storage
+                    .constraint_data(*constraint)
+                    .bounds
+                    .is_concrete(db, env)
+            })
+        {
             return PathAssignments::new(constraints, FxHashSet::default());
         }
 
@@ -9562,6 +9571,7 @@
         let t_int = create_constraint(db, &builder, t, KnownClass::Int);
         let t_str = create_constraint(db, &builder, t, KnownClass::Str);
         let set = t_int.or(db, &builder, || t_str);
+        let inferable = TypeVarSet::from_typevars(db, [t]);
         let source_orders = builder
             .storage
             .borrow()
@@ -9571,7 +9581,7 @@
             &env,
             &mut builder.storage.borrow_mut(),
             set.node,
-            TypeVarSet::from_typevars(db, [t]),
+            inferable,
             set.source_order,
         );
 
@@ -9587,7 +9597,8 @@
                 remaining_paths,
                 remaining_visits,
             };
-            let mut walker = SolutionWalker::new(source_orders.clone());
+            let mut walker =
+                SolutionWalker::new(db, &mut storage, inferable, source_orders.clone());
             assert_eq!(
                 walker.visit_node(db, &env, &mut storage, &mut path, set.node, &mut limits),
                 ControlFlow::Break(error)
@@ -9595,7 +9606,8 @@
             drop(walker);
 
             let mut limits = UnboundedSolutionLimits;
-            let mut walker = SolutionWalker::new(source_orders.clone());
+            let mut walker =
+                SolutionWalker::new(db, &mut storage, inferable, source_orders.clone());
             let ControlFlow::Continue(()) =
                 walker.visit_node(db, &env, &mut storage, &mut path, set.node, &mut limits);
             assert_eq!(walker.finish(db, &env, &mut storage), expected);
diff --git a/crates/ty_python_semantic/src/types/constraints/solutions.rs b/crates/ty_python_semantic/src/types/constraints/solutions.rs
index 6ed6a89..0f62946 100644
--- a/crates/ty_python_semantic/src/types/constraints/solutions.rs
+++ b/crates/ty_python_semantic/src/types/constraints/solutions.rs
@@ -4,7 +4,7 @@
 
 use crate::types::constraints::support::Support;
 use crate::types::constraints::{
-    ALWAYS_FALSE, ConstraintAssignment, ConstraintBoundsBuilder, ConstraintId,
+    ALWAYS_FALSE, ConstraintAssignment, ConstraintBound, ConstraintBoundsBuilder, ConstraintId,
     ConstraintSetStorage, Node, NodeId, PathAssignments, PathBounds, SolutionLimits,
 };
 use crate::types::typevar::TypeVarSet;
@@ -111,7 +111,7 @@
             // This node cannot affect the solution we've found. Make sure that the node has _at
             // least one_ satisfiable path, without walking them all. As long as it does, we can
             // report the solution we have so far as-is.
-            if Self::node_is_satisfiable_on_path(db, env, storage, path, node) {
+            if Self::node_is_satisfiable_on_path(db, env, storage, path, node, limits)? {
                 limits.satisfied_path()?;
                 self.found_satisfied_path(storage, path, &visible_typevars);
             }
@@ -145,68 +145,47 @@
     /// Returns if there is _any_ satisfiable path in `node`, assuming that the assignments in
     /// `path` already hold. Avoids walking the entire subtree if possible, by returning early once
     /// we find the first satisfied path.
-    fn node_is_satisfiable_on_path(
+    fn node_is_satisfiable_on_path<L: SolutionLimits>(
         db: &'db dyn Db,
         env: &ProgramEnvironment<'db>,
         storage: &mut ConstraintSetStorage<'db>,
         path: &mut PathAssignments,
         node: NodeId,
-    ) -> bool {
+        limits: &mut L,
+    ) -> ControlFlow<L::Break, bool> {
         match node.node() {
-            Node::AlwaysTrue => return true,
-            Node::AlwaysFalse => return false,
+            Node::AlwaysTrue => return ControlFlow::Continue(true),
+            Node::AlwaysFalse => return ControlFlow::Continue(false),
             Node::Interior(_) => {}
         }
 
         let interior = storage.interior_node_data(node);
+        let constraint = interior.constraint;
+        for (assignment, child) in [
+            (constraint.when_true(), interior.if_true),
+            (constraint.when_unconstrained(), interior.if_uncertain),
+            (constraint.when_false(), interior.if_false),
+        ] {
+            let is_satisfied = path.walk_edge(
+                db,
+                env,
+                storage,
+                assignment,
+                |storage, path, _new_range, found_conflict| {
+                    if found_conflict {
+                        return ControlFlow::Continue(false);
+                    }
 
-        let true_is_satisfied = path.walk_edge(
-            db,
-            env,
-            storage,
-            interior.constraint.when_true(),
-            |storage, path, _new_range, found_conflict| {
-                if found_conflict {
-                    false
-                } else {
-                    Self::node_is_satisfiable_on_path(db, env, storage, path, interior.if_true)
-                }
-            },
-        );
-        if true_is_satisfied {
-            return true;
+                    limits.visit_node()?;
+                    Self::node_is_satisfiable_on_path(db, env, storage, path, child, limits)
+                },
+            )?;
+            if is_satisfied {
+                return ControlFlow::Continue(true);
+            }
         }
 
-        let uncertain_is_satisfied = path.walk_edge(
-            db,
-            env,
-            storage,
-            interior.constraint.when_unconstrained(),
-            |storage, path, _new_range, found_conflict| {
-                if found_conflict {
-                    false
-                } else {
-                    Self::node_is_satisfiable_on_path(db, env, storage, path, interior.if_uncertain)
-                }
-            },
-        );
-        if uncertain_is_satisfied {
-            return true;
-        }
-
-        path.walk_edge(
-            db,
-            env,
-            storage,
-            interior.constraint.when_false(),
-            |storage, path, _new_range, found_conflict| {
-                if found_conflict {
-                    false
-                } else {
-                    Self::node_is_satisfiable_on_path(db, env, storage, path, interior.if_false)
-                }
-            },
-        )
+        ControlFlow::Continue(false)
     }
 
     fn found_satisfied_path(
@@ -226,6 +205,11 @@
                     (assignment.constraint(), source_order)
                 })
                 .collect();
+        // 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 `PathAssignments` 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.
         path.sort_by_key(|(_, source_order)| *source_order);
         self.sorted_paths.push(path);
     }
@@ -255,35 +239,52 @@
         let mut any_constrained_solutions = false;
         let mut mappings: FxIndexMap<BoundTypeVarInstance<'db>, ConstraintBoundsBuilder<'db>> =
             FxIndexMap::default();
+        let is_bare_inferable_typevar = |bound: ConstraintBound<'db>| {
+            matches!(
+                bound,
+                ConstraintBound::Evidence(Type::TypeVar(typevar))
+                    if typevar.is_inferable(db, self.inferable)
+            )
+        };
 
         for path in self.sorted_paths {
             mappings.clear();
             for (constraint, _) in path {
                 let constraint = storage.constraint_data(constraint);
                 let typevar = constraint.typevar;
-                if let Some(lower) = constraint.bounds.lower {
-                    if typevar.is_inferable(db, self.inferable) {
-                        let bounds = mappings.entry(typevar).or_default();
-                        bounds.add_lower(db, env, lower);
-                    }
 
-                    if let Type::TypeVar(lower_bound_typevar) = lower.ty()
-                        && lower_bound_typevar.is_inferable(db, self.inferable)
-                    {
+                // A direct relationship between an inferable and non-inferable typevar must
+                // contribute bounds for both endpoints. Contextual inference relies on the
+                // reverse, non-inferable binding to preserve relationships to outer typevars.
+                // Constraints on unrelated non-inferable typevars must not contribute bindings.
+                if !typevar.is_inferable(db, self.inferable)
+                    && !constraint
+                        .bounds
+                        .lower
+                        .is_some_and(is_bare_inferable_typevar)
+                    && !constraint
+                        .bounds
+                        .upper
+                        .is_some_and(is_bare_inferable_typevar)
+                {
+                    continue;
+                }
+
+                if let Some(lower) = constraint.bounds.lower {
+                    let bounds = mappings.entry(typevar).or_default();
+                    bounds.add_lower(db, env, lower);
+
+                    if let Type::TypeVar(lower_bound_typevar) = lower.ty() {
                         let bounds = mappings.entry(lower_bound_typevar).or_default();
                         bounds.add_upper(db, env, lower.with_type(Type::TypeVar(typevar)));
                     }
                 }
 
                 if let Some(upper) = constraint.bounds.upper {
-                    if typevar.is_inferable(db, self.inferable) {
-                        let bounds = mappings.entry(typevar).or_default();
-                        bounds.add_upper(db, env, upper);
-                    }
+                    let bounds = mappings.entry(typevar).or_default();
+                    bounds.add_upper(db, env, upper);
 
-                    if let Type::TypeVar(upper_bound_typevar) = upper.ty()
-                        && upper_bound_typevar.is_inferable(db, self.inferable)
-                    {
+                    if let Type::TypeVar(upper_bound_typevar) = upper.ty() {
                         let bounds = mappings.entry(upper_bound_typevar).or_default();
                         bounds.add_lower(db, env, upper.with_type(Type::TypeVar(typevar)));
                     }