about summary refs log tree commit diff
path: root/compiler/rustc_trait_selection/src
diff options
context:
space:
mode:
authorbors <bors@rust-lang.org>2023-09-21 07:58:28 +0000
committerbors <bors@rust-lang.org>2023-09-21 07:58:28 +0000
commite4a361a48a59ead52b302aaa2e1d9d345264935a (patch)
treec7b1c39afdc5368b770522b72fb73cacf5956ddf /compiler/rustc_trait_selection/src
parent0a689c1be85d635bf61ffb7922ef9ce02587a3b1 (diff)
parent614760f612fa72ba9d6955c00624c592b884d28f (diff)
downloadrust-e4a361a48a59ead52b302aaa2e1d9d345264935a.tar.gz
rust-e4a361a48a59ead52b302aaa2e1d9d345264935a.zip
Auto merge of #115996 - lcnr:intercrate_ambiguity_causes-uwu, r=compiler-errors
implement `intercrate_ambiguity_causes` in the new solver

I added some comments but this is still somewhat of a mess. I think we should for the most part be able to treat all of this as a black box, so I can accept that this code isn't too great.

I also believe that some of the weirdness here is unavoidable, as proof trees - and their visitor - hide semantically relevant information, so they cannot perfectly represent the actual solver behavior.

There are some known bugs here when testing with `./x.py test tests/ui --bless -- --target-rustcflags -Ztrait-solver=next-coherence`. While I haven't diagnosed them all in detail I believe we are able to handle them all separately

- `structurally_normalize` currently does not normalize opaque types, resulting in divergence between the solver internal `trait_ref_is_knowable` and the one when computing intercrate ambiguity causes.
- we don't add an `intercrate_ambiguity_cause` for reserved impls
- we should `deeply_normalize` the trait ref before printing it, that requires a "best effort" version of `deeply_normalize`

r? `@compiler-errors`
Diffstat (limited to 'compiler/rustc_trait_selection/src')
-rw-r--r--compiler/rustc_trait_selection/src/solve/eval_ctxt.rs9
-rw-r--r--compiler/rustc_trait_selection/src/solve/eval_ctxt/canonical.rs97
-rw-r--r--compiler/rustc_trait_selection/src/solve/inspect/analyse.rs235
-rw-r--r--compiler/rustc_trait_selection/src/solve/inspect/build.rs (renamed from compiler/rustc_trait_selection/src/solve/inspect.rs)238
-rw-r--r--compiler/rustc_trait_selection/src/solve/inspect/mod.rs7
-rw-r--r--compiler/rustc_trait_selection/src/solve/mod.rs2
-rw-r--r--compiler/rustc_trait_selection/src/traits/coherence.rs220
-rw-r--r--compiler/rustc_trait_selection/src/traits/structural_normalize.rs12
8 files changed, 659 insertions, 161 deletions
diff --git a/compiler/rustc_trait_selection/src/solve/eval_ctxt.rs b/compiler/rustc_trait_selection/src/solve/eval_ctxt.rs
index 7941f64873b..066129d8e47 100644
--- a/compiler/rustc_trait_selection/src/solve/eval_ctxt.rs
+++ b/compiler/rustc_trait_selection/src/solve/eval_ctxt.rs
@@ -344,7 +344,8 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
         goal: Goal<'tcx, ty::Predicate<'tcx>>,
     ) -> Result<(bool, Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution> {
         let (orig_values, canonical_goal) = self.canonicalize_goal(goal);
-        let mut goal_evaluation = self.inspect.new_goal_evaluation(goal, goal_evaluation_kind);
+        let mut goal_evaluation =
+            self.inspect.new_goal_evaluation(goal, &orig_values, goal_evaluation_kind);
         let encountered_overflow = self.search_graph.encountered_overflow();
         let canonical_response = EvalCtxt::evaluate_canonical_goal(
             self.tcx(),
@@ -568,7 +569,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
                 GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::Yes },
                 unconstrained_goal,
             )?;
-            self.add_goals(instantiate_goals);
+            self.nested_goals.goals.extend(instantiate_goals);
 
             // Finally, equate the goal's RHS with the unconstrained var.
             // We put the nested goals from this into goals instead of
@@ -605,7 +606,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
                 GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::No },
                 goal,
             )?;
-            self.add_goals(instantiate_goals);
+            self.nested_goals.goals.extend(instantiate_goals);
             if has_changed {
                 unchanged_certainty = None;
             }
@@ -613,7 +614,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
             match certainty {
                 Certainty::Yes => {}
                 Certainty::Maybe(_) => {
-                    self.add_goal(goal);
+                    self.nested_goals.goals.push(goal);
                     unchanged_certainty = unchanged_certainty.map(|c| c.unify_with(certainty));
                 }
             }
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 790f9b840f2..b3f9218d761 100644
--- a/compiler/rustc_trait_selection/src/solve/eval_ctxt/canonical.rs
+++ b/compiler/rustc_trait_selection/src/solve/eval_ctxt/canonical.rs
@@ -10,17 +10,21 @@
 //! [c]: https://rustc-dev-guide.rust-lang.org/solve/canonicalization.html
 use super::{CanonicalInput, Certainty, EvalCtxt, Goal};
 use crate::solve::canonicalize::{CanonicalizeMode, Canonicalizer};
-use crate::solve::{response_no_constraints_raw, CanonicalResponse, QueryResult, Response};
+use crate::solve::{
+    inspect, response_no_constraints_raw, CanonicalResponse, QueryResult, Response,
+};
 use rustc_data_structures::fx::FxHashSet;
 use rustc_index::IndexVec;
 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::InferCtxt;
+use rustc_infer::infer::{DefineOpaqueTypes, InferCtxt, InferOk};
+use rustc_middle::infer::canonical::Canonical;
 use rustc_middle::traits::query::NoSolution;
 use rustc_middle::traits::solve::{
     ExternalConstraintsData, MaybeCause, PredefinedOpaquesData, QueryInput,
 };
+use rustc_middle::traits::ObligationCause;
 use rustc_middle::ty::{
     self, BoundVar, GenericArgKind, Ty, TyCtxt, TypeFoldable, TypeFolder, TypeSuperFoldable,
     TypeVisitableExt,
@@ -29,6 +33,22 @@ use rustc_span::DUMMY_SP;
 use std::iter;
 use std::ops::Deref;
 
+trait ResponseT<'tcx> {
+    fn var_values(&self) -> CanonicalVarValues<'tcx>;
+}
+
+impl<'tcx> ResponseT<'tcx> for Response<'tcx> {
+    fn var_values(&self) -> CanonicalVarValues<'tcx> {
+        self.var_values
+    }
+}
+
+impl<'tcx, T> ResponseT<'tcx> for inspect::State<'tcx, T> {
+    fn var_values(&self) -> CanonicalVarValues<'tcx> {
+        self.var_values
+    }
+}
+
 impl<'tcx> EvalCtxt<'_, 'tcx> {
     /// Canonicalizes the goal remembering the original values
     /// for each bound variable.
@@ -188,12 +208,14 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
         original_values: Vec<ty::GenericArg<'tcx>>,
         response: CanonicalResponse<'tcx>,
     ) -> Result<(Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution> {
-        let substitution = self.compute_query_response_substitution(&original_values, &response);
+        let substitution =
+            Self::compute_query_response_substitution(self.infcx, &original_values, &response);
 
         let Response { var_values, external_constraints, certainty } =
             response.substitute(self.tcx(), &substitution);
 
-        let nested_goals = self.unify_query_var_values(param_env, &original_values, var_values)?;
+        let nested_goals =
+            Self::unify_query_var_values(self.infcx, param_env, &original_values, var_values)?;
 
         let ExternalConstraintsData { region_constraints, opaque_types } =
             external_constraints.deref();
@@ -206,21 +228,21 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
     /// This returns the substitutions to instantiate the bound variables of
     /// the canonical response. This depends on the `original_values` for the
     /// bound variables.
-    fn compute_query_response_substitution(
-        &self,
+    fn compute_query_response_substitution<T: ResponseT<'tcx>>(
+        infcx: &InferCtxt<'tcx>,
         original_values: &[ty::GenericArg<'tcx>],
-        response: &CanonicalResponse<'tcx>,
+        response: &Canonical<'tcx, T>,
     ) -> CanonicalVarValues<'tcx> {
         // FIXME: Longterm canonical queries should deal with all placeholders
         // created inside of the query directly instead of returning them to the
         // caller.
-        let prev_universe = self.infcx.universe();
+        let prev_universe = infcx.universe();
         let universes_created_in_query = response.max_universe.index();
         for _ in 0..universes_created_in_query {
-            self.infcx.create_next_universe();
+            infcx.create_next_universe();
         }
 
-        let var_values = response.value.var_values;
+        let var_values = response.value.var_values();
         assert_eq!(original_values.len(), var_values.len());
 
         // If the query did not make progress with constraining inference variables,
@@ -254,13 +276,13 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
             }
         }
 
-        let var_values = self.tcx().mk_args_from_iter(response.variables.iter().enumerate().map(
+        let var_values = infcx.tcx.mk_args_from_iter(response.variables.iter().enumerate().map(
             |(index, info)| {
                 if info.universe() != ty::UniverseIndex::ROOT {
                     // A variable from inside a binder of the query. While ideally these shouldn't
                     // exist at all (see the FIXME at the start of this method), we have to deal with
                     // them for now.
-                    self.infcx.instantiate_canonical_var(DUMMY_SP, info, |idx| {
+                    infcx.instantiate_canonical_var(DUMMY_SP, info, |idx| {
                         ty::UniverseIndex::from(prev_universe.index() + idx.index())
                     })
                 } else if info.is_existential() {
@@ -274,7 +296,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
                     if let Some(v) = opt_values[BoundVar::from_usize(index)] {
                         v
                     } else {
-                        self.infcx.instantiate_canonical_var(DUMMY_SP, info, |_| prev_universe)
+                        infcx.instantiate_canonical_var(DUMMY_SP, info, |_| prev_universe)
                     }
                 } else {
                     // For placeholders which were already part of the input, we simply map this
@@ -287,9 +309,9 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
         CanonicalVarValues { var_values }
     }
 
-    #[instrument(level = "debug", skip(self, param_env), ret)]
+    #[instrument(level = "debug", skip(infcx, param_env), ret)]
     fn unify_query_var_values(
-        &self,
+        infcx: &InferCtxt<'tcx>,
         param_env: ty::ParamEnv<'tcx>,
         original_values: &[ty::GenericArg<'tcx>],
         var_values: CanonicalVarValues<'tcx>,
@@ -298,7 +320,18 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
 
         let mut nested_goals = vec![];
         for (&orig, response) in iter::zip(original_values, var_values.var_values) {
-            nested_goals.extend(self.eq_and_get_goals(param_env, orig, response)?);
+            nested_goals.extend(
+                infcx
+                    .at(&ObligationCause::dummy(), param_env)
+                    .eq(DefineOpaqueTypes::No, orig, response)
+                    .map(|InferOk { value: (), obligations }| {
+                        obligations.into_iter().map(|o| Goal::from(o))
+                    })
+                    .map_err(|e| {
+                        debug!(?e, "failed to equate");
+                        NoSolution
+                    })?,
+            );
         }
 
         Ok(nested_goals)
@@ -403,3 +436,35 @@ impl<'tcx> TypeFolder<TyCtxt<'tcx>> for EagerResolver<'_, '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 { infcx: ecx.infcx });
+        Canonicalizer::canonicalize(
+            ecx.infcx,
+            CanonicalizeMode::Response { max_input_universe: ecx.max_input_universe },
+            &mut vec![],
+            state,
+        )
+    }
+
+    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>,
+    ) -> Result<(Vec<Goal<'tcx, ty::Predicate<'tcx>>>, T), NoSolution> {
+        let substitution =
+            EvalCtxt::compute_query_response_substitution(infcx, original_values, &state);
+
+        let inspect::State { var_values, data } = state.substitute(infcx.tcx, &substitution);
+
+        let nested_goals =
+            EvalCtxt::unify_query_var_values(infcx, param_env, original_values, var_values)?;
+        Ok((nested_goals, data))
+    }
+}
diff --git a/compiler/rustc_trait_selection/src/solve/inspect/analyse.rs b/compiler/rustc_trait_selection/src/solve/inspect/analyse.rs
new file mode 100644
index 00000000000..15c8d9e5bcb
--- /dev/null
+++ b/compiler/rustc_trait_selection/src/solve/inspect/analyse.rs
@@ -0,0 +1,235 @@
+/// An infrastructure to mechanically analyse proof trees.
+///
+/// It is unavoidable that this representation is somewhat
+/// lossy as it should hide quite a few semantically relevant things,
+/// e.g. canonicalization and the order of nested goals.
+///
+/// @lcnr: However, a lot of the weirdness here is not strictly necessary
+/// and could be improved in the future. This is mostly good enough for
+/// coherence right now and was annoying to implement, so I am leaving it
+/// as is until we start using it for something else.
+use std::ops::ControlFlow;
+
+use rustc_infer::infer::InferCtxt;
+use rustc_middle::traits::query::NoSolution;
+use rustc_middle::traits::solve::{inspect, QueryResult};
+use rustc_middle::traits::solve::{Certainty, Goal};
+use rustc_middle::ty;
+
+use crate::solve::inspect::ProofTreeBuilder;
+use crate::solve::{GenerateProofTree, InferCtxtEvalExt, UseGlobalCache};
+
+pub struct InspectGoal<'a, 'tcx> {
+    infcx: &'a InferCtxt<'tcx>,
+    depth: usize,
+    orig_values: &'a [ty::GenericArg<'tcx>],
+    goal: Goal<'tcx, ty::Predicate<'tcx>>,
+    evaluation: &'a inspect::GoalEvaluation<'tcx>,
+}
+
+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>>>>,
+    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
+    }
+
+    pub fn result(&self) -> Result<Certainty, NoSolution> {
+        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,
+    ) -> ControlFlow<V::BreakTy> {
+        // HACK: An arbitrary cutoff to avoid dealing with overflow and cycles.
+        if self.goal.depth >= 10 {
+            let infcx = self.goal.infcx;
+            infcx.probe(|_| {
+                let mut instantiated_goals = vec![];
+                for goal in &self.nested_goals {
+                    let goal = match ProofTreeBuilder::instantiate_canonical_state(
+                        infcx,
+                        self.goal.goal.param_env,
+                        self.goal.orig_values,
+                        *goal,
+                    ) {
+                        Ok((_goals, goal)) => goal,
+                        Err(NoSolution) => {
+                            warn!(
+                                "unexpected failure when instantiating {:?}: {:?}",
+                                goal, self.nested_goals
+                            );
+                            return ControlFlow::Continue(());
+                        }
+                    };
+                    instantiated_goals.push(goal);
+                }
+
+                for &goal in &instantiated_goals {
+                    let (_, proof_tree) =
+                        infcx.evaluate_root_goal(goal, GenerateProofTree::Yes(UseGlobalCache::No));
+                    let proof_tree = proof_tree.unwrap();
+                    visitor.visit_goal(&InspectGoal::new(
+                        infcx,
+                        self.goal.depth + 1,
+                        &proof_tree,
+                    ))?;
+                }
+
+                ControlFlow::Continue(())
+            })?;
+        }
+        ControlFlow::Continue(())
+    }
+}
+
+impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
+    pub fn infcx(&self) -> &'a InferCtxt<'tcx> {
+        self.infcx
+    }
+
+    pub fn goal(&self) -> Goal<'tcx, ty::Predicate<'tcx>> {
+        self.goal
+    }
+
+    pub fn result(&self) -> Result<Certainty, NoSolution> {
+        self.evaluation.evaluation.result.map(|c| c.value.certainty)
+    }
+
+    fn candidates_recur(
+        &'a self,
+        candidates: &mut Vec<InspectCandidate<'a, 'tcx>>,
+        nested_goals: &mut Vec<inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>>,
+        probe: &inspect::Probe<'tcx>,
+    ) {
+        for step in &probe.steps {
+            match step {
+                &inspect::ProbeStep::AddGoal(goal) => nested_goals.push(goal),
+                inspect::ProbeStep::EvaluateGoals(_) => (),
+                inspect::ProbeStep::NestedProbe(ref probe) => {
+                    // Nested probes have to prove goals added in their parent
+                    // but do not leak them, so we truncate the added goals
+                    // afterwards.
+                    let num_goals = nested_goals.len();
+                    self.candidates_recur(candidates, nested_goals, probe);
+                    nested_goals.truncate(num_goals);
+                }
+            }
+        }
+
+        match probe.kind {
+            inspect::ProbeKind::NormalizedSelfTyAssembly
+            | inspect::ProbeKind::UnsizeAssembly
+            | inspect::ProbeKind::UpcastProjectionCompatibility => (),
+            // We add a candidate for the root evaluation if there
+            // is only one way to prove a given goal, e.g. for `WellFormed`.
+            //
+            // 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() {
+                    candidates.push(InspectCandidate {
+                        goal: self,
+                        kind: probe.kind,
+                        nested_goals: nested_goals.clone(),
+                        result,
+                    });
+                }
+            }
+            inspect::ProbeKind::MiscCandidate { name: _, result }
+            | inspect::ProbeKind::TraitCandidate { source: _, result } => {
+                candidates.push(InspectCandidate {
+                    goal: self,
+                    kind: probe.kind,
+                    nested_goals: nested_goals.clone(),
+                    result,
+                });
+            }
+        }
+    }
+
+    pub fn candidates(&'a self) -> Vec<InspectCandidate<'a, 'tcx>> {
+        let mut candidates = vec![];
+        let last_eval_step = match self.evaluation.evaluation.kind {
+            inspect::CanonicalGoalEvaluationKind::Overflow
+            | inspect::CanonicalGoalEvaluationKind::CacheHit(_) => {
+                warn!("unexpected root evaluation: {:?}", self.evaluation);
+                return vec![];
+            }
+            inspect::CanonicalGoalEvaluationKind::Uncached { ref revisions } => {
+                if let Some(last) = revisions.last() {
+                    last
+                } else {
+                    return vec![];
+                }
+            }
+        };
+
+        let mut nested_goals = vec![];
+        self.candidates_recur(&mut candidates, &mut nested_goals, &last_eval_step.evaluation);
+
+        candidates
+    }
+
+    fn new(
+        infcx: &'a InferCtxt<'tcx>,
+        depth: usize,
+        root: &'a inspect::GoalEvaluation<'tcx>,
+    ) -> Self {
+        match root.kind {
+            inspect::GoalEvaluationKind::Root { ref orig_values } => InspectGoal {
+                infcx,
+                depth,
+                orig_values,
+                goal: infcx.resolve_vars_if_possible(root.uncanonicalized_goal),
+                evaluation: root,
+            },
+            inspect::GoalEvaluationKind::Nested { .. } => unreachable!(),
+        }
+    }
+}
+
+/// The public API to interact with proof trees.
+pub trait ProofTreeVisitor<'tcx> {
+    type BreakTy;
+
+    fn visit_goal(&mut self, goal: &InspectGoal<'_, 'tcx>) -> ControlFlow<Self::BreakTy>;
+}
+
+pub trait ProofTreeInferCtxtExt<'tcx> {
+    fn visit_proof_tree<V: ProofTreeVisitor<'tcx>>(
+        &self,
+        goal: Goal<'tcx, ty::Predicate<'tcx>>,
+        visitor: &mut V,
+    ) -> ControlFlow<V::BreakTy>;
+}
+
+impl<'tcx> ProofTreeInferCtxtExt<'tcx> for InferCtxt<'tcx> {
+    fn visit_proof_tree<V: ProofTreeVisitor<'tcx>>(
+        &self,
+        goal: Goal<'tcx, ty::Predicate<'tcx>>,
+        visitor: &mut V,
+    ) -> ControlFlow<V::BreakTy> {
+        let (_, proof_tree) =
+            self.evaluate_root_goal(goal, GenerateProofTree::Yes(UseGlobalCache::No));
+        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.rs b/compiler/rustc_trait_selection/src/solve/inspect/build.rs
index 749bba33c9b..2eba98b02e9 100644
--- a/compiler/rustc_trait_selection/src/solve/inspect.rs
+++ b/compiler/rustc_trait_selection/src/solve/inspect/build.rs
@@ -1,28 +1,107 @@
+//! Building proof trees incrementally during trait solving.
+//!
+//! This code is *a bit* of a mess and can hopefully be
+//! mostly ignored. For a general overview of how it works,
+//! see the comment on [ProofTreeBuilder].
 use rustc_middle::traits::query::NoSolution;
-use rustc_middle::traits::solve::inspect::{self, CacheHit, ProbeKind};
 use rustc_middle::traits::solve::{
     CanonicalInput, Certainty, Goal, IsNormalizesToHack, QueryInput, QueryResult,
 };
 use rustc_middle::ty::{self, TyCtxt};
 use rustc_session::config::DumpSolverProofTree;
 
-use super::eval_ctxt::UseGlobalCache;
-use super::{GenerateProofTree, GoalEvaluationKind};
+use crate::solve::eval_ctxt::UseGlobalCache;
+use crate::solve::{self, inspect, EvalCtxt, GenerateProofTree};
+
+/// The core data structure when building proof trees.
+///
+/// In case the current evaluation does not generate a proof
+/// tree, `state` is simply `None` and we avoid any work.
+///
+/// The possible states of the solver are represented via
+/// variants of [DebugSolver]. For any nested computation we call
+/// `ProofTreeBuilder::new_nested_computation_kind` which
+/// creates a new `ProofTreeBuilder` to temporarily replace the
+/// current one. Once that nested computation is done,
+/// `ProofTreeBuilder::nested_computation_kind` is called
+/// to add the finished nested evaluation to the parent.
+///
+/// We provide additional information to the current state
+/// by calling methods such as `ProofTreeBuilder::probe_kind`.
+///
+/// The actual structure closely mirrors the finished proof
+/// trees. At the end of trait solving `ProofTreeBuilder::finalize`
+/// is called to recursively convert the whole structure to a
+/// finished proof tree.
+pub(in crate::solve) struct ProofTreeBuilder<'tcx> {
+    state: Option<Box<BuilderData<'tcx>>>,
+}
+
+struct BuilderData<'tcx> {
+    tree: DebugSolver<'tcx>,
+    use_global_cache: UseGlobalCache,
+}
+
+/// The current state of the proof tree builder, at most places
+/// in the code, only one or two variants are actually possible.
+///
+/// We simply ICE in case that assumption is broken.
+#[derive(Debug)]
+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> {
+    fn from(g: WipGoalEvaluation<'tcx>) -> DebugSolver<'tcx> {
+        DebugSolver::GoalEvaluation(g)
+    }
+}
+
+impl<'tcx> From<WipCanonicalGoalEvaluation<'tcx>> for DebugSolver<'tcx> {
+    fn from(g: WipCanonicalGoalEvaluation<'tcx>) -> DebugSolver<'tcx> {
+        DebugSolver::CanonicalGoalEvaluation(g)
+    }
+}
+
+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)]
-pub struct WipGoalEvaluation<'tcx> {
+struct WipGoalEvaluation<'tcx> {
     pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
-    pub kind: WipGoalEvaluationKind,
+    pub kind: WipGoalEvaluationKind<'tcx>,
     pub evaluation: Option<WipCanonicalGoalEvaluation<'tcx>>,
     pub returned_goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
 }
 
 impl<'tcx> WipGoalEvaluation<'tcx> {
-    pub fn finalize(self) -> inspect::GoalEvaluation<'tcx> {
+    fn finalize(self) -> inspect::GoalEvaluation<'tcx> {
         inspect::GoalEvaluation {
             uncanonicalized_goal: self.uncanonicalized_goal,
             kind: match self.kind {
-                WipGoalEvaluationKind::Root => inspect::GoalEvaluationKind::Root,
+                WipGoalEvaluationKind::Root { orig_values } => {
+                    inspect::GoalEvaluationKind::Root { orig_values }
+                }
                 WipGoalEvaluationKind::Nested { is_normalizes_to_hack } => {
                     inspect::GoalEvaluationKind::Nested { is_normalizes_to_hack }
                 }
@@ -34,27 +113,27 @@ impl<'tcx> WipGoalEvaluation<'tcx> {
 }
 
 #[derive(Eq, PartialEq, Debug)]
-pub enum WipGoalEvaluationKind {
-    Root,
+pub(in crate::solve) enum WipGoalEvaluationKind<'tcx> {
+    Root { orig_values: Vec<ty::GenericArg<'tcx>> },
     Nested { is_normalizes_to_hack: IsNormalizesToHack },
 }
 
 #[derive(Eq, PartialEq, Debug)]
-pub enum WipCanonicalGoalEvaluationKind {
+pub(in crate::solve) enum WipCanonicalGoalEvaluationKind {
     Overflow,
-    CacheHit(CacheHit),
+    CacheHit(inspect::CacheHit),
 }
 
 #[derive(Eq, PartialEq, Debug)]
-pub struct WipCanonicalGoalEvaluation<'tcx> {
-    pub goal: CanonicalInput<'tcx>,
-    pub kind: Option<WipCanonicalGoalEvaluationKind>,
-    pub revisions: Vec<WipGoalEvaluationStep<'tcx>>,
-    pub result: Option<QueryResult<'tcx>>,
+struct WipCanonicalGoalEvaluation<'tcx> {
+    goal: CanonicalInput<'tcx>,
+    kind: Option<WipCanonicalGoalEvaluationKind>,
+    revisions: Vec<WipGoalEvaluationStep<'tcx>>,
+    result: Option<QueryResult<'tcx>>,
 }
 
 impl<'tcx> WipCanonicalGoalEvaluation<'tcx> {
-    pub fn finalize(self) -> inspect::CanonicalGoalEvaluation<'tcx> {
+    fn finalize(self) -> inspect::CanonicalGoalEvaluation<'tcx> {
         let kind = match self.kind {
             Some(WipCanonicalGoalEvaluationKind::Overflow) => {
                 inspect::CanonicalGoalEvaluationKind::Overflow
@@ -76,13 +155,13 @@ impl<'tcx> WipCanonicalGoalEvaluation<'tcx> {
 }
 
 #[derive(Eq, PartialEq, Debug)]
-pub struct WipAddedGoalsEvaluation<'tcx> {
-    pub evaluations: Vec<Vec<WipGoalEvaluation<'tcx>>>,
-    pub result: Option<Result<Certainty, NoSolution>>,
+struct WipAddedGoalsEvaluation<'tcx> {
+    evaluations: Vec<Vec<WipGoalEvaluation<'tcx>>>,
+    result: Option<Result<Certainty, NoSolution>>,
 }
 
 impl<'tcx> WipAddedGoalsEvaluation<'tcx> {
-    pub fn finalize(self) -> inspect::AddedGoalsEvaluation<'tcx> {
+    fn finalize(self) -> inspect::AddedGoalsEvaluation<'tcx> {
         inspect::AddedGoalsEvaluation {
             evaluations: self
                 .evaluations
@@ -97,17 +176,17 @@ impl<'tcx> WipAddedGoalsEvaluation<'tcx> {
 }
 
 #[derive(Eq, PartialEq, Debug)]
-pub struct WipGoalEvaluationStep<'tcx> {
-    pub instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
+struct WipGoalEvaluationStep<'tcx> {
+    instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
 
-    pub evaluation: WipProbe<'tcx>,
+    evaluation: WipProbe<'tcx>,
 }
 
 impl<'tcx> WipGoalEvaluationStep<'tcx> {
-    pub fn finalize(self) -> inspect::GoalEvaluationStep<'tcx> {
+    fn finalize(self) -> inspect::GoalEvaluationStep<'tcx> {
         let evaluation = self.evaluation.finalize();
         match evaluation.kind {
-            ProbeKind::Root { .. } => (),
+            inspect::ProbeKind::Root { .. } => (),
             _ => unreachable!("unexpected root evaluation: {evaluation:?}"),
         }
         inspect::GoalEvaluationStep { instantiated_goal: self.instantiated_goal, evaluation }
@@ -115,13 +194,13 @@ impl<'tcx> WipGoalEvaluationStep<'tcx> {
 }
 
 #[derive(Eq, PartialEq, Debug)]
-pub struct WipProbe<'tcx> {
+struct WipProbe<'tcx> {
     pub steps: Vec<WipProbeStep<'tcx>>,
-    pub kind: Option<ProbeKind<'tcx>>,
+    pub kind: Option<inspect::ProbeKind<'tcx>>,
 }
 
 impl<'tcx> WipProbe<'tcx> {
-    pub fn finalize(self) -> inspect::Probe<'tcx> {
+    fn finalize(self) -> inspect::Probe<'tcx> {
         inspect::Probe {
             steps: self.steps.into_iter().map(WipProbeStep::finalize).collect(),
             kind: self.kind.unwrap(),
@@ -130,14 +209,14 @@ impl<'tcx> WipProbe<'tcx> {
 }
 
 #[derive(Eq, PartialEq, Debug)]
-pub enum WipProbeStep<'tcx> {
-    AddGoal(Goal<'tcx, ty::Predicate<'tcx>>),
+enum WipProbeStep<'tcx> {
+    AddGoal(inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>),
     EvaluateGoals(WipAddedGoalsEvaluation<'tcx>),
     NestedProbe(WipProbe<'tcx>),
 }
 
 impl<'tcx> WipProbeStep<'tcx> {
-    pub fn finalize(self) -> inspect::ProbeStep<'tcx> {
+    fn finalize(self) -> inspect::ProbeStep<'tcx> {
         match self {
             WipProbeStep::AddGoal(goal) => inspect::ProbeStep::AddGoal(goal),
             WipProbeStep::EvaluateGoals(eval) => inspect::ProbeStep::EvaluateGoals(eval.finalize()),
@@ -146,55 +225,6 @@ impl<'tcx> WipProbeStep<'tcx> {
     }
 }
 
-#[derive(Debug)]
-pub 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> {
-    fn from(g: WipGoalEvaluation<'tcx>) -> DebugSolver<'tcx> {
-        DebugSolver::GoalEvaluation(g)
-    }
-}
-
-impl<'tcx> From<WipCanonicalGoalEvaluation<'tcx>> for DebugSolver<'tcx> {
-    fn from(g: WipCanonicalGoalEvaluation<'tcx>) -> DebugSolver<'tcx> {
-        DebugSolver::CanonicalGoalEvaluation(g)
-    }
-}
-
-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)
-    }
-}
-
-pub struct ProofTreeBuilder<'tcx> {
-    state: Option<Box<BuilderData<'tcx>>>,
-}
-
-struct BuilderData<'tcx> {
-    tree: DebugSolver<'tcx>,
-    use_global_cache: UseGlobalCache,
-}
-
 impl<'tcx> ProofTreeBuilder<'tcx> {
     fn new(
         state: impl Into<DebugSolver<'tcx>>,
@@ -273,16 +303,19 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
         self.state.is_none()
     }
 
-    pub(super) fn new_goal_evaluation(
+    pub(in crate::solve) fn new_goal_evaluation(
         &mut self,
         goal: Goal<'tcx, ty::Predicate<'tcx>>,
-        kind: GoalEvaluationKind,
+        orig_values: &[ty::GenericArg<'tcx>],
+        kind: solve::GoalEvaluationKind,
     ) -> ProofTreeBuilder<'tcx> {
         self.nested(|| WipGoalEvaluation {
             uncanonicalized_goal: goal,
             kind: match kind {
-                GoalEvaluationKind::Root => WipGoalEvaluationKind::Root,
-                GoalEvaluationKind::Nested { is_normalizes_to_hack } => {
+                solve::GoalEvaluationKind::Root => {
+                    WipGoalEvaluationKind::Root { orig_values: orig_values.to_vec() }
+                }
+                solve::GoalEvaluationKind::Nested { is_normalizes_to_hack } => {
                     WipGoalEvaluationKind::Nested { is_normalizes_to_hack }
                 }
             },
@@ -379,7 +412,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
         self.nested(|| WipProbe { steps: vec![], kind: None })
     }
 
-    pub fn probe_kind(&mut self, probe_kind: ProbeKind<'tcx>) {
+    pub fn probe_kind(&mut self, probe_kind: inspect::ProbeKind<'tcx>) {
         if let Some(this) = self.as_mut() {
             match this {
                 DebugSolver::Probe(this) => {
@@ -390,18 +423,22 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
         }
     }
 
-    pub fn add_goal(&mut self, goal: Goal<'tcx, ty::Predicate<'tcx>>) {
-        if let Some(this) = self.as_mut() {
-            match this {
-                DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
-                    evaluation: WipProbe { steps, .. },
-                    ..
-                })
-                | DebugSolver::Probe(WipProbe { steps, .. }) => {
-                    steps.push(WipProbeStep::AddGoal(goal))
-                }
-                _ => unreachable!(),
-            }
+    pub fn add_goal(ecx: &mut EvalCtxt<'_, 'tcx>, 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(goal)),
+            s => unreachable!("tried to add {goal:?} to {s:?}"),
         }
     }
 
@@ -471,7 +508,10 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
                 }
                 DebugSolver::GoalEvaluationStep(evaluation_step) => {
                     assert_eq!(
-                        evaluation_step.evaluation.kind.replace(ProbeKind::Root { result }),
+                        evaluation_step
+                            .evaluation
+                            .kind
+                            .replace(inspect::ProbeKind::Root { result }),
                         None
                     );
                 }
diff --git a/compiler/rustc_trait_selection/src/solve/inspect/mod.rs b/compiler/rustc_trait_selection/src/solve/inspect/mod.rs
new file mode 100644
index 00000000000..60d52305a6b
--- /dev/null
+++ b/compiler/rustc_trait_selection/src/solve/inspect/mod.rs
@@ -0,0 +1,7 @@
+pub use rustc_middle::traits::solve::inspect::*;
+
+mod build;
+pub(in crate::solve) use build::*;
+
+mod analyse;
+pub use analyse::*;
diff --git a/compiler/rustc_trait_selection/src/solve/mod.rs b/compiler/rustc_trait_selection/src/solve/mod.rs
index bd612ce4778..77a3b5e1284 100644
--- a/compiler/rustc_trait_selection/src/solve/mod.rs
+++ b/compiler/rustc_trait_selection/src/solve/mod.rs
@@ -235,7 +235,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
 
     #[instrument(level = "debug", skip(self))]
     fn add_goal(&mut self, goal: Goal<'tcx, ty::Predicate<'tcx>>) {
-        self.inspect.add_goal(goal);
+        inspect::ProofTreeBuilder::add_goal(self, goal);
         self.nested_goals.goals.push(goal);
     }
 
diff --git a/compiler/rustc_trait_selection/src/traits/coherence.rs b/compiler/rustc_trait_selection/src/traits/coherence.rs
index e90723b0ee8..59f712721fb 100644
--- a/compiler/rustc_trait_selection/src/traits/coherence.rs
+++ b/compiler/rustc_trait_selection/src/traits/coherence.rs
@@ -6,9 +6,15 @@
 
 use crate::infer::outlives::env::OutlivesEnvironment;
 use crate::infer::InferOk;
+use crate::solve::inspect;
+use crate::solve::inspect::{InspectGoal, ProofTreeInferCtxtExt, ProofTreeVisitor};
+use crate::traits::engine::TraitEngineExt;
 use crate::traits::outlives_bounds::InferCtxtExt as _;
+use crate::traits::query::evaluate_obligation::InferCtxtExt;
 use crate::traits::select::{IntercrateAmbiguityCause, TreatInductiveCycleAs};
+use crate::traits::structural_normalize::StructurallyNormalizeExt;
 use crate::traits::util::impl_subject_and_oblig;
+use crate::traits::NormalizeExt;
 use crate::traits::SkipLeakCheck;
 use crate::traits::{
     self, Obligation, ObligationCause, ObligationCtxt, PredicateObligation, PredicateObligations,
@@ -18,10 +24,13 @@ use rustc_data_structures::fx::FxIndexSet;
 use rustc_errors::Diagnostic;
 use rustc_hir::def_id::{DefId, CRATE_DEF_ID, LOCAL_CRATE};
 use rustc_infer::infer::{DefineOpaqueTypes, InferCtxt, TyCtxtInferExt};
-use rustc_infer::traits::util;
+use rustc_infer::traits::{util, TraitEngine};
+use rustc_middle::traits::query::NoSolution;
+use rustc_middle::traits::solve::{Certainty, Goal};
 use rustc_middle::traits::specialization_graph::OverlapMode;
 use rustc_middle::traits::DefiningAnchor;
 use rustc_middle::ty::fast_reject::{DeepRejectCtxt, TreatParams};
+use rustc_middle::ty::print::with_no_trimmed_paths;
 use rustc_middle::ty::visit::{TypeVisitable, TypeVisitableExt};
 use rustc_middle::ty::{self, Ty, TyCtxt, TypeVisitor};
 use rustc_session::lint::builtin::COINDUCTIVE_OVERLAP_IN_COHERENCE;
@@ -31,9 +40,6 @@ use std::fmt::Debug;
 use std::iter;
 use std::ops::ControlFlow;
 
-use super::query::evaluate_obligation::InferCtxtExt;
-use super::NormalizeExt;
-
 /// Whether we do the orphan check relative to this crate or
 /// to some remote crate.
 #[derive(Copy, Clone, Debug)]
@@ -205,19 +211,19 @@ fn overlap<'tcx>(
 
     // Equate the headers to find their intersection (the general type, with infer vars,
     // that may apply both impls).
-    let equate_obligations = equate_impl_headers(selcx.infcx, &impl1_header, &impl2_header)?;
+    let mut obligations = equate_impl_headers(selcx.infcx, &impl1_header, &impl2_header)?;
     debug!("overlap: unification check succeeded");
 
+    obligations.extend(
+        [&impl1_header.predicates, &impl2_header.predicates].into_iter().flatten().map(
+            |&predicate| Obligation::new(infcx.tcx, ObligationCause::dummy(), param_env, predicate),
+        ),
+    );
+
     if overlap_mode.use_implicit_negative() {
         for mode in [TreatInductiveCycleAs::Ambig, TreatInductiveCycleAs::Recur] {
             if let Some(failing_obligation) = selcx.with_treat_inductive_cycle_as(mode, |selcx| {
-                impl_intersection_has_impossible_obligation(
-                    selcx,
-                    param_env,
-                    &impl1_header,
-                    &impl2_header,
-                    &equate_obligations,
-                )
+                impl_intersection_has_impossible_obligation(selcx, &obligations)
             }) {
                 if matches!(mode, TreatInductiveCycleAs::Recur) {
                     let first_local_impl = impl1_header
@@ -281,7 +287,14 @@ fn overlap<'tcx>(
         return None;
     }
 
-    let intercrate_ambiguity_causes = selcx.take_intercrate_ambiguity_causes();
+    let intercrate_ambiguity_causes = if !overlap_mode.use_implicit_negative() {
+        Default::default()
+    } else if infcx.next_trait_solver() {
+        compute_intercrate_ambiguity_causes(&infcx, &obligations)
+    } else {
+        selcx.take_intercrate_ambiguity_causes()
+    };
+
     debug!("overlap: intercrate_ambiguity_causes={:#?}", intercrate_ambiguity_causes);
     let involves_placeholder = infcx
         .inner
@@ -335,34 +348,24 @@ fn equate_impl_headers<'tcx>(
 /// of the two impls above to be empty.
 ///
 /// Importantly, this works even if there isn't a `impl !Error for MyLocalType`.
-fn impl_intersection_has_impossible_obligation<'cx, 'tcx>(
+fn impl_intersection_has_impossible_obligation<'a, 'cx, 'tcx>(
     selcx: &mut SelectionContext<'cx, 'tcx>,
-    param_env: ty::ParamEnv<'tcx>,
-    impl1_header: &ty::ImplHeader<'tcx>,
-    impl2_header: &ty::ImplHeader<'tcx>,
-    obligations: &PredicateObligations<'tcx>,
-) -> Option<PredicateObligation<'tcx>> {
+    obligations: &'a [PredicateObligation<'tcx>],
+) -> Option<&'a PredicateObligation<'tcx>> {
     let infcx = selcx.infcx;
 
-    [&impl1_header.predicates, &impl2_header.predicates]
-        .into_iter()
-        .flatten()
-        .map(|&predicate| {
-            Obligation::new(infcx.tcx, ObligationCause::dummy(), param_env, predicate)
-        })
-        .chain(obligations.into_iter().cloned())
-        .find(|obligation: &PredicateObligation<'tcx>| {
-            if infcx.next_trait_solver() {
-                infcx.evaluate_obligation(obligation).map_or(false, |result| !result.may_apply())
-            } else {
-                // We use `evaluate_root_obligation` to correctly track intercrate
-                // ambiguity clauses. We cannot use this in the new solver.
-                selcx.evaluate_root_obligation(obligation).map_or(
-                    false, // Overflow has occurred, and treat the obligation as possibly holding.
-                    |result| !result.may_apply(),
-                )
-            }
-        })
+    obligations.iter().find(|obligation| {
+        if infcx.next_trait_solver() {
+            infcx.evaluate_obligation(obligation).map_or(false, |result| !result.may_apply())
+        } else {
+            // We use `evaluate_root_obligation` to correctly track intercrate
+            // ambiguity clauses. We cannot use this in the new solver.
+            selcx.evaluate_root_obligation(obligation).map_or(
+                false, // Overflow has occurred, and treat the obligation as possibly holding.
+                |result| !result.may_apply(),
+            )
+        }
+    })
 }
 
 /// Check if both impls can be satisfied by a common type by considering whether
@@ -882,3 +885,144 @@ where
         ControlFlow::Continue(())
     }
 }
+
+/// Compute the `intercrate_ambiguity_causes` for the new solver using
+/// "proof trees".
+///
+/// This is a bit scuffed but seems to be good enough, at least
+/// when looking at UI tests. Given that it is only used to improve
+/// diagnostics this is good enough. We can always improve it once there
+/// are test cases where it is currently not enough.
+fn compute_intercrate_ambiguity_causes<'tcx>(
+    infcx: &InferCtxt<'tcx>,
+    obligations: &[PredicateObligation<'tcx>],
+) -> FxIndexSet<IntercrateAmbiguityCause> {
+    let mut causes: FxIndexSet<IntercrateAmbiguityCause> = Default::default();
+
+    for obligation in obligations {
+        search_ambiguity_causes(infcx, obligation.clone().into(), &mut causes);
+    }
+
+    causes
+}
+
+struct AmbiguityCausesVisitor<'a> {
+    causes: &'a mut FxIndexSet<IntercrateAmbiguityCause>,
+}
+
+impl<'a, 'tcx> ProofTreeVisitor<'tcx> for AmbiguityCausesVisitor<'a> {
+    type BreakTy = !;
+    fn visit_goal(&mut self, goal: &InspectGoal<'_, 'tcx>) -> ControlFlow<Self::BreakTy> {
+        let infcx = goal.infcx();
+        for cand in goal.candidates() {
+            cand.visit_nested(self)?;
+        }
+        // When searching for intercrate ambiguity causes, we only need to look
+        // at ambiguous goals, as for others the coherence unknowable candidate
+        // was irrelevant.
+        match goal.result() {
+            Ok(Certainty::Maybe(_)) => {}
+            Ok(Certainty::Yes) | Err(NoSolution) => return ControlFlow::Continue(()),
+        }
+
+        let Goal { param_env, predicate } = goal.goal();
+
+        // For bound predicates we simply call `infcx.replace_bound_vars_with_placeholders`
+        // and then prove the resulting predicate as a nested goal.
+        let trait_ref = match predicate.kind().no_bound_vars() {
+            Some(ty::PredicateKind::Clause(ty::ClauseKind::Trait(tr))) => tr.trait_ref,
+            Some(ty::PredicateKind::Clause(ty::ClauseKind::Projection(proj))) => {
+                proj.projection_ty.trait_ref(infcx.tcx)
+            }
+            _ => return ControlFlow::Continue(()),
+        };
+
+        let mut ambiguity_cause = None;
+        for cand in goal.candidates() {
+            // FIXME: boiiii, using string comparisions here sure is scuffed.
+            if let inspect::ProbeKind::MiscCandidate { name: "coherence unknowable", result: _ } =
+                cand.kind()
+            {
+                let lazily_normalize_ty = |ty: Ty<'tcx>| {
+                    let mut fulfill_cx = <dyn TraitEngine<'tcx>>::new(infcx);
+                    if matches!(ty.kind(), ty::Alias(..)) {
+                        // FIXME(-Ztrait-solver=next-coherence): we currently don't
+                        // normalize opaque types here, resulting in diverging behavior
+                        // for TAITs.
+                        match infcx
+                            .at(&ObligationCause::dummy(), param_env)
+                            .structurally_normalize(ty, &mut *fulfill_cx)
+                        {
+                            Ok(ty) => Ok(ty),
+                            Err(_errs) => Err(()),
+                        }
+                    } else {
+                        Ok(ty)
+                    }
+                };
+
+                infcx.probe(|_| {
+                    match trait_ref_is_knowable(infcx.tcx, trait_ref, lazily_normalize_ty) {
+                        Err(()) => {}
+                        Ok(Ok(())) => warn!("expected an unknowable trait ref: {trait_ref:?}"),
+                        Ok(Err(conflict)) => {
+                            if !trait_ref.references_error() {
+                                let self_ty = trait_ref.self_ty();
+                                let (trait_desc, self_desc) = with_no_trimmed_paths!({
+                                    let trait_desc = trait_ref.print_only_trait_path().to_string();
+                                    let self_desc = self_ty
+                                        .has_concrete_skeleton()
+                                        .then(|| self_ty.to_string());
+                                    (trait_desc, self_desc)
+                                });
+                                ambiguity_cause = Some(match conflict {
+                                    Conflict::Upstream => {
+                                        IntercrateAmbiguityCause::UpstreamCrateUpdate {
+                                            trait_desc,
+                                            self_desc,
+                                        }
+                                    }
+                                    Conflict::Downstream => {
+                                        IntercrateAmbiguityCause::DownstreamCrate {
+                                            trait_desc,
+                                            self_desc,
+                                        }
+                                    }
+                                });
+                            }
+                        }
+                    }
+                })
+            } else {
+                match cand.result() {
+                    // We only add an ambiguity cause if the goal would otherwise
+                    // result in an error.
+                    //
+                    // FIXME: While this matches the behavior of the
+                    // old solver, it is not the only way in which the unknowable
+                    // candidates *weaken* coherence, they can also force otherwise
+                    // sucessful normalization to be ambiguous.
+                    Ok(Certainty::Maybe(_) | Certainty::Yes) => {
+                        ambiguity_cause = None;
+                        break;
+                    }
+                    Err(NoSolution) => continue,
+                }
+            }
+        }
+
+        if let Some(ambiguity_cause) = ambiguity_cause {
+            self.causes.insert(ambiguity_cause);
+        }
+
+        ControlFlow::Continue(())
+    }
+}
+
+fn search_ambiguity_causes<'tcx>(
+    infcx: &InferCtxt<'tcx>,
+    goal: Goal<'tcx, ty::Predicate<'tcx>>,
+    causes: &mut FxIndexSet<IntercrateAmbiguityCause>,
+) {
+    infcx.visit_proof_tree(goal, &mut AmbiguityCausesVisitor { causes });
+}
diff --git a/compiler/rustc_trait_selection/src/traits/structural_normalize.rs b/compiler/rustc_trait_selection/src/traits/structural_normalize.rs
index d3c4dc45923..9d6be768901 100644
--- a/compiler/rustc_trait_selection/src/traits/structural_normalize.rs
+++ b/compiler/rustc_trait_selection/src/traits/structural_normalize.rs
@@ -22,9 +22,14 @@ impl<'tcx> StructurallyNormalizeExt<'tcx> for At<'_, 'tcx> {
         assert!(!ty.is_ty_var(), "should have resolved vars before calling");
 
         if self.infcx.next_trait_solver() {
-            while let ty::Alias(ty::Projection | ty::Inherent | ty::Weak, projection_ty) =
-                *ty.kind()
-            {
+            // FIXME(-Ztrait-solver=next): correctly handle
+            // overflow here.
+            for _ in 0..256 {
+                let ty::Alias(ty::Projection | ty::Inherent | ty::Weak, projection_ty) = *ty.kind()
+                else {
+                    break;
+                };
+
                 let new_infer_ty = self.infcx.next_ty_var(TypeVariableOrigin {
                     kind: TypeVariableOriginKind::NormalizeProjectionType,
                     span: self.cause.span,
@@ -49,6 +54,7 @@ impl<'tcx> StructurallyNormalizeExt<'tcx> for At<'_, 'tcx> {
                     break;
                 }
             }
+
             Ok(ty)
         } else {
             Ok(self.normalize(ty).into_value_registering_obligations(self.infcx, fulfill_cx))