Skip to content

Commit

Permalink
Rollup merge of rust-lang#119071 - lcnr:overflowo, r=compiler-errors
Browse files Browse the repository at this point in the history
-Znext-solver: adapt overflow rules to avoid breakage

Do not erase overflow constraints if they are from equating the impl header when normalizing[^1].

This should be the minimal change to not break crates depending on the old project behavior of "apply impl constraints while only lazily evaluating any nested goals".

Fixes rust-lang/trait-system-refactor-initiative#70, see https://hackmd.io/ATf4hN0NRY-w2LIVgeFsVg for the reasoning behind this.

Only keeping constraints on overflow for `normalize-to` goals as that's the only thing needed for backcompat. It also allows us to not track the origin of root obligations. The issue with root goals would be something like the following:

```rust
trait Foo {}
trait Bar {}

trait FooBar {}
impl<T: Foo + Bar> FooBar for T {}

// These two should behave the same, rn we can drop constraints for both,
// but if we don't drop `Misc` goals we would only drop the constraints for
// `FooBar` unless we track origins of root obligations.
fn func1<T: Foo + Bar>() {}
fn func2<T: FooBaz>() {}
```

[^1]: mostly, the actual rules are slightly different

r? `@compiler-errors`
  • Loading branch information
compiler-errors authored Dec 19, 2023
2 parents b25b723 + 17705ea commit 49dc89d
Show file tree
Hide file tree
Showing 18 changed files with 269 additions and 104 deletions.
21 changes: 21 additions & 0 deletions compiler/rustc_middle/src/traits/solve.rs
Original file line number Diff line number Diff line change
Expand Up @@ -233,6 +233,27 @@ impl<'tcx> TypeVisitable<TyCtxt<'tcx>> for PredefinedOpaques<'tcx> {
}
}

/// Why a specific goal has to be proven.
///
/// This is necessary as we treat nested goals different depending on
/// their source.
#[derive(Copy, Clone, Debug, PartialEq, Eq)]
pub enum GoalSource {
Misc,
/// We're proving a where-bound of an impl.
///
/// FIXME(-Znext-solver=coinductive): Explain how and why this
/// changes whether cycles are coinductive.
///
/// This also impacts whether we erase constraints on overflow.
/// Erasing constraints is generally very useful for perf and also
/// results in better error messages by avoiding spurious errors.
/// We do not erase overflow constraints in `normalizes-to` goals unless
/// they are from an impl where-clause. This is necessary due to
/// backwards compatability, cc trait-system-refactor-initiatitive#70.
ImplWhereBound,
}

#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, HashStable)]
pub enum IsNormalizesToHack {
Yes,
Expand Down
6 changes: 3 additions & 3 deletions compiler/rustc_middle/src/traits/solve/inspect.rs
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,8 @@
//! [canonicalized]: https://rustc-dev-guide.rust-lang.org/solve/canonicalization.html

use super::{
CandidateSource, Canonical, CanonicalInput, Certainty, Goal, IsNormalizesToHack, NoSolution,
QueryInput, QueryResult,
CandidateSource, Canonical, CanonicalInput, Certainty, Goal, GoalSource, IsNormalizesToHack,
NoSolution, QueryInput, QueryResult,
};
use crate::{infer::canonical::CanonicalVarValues, ty};
use format::ProofTreeFormatter;
Expand Down Expand Up @@ -115,7 +115,7 @@ impl Debug for Probe<'_> {
pub enum ProbeStep<'tcx> {
/// We added a goal to the `EvalCtxt` which will get proven
/// the next time `EvalCtxt::try_evaluate_added_goals` is called.
AddGoal(CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>),
AddGoal(GoalSource, CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>),
/// The inside of a `EvalCtxt::try_evaluate_added_goals` call.
EvaluateGoals(AddedGoalsEvaluation<'tcx>),
/// A call to `probe` while proving the current goal. This is
Expand Down
8 changes: 7 additions & 1 deletion compiler/rustc_middle/src/traits/solve/inspect/format.rs
Original file line number Diff line number Diff line change
Expand Up @@ -123,7 +123,13 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
self.nested(|this| {
for step in &probe.steps {
match step {
ProbeStep::AddGoal(goal) => writeln!(this.f, "ADDED GOAL: {goal:?}")?,
ProbeStep::AddGoal(source, goal) => {
let source = match source {
GoalSource::Misc => "misc",
GoalSource::ImplWhereBound => "impl where-bound",
};
writeln!(this.f, "ADDED GOAL ({source}): {goal:?}")?
}
ProbeStep::EvaluateGoals(eval) => this.format_added_goals_evaluation(eval)?,
ProbeStep::NestedProbe(probe) => this.format_probe(probe)?,
ProbeStep::CommitIfOkStart => writeln!(this.f, "COMMIT_IF_OK START")?,
Expand Down
16 changes: 9 additions & 7 deletions compiler/rustc_trait_selection/src/solve/alias_relate.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@
//! * bidirectional-normalizes-to: If `A` and `B` are both projections, and both
//! may apply, then we can compute the "intersection" of both normalizes-to by
//! performing them together. This is used specifically to resolve ambiguities.
use super::EvalCtxt;
use super::{EvalCtxt, GoalSource};
use rustc_infer::infer::DefineOpaqueTypes;
use rustc_infer::traits::query::NoSolution;
use rustc_middle::traits::solve::{Certainty, Goal, QueryResult};
Expand Down Expand Up @@ -89,11 +89,10 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
ty::TermKind::Const(_) => {
if let Some(alias) = term.to_alias_ty(self.tcx()) {
let term = self.next_term_infer_of_kind(term);
self.add_goal(Goal::new(
self.tcx(),
param_env,
ty::NormalizesTo { alias, term },
));
self.add_goal(
GoalSource::Misc,
Goal::new(self.tcx(), param_env, ty::NormalizesTo { alias, term }),
);
self.try_evaluate_added_goals()?;
Ok(Some(self.resolve_vars_if_possible(term)))
} else {
Expand All @@ -109,7 +108,10 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
opaque: ty::AliasTy<'tcx>,
term: ty::Term<'tcx>,
) -> QueryResult<'tcx> {
self.add_goal(Goal::new(self.tcx(), param_env, ty::NormalizesTo { alias: opaque, term }));
self.add_goal(
GoalSource::Misc,
Goal::new(self.tcx(), param_env, ty::NormalizesTo { alias: opaque, term }),
);
self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
}

Expand Down
23 changes: 15 additions & 8 deletions compiler/rustc_trait_selection/src/solve/assembly/mod.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
//! Code shared by trait and projection goals for candidate assembly.

use super::{EvalCtxt, SolverMode};
use crate::solve::GoalSource;
use crate::traits::coherence;
use rustc_hir::def_id::DefId;
use rustc_infer::traits::query::NoSolution;
Expand Down Expand Up @@ -62,7 +63,9 @@ pub(super) trait GoalKind<'tcx>:
requirements: impl IntoIterator<Item = Goal<'tcx, ty::Predicate<'tcx>>>,
) -> QueryResult<'tcx> {
Self::probe_and_match_goal_against_assumption(ecx, goal, assumption, |ecx| {
ecx.add_goals(requirements);
// FIXME(-Znext-solver=coinductive): check whether this should be
// `GoalSource::ImplWhereBound` for any caller.
ecx.add_goals(GoalSource::Misc, requirements);
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
})
}
Expand Down Expand Up @@ -94,12 +97,16 @@ pub(super) trait GoalKind<'tcx>:
let ty::Dynamic(bounds, _, _) = *goal.predicate.self_ty().kind() else {
bug!("expected object type in `consider_object_bound_candidate`");
};
ecx.add_goals(structural_traits::predicates_for_object_candidate(
ecx,
goal.param_env,
goal.predicate.trait_ref(tcx),
bounds,
));
// FIXME(-Znext-solver=coinductive): Should this be `GoalSource::ImplWhereBound`?
ecx.add_goals(
GoalSource::Misc,
structural_traits::predicates_for_object_candidate(
ecx,
goal.param_env,
goal.predicate.trait_ref(tcx),
bounds,
),
);
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
})
}
Expand Down Expand Up @@ -364,7 +371,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
let normalized_ty = ecx.next_ty_infer();
let normalizes_to_goal =
goal.with(tcx, ty::NormalizesTo { alias, term: normalized_ty.into() });
ecx.add_goal(normalizes_to_goal);
ecx.add_goal(GoalSource::Misc, normalizes_to_goal);
if let Err(NoSolution) = ecx.try_evaluate_added_goals() {
debug!("self type normalization failed");
return vec![];
Expand Down
14 changes: 0 additions & 14 deletions compiler/rustc_trait_selection/src/solve/eval_ctxt/canonical.rs
Original file line number Diff line number Diff line change
Expand Up @@ -94,20 +94,6 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
);

let certainty = certainty.unify_with(goals_certainty);
if let Certainty::OVERFLOW = certainty {
// If we have overflow, it's probable that we're substituting a type
// into itself infinitely and any partial substitutions in the query
// response are probably not useful anyways, so just return an empty
// query response.
//
// This may prevent us from potentially useful inference, e.g.
// 2 candidates, one ambiguous and one overflow, which both
// have the same inference constraints.
//
// Changing this to retain some constraints in the future
// won't be a breaking change, so this is good enough for now.
return Ok(self.make_ambiguous_response_no_constraints(MaybeCause::Overflow));
}

let var_values = self.var_values;
let external_constraints = self.compute_external_query_constraints()?;
Expand Down
91 changes: 70 additions & 21 deletions compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -23,14 +23,15 @@ use rustc_middle::ty::{
use rustc_session::config::DumpSolverProofTree;
use rustc_span::DUMMY_SP;
use std::io::Write;
use std::iter;
use std::ops::ControlFlow;

use crate::traits::vtable::{count_own_vtable_entries, prepare_vtable_segments, VtblSegment};

use super::inspect::ProofTreeBuilder;
use super::SolverMode;
use super::{search_graph, GoalEvaluationKind};
use super::{search_graph::SearchGraph, Goal};
use super::{GoalSource, SolverMode};
pub use select::InferCtxtSelectExt;

mod canonical;
Expand Down Expand Up @@ -105,7 +106,7 @@ pub(super) struct NestedGoals<'tcx> {
/// can be unsound with more powerful coinduction in the future.
pub(super) normalizes_to_hack_goal: Option<Goal<'tcx, ty::NormalizesTo<'tcx>>>,
/// The rest of the goals which have not yet processed or remain ambiguous.
pub(super) goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
pub(super) goals: Vec<(GoalSource, Goal<'tcx, ty::Predicate<'tcx>>)>,
}

impl<'tcx> NestedGoals<'tcx> {
Expand Down Expand Up @@ -156,7 +157,7 @@ impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> {
Option<inspect::GoalEvaluation<'tcx>>,
) {
EvalCtxt::enter_root(self, generate_proof_tree, |ecx| {
ecx.evaluate_goal(GoalEvaluationKind::Root, goal)
ecx.evaluate_goal(GoalEvaluationKind::Root, GoalSource::Misc, goal)
})
}
}
Expand Down Expand Up @@ -334,6 +335,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
fn evaluate_goal(
&mut self,
goal_evaluation_kind: GoalEvaluationKind,
source: GoalSource,
goal: Goal<'tcx, ty::Predicate<'tcx>>,
) -> Result<(bool, Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution> {
let (orig_values, canonical_goal) = self.canonicalize_goal(goal);
Expand All @@ -353,13 +355,13 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
Ok(response) => response,
};

let has_changed = !canonical_response.value.var_values.is_identity_modulo_regions()
|| !canonical_response.value.external_constraints.opaque_types.is_empty();
let (certainty, nested_goals) = match self.instantiate_and_apply_query_response(
goal.param_env,
orig_values,
canonical_response,
) {
let (certainty, has_changed, nested_goals) = match self
.instantiate_response_discarding_overflow(
goal.param_env,
source,
orig_values,
canonical_response,
) {
Err(e) => {
self.inspect.goal_evaluation(goal_evaluation);
return Err(e);
Expand All @@ -386,6 +388,44 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
Ok((has_changed, certainty, nested_goals))
}

fn instantiate_response_discarding_overflow(
&mut self,
param_env: ty::ParamEnv<'tcx>,
source: GoalSource,
original_values: Vec<ty::GenericArg<'tcx>>,
response: CanonicalResponse<'tcx>,
) -> Result<(Certainty, bool, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution> {
// The old solver did not evaluate nested goals when normalizing.
// It returned the selection constraints allowing a `Projection`
// obligation to not hold in coherence while avoiding the fatal error
// from overflow.
//
// We match this behavior here by considering all constraints
// from nested goals which are not from where-bounds. We will already
// need to track which nested goals are required by impl where-bounds
// for coinductive cycles, so we simply reuse that here.
//
// While we could consider overflow constraints in more cases, this should
// not be necessary for backcompat and results in better perf. It also
// avoids a potential inconsistency which would otherwise require some
// tracking for root goals as well. See #119071 for an example.
let keep_overflow_constraints = || {
self.search_graph.current_goal_is_normalizes_to()
&& source != GoalSource::ImplWhereBound
};

if response.value.certainty == Certainty::OVERFLOW && !keep_overflow_constraints() {
Ok((Certainty::OVERFLOW, false, Vec::new()))
} else {
let has_changed = !response.value.var_values.is_identity_modulo_regions()
|| !response.value.external_constraints.opaque_types.is_empty();

let (certainty, nested_goals) =
self.instantiate_and_apply_query_response(param_env, original_values, response)?;
Ok((certainty, has_changed, nested_goals))
}
}

fn compute_goal(&mut self, goal: Goal<'tcx, ty::Predicate<'tcx>>) -> QueryResult<'tcx> {
let Goal { param_env, predicate } = goal;
let kind = predicate.kind();
Expand Down Expand Up @@ -439,7 +479,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
} else {
let kind = self.infcx.instantiate_binder_with_placeholders(kind);
let goal = goal.with(self.tcx(), ty::Binder::dummy(kind));
self.add_goal(goal);
self.add_goal(GoalSource::Misc, goal);
self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
}
}
Expand Down Expand Up @@ -488,6 +528,13 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
let mut goals = core::mem::replace(&mut self.nested_goals, NestedGoals::new());

self.inspect.evaluate_added_goals_loop_start();

fn with_misc_source<'tcx>(
it: impl IntoIterator<Item = Goal<'tcx, ty::Predicate<'tcx>>>,
) -> impl Iterator<Item = (GoalSource, Goal<'tcx, ty::Predicate<'tcx>>)> {
iter::zip(iter::repeat(GoalSource::Misc), it)
}

// If this loop did not result in any progress, what's our final certainty.
let mut unchanged_certainty = Some(Certainty::Yes);
if let Some(goal) = goals.normalizes_to_hack_goal.take() {
Expand All @@ -501,9 +548,10 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {

let (_, certainty, instantiate_goals) = self.evaluate_goal(
GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::Yes },
GoalSource::Misc,
unconstrained_goal,
)?;
self.nested_goals.goals.extend(instantiate_goals);
self.nested_goals.goals.extend(with_misc_source(instantiate_goals));

// Finally, equate the goal's RHS with the unconstrained var.
// We put the nested goals from this into goals instead of
Expand All @@ -512,7 +560,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
// matters in practice, though.
let eq_goals =
self.eq_and_get_goals(goal.param_env, goal.predicate.term, unconstrained_rhs)?;
goals.goals.extend(eq_goals);
goals.goals.extend(with_misc_source(eq_goals));

// We only look at the `projection_ty` part here rather than
// looking at the "has changed" return from evaluate_goal,
Expand All @@ -533,20 +581,21 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
}
}

for goal in goals.goals.drain(..) {
for (source, goal) in goals.goals.drain(..) {
let (has_changed, certainty, instantiate_goals) = self.evaluate_goal(
GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::No },
source,
goal,
)?;
self.nested_goals.goals.extend(instantiate_goals);
self.nested_goals.goals.extend(with_misc_source(instantiate_goals));
if has_changed {
unchanged_certainty = None;
}

match certainty {
Certainty::Yes => {}
Certainty::Maybe(_) => {
self.nested_goals.goals.push(goal);
self.nested_goals.goals.push((source, goal));
unchanged_certainty = unchanged_certainty.map(|c| c.unify_with(certainty));
}
}
Expand Down Expand Up @@ -670,7 +719,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
.at(&ObligationCause::dummy(), param_env)
.eq(DefineOpaqueTypes::No, lhs, rhs)
.map(|InferOk { value: (), obligations }| {
self.add_goals(obligations.into_iter().map(|o| o.into()));
self.add_goals(GoalSource::Misc, obligations.into_iter().map(|o| o.into()));
})
.map_err(|e| {
debug!(?e, "failed to equate");
Expand All @@ -689,7 +738,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
.at(&ObligationCause::dummy(), param_env)
.sub(DefineOpaqueTypes::No, sub, sup)
.map(|InferOk { value: (), obligations }| {
self.add_goals(obligations.into_iter().map(|o| o.into()));
self.add_goals(GoalSource::Misc, obligations.into_iter().map(|o| o.into()));
})
.map_err(|e| {
debug!(?e, "failed to subtype");
Expand All @@ -709,7 +758,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
.at(&ObligationCause::dummy(), param_env)
.relate(DefineOpaqueTypes::No, lhs, variance, rhs)
.map(|InferOk { value: (), obligations }| {
self.add_goals(obligations.into_iter().map(|o| o.into()));
self.add_goals(GoalSource::Misc, obligations.into_iter().map(|o| o.into()));
})
.map_err(|e| {
debug!(?e, "failed to relate");
Expand Down Expand Up @@ -842,7 +891,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
true,
&mut obligations,
)?;
self.add_goals(obligations.into_iter().map(|o| o.into()));
self.add_goals(GoalSource::Misc, obligations.into_iter().map(|o| o.into()));
Ok(())
}

Expand All @@ -862,7 +911,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
hidden_ty,
&mut obligations,
);
self.add_goals(obligations.into_iter().map(|o| o.into()));
self.add_goals(GoalSource::Misc, obligations.into_iter().map(|o| o.into()));
}

// Do something for each opaque/hidden pair defined with `def_id` in the
Expand Down
Loading

0 comments on commit 49dc89d

Please sign in to comment.