do not prefer trivially true candidates with -Znext-solver

compiler/rustc_next_trait_solver/src/solve/assembly/mod.rs

@@ -1340,7 +1340,7 @@ where
                     candidates.retain(|c| matches!(c.source, CandidateSource::ParamEnv(_)));
                 }
 
-                if let Some((response, _)) = self.try_merge_candidates(&candidates) {
+                if let Some(response) = self.try_merge_candidates(&candidates) {
                     Ok(response)
                 } else {
                     self.flounder(&candidates).map_err(Into::into)
@@ -1362,7 +1362,7 @@ where
                 // means we can just ignore inference constraints and don't have to special-case
                 // constraining the normalized-to `term`.
                 self.filter_specialized_impls(AllowInferenceConstraints::Yes, &mut candidates);
-                if let Some((response, _)) = self.try_merge_candidates(&candidates) {
+                if let Some(response) = self.try_merge_candidates(&candidates) {
                     Ok(response)
                 } else {
                     self.flounder(&candidates).map_err(Into::into)

compiler/rustc_next_trait_solver/src/solve/mod.rs

@@ -25,7 +25,10 @@ use rustc_type_ir::inherent::*;
 use rustc_type_ir::lang_items::SolverTraitLangItem;
 pub use rustc_type_ir::solve::*;
 use rustc_type_ir::transmute::Condition;
-use rustc_type_ir::{self as ty, Const, Interner, Region, TraitClause, TypeVisitableExt, Upcast};
+use rustc_type_ir::{
+    self as ty, BoundVarIndexKind, Const, Interner, Region, TraitClause, TypeFlags,
+    TypeSuperVisitable, TypeVisitable, TypeVisitableExt, TypeVisitor, Upcast,
+};
 use thin_vec::{ThinVec, thin_vec};
 use tracing::instrument;
 
@@ -89,25 +92,107 @@ fn equal_response_modulo_region_constraints<I: Interner>(
     b: &CanonicalResponse<I>,
 ) -> bool {
     let CanonicalResponse {
-        max_universe: a_max_universe,
-        var_kinds: a_var_kinds,
-        value:
-            Response {
-                var_values: a_var_values,
-                certainty: a_certainty,
-                external_constraints: a_external_constraints,
-            },
+        max_universe: _, // implied by `var_kinds` being equal.
+        var_kinds,
+        value: Response { var_values, certainty, external_constraints },
     } = a;
 
     let ExternalConstraintsData { region_constraints: _, opaque_types, normalization_nested_goals } =
-        &**a_external_constraints;
+        &**external_constraints;
 
-    a_max_universe == &b.max_universe
-        && a_var_kinds == &b.var_kinds
-        && a_var_values == &b.value.var_values
-        && a_certainty == &b.value.certainty
+    let eq_up_to_var_kinds = var_values == &b.value.var_values
+        && certainty == &b.value.certainty
         && opaque_types == &b.value.external_constraints.opaque_types
-        && normalization_nested_goals == &b.value.external_constraints.normalization_nested_goals
+        && normalization_nested_goals == &b.value.external_constraints.normalization_nested_goals;
+
+    if !eq_up_to_var_kinds {
+        return false;
+    }
+
+    if var_kinds == &b.var_kinds {
+        true
+    } else {
+        // If only the `var_kinds` are different, we have to check whether they only
+        // differ due to region constraints.
+        //
+        // FIXME: This is only only sufficient if region constraints are canonicalized
+        // last, which they are not. This means this check incorrectly returns `false` if
+        // either the `opaque_types` or `normalization_nested_goals` reference variables
+        // not mentioned before. The only way this happens is if they mention placeholders
+        // or higher-ranked existential variables created inside of the query. This feels
+        // very unlikely and maybe not even worth fixing.
+        let num_shared: usize =
+            var_kinds.iter().zip(b.var_kinds.iter()).take_while(|(a, b)| a == b).count();
+        response_only_references_shared_vars_outside_of_region_constraints(num_shared, a)
+            && response_only_references_shared_vars_outside_of_region_constraints(num_shared, b)
+    }
+}
+
+/// This is slightly hacky. If responses differ in their `var_values`, then even if their
+/// `opaque_types` are structurally equal, they could still be different because the
+/// same `var_value` maps to a different value when instantiating the response.
+///
+/// To handle this, we make sure that everything but the region constraints only reference
+/// `var_values` which are the same for both responses.
+fn response_only_references_shared_vars_outside_of_region_constraints<I: Interner>(
+    num_shared: usize,
+    response: &CanonicalResponse<I>,
+) -> bool {
+    struct OnlyReferencesSharedVars {
+        num_shared: usize,
+    }
+    impl<I: Interner> TypeVisitor<I> for OnlyReferencesSharedVars {
+        type Result = Result<(), ()>;
+
+        fn visit_ty(&mut self, t: I::Ty) -> Result<(), ()> {
+            if let ty::Bound(BoundVarIndexKind::Canonical, b) = t.kind() {
+                if b.var.as_usize() >= self.num_shared { Err(()) } else { Ok(()) }
+            } else if t.has_type_flags(TypeFlags::HAS_CANONICAL_BOUND) {
+                t.super_visit_with(self)
+            } else {
+                Ok(())
+            }
+        }
+
+        fn visit_region(&mut self, r: Region<I>) -> Result<(), ()> {
+            if let ty::ReBound(BoundVarIndexKind::Canonical, b) = r.kind() {
+                if b.var.as_usize() >= self.num_shared { Err(()) } else { Ok(()) }
+            } else {
+                Ok(())
+            }
+        }
+
+        fn visit_const(&mut self, c: Const<I>) -> Result<(), ()> {
+            if let ty::ConstKind::Bound(BoundVarIndexKind::Canonical, b) = c.kind() {
+                if b.var.as_usize() >= self.num_shared { Err(()) } else { Ok(()) }
+            } else if c.has_type_flags(TypeFlags::HAS_CANONICAL_BOUND) {
+                c.super_visit_with(self)
+            } else {
+                Ok(())
+            }
+        }
+
+        fn visit_predicate<P: rustc_type_ir::PredicateProxy<I>>(&mut self, p: P) -> Result<(), ()> {
+            if p.has_type_flags(TypeFlags::HAS_CANONICAL_BOUND) {
+                p.super_visit_with(self)
+            } else {
+                Ok(())
+            }
+        }
+    }
+
+    let CanonicalResponse {
+        max_universe: _,
+        var_kinds: _,
+        value: Response { var_values, certainty: _, external_constraints },
+    } = response;
+    let ExternalConstraintsData { region_constraints: _, opaque_types, normalization_nested_goals } =
+        &**external_constraints;
+
+    let mut visitor = OnlyReferencesSharedVars { num_shared };
+    var_values.visit_with(&mut visitor).is_ok()
+        && opaque_types.visit_with(&mut visitor).is_ok()
+        && normalization_nested_goals.visit_with(&mut visitor).is_ok()
 }
 
 impl<'a, D, I> EvalCtxt<'a, D>
@@ -322,66 +407,50 @@ where
     }
 }
 
-#[derive(Debug)]
-enum MergeCandidateInfo {
-    AlwaysApplicable(usize),
-    EqualResponse,
-}
-
 impl<D, I> EvalCtxt<'_, D>
 where
     D: SolverDelegate<Interner = I>,
     I: Interner,
 {
     /// Try to merge multiple possible ways to prove a goal, if that is not possible returns `None`.
+    /// We only merge candidates which are equal modulo region constraints. Long-term, we want to
+    /// emit an OR of the constraints of all candidates, for now we fail with ambiguity unless all
+    /// candidates have the same constraints or one candidate has no region constraints at all.
     ///
     /// In this case we tend to flounder and return ambiguity by calling `[EvalCtxt::flounder]`.
     #[instrument(level = "trace", skip(self), ret)]
     fn try_merge_candidates(
         &mut self,
         candidates: &[Candidate<I>],
-    ) -> Option<(CanonicalResponse<I>, MergeCandidateInfo)> {
-        if candidates.is_empty() {
+    ) -> Option<CanonicalResponse<I>> {
+        let Some((first, rest)) = candidates.split_first() else {
             return None;
-        }
-
-        let always_applicable = candidates.iter().enumerate().find(|(_, candidate)| {
-            candidate.result.value.certainty == Certainty::Yes
-                && has_no_inference_or_external_constraints(candidate.result)
-        });
+        };
 
-        if let Some((i, candidate)) = always_applicable {
-            return Some((candidate.result, MergeCandidateInfo::AlwaysApplicable(i)));
+        // Check whether all candidates are equal modulo regions.
+        if rest.iter().any(|candidate| {
+            !equal_response_modulo_region_constraints(&first.result, &candidate.result)
+        }) {
+            return None;
         }
 
-        let one: CanonicalResponse<I> = candidates[0].result;
-
-        if candidates[1..]
-            .iter()
-            .all(|candidate| equal_response_modulo_region_constraints(&one, &candidate.result))
-        {
-            let region_constraints = &one.value.external_constraints.region_constraints;
-            if candidates[1..].iter().all(|candidate| {
-                &candidate.result.value.external_constraints.region_constraints
-                    == region_constraints
-            }) {
-                return Some((one, MergeCandidateInfo::EqualResponse));
-            }
-
-            // If candidates differ only in region constraints, their merged region
-            // constraints are an `Or` of their respective constraints. If one of them
-            // has no region constraints, the `Or` constraint evaluates to `true`.
-            //
-            // This is a special case of `-Zassumptions-on-binders` and should be
-            // replaced eventually.
-            if let Some(candidate) = candidates.iter().find(|candidate| {
-                candidate.result.value.external_constraints.region_constraints.is_empty()
-            }) {
-                return Some((candidate.result, MergeCandidateInfo::EqualResponse));
-            }
+        // Merging constraints is trivial if they are same.
+        let region_constraints = &first.result.value.external_constraints.region_constraints;
+        if candidates[1..].iter().all(|candidate| {
+            &candidate.result.value.external_constraints.region_constraints == region_constraints
+        }) {
+            return Some(first.result);
         }
 
-        None
+        // If candidates differ only in region constraints, their merged region
+        // constraints are an OR of their respective constraints. We don't support
+        // OR constraints yet, so the only way we can merge differing candidates
+        // if one of them has no region constraints as then the OR constraint
+        // is trivially true.
+        candidates
+            .iter()
+            .find(|c| c.result.value.external_constraints.region_constraints.is_empty())
+            .map(|c| c.result)
     }
 
     fn bail_with_ambiguity(&mut self, candidates: &[Candidate<I>]) -> CanonicalResponse<I> {

compiler/rustc_next_trait_solver/src/solve/trait_goals.rs

@@ -24,7 +24,7 @@ use crate::solve::assembly::{
 use crate::solve::inspect::ProbeKind;
 use crate::solve::{
     BuiltinImplSource, CandidateSource, Certainty, EvalCtxt, Goal, GoalSource, MaybeCause,
-    MergeCandidateInfo, NoSolution, ParamEnvSource, StalledOnCoroutines, flatten_answer_tree,
+    NoSolution, ParamEnvSource, StalledOnCoroutines, flatten_answer_tree,
     has_only_region_constraints,
 };
 
@@ -1600,7 +1600,7 @@ where
             .all(|candidate| matches!(candidate.source, CandidateSource::BuiltinImpl(_)));
 
         if is_marker || all_builtin {
-            self.try_merge_candidates(candidates).map(|(response, _)| response)
+            self.try_merge_candidates(candidates)
         } else if candidates.len() > 1 {
             None
         } else {
@@ -1613,7 +1613,7 @@ where
         candidates: &[Candidate<I>],
         proven_via: TraitGoalProvenVia,
     ) -> (CanonicalResponse<I>, Option<TraitGoalProvenVia>) {
-        if let Some((response, _)) = self.try_merge_candidates(candidates) {
+        if let Some(response) = self.try_merge_candidates(candidates) {
             (response, Some(proven_via))
         } else {
             (self.bail_with_ambiguity(candidates), None)
@@ -1678,6 +1678,7 @@ where
             let alias_bounds: Vec<_> = candidates
                 .extract_if(.., |c| matches!(c.source, CandidateSource::AliasBound(..)))
                 .collect();
+            candidates.into_iter().for_each(|c| self.ignore_candidate_head_usages(c.head_usages));
             return Ok(self.merge_candidates_or_bail_with_ambiguity(
                 &alias_bounds,
                 TraitGoalProvenVia::AliasBound,
@@ -1693,38 +1694,10 @@ where
             let where_bounds: Vec<_> = candidates
                 .extract_if(.., |c| matches!(c.source, CandidateSource::ParamEnv(_)))
                 .collect();
-            let Some((response, info)) = self.try_merge_candidates(&where_bounds) else {
+            candidates.into_iter().for_each(|c| self.ignore_candidate_head_usages(c.head_usages));
+            let Some(response) = self.try_merge_candidates(&where_bounds) else {
                 return Ok((self.bail_with_ambiguity(&where_bounds), None));
             };
-            match info {
-                // If there's an always applicable candidate, the result of all
-                // other candidates does not matter. This means we can ignore
-                // them when checking whether we've reached a fixpoint.
-                //
-                // We always prefer the first always applicable candidate, even if a
-                // later candidate is also always applicable and would result in fewer
-                // reruns. We could slightly improve this by e.g. searching for another
-                // always applicable candidate which doesn't depend on any cycle heads.
-                //
-                // NOTE: This is optimization is observable in case there is an always
-                // applicable global candidate and another non-global candidate which only
-                // applies because of a provisional result. I can't even think of a test
-                // case where this would occur and even then, this would not be unsound.
-                // Supporting this makes the code more involved, so I am just going to
-                // ignore this for now.
-                MergeCandidateInfo::AlwaysApplicable(i) => {
-                    for (j, c) in where_bounds.into_iter().enumerate() {
-                        if i != j {
-                            self.ignore_candidate_head_usages(c.head_usages)
-                        }
-                    }
-                    // If a where-bound does not apply, we don't actually get a
-                    // candidate for it. We manually track the head usages
-                    // of all failed `ParamEnv` candidates instead.
-                    self.ignore_candidate_head_usages(failed_candidate_info.param_env_head_usages);
-                }
-                MergeCandidateInfo::EqualResponse => {}
-            }
             return Ok((response, Some(TraitGoalProvenVia::ParamEnv)));
         }
 
@@ -1733,6 +1706,7 @@ where
             let alias_bounds: Vec<_> = candidates
                 .extract_if(.., |c| matches!(c.source, CandidateSource::AliasBound(_)))
                 .collect();
+            candidates.into_iter().for_each(|c| self.ignore_candidate_head_usages(c.head_usages));
             return Ok(self.merge_candidates_or_bail_with_ambiguity(
                 &alias_bounds,
                 TraitGoalProvenVia::AliasBound,

tests/ui/traits/next-solver/assembly/item-bound-eq-modulo-placeholder-constraint.rs

@@ -0,0 +1,29 @@
+//@ revisions: current next
+//@ ignore-compare-mode-next-solver (explicit revisions)
+//@[next] compile-flags: -Znext-solver
+//@ check-pass
+
+// When proving `C::Val<'a>: for<'b> PartialEq<C::Val<'b>>` there are
+// two candidates:
+// - `C::Val<'a>: PartialEq<C::Val<'a>>`
+// - `for<'b> C::Val<'a>: PartialEq<C::Val<'b>>`
+//
+// The first candidate results in an `'!b == 'a` constraint while the
+// second one has no region constraints. The constraint of the first
+// candidate means the canonical response has an entry for `'b` in its
+// `var_values`. This previously caused us to not prefer the second
+// constraint.
+//
+// FIXME(trait-system-refactor-initiative#305): Now, actually, the first
+// candidate should just result in a leak check failure, but doesn't.
+// That's a separate issue though :>
+trait Cursor {
+    type Val<'a>: PartialEq + for<'b> PartialEq<Self::Val<'b>>;
+}
+impl<C: Cursor> Cursor for &C {
+    // for<'b> C::Val<'a>: PartialEq<C::Val<'b>>
+    // -  C::Val<'a>: PartialEq<C::Val<'a>>`
+    // -  for<'b> C::Val<'a>: PartialEq<C::Val<'b>>
+    type Val<'a> = C::Val<'a>;
+}
+fn main() {}