Skip to content

Record certainty of evaluate_added_goals_and_make_canonical_response call in candidate #124444

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.

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

Merged
merged 1 commit into from
Apr 28, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
6 changes: 6 additions & 0 deletions compiler/rustc_middle/src/traits/solve/inspect.rs
Original file line number Diff line number Diff line change
Expand Up @@ -122,6 +122,12 @@ pub enum ProbeStep<'tcx> {
/// used whenever there are multiple candidates to prove the
/// current goalby .
NestedProbe(Probe<'tcx>),
/// A call to `EvalCtxt::evaluate_added_goals_make_canonical_response` with
/// `Certainty` was made. This is the certainty passed in, so it's not unified
/// with the certainty of the `try_evaluate_added_goals` that is done within;
/// if it's `Certainty::Yes`, then we can trust that the candidate is "finished"
/// and we didn't force ambiguity for some reason.
MakeCanonicalResponse { shallow_certainty: Certainty },
}

/// What kind of probe we're in. In case the probe represents a candidate, or
Expand Down
3 changes: 3 additions & 0 deletions compiler/rustc_middle/src/traits/solve/inspect/format.rs
Original file line number Diff line number Diff line change
Expand Up @@ -132,6 +132,9 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
}
ProbeStep::EvaluateGoals(eval) => this.format_added_goals_evaluation(eval)?,
ProbeStep::NestedProbe(probe) => this.format_probe(probe)?,
ProbeStep::MakeCanonicalResponse { shallow_certainty } => {
writeln!(this.f, "EVALUATE GOALS AND MAKE RESPONSE: {shallow_certainty:?}")?
}
}
}
Ok(())
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -98,6 +98,8 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
previous call to `try_evaluate_added_goals!`"
);

self.inspect.make_canonical_response(certainty);

// When normalizing, we've replaced the expected term with an unconstrained
// inference variable. This means that we dropped information which could
// have been important. We handle this by instead returning the nested goals
Expand Down
21 changes: 21 additions & 0 deletions compiler/rustc_trait_selection/src/solve/inspect/analyse.rs
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,7 @@ pub struct InspectCandidate<'a, 'tcx> {
nested_goals: Vec<inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>>,
final_state: inspect::CanonicalState<'tcx, ()>,
result: QueryResult<'tcx>,
candidate_certainty: Option<Certainty>,
}

impl<'a, 'tcx> InspectCandidate<'a, 'tcx> {
Expand All @@ -56,6 +57,19 @@ impl<'a, 'tcx> InspectCandidate<'a, 'tcx> {
self.result.map(|c| c.value.certainty)
}

/// Certainty passed into `evaluate_added_goals_and_make_canonical_response`.
///
/// If this certainty is `Some(Yes)`, then we must be confident that the candidate
/// must hold iff it's nested goals hold. This is not true if the certainty is
/// `Some(Maybe)`, which suggests we forced ambiguity instead, or if it is `None`,
/// which suggests we may have not assembled any candidates at all.
///
/// This is *not* the certainty of the candidate's nested evaluation, which can be
/// accessed with [`Self::result`] instead.
pub fn candidate_certainty(&self) -> Option<Certainty> {
self.candidate_certainty
}

/// Visit all nested goals of this candidate without rolling
/// back their inference constraints. This function modifies
/// the state of the `infcx`.
Expand Down Expand Up @@ -160,7 +174,9 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
nested_goals: &mut Vec<inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>>,
probe: &inspect::Probe<'tcx>,
) {
let mut candidate_certainty = None;
let num_candidates = candidates.len();

for step in &probe.steps {
match step {
&inspect::ProbeStep::AddGoal(_source, goal) => nested_goals.push(goal),
Expand All @@ -172,6 +188,9 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
self.candidates_recur(candidates, nested_goals, probe);
nested_goals.truncate(num_goals);
}
inspect::ProbeStep::MakeCanonicalResponse { shallow_certainty } => {
assert_eq!(candidate_certainty.replace(*shallow_certainty), None);
}
inspect::ProbeStep::EvaluateGoals(_) => (),
}
}
Expand All @@ -195,6 +214,7 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
nested_goals: nested_goals.clone(),
final_state: probe.final_state,
result,
candidate_certainty,
})
}
}
Expand All @@ -206,6 +226,7 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
nested_goals: nested_goals.clone(),
final_state: probe.final_state,
result,
candidate_certainty,
});
}
}
Expand Down
17 changes: 17 additions & 0 deletions compiler/rustc_trait_selection/src/solve/inspect/build.rs
Original file line number Diff line number Diff line change
Expand Up @@ -241,6 +241,7 @@ enum WipProbeStep<'tcx> {
AddGoal(GoalSource, inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>),
EvaluateGoals(WipAddedGoalsEvaluation<'tcx>),
NestedProbe(WipProbe<'tcx>),
MakeCanonicalResponse { shallow_certainty: Certainty },
}

impl<'tcx> WipProbeStep<'tcx> {
Expand All @@ -249,6 +250,9 @@ impl<'tcx> WipProbeStep<'tcx> {
WipProbeStep::AddGoal(source, goal) => inspect::ProbeStep::AddGoal(source, goal),
WipProbeStep::EvaluateGoals(eval) => inspect::ProbeStep::EvaluateGoals(eval.finalize()),
WipProbeStep::NestedProbe(probe) => inspect::ProbeStep::NestedProbe(probe.finalize()),
WipProbeStep::MakeCanonicalResponse { shallow_certainty } => {
inspect::ProbeStep::MakeCanonicalResponse { shallow_certainty }
}
}
}
}
Expand Down Expand Up @@ -530,6 +534,19 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
}
}

pub fn make_canonical_response(&mut self, shallow_certainty: Certainty) {
match self.as_mut() {
Some(DebugSolver::GoalEvaluationStep(state)) => {
state
.current_evaluation_scope()
.steps
.push(WipProbeStep::MakeCanonicalResponse { shallow_certainty });
}
None => {}
_ => {}
}
}

pub fn finish_probe(mut self) -> ProofTreeBuilder<'tcx> {
match self.as_mut() {
None => {}
Expand Down
Loading