hir typeck: look into nested goals

uses a `ProofTreeVisitor` to look into nested
goals when looking at the pending obligations
during hir typeck. Used by closure signature
inference, coercion, and for async functions.

8 files changed, 418 insertions, 237 deletions

diff --git a/compiler/rustc_trait_selection/src/solve/assembly/mod.rs b/compiler/rustc_trait_selection/src/solve/assembly/mod.rs
index 68b0db21141..95221529093 100644
--- a/compiler/rustc_trait_selection/src/solve/assembly/mod.rs
+++ b/compiler/rustc_trait_selection/src/solve/assembly/mod.rs
@@ -1,7 +1,7 @@
 //! Code shared by trait and projection goals for candidate assembly.
 
-use super::{EvalCtxt, SolverMode};
 use crate::solve::GoalSource;
+use crate::solve::{inspect, EvalCtxt, SolverMode};
 use crate::traits::coherence;
 use rustc_hir::def_id::DefId;
 use rustc_infer::traits::query::NoSolution;
@@ -16,6 +16,7 @@ use rustc_middle::ty::{fast_reject, TypeFoldable};
 use rustc_middle::ty::{ToPredicate, TypeVisitableExt};
 use rustc_span::{ErrorGuaranteed, DUMMY_SP};
 use std::fmt::Debug;
+use std::mem;
 
 pub(super) mod structural_traits;
 
@@ -315,20 +316,17 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
     }
 
     fn forced_ambiguity(&mut self, cause: MaybeCause) -> Vec<Candidate<'tcx>> {
-        let source = CandidateSource::BuiltinImpl(BuiltinImplSource::Misc);
-        let certainty = Certainty::Maybe(cause);
         // This may fail if `try_evaluate_added_goals` overflows because it
         // fails to reach a fixpoint but ends up getting an error after
         // running for some additional step.
         //
-        // FIXME: Add a test for this. It seems to be necessary for typenum but
-        // is incredibly hard to minimize as it may rely on being inside of a
-        // trait solver cycle.
-        let result = self.evaluate_added_goals_and_make_canonical_response(certainty);
-        let mut dummy_probe = self.inspect.new_probe();
-        dummy_probe.probe_kind(ProbeKind::TraitCandidate { source, result });
-        self.inspect.finish_probe(dummy_probe);
-        if let Ok(result) = result { vec![Candidate { source, result }] } else { vec![] }
+        // cc trait-system-refactor-initiative#105
+        let source = CandidateSource::BuiltinImpl(BuiltinImplSource::Misc);
+        let certainty = Certainty::Maybe(cause);
+        let result = self
+            .probe_trait_candidate(source)
+            .enter(|this| this.evaluate_added_goals_and_make_canonical_response(certainty));
+        if let Ok(cand) = result { vec![cand] } else { vec![] }
     }
 
     #[instrument(level = "debug", skip_all)]
@@ -813,6 +811,11 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
         goal: Goal<'tcx, G>,
         candidates: &mut Vec<Candidate<'tcx>>,
     ) {
+        // HACK: We temporarily remove the `ProofTreeBuilder` to
+        // avoid adding `Trait` candidates to the candidates used
+        // to prove the current goal.
+        let inspect = mem::replace(&mut self.inspect, inspect::ProofTreeBuilder::new_noop());
+
         let tcx = self.tcx();
         let trait_goal: Goal<'tcx, ty::TraitPredicate<'tcx>> =
             goal.with(tcx, goal.predicate.trait_ref(tcx));
@@ -846,6 +849,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
                 }
             }
         }
+        self.inspect = inspect;
     }
 
     /// If there are multiple ways to prove a trait or projection goal, we have
diff --git a/compiler/rustc_trait_selection/src/solve/eval_ctxt/canonical.rs b/compiler/rustc_trait_selection/src/solve/eval_ctxt/canonical.rs
index 0b37163d597..9edeb0fa71b 100644
--- a/compiler/rustc_trait_selection/src/solve/eval_ctxt/canonical.rs
+++ b/compiler/rustc_trait_selection/src/solve/eval_ctxt/canonical.rs
@@ -19,9 +19,12 @@ use rustc_infer::infer::canonical::query_response::make_query_region_constraints
 use rustc_infer::infer::canonical::CanonicalVarValues;
 use rustc_infer::infer::canonical::{CanonicalExt, QueryRegionConstraints};
 use rustc_infer::infer::resolve::EagerResolver;
+use rustc_infer::infer::type_variable::TypeVariableOrigin;
+use rustc_infer::infer::RegionVariableOrigin;
 use rustc_infer::infer::{InferCtxt, InferOk};
 use rustc_infer::traits::solve::NestedNormalizationGoals;
 use rustc_middle::infer::canonical::Canonical;
+use rustc_middle::infer::unify_key::ConstVariableOrigin;
 use rustc_middle::traits::query::NoSolution;
 use rustc_middle::traits::solve::{
     ExternalConstraintsData, MaybeCause, PredefinedOpaquesData, QueryInput,
@@ -29,7 +32,7 @@ use rustc_middle::traits::solve::{
 use rustc_middle::traits::ObligationCause;
 use rustc_middle::ty::{self, BoundVar, GenericArgKind, Ty, TyCtxt, TypeFoldable};
 use rustc_next_trait_solver::canonicalizer::{CanonicalizeMode, Canonicalizer};
-use rustc_span::DUMMY_SP;
+use rustc_span::{Span, DUMMY_SP};
 use std::assert_matches::assert_matches;
 use std::iter;
 use std::ops::Deref;
@@ -374,36 +377,70 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
     }
 }
 
-impl<'tcx> inspect::ProofTreeBuilder<'tcx> {
-    pub fn make_canonical_state<T: TypeFoldable<TyCtxt<'tcx>>>(
-        ecx: &EvalCtxt<'_, 'tcx>,
-        data: T,
-    ) -> inspect::CanonicalState<'tcx, T> {
-        let state = inspect::State { var_values: ecx.var_values, data };
-        let state = state.fold_with(&mut EagerResolver::new(ecx.infcx));
-        Canonicalizer::canonicalize(
-            ecx.infcx,
-            CanonicalizeMode::Response { max_input_universe: ecx.max_input_universe },
-            &mut vec![],
-            state,
-        )
+/// Used by proof trees to be able to recompute intermediate actions while
+/// evaluating a goal. The `var_values` not only include the bound variables
+/// of the query input, but also contain all unconstrained inference vars
+/// created while evaluating this goal.
+pub(in crate::solve) fn make_canonical_state<'tcx, T: TypeFoldable<TyCtxt<'tcx>>>(
+    infcx: &InferCtxt<'tcx>,
+    var_values: &[ty::GenericArg<'tcx>],
+    max_input_universe: ty::UniverseIndex,
+    data: T,
+) -> inspect::CanonicalState<'tcx, T> {
+    let var_values = CanonicalVarValues { var_values: infcx.tcx.mk_args(var_values) };
+    let state = inspect::State { var_values, data };
+    let state = state.fold_with(&mut EagerResolver::new(infcx));
+    Canonicalizer::canonicalize(
+        infcx,
+        CanonicalizeMode::Response { max_input_universe },
+        &mut vec![],
+        state,
+    )
+}
+
+/// Instantiate a `CanonicalState`.
+///
+/// Unlike for query responses, `CanonicalState` also track fresh inference
+/// variables created while evaluating a goal. When creating two separate
+/// `CanonicalState` during a single evaluation both may reference this
+/// fresh inference variable. When instantiating them we now create separate
+/// inference variables for it and have to unify them somehow. We do this
+/// by extending the `var_values` while building the proof tree.
+///
+/// This currently assumes that unifying the var values trivially succeeds.
+/// Adding any inference constraints which weren't present when originally
+/// computing the canonical query can result in bugs.
+pub(in crate::solve) fn instantiate_canonical_state<'tcx, T: TypeFoldable<TyCtxt<'tcx>>>(
+    infcx: &InferCtxt<'tcx>,
+    span: Span,
+    param_env: ty::ParamEnv<'tcx>,
+    orig_values: &mut Vec<ty::GenericArg<'tcx>>,
+    state: inspect::CanonicalState<'tcx, T>,
+) -> T {
+    // In case any fresh inference variables have been created between `state`
+    // and the previous instantiation, extend `orig_values` for it.
+    assert!(orig_values.len() <= state.value.var_values.len());
+    for i in orig_values.len()..state.value.var_values.len() {
+        let unconstrained = match state.value.var_values.var_values[i].unpack() {
+            ty::GenericArgKind::Lifetime(_) => {
+                infcx.next_region_var(RegionVariableOrigin::MiscVariable(span)).into()
+            }
+            ty::GenericArgKind::Type(_) => {
+                infcx.next_ty_var(TypeVariableOrigin { param_def_id: None, span }).into()
+            }
+            ty::GenericArgKind::Const(ct) => infcx
+                .next_const_var(ct.ty(), ConstVariableOrigin { param_def_id: None, span })
+                .into(),
+        };
+
+        orig_values.push(unconstrained);
     }
 
-    /// Instantiate a `CanonicalState`. This assumes that unifying the var values
-    /// trivially succeeds. Adding any inference constraints which weren't present when
-    /// originally computing the canonical query can result in bugs.
-    pub fn instantiate_canonical_state<T: TypeFoldable<TyCtxt<'tcx>>>(
-        infcx: &InferCtxt<'tcx>,
-        param_env: ty::ParamEnv<'tcx>,
-        original_values: &[ty::GenericArg<'tcx>],
-        state: inspect::CanonicalState<'tcx, T>,
-    ) -> T {
-        let instantiation =
-            EvalCtxt::compute_query_response_instantiation_values(infcx, original_values, &state);
+    let instantiation =
+        EvalCtxt::compute_query_response_instantiation_values(infcx, orig_values, &state);
 
-        let inspect::State { var_values, data } = state.instantiate(infcx.tcx, &instantiation);
+    let inspect::State { var_values, data } = state.instantiate(infcx.tcx, &instantiation);
 
-        EvalCtxt::unify_query_var_values(infcx, param_env, original_values, var_values);
-        data
-    }
+    EvalCtxt::unify_query_var_values(infcx, param_env, orig_values, var_values);
+    data
 }
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 f914e6b3f2e..21efce74879 100644
--- a/compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs
+++ b/compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs
@@ -34,7 +34,7 @@ use super::{search_graph::SearchGraph, Goal};
 use super::{GoalSource, SolverMode};
 pub use select::InferCtxtSelectExt;
 
-mod canonical;
+pub(super) mod canonical;
 mod probe;
 mod select;
 
@@ -84,7 +84,7 @@ pub struct EvalCtxt<'a, 'tcx> {
 
     pub(super) search_graph: &'a mut SearchGraph<'tcx>,
 
-    pub(super) nested_goals: NestedGoals<'tcx>,
+    nested_goals: NestedGoals<'tcx>,
 
     // Has this `EvalCtxt` errored out with `NoSolution` in `try_evaluate_added_goals`?
     //
@@ -161,7 +161,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
     /// Creates a root evaluation context and search graph. This should only be
     /// used from outside of any evaluation, and other methods should be preferred
     /// over using this manually (such as [`InferCtxtEvalExt::evaluate_root_goal`]).
-    fn enter_root<R>(
+    pub(super) fn enter_root<R>(
         infcx: &InferCtxt<'tcx>,
         generate_proof_tree: GenerateProofTree,
         f: impl FnOnce(&mut EvalCtxt<'_, 'tcx>) -> R,
@@ -242,7 +242,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
             search_graph,
             nested_goals: NestedGoals::new(),
             tainted: Ok(()),
-            inspect: canonical_goal_evaluation.new_goal_evaluation_step(input),
+            inspect: canonical_goal_evaluation.new_goal_evaluation_step(var_values, input),
         };
 
         for &(key, ty) in &input.predefined_opaques_in_body.opaque_types {
@@ -255,7 +255,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
         }
 
         let result = f(&mut ecx, input.goal);
-
+        ecx.inspect.probe_final_state(ecx.infcx, ecx.max_input_universe);
         canonical_goal_evaluation.goal_evaluation_step(ecx.inspect);
 
         // When creating a query response we clone the opaque type constraints
@@ -338,7 +338,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
     /// storage.
     // FIXME(-Znext-solver=coinduction): `_source` is currently unused but will
     // be necessary once we implement the new coinduction approach.
-    fn evaluate_goal_raw(
+    pub(super) fn evaluate_goal_raw(
         &mut self,
         goal_evaluation_kind: GoalEvaluationKind,
         _source: GoalSource,
@@ -458,13 +458,23 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
         }
     }
 
+    #[instrument(level = "debug", skip(self))]
+    pub(super) fn add_normalizes_to_goal(&mut self, goal: Goal<'tcx, ty::NormalizesTo<'tcx>>) {
+        self.inspect.add_normalizes_to_goal(self.infcx, self.max_input_universe, goal);
+        self.nested_goals.normalizes_to_goals.push(goal);
+    }
+
+    #[instrument(level = "debug", skip(self))]
+    pub(super) fn add_goal(&mut self, source: GoalSource, goal: Goal<'tcx, ty::Predicate<'tcx>>) {
+        self.inspect.add_goal(self.infcx, self.max_input_universe, source, goal);
+        self.nested_goals.goals.push((source, goal));
+    }
+
     // Recursively evaluates all the goals added to this `EvalCtxt` to completion, returning
     // the certainty of all the goals.
     #[instrument(level = "debug", skip(self))]
     pub(super) fn try_evaluate_added_goals(&mut self) -> Result<Certainty, NoSolution> {
-        let inspect = self.inspect.new_evaluate_added_goals();
-        let inspect = core::mem::replace(&mut self.inspect, inspect);
-
+        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
@@ -482,15 +492,12 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
             }
         }
 
-        self.inspect.eval_added_goals_result(response);
+        self.inspect.evaluate_added_goals_result(response);
 
         if response.is_err() {
             self.tainted = Err(NoSolution);
         }
 
-        let goal_evaluations = std::mem::replace(&mut self.inspect, inspect);
-        self.inspect.added_goals_evaluation(goal_evaluations);
-
         response
     }
 
@@ -499,10 +506,9 @@ impl<'a, 'tcx> EvalCtxt<'a, '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);
 
-        self.inspect.evaluate_added_goals_loop_start();
-
         // If this loop did not result in any progress, what's our final certainty.
         let mut unchanged_certainty = Some(Certainty::Yes);
         for goal in goals.normalizes_to_goals {
@@ -586,17 +592,23 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
         self.infcx.tcx
     }
 
-    pub(super) fn next_ty_infer(&self) -> Ty<'tcx> {
-        self.infcx.next_ty_var(TypeVariableOrigin { param_def_id: None, span: DUMMY_SP })
+    pub(super) fn next_ty_infer(&mut self) -> Ty<'tcx> {
+        let ty = self.infcx.next_ty_var(TypeVariableOrigin { param_def_id: None, span: DUMMY_SP });
+        self.inspect.add_var_value(ty);
+        ty
     }
 
-    pub(super) fn next_const_infer(&self, ty: Ty<'tcx>) -> ty::Const<'tcx> {
-        self.infcx.next_const_var(ty, ConstVariableOrigin { param_def_id: None, span: DUMMY_SP })
+    pub(super) fn next_const_infer(&mut self, ty: Ty<'tcx>) -> ty::Const<'tcx> {
+        let ct = self
+            .infcx
+            .next_const_var(ty, ConstVariableOrigin { param_def_id: None, span: DUMMY_SP });
+        self.inspect.add_var_value(ct);
+        ct
     }
 
     /// Returns a ty infer or a const infer depending on whether `kind` is a `Ty` or `Const`.
     /// If `kind` is an integer inference variable this will still return a ty infer var.
-    pub(super) fn next_term_infer_of_kind(&self, kind: ty::Term<'tcx>) -> ty::Term<'tcx> {
+    pub(super) fn next_term_infer_of_kind(&mut self, kind: ty::Term<'tcx>) -> ty::Term<'tcx> {
         match kind.unpack() {
             ty::TermKind::Ty(_) => self.next_ty_infer().into(),
             ty::TermKind::Const(ct) => self.next_const_infer(ct.ty()).into(),
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 5b1124e8b9f..9d59723e441 100644
--- a/compiler/rustc_trait_selection/src/solve/eval_ctxt/probe.rs
+++ b/compiler/rustc_trait_selection/src/solve/eval_ctxt/probe.rs
@@ -20,23 +20,29 @@ where
     pub(in crate::solve) fn enter(self, f: impl FnOnce(&mut EvalCtxt<'_, 'tcx>) -> T) -> T {
         let ProbeCtxt { ecx: outer_ecx, probe_kind, _result } = self;
 
+        let infcx = outer_ecx.infcx;
+        let max_input_universe = outer_ecx.max_input_universe;
         let mut nested_ecx = EvalCtxt {
-            infcx: outer_ecx.infcx,
+            infcx,
             variables: outer_ecx.variables,
             var_values: outer_ecx.var_values,
             is_normalizes_to_goal: outer_ecx.is_normalizes_to_goal,
             predefined_opaques_in_body: outer_ecx.predefined_opaques_in_body,
-            max_input_universe: outer_ecx.max_input_universe,
+            max_input_universe,
             search_graph: outer_ecx.search_graph,
             nested_goals: outer_ecx.nested_goals.clone(),
             tainted: outer_ecx.tainted,
-            inspect: outer_ecx.inspect.new_probe(),
+            inspect: outer_ecx.inspect.take_and_enter_probe(),
         };
-        let r = nested_ecx.infcx.probe(|_| f(&mut nested_ecx));
-        if !outer_ecx.inspect.is_noop() {
+        let r = nested_ecx.infcx.probe(|_| {
+            let r = f(&mut nested_ecx);
+            nested_ecx.inspect.probe_final_state(infcx, max_input_universe);
+            r
+        });
+        if !nested_ecx.inspect.is_noop() {
             let probe_kind = probe_kind(&r);
             nested_ecx.inspect.probe_kind(probe_kind);
-            outer_ecx.inspect.finish_probe(nested_ecx.inspect);
+            outer_ecx.inspect = nested_ecx.inspect.finish_probe();
         }
         r
     }
diff --git a/compiler/rustc_trait_selection/src/solve/inspect/analyse.rs b/compiler/rustc_trait_selection/src/solve/inspect/analyse.rs
index 56c32d3d539..dbded4cbd37 100644
--- a/compiler/rustc_trait_selection/src/solve/inspect/analyse.rs
+++ b/compiler/rustc_trait_selection/src/solve/inspect/analyse.rs
@@ -11,15 +11,24 @@
 
 use rustc_ast_ir::try_visit;
 use rustc_ast_ir::visit::VisitorResult;
-use rustc_infer::infer::InferCtxt;
+use rustc_infer::infer::type_variable::TypeVariableOrigin;
+use rustc_infer::infer::{DefineOpaqueTypes, InferCtxt, InferOk};
+use rustc_middle::infer::unify_key::ConstVariableOrigin;
 use rustc_middle::traits::query::NoSolution;
 use rustc_middle::traits::solve::{inspect, QueryResult};
 use rustc_middle::traits::solve::{Certainty, Goal};
+use rustc_middle::traits::ObligationCause;
 use rustc_middle::ty;
+use rustc_span::Span;
 
-use crate::solve::inspect::ProofTreeBuilder;
+use crate::solve::eval_ctxt::canonical;
+use crate::solve::{EvalCtxt, GoalEvaluationKind, GoalSource};
 use crate::solve::{GenerateProofTree, InferCtxtEvalExt};
 
+pub struct InspectConfig {
+    pub max_depth: usize,
+}
+
 pub struct InspectGoal<'a, 'tcx> {
     infcx: &'a InferCtxt<'tcx>,
     depth: usize,
@@ -32,14 +41,11 @@ pub struct InspectCandidate<'a, 'tcx> {
     goal: &'a InspectGoal<'a, 'tcx>,
     kind: inspect::ProbeKind<'tcx>,
     nested_goals: Vec<inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>>,
+    final_state: inspect::CanonicalState<'tcx, ()>,
     result: QueryResult<'tcx>,
 }
 
 impl<'a, 'tcx> InspectCandidate<'a, 'tcx> {
-    pub fn infcx(&self) -> &'a InferCtxt<'tcx> {
-        self.goal.infcx
-    }
-
     pub fn kind(&self) -> inspect::ProbeKind<'tcx> {
         self.kind
     }
@@ -48,55 +54,88 @@ impl<'a, 'tcx> InspectCandidate<'a, 'tcx> {
         self.result.map(|c| c.value.certainty)
     }
 
-    /// Visit the nested goals of this candidate.
-    ///
-    /// FIXME(@lcnr): we have to slightly adapt this API
-    /// to also use it to compute the most relevant goal
-    /// for fulfillment errors. Will do that once we actually
-    /// need it.
-    pub fn visit_nested<V: ProofTreeVisitor<'tcx>>(&self, visitor: &mut V) -> V::Result {
-        // HACK: An arbitrary cutoff to avoid dealing with overflow and cycles.
-        if self.goal.depth <= 10 {
+    /// Visit all nested goals of this candidate without rolling
+    /// back their inference constraints. This function modifies
+    /// the state of the `infcx`.
+    pub fn visit_nested_no_probe<V: ProofTreeVisitor<'tcx>>(&self, visitor: &mut V) -> V::Result {
+        if self.goal.depth < visitor.config().max_depth {
             let infcx = self.goal.infcx;
-            infcx.probe(|_| {
-                let mut instantiated_goals = vec![];
-                for goal in &self.nested_goals {
-                    let goal = ProofTreeBuilder::instantiate_canonical_state(
-                        infcx,
-                        self.goal.goal.param_env,
-                        self.goal.orig_values,
-                        *goal,
-                    );
-                    instantiated_goals.push(goal);
-                }
+            let param_env = self.goal.goal.param_env;
+            let mut orig_values = self.goal.orig_values.to_vec();
+            let mut instantiated_goals = vec![];
+            for goal in &self.nested_goals {
+                let goal = canonical::instantiate_canonical_state(
+                    infcx,
+                    visitor.span(),
+                    param_env,
+                    &mut orig_values,
+                    *goal,
+                );
+                instantiated_goals.push(goal);
+            }
 
-                for goal in instantiated_goals.iter().copied() {
-                    // We need to be careful with `NormalizesTo` goals as the
-                    // expected term has to be replaced with an unconstrained
-                    // inference variable.
-                    if let Some(kind) = goal.predicate.kind().no_bound_vars()
-                        && let ty::PredicateKind::NormalizesTo(predicate) = kind
-                        && !predicate.alias.is_opaque(infcx.tcx)
-                    {
-                        // FIXME: We currently skip these goals as
-                        // `fn evaluate_root_goal` ICEs if there are any
-                        // `NestedNormalizationGoals`.
-                        continue;
-                    };
-                    let (_, proof_tree) = infcx.evaluate_root_goal(goal, GenerateProofTree::Yes);
-                    let proof_tree = proof_tree.unwrap();
-                    try_visit!(visitor.visit_goal(&InspectGoal::new(
-                        infcx,
-                        self.goal.depth + 1,
-                        &proof_tree,
-                    )));
-                }
+            let () = canonical::instantiate_canonical_state(
+                infcx,
+                visitor.span(),
+                param_env,
+                &mut orig_values,
+                self.final_state,
+            );
 
-                V::Result::output()
-            })
-        } else {
-            V::Result::output()
+            for &goal in &instantiated_goals {
+                let proof_tree = match goal.predicate.kind().no_bound_vars() {
+                    Some(ty::PredicateKind::NormalizesTo(ty::NormalizesTo { alias, term })) => {
+                        let unconstrained_term = match term.unpack() {
+                            ty::TermKind::Ty(_) => infcx
+                                .next_ty_var(TypeVariableOrigin {
+                                    param_def_id: None,
+                                    span: visitor.span(),
+                                })
+                                .into(),
+                            ty::TermKind::Const(ct) => infcx
+                                .next_const_var(
+                                    ct.ty(),
+                                    ConstVariableOrigin {
+                                        param_def_id: None,
+                                        span: visitor.span(),
+                                    },
+                                )
+                                .into(),
+                        };
+                        let goal = goal
+                            .with(infcx.tcx, ty::NormalizesTo { alias, term: unconstrained_term });
+                        let proof_tree =
+                            EvalCtxt::enter_root(infcx, GenerateProofTree::Yes, |ecx| {
+                                ecx.evaluate_goal_raw(
+                                    GoalEvaluationKind::Root,
+                                    GoalSource::Misc,
+                                    goal,
+                                )
+                            })
+                            .1;
+                        let InferOk { value: (), obligations: _ } = infcx
+                            .at(&ObligationCause::dummy(), param_env)
+                            .eq(DefineOpaqueTypes::Yes, term, unconstrained_term)
+                            .unwrap();
+                        proof_tree
+                    }
+                    _ => infcx.evaluate_root_goal(goal, GenerateProofTree::Yes).1,
+                };
+                try_visit!(visitor.visit_goal(&InspectGoal::new(
+                    infcx,
+                    self.goal.depth + 1,
+                    &proof_tree.unwrap(),
+                )));
+            }
         }
+
+        V::Result::output()
+    }
+
+    /// Visit all nested goals of this candidate, rolling back
+    /// all inference constraints.
+    pub fn visit_nested_in_probe<V: ProofTreeVisitor<'tcx>>(&self, visitor: &mut V) -> V::Result {
+        self.goal.infcx.probe(|_| self.visit_nested_no_probe(visitor))
     }
 }
 
@@ -119,6 +158,7 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
         nested_goals: &mut Vec<inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>>,
         probe: &inspect::Probe<'tcx>,
     ) {
+        let num_candidates = candidates.len();
         for step in &probe.steps {
             match step {
                 &inspect::ProbeStep::AddGoal(_source, goal) => nested_goals.push(goal),
@@ -144,23 +184,25 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
             // FIXME: This is currently wrong if we don't even try any
             // candidates, e.g. for a trait goal, as in this case `candidates` is
             // actually supposed to be empty.
-            inspect::ProbeKind::Root { result } => {
-                if candidates.is_empty() {
+            inspect::ProbeKind::Root { result }
+            | inspect::ProbeKind::TryNormalizeNonRigid { result } => {
+                if candidates.len() == num_candidates {
                     candidates.push(InspectCandidate {
                         goal: self,
                         kind: probe.kind,
                         nested_goals: nested_goals.clone(),
+                        final_state: probe.final_state,
                         result,
-                    });
+                    })
                 }
             }
-            inspect::ProbeKind::TryNormalizeNonRigid { result }
-            | inspect::ProbeKind::MiscCandidate { name: _, result }
+            inspect::ProbeKind::MiscCandidate { name: _, result }
             | inspect::ProbeKind::TraitCandidate { source: _, result } => {
                 candidates.push(InspectCandidate {
                     goal: self,
                     kind: probe.kind,
                     nested_goals: nested_goals.clone(),
+                    final_state: probe.final_state,
                     result,
                 });
             }
@@ -191,6 +233,17 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
         candidates
     }
 
+    /// Returns the single candidate applicable for the current goal, if it exists.
+    ///
+    /// Returns `None` if there are either no or multiple applicable candidates.
+    pub fn unique_applicable_candidate(&'a self) -> Option<InspectCandidate<'a, 'tcx>> {
+        // FIXME(-Znext-solver): This does not handle impl candidates
+        // hidden by env candidates.
+        let mut candidates = self.candidates();
+        candidates.retain(|c| c.result().is_ok());
+        candidates.pop().filter(|_| candidates.is_empty())
+    }
+
     fn new(
         infcx: &'a InferCtxt<'tcx>,
         depth: usize,
@@ -213,6 +266,12 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
 pub trait ProofTreeVisitor<'tcx> {
     type Result: VisitorResult = ();
 
+    fn span(&self) -> Span;
+
+    fn config(&self) -> InspectConfig {
+        InspectConfig { max_depth: 10 }
+    }
+
     fn visit_goal(&mut self, goal: &InspectGoal<'_, 'tcx>) -> Self::Result;
 }
 
@@ -223,10 +282,8 @@ impl<'tcx> InferCtxt<'tcx> {
         goal: Goal<'tcx, ty::Predicate<'tcx>>,
         visitor: &mut V,
     ) -> V::Result {
-        self.probe(|_| {
-            let (_, proof_tree) = self.evaluate_root_goal(goal, GenerateProofTree::Yes);
-            let proof_tree = proof_tree.unwrap();
-            visitor.visit_goal(&InspectGoal::new(self, 0, &proof_tree))
-        })
+        let (_, proof_tree) = self.evaluate_root_goal(goal, GenerateProofTree::Yes);
+        let proof_tree = proof_tree.unwrap();
+        visitor.visit_goal(&InspectGoal::new(self, 0, &proof_tree))
     }
 }
diff --git a/compiler/rustc_trait_selection/src/solve/inspect/build.rs b/compiler/rustc_trait_selection/src/solve/inspect/build.rs
index 43c76cc5f4a..c3651517d49 100644
--- a/compiler/rustc_trait_selection/src/solve/inspect/build.rs
+++ b/compiler/rustc_trait_selection/src/solve/inspect/build.rs
@@ -5,6 +5,8 @@
 //! see the comment on [ProofTreeBuilder].
 use std::mem;
 
+use rustc_infer::infer::InferCtxt;
+use rustc_middle::infer::canonical::CanonicalVarValues;
 use rustc_middle::traits::query::NoSolution;
 use rustc_middle::traits::solve::{
     CanonicalInput, Certainty, Goal, GoalSource, QueryInput, QueryResult,
@@ -12,7 +14,8 @@ use rustc_middle::traits::solve::{
 use rustc_middle::ty::{self, TyCtxt};
 use rustc_session::config::DumpSolverProofTree;
 
-use crate::solve::{self, inspect, EvalCtxt, GenerateProofTree};
+use crate::solve::eval_ctxt::canonical;
+use crate::solve::{self, inspect, GenerateProofTree};
 
 /// The core data structure when building proof trees.
 ///
@@ -47,9 +50,7 @@ enum DebugSolver<'tcx> {
     Root,
     GoalEvaluation(WipGoalEvaluation<'tcx>),
     CanonicalGoalEvaluation(WipCanonicalGoalEvaluation<'tcx>),
-    AddedGoalsEvaluation(WipAddedGoalsEvaluation<'tcx>),
     GoalEvaluationStep(WipGoalEvaluationStep<'tcx>),
-    Probe(WipProbe<'tcx>),
 }
 
 impl<'tcx> From<WipGoalEvaluation<'tcx>> for DebugSolver<'tcx> {
@@ -64,24 +65,12 @@ impl<'tcx> From<WipCanonicalGoalEvaluation<'tcx>> for DebugSolver<'tcx> {
     }
 }
 
-impl<'tcx> From<WipAddedGoalsEvaluation<'tcx>> for DebugSolver<'tcx> {
-    fn from(g: WipAddedGoalsEvaluation<'tcx>) -> DebugSolver<'tcx> {
-        DebugSolver::AddedGoalsEvaluation(g)
-    }
-}
-
 impl<'tcx> From<WipGoalEvaluationStep<'tcx>> for DebugSolver<'tcx> {
     fn from(g: WipGoalEvaluationStep<'tcx>) -> DebugSolver<'tcx> {
         DebugSolver::GoalEvaluationStep(g)
     }
 }
 
-impl<'tcx> From<WipProbe<'tcx>> for DebugSolver<'tcx> {
-    fn from(p: WipProbe<'tcx>) -> DebugSolver<'tcx> {
-        DebugSolver::Probe(p)
-    }
-}
-
 #[derive(Eq, PartialEq, Debug)]
 struct WipGoalEvaluation<'tcx> {
     pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
@@ -184,12 +173,41 @@ impl<'tcx> WipAddedGoalsEvaluation<'tcx> {
 
 #[derive(Eq, PartialEq, Debug)]
 struct WipGoalEvaluationStep<'tcx> {
+    /// Unlike `EvalCtxt::var_values`, we append a new
+    /// generic arg here whenever we create a new inference
+    /// variable.
+    ///
+    /// This is necessary as we otherwise don't unify these
+    /// vars when instantiating multiple `CanonicalState`.
+    var_values: Vec<ty::GenericArg<'tcx>>,
     instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
-
+    probe_depth: usize,
     evaluation: WipProbe<'tcx>,
 }
 
 impl<'tcx> WipGoalEvaluationStep<'tcx> {
+    fn current_evaluation_scope(&mut self) -> &mut WipProbe<'tcx> {
+        let mut current = &mut self.evaluation;
+        for _ in 0..self.probe_depth {
+            match current.steps.last_mut() {
+                Some(WipProbeStep::NestedProbe(p)) => current = p,
+                _ => bug!(),
+            }
+        }
+        current
+    }
+
+    fn added_goals_evaluation(&mut self) -> &mut WipAddedGoalsEvaluation<'tcx> {
+        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<'tcx> {
         let evaluation = self.evaluation.finalize();
         match evaluation.kind {
@@ -202,8 +220,10 @@ impl<'tcx> WipGoalEvaluationStep<'tcx> {
 
 #[derive(Eq, PartialEq, Debug)]
 struct WipProbe<'tcx> {
-    pub steps: Vec<WipProbeStep<'tcx>>,
-    pub kind: Option<inspect::ProbeKind<'tcx>>,
+    initial_num_var_values: usize,
+    steps: Vec<WipProbeStep<'tcx>>,
+    kind: Option<inspect::ProbeKind<'tcx>>,
+    final_state: Option<inspect::CanonicalState<'tcx, ()>>,
 }
 
 impl<'tcx> WipProbe<'tcx> {
@@ -211,6 +231,7 @@ impl<'tcx> WipProbe<'tcx> {
         inspect::Probe {
             steps: self.steps.into_iter().map(WipProbeStep::finalize).collect(),
             kind: self.kind.unwrap(),
+            final_state: self.final_state.unwrap(),
         }
     }
 }
@@ -245,6 +266,12 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
         self.state.as_deref_mut()
     }
 
+    pub fn take_and_enter_probe(&mut self) -> ProofTreeBuilder<'tcx> {
+        let mut nested = ProofTreeBuilder { state: self.state.take() };
+        nested.enter_probe();
+        nested
+    }
+
     pub fn finalize(self) -> Option<inspect::GoalEvaluation<'tcx>> {
         match *self.state? {
             DebugSolver::GoalEvaluation(wip_goal_evaluation) => {
@@ -362,11 +389,14 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
         if let Some(this) = self.as_mut() {
             match (this, *goal_evaluation.state.unwrap()) {
                 (
-                    DebugSolver::AddedGoalsEvaluation(WipAddedGoalsEvaluation {
-                        evaluations, ..
-                    }),
+                    DebugSolver::GoalEvaluationStep(state),
                     DebugSolver::GoalEvaluation(goal_evaluation),
-                ) => evaluations.last_mut().unwrap().push(goal_evaluation),
+                ) => state
+                    .added_goals_evaluation()
+                    .evaluations
+                    .last_mut()
+                    .unwrap()
+                    .push(goal_evaluation),
                 (this @ DebugSolver::Root, goal_evaluation) => *this = goal_evaluation,
                 _ => unreachable!(),
             }
@@ -375,13 +405,22 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
 
     pub fn new_goal_evaluation_step(
         &mut self,
+        var_values: CanonicalVarValues<'tcx>,
         instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
     ) -> ProofTreeBuilder<'tcx> {
         self.nested(|| WipGoalEvaluationStep {
+            var_values: var_values.var_values.to_vec(),
             instantiated_goal,
-            evaluation: WipProbe { steps: vec![], kind: None },
+            evaluation: WipProbe {
+                initial_num_var_values: var_values.len(),
+                steps: vec![],
+                kind: None,
+                final_state: None,
+            },
+            probe_depth: 0,
         })
     }
+
     pub fn goal_evaluation_step(&mut self, goal_evaluation_step: ProofTreeBuilder<'tcx>) {
         if let Some(this) = self.as_mut() {
             match (this, *goal_evaluation_step.state.unwrap()) {
@@ -396,112 +435,146 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
         }
     }
 
-    pub fn new_probe(&mut self) -> ProofTreeBuilder<'tcx> {
-        self.nested(|| WipProbe { steps: vec![], kind: None })
+    pub fn add_var_value<T: Into<ty::GenericArg<'tcx>>>(&mut self, arg: T) {
+        match self.as_mut() {
+            None => {}
+            Some(DebugSolver::GoalEvaluationStep(state)) => {
+                state.var_values.push(arg.into());
+            }
+            Some(s) => bug!("tried to add var values to {s:?}"),
+        }
+    }
+
+    pub fn enter_probe(&mut self) {
+        match self.as_mut() {
+            None => {}
+            Some(DebugSolver::GoalEvaluationStep(state)) => {
+                let initial_num_var_values = state.var_values.len();
+                state.current_evaluation_scope().steps.push(WipProbeStep::NestedProbe(WipProbe {
+                    initial_num_var_values,
+                    steps: vec![],
+                    kind: None,
+                    final_state: None,
+                }));
+                state.probe_depth += 1;
+            }
+            Some(s) => bug!("tried to start probe to {s:?}"),
+        }
     }
 
     pub fn probe_kind(&mut self, probe_kind: inspect::ProbeKind<'tcx>) {
-        if let Some(this) = self.as_mut() {
-            match this {
-                DebugSolver::Probe(this) => {
-                    assert_eq!(this.kind.replace(probe_kind), None)
-                }
-                _ => unreachable!(),
+        match self.as_mut() {
+            None => {}
+            Some(DebugSolver::GoalEvaluationStep(state)) => {
+                let prev = state.current_evaluation_scope().kind.replace(probe_kind);
+                assert_eq!(prev, None);
             }
+            _ => bug!(),
         }
     }
 
-    pub fn add_normalizes_to_goal(
-        ecx: &mut EvalCtxt<'_, 'tcx>,
-        goal: Goal<'tcx, ty::NormalizesTo<'tcx>>,
+    pub fn probe_final_state(
+        &mut self,
+        infcx: &InferCtxt<'tcx>,
+        max_input_universe: ty::UniverseIndex,
     ) {
-        if ecx.inspect.is_noop() {
-            return;
+        match self.as_mut() {
+            None => {}
+            Some(DebugSolver::GoalEvaluationStep(state)) => {
+                let final_state = canonical::make_canonical_state(
+                    infcx,
+                    &state.var_values,
+                    max_input_universe,
+                    (),
+                );
+                let prev = state.current_evaluation_scope().final_state.replace(final_state);
+                assert_eq!(prev, None);
+            }
+            _ => bug!(),
         }
+    }
 
-        Self::add_goal(ecx, GoalSource::Misc, goal.with(ecx.tcx(), goal.predicate));
+    pub fn add_normalizes_to_goal(
+        &mut self,
+        infcx: &InferCtxt<'tcx>,
+        max_input_universe: ty::UniverseIndex,
+        goal: Goal<'tcx, ty::NormalizesTo<'tcx>>,
+    ) {
+        self.add_goal(
+            infcx,
+            max_input_universe,
+            GoalSource::Misc,
+            goal.with(infcx.tcx, goal.predicate),
+        );
     }
 
     pub fn add_goal(
-        ecx: &mut EvalCtxt<'_, 'tcx>,
+        &mut self,
+        infcx: &InferCtxt<'tcx>,
+        max_input_universe: ty::UniverseIndex,
         source: GoalSource,
         goal: Goal<'tcx, ty::Predicate<'tcx>>,
     ) {
-        // Can't use `if let Some(this) = ecx.inspect.as_mut()` here because
-        // we have to immutably use the `EvalCtxt` for `make_canonical_state`.
-        if ecx.inspect.is_noop() {
-            return;
-        }
-
-        let goal = Self::make_canonical_state(ecx, goal);
-
-        match ecx.inspect.as_mut().unwrap() {
-            DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
-                evaluation: WipProbe { steps, .. },
-                ..
-            })
-            | DebugSolver::Probe(WipProbe { steps, .. }) => {
-                steps.push(WipProbeStep::AddGoal(source, goal))
+        match self.as_mut() {
+            None => {}
+            Some(DebugSolver::GoalEvaluationStep(state)) => {
+                let goal = canonical::make_canonical_state(
+                    infcx,
+                    &state.var_values,
+                    max_input_universe,
+                    goal,
+                );
+                state.current_evaluation_scope().steps.push(WipProbeStep::AddGoal(source, goal))
             }
-            s => unreachable!("tried to add {goal:?} to {s:?}"),
+            _ => bug!(),
         }
     }
 
-    pub fn finish_probe(&mut self, probe: ProofTreeBuilder<'tcx>) {
-        if let Some(this) = self.as_mut() {
-            match (this, *probe.state.unwrap()) {
-                (
-                    DebugSolver::Probe(WipProbe { steps, .. })
-                    | DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
-                        evaluation: WipProbe { steps, .. },
-                        ..
-                    }),
-                    DebugSolver::Probe(probe),
-                ) => steps.push(WipProbeStep::NestedProbe(probe)),
-                _ => unreachable!(),
+    pub fn finish_probe(mut self) -> ProofTreeBuilder<'tcx> {
+        match self.as_mut() {
+            None => {}
+            Some(DebugSolver::GoalEvaluationStep(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);
+                state.probe_depth -= 1;
             }
+            _ => bug!(),
         }
-    }
 
-    pub fn new_evaluate_added_goals(&mut self) -> ProofTreeBuilder<'tcx> {
-        self.nested(|| WipAddedGoalsEvaluation { evaluations: vec![], result: None })
+        self
     }
 
-    pub fn evaluate_added_goals_loop_start(&mut self) {
-        if let Some(this) = self.as_mut() {
-            match this {
-                DebugSolver::AddedGoalsEvaluation(this) => {
-                    this.evaluations.push(vec![]);
-                }
-                _ => unreachable!(),
+    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 eval_added_goals_result(&mut self, result: Result<Certainty, NoSolution>) {
-        if let Some(this) = self.as_mut() {
-            match this {
-                DebugSolver::AddedGoalsEvaluation(this) => {
-                    assert_eq!(this.result.replace(result), None);
-                }
-                _ => unreachable!(),
+    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 added_goals_evaluation(&mut self, added_goals_evaluation: ProofTreeBuilder<'tcx>) {
-        if let Some(this) = self.as_mut() {
-            match (this, *added_goals_evaluation.state.unwrap()) {
-                (
-                    DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
-                        evaluation: WipProbe { steps, .. },
-                        ..
-                    })
-                    | DebugSolver::Probe(WipProbe { steps, .. }),
-                    DebugSolver::AddedGoalsEvaluation(added_goals_evaluation),
-                ) => steps.push(WipProbeStep::EvaluateGoals(added_goals_evaluation)),
-                _ => unreachable!(),
+    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!(),
         }
     }
 
diff --git a/compiler/rustc_trait_selection/src/solve/mod.rs b/compiler/rustc_trait_selection/src/solve/mod.rs
index da5cd15a10d..e58babe3208 100644
--- a/compiler/rustc_trait_selection/src/solve/mod.rs
+++ b/compiler/rustc_trait_selection/src/solve/mod.rs
@@ -200,18 +200,6 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
 }
 
 impl<'tcx> EvalCtxt<'_, 'tcx> {
-    #[instrument(level = "debug", skip(self))]
-    fn add_normalizes_to_goal(&mut self, goal: Goal<'tcx, ty::NormalizesTo<'tcx>>) {
-        inspect::ProofTreeBuilder::add_normalizes_to_goal(self, goal);
-        self.nested_goals.normalizes_to_goals.push(goal);
-    }
-
-    #[instrument(level = "debug", skip(self))]
-    fn add_goal(&mut self, source: GoalSource, goal: Goal<'tcx, ty::Predicate<'tcx>>) {
-        inspect::ProofTreeBuilder::add_goal(self, source, goal);
-        self.nested_goals.goals.push((source, goal));
-    }
-
     #[instrument(level = "debug", skip(self, goals))]
     fn add_goals(
         &mut self,
diff --git a/compiler/rustc_trait_selection/src/traits/coherence.rs b/compiler/rustc_trait_selection/src/traits/coherence.rs
index 36028b51659..a4208cdc3c6 100644
--- a/compiler/rustc_trait_selection/src/traits/coherence.rs
+++ b/compiler/rustc_trait_selection/src/traits/coherence.rs
@@ -30,7 +30,7 @@ use rustc_middle::ty::fast_reject::{DeepRejectCtxt, TreatParams};
 use rustc_middle::ty::visit::{TypeVisitable, TypeVisitableExt};
 use rustc_middle::ty::{self, Ty, TyCtxt, TypeSuperVisitable, TypeVisitor};
 use rustc_span::symbol::sym;
-use rustc_span::DUMMY_SP;
+use rustc_span::{Span, DUMMY_SP};
 use std::fmt::Debug;
 use std::ops::ControlFlow;
 
@@ -1022,10 +1022,14 @@ struct AmbiguityCausesVisitor<'a, 'tcx> {
 }
 
 impl<'a, 'tcx> ProofTreeVisitor<'tcx> for AmbiguityCausesVisitor<'a, 'tcx> {
+    fn span(&self) -> Span {
+        DUMMY_SP
+    }
+
     fn visit_goal(&mut self, goal: &InspectGoal<'_, 'tcx>) {
         let infcx = goal.infcx();
         for cand in goal.candidates() {
-            cand.visit_nested(self);
+            cand.visit_nested_in_probe(self);
         }
         // When searching for intercrate ambiguity causes, we only need to look
         // at ambiguous goals, as for others the coherence unknowable candidate
@@ -1157,5 +1161,5 @@ fn search_ambiguity_causes<'tcx>(
     goal: Goal<'tcx, ty::Predicate<'tcx>>,
     causes: &mut FxIndexSet<IntercrateAmbiguityCause<'tcx>>,
 ) {
-    infcx.visit_proof_tree(goal, &mut AmbiguityCausesVisitor { causes });
+    infcx.probe(|_| infcx.visit_proof_tree(goal, &mut AmbiguityCausesVisitor { causes }));
 }