remove proof tree formatter, make em shallow

16 files changed, 135 insertions, 505 deletions

diff --git a/compiler/rustc_interface/src/tests.rs b/compiler/rustc_interface/src/tests.rs
index 36f9dda7250..c6cf7cf4f3f 100644
--- a/compiler/rustc_interface/src/tests.rs
+++ b/compiler/rustc_interface/src/tests.rs
@@ -799,10 +799,7 @@ fn test_unstable_options_tracking_hash() {
     tracked!(mir_opt_level, Some(4));
     tracked!(move_size_limit, Some(4096));
     tracked!(mutable_noalias, false);
-    tracked!(
-        next_solver,
-        Some(NextSolverConfig { coherence: true, globally: false, dump_tree: Default::default() })
-    );
+    tracked!(next_solver, Some(NextSolverConfig { coherence: true, globally: false }));
     tracked!(no_generate_arange_section, true);
     tracked!(no_jump_tables, true);
     tracked!(no_link, true);
diff --git a/compiler/rustc_middle/src/arena.rs b/compiler/rustc_middle/src/arena.rs
index 7392eb6c2bb..b0e72eaf5a4 100644
--- a/compiler/rustc_middle/src/arena.rs
+++ b/compiler/rustc_middle/src/arena.rs
@@ -61,7 +61,10 @@ macro_rules! arena_types {
             [] dtorck_constraint: rustc_middle::traits::query::DropckConstraint<'tcx>,
             [] candidate_step: rustc_middle::traits::query::CandidateStep<'tcx>,
             [] autoderef_bad_ty: rustc_middle::traits::query::MethodAutoderefBadTy<'tcx>,
-            [] canonical_goal_evaluation: rustc_next_trait_solver::solve::inspect::GoalEvaluationStep<rustc_middle::ty::TyCtxt<'tcx>>,
+            [] canonical_goal_evaluation:
+                rustc_next_trait_solver::solve::inspect::CanonicalGoalEvaluationStep<
+                    rustc_middle::ty::TyCtxt<'tcx>
+                >,
             [] query_region_constraints: rustc_middle::infer::canonical::QueryRegionConstraints<'tcx>,
             [] type_op_subtype:
                 rustc_middle::infer::canonical::Canonical<'tcx,
diff --git a/compiler/rustc_middle/src/traits/solve/cache.rs b/compiler/rustc_middle/src/traits/solve/cache.rs
index 2ff4ade21d0..dc31114b2c4 100644
--- a/compiler/rustc_middle/src/traits/solve/cache.rs
+++ b/compiler/rustc_middle/src/traits/solve/cache.rs
@@ -17,7 +17,7 @@ pub struct EvaluationCache<'tcx> {
 #[derive(Debug, PartialEq, Eq)]
 pub struct CacheData<'tcx> {
     pub result: QueryResult<'tcx>,
-    pub proof_tree: Option<&'tcx [inspect::GoalEvaluationStep<TyCtxt<'tcx>>]>,
+    pub proof_tree: Option<&'tcx inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>>,
     pub additional_depth: usize,
     pub encountered_overflow: bool,
 }
@@ -28,7 +28,7 @@ impl<'tcx> EvaluationCache<'tcx> {
         &self,
         tcx: TyCtxt<'tcx>,
         key: CanonicalInput<'tcx>,
-        proof_tree: Option<&'tcx [inspect::GoalEvaluationStep<TyCtxt<'tcx>>]>,
+        proof_tree: Option<&'tcx inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>>,
         additional_depth: usize,
         encountered_overflow: bool,
         cycle_participants: FxHashSet<CanonicalInput<'tcx>>,
@@ -107,7 +107,7 @@ struct Success<'tcx> {
 #[derive(Clone, Copy)]
 pub struct QueryData<'tcx> {
     pub result: QueryResult<'tcx>,
-    pub proof_tree: Option<&'tcx [inspect::GoalEvaluationStep<TyCtxt<'tcx>>]>,
+    pub proof_tree: Option<&'tcx inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>>,
 }
 
 /// The cache entry for a goal `CanonicalInput`.
diff --git a/compiler/rustc_middle/src/ty/context.rs b/compiler/rustc_middle/src/ty/context.rs
index 6e53b5bb520..d138cd9ceb9 100644
--- a/compiler/rustc_middle/src/ty/context.rs
+++ b/compiler/rustc_middle/src/ty/context.rs
@@ -103,7 +103,8 @@ impl<'tcx> Interner for TyCtxt<'tcx> {
     type PredefinedOpaques = solve::PredefinedOpaques<'tcx>;
     type DefiningOpaqueTypes = &'tcx ty::List<LocalDefId>;
     type ExternalConstraints = ExternalConstraints<'tcx>;
-    type GoalEvaluationSteps = &'tcx [solve::inspect::GoalEvaluationStep<TyCtxt<'tcx>>];
+    type CanonicalGoalEvaluationStepRef =
+        &'tcx solve::inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>;
 
     type Ty = Ty<'tcx>;
     type Tys = &'tcx List<Ty<'tcx>>;
diff --git a/compiler/rustc_session/src/config.rs b/compiler/rustc_session/src/config.rs
index 5ac4d194e87..c90da966e70 100644
--- a/compiler/rustc_session/src/config.rs
+++ b/compiler/rustc_session/src/config.rs
@@ -796,16 +796,6 @@ pub struct NextSolverConfig {
     /// Whether the new trait solver should be enabled everywhere.
     /// This is only `true` if `coherence` is also enabled.
     pub globally: bool,
-    /// Whether to dump proof trees after computing a proof tree.
-    pub dump_tree: DumpSolverProofTree,
-}
-
-#[derive(Default, Debug, Copy, Clone, Hash, PartialEq, Eq)]
-pub enum DumpSolverProofTree {
-    Always,
-    OnError,
-    #[default]
-    Never,
 }
 
 #[derive(Clone)]
diff --git a/compiler/rustc_session/src/options.rs b/compiler/rustc_session/src/options.rs
index 65660286dd7..6309fcdd2db 100644
--- a/compiler/rustc_session/src/options.rs
+++ b/compiler/rustc_session/src/options.rs
@@ -399,7 +399,8 @@ mod desc {
     pub const parse_instrument_xray: &str = "either a boolean (`yes`, `no`, `on`, `off`, etc), or a comma separated list of settings: `always` or `never` (mutually exclusive), `ignore-loops`, `instruction-threshold=N`, `skip-entry`, `skip-exit`";
     pub const parse_unpretty: &str = "`string` or `string=string`";
     pub const parse_treat_err_as_bug: &str = "either no value or a non-negative number";
-    pub const parse_next_solver_config: &str = "a comma separated list of solver configurations: `globally` (default), `coherence`, `dump-tree`, `dump-tree-on-error";
+    pub const parse_next_solver_config: &str =
+        "a comma separated list of solver configurations: `globally` (default), and `coherence`";
     pub const parse_lto: &str =
         "either a boolean (`yes`, `no`, `on`, `off`, etc), `thin`, `fat`, or omitted";
     pub const parse_linker_plugin_lto: &str =
@@ -1058,7 +1059,6 @@ mod parse {
         if let Some(config) = v {
             let mut coherence = false;
             let mut globally = true;
-            let mut dump_tree = None;
             for c in config.split(',') {
                 match c {
                     "globally" => globally = true,
@@ -1066,31 +1066,13 @@ mod parse {
                         globally = false;
                         coherence = true;
                     }
-                    "dump-tree" => {
-                        if dump_tree.replace(DumpSolverProofTree::Always).is_some() {
-                            return false;
-                        }
-                    }
-                    "dump-tree-on-error" => {
-                        if dump_tree.replace(DumpSolverProofTree::OnError).is_some() {
-                            return false;
-                        }
-                    }
                     _ => return false,
                 }
             }
 
-            *slot = Some(NextSolverConfig {
-                coherence: coherence || globally,
-                globally,
-                dump_tree: dump_tree.unwrap_or_default(),
-            });
+            *slot = Some(NextSolverConfig { coherence: coherence || globally, globally });
         } else {
-            *slot = Some(NextSolverConfig {
-                coherence: true,
-                globally: true,
-                dump_tree: Default::default(),
-            });
+            *slot = Some(NextSolverConfig { coherence: true, globally: true });
         }
 
         true
diff --git a/compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs b/compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs
index 7e1d7d73e0b..ce408ddea37 100644
--- a/compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs
+++ b/compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs
@@ -1,6 +1,3 @@
-use std::io::Write;
-use std::ops::ControlFlow;
-
 use rustc_data_structures::stack::ensure_sufficient_stack;
 use rustc_hir::def_id::DefId;
 use rustc_infer::infer::at::ToTrace;
@@ -20,10 +17,10 @@ use rustc_middle::ty::{
     self, InferCtxtLike, OpaqueTypeKey, Ty, TyCtxt, TypeFoldable, TypeSuperVisitable,
     TypeVisitable, TypeVisitableExt, TypeVisitor,
 };
-use rustc_session::config::DumpSolverProofTree;
 use rustc_span::DUMMY_SP;
 use rustc_type_ir::{self as ir, CanonicalVarValues, Interner};
 use rustc_type_ir_macros::{Lift_Generic, TypeFoldable_Generic, TypeVisitable_Generic};
+use std::ops::ControlFlow;
 
 use crate::traits::coherence;
 use crate::traits::vtable::{count_own_vtable_entries, prepare_vtable_segments, VtblSegment};
@@ -135,8 +132,7 @@ impl<I: Interner> NestedGoals<I> {
 #[derive(PartialEq, Eq, Debug, Hash, HashStable, Clone, Copy)]
 pub enum GenerateProofTree {
     Yes,
-    IfEnabled,
-    Never,
+    No,
 }
 
 #[extension(pub trait InferCtxtEvalExt<'tcx>)]
@@ -182,7 +178,7 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
             infcx,
             search_graph: &mut search_graph,
             nested_goals: NestedGoals::new(),
-            inspect: ProofTreeBuilder::new_maybe_root(infcx.tcx, generate_proof_tree),
+            inspect: ProofTreeBuilder::new_maybe_root(generate_proof_tree),
 
             // Only relevant when canonicalizing the response,
             // which we don't do within this evaluation context.
@@ -197,23 +193,14 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
         };
         let result = f(&mut ecx);
 
-        let tree = ecx.inspect.finalize();
-        if let (Some(tree), DumpSolverProofTree::Always) = (
-            &tree,
-            infcx.tcx.sess.opts.unstable_opts.next_solver.map(|c| c.dump_tree).unwrap_or_default(),
-        ) {
-            let mut lock = std::io::stdout().lock();
-            let _ = lock.write_fmt(format_args!("{tree:?}\n"));
-            let _ = lock.flush();
-        }
-
+        let proof_tree = ecx.inspect.finalize();
         assert!(
             ecx.nested_goals.is_empty(),
             "root `EvalCtxt` should not have any goals added to it"
         );
 
         assert!(search_graph.is_empty());
-        (result, tree)
+        (result, proof_tree)
     }
 
     /// Creates a nested evaluation context that shares the same search graph as the
@@ -483,7 +470,6 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
     // the certainty of all the goals.
     #[instrument(level = "trace", skip(self))]
     pub(super) fn try_evaluate_added_goals(&mut self) -> Result<Certainty, NoSolution> {
-        self.inspect.start_evaluate_added_goals();
         let mut response = Ok(Certainty::overflow(false));
         for _ in 0..FIXPOINT_STEP_LIMIT {
             // FIXME: This match is a bit ugly, it might be nice to change the inspect
@@ -501,8 +487,6 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
             }
         }
 
-        self.inspect.evaluate_added_goals_result(response);
-
         if response.is_err() {
             self.tainted = Err(NoSolution);
         }
@@ -515,7 +499,6 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
     /// Goals for the next step get directly added to the nested goals of the `EvalCtxt`.
     fn evaluate_added_goals_step(&mut self) -> Result<Option<Certainty>, NoSolution> {
         let tcx = self.tcx();
-        self.inspect.start_evaluate_added_goals_step();
         let mut goals = core::mem::take(&mut self.nested_goals);
 
         // If this loop did not result in any progress, what's our final certainty.
diff --git a/compiler/rustc_trait_selection/src/solve/fulfill.rs b/compiler/rustc_trait_selection/src/solve/fulfill.rs
index 7291eb00e72..d28cf834032 100644
--- a/compiler/rustc_trait_selection/src/solve/fulfill.rs
+++ b/compiler/rustc_trait_selection/src/solve/fulfill.rs
@@ -79,7 +79,7 @@ impl<'tcx> ObligationStorage<'tcx> {
             // change.
             self.overflowed.extend(self.pending.extract_if(|o| {
                 let goal = o.clone().into();
-                let result = infcx.evaluate_root_goal(goal, GenerateProofTree::Never).0;
+                let result = infcx.evaluate_root_goal(goal, GenerateProofTree::No).0;
                 match result {
                     Ok((has_changed, _)) => has_changed,
                     _ => false,
@@ -159,7 +159,7 @@ impl<'tcx> TraitEngine<'tcx> for FulfillmentCtxt<'tcx> {
             let mut has_changed = false;
             for obligation in self.obligations.unstalled_for_select() {
                 let goal = obligation.clone().into();
-                let result = infcx.evaluate_root_goal(goal, GenerateProofTree::IfEnabled).0;
+                let result = infcx.evaluate_root_goal(goal, GenerateProofTree::No).0;
                 self.inspect_evaluated_obligation(infcx, &obligation, &result);
                 let (changed, certainty) = match result {
                     Ok(result) => result,
@@ -246,7 +246,7 @@ fn fulfillment_error_for_stalled<'tcx>(
     root_obligation: PredicateObligation<'tcx>,
 ) -> FulfillmentError<'tcx> {
     let (code, refine_obligation) = infcx.probe(|_| {
-        match infcx.evaluate_root_goal(root_obligation.clone().into(), GenerateProofTree::Never).0 {
+        match infcx.evaluate_root_goal(root_obligation.clone().into(), GenerateProofTree::No).0 {
             Ok((_, Certainty::Maybe(MaybeCause::Ambiguity))) => {
                 (FulfillmentErrorCode::Ambiguity { overflow: None }, true)
             }
diff --git a/compiler/rustc_trait_selection/src/solve/inspect/analyse.rs b/compiler/rustc_trait_selection/src/solve/inspect/analyse.rs
index 737d03f73f0..447357f8b3f 100644
--- a/compiler/rustc_trait_selection/src/solve/inspect/analyse.rs
+++ b/compiler/rustc_trait_selection/src/solve/inspect/analyse.rs
@@ -317,7 +317,6 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
                 inspect::ProbeStep::RecordImplArgs { impl_args: i } => {
                     assert_eq!(impl_args.replace(i), None);
                 }
-                inspect::ProbeStep::EvaluateGoals(_) => (),
             }
         }
 
@@ -359,13 +358,7 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
                 warn!("unexpected root evaluation: {:?}", self.evaluation_kind);
                 return vec![];
             }
-            inspect::CanonicalGoalEvaluationKind::Evaluation { revisions } => {
-                if let Some(last) = revisions.last() {
-                    last
-                } else {
-                    return vec![];
-                }
-            }
+            inspect::CanonicalGoalEvaluationKind::Evaluation { final_revision } => final_revision,
         };
 
         let mut nested_goals = vec![];
@@ -392,9 +385,7 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
         normalizes_to_term_hack: Option<NormalizesToTermHack<'tcx>>,
         source: GoalSource,
     ) -> Self {
-        let inspect::GoalEvaluation { uncanonicalized_goal, kind, evaluation } = root;
-        let inspect::GoalEvaluationKind::Root { orig_values } = kind else { unreachable!() };
-
+        let inspect::GoalEvaluation { uncanonicalized_goal, orig_values, evaluation } = root;
         let result = evaluation.result.and_then(|ok| {
             if let Some(term_hack) = normalizes_to_term_hack {
                 infcx
diff --git a/compiler/rustc_trait_selection/src/solve/inspect/build.rs b/compiler/rustc_trait_selection/src/solve/inspect/build.rs
index 803300c5196..3c633362648 100644
--- a/compiler/rustc_trait_selection/src/solve/inspect/build.rs
+++ b/compiler/rustc_trait_selection/src/solve/inspect/build.rs
@@ -5,20 +5,17 @@
 //! see the comment on [ProofTreeBuilder].
 use std::mem;
 
+use crate::solve::eval_ctxt::canonical;
+use crate::solve::{self, inspect, GenerateProofTree};
 use rustc_infer::infer::InferCtxt;
 use rustc_middle::bug;
 use rustc_middle::infer::canonical::CanonicalVarValues;
-use rustc_middle::traits::query::NoSolution;
 use rustc_middle::ty::{self, TyCtxt};
 use rustc_next_trait_solver::solve::{
     CanonicalInput, Certainty, Goal, GoalSource, QueryInput, QueryResult,
 };
-use rustc_session::config::DumpSolverProofTree;
 use rustc_type_ir::Interner;
 
-use crate::solve::eval_ctxt::canonical;
-use crate::solve::{self, inspect, GenerateProofTree};
-
 /// The core data structure when building proof trees.
 ///
 /// In case the current evaluation does not generate a proof
@@ -53,7 +50,7 @@ enum DebugSolver<I: Interner> {
     Root,
     GoalEvaluation(WipGoalEvaluation<I>),
     CanonicalGoalEvaluation(WipCanonicalGoalEvaluation<I>),
-    GoalEvaluationStep(WipGoalEvaluationStep<I>),
+    CanonicalGoalEvaluationStep(WipCanonicalGoalEvaluationStep<I>),
 }
 
 impl<I: Interner> From<WipGoalEvaluation<I>> for DebugSolver<I> {
@@ -68,9 +65,9 @@ impl<I: Interner> From<WipCanonicalGoalEvaluation<I>> for DebugSolver<I> {
     }
 }
 
-impl<I: Interner> From<WipGoalEvaluationStep<I>> for DebugSolver<I> {
-    fn from(g: WipGoalEvaluationStep<I>) -> DebugSolver<I> {
-        DebugSolver::GoalEvaluationStep(g)
+impl<I: Interner> From<WipCanonicalGoalEvaluationStep<I>> for DebugSolver<I> {
+    fn from(g: WipCanonicalGoalEvaluationStep<I>) -> DebugSolver<I> {
+        DebugSolver::CanonicalGoalEvaluationStep(g)
     }
 }
 
@@ -78,7 +75,7 @@ impl<I: Interner> From<WipGoalEvaluationStep<I>> for DebugSolver<I> {
 #[derivative(PartialEq(bound = ""), Eq(bound = ""), Debug(bound = ""))]
 struct WipGoalEvaluation<I: Interner> {
     pub uncanonicalized_goal: Goal<I, I::Predicate>,
-    pub kind: WipGoalEvaluationKind<I>,
+    pub orig_values: Vec<I::GenericArg>,
     pub evaluation: Option<WipCanonicalGoalEvaluation<I>>,
 }
 
@@ -86,31 +83,19 @@ impl<I: Interner> WipGoalEvaluation<I> {
     fn finalize(self) -> inspect::GoalEvaluation<I> {
         inspect::GoalEvaluation {
             uncanonicalized_goal: self.uncanonicalized_goal,
-            kind: match self.kind {
-                WipGoalEvaluationKind::Root { orig_values } => {
-                    inspect::GoalEvaluationKind::Root { orig_values }
-                }
-                WipGoalEvaluationKind::Nested => inspect::GoalEvaluationKind::Nested,
-            },
+            orig_values: self.orig_values,
             evaluation: self.evaluation.unwrap().finalize(),
         }
     }
 }
 
 #[derive(derivative::Derivative)]
-#[derivative(PartialEq(bound = ""), Eq(bound = ""), Debug(bound = ""))]
-pub(in crate::solve) enum WipGoalEvaluationKind<I: Interner> {
-    Root { orig_values: Vec<I::GenericArg> },
-    Nested,
-}
-
-#[derive(derivative::Derivative)]
 #[derivative(PartialEq(bound = ""), Eq(bound = ""))]
 pub(in crate::solve) enum WipCanonicalGoalEvaluationKind<I: Interner> {
     Overflow,
     CycleInStack,
     ProvisionalCacheHit,
-    Interned { revisions: I::GoalEvaluationSteps },
+    Interned { final_revision: I::CanonicalGoalEvaluationStepRef },
 }
 
 impl<I: Interner> std::fmt::Debug for WipCanonicalGoalEvaluationKind<I> {
@@ -119,7 +104,9 @@ impl<I: Interner> std::fmt::Debug for WipCanonicalGoalEvaluationKind<I> {
             Self::Overflow => write!(f, "Overflow"),
             Self::CycleInStack => write!(f, "CycleInStack"),
             Self::ProvisionalCacheHit => write!(f, "ProvisionalCacheHit"),
-            Self::Interned { revisions: _ } => f.debug_struct("Interned").finish_non_exhaustive(),
+            Self::Interned { final_revision: _ } => {
+                f.debug_struct("Interned").finish_non_exhaustive()
+            }
         }
     }
 }
@@ -131,13 +118,15 @@ struct WipCanonicalGoalEvaluation<I: Interner> {
     kind: Option<WipCanonicalGoalEvaluationKind<I>>,
     /// Only used for uncached goals. After we finished evaluating
     /// the goal, this is interned and moved into `kind`.
-    revisions: Vec<WipGoalEvaluationStep<I>>,
+    final_revision: Option<WipCanonicalGoalEvaluationStep<I>>,
     result: Option<QueryResult<I>>,
 }
 
 impl<I: Interner> WipCanonicalGoalEvaluation<I> {
     fn finalize(self) -> inspect::CanonicalGoalEvaluation<I> {
-        assert!(self.revisions.is_empty());
+        // We've already interned the final revision in
+        // `fn finalize_canonical_goal_evaluation`.
+        assert!(self.final_revision.is_none());
         let kind = match self.kind.unwrap() {
             WipCanonicalGoalEvaluationKind::Overflow => {
                 inspect::CanonicalGoalEvaluationKind::Overflow
@@ -148,8 +137,8 @@ impl<I: Interner> WipCanonicalGoalEvaluation<I> {
             WipCanonicalGoalEvaluationKind::ProvisionalCacheHit => {
                 inspect::CanonicalGoalEvaluationKind::ProvisionalCacheHit
             }
-            WipCanonicalGoalEvaluationKind::Interned { revisions } => {
-                inspect::CanonicalGoalEvaluationKind::Evaluation { revisions }
+            WipCanonicalGoalEvaluationKind::Interned { final_revision } => {
+                inspect::CanonicalGoalEvaluationKind::Evaluation { final_revision }
             }
         };
 
@@ -159,29 +148,7 @@ impl<I: Interner> WipCanonicalGoalEvaluation<I> {
 
 #[derive(derivative::Derivative)]
 #[derivative(PartialEq(bound = ""), Eq(bound = ""), Debug(bound = ""))]
-struct WipAddedGoalsEvaluation<I: Interner> {
-    evaluations: Vec<Vec<WipGoalEvaluation<I>>>,
-    result: Option<Result<Certainty, NoSolution>>,
-}
-
-impl<I: Interner> WipAddedGoalsEvaluation<I> {
-    fn finalize(self) -> inspect::AddedGoalsEvaluation<I> {
-        inspect::AddedGoalsEvaluation {
-            evaluations: self
-                .evaluations
-                .into_iter()
-                .map(|evaluations| {
-                    evaluations.into_iter().map(WipGoalEvaluation::finalize).collect()
-                })
-                .collect(),
-            result: self.result.unwrap(),
-        }
-    }
-}
-
-#[derive(derivative::Derivative)]
-#[derivative(PartialEq(bound = ""), Eq(bound = ""), Debug(bound = ""))]
-struct WipGoalEvaluationStep<I: Interner> {
+struct WipCanonicalGoalEvaluationStep<I: Interner> {
     /// Unlike `EvalCtxt::var_values`, we append a new
     /// generic arg here whenever we create a new inference
     /// variable.
@@ -194,7 +161,7 @@ struct WipGoalEvaluationStep<I: Interner> {
     evaluation: WipProbe<I>,
 }
 
-impl<I: Interner> WipGoalEvaluationStep<I> {
+impl<I: Interner> WipCanonicalGoalEvaluationStep<I> {
     fn current_evaluation_scope(&mut self) -> &mut WipProbe<I> {
         let mut current = &mut self.evaluation;
         for _ in 0..self.probe_depth {
@@ -206,24 +173,16 @@ impl<I: Interner> WipGoalEvaluationStep<I> {
         current
     }
 
-    fn added_goals_evaluation(&mut self) -> &mut WipAddedGoalsEvaluation<I> {
-        let mut current = &mut self.evaluation;
-        loop {
-            match current.steps.last_mut() {
-                Some(WipProbeStep::NestedProbe(p)) => current = p,
-                Some(WipProbeStep::EvaluateGoals(evaluation)) => return evaluation,
-                _ => bug!(),
-            }
-        }
-    }
-
-    fn finalize(self) -> inspect::GoalEvaluationStep<I> {
+    fn finalize(self) -> inspect::CanonicalGoalEvaluationStep<I> {
         let evaluation = self.evaluation.finalize();
         match evaluation.kind {
             inspect::ProbeKind::Root { .. } => (),
             _ => unreachable!("unexpected root evaluation: {evaluation:?}"),
         }
-        inspect::GoalEvaluationStep { instantiated_goal: self.instantiated_goal, evaluation }
+        inspect::CanonicalGoalEvaluationStep {
+            instantiated_goal: self.instantiated_goal,
+            evaluation,
+        }
     }
 }
 
@@ -250,7 +209,6 @@ impl<I: Interner> WipProbe<I> {
 #[derivative(PartialEq(bound = ""), Eq(bound = ""), Debug(bound = ""))]
 enum WipProbeStep<I: Interner> {
     AddGoal(GoalSource, inspect::CanonicalState<I, Goal<I, I::Predicate>>),
-    EvaluateGoals(WipAddedGoalsEvaluation<I>),
     NestedProbe(WipProbe<I>),
     MakeCanonicalResponse { shallow_certainty: Certainty },
     RecordImplArgs { impl_args: inspect::CanonicalState<I, I::GenericArgs> },
@@ -260,7 +218,6 @@ impl<I: Interner> WipProbeStep<I> {
     fn finalize(self) -> inspect::ProbeStep<I> {
         match self {
             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::RecordImplArgs { impl_args } => {
                 inspect::ProbeStep::RecordImplArgs { impl_args }
@@ -278,6 +235,15 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
         ProofTreeBuilder { state: Some(Box::new(state.into())) }
     }
 
+    fn opt_nested<T: Into<DebugSolver<TyCtxt<'tcx>>>>(
+        &self,
+        state: impl FnOnce() -> Option<T>,
+    ) -> Self {
+        ProofTreeBuilder {
+            state: self.state.as_ref().and_then(|_| Some(state()?.into())).map(Box::new),
+        }
+    }
+
     fn nested<T: Into<DebugSolver<TyCtxt<'tcx>>>>(&self, state: impl FnOnce() -> T) -> Self {
         ProofTreeBuilder { state: self.state.as_ref().map(|_| Box::new(state().into())) }
     }
@@ -302,22 +268,10 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
     }
 
     pub fn new_maybe_root(
-        tcx: TyCtxt<'tcx>,
         generate_proof_tree: GenerateProofTree,
     ) -> ProofTreeBuilder<TyCtxt<'tcx>> {
         match generate_proof_tree {
-            GenerateProofTree::Never => ProofTreeBuilder::new_noop(),
-            GenerateProofTree::IfEnabled => {
-                let opts = &tcx.sess.opts.unstable_opts;
-                match opts.next_solver.map(|c| c.dump_tree).unwrap_or_default() {
-                    DumpSolverProofTree::Always => ProofTreeBuilder::new_root(),
-                    // `OnError` is handled by reevaluating goals in error
-                    // reporting with `GenerateProofTree::Yes`.
-                    DumpSolverProofTree::OnError | DumpSolverProofTree::Never => {
-                        ProofTreeBuilder::new_noop()
-                    }
-                }
-            }
+            GenerateProofTree::No => ProofTreeBuilder::new_noop(),
             GenerateProofTree::Yes => ProofTreeBuilder::new_root(),
         }
     }
@@ -340,15 +294,13 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
         orig_values: &[ty::GenericArg<'tcx>],
         kind: solve::GoalEvaluationKind,
     ) -> ProofTreeBuilder<TyCtxt<'tcx>> {
-        self.nested(|| WipGoalEvaluation {
-            uncanonicalized_goal: goal,
-            kind: match kind {
-                solve::GoalEvaluationKind::Root => {
-                    WipGoalEvaluationKind::Root { orig_values: orig_values.to_vec() }
-                }
-                solve::GoalEvaluationKind::Nested => WipGoalEvaluationKind::Nested,
-            },
-            evaluation: None,
+        self.opt_nested(|| match kind {
+            solve::GoalEvaluationKind::Root => Some(WipGoalEvaluation {
+                uncanonicalized_goal: goal,
+                orig_values: orig_values.to_vec(),
+                evaluation: None,
+            }),
+            solve::GoalEvaluationKind::Nested => None,
         })
     }
 
@@ -359,24 +311,22 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
         self.nested(|| WipCanonicalGoalEvaluation {
             goal,
             kind: None,
-            revisions: vec![],
+            final_revision: None,
             result: None,
         })
     }
 
-    pub fn finalize_evaluation(
+    pub fn finalize_canonical_goal_evaluation(
         &mut self,
         tcx: TyCtxt<'tcx>,
-    ) -> Option<&'tcx [inspect::GoalEvaluationStep<TyCtxt<'tcx>>]> {
+    ) -> Option<&'tcx inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>> {
         self.as_mut().map(|this| match this {
             DebugSolver::CanonicalGoalEvaluation(evaluation) => {
-                let revisions = mem::take(&mut evaluation.revisions)
-                    .into_iter()
-                    .map(WipGoalEvaluationStep::finalize);
-                let revisions = &*tcx.arena.alloc_from_iter(revisions);
-                let kind = WipCanonicalGoalEvaluationKind::Interned { revisions };
+                let final_revision = mem::take(&mut evaluation.final_revision).unwrap();
+                let final_revision = &*tcx.arena.alloc(final_revision.finalize());
+                let kind = WipCanonicalGoalEvaluationKind::Interned { final_revision };
                 assert_eq!(evaluation.kind.replace(kind), None);
-                revisions
+                final_revision
             }
             _ => unreachable!(),
         })
@@ -400,7 +350,10 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
         }
     }
 
-    pub fn goal_evaluation_kind(&mut self, kind: WipCanonicalGoalEvaluationKind<TyCtxt<'tcx>>) {
+    pub fn canonical_goal_evaluation_kind(
+        &mut self,
+        kind: WipCanonicalGoalEvaluationKind<TyCtxt<'tcx>>,
+    ) {
         if let Some(this) = self.as_mut() {
             match this {
                 DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
@@ -413,17 +366,11 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
 
     pub fn goal_evaluation(&mut self, goal_evaluation: ProofTreeBuilder<TyCtxt<'tcx>>) {
         if let Some(this) = self.as_mut() {
-            match (this, *goal_evaluation.state.unwrap()) {
-                (
-                    DebugSolver::GoalEvaluationStep(state),
-                    DebugSolver::GoalEvaluation(goal_evaluation),
-                ) => state
-                    .added_goals_evaluation()
-                    .evaluations
-                    .last_mut()
-                    .unwrap()
-                    .push(goal_evaluation),
-                (this @ DebugSolver::Root, goal_evaluation) => *this = goal_evaluation,
+            match this {
+                DebugSolver::Root => *this = *goal_evaluation.state.unwrap(),
+                DebugSolver::CanonicalGoalEvaluationStep(_) => {
+                    assert!(goal_evaluation.state.is_none())
+                }
                 _ => unreachable!(),
             }
         }
@@ -434,7 +381,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
         var_values: CanonicalVarValues<'tcx>,
         instantiated_goal: QueryInput<TyCtxt<'tcx>, ty::Predicate<'tcx>>,
     ) -> ProofTreeBuilder<TyCtxt<'tcx>> {
-        self.nested(|| WipGoalEvaluationStep {
+        self.nested(|| WipCanonicalGoalEvaluationStep {
             var_values: var_values.var_values.to_vec(),
             instantiated_goal,
             evaluation: WipProbe {
@@ -452,9 +399,9 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
             match (this, *goal_evaluation_step.state.unwrap()) {
                 (
                     DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluations),
-                    DebugSolver::GoalEvaluationStep(goal_evaluation_step),
+                    DebugSolver::CanonicalGoalEvaluationStep(goal_evaluation_step),
                 ) => {
-                    canonical_goal_evaluations.revisions.push(goal_evaluation_step);
+                    canonical_goal_evaluations.final_revision = Some(goal_evaluation_step);
                 }
                 _ => unreachable!(),
             }
@@ -464,7 +411,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
     pub fn add_var_value<T: Into<ty::GenericArg<'tcx>>>(&mut self, arg: T) {
         match self.as_mut() {
             None => {}
-            Some(DebugSolver::GoalEvaluationStep(state)) => {
+            Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
                 state.var_values.push(arg.into());
             }
             Some(s) => bug!("tried to add var values to {s:?}"),
@@ -474,7 +421,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
     pub fn enter_probe(&mut self) {
         match self.as_mut() {
             None => {}
-            Some(DebugSolver::GoalEvaluationStep(state)) => {
+            Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
                 let initial_num_var_values = state.var_values.len();
                 state.current_evaluation_scope().steps.push(WipProbeStep::NestedProbe(WipProbe {
                     initial_num_var_values,
@@ -491,7 +438,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
     pub fn probe_kind(&mut self, probe_kind: inspect::ProbeKind<TyCtxt<'tcx>>) {
         match self.as_mut() {
             None => {}
-            Some(DebugSolver::GoalEvaluationStep(state)) => {
+            Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
                 let prev = state.current_evaluation_scope().kind.replace(probe_kind);
                 assert_eq!(prev, None);
             }
@@ -506,7 +453,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
     ) {
         match self.as_mut() {
             None => {}
-            Some(DebugSolver::GoalEvaluationStep(state)) => {
+            Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
                 let final_state = canonical::make_canonical_state(
                     infcx,
                     &state.var_values,
@@ -543,7 +490,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
     ) {
         match self.as_mut() {
             None => {}
-            Some(DebugSolver::GoalEvaluationStep(state)) => {
+            Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
                 let goal = canonical::make_canonical_state(
                     infcx,
                     &state.var_values,
@@ -563,7 +510,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
         impl_args: ty::GenericArgsRef<'tcx>,
     ) {
         match self.as_mut() {
-            Some(DebugSolver::GoalEvaluationStep(state)) => {
+            Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
                 let impl_args = canonical::make_canonical_state(
                     infcx,
                     &state.var_values,
@@ -582,7 +529,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
 
     pub fn make_canonical_response(&mut self, shallow_certainty: Certainty) {
         match self.as_mut() {
-            Some(DebugSolver::GoalEvaluationStep(state)) => {
+            Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
                 state
                     .current_evaluation_scope()
                     .steps
@@ -596,7 +543,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
     pub fn finish_probe(mut self) -> ProofTreeBuilder<TyCtxt<'tcx>> {
         match self.as_mut() {
             None => {}
-            Some(DebugSolver::GoalEvaluationStep(state)) => {
+            Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
                 assert_ne!(state.probe_depth, 0);
                 let num_var_values = state.current_evaluation_scope().initial_num_var_values;
                 state.var_values.truncate(num_var_values);
@@ -608,46 +555,13 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
         self
     }
 
-    pub fn start_evaluate_added_goals(&mut self) {
-        match self.as_mut() {
-            None => {}
-            Some(DebugSolver::GoalEvaluationStep(state)) => {
-                state.current_evaluation_scope().steps.push(WipProbeStep::EvaluateGoals(
-                    WipAddedGoalsEvaluation { evaluations: vec![], result: None },
-                ));
-            }
-            _ => bug!(),
-        }
-    }
-
-    pub fn start_evaluate_added_goals_step(&mut self) {
-        match self.as_mut() {
-            None => {}
-            Some(DebugSolver::GoalEvaluationStep(state)) => {
-                state.added_goals_evaluation().evaluations.push(vec![]);
-            }
-            _ => bug!(),
-        }
-    }
-
-    pub fn evaluate_added_goals_result(&mut self, result: Result<Certainty, NoSolution>) {
-        match self.as_mut() {
-            None => {}
-            Some(DebugSolver::GoalEvaluationStep(state)) => {
-                let prev = state.added_goals_evaluation().result.replace(result);
-                assert_eq!(prev, None);
-            }
-            _ => bug!(),
-        }
-    }
-
     pub fn query_result(&mut self, result: QueryResult<TyCtxt<'tcx>>) {
         if let Some(this) = self.as_mut() {
             match this {
                 DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
                     assert_eq!(canonical_goal_evaluation.result.replace(result), None);
                 }
-                DebugSolver::GoalEvaluationStep(evaluation_step) => {
+                DebugSolver::CanonicalGoalEvaluationStep(evaluation_step) => {
                     assert_eq!(
                         evaluation_step
                             .evaluation
diff --git a/compiler/rustc_trait_selection/src/solve/search_graph.rs b/compiler/rustc_trait_selection/src/solve/search_graph.rs
index bcd210f789b..6be623b6044 100644
--- a/compiler/rustc_trait_selection/src/solve/search_graph.rs
+++ b/compiler/rustc_trait_selection/src/solve/search_graph.rs
@@ -274,7 +274,8 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
                 last.encountered_overflow = true;
             }
 
-            inspect.goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::Overflow);
+            inspect
+                .canonical_goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::Overflow);
             return Self::response_no_constraints(tcx, input, Certainty::overflow(true));
         };
 
@@ -302,8 +303,9 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
             // We have a nested goal which is already in the provisional cache, use
             // its result. We do not provide any usage kind as that should have been
             // already set correctly while computing the cache entry.
-            inspect
-                .goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::ProvisionalCacheHit);
+            inspect.canonical_goal_evaluation_kind(
+                inspect::WipCanonicalGoalEvaluationKind::ProvisionalCacheHit,
+            );
             Self::tag_cycle_participants(&mut self.stack, HasBeenUsed::empty(), entry.head);
             return entry.result;
         } else if let Some(stack_depth) = cache_entry.stack_depth {
@@ -314,7 +316,9 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
             //
             // Finally we can return either the provisional response or the initial response
             // in case we're in the first fixpoint iteration for this goal.
-            inspect.goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::CycleInStack);
+            inspect.canonical_goal_evaluation_kind(
+                inspect::WipCanonicalGoalEvaluationKind::CycleInStack,
+            );
             let is_coinductive_cycle = Self::stack_coinductive_from(tcx, &self.stack, stack_depth);
             let usage_kind = if is_coinductive_cycle {
                 HasBeenUsed::COINDUCTIVE_CYCLE
@@ -371,7 +375,7 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
                 (current_entry, result)
             });
 
-        let proof_tree = inspect.finalize_evaluation(tcx);
+        let proof_tree = inspect.finalize_canonical_goal_evaluation(tcx);
 
         // We're now done with this goal. In case this goal is involved in a larger cycle
         // do not remove it from the provisional cache and update its provisional result.
@@ -433,9 +437,9 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
         // the goal. We simply overwrite the existing entry once we're done,
         // caching the proof tree.
         if !inspect.is_noop() {
-            if let Some(revisions) = proof_tree {
-                let kind = inspect::WipCanonicalGoalEvaluationKind::Interned { revisions };
-                inspect.goal_evaluation_kind(kind);
+            if let Some(final_revision) = proof_tree {
+                let kind = inspect::WipCanonicalGoalEvaluationKind::Interned { final_revision };
+                inspect.canonical_goal_evaluation_kind(kind);
             } else {
                 return None;
             }
diff --git a/compiler/rustc_trait_selection/src/traits/error_reporting/mod.rs b/compiler/rustc_trait_selection/src/traits/error_reporting/mod.rs
index e50edfdc656..633d488f7be 100644
--- a/compiler/rustc_trait_selection/src/traits/error_reporting/mod.rs
+++ b/compiler/rustc_trait_selection/src/traits/error_reporting/mod.rs
@@ -7,15 +7,11 @@ pub mod suggestions;
 mod type_err_ctxt_ext;
 
 use super::{Obligation, ObligationCause, ObligationCauseCode, PredicateObligation};
-use crate::infer::InferCtxt;
-use crate::solve::{GenerateProofTree, InferCtxtEvalExt};
 use rustc_hir as hir;
 use rustc_hir::def_id::DefId;
 use rustc_hir::intravisit::Visitor;
-use rustc_middle::traits::solve::Goal;
 use rustc_middle::ty::{self, Ty, TyCtxt};
 use rustc_span::Span;
-use std::io::Write;
 use std::ops::ControlFlow;
 
 pub use self::infer_ctxt_ext::*;
@@ -184,16 +180,3 @@ pub enum DefIdOrName {
     DefId(DefId),
     Name(&'static str),
 }
-
-pub fn dump_proof_tree<'tcx>(o: &Obligation<'tcx, ty::Predicate<'tcx>>, infcx: &InferCtxt<'tcx>) {
-    infcx.probe(|_| {
-        let goal = Goal { predicate: o.predicate, param_env: o.param_env };
-        let tree = infcx
-            .evaluate_root_goal(goal, GenerateProofTree::Yes)
-            .1
-            .expect("proof tree should have been generated");
-        let mut lock = std::io::stdout().lock();
-        let _ = lock.write_fmt(format_args!("{tree:?}\n"));
-        let _ = lock.flush();
-    });
-}
diff --git a/compiler/rustc_trait_selection/src/traits/error_reporting/type_err_ctxt_ext.rs b/compiler/rustc_trait_selection/src/traits/error_reporting/type_err_ctxt_ext.rs
index 494fca0336c..46953a61296 100644
--- a/compiler/rustc_trait_selection/src/traits/error_reporting/type_err_ctxt_ext.rs
+++ b/compiler/rustc_trait_selection/src/traits/error_reporting/type_err_ctxt_ext.rs
@@ -46,7 +46,6 @@ use rustc_middle::ty::{
     TypeVisitableExt, Upcast,
 };
 use rustc_middle::{bug, span_bug};
-use rustc_session::config::DumpSolverProofTree;
 use rustc_session::Limit;
 use rustc_span::def_id::LOCAL_CRATE;
 use rustc_span::symbol::sym;
@@ -56,8 +55,8 @@ use std::fmt;
 use std::iter;
 
 use super::{
-    dump_proof_tree, ArgKind, CandidateSimilarity, FindExprBySpan, FindTypeParam,
-    GetSafeTransmuteErrorAndReason, HasNumericInferVisitor, ImplCandidate, UnsatisfiedConst,
+    ArgKind, CandidateSimilarity, FindExprBySpan, FindTypeParam, GetSafeTransmuteErrorAndReason,
+    HasNumericInferVisitor, ImplCandidate, UnsatisfiedConst,
 };
 
 pub use rustc_infer::traits::error_reporting::*;
@@ -369,13 +368,6 @@ impl<'tcx> TypeErrCtxt<'_, 'tcx> {
         error: &SelectionError<'tcx>,
     ) -> ErrorGuaranteed {
         let tcx = self.tcx;
-
-        if tcx.sess.opts.unstable_opts.next_solver.map(|c| c.dump_tree).unwrap_or_default()
-            == DumpSolverProofTree::OnError
-        {
-            dump_proof_tree(root_obligation, self.infcx);
-        }
-
         let mut span = obligation.cause.span;
 
         let mut err = match *error {
@@ -1529,12 +1521,6 @@ impl<'tcx> TypeErrCtxt<'_, 'tcx> {
 
     #[instrument(skip(self), level = "debug")]
     fn report_fulfillment_error(&self, error: &FulfillmentError<'tcx>) -> ErrorGuaranteed {
-        if self.tcx.sess.opts.unstable_opts.next_solver.map(|c| c.dump_tree).unwrap_or_default()
-            == DumpSolverProofTree::OnError
-        {
-            dump_proof_tree(&error.root_obligation, self.infcx);
-        }
-
         match error.code {
             FulfillmentErrorCode::Select(ref selection_error) => self.report_selection_error(
                 error.obligation.clone(),
diff --git a/compiler/rustc_type_ir/src/interner.rs b/compiler/rustc_type_ir/src/interner.rs
index 9b8bb210ff4..c77414afc52 100644
--- a/compiler/rustc_type_ir/src/interner.rs
+++ b/compiler/rustc_type_ir/src/interner.rs
@@ -5,7 +5,7 @@ use std::ops::Deref;
 
 use crate::inherent::*;
 use crate::ir_print::IrPrint;
-use crate::solve::inspect::GoalEvaluationStep;
+use crate::solve::inspect::CanonicalGoalEvaluationStep;
 use crate::visit::{Flags, TypeSuperVisitable, TypeVisitable};
 use crate::{
     AliasTerm, AliasTermKind, AliasTy, AliasTyKind, CanonicalVarInfo, CoercePredicate,
@@ -55,7 +55,11 @@ pub trait Interner:
     type PredefinedOpaques: Copy + Debug + Hash + Eq;
     type DefiningOpaqueTypes: Copy + Debug + Hash + Default + Eq + TypeVisitable<Self>;
     type ExternalConstraints: Copy + Debug + Hash + Eq;
-    type GoalEvaluationSteps: Copy + Debug + Hash + Eq + Deref<Target = [GoalEvaluationStep<Self>]>;
+    type CanonicalGoalEvaluationStepRef: Copy
+        + Debug
+        + Hash
+        + Eq
+        + Deref<Target = CanonicalGoalEvaluationStep<Self>>;
 
     // Kinds of tys
     type Ty: Ty<Self>;
diff --git a/compiler/rustc_type_ir/src/solve/inspect.rs b/compiler/rustc_type_ir/src/solve/inspect.rs
index c4f6ee2669b..0733c730064 100644
--- a/compiler/rustc_type_ir/src/solve/inspect.rs
+++ b/compiler/rustc_type_ir/src/solve/inspect.rs
@@ -1,36 +1,29 @@
 //! Data structure used to inspect trait solver behavior.
 //!
 //! During trait solving we optionally build "proof trees", the root of
-//! which is a [GoalEvaluation] with [GoalEvaluationKind::Root]. These
-//! trees are used to improve the debug experience and are also used by
-//! the compiler itself to provide necessary context for error messages.
+//! which is a [GoalEvaluation]. These  trees are used by the compiler
+//! to inspect the behavior of the trait solver and to access its internal
+//! state, e.g. for diagnostics and when selecting impls during codegen.
 //!
 //! Because each nested goal in the solver gets [canonicalized] separately
 //! and we discard inference progress via "probes", we cannot mechanically
 //! use proof trees without somehow "lifting up" data local to the current
-//! `InferCtxt`. Any data used mechanically is therefore canonicalized and
-//! stored as [CanonicalState]. As printing canonicalized data worsens the
-//! debugging dumps, we do not simply canonicalize everything.
+//! `InferCtxt`. To use the data from evaluation we therefore canonicalize
+//! it and store it as a [CanonicalState].
 //!
-//! This means proof trees contain inference variables and placeholders
-//! local to a different `InferCtxt` which must not be used with the
-//! current one.
+//! Proof trees are only shallow, we do not compute the proof tree for nested
+//! goals. Visiting proof trees instead recomputes nested goals in the parents
+//! inference context when necessary.
 //!
 //! [canonicalized]: https://rustc-dev-guide.rust-lang.org/solve/canonicalization.html
 
-mod format;
-
-use std::fmt::{Debug, Write};
-use std::hash::Hash;
-
-use rustc_type_ir_macros::{TypeFoldable_Generic, TypeVisitable_Generic};
-
-use self::format::ProofTreeFormatter;
 use crate::solve::{
-    CandidateSource, CanonicalInput, Certainty, Goal, GoalSource, NoSolution, QueryInput,
-    QueryResult,
+    CandidateSource, CanonicalInput, Certainty, Goal, GoalSource, QueryInput, QueryResult,
 };
 use crate::{Canonical, CanonicalVarValues, Interner};
+use rustc_type_ir_macros::{TypeFoldable_Generic, TypeVisitable_Generic};
+use std::fmt::Debug;
+use std::hash::Hash;
 
 /// Some `data` together with information about how they relate to the input
 /// of the canonical query.
@@ -55,23 +48,15 @@ pub struct State<I: Interner, T> {
 
 pub type CanonicalState<I, T> = Canonical<I, State<I, T>>;
 
-/// When evaluating the root goals we also store the
-/// original values for the `CanonicalVarValues` of the
-/// canonicalized goal. We use this to map any [CanonicalState]
-/// from the local `InferCtxt` of the solver query to
-/// the `InferCtxt` of the caller.
-#[derive(derivative::Derivative)]
-#[derivative(PartialEq(bound = ""), Eq(bound = ""), Hash(bound = ""), Debug(bound = ""))]
-pub enum GoalEvaluationKind<I: Interner> {
-    Root { orig_values: Vec<I::GenericArg> },
-    Nested,
-}
-
+/// When evaluating a goal we also store the original values
+/// for the `CanonicalVarValues` of the canonicalized goal.
+/// We use this to map any [CanonicalState] from the local `InferCtxt`
+/// of the solver query to the `InferCtxt` of the caller.
 #[derive(derivative::Derivative)]
 #[derivative(PartialEq(bound = ""), Eq(bound = ""), Hash(bound = ""))]
 pub struct GoalEvaluation<I: Interner> {
     pub uncanonicalized_goal: Goal<I, I::Predicate>,
-    pub kind: GoalEvaluationKind<I>,
+    pub orig_values: Vec<I::GenericArg>,
     pub evaluation: CanonicalGoalEvaluation<I>,
 }
 
@@ -89,24 +74,12 @@ pub enum CanonicalGoalEvaluationKind<I: Interner> {
     Overflow,
     CycleInStack,
     ProvisionalCacheHit,
-    Evaluation { revisions: I::GoalEvaluationSteps },
-}
-impl<I: Interner> Debug for GoalEvaluation<I> {
-    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        ProofTreeFormatter::new(f).format_goal_evaluation(self)
-    }
+    Evaluation { final_revision: I::CanonicalGoalEvaluationStepRef },
 }
 
 #[derive(derivative::Derivative)]
 #[derivative(PartialEq(bound = ""), Eq(bound = ""), Hash(bound = ""), Debug(bound = ""))]
-pub struct AddedGoalsEvaluation<I: Interner> {
-    pub evaluations: Vec<Vec<GoalEvaluation<I>>>,
-    pub result: Result<Certainty, NoSolution>,
-}
-
-#[derive(derivative::Derivative)]
-#[derivative(PartialEq(bound = ""), Eq(bound = ""), Hash(bound = ""), Debug(bound = ""))]
-pub struct GoalEvaluationStep<I: Interner> {
+pub struct CanonicalGoalEvaluationStep<I: Interner> {
     pub instantiated_goal: QueryInput<I, I::Predicate>,
 
     /// The actual evaluation of the goal, always `ProbeKind::Root`.
@@ -117,7 +90,7 @@ pub struct GoalEvaluationStep<I: Interner> {
 /// corresponds to a `EvalCtxt::probe(_X)` call or the root evaluation
 /// of a goal.
 #[derive(derivative::Derivative)]
-#[derivative(PartialEq(bound = ""), Eq(bound = ""), Hash(bound = ""))]
+#[derivative(Debug(bound = ""), PartialEq(bound = ""), Eq(bound = ""), Hash(bound = ""))]
 pub struct Probe<I: Interner> {
     /// What happened inside of this probe in chronological order.
     pub steps: Vec<ProbeStep<I>>,
@@ -125,23 +98,15 @@ pub struct Probe<I: Interner> {
     pub final_state: CanonicalState<I, ()>,
 }
 
-impl<I: Interner> Debug for Probe<I> {
-    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        ProofTreeFormatter::new(f).format_probe(self)
-    }
-}
-
 #[derive(derivative::Derivative)]
 #[derivative(PartialEq(bound = ""), Eq(bound = ""), Hash(bound = ""), Debug(bound = ""))]
 pub enum ProbeStep<I: Interner> {
     /// We added a goal to the `EvalCtxt` which will get proven
     /// the next time `EvalCtxt::try_evaluate_added_goals` is called.
     AddGoal(GoalSource, CanonicalState<I, Goal<I, I::Predicate>>),
-    /// The inside of a `EvalCtxt::try_evaluate_added_goals` call.
-    EvaluateGoals(AddedGoalsEvaluation<I>),
     /// A call to `probe` while proving the current goal. This is
     /// used whenever there are multiple candidates to prove the
-    /// current goalby .
+    /// current goal.
     NestedProbe(Probe<I>),
     /// A trait goal was satisfied by an impl candidate.
     RecordImplArgs { impl_args: CanonicalState<I, I::GenericArgs> },
diff --git a/compiler/rustc_type_ir/src/solve/inspect/format.rs b/compiler/rustc_type_ir/src/solve/inspect/format.rs
deleted file mode 100644
index 44ade04cf98..00000000000
--- a/compiler/rustc_type_ir/src/solve/inspect/format.rs
+++ /dev/null
@@ -1,173 +0,0 @@
-use std::marker::PhantomData;
-
-use super::*;
-
-pub(super) struct ProofTreeFormatter<'a, 'b, I> {
-    f: &'a mut (dyn Write + 'b),
-    _interner: PhantomData<I>,
-}
-
-enum IndentorState {
-    StartWithNewline,
-    OnNewline,
-    Inline,
-}
-
-/// A formatter which adds 4 spaces of indentation to its input before
-/// passing it on to its nested formatter.
-///
-/// We can use this for arbitrary levels of indentation by nesting it.
-struct Indentor<'a, 'b> {
-    f: &'a mut (dyn Write + 'b),
-    state: IndentorState,
-}
-
-impl Write for Indentor<'_, '_> {
-    fn write_str(&mut self, s: &str) -> std::fmt::Result {
-        for line in s.split_inclusive('\n') {
-            match self.state {
-                IndentorState::StartWithNewline => self.f.write_str("\n    ")?,
-                IndentorState::OnNewline => self.f.write_str("    ")?,
-                IndentorState::Inline => {}
-            }
-            self.state =
-                if line.ends_with('\n') { IndentorState::OnNewline } else { IndentorState::Inline };
-            self.f.write_str(line)?;
-        }
-
-        Ok(())
-    }
-}
-
-impl<'a, 'b, I: Interner> ProofTreeFormatter<'a, 'b, I> {
-    pub(super) fn new(f: &'a mut (dyn Write + 'b)) -> Self {
-        ProofTreeFormatter { f, _interner: PhantomData }
-    }
-
-    fn nested<F>(&mut self, func: F) -> std::fmt::Result
-    where
-        F: FnOnce(&mut ProofTreeFormatter<'_, '_, I>) -> std::fmt::Result,
-    {
-        write!(self.f, " {{")?;
-        func(&mut ProofTreeFormatter {
-            f: &mut Indentor { f: self.f, state: IndentorState::StartWithNewline },
-            _interner: PhantomData,
-        })?;
-        writeln!(self.f, "}}")
-    }
-
-    pub(super) fn format_goal_evaluation(&mut self, eval: &GoalEvaluation<I>) -> std::fmt::Result {
-        let goal_text = match eval.kind {
-            GoalEvaluationKind::Root { orig_values: _ } => "ROOT GOAL",
-            GoalEvaluationKind::Nested => "GOAL",
-        };
-        write!(self.f, "{}: {:?}", goal_text, eval.uncanonicalized_goal)?;
-        self.nested(|this| this.format_canonical_goal_evaluation(&eval.evaluation))
-    }
-
-    pub(super) fn format_canonical_goal_evaluation(
-        &mut self,
-        eval: &CanonicalGoalEvaluation<I>,
-    ) -> std::fmt::Result {
-        writeln!(self.f, "GOAL: {:?}", eval.goal)?;
-
-        match &eval.kind {
-            CanonicalGoalEvaluationKind::Overflow => {
-                writeln!(self.f, "OVERFLOW: {:?}", eval.result)
-            }
-            CanonicalGoalEvaluationKind::CycleInStack => {
-                writeln!(self.f, "CYCLE IN STACK: {:?}", eval.result)
-            }
-            CanonicalGoalEvaluationKind::ProvisionalCacheHit => {
-                writeln!(self.f, "PROVISIONAL CACHE HIT: {:?}", eval.result)
-            }
-            CanonicalGoalEvaluationKind::Evaluation { revisions } => {
-                for (n, step) in revisions.iter().enumerate() {
-                    write!(self.f, "REVISION {n}")?;
-                    self.nested(|this| this.format_evaluation_step(step))?;
-                }
-                writeln!(self.f, "RESULT: {:?}", eval.result)
-            }
-        }
-    }
-
-    pub(super) fn format_evaluation_step(
-        &mut self,
-        evaluation_step: &GoalEvaluationStep<I>,
-    ) -> std::fmt::Result {
-        writeln!(self.f, "INSTANTIATED: {:?}", evaluation_step.instantiated_goal)?;
-        self.format_probe(&evaluation_step.evaluation)
-    }
-
-    pub(super) fn format_probe(&mut self, probe: &Probe<I>) -> std::fmt::Result {
-        match &probe.kind {
-            ProbeKind::Root { result } => {
-                write!(self.f, "ROOT RESULT: {result:?}")
-            }
-            ProbeKind::TryNormalizeNonRigid { result } => {
-                write!(self.f, "TRY NORMALIZE NON-RIGID: {result:?}")
-            }
-            ProbeKind::NormalizedSelfTyAssembly => {
-                write!(self.f, "NORMALIZING SELF TY FOR ASSEMBLY:")
-            }
-            ProbeKind::UnsizeAssembly => {
-                write!(self.f, "ASSEMBLING CANDIDATES FOR UNSIZING:")
-            }
-            ProbeKind::UpcastProjectionCompatibility => {
-                write!(self.f, "PROBING FOR PROJECTION COMPATIBILITY FOR UPCASTING:")
-            }
-            ProbeKind::OpaqueTypeStorageLookup { result } => {
-                write!(self.f, "PROBING FOR AN EXISTING OPAQUE: {result:?}")
-            }
-            ProbeKind::TraitCandidate { source, result } => {
-                write!(self.f, "CANDIDATE {source:?}: {result:?}")
-            }
-            ProbeKind::ShadowedEnvProbing => {
-                write!(self.f, "PROBING FOR IMPLS SHADOWED BY PARAM-ENV CANDIDATE:")
-            }
-        }?;
-
-        self.nested(|this| {
-            for step in &probe.steps {
-                match step {
-                    ProbeStep::AddGoal(source, goal) => {
-                        let source = match source {
-                            GoalSource::Misc => "misc",
-                            GoalSource::ImplWhereBound => "impl where-bound",
-                            GoalSource::InstantiateHigherRanked => "higher-ranked goal",
-                        };
-                        writeln!(this.f, "ADDED GOAL ({source}): {goal:?}")?
-                    }
-                    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:?}")?
-                    }
-                    ProbeStep::RecordImplArgs { impl_args } => {
-                        writeln!(this.f, "RECORDED IMPL ARGS: {impl_args:?}")?
-                    }
-                }
-            }
-            Ok(())
-        })
-    }
-
-    pub(super) fn format_added_goals_evaluation(
-        &mut self,
-        added_goals_evaluation: &AddedGoalsEvaluation<I>,
-    ) -> std::fmt::Result {
-        writeln!(self.f, "TRY_EVALUATE_ADDED_GOALS: {:?}", added_goals_evaluation.result)?;
-
-        for (n, iterations) in added_goals_evaluation.evaluations.iter().enumerate() {
-            write!(self.f, "ITERATION {n}")?;
-            self.nested(|this| {
-                for goal_evaluation in iterations {
-                    this.format_goal_evaluation(goal_evaluation)?;
-                }
-                Ok(())
-            })?;
-        }
-
-        Ok(())
-    }
-}