track the source of nested goals

This commit is contained in:
lcnr 2023-12-18 07:49:46 +01:00
parent 321b6565a5
commit ca718ffd2d
14 changed files with 173 additions and 81 deletions

View File

@ -233,6 +233,24 @@ 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.
ImplWhereBound,
}
#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, HashStable)] #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, HashStable)]
pub enum IsNormalizesToHack { pub enum IsNormalizesToHack {
Yes, Yes,

View File

@ -19,8 +19,8 @@
//! [canonicalized]: https://rustc-dev-guide.rust-lang.org/solve/canonicalization.html //! [canonicalized]: https://rustc-dev-guide.rust-lang.org/solve/canonicalization.html
use super::{ use super::{
CandidateSource, Canonical, CanonicalInput, Certainty, Goal, IsNormalizesToHack, NoSolution, CandidateSource, Canonical, CanonicalInput, Certainty, Goal, GoalSource, IsNormalizesToHack,
QueryInput, QueryResult, NoSolution, QueryInput, QueryResult,
}; };
use crate::{infer::canonical::CanonicalVarValues, ty}; use crate::{infer::canonical::CanonicalVarValues, ty};
use format::ProofTreeFormatter; use format::ProofTreeFormatter;
@ -115,7 +115,7 @@ impl Debug for Probe<'_> {
pub enum ProbeStep<'tcx> { pub enum ProbeStep<'tcx> {
/// We added a goal to the `EvalCtxt` which will get proven /// We added a goal to the `EvalCtxt` which will get proven
/// the next time `EvalCtxt::try_evaluate_added_goals` is called. /// 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. /// The inside of a `EvalCtxt::try_evaluate_added_goals` call.
EvaluateGoals(AddedGoalsEvaluation<'tcx>), EvaluateGoals(AddedGoalsEvaluation<'tcx>),
/// A call to `probe` while proving the current goal. This is /// A call to `probe` while proving the current goal. This is

View File

@ -123,7 +123,13 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
self.nested(|this| { self.nested(|this| {
for step in &probe.steps { for step in &probe.steps {
match step { 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::EvaluateGoals(eval) => this.format_added_goals_evaluation(eval)?,
ProbeStep::NestedProbe(probe) => this.format_probe(probe)?, ProbeStep::NestedProbe(probe) => this.format_probe(probe)?,
ProbeStep::CommitIfOkStart => writeln!(this.f, "COMMIT_IF_OK START")?, ProbeStep::CommitIfOkStart => writeln!(this.f, "COMMIT_IF_OK START")?,

View File

@ -11,7 +11,7 @@
//! * bidirectional-normalizes-to: If `A` and `B` are both projections, and both //! * 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 //! may apply, then we can compute the "intersection" of both normalizes-to by
//! performing them together. This is used specifically to resolve ambiguities. //! 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::infer::DefineOpaqueTypes;
use rustc_infer::traits::query::NoSolution; use rustc_infer::traits::query::NoSolution;
use rustc_middle::traits::solve::{Certainty, Goal, QueryResult}; use rustc_middle::traits::solve::{Certainty, Goal, QueryResult};
@ -89,11 +89,10 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
ty::TermKind::Const(_) => { ty::TermKind::Const(_) => {
if let Some(alias) = term.to_alias_ty(self.tcx()) { if let Some(alias) = term.to_alias_ty(self.tcx()) {
let term = self.next_term_infer_of_kind(term); let term = self.next_term_infer_of_kind(term);
self.add_goal(Goal::new( self.add_goal(
self.tcx(), GoalSource::Misc,
param_env, Goal::new(self.tcx(), param_env, ty::NormalizesTo { alias, term }),
ty::NormalizesTo { alias, term }, );
));
self.try_evaluate_added_goals()?; self.try_evaluate_added_goals()?;
Ok(Some(self.resolve_vars_if_possible(term))) Ok(Some(self.resolve_vars_if_possible(term)))
} else { } else {
@ -109,7 +108,10 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
opaque: ty::AliasTy<'tcx>, opaque: ty::AliasTy<'tcx>,
term: ty::Term<'tcx>, term: ty::Term<'tcx>,
) -> QueryResult<'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) self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
} }

View File

@ -1,6 +1,7 @@
//! Code shared by trait and projection goals for candidate assembly. //! Code shared by trait and projection goals for candidate assembly.
use super::{EvalCtxt, SolverMode}; use super::{EvalCtxt, SolverMode};
use crate::solve::GoalSource;
use crate::traits::coherence; use crate::traits::coherence;
use rustc_hir::def_id::DefId; use rustc_hir::def_id::DefId;
use rustc_infer::traits::query::NoSolution; use rustc_infer::traits::query::NoSolution;
@ -62,7 +63,9 @@ pub(super) trait GoalKind<'tcx>:
requirements: impl IntoIterator<Item = Goal<'tcx, ty::Predicate<'tcx>>>, requirements: impl IntoIterator<Item = Goal<'tcx, ty::Predicate<'tcx>>>,
) -> QueryResult<'tcx> { ) -> QueryResult<'tcx> {
Self::probe_and_match_goal_against_assumption(ecx, goal, assumption, |ecx| { 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) ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
}) })
} }
@ -94,12 +97,16 @@ pub(super) trait GoalKind<'tcx>:
let ty::Dynamic(bounds, _, _) = *goal.predicate.self_ty().kind() else { let ty::Dynamic(bounds, _, _) = *goal.predicate.self_ty().kind() else {
bug!("expected object type in `consider_object_bound_candidate`"); bug!("expected object type in `consider_object_bound_candidate`");
}; };
ecx.add_goals(structural_traits::predicates_for_object_candidate( // FIXME(-Znext-solver=coinductive): Should this be `GoalSource::ImplWhereBound`?
ecx, ecx.add_goals(
goal.param_env, GoalSource::Misc,
goal.predicate.trait_ref(tcx), structural_traits::predicates_for_object_candidate(
bounds, ecx,
)); goal.param_env,
goal.predicate.trait_ref(tcx),
bounds,
),
);
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes) ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
}) })
} }
@ -364,7 +371,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
let normalized_ty = ecx.next_ty_infer(); let normalized_ty = ecx.next_ty_infer();
let normalizes_to_goal = let normalizes_to_goal =
goal.with(tcx, ty::NormalizesTo { alias, term: normalized_ty.into() }); 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() { if let Err(NoSolution) = ecx.try_evaluate_added_goals() {
debug!("self type normalization failed"); debug!("self type normalization failed");
return vec![]; return vec![];

View File

@ -23,14 +23,15 @@ use rustc_middle::ty::{
use rustc_session::config::DumpSolverProofTree; use rustc_session::config::DumpSolverProofTree;
use rustc_span::DUMMY_SP; use rustc_span::DUMMY_SP;
use std::io::Write; use std::io::Write;
use std::iter;
use std::ops::ControlFlow; use std::ops::ControlFlow;
use crate::traits::vtable::{count_own_vtable_entries, prepare_vtable_segments, VtblSegment}; use crate::traits::vtable::{count_own_vtable_entries, prepare_vtable_segments, VtblSegment};
use super::inspect::ProofTreeBuilder; use super::inspect::ProofTreeBuilder;
use super::SolverMode;
use super::{search_graph, GoalEvaluationKind}; use super::{search_graph, GoalEvaluationKind};
use super::{search_graph::SearchGraph, Goal}; use super::{search_graph::SearchGraph, Goal};
use super::{GoalSource, SolverMode};
pub use select::InferCtxtSelectExt; pub use select::InferCtxtSelectExt;
mod canonical; mod canonical;
@ -105,7 +106,7 @@ pub(super) struct NestedGoals<'tcx> {
/// can be unsound with more powerful coinduction in the future. /// can be unsound with more powerful coinduction in the future.
pub(super) normalizes_to_hack_goal: Option<Goal<'tcx, ty::NormalizesTo<'tcx>>>, 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. /// 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> { impl<'tcx> NestedGoals<'tcx> {
@ -439,7 +440,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
} else { } else {
let kind = self.infcx.instantiate_binder_with_placeholders(kind); let kind = self.infcx.instantiate_binder_with_placeholders(kind);
let goal = goal.with(self.tcx(), ty::Binder::dummy(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) self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
} }
} }
@ -488,6 +489,13 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
let mut goals = core::mem::replace(&mut self.nested_goals, NestedGoals::new()); let mut goals = core::mem::replace(&mut self.nested_goals, NestedGoals::new());
self.inspect.evaluate_added_goals_loop_start(); 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. // If this loop did not result in any progress, what's our final certainty.
let mut unchanged_certainty = Some(Certainty::Yes); let mut unchanged_certainty = Some(Certainty::Yes);
if let Some(goal) = goals.normalizes_to_hack_goal.take() { if let Some(goal) = goals.normalizes_to_hack_goal.take() {
@ -503,7 +511,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::Yes }, GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::Yes },
unconstrained_goal, 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. // Finally, equate the goal's RHS with the unconstrained var.
// We put the nested goals from this into goals instead of // We put the nested goals from this into goals instead of
@ -512,7 +520,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
// matters in practice, though. // matters in practice, though.
let eq_goals = let eq_goals =
self.eq_and_get_goals(goal.param_env, goal.predicate.term, unconstrained_rhs)?; 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 // We only look at the `projection_ty` part here rather than
// looking at the "has changed" return from evaluate_goal, // looking at the "has changed" return from evaluate_goal,
@ -533,12 +541,12 @@ 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( let (has_changed, certainty, instantiate_goals) = self.evaluate_goal(
GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::No }, GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::No },
goal, goal,
)?; )?;
self.nested_goals.goals.extend(instantiate_goals); self.nested_goals.goals.extend(with_misc_source(instantiate_goals));
if has_changed { if has_changed {
unchanged_certainty = None; unchanged_certainty = None;
} }
@ -546,7 +554,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
match certainty { match certainty {
Certainty::Yes => {} Certainty::Yes => {}
Certainty::Maybe(_) => { 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)); unchanged_certainty = unchanged_certainty.map(|c| c.unify_with(certainty));
} }
} }
@ -670,7 +678,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
.at(&ObligationCause::dummy(), param_env) .at(&ObligationCause::dummy(), param_env)
.eq(DefineOpaqueTypes::No, lhs, rhs) .eq(DefineOpaqueTypes::No, lhs, rhs)
.map(|InferOk { value: (), obligations }| { .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| { .map_err(|e| {
debug!(?e, "failed to equate"); debug!(?e, "failed to equate");
@ -689,7 +697,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
.at(&ObligationCause::dummy(), param_env) .at(&ObligationCause::dummy(), param_env)
.sub(DefineOpaqueTypes::No, sub, sup) .sub(DefineOpaqueTypes::No, sub, sup)
.map(|InferOk { value: (), obligations }| { .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| { .map_err(|e| {
debug!(?e, "failed to subtype"); debug!(?e, "failed to subtype");
@ -709,7 +717,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
.at(&ObligationCause::dummy(), param_env) .at(&ObligationCause::dummy(), param_env)
.relate(DefineOpaqueTypes::No, lhs, variance, rhs) .relate(DefineOpaqueTypes::No, lhs, variance, rhs)
.map(|InferOk { value: (), obligations }| { .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| { .map_err(|e| {
debug!(?e, "failed to relate"); debug!(?e, "failed to relate");
@ -842,7 +850,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
true, true,
&mut obligations, &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(()) Ok(())
} }
@ -862,7 +870,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
hidden_ty, hidden_ty,
&mut obligations, &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 // Do something for each opaque/hidden pair defined with `def_id` in the

View File

@ -119,7 +119,7 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
) { ) {
for step in &probe.steps { for step in &probe.steps {
match step { match step {
&inspect::ProbeStep::AddGoal(goal) => nested_goals.push(goal), &inspect::ProbeStep::AddGoal(_source, goal) => nested_goals.push(goal),
inspect::ProbeStep::NestedProbe(ref probe) => { inspect::ProbeStep::NestedProbe(ref probe) => {
// Nested probes have to prove goals added in their parent // Nested probes have to prove goals added in their parent
// but do not leak them, so we truncate the added goals // but do not leak them, so we truncate the added goals

View File

@ -7,7 +7,7 @@ use std::mem;
use rustc_middle::traits::query::NoSolution; use rustc_middle::traits::query::NoSolution;
use rustc_middle::traits::solve::{ use rustc_middle::traits::solve::{
CanonicalInput, Certainty, Goal, IsNormalizesToHack, QueryInput, QueryResult, CanonicalInput, Certainty, Goal, GoalSource, IsNormalizesToHack, QueryInput, QueryResult,
}; };
use rustc_middle::ty::{self, TyCtxt}; use rustc_middle::ty::{self, TyCtxt};
use rustc_session::config::DumpSolverProofTree; use rustc_session::config::DumpSolverProofTree;
@ -216,7 +216,7 @@ impl<'tcx> WipProbe<'tcx> {
#[derive(Eq, PartialEq, Debug)] #[derive(Eq, PartialEq, Debug)]
enum WipProbeStep<'tcx> { enum WipProbeStep<'tcx> {
AddGoal(inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>), AddGoal(GoalSource, inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>),
EvaluateGoals(WipAddedGoalsEvaluation<'tcx>), EvaluateGoals(WipAddedGoalsEvaluation<'tcx>),
NestedProbe(WipProbe<'tcx>), NestedProbe(WipProbe<'tcx>),
CommitIfOkStart, CommitIfOkStart,
@ -226,7 +226,7 @@ enum WipProbeStep<'tcx> {
impl<'tcx> WipProbeStep<'tcx> { impl<'tcx> WipProbeStep<'tcx> {
fn finalize(self) -> inspect::ProbeStep<'tcx> { fn finalize(self) -> inspect::ProbeStep<'tcx> {
match self { match self {
WipProbeStep::AddGoal(goal) => inspect::ProbeStep::AddGoal(goal), WipProbeStep::AddGoal(source, goal) => inspect::ProbeStep::AddGoal(source, goal),
WipProbeStep::EvaluateGoals(eval) => inspect::ProbeStep::EvaluateGoals(eval.finalize()), WipProbeStep::EvaluateGoals(eval) => inspect::ProbeStep::EvaluateGoals(eval.finalize()),
WipProbeStep::NestedProbe(probe) => inspect::ProbeStep::NestedProbe(probe.finalize()), WipProbeStep::NestedProbe(probe) => inspect::ProbeStep::NestedProbe(probe.finalize()),
WipProbeStep::CommitIfOkStart => inspect::ProbeStep::CommitIfOkStart, WipProbeStep::CommitIfOkStart => inspect::ProbeStep::CommitIfOkStart,
@ -428,7 +428,11 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
} }
} }
pub fn add_goal(ecx: &mut EvalCtxt<'_, 'tcx>, goal: Goal<'tcx, ty::Predicate<'tcx>>) { pub fn add_goal(
ecx: &mut EvalCtxt<'_, 'tcx>,
source: GoalSource,
goal: Goal<'tcx, ty::Predicate<'tcx>>,
) {
// Can't use `if let Some(this) = ecx.inspect.as_mut()` here because // Can't use `if let Some(this) = ecx.inspect.as_mut()` here because
// we have to immutably use the `EvalCtxt` for `make_canonical_state`. // we have to immutably use the `EvalCtxt` for `make_canonical_state`.
if ecx.inspect.is_noop() { if ecx.inspect.is_noop() {
@ -442,7 +446,9 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
evaluation: WipProbe { steps, .. }, evaluation: WipProbe { steps, .. },
.. ..
}) })
| DebugSolver::Probe(WipProbe { steps, .. }) => steps.push(WipProbeStep::AddGoal(goal)), | DebugSolver::Probe(WipProbe { steps, .. }) => {
steps.push(WipProbeStep::AddGoal(source, goal))
}
s => unreachable!("tried to add {goal:?} to {s:?}"), s => unreachable!("tried to add {goal:?} to {s:?}"),
} }
} }

View File

@ -19,8 +19,8 @@ use rustc_infer::infer::DefineOpaqueTypes;
use rustc_infer::traits::query::NoSolution; use rustc_infer::traits::query::NoSolution;
use rustc_middle::infer::canonical::CanonicalVarInfos; use rustc_middle::infer::canonical::CanonicalVarInfos;
use rustc_middle::traits::solve::{ use rustc_middle::traits::solve::{
CanonicalResponse, Certainty, ExternalConstraintsData, Goal, IsNormalizesToHack, QueryResult, CanonicalResponse, Certainty, ExternalConstraintsData, Goal, GoalSource, IsNormalizesToHack,
Response, QueryResult, Response,
}; };
use rustc_middle::ty::{self, OpaqueTypeKey, Ty, TyCtxt, UniverseIndex}; use rustc_middle::ty::{self, OpaqueTypeKey, Ty, TyCtxt, UniverseIndex};
use rustc_middle::ty::{ use rustc_middle::ty::{
@ -157,7 +157,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
) -> QueryResult<'tcx> { ) -> QueryResult<'tcx> {
match self.well_formed_goals(goal.param_env, goal.predicate) { match self.well_formed_goals(goal.param_env, goal.predicate) {
Some(goals) => { Some(goals) => {
self.add_goals(goals); self.add_goals(GoalSource::Misc, goals);
self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes) self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
} }
None => self.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS), None => self.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS),
@ -223,15 +223,19 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
} }
#[instrument(level = "debug", skip(self))] #[instrument(level = "debug", skip(self))]
fn add_goal(&mut self, goal: Goal<'tcx, ty::Predicate<'tcx>>) { fn add_goal(&mut self, source: GoalSource, goal: Goal<'tcx, ty::Predicate<'tcx>>) {
inspect::ProofTreeBuilder::add_goal(self, goal); inspect::ProofTreeBuilder::add_goal(self, source, goal);
self.nested_goals.goals.push(goal); self.nested_goals.goals.push((source, goal));
} }
#[instrument(level = "debug", skip(self, goals))] #[instrument(level = "debug", skip(self, goals))]
fn add_goals(&mut self, goals: impl IntoIterator<Item = Goal<'tcx, ty::Predicate<'tcx>>>) { fn add_goals(
&mut self,
source: GoalSource,
goals: impl IntoIterator<Item = Goal<'tcx, ty::Predicate<'tcx>>>,
) {
for goal in goals { for goal in goals {
self.add_goal(goal); self.add_goal(source, goal);
} }
} }
@ -335,7 +339,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
param_env, param_env,
ty::NormalizesTo { alias, term: normalized_ty.into() }, ty::NormalizesTo { alias, term: normalized_ty.into() },
); );
this.add_goal(normalizes_to_goal); this.add_goal(GoalSource::Misc, normalizes_to_goal);
this.try_evaluate_added_goals()?; this.try_evaluate_added_goals()?;
let ty = this.resolve_vars_if_possible(normalized_ty); let ty = this.resolve_vars_if_possible(normalized_ty);
Ok(this.try_normalize_ty_recur(param_env, define_opaque_types, depth + 1, ty)) Ok(this.try_normalize_ty_recur(param_env, define_opaque_types, depth + 1, ty))

View File

@ -4,10 +4,10 @@
//! 1. instantiate substs, //! 1. instantiate substs,
//! 2. equate the self type, and //! 2. equate the self type, and
//! 3. instantiate and register where clauses. //! 3. instantiate and register where clauses.
use rustc_middle::traits::solve::{Certainty, Goal, QueryResult}; use rustc_middle::traits::solve::{Certainty, Goal, GoalSource, QueryResult};
use rustc_middle::ty; use rustc_middle::ty;
use super::EvalCtxt; use crate::solve::EvalCtxt;
impl<'tcx> EvalCtxt<'_, 'tcx> { impl<'tcx> EvalCtxt<'_, 'tcx> {
pub(super) fn normalize_inherent_associated_type( pub(super) fn normalize_inherent_associated_type(
@ -38,7 +38,13 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
.expect("expected goal term to be fully unconstrained"); .expect("expected goal term to be fully unconstrained");
// Check both where clauses on the impl and IAT // Check both where clauses on the impl and IAT
//
// FIXME(-Znext-solver=coinductive): I think this should be split
// and we tag the impl bounds with `GoalSource::ImplWhereBound`?
// Right not this includes both the impl and the assoc item where bounds,
// and I don't think the assoc item where-bounds are allowed to be coinductive.
self.add_goals( self.add_goals(
GoalSource::Misc,
tcx.predicates_of(inherent.def_id) tcx.predicates_of(inherent.def_id)
.instantiate(tcx, inherent_substs) .instantiate(tcx, inherent_substs)
.into_iter() .into_iter()

View File

@ -1,7 +1,7 @@
use crate::traits::{check_args_compatible, specialization_graph}; use crate::traits::{check_args_compatible, specialization_graph};
use super::assembly::{self, structural_traits, Candidate}; use super::assembly::{self, structural_traits, Candidate};
use super::EvalCtxt; use super::{EvalCtxt, GoalSource};
use rustc_hir::def::DefKind; use rustc_hir::def::DefKind;
use rustc_hir::def_id::DefId; use rustc_hir::def_id::DefId;
use rustc_hir::LangItem; use rustc_hir::LangItem;
@ -128,6 +128,7 @@ impl<'tcx> assembly::GoalKind<'tcx> for NormalizesTo<'tcx> {
// Add GAT where clauses from the trait's definition // Add GAT where clauses from the trait's definition
ecx.add_goals( ecx.add_goals(
GoalSource::Misc,
tcx.predicates_of(goal.predicate.def_id()) tcx.predicates_of(goal.predicate.def_id())
.instantiate_own(tcx, goal.predicate.alias.args) .instantiate_own(tcx, goal.predicate.alias.args)
.map(|(pred, _)| goal.with(tcx, pred)), .map(|(pred, _)| goal.with(tcx, pred)),
@ -169,10 +170,11 @@ impl<'tcx> assembly::GoalKind<'tcx> for NormalizesTo<'tcx> {
.predicates .predicates
.into_iter() .into_iter()
.map(|pred| goal.with(tcx, pred)); .map(|pred| goal.with(tcx, pred));
ecx.add_goals(where_clause_bounds); ecx.add_goals(GoalSource::ImplWhereBound, where_clause_bounds);
// Add GAT where clauses from the trait's definition // Add GAT where clauses from the trait's definition
ecx.add_goals( ecx.add_goals(
GoalSource::Misc,
tcx.predicates_of(goal.predicate.def_id()) tcx.predicates_of(goal.predicate.def_id())
.instantiate_own(tcx, goal.predicate.alias.args) .instantiate_own(tcx, goal.predicate.alias.args)
.map(|(pred, _)| goal.with(tcx, pred)), .map(|(pred, _)| goal.with(tcx, pred)),
@ -413,7 +415,8 @@ impl<'tcx> assembly::GoalKind<'tcx> for NormalizesTo<'tcx> {
DUMMY_SP, DUMMY_SP,
[ty::GenericArg::from(goal.predicate.self_ty())], [ty::GenericArg::from(goal.predicate.self_ty())],
); );
ecx.add_goal(goal.with(tcx, sized_predicate)); // FIXME(-Znext-solver=coinductive): Should this be `GoalSource::ImplWhereBound`?
ecx.add_goal(GoalSource::Misc, goal.with(tcx, sized_predicate));
tcx.types.unit tcx.types.unit
} }
@ -421,7 +424,11 @@ impl<'tcx> assembly::GoalKind<'tcx> for NormalizesTo<'tcx> {
None => tcx.types.unit, None => tcx.types.unit,
Some(field_def) => { Some(field_def) => {
let self_ty = field_def.ty(tcx, args); let self_ty = field_def.ty(tcx, args);
ecx.add_goal(goal.with(tcx, goal.predicate.with_self_ty(tcx, self_ty))); // FIXME(-Znext-solver=coinductive): Should this be `GoalSource::ImplWhereBound`?
ecx.add_goal(
GoalSource::Misc,
goal.with(tcx, goal.predicate.with_self_ty(tcx, self_ty)),
);
return ecx return ecx
.evaluate_added_goals_and_make_canonical_response(Certainty::Yes); .evaluate_added_goals_and_make_canonical_response(Certainty::Yes);
} }
@ -431,7 +438,11 @@ impl<'tcx> assembly::GoalKind<'tcx> for NormalizesTo<'tcx> {
ty::Tuple(elements) => match elements.last() { ty::Tuple(elements) => match elements.last() {
None => tcx.types.unit, None => tcx.types.unit,
Some(&self_ty) => { Some(&self_ty) => {
ecx.add_goal(goal.with(tcx, goal.predicate.with_self_ty(tcx, self_ty))); // FIXME(-Znext-solver=coinductive): Should this be `GoalSource::ImplWhereBound`?
ecx.add_goal(
GoalSource::Misc,
goal.with(tcx, goal.predicate.with_self_ty(tcx, self_ty)),
);
return ecx return ecx
.evaluate_added_goals_and_make_canonical_response(Certainty::Yes); .evaluate_added_goals_and_make_canonical_response(Certainty::Yes);
} }

View File

@ -3,10 +3,10 @@
//! //!
//! Since a weak alias is not ambiguous, this just computes the `type_of` of //! Since a weak alias is not ambiguous, this just computes the `type_of` of
//! the alias and registers the where-clauses of the type alias. //! the alias and registers the where-clauses of the type alias.
use rustc_middle::traits::solve::{Certainty, Goal, QueryResult}; use rustc_middle::traits::solve::{Certainty, Goal, GoalSource, QueryResult};
use rustc_middle::ty; use rustc_middle::ty;
use super::EvalCtxt; use crate::solve::EvalCtxt;
impl<'tcx> EvalCtxt<'_, 'tcx> { impl<'tcx> EvalCtxt<'_, 'tcx> {
pub(super) fn normalize_weak_type( pub(super) fn normalize_weak_type(
@ -22,6 +22,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
// Check where clauses // Check where clauses
self.add_goals( self.add_goals(
GoalSource::Misc,
tcx.predicates_of(weak_ty.def_id) tcx.predicates_of(weak_ty.def_id)
.instantiate(tcx, weak_ty.args) .instantiate(tcx, weak_ty.args)
.predicates .predicates

View File

@ -1,3 +1,5 @@
use crate::solve::GoalSource;
use super::EvalCtxt; use super::EvalCtxt;
use rustc_middle::traits::solve::{Certainty, Goal, QueryResult}; use rustc_middle::traits::solve::{Certainty, Goal, QueryResult};
use rustc_middle::ty::{self, ProjectionPredicate}; use rustc_middle::ty::{self, ProjectionPredicate};
@ -22,14 +24,15 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
) )
.into(), .into(),
}; };
self.add_goal(goal.with( let goal = goal.with(
tcx, tcx,
ty::PredicateKind::AliasRelate( ty::PredicateKind::AliasRelate(
projection_term, projection_term,
goal.predicate.term, goal.predicate.term,
ty::AliasRelationDirection::Equate, ty::AliasRelationDirection::Equate,
), ),
)); );
self.add_goal(GoalSource::Misc, goal);
self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes) self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
} }
} }

View File

@ -1,7 +1,7 @@
//! Dealing with trait goals, i.e. `T: Trait<'a, U>`. //! Dealing with trait goals, i.e. `T: Trait<'a, U>`.
use super::assembly::{self, structural_traits, Candidate}; use super::assembly::{self, structural_traits, Candidate};
use super::{EvalCtxt, SolverMode}; use super::{EvalCtxt, GoalSource, SolverMode};
use rustc_hir::def_id::DefId; use rustc_hir::def_id::DefId;
use rustc_hir::{LangItem, Movability}; use rustc_hir::{LangItem, Movability};
use rustc_infer::traits::query::NoSolution; use rustc_infer::traits::query::NoSolution;
@ -72,7 +72,7 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
.predicates .predicates
.into_iter() .into_iter()
.map(|pred| goal.with(tcx, pred)); .map(|pred| goal.with(tcx, pred));
ecx.add_goals(where_clause_bounds); ecx.add_goals(GoalSource::ImplWhereBound, where_clause_bounds);
ecx.evaluate_added_goals_and_make_canonical_response(maximal_certainty) ecx.evaluate_added_goals_and_make_canonical_response(maximal_certainty)
}) })
@ -172,7 +172,11 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
let nested_obligations = tcx let nested_obligations = tcx
.predicates_of(goal.predicate.def_id()) .predicates_of(goal.predicate.def_id())
.instantiate(tcx, goal.predicate.trait_ref.args); .instantiate(tcx, goal.predicate.trait_ref.args);
ecx.add_goals(nested_obligations.predicates.into_iter().map(|p| goal.with(tcx, p))); // FIXME(-Znext-solver=coinductive): Should this be `GoalSource::ImplWhereBound`?
ecx.add_goals(
GoalSource::Misc,
nested_obligations.predicates.into_iter().map(|p| goal.with(tcx, p)),
);
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes) ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
}) })
} }
@ -512,17 +516,23 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
// Check that the type implements all of the predicates of the trait object. // Check that the type implements all of the predicates of the trait object.
// (i.e. the principal, all of the associated types match, and any auto traits) // (i.e. the principal, all of the associated types match, and any auto traits)
ecx.add_goals(b_data.iter().map(|pred| goal.with(tcx, pred.with_self_ty(tcx, a_ty)))); ecx.add_goals(
GoalSource::ImplWhereBound,
b_data.iter().map(|pred| goal.with(tcx, pred.with_self_ty(tcx, a_ty))),
);
// The type must be `Sized` to be unsized. // The type must be `Sized` to be unsized.
if let Some(sized_def_id) = tcx.lang_items().sized_trait() { if let Some(sized_def_id) = tcx.lang_items().sized_trait() {
ecx.add_goal(goal.with(tcx, ty::TraitRef::new(tcx, sized_def_id, [a_ty]))); ecx.add_goal(
GoalSource::ImplWhereBound,
goal.with(tcx, ty::TraitRef::new(tcx, sized_def_id, [a_ty])),
);
} else { } else {
return Err(NoSolution); return Err(NoSolution);
} }
// The type must outlive the lifetime of the `dyn` we're unsizing into. // The type must outlive the lifetime of the `dyn` we're unsizing into.
ecx.add_goal(goal.with(tcx, ty::OutlivesPredicate(a_ty, b_region))); ecx.add_goal(GoalSource::Misc, goal.with(tcx, ty::OutlivesPredicate(a_ty, b_region)));
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes) ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
}) })
} }
@ -749,11 +759,14 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
} }
// Also require that a_ty's lifetime outlives b_ty's lifetime. // Also require that a_ty's lifetime outlives b_ty's lifetime.
self.add_goal(Goal::new( self.add_goal(
self.tcx(), GoalSource::ImplWhereBound,
param_env, Goal::new(
ty::Binder::dummy(ty::OutlivesPredicate(a_region, b_region)), self.tcx(),
)); param_env,
ty::Binder::dummy(ty::OutlivesPredicate(a_region, b_region)),
),
);
self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes) self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
} }
@ -826,14 +839,17 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
// Finally, we require that `TailA: Unsize<TailB>` for the tail field // Finally, we require that `TailA: Unsize<TailB>` for the tail field
// types. // types.
self.eq(goal.param_env, unsized_a_ty, b_ty)?; self.eq(goal.param_env, unsized_a_ty, b_ty)?;
self.add_goal(goal.with( self.add_goal(
tcx, GoalSource::ImplWhereBound,
ty::TraitRef::new( goal.with(
tcx, tcx,
tcx.lang_items().unsize_trait().unwrap(), ty::TraitRef::new(
[a_tail_ty, b_tail_ty], tcx,
tcx.lang_items().unsize_trait().unwrap(),
[a_tail_ty, b_tail_ty],
),
), ),
)); );
self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes) self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
} }
@ -865,14 +881,17 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
self.eq(goal.param_env, unsized_a_ty, b_ty)?; self.eq(goal.param_env, unsized_a_ty, b_ty)?;
// Similar to ADTs, require that we can unsize the tail. // Similar to ADTs, require that we can unsize the tail.
self.add_goal(goal.with( self.add_goal(
tcx, GoalSource::ImplWhereBound,
ty::TraitRef::new( goal.with(
tcx, tcx,
tcx.lang_items().unsize_trait().unwrap(), ty::TraitRef::new(
[a_last_ty, b_last_ty], tcx,
tcx.lang_items().unsize_trait().unwrap(),
[a_last_ty, b_last_ty],
),
), ),
)); );
self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes) self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
} }
@ -981,6 +1000,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
) -> QueryResult<'tcx> { ) -> QueryResult<'tcx> {
self.probe_misc_candidate("constituent tys").enter(|ecx| { self.probe_misc_candidate("constituent tys").enter(|ecx| {
ecx.add_goals( ecx.add_goals(
GoalSource::ImplWhereBound,
constituent_tys(ecx, goal.predicate.self_ty())? constituent_tys(ecx, goal.predicate.self_ty())?
.into_iter() .into_iter()
.map(|ty| goal.with(ecx.tcx(), goal.predicate.with_self_ty(ecx.tcx(), ty))) .map(|ty| goal.with(ecx.tcx(), goal.predicate.with_self_ty(ecx.tcx(), ty)))