about summary refs log tree commit diff
diff options
context:
space:
mode:
authorMatthias Krüger <matthias.krueger@famsik.de>2023-09-18 13:02:18 +0200
committerGitHub <noreply@github.com>2023-09-18 13:02:18 +0200
commit944c4134d235bbecc88ecd6129b4e5b2cacb9c2e (patch)
tree25f28a4d501c1d5683c00a385baae9075b02a108
parentc843ac2ad9368f71f86ac8aad4319e60ae989b3d (diff)
parent0cb800ec342c95478fbca4ae94bd5a6c10c9c093 (diff)
downloadrust-944c4134d235bbecc88ecd6129b4e5b2cacb9c2e.tar.gz
rust-944c4134d235bbecc88ecd6129b4e5b2cacb9c2e.zip
Rollup merge of #115838 - lcnr:added-goals, r=compiler-errors
inspect: closer to proof trees for coherence

a continuation of #115751. Now explicitly store the added goals

r? ```@compiler-errors```
-rw-r--r--compiler/rustc_middle/src/traits/solve/inspect.rs33
-rw-r--r--compiler/rustc_middle/src/traits/solve/inspect/format.rs34
-rw-r--r--compiler/rustc_trait_selection/src/solve/eval_ctxt.rs27
-rw-r--r--compiler/rustc_trait_selection/src/solve/eval_ctxt/probe.rs4
-rw-r--r--compiler/rustc_trait_selection/src/solve/inspect.rs138
-rw-r--r--compiler/rustc_trait_selection/src/solve/mod.rs10
-rw-r--r--compiler/rustc_trait_selection/src/solve/search_graph/mod.rs6
7 files changed, 160 insertions, 92 deletions
diff --git a/compiler/rustc_middle/src/traits/solve/inspect.rs b/compiler/rustc_middle/src/traits/solve/inspect.rs
index d8b3a061b77..c3ed40867cf 100644
--- a/compiler/rustc_middle/src/traits/solve/inspect.rs
+++ b/compiler/rustc_middle/src/traits/solve/inspect.rs
@@ -15,9 +15,15 @@ pub enum CacheHit {
 }
 
 #[derive(Eq, PartialEq)]
+pub enum GoalEvaluationKind {
+    Root,
+    Nested { is_normalizes_to_hack: IsNormalizesToHack },
+}
+
+#[derive(Eq, PartialEq)]
 pub struct GoalEvaluation<'tcx> {
     pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
-    pub is_normalizes_to_hack: IsNormalizesToHack,
+    pub kind: GoalEvaluationKind,
     pub evaluation: CanonicalGoalEvaluation<'tcx>,
     pub returned_goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
 }
@@ -25,12 +31,12 @@ pub struct GoalEvaluation<'tcx> {
 #[derive(Eq, PartialEq)]
 pub struct CanonicalGoalEvaluation<'tcx> {
     pub goal: CanonicalInput<'tcx>,
-    pub kind: GoalEvaluationKind<'tcx>,
+    pub kind: CanonicalGoalEvaluationKind<'tcx>,
     pub result: QueryResult<'tcx>,
 }
 
 #[derive(Eq, PartialEq)]
-pub enum GoalEvaluationKind<'tcx> {
+pub enum CanonicalGoalEvaluationKind<'tcx> {
     Overflow,
     CacheHit(CacheHit),
     Uncached { revisions: Vec<GoalEvaluationStep<'tcx>> },
@@ -52,22 +58,31 @@ pub struct GoalEvaluationStep<'tcx> {
     pub instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
 
     /// The actual evaluation of the goal, always `ProbeKind::Root`.
-    pub evaluation: GoalCandidate<'tcx>,
+    pub evaluation: Probe<'tcx>,
 }
 
+/// A self-contained computation during trait solving. This either
+/// corresponds to a `EvalCtxt::probe(_X)` call or the root evaluation
+/// of a goal.
 #[derive(Eq, PartialEq)]
-pub struct GoalCandidate<'tcx> {
-    pub added_goals_evaluations: Vec<AddedGoalsEvaluation<'tcx>>,
-    pub candidates: Vec<GoalCandidate<'tcx>>,
+pub struct Probe<'tcx> {
+    pub steps: Vec<ProbeStep<'tcx>>,
     pub kind: ProbeKind<'tcx>,
 }
 
-impl Debug for GoalCandidate<'_> {
+impl Debug for Probe<'_> {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        ProofTreeFormatter::new(f).format_candidate(self)
+        ProofTreeFormatter::new(f).format_probe(self)
     }
 }
 
+#[derive(Eq, PartialEq)]
+pub enum ProbeStep<'tcx> {
+    AddGoal(Goal<'tcx, ty::Predicate<'tcx>>),
+    EvaluateGoals(AddedGoalsEvaluation<'tcx>),
+    NestedProbe(Probe<'tcx>),
+}
+
 #[derive(Debug, PartialEq, Eq)]
 pub enum ProbeKind<'tcx> {
     /// The root inference context while proving a goal.
diff --git a/compiler/rustc_middle/src/traits/solve/inspect/format.rs b/compiler/rustc_middle/src/traits/solve/inspect/format.rs
index d916e80a625..d33e83ae1ed 100644
--- a/compiler/rustc_middle/src/traits/solve/inspect/format.rs
+++ b/compiler/rustc_middle/src/traits/solve/inspect/format.rs
@@ -40,9 +40,12 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
     }
 
     pub(super) fn format_goal_evaluation(&mut self, eval: &GoalEvaluation<'_>) -> std::fmt::Result {
-        let goal_text = match eval.is_normalizes_to_hack {
-            IsNormalizesToHack::Yes => "NORMALIZES-TO HACK GOAL",
-            IsNormalizesToHack::No => "GOAL",
+        let goal_text = match eval.kind {
+            GoalEvaluationKind::Root => "ROOT GOAL",
+            GoalEvaluationKind::Nested { is_normalizes_to_hack } => match is_normalizes_to_hack {
+                IsNormalizesToHack::No => "GOAL",
+                IsNormalizesToHack::Yes => "NORMALIZES-TO HACK GOAL",
+            },
         };
         writeln!(self.f, "{}: {:?}", goal_text, eval.uncanonicalized_goal)?;
         self.nested(|this| this.format_canonical_goal_evaluation(&eval.evaluation))?;
@@ -68,16 +71,16 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
         writeln!(self.f, "GOAL: {:?}", eval.goal)?;
 
         match &eval.kind {
-            GoalEvaluationKind::Overflow => {
+            CanonicalGoalEvaluationKind::Overflow => {
                 writeln!(self.f, "OVERFLOW: {:?}", eval.result)
             }
-            GoalEvaluationKind::CacheHit(CacheHit::Global) => {
+            CanonicalGoalEvaluationKind::CacheHit(CacheHit::Global) => {
                 writeln!(self.f, "GLOBAL CACHE HIT: {:?}", eval.result)
             }
-            GoalEvaluationKind::CacheHit(CacheHit::Provisional) => {
+            CanonicalGoalEvaluationKind::CacheHit(CacheHit::Provisional) => {
                 writeln!(self.f, "PROVISIONAL CACHE HIT: {:?}", eval.result)
             }
-            GoalEvaluationKind::Uncached { revisions } => {
+            CanonicalGoalEvaluationKind::Uncached { revisions } => {
                 for (n, step) in revisions.iter().enumerate() {
                     writeln!(self.f, "REVISION {n}")?;
                     self.nested(|this| this.format_evaluation_step(step))?;
@@ -92,11 +95,11 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
         evaluation_step: &GoalEvaluationStep<'_>,
     ) -> std::fmt::Result {
         writeln!(self.f, "INSTANTIATED: {:?}", evaluation_step.instantiated_goal)?;
-        self.format_candidate(&evaluation_step.evaluation)
+        self.format_probe(&evaluation_step.evaluation)
     }
 
-    pub(super) fn format_candidate(&mut self, candidate: &GoalCandidate<'_>) -> std::fmt::Result {
-        match &candidate.kind {
+    pub(super) fn format_probe(&mut self, probe: &Probe<'_>) -> std::fmt::Result {
+        match &probe.kind {
             ProbeKind::Root { result } => {
                 writeln!(self.f, "ROOT RESULT: {result:?}")
             }
@@ -118,11 +121,12 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
         }?;
 
         self.nested(|this| {
-            for candidate in &candidate.candidates {
-                this.format_candidate(candidate)?;
-            }
-            for nested in &candidate.added_goals_evaluations {
-                this.format_added_goals_evaluation(nested)?;
+            for step in &probe.steps {
+                match step {
+                    ProbeStep::AddGoal(goal) => writeln!(this.f, "ADDED GOAL: {goal:?}")?,
+                    ProbeStep::EvaluateGoals(eval) => this.format_added_goals_evaluation(eval)?,
+                    ProbeStep::NestedProbe(probe) => this.format_probe(probe)?,
+                }
             }
             Ok(())
         })
diff --git a/compiler/rustc_trait_selection/src/solve/eval_ctxt.rs b/compiler/rustc_trait_selection/src/solve/eval_ctxt.rs
index 307c0516f70..51cb192a1e8 100644
--- a/compiler/rustc_trait_selection/src/solve/eval_ctxt.rs
+++ b/compiler/rustc_trait_selection/src/solve/eval_ctxt.rs
@@ -28,8 +28,8 @@ use std::ops::ControlFlow;
 use crate::traits::vtable::{count_own_vtable_entries, prepare_vtable_segments, VtblSegment};
 
 use super::inspect::ProofTreeBuilder;
-use super::search_graph;
 use super::SolverMode;
+use super::{search_graph, GoalEvaluationKind};
 use super::{search_graph::SearchGraph, Goal};
 pub use select::InferCtxtSelectExt;
 
@@ -85,7 +85,7 @@ pub struct EvalCtxt<'a, 'tcx> {
     // evaluation code.
     tainted: Result<(), NoSolution>,
 
-    inspect: ProofTreeBuilder<'tcx>,
+    pub(super) inspect: ProofTreeBuilder<'tcx>,
 }
 
 #[derive(Debug, Clone)]
@@ -164,7 +164,7 @@ impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> {
         Option<inspect::GoalEvaluation<'tcx>>,
     ) {
         EvalCtxt::enter_root(self, generate_proof_tree, |ecx| {
-            ecx.evaluate_goal(IsNormalizesToHack::No, goal)
+            ecx.evaluate_goal(GoalEvaluationKind::Root, goal)
         })
     }
 }
@@ -340,11 +340,11 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
     /// been constrained and the certainty of the result.
     fn evaluate_goal(
         &mut self,
-        is_normalizes_to_hack: IsNormalizesToHack,
+        goal_evaluation_kind: GoalEvaluationKind,
         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);
-        let mut goal_evaluation = self.inspect.new_goal_evaluation(goal, is_normalizes_to_hack);
+        let mut goal_evaluation = self.inspect.new_goal_evaluation(goal, goal_evaluation_kind);
         let encountered_overflow = self.search_graph.encountered_overflow();
         let canonical_response = EvalCtxt::evaluate_canonical_goal(
             self.tcx(),
@@ -389,7 +389,10 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
         // solver cycle.
         if cfg!(debug_assertions)
             && has_changed
-            && is_normalizes_to_hack == IsNormalizesToHack::No
+            && !matches!(
+                goal_evaluation_kind,
+                GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::Yes }
+            )
             && !self.search_graph.in_cycle()
         {
             // The nested evaluation has to happen with the original state
@@ -561,8 +564,10 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
                 },
             );
 
-            let (_, certainty, instantiate_goals) =
-                self.evaluate_goal(IsNormalizesToHack::Yes, unconstrained_goal)?;
+            let (_, certainty, instantiate_goals) = self.evaluate_goal(
+                GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::Yes },
+                unconstrained_goal,
+            )?;
             self.add_goals(instantiate_goals);
 
             // Finally, equate the goal's RHS with the unconstrained var.
@@ -596,8 +601,10 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
         }
 
         for goal in goals.goals.drain(..) {
-            let (has_changed, certainty, instantiate_goals) =
-                self.evaluate_goal(IsNormalizesToHack::No, goal)?;
+            let (has_changed, certainty, instantiate_goals) = self.evaluate_goal(
+                GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::No },
+                goal,
+            )?;
             self.add_goals(instantiate_goals);
             if has_changed {
                 unchanged_certainty = None;
diff --git a/compiler/rustc_trait_selection/src/solve/eval_ctxt/probe.rs b/compiler/rustc_trait_selection/src/solve/eval_ctxt/probe.rs
index f88cfbac3f3..6087b916790 100644
--- a/compiler/rustc_trait_selection/src/solve/eval_ctxt/probe.rs
+++ b/compiler/rustc_trait_selection/src/solve/eval_ctxt/probe.rs
@@ -24,13 +24,13 @@ where
             search_graph: outer_ecx.search_graph,
             nested_goals: outer_ecx.nested_goals.clone(),
             tainted: outer_ecx.tainted,
-            inspect: outer_ecx.inspect.new_goal_candidate(),
+            inspect: outer_ecx.inspect.new_probe(),
         };
         let r = nested_ecx.infcx.probe(|_| f(&mut nested_ecx));
         if !outer_ecx.inspect.is_noop() {
             let probe_kind = probe_kind(&r);
             nested_ecx.inspect.probe_kind(probe_kind);
-            outer_ecx.inspect.goal_candidate(nested_ecx.inspect);
+            outer_ecx.inspect.finish_probe(nested_ecx.inspect);
         }
         r
     }
diff --git a/compiler/rustc_trait_selection/src/solve/inspect.rs b/compiler/rustc_trait_selection/src/solve/inspect.rs
index 46025da7683..749bba33c9b 100644
--- a/compiler/rustc_trait_selection/src/solve/inspect.rs
+++ b/compiler/rustc_trait_selection/src/solve/inspect.rs
@@ -7,13 +7,13 @@ use rustc_middle::ty::{self, TyCtxt};
 use rustc_session::config::DumpSolverProofTree;
 
 use super::eval_ctxt::UseGlobalCache;
-use super::GenerateProofTree;
+use super::{GenerateProofTree, GoalEvaluationKind};
 
 #[derive(Eq, PartialEq, Debug)]
 pub struct WipGoalEvaluation<'tcx> {
     pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
+    pub kind: WipGoalEvaluationKind,
     pub evaluation: Option<WipCanonicalGoalEvaluation<'tcx>>,
-    pub is_normalizes_to_hack: IsNormalizesToHack,
     pub returned_goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
 }
 
@@ -21,8 +21,13 @@ impl<'tcx> WipGoalEvaluation<'tcx> {
     pub fn finalize(self) -> inspect::GoalEvaluation<'tcx> {
         inspect::GoalEvaluation {
             uncanonicalized_goal: self.uncanonicalized_goal,
+            kind: match self.kind {
+                WipGoalEvaluationKind::Root => inspect::GoalEvaluationKind::Root,
+                WipGoalEvaluationKind::Nested { is_normalizes_to_hack } => {
+                    inspect::GoalEvaluationKind::Nested { is_normalizes_to_hack }
+                }
+            },
             evaluation: self.evaluation.unwrap().finalize(),
-            is_normalizes_to_hack: self.is_normalizes_to_hack,
             returned_goals: self.returned_goals,
         }
     }
@@ -30,6 +35,12 @@ impl<'tcx> WipGoalEvaluation<'tcx> {
 
 #[derive(Eq, PartialEq, Debug)]
 pub enum WipGoalEvaluationKind {
+    Root,
+    Nested { is_normalizes_to_hack: IsNormalizesToHack },
+}
+
+#[derive(Eq, PartialEq, Debug)]
+pub enum WipCanonicalGoalEvaluationKind {
     Overflow,
     CacheHit(CacheHit),
 }
@@ -37,7 +48,7 @@ pub enum WipGoalEvaluationKind {
 #[derive(Eq, PartialEq, Debug)]
 pub struct WipCanonicalGoalEvaluation<'tcx> {
     pub goal: CanonicalInput<'tcx>,
-    pub kind: Option<WipGoalEvaluationKind>,
+    pub kind: Option<WipCanonicalGoalEvaluationKind>,
     pub revisions: Vec<WipGoalEvaluationStep<'tcx>>,
     pub result: Option<QueryResult<'tcx>>,
 }
@@ -45,11 +56,13 @@ pub struct WipCanonicalGoalEvaluation<'tcx> {
 impl<'tcx> WipCanonicalGoalEvaluation<'tcx> {
     pub fn finalize(self) -> inspect::CanonicalGoalEvaluation<'tcx> {
         let kind = match self.kind {
-            Some(WipGoalEvaluationKind::Overflow) => inspect::GoalEvaluationKind::Overflow,
-            Some(WipGoalEvaluationKind::CacheHit(hit)) => {
-                inspect::GoalEvaluationKind::CacheHit(hit)
+            Some(WipCanonicalGoalEvaluationKind::Overflow) => {
+                inspect::CanonicalGoalEvaluationKind::Overflow
             }
-            None => inspect::GoalEvaluationKind::Uncached {
+            Some(WipCanonicalGoalEvaluationKind::CacheHit(hit)) => {
+                inspect::CanonicalGoalEvaluationKind::CacheHit(hit)
+            }
+            None => inspect::CanonicalGoalEvaluationKind::Uncached {
                 revisions: self
                     .revisions
                     .into_iter()
@@ -87,7 +100,7 @@ impl<'tcx> WipAddedGoalsEvaluation<'tcx> {
 pub struct WipGoalEvaluationStep<'tcx> {
     pub instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
 
-    pub evaluation: WipGoalCandidate<'tcx>,
+    pub evaluation: WipProbe<'tcx>,
 }
 
 impl<'tcx> WipGoalEvaluationStep<'tcx> {
@@ -102,26 +115,37 @@ impl<'tcx> WipGoalEvaluationStep<'tcx> {
 }
 
 #[derive(Eq, PartialEq, Debug)]
-pub struct WipGoalCandidate<'tcx> {
-    pub added_goals_evaluations: Vec<WipAddedGoalsEvaluation<'tcx>>,
-    pub candidates: Vec<WipGoalCandidate<'tcx>>,
+pub struct WipProbe<'tcx> {
+    pub steps: Vec<WipProbeStep<'tcx>>,
     pub kind: Option<ProbeKind<'tcx>>,
 }
 
-impl<'tcx> WipGoalCandidate<'tcx> {
-    pub fn finalize(self) -> inspect::GoalCandidate<'tcx> {
-        inspect::GoalCandidate {
-            added_goals_evaluations: self
-                .added_goals_evaluations
-                .into_iter()
-                .map(WipAddedGoalsEvaluation::finalize)
-                .collect(),
-            candidates: self.candidates.into_iter().map(WipGoalCandidate::finalize).collect(),
+impl<'tcx> WipProbe<'tcx> {
+    pub fn finalize(self) -> inspect::Probe<'tcx> {
+        inspect::Probe {
+            steps: self.steps.into_iter().map(WipProbeStep::finalize).collect(),
             kind: self.kind.unwrap(),
         }
     }
 }
 
+#[derive(Eq, PartialEq, Debug)]
+pub enum WipProbeStep<'tcx> {
+    AddGoal(Goal<'tcx, ty::Predicate<'tcx>>),
+    EvaluateGoals(WipAddedGoalsEvaluation<'tcx>),
+    NestedProbe(WipProbe<'tcx>),
+}
+
+impl<'tcx> WipProbeStep<'tcx> {
+    pub fn finalize(self) -> inspect::ProbeStep<'tcx> {
+        match self {
+            WipProbeStep::AddGoal(goal) => inspect::ProbeStep::AddGoal(goal),
+            WipProbeStep::EvaluateGoals(eval) => inspect::ProbeStep::EvaluateGoals(eval.finalize()),
+            WipProbeStep::NestedProbe(probe) => inspect::ProbeStep::NestedProbe(probe.finalize()),
+        }
+    }
+}
+
 #[derive(Debug)]
 pub enum DebugSolver<'tcx> {
     Root,
@@ -129,7 +153,7 @@ pub enum DebugSolver<'tcx> {
     CanonicalGoalEvaluation(WipCanonicalGoalEvaluation<'tcx>),
     AddedGoalsEvaluation(WipAddedGoalsEvaluation<'tcx>),
     GoalEvaluationStep(WipGoalEvaluationStep<'tcx>),
-    GoalCandidate(WipGoalCandidate<'tcx>),
+    Probe(WipProbe<'tcx>),
 }
 
 impl<'tcx> From<WipGoalEvaluation<'tcx>> for DebugSolver<'tcx> {
@@ -156,9 +180,9 @@ impl<'tcx> From<WipGoalEvaluationStep<'tcx>> for DebugSolver<'tcx> {
     }
 }
 
-impl<'tcx> From<WipGoalCandidate<'tcx>> for DebugSolver<'tcx> {
-    fn from(g: WipGoalCandidate<'tcx>) -> DebugSolver<'tcx> {
-        DebugSolver::GoalCandidate(g)
+impl<'tcx> From<WipProbe<'tcx>> for DebugSolver<'tcx> {
+    fn from(p: WipProbe<'tcx>) -> DebugSolver<'tcx> {
+        DebugSolver::Probe(p)
     }
 }
 
@@ -249,15 +273,20 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
         self.state.is_none()
     }
 
-    pub fn new_goal_evaluation(
+    pub(super) fn new_goal_evaluation(
         &mut self,
         goal: Goal<'tcx, ty::Predicate<'tcx>>,
-        is_normalizes_to_hack: IsNormalizesToHack,
+        kind: GoalEvaluationKind,
     ) -> ProofTreeBuilder<'tcx> {
         self.nested(|| WipGoalEvaluation {
             uncanonicalized_goal: goal,
+            kind: match kind {
+                GoalEvaluationKind::Root => WipGoalEvaluationKind::Root,
+                GoalEvaluationKind::Nested { is_normalizes_to_hack } => {
+                    WipGoalEvaluationKind::Nested { is_normalizes_to_hack }
+                }
+            },
             evaluation: None,
-            is_normalizes_to_hack,
             returned_goals: vec![],
         })
     }
@@ -286,7 +315,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
         }
     }
 
-    pub fn goal_evaluation_kind(&mut self, kind: WipGoalEvaluationKind) {
+    pub fn goal_evaluation_kind(&mut self, kind: WipCanonicalGoalEvaluationKind) {
         if let Some(this) = self.as_mut() {
             match this {
                 DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
@@ -329,11 +358,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
     ) -> ProofTreeBuilder<'tcx> {
         self.nested(|| WipGoalEvaluationStep {
             instantiated_goal,
-            evaluation: WipGoalCandidate {
-                added_goals_evaluations: vec![],
-                candidates: vec![],
-                kind: None,
-            },
+            evaluation: WipProbe { steps: vec![], kind: None },
         })
     }
     pub fn goal_evaluation_step(&mut self, goal_evaluation_step: ProofTreeBuilder<'tcx>) {
@@ -350,18 +375,14 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
         }
     }
 
-    pub fn new_goal_candidate(&mut self) -> ProofTreeBuilder<'tcx> {
-        self.nested(|| WipGoalCandidate {
-            added_goals_evaluations: vec![],
-            candidates: vec![],
-            kind: None,
-        })
+    pub fn new_probe(&mut self) -> ProofTreeBuilder<'tcx> {
+        self.nested(|| WipProbe { steps: vec![], kind: None })
     }
 
     pub fn probe_kind(&mut self, probe_kind: ProbeKind<'tcx>) {
         if let Some(this) = self.as_mut() {
             match this {
-                DebugSolver::GoalCandidate(this) => {
+                DebugSolver::Probe(this) => {
                     assert_eq!(this.kind.replace(probe_kind), None)
                 }
                 _ => unreachable!(),
@@ -369,17 +390,32 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
         }
     }
 
-    pub fn goal_candidate(&mut self, candidate: ProofTreeBuilder<'tcx>) {
+    pub fn add_goal(&mut self, goal: Goal<'tcx, ty::Predicate<'tcx>>) {
         if let Some(this) = self.as_mut() {
-            match (this, candidate.state.unwrap().tree) {
+            match this {
+                DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
+                    evaluation: WipProbe { steps, .. },
+                    ..
+                })
+                | DebugSolver::Probe(WipProbe { steps, .. }) => {
+                    steps.push(WipProbeStep::AddGoal(goal))
+                }
+                _ => unreachable!(),
+            }
+        }
+    }
+
+    pub fn finish_probe(&mut self, probe: ProofTreeBuilder<'tcx>) {
+        if let Some(this) = self.as_mut() {
+            match (this, probe.state.unwrap().tree) {
                 (
-                    DebugSolver::GoalCandidate(WipGoalCandidate { candidates, .. })
+                    DebugSolver::Probe(WipProbe { steps, .. })
                     | DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
-                        evaluation: WipGoalCandidate { candidates, .. },
+                        evaluation: WipProbe { steps, .. },
                         ..
                     }),
-                    DebugSolver::GoalCandidate(candidate),
-                ) => candidates.push(candidate),
+                    DebugSolver::Probe(probe),
+                ) => steps.push(WipProbeStep::NestedProbe(probe)),
                 _ => unreachable!(),
             }
         }
@@ -416,14 +452,12 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
             match (this, added_goals_evaluation.state.unwrap().tree) {
                 (
                     DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
-                        evaluation: WipGoalCandidate { added_goals_evaluations, .. },
+                        evaluation: WipProbe { steps, .. },
                         ..
                     })
-                    | DebugSolver::GoalCandidate(WipGoalCandidate {
-                        added_goals_evaluations, ..
-                    }),
+                    | DebugSolver::Probe(WipProbe { steps, .. }),
                     DebugSolver::AddedGoalsEvaluation(added_goals_evaluation),
-                ) => added_goals_evaluations.push(added_goals_evaluation),
+                ) => steps.push(WipProbeStep::EvaluateGoals(added_goals_evaluation)),
                 _ => unreachable!(),
             }
         }
diff --git a/compiler/rustc_trait_selection/src/solve/mod.rs b/compiler/rustc_trait_selection/src/solve/mod.rs
index c492408bc76..bd612ce4778 100644
--- a/compiler/rustc_trait_selection/src/solve/mod.rs
+++ b/compiler/rustc_trait_selection/src/solve/mod.rs
@@ -19,7 +19,8 @@ use rustc_infer::infer::canonical::{Canonical, CanonicalVarValues};
 use rustc_infer::traits::query::NoSolution;
 use rustc_middle::infer::canonical::CanonicalVarInfos;
 use rustc_middle::traits::solve::{
-    CanonicalResponse, Certainty, ExternalConstraintsData, Goal, QueryResult, Response,
+    CanonicalResponse, Certainty, ExternalConstraintsData, Goal, IsNormalizesToHack, QueryResult,
+    Response,
 };
 use rustc_middle::ty::{self, Ty, TyCtxt, UniverseIndex};
 use rustc_middle::ty::{
@@ -59,6 +60,12 @@ enum SolverMode {
     Coherence,
 }
 
+#[derive(Debug, Copy, Clone, PartialEq, Eq)]
+enum GoalEvaluationKind {
+    Root,
+    Nested { is_normalizes_to_hack: IsNormalizesToHack },
+}
+
 trait CanonicalResponseExt {
     fn has_no_inference_or_external_constraints(&self) -> bool;
 
@@ -228,6 +235,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
 
     #[instrument(level = "debug", skip(self))]
     fn add_goal(&mut self, goal: Goal<'tcx, ty::Predicate<'tcx>>) {
+        self.inspect.add_goal(goal);
         self.nested_goals.goals.push(goal);
     }
 
diff --git a/compiler/rustc_trait_selection/src/solve/search_graph/mod.rs b/compiler/rustc_trait_selection/src/solve/search_graph/mod.rs
index c816b51f67a..16de518e8e0 100644
--- a/compiler/rustc_trait_selection/src/solve/search_graph/mod.rs
+++ b/compiler/rustc_trait_selection/src/solve/search_graph/mod.rs
@@ -187,7 +187,7 @@ impl<'tcx> SearchGraph<'tcx> {
                 last.encountered_overflow = true;
             }
 
-            inspect.goal_evaluation_kind(inspect::WipGoalEvaluationKind::Overflow);
+            inspect.goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::Overflow);
             return Self::response_no_constraints(tcx, input, Certainty::OVERFLOW);
         };
 
@@ -203,7 +203,7 @@ impl<'tcx> SearchGraph<'tcx> {
                     available_depth,
                 )
             {
-                inspect.goal_evaluation_kind(inspect::WipGoalEvaluationKind::CacheHit(
+                inspect.goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::CacheHit(
                     CacheHit::Global,
                 ));
                 self.on_cache_hit(reached_depth, encountered_overflow);
@@ -240,7 +240,7 @@ impl<'tcx> SearchGraph<'tcx> {
             // Finally we can return either the provisional response for that goal if we have a
             // coinductive cycle or an ambiguous result if the cycle is inductive.
             Entry::Occupied(entry_index) => {
-                inspect.goal_evaluation_kind(inspect::WipGoalEvaluationKind::CacheHit(
+                inspect.goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::CacheHit(
                     CacheHit::Provisional,
                 ));