proof tree cleanup 1/n

lcnr · lcnr · commit ef65bdad9c71 · 2025-08-28T09:57:36.000+02:00
diff --git a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs
@@ -24,9 +24,8 @@ use crate::solve::inspect::{self, ProofTreeBuilder};
 use crate::solve::search_graph::SearchGraph;
 use crate::solve::ty::may_use_unstable_feature;
 use crate::solve::{
-    CanonicalInput, Certainty, FIXPOINT_STEP_LIMIT, Goal, GoalEvaluation, GoalEvaluationKind,
-    GoalSource, GoalStalledOn, HasChanged, NestedNormalizationGoals, NoSolution, QueryInput,
-    QueryResult,
+    CanonicalInput, Certainty, FIXPOINT_STEP_LIMIT, Goal, GoalEvaluation, GoalSource,
+    GoalStalledOn, HasChanged, NestedNormalizationGoals, NoSolution, QueryInput, QueryResult,
 };
 
 pub(super) mod canonical;
@@ -172,10 +171,7 @@ pub trait SolverDelegateEvalExt: SolverDelegate {
         goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
         span: <Self::Interner as Interner>::Span,
     ) -> (
-        Result<
-            (NestedNormalizationGoals<Self::Interner>, GoalEvaluation<Self::Interner>),
-            NoSolution,
-        >,
+        Result<NestedNormalizationGoals<Self::Interner>, NoSolution>,
         inspect::GoalEvaluation<Self::Interner>,
     );
 }
@@ -192,14 +188,9 @@ where
         span: I::Span,
         stalled_on: Option<GoalStalledOn<I>>,
     ) -> Result<GoalEvaluation<I>, NoSolution> {
-        EvalCtxt::enter_root(
-            self,
-            self.cx().recursion_limit(),
-            GenerateProofTree::No,
-            span,
-            |ecx| ecx.evaluate_goal(GoalEvaluationKind::Root, GoalSource::Misc, goal, stalled_on),
-        )
-        .0
+        EvalCtxt::enter_root(self, self.cx().recursion_limit(), span, |ecx| {
+            ecx.evaluate_goal(GoalSource::Misc, goal, stalled_on)
+        })
     }
 
     fn root_goal_may_hold_with_depth(
@@ -208,10 +199,9 @@ where
         goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
     ) -> bool {
         self.probe(|| {
-            EvalCtxt::enter_root(self, root_depth, GenerateProofTree::No, I::Span::dummy(), |ecx| {
-                ecx.evaluate_goal(GoalEvaluationKind::Root, GoalSource::Misc, goal, None)
+            EvalCtxt::enter_root(self, root_depth, I::Span::dummy(), |ecx| {
+                ecx.evaluate_goal(GoalSource::Misc, goal, None)
             })
-            .0
         })
         .is_ok()
     }
@@ -221,18 +211,10 @@ where
         &self,
         goal: Goal<I, I::Predicate>,
         span: I::Span,
-    ) -> (
-        Result<(NestedNormalizationGoals<I>, GoalEvaluation<I>), NoSolution>,
-        inspect::GoalEvaluation<I>,
-    ) {
-        let (result, proof_tree) = EvalCtxt::enter_root(
-            self,
-            self.cx().recursion_limit(),
-            GenerateProofTree::Yes,
-            span,
-            |ecx| ecx.evaluate_goal_raw(GoalEvaluationKind::Root, GoalSource::Misc, goal, None),
-        );
-        (result, proof_tree.unwrap())
+    ) -> (Result<NestedNormalizationGoals<I>, NoSolution>, inspect::GoalEvaluation<I>) {
+        EvalCtxt::enter_root(self, self.cx().recursion_limit(), span, |ecx| {
+            ecx.evaluate_goal_for_proof_tree(goal)
+        })
     }
 }
 
@@ -301,17 +283,16 @@ where
     pub(super) fn enter_root<R>(
         delegate: &D,
         root_depth: usize,
-        generate_proof_tree: GenerateProofTree,
         origin_span: I::Span,
         f: impl FnOnce(&mut EvalCtxt<'_, D>) -> R,
-    ) -> (R, Option<inspect::GoalEvaluation<I>>) {
+    ) -> R {
         let mut search_graph = SearchGraph::new(root_depth);
 
         let mut ecx = EvalCtxt {
             delegate,
             search_graph: &mut search_graph,
             nested_goals: Default::default(),
-            inspect: ProofTreeBuilder::new_maybe_root(generate_proof_tree),
+            inspect: ProofTreeBuilder::new_noop(),
 
             // Only relevant when canonicalizing the response,
             // which we don't do within this evaluation context.
@@ -324,15 +305,12 @@ where
             tainted: Ok(()),
         };
         let result = f(&mut ecx);
-
-        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, proof_tree)
+        result
     }
 
     /// Creates a nested evaluation context that shares the same search graph as the
@@ -406,13 +384,12 @@ where
     /// been constrained and the certainty of the result.
     fn evaluate_goal(
         &mut self,
-        goal_evaluation_kind: GoalEvaluationKind,
         source: GoalSource,
         goal: Goal<I, I::Predicate>,
         stalled_on: Option<GoalStalledOn<I>>,
     ) -> Result<GoalEvaluation<I>, NoSolution> {
         let (normalization_nested_goals, goal_evaluation) =
-            self.evaluate_goal_raw(goal_evaluation_kind, source, goal, stalled_on)?;
+            self.evaluate_goal_raw(source, goal, stalled_on)?;
         assert!(normalization_nested_goals.is_empty());
         Ok(goal_evaluation)
     }
@@ -426,7 +403,6 @@ where
     /// storage.
     pub(super) fn evaluate_goal_raw(
         &mut self,
-        goal_evaluation_kind: GoalEvaluationKind,
         source: GoalSource,
         goal: Goal<I, I::Predicate>,
         stalled_on: Option<GoalStalledOn<I>>,
@@ -459,16 +435,12 @@ where
         let (goal, opaque_types) = eager_resolve_vars(self.delegate, (goal, opaque_types));
 
         let (orig_values, canonical_goal) = self.canonicalize_goal(goal, opaque_types);
-        let mut goal_evaluation =
-            self.inspect.new_goal_evaluation(goal, &orig_values, goal_evaluation_kind);
         let canonical_result = self.search_graph.evaluate_goal(
             self.cx(),
             canonical_goal,
             self.step_kind_for_source(source),
-            &mut goal_evaluation,
+            &mut ProofTreeBuilder::new_noop(),
         );
-        goal_evaluation.query_result(canonical_result);
-        self.inspect.goal_evaluation(goal_evaluation);
         let response = match canonical_result {
             Err(e) => return Err(e),
             Ok(response) => response,
@@ -542,6 +514,35 @@ where
         ))
     }
 
+    /// Evaluate a goal to build a proof tree. This is a copy of [EvalCtxt::evaluate_goal_raw].
+    pub(super) fn evaluate_goal_for_proof_tree(
+        &mut self,
+        goal: Goal<I, I::Predicate>,
+    ) -> (Result<NestedNormalizationGoals<I>, NoSolution>, inspect::GoalEvaluation<I>) {
+        let opaque_types = self.delegate.clone_opaque_types_lookup_table();
+        let (goal, opaque_types) = eager_resolve_vars(self.delegate, (goal, opaque_types));
+
+        let (orig_values, canonical_goal) = self.canonicalize_goal(goal, opaque_types);
+        let mut goal_evaluation = ProofTreeBuilder::new_goal_evaluation(goal, &orig_values);
+        let canonical_result = self.search_graph.evaluate_goal(
+            self.cx(),
+            canonical_goal,
+            self.step_kind_for_source(GoalSource::Misc),
+            &mut goal_evaluation,
+        );
+        goal_evaluation.query_result(canonical_result);
+        let proof_tree = goal_evaluation.finalize();
+        let response = match canonical_result {
+            Err(e) => return (Err(e), proof_tree),
+            Ok(response) => response,
+        };
+
+        let (normalization_nested_goals, _certainty) =
+            self.instantiate_and_apply_query_response(goal.param_env, &orig_values, response);
+
+        (Ok(normalization_nested_goals), proof_tree)
+    }
+
     pub(super) fn compute_goal(&mut self, goal: Goal<I, I::Predicate>) -> QueryResult<I> {
         let Goal { param_env, predicate } = goal;
         let kind = predicate.kind();
@@ -676,12 +677,7 @@ where
                 let (
                     NestedNormalizationGoals(nested_goals),
                     GoalEvaluation { goal, certainty, stalled_on, has_changed: _ },
-                ) = self.evaluate_goal_raw(
-                    GoalEvaluationKind::Nested,
-                    source,
-                    unconstrained_goal,
-                    stalled_on,
-                )?;
+                ) = self.evaluate_goal_raw(source, unconstrained_goal, stalled_on)?;
                 // Add the nested goals from normalization to our own nested goals.
                 trace!(?nested_goals);
                 self.nested_goals.extend(nested_goals.into_iter().map(|(s, g)| (s, g, None)));
@@ -734,7 +730,7 @@ where
                 }
             } else {
                 let GoalEvaluation { goal, certainty, has_changed, stalled_on } =
-                    self.evaluate_goal(GoalEvaluationKind::Nested, source, goal, stalled_on)?;
+                    self.evaluate_goal(source, goal, stalled_on)?;
                 if has_changed == HasChanged::Yes {
                     unchanged_certainty = None;
                 }
diff --git a/compiler/rustc_next_trait_solver/src/solve/inspect/build.rs b/compiler/rustc_next_trait_solver/src/solve/inspect/build.rs
@@ -12,9 +12,7 @@ use rustc_type_ir::{self as ty, Interner};
 
 use crate::delegate::SolverDelegate;
 use crate::solve::eval_ctxt::canonical;
-use crate::solve::{
-    Certainty, GenerateProofTree, Goal, GoalEvaluationKind, GoalSource, QueryResult, inspect,
-};
+use crate::solve::{Certainty, Goal, GoalSource, QueryResult, inspect};
 
 /// The core data structure when building proof trees.
 ///
@@ -51,7 +49,6 @@ where
 /// We simply ICE in case that assumption is broken.
 #[derive_where(Debug; I: Interner)]
 enum DebugSolver<I: Interner> {
-    Root,
     GoalEvaluation(WipGoalEvaluation<I>),
     CanonicalGoalEvaluationStep(WipCanonicalGoalEvaluationStep<I>),
 }
@@ -182,17 +179,6 @@ impl<I: Interner> WipProbeStep<I> {
 }
 
 impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
-    fn new(state: impl Into<DebugSolver<I>>) -> ProofTreeBuilder<D> {
-        ProofTreeBuilder { state: Some(Box::new(state.into())), _infcx: PhantomData }
-    }
-
-    fn opt_nested<T: Into<DebugSolver<I>>>(&self, state: impl FnOnce() -> Option<T>) -> Self {
-        ProofTreeBuilder {
-            state: self.state.as_ref().and_then(|_| Some(state()?.into())).map(Box::new),
-            _infcx: PhantomData,
-        }
-    }
-
     fn nested<T: Into<DebugSolver<I>>>(&self, state: impl FnOnce() -> T) -> Self {
         ProofTreeBuilder {
             state: self.state.as_ref().map(|_| Box::new(state().into())),
@@ -210,50 +196,35 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
         nested
     }
 
-    pub(crate) fn finalize(self) -> Option<inspect::GoalEvaluation<I>> {
-        match *self.state? {
-            DebugSolver::GoalEvaluation(wip_goal_evaluation) => {
-                Some(wip_goal_evaluation.finalize())
-            }
+    pub(crate) fn finalize(self) -> inspect::GoalEvaluation<I> {
+        match *self.state.unwrap() {
+            DebugSolver::GoalEvaluation(wip_goal_evaluation) => wip_goal_evaluation.finalize(),
             root => unreachable!("unexpected proof tree builder root node: {:?}", root),
         }
     }
 
-    pub(crate) fn new_maybe_root(generate_proof_tree: GenerateProofTree) -> ProofTreeBuilder<D> {
-        match generate_proof_tree {
-            GenerateProofTree::No => ProofTreeBuilder::new_noop(),
-            GenerateProofTree::Yes => ProofTreeBuilder::new_root(),
-        }
-    }
-
-    fn new_root() -> ProofTreeBuilder<D> {
-        ProofTreeBuilder::new(DebugSolver::Root)
+    pub(crate) fn is_noop(&self) -> bool {
+        self.state.is_none()
     }
 
-    fn new_noop() -> ProofTreeBuilder<D> {
+    pub(crate) fn new_noop() -> ProofTreeBuilder<D> {
         ProofTreeBuilder { state: None, _infcx: PhantomData }
     }
 
-    pub(crate) fn is_noop(&self) -> bool {
-        self.state.is_none()
-    }
-
     pub(in crate::solve) fn new_goal_evaluation(
-        &mut self,
         uncanonicalized_goal: Goal<I, I::Predicate>,
         orig_values: &[I::GenericArg],
-        kind: GoalEvaluationKind,
     ) -> ProofTreeBuilder<D> {
-        self.opt_nested(|| match kind {
-            GoalEvaluationKind::Root => Some(WipGoalEvaluation {
+        ProofTreeBuilder {
+            state: Some(Box::new(DebugSolver::GoalEvaluation(WipGoalEvaluation {
                 uncanonicalized_goal,
                 orig_values: orig_values.to_vec(),
                 encountered_overflow: false,
                 final_revision: None,
                 result: None,
-            }),
-            GoalEvaluationKind::Nested => None,
-        })
+            }))),
+            _infcx: PhantomData,
+        }
     }
 
     pub(crate) fn canonical_goal_evaluation_overflow(&mut self) {
@@ -267,18 +238,6 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
         }
     }
 
-    pub(crate) fn goal_evaluation(&mut self, goal_evaluation: ProofTreeBuilder<D>) {
-        if let Some(this) = self.as_mut() {
-            match this {
-                DebugSolver::Root => *this = *goal_evaluation.state.unwrap(),
-                DebugSolver::CanonicalGoalEvaluationStep(_) => {
-                    assert!(goal_evaluation.state.is_none())
-                }
-                _ => unreachable!(),
-            }
-        }
-    }
-
     pub(crate) fn new_goal_evaluation_step(
         &mut self,
         var_values: ty::CanonicalVarValues<I>,
@@ -457,7 +416,6 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
                         None
                     );
                 }
-                _ => unreachable!(),
             }
         }
     }
diff --git a/compiler/rustc_next_trait_solver/src/solve/mod.rs b/compiler/rustc_next_trait_solver/src/solve/mod.rs
@@ -42,12 +42,6 @@ use crate::solve::assembly::Candidate;
 /// recursion limit again. However, this feels very unlikely.
 const FIXPOINT_STEP_LIMIT: usize = 8;
 
-#[derive(Debug, Copy, Clone, PartialEq, Eq)]
-enum GoalEvaluationKind {
-    Root,
-    Nested,
-}
-
 /// Whether evaluating this goal ended up changing the
 /// inference state.
 #[derive(PartialEq, Eq, Debug, Hash, Clone, Copy)]
diff --git a/compiler/rustc_trait_selection/src/solve/inspect/analyse.rs b/compiler/rustc_trait_selection/src/solve/inspect/analyse.rs
@@ -249,7 +249,7 @@ impl<'a, 'tcx> InspectCandidate<'a, 'tcx> {
                     // `InspectGoal::new` so that the goal has the right result (and maintains
                     // the impression that we don't do this normalizes-to infer hack at all).
                     let (nested, proof_tree) = infcx.evaluate_root_goal_for_proof_tree(goal, span);
-                    let nested_goals_result = nested.and_then(|(nested, _)| {
+                    let nested_goals_result = nested.and_then(|nested| {
                         normalizes_to_term_hack.constrain_and(
                             infcx,
                             span,
