Skip to content

Next-solver do not prefer trivially true candidates #163589

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
lcnr wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

Next-solver do not prefer trivially true candidates #163589

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions compiler/rustc_next_trait_solver/src/solve/assembly/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1335,7 +1335,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)
Expand All @@ -1357,7 +1357,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)
Expand Down
84 changes: 29 additions & 55 deletions compiler/rustc_next_trait_solver/src/solve/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -86,23 +86,18 @@ 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,
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
max_universe == &b.max_universe
&& var_kinds == &b.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
}
Expand Down Expand Up @@ -319,12 +314,6 @@ where
}
}

#[derive(Debug)]
enum MergeCandidateInfo {
AlwaysApplicable(usize),
EqualResponse,
}

impl<D, I> EvalCtxt<'_, D>
where
D: SolverDelegate<Interner = I>,
Expand All @@ -337,48 +326,33 @@ where
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)));
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));
}
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> {
Expand Down
41 changes: 7 additions & 34 deletions compiler/rustc_next_trait_solver/src/solve/trait_goals.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,8 +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,
has_only_region_constraints,
NoSolution, ParamEnvSource, StalledOnCoroutines, has_only_region_constraints,
};

impl<D, I> assembly::GoalKind<D> for TraitClause<I>
Expand Down Expand Up @@ -1575,7 +1574,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 {
Expand All @@ -1588,7 +1587,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)
Expand Down Expand Up @@ -1653,6 +1652,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,
Expand All @@ -1668,38 +1668,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)));
}

Expand All @@ -1708,6 +1680,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,
Expand Down
44 changes: 0 additions & 44 deletions tests/ui/traits/next-solver/cycles/inductive-cycle-but-ok.rs
View file
Open in desktop

This file was deleted.

36 changes: 0 additions & 36 deletions tests/ui/traits/next-solver/cycles/inductive-cycle-discarded-coinductive-constraints.rs
View file
Open in desktop

This file was deleted.

Loading