Skip to content
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

Jump to bottom

Freshen normalizes-to hack goal RHS in the evaluate loop #109679

Merged
merged 1 commit into from
Mar 31, 2023
Merged

Freshen normalizes-to hack goal RHS in the evaluate loop #109679

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
102 changes: 69 additions & 33 deletions compiler/rustc_trait_selection/src/solve/eval_ctxt.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,20 @@ pub(super) enum IsNormalizesToHack {

#[derive(Debug, Clone)]
pub(super) struct NestedGoals<'tcx> {
/// This normalizes-to goal that is treated specially during the evaluation
/// loop. In each iteration we take the RHS of the projection, replace it with
/// a fresh inference variable, and only after evaluating that goal do we
/// equate the fresh inference variable with the actual RHS of the predicate.
///
/// This is both to improve caching, and to avoid using the RHS of the
/// projection predicate to influence the normalizes-to candidate we select.
///
/// This is not a 'real' nested goal. We must not forget to replace the RHS
/// with a fresh inference variable when we evaluate this goal. That can result
/// in a trait solver cycle. This would currently result in overflow but can be
/// can be unsound with more powerful coinduction in the future.
pub(super) normalizes_to_hack_goal: Option<Goal<'tcx, ty::ProjectionPredicate<'tcx>>>,
/// The rest of the goals which have not yet processed or remain ambiguous.
pub(super) goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
}

Expand Down Expand Up @@ -163,6 +176,10 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
canonical_response,
)?;

if !has_changed && !nested_goals.is_empty() {
bug!("an unchanged goal shouldn't have any side-effects on instantiation");
}

// Check that rerunning this query with its inference constraints applied
// doesn't result in new inference constraints and has the same result.
//
Expand All @@ -180,9 +197,17 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
let canonical_response =
EvalCtxt::evaluate_canonical_goal(self.tcx(), self.search_graph, canonical_goal)?;
if !canonical_response.value.var_values.is_identity() {
bug!("unstable result: {goal:?} {canonical_goal:?} {canonical_response:?}");
bug!(
"unstable result: re-canonicalized goal={canonical_goal:#?} \
response={canonical_response:#?}"
);
compiler-errors marked this conversation as resolved.
Show resolved Hide resolved
}
if certainty != canonical_response.value.certainty {
bug!(
"unstable certainty: {certainty:#?} re-canonicalized goal={canonical_goal:#?} \
response={canonical_response:#?}"
);
}
assert_eq!(certainty, canonical_response.value.certainty);
}

Ok((has_changed, certainty, nested_goals))
Expand Down Expand Up @@ -262,15 +287,44 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
let mut has_changed = Err(Certainty::Yes);

if let Some(goal) = goals.normalizes_to_hack_goal.take() {
let (_, certainty, nested_goals) = match this.evaluate_goal(
IsNormalizesToHack::Yes,
goal.with(this.tcx(), ty::Binder::dummy(goal.predicate)),
// Replace the goal with an unconstrained infer var, so the
// RHS does not affect projection candidate assembly.
let unconstrained_rhs = this.next_term_infer_of_kind(goal.predicate.term);
let unconstrained_goal = goal.with(
this.tcx(),
ty::Binder::dummy(ty::ProjectionPredicate {
projection_ty: goal.predicate.projection_ty,
term: unconstrained_rhs,
}),
);

let (_, certainty, instantiate_goals) =
match this.evaluate_goal(IsNormalizesToHack::Yes, unconstrained_goal) {
Ok(r) => r,
Err(NoSolution) => return Some(Err(NoSolution)),
};
new_goals.goals.extend(instantiate_goals);

// Finally, equate the goal's RHS with the unconstrained var.
// We put the nested goals from this into goals instead of
// next_goals to avoid needing to process the loop one extra
// time if this goal returns something -- I don't think this
// matters in practice, though.
match this.eq_and_get_goals(
goal.param_env,
goal.predicate.term,
unconstrained_rhs,
) {
Ok(r) => r,
Ok(eq_goals) => {
goals.goals.extend(eq_goals);
}
Err(NoSolution) => return Some(Err(NoSolution)),
};
new_goals.goals.extend(nested_goals);

// We only look at the `projection_ty` part here rather than
// looking at the "has changed" return from evaluate_goal,
// because we expect the `unconstrained_rhs` part of the predicate
// to have changed -- that means we actually normalized successfully!
if goal.predicate.projection_ty
!= this.resolve_vars_if_possible(goal.predicate.projection_ty)
{
Expand All @@ -280,40 +334,22 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
match certainty {
Certainty::Yes => {}
Certainty::Maybe(_) => {
let goal = this.resolve_vars_if_possible(goal);

// The rhs of this `normalizes-to` must always be an unconstrained infer var as it is
// the hack used by `normalizes-to` to ensure that every `normalizes-to` behaves the same
// regardless of the rhs.
//
// However it is important not to unconditionally replace the rhs with a new infer var
// as otherwise we may replace the original unconstrained infer var with a new infer var
// and never propagate any constraints on the new var back to the original var.
let term = this
.term_is_fully_unconstrained(goal)
.then_some(goal.predicate.term)
.unwrap_or_else(|| {
this.next_term_infer_of_kind(goal.predicate.term)
});
let projection_pred = ty::ProjectionPredicate {
term,
projection_ty: goal.predicate.projection_ty,
};
// We need to resolve vars here so that we correctly
// deal with `has_changed` in the next iteration.
new_goals.normalizes_to_hack_goal =
Some(goal.with(this.tcx(), projection_pred));

Some(this.resolve_vars_if_possible(goal));
compiler-errors marked this conversation as resolved.
Show resolved Hide resolved
has_changed = has_changed.map_err(|c| c.unify_and(certainty));
}
}
}

for nested_goal in goals.goals.drain(..) {
let (changed, certainty, nested_goals) =
match this.evaluate_goal(IsNormalizesToHack::No, nested_goal) {
for goal in goals.goals.drain(..) {
let (changed, certainty, instantiate_goals) =
match this.evaluate_goal(IsNormalizesToHack::No, goal) {
Ok(result) => result,
Err(NoSolution) => return Some(Err(NoSolution)),
};
new_goals.goals.extend(nested_goals);
new_goals.goals.extend(instantiate_goals);

if changed {
has_changed = Ok(());
Expand All @@ -322,7 +358,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
match certainty {
Certainty::Yes => {}
Certainty::Maybe(_) => {
new_goals.goals.push(nested_goal);
new_goals.goals.push(goal);
has_changed = has_changed.map_err(|c| c.unify_and(certainty));
}
}
Expand Down
11 changes: 1 addition & 10 deletions compiler/rustc_trait_selection/src/solve/project_goals.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,16 +35,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
let candidates = self.assemble_and_evaluate_candidates(goal);
self.merge_candidates(candidates)
} else {
let predicate = goal.predicate;
let unconstrained_rhs = self.next_term_infer_of_kind(predicate.term);
let unconstrained_predicate = ProjectionPredicate {
projection_ty: goal.predicate.projection_ty,
term: unconstrained_rhs,
};

self.set_normalizes_to_hack_goal(goal.with(self.tcx(), unconstrained_predicate));
self.try_evaluate_added_goals()?;
self.eq(goal.param_env, unconstrained_rhs, predicate.term)?;
self.set_normalizes_to_hack_goal(goal);
self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
}
}
Expand Down