Merging upstream version 1.72.1+dfsg1.

Signed-off-by: Daniel Baumann <daniel.baumann@progress-linux.org>

17 files changed, 2015 insertions, 562 deletions

diff --git a/compiler/rustc_trait_selection/src/solve/alias_relate.rs b/compiler/rustc_trait_selection/src/solve/alias_relate.rs
new file mode 100644
index 000000000..422a6ee34
--- /dev/null
+++ b/compiler/rustc_trait_selection/src/solve/alias_relate.rs
@@ -0,0 +1,195 @@
+use super::{EvalCtxt, SolverMode};
+use rustc_infer::traits::query::NoSolution;
+use rustc_middle::traits::solve::{Certainty, Goal, QueryResult};
+use rustc_middle::ty;
+
+/// We may need to invert the alias relation direction if dealing an alias on the RHS.
+#[derive(Debug)]
+enum Invert {
+    No,
+    Yes,
+}
+
+impl<'tcx> EvalCtxt<'_, 'tcx> {
+    #[instrument(level = "debug", skip(self), ret)]
+    pub(super) fn compute_alias_relate_goal(
+        &mut self,
+        goal: Goal<'tcx, (ty::Term<'tcx>, ty::Term<'tcx>, ty::AliasRelationDirection)>,
+    ) -> QueryResult<'tcx> {
+        let tcx = self.tcx();
+        let Goal { param_env, predicate: (lhs, rhs, direction) } = goal;
+        if lhs.is_infer() || rhs.is_infer() {
+            bug!(
+                "`AliasRelate` goal with an infer var on lhs or rhs which should have been instantiated"
+            );
+        }
+
+        match (lhs.to_alias_ty(tcx), rhs.to_alias_ty(tcx)) {
+            (None, None) => bug!("`AliasRelate` goal without an alias on either lhs or rhs"),
+
+            // RHS is not a projection, only way this is true is if LHS normalizes-to RHS
+            (Some(alias_lhs), None) => self.assemble_normalizes_to_candidate(
+                param_env,
+                alias_lhs,
+                rhs,
+                direction,
+                Invert::No,
+            ),
+
+            // LHS is not a projection, only way this is true is if RHS normalizes-to LHS
+            (None, Some(alias_rhs)) => self.assemble_normalizes_to_candidate(
+                param_env,
+                alias_rhs,
+                lhs,
+                direction,
+                Invert::Yes,
+            ),
+
+            (Some(alias_lhs), Some(alias_rhs)) => {
+                debug!("both sides are aliases");
+
+                let mut candidates = Vec::new();
+                // LHS normalizes-to RHS
+                candidates.extend(self.assemble_normalizes_to_candidate(
+                    param_env,
+                    alias_lhs,
+                    rhs,
+                    direction,
+                    Invert::No,
+                ));
+                // RHS normalizes-to RHS
+                candidates.extend(self.assemble_normalizes_to_candidate(
+                    param_env,
+                    alias_rhs,
+                    lhs,
+                    direction,
+                    Invert::Yes,
+                ));
+                // Relate via substs
+                let subst_relate_response = self
+                    .assemble_subst_relate_candidate(param_env, alias_lhs, alias_rhs, direction);
+                candidates.extend(subst_relate_response);
+                debug!(?candidates);
+
+                if let Some(merged) = self.try_merge_responses(&candidates) {
+                    Ok(merged)
+                } else {
+                    // When relating two aliases and we have ambiguity, we prefer
+                    // relating the generic arguments of the aliases over normalizing
+                    // them. This is necessary for inference during typeck.
+                    //
+                    // As this is incomplete, we must not do so during coherence.
+                    match self.solver_mode() {
+                        SolverMode::Normal => {
+                            if let Ok(subst_relate_response) = subst_relate_response {
+                                Ok(subst_relate_response)
+                            } else if let Ok(bidirectional_normalizes_to_response) = self
+                                .assemble_bidirectional_normalizes_to_candidate(
+                                    param_env, lhs, rhs, direction,
+                                )
+                            {
+                                Ok(bidirectional_normalizes_to_response)
+                            } else {
+                                self.flounder(&candidates)
+                            }
+                        }
+                        SolverMode::Coherence => self.flounder(&candidates),
+                    }
+                }
+            }
+        }
+    }
+
+    #[instrument(level = "debug", skip(self), ret)]
+    fn assemble_normalizes_to_candidate(
+        &mut self,
+        param_env: ty::ParamEnv<'tcx>,
+        alias: ty::AliasTy<'tcx>,
+        other: ty::Term<'tcx>,
+        direction: ty::AliasRelationDirection,
+        invert: Invert,
+    ) -> QueryResult<'tcx> {
+        self.probe_candidate("normalizes-to").enter(|ecx| {
+            ecx.normalizes_to_inner(param_env, alias, other, direction, invert)?;
+            ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
+        })
+    }
+
+    fn normalizes_to_inner(
+        &mut self,
+        param_env: ty::ParamEnv<'tcx>,
+        alias: ty::AliasTy<'tcx>,
+        other: ty::Term<'tcx>,
+        direction: ty::AliasRelationDirection,
+        invert: Invert,
+    ) -> Result<(), NoSolution> {
+        let other = match direction {
+            // This is purely an optimization.
+            ty::AliasRelationDirection::Equate => other,
+
+            ty::AliasRelationDirection::Subtype => {
+                let fresh = self.next_term_infer_of_kind(other);
+                let (sub, sup) = match invert {
+                    Invert::No => (fresh, other),
+                    Invert::Yes => (other, fresh),
+                };
+                self.sub(param_env, sub, sup)?;
+                fresh
+            }
+        };
+        self.add_goal(Goal::new(
+            self.tcx(),
+            param_env,
+            ty::Binder::dummy(ty::ProjectionPredicate { projection_ty: alias, term: other }),
+        ));
+
+        Ok(())
+    }
+
+    fn assemble_subst_relate_candidate(
+        &mut self,
+        param_env: ty::ParamEnv<'tcx>,
+        alias_lhs: ty::AliasTy<'tcx>,
+        alias_rhs: ty::AliasTy<'tcx>,
+        direction: ty::AliasRelationDirection,
+    ) -> QueryResult<'tcx> {
+        self.probe_candidate("substs relate").enter(|ecx| {
+            match direction {
+                ty::AliasRelationDirection::Equate => {
+                    ecx.eq(param_env, alias_lhs, alias_rhs)?;
+                }
+                ty::AliasRelationDirection::Subtype => {
+                    ecx.sub(param_env, alias_lhs, alias_rhs)?;
+                }
+            }
+
+            ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
+        })
+    }
+
+    fn assemble_bidirectional_normalizes_to_candidate(
+        &mut self,
+        param_env: ty::ParamEnv<'tcx>,
+        lhs: ty::Term<'tcx>,
+        rhs: ty::Term<'tcx>,
+        direction: ty::AliasRelationDirection,
+    ) -> QueryResult<'tcx> {
+        self.probe_candidate("bidir normalizes-to").enter(|ecx| {
+            ecx.normalizes_to_inner(
+                param_env,
+                lhs.to_alias_ty(ecx.tcx()).unwrap(),
+                rhs,
+                direction,
+                Invert::No,
+            )?;
+            ecx.normalizes_to_inner(
+                param_env,
+                rhs.to_alias_ty(ecx.tcx()).unwrap(),
+                lhs,
+                direction,
+                Invert::Yes,
+            )?;
+            ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
+        })
+    }
+}
diff --git a/compiler/rustc_trait_selection/src/solve/assembly/mod.rs b/compiler/rustc_trait_selection/src/solve/assembly/mod.rs
index f32ff0442..28138054a 100644
--- a/compiler/rustc_trait_selection/src/solve/assembly/mod.rs
+++ b/compiler/rustc_trait_selection/src/solve/assembly/mod.rs
@@ -8,6 +8,7 @@ use rustc_hir::def_id::DefId;
 use rustc_infer::traits::query::NoSolution;
 use rustc_infer::traits::util::elaborate;
 use rustc_infer::traits::Reveal;
+use rustc_middle::traits::solve::inspect::CandidateKind;
 use rustc_middle::traits::solve::{CanonicalResponse, Certainty, Goal, MaybeCause, QueryResult};
 use rustc_middle::ty::fast_reject::TreatProjections;
 use rustc_middle::ty::TypeFoldable;
@@ -48,7 +49,7 @@ pub(super) enum CandidateSource {
     /// Notable examples are auto traits, `Sized`, and `DiscriminantKind`.
     /// For a list of all traits with builtin impls, check out the
     /// [`EvalCtxt::assemble_builtin_impl_candidates`] method. Not
-    BuiltinImpl,
+    BuiltinImpl(BuiltinImplSource),
     /// An assumption from the environment.
     ///
     /// More precisely we've used the `n-th` assumption in the `param_env`.
@@ -86,6 +87,16 @@ pub(super) enum CandidateSource {
     AliasBound,
 }
 
+/// Records additional information about what kind of built-in impl this is.
+/// This should only be used by selection.
+#[derive(Debug, Clone, Copy)]
+pub(super) enum BuiltinImplSource {
+    TraitUpcasting,
+    Object,
+    Misc,
+    Ambiguity,
+}
+
 /// Methods used to assemble candidates for either trait or projection goals.
 pub(super) trait GoalKind<'tcx>:
     TypeFoldable<TyCtxt<'tcx>> + Copy + Eq + std::fmt::Display
@@ -105,7 +116,7 @@ pub(super) trait GoalKind<'tcx>:
     fn probe_and_match_goal_against_assumption(
         ecx: &mut EvalCtxt<'_, 'tcx>,
         goal: Goal<'tcx, Self>,
-        assumption: ty::Predicate<'tcx>,
+        assumption: ty::Clause<'tcx>,
         then: impl FnOnce(&mut EvalCtxt<'_, 'tcx>) -> QueryResult<'tcx>,
     ) -> QueryResult<'tcx>;
 
@@ -115,7 +126,7 @@ pub(super) trait GoalKind<'tcx>:
     fn consider_implied_clause(
         ecx: &mut EvalCtxt<'_, 'tcx>,
         goal: Goal<'tcx, Self>,
-        assumption: ty::Predicate<'tcx>,
+        assumption: ty::Clause<'tcx>,
         requirements: impl IntoIterator<Item = Goal<'tcx, ty::Predicate<'tcx>>>,
     ) -> QueryResult<'tcx> {
         Self::probe_and_match_goal_against_assumption(ecx, goal, assumption, |ecx| {
@@ -131,7 +142,7 @@ pub(super) trait GoalKind<'tcx>:
     fn consider_alias_bound_candidate(
         ecx: &mut EvalCtxt<'_, 'tcx>,
         goal: Goal<'tcx, Self>,
-        assumption: ty::Predicate<'tcx>,
+        assumption: ty::Clause<'tcx>,
     ) -> QueryResult<'tcx> {
         Self::probe_and_match_goal_against_assumption(ecx, goal, assumption, |ecx| {
             ecx.validate_alias_bound_self_from_param_env(goal)
@@ -144,7 +155,7 @@ pub(super) trait GoalKind<'tcx>:
     fn consider_object_bound_candidate(
         ecx: &mut EvalCtxt<'_, 'tcx>,
         goal: Goal<'tcx, Self>,
-        assumption: ty::Predicate<'tcx>,
+        assumption: ty::Clause<'tcx>,
     ) -> QueryResult<'tcx> {
         Self::probe_and_match_goal_against_assumption(ecx, goal, assumption, |ecx| {
             let tcx = ecx.tcx();
@@ -294,7 +305,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
         // least structurally resolve the type one layer.
         if goal.predicate.self_ty().is_ty_var() {
             return vec![Candidate {
-                source: CandidateSource::BuiltinImpl,
+                source: CandidateSource::BuiltinImpl(BuiltinImplSource::Ambiguity),
                 result: self
                     .evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS)
                     .unwrap(),
@@ -320,11 +331,20 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
         candidates
     }
 
-    /// If the self type of a goal is a projection, computing the relevant candidates is difficult.
+    /// If the self type of a goal is an alias we first try to normalize the self type
+    /// and compute the candidates for the normalized self type in case that succeeds.
+    ///
+    /// These candidates are used in addition to the ones with the alias as a self type.
+    /// We do this to simplify both builtin candidates and for better performance.
+    ///
+    /// We generate the builtin candidates on the fly by looking at the self type, e.g.
+    /// add `FnPtr` candidates if the self type is a function pointer. Handling builtin
+    /// candidates while the self type is still an alias seems difficult. This is similar
+    /// to `try_structurally_resolve_type` during hir typeck (FIXME once implemented).
     ///
-    /// To deal with this, we first try to normalize the self type and add the candidates for the normalized
-    /// self type to the list of candidates in case that succeeds. We also have to consider candidates with the
-    /// projection as a self type as well
+    /// Looking at all impls for some trait goal is prohibitively expensive. We therefore
+    /// only look at implementations with a matching self type. Because of this function,
+    /// we can avoid looking at all existing impls if the self type is an alias.
     #[instrument(level = "debug", skip_all)]
     fn assemble_candidates_after_normalizing_self_ty<G: GoalKind<'tcx>>(
         &mut self,
@@ -336,37 +356,41 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
             return
         };
 
-        let normalized_self_candidates: Result<_, NoSolution> = self.probe(|ecx| {
-            ecx.with_incremented_depth(
-                |ecx| {
-                    let result = ecx.evaluate_added_goals_and_make_canonical_response(
-                        Certainty::Maybe(MaybeCause::Overflow),
-                    )?;
-                    Ok(vec![Candidate { source: CandidateSource::BuiltinImpl, result }])
-                },
-                |ecx| {
-                    let normalized_ty = ecx.next_ty_infer();
-                    let normalizes_to_goal = goal.with(
-                        tcx,
-                        ty::Binder::dummy(ty::ProjectionPredicate {
-                            projection_ty,
-                            term: normalized_ty.into(),
-                        }),
-                    );
-                    ecx.add_goal(normalizes_to_goal);
-                    let _ = ecx.try_evaluate_added_goals().inspect_err(|_| {
-                        debug!("self type normalization failed");
-                    })?;
-                    let normalized_ty = ecx.resolve_vars_if_possible(normalized_ty);
-                    debug!(?normalized_ty, "self type normalized");
-                    // NOTE: Alternatively we could call `evaluate_goal` here and only
-                    // have a `Normalized` candidate. This doesn't work as long as we
-                    // use `CandidateSource` in winnowing.
-                    let goal = goal.with(tcx, goal.predicate.with_self_ty(tcx, normalized_ty));
-                    Ok(ecx.assemble_and_evaluate_candidates(goal))
-                },
-            )
-        });
+        let normalized_self_candidates: Result<_, NoSolution> =
+            self.probe(|_| CandidateKind::NormalizedSelfTyAssembly).enter(|ecx| {
+                ecx.with_incremented_depth(
+                    |ecx| {
+                        let result = ecx.evaluate_added_goals_and_make_canonical_response(
+                            Certainty::Maybe(MaybeCause::Overflow),
+                        )?;
+                        Ok(vec![Candidate {
+                            source: CandidateSource::BuiltinImpl(BuiltinImplSource::Ambiguity),
+                            result,
+                        }])
+                    },
+                    |ecx| {
+                        let normalized_ty = ecx.next_ty_infer();
+                        let normalizes_to_goal = goal.with(
+                            tcx,
+                            ty::Binder::dummy(ty::ProjectionPredicate {
+                                projection_ty,
+                                term: normalized_ty.into(),
+                            }),
+                        );
+                        ecx.add_goal(normalizes_to_goal);
+                        let _ = ecx.try_evaluate_added_goals().inspect_err(|_| {
+                            debug!("self type normalization failed");
+                        })?;
+                        let normalized_ty = ecx.resolve_vars_if_possible(normalized_ty);
+                        debug!(?normalized_ty, "self type normalized");
+                        // NOTE: Alternatively we could call `evaluate_goal` here and only
+                        // have a `Normalized` candidate. This doesn't work as long as we
+                        // use `CandidateSource` in winnowing.
+                        let goal = goal.with(tcx, goal.predicate.with_self_ty(tcx, normalized_ty));
+                        Ok(ecx.assemble_and_evaluate_candidates(goal))
+                    },
+                )
+            });
 
         if let Ok(normalized_self_candidates) = normalized_self_candidates {
             candidates.extend(normalized_self_candidates);
@@ -445,9 +469,10 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
         };
 
         match result {
-            Ok(result) => {
-                candidates.push(Candidate { source: CandidateSource::BuiltinImpl, result })
-            }
+            Ok(result) => candidates.push(Candidate {
+                source: CandidateSource::BuiltinImpl(BuiltinImplSource::Misc),
+                result,
+            }),
             Err(NoSolution) => (),
         }
 
@@ -455,7 +480,10 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
         // `trait Foo: Bar<A> + Bar<B>` and `dyn Foo: Unsize<dyn Bar<_>>`
         if lang_items.unsize_trait() == Some(trait_def_id) {
             for result in G::consider_builtin_dyn_upcast_candidates(self, goal) {
-                candidates.push(Candidate { source: CandidateSource::BuiltinImpl, result });
+                candidates.push(Candidate {
+                    source: CandidateSource::BuiltinImpl(BuiltinImplSource::TraitUpcasting),
+                    result,
+                });
             }
         }
     }
@@ -508,10 +536,11 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
             | ty::Placeholder(..)
             | ty::Infer(ty::IntVar(_) | ty::FloatVar(_))
             | ty::Alias(ty::Inherent, _)
+            | ty::Alias(ty::Weak, _)
             | ty::Error(_) => return,
             ty::Infer(ty::TyVar(_) | ty::FreshTy(_) | ty::FreshIntTy(_) | ty::FreshFloatTy(_))
             | ty::Bound(..) => bug!("unexpected self type for `{goal:?}`"),
-            // Excluding IATs here as they don't have meaningful item bounds.
+            // Excluding IATs and type aliases here as they don't have meaningful item bounds.
             ty::Alias(ty::Projection | ty::Opaque, alias_ty) => alias_ty,
         };
 
@@ -618,9 +647,10 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
         };
 
         match result {
-            Ok(result) => {
-                candidates.push(Candidate { source: CandidateSource::BuiltinImpl, result })
-            }
+            Ok(result) => candidates.push(Candidate {
+                source: CandidateSource::BuiltinImpl(BuiltinImplSource::Misc),
+                result,
+            }),
             Err(NoSolution) => (),
         }
     }
@@ -631,6 +661,11 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
         goal: Goal<'tcx, G>,
         candidates: &mut Vec<Candidate<'tcx>>,
     ) {
+        let tcx = self.tcx();
+        if !tcx.trait_def(goal.predicate.trait_def_id(tcx)).implement_via_object {
+            return;
+        }
+
         let self_ty = goal.predicate.self_ty();
         let bounds = match *self_ty.kind() {
             ty::Bool
@@ -663,7 +698,6 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
             ty::Dynamic(bounds, ..) => bounds,
         };
 
-        let tcx = self.tcx();
         let own_bounds: FxIndexSet<_> =
             bounds.iter().map(|bound| bound.with_self_ty(tcx, self_ty)).collect();
         for assumption in elaborate(tcx, own_bounds.iter().copied())
@@ -675,17 +709,16 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
             // projection predicates that we reach by elaborating the principal trait ref,
             // since that'll cause ambiguity.
             //
-            // We can remove this when we have implemented intersections in responses.
-            if assumption.to_opt_poly_projection_pred().is_some()
-                && !own_bounds.contains(&assumption)
-            {
+            // We can remove this when we have implemented lifetime intersections in responses.
+            if assumption.as_projection_clause().is_some() && !own_bounds.contains(&assumption) {
                 continue;
             }
 
             match G::consider_object_bound_candidate(self, goal, assumption) {
-                Ok(result) => {
-                    candidates.push(Candidate { source: CandidateSource::BuiltinImpl, result })
-                }
+                Ok(result) => candidates.push(Candidate {
+                    source: CandidateSource::BuiltinImpl(BuiltinImplSource::Object),
+                    result,
+                }),
                 Err(NoSolution) => (),
             }
         }
@@ -706,8 +739,10 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
                     Err(_) => match self
                         .evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS)
                     {
-                        Ok(result) => candidates
-                            .push(Candidate { source: CandidateSource::BuiltinImpl, result }),
+                        Ok(result) => candidates.push(Candidate {
+                            source: CandidateSource::BuiltinImpl(BuiltinImplSource::Ambiguity),
+                            result,
+                        }),
                         // FIXME: This will be reachable at some point if we're in
                         // `assemble_candidates_after_normalizing_self_ty` and we get a
                         // universe error. We'll deal with it at this point.
diff --git a/compiler/rustc_trait_selection/src/solve/assembly/structural_traits.rs b/compiler/rustc_trait_selection/src/solve/assembly/structural_traits.rs
index 0ede32c75..3bb8cad15 100644
--- a/compiler/rustc_trait_selection/src/solve/assembly/structural_traits.rs
+++ b/compiler/rustc_trait_selection/src/solve/assembly/structural_traits.rs
@@ -28,12 +28,12 @@ pub(in crate::solve) fn instantiate_constituent_tys_for_auto_trait<'tcx>(
         | ty::Char => Ok(vec![]),
 
         // Treat `str` like it's defined as `struct str([u8]);`
-        ty::Str => Ok(vec![tcx.mk_slice(tcx.types.u8)]),
+        ty::Str => Ok(vec![Ty::new_slice(tcx, tcx.types.u8)]),
 
         ty::Dynamic(..)
         | ty::Param(..)
         | ty::Foreign(..)
-        | ty::Alias(ty::Projection | ty::Inherent, ..)
+        | ty::Alias(ty::Projection | ty::Inherent | ty::Weak, ..)
         | ty::Placeholder(..)
         | ty::Bound(..)
         | ty::Infer(_) => {
@@ -96,7 +96,7 @@ pub(in crate::solve) fn replace_erased_lifetimes_with_bound_vars<'tcx>(
             let br =
                 ty::BoundRegion { var: ty::BoundVar::from_u32(counter), kind: ty::BrAnon(None) };
             counter += 1;
-            tcx.mk_re_late_bound(current_depth, br)
+            ty::Region::new_late_bound(tcx, current_depth, br)
         }
         // All free regions should be erased here.
         r => bug!("unexpected region: {r:?}"),
@@ -148,11 +148,7 @@ pub(in crate::solve) fn instantiate_constituent_tys_for_sized_trait<'tcx>(
 
         ty::Adt(def, substs) => {
             let sized_crit = def.sized_constraint(ecx.tcx());
-            Ok(sized_crit
-                .0
-                .iter()
-                .map(|ty| sized_crit.rebind(*ty).subst(ecx.tcx(), substs))
-                .collect())
+            Ok(sized_crit.subst_iter_copied(ecx.tcx(), substs).collect())
         }
     }
 }
@@ -237,7 +233,7 @@ pub(in crate::solve) fn extract_tupled_inputs_and_output_from_callable<'tcx>(
             {
                 Ok(Some(
                     sig.subst(tcx, substs)
-                        .map_bound(|sig| (tcx.mk_tup(sig.inputs()), sig.output())),
+                        .map_bound(|sig| (Ty::new_tup(tcx, sig.inputs()), sig.output())),
                 ))
             } else {
                 Err(NoSolution)
@@ -246,7 +242,7 @@ pub(in crate::solve) fn extract_tupled_inputs_and_output_from_callable<'tcx>(
         // keep this in sync with assemble_fn_pointer_candidates until the old solver is removed.
         ty::FnPtr(sig) => {
             if sig.is_fn_trait_compatible() {
-                Ok(Some(sig.map_bound(|sig| (tcx.mk_tup(sig.inputs()), sig.output()))))
+                Ok(Some(sig.map_bound(|sig| (Ty::new_tup(tcx, sig.inputs()), sig.output()))))
             } else {
                 Err(NoSolution)
             }
@@ -347,7 +343,7 @@ pub(in crate::solve) fn predicates_for_object_candidate<'tcx>(
     param_env: ty::ParamEnv<'tcx>,
     trait_ref: ty::TraitRef<'tcx>,
     object_bound: &'tcx ty::List<ty::PolyExistentialPredicate<'tcx>>,
-) -> Vec<ty::Predicate<'tcx>> {
+) -> Vec<ty::Clause<'tcx>> {
     let tcx = ecx.tcx();
     let mut requirements = vec![];
     requirements.extend(
@@ -357,7 +353,7 @@ pub(in crate::solve) fn predicates_for_object_candidate<'tcx>(
         // FIXME(associated_const_equality): Also add associated consts to
         // the requirements here.
         if item.kind == ty::AssocKind::Type {
-            requirements.extend(tcx.item_bounds(item.def_id).subst(tcx, trait_ref.substs));
+            requirements.extend(tcx.item_bounds(item.def_id).subst_iter(tcx, trait_ref.substs));
         }
     }
 
diff --git a/compiler/rustc_trait_selection/src/solve/canonicalize.rs b/compiler/rustc_trait_selection/src/solve/canonicalize.rs
index ff4bff10c..255620489 100644
--- a/compiler/rustc_trait_selection/src/solve/canonicalize.rs
+++ b/compiler/rustc_trait_selection/src/solve/canonicalize.rs
@@ -208,8 +208,25 @@ impl<'tcx> TypeFolder<TyCtxt<'tcx>> for Canonicalizer<'_, 'tcx> {
         t
     }
 
-    fn fold_region(&mut self, r: ty::Region<'tcx>) -> ty::Region<'tcx> {
-        let r = self.infcx.shallow_resolve(r);
+    fn fold_region(&mut self, mut r: ty::Region<'tcx>) -> ty::Region<'tcx> {
+        match self.canonicalize_mode {
+            CanonicalizeMode::Input => {
+                // Don't resolve infer vars in input, since it affects
+                // caching and may cause trait selection bugs which rely
+                // on regions to be equal.
+            }
+            CanonicalizeMode::Response { .. } => {
+                if let ty::ReVar(vid) = *r {
+                    r = self
+                        .infcx
+                        .inner
+                        .borrow_mut()
+                        .unwrap_region_constraints()
+                        .opportunistic_resolve_var(self.infcx.tcx, vid);
+                }
+            }
+        }
+
         let kind = match *r {
             ty::ReLateBound(..) => return r,
 
@@ -255,7 +272,7 @@ impl<'tcx> TypeFolder<TyCtxt<'tcx>> for Canonicalizer<'_, 'tcx> {
             }),
         );
         let br = ty::BoundRegion { var, kind: BrAnon(None) };
-        self.interner().mk_re_late_bound(self.binder_index, br)
+        ty::Region::new_late_bound(self.interner(), self.binder_index, br)
     }
 
     fn fold_ty(&mut self, mut t: Ty<'tcx>) -> Ty<'tcx> {
@@ -266,7 +283,7 @@ impl<'tcx> TypeFolder<TyCtxt<'tcx>> for Canonicalizer<'_, 'tcx> {
                 // any equated inference vars correctly!
                 let root_vid = self.infcx.root_var(vid);
                 if root_vid != vid {
-                    t = self.infcx.tcx.mk_ty_var(root_vid);
+                    t = Ty::new_var(self.infcx.tcx, root_vid);
                     vid = root_vid;
                 }
 
@@ -349,7 +366,7 @@ impl<'tcx> TypeFolder<TyCtxt<'tcx>> for Canonicalizer<'_, 'tcx> {
             }),
         );
         let bt = ty::BoundTy { var, kind: BoundTyKind::Anon };
-        self.interner().mk_bound(self.binder_index, bt)
+        Ty::new_bound(self.infcx.tcx, self.binder_index, bt)
     }
 
     fn fold_const(&mut self, mut c: ty::Const<'tcx>) -> ty::Const<'tcx> {
@@ -360,7 +377,7 @@ impl<'tcx> TypeFolder<TyCtxt<'tcx>> for Canonicalizer<'_, 'tcx> {
                 // any equated inference vars correctly!
                 let root_vid = self.infcx.root_const_var(vid);
                 if root_vid != vid {
-                    c = self.infcx.tcx.mk_const(ty::InferConst::Var(root_vid), c.ty());
+                    c = ty::Const::new_var(self.infcx.tcx, root_vid, c.ty());
                     vid = root_vid;
                 }
 
@@ -409,6 +426,6 @@ impl<'tcx> TypeFolder<TyCtxt<'tcx>> for Canonicalizer<'_, 'tcx> {
                 var
             }),
         );
-        self.interner().mk_const(ty::ConstKind::Bound(self.binder_index, var), c.ty())
+        ty::Const::new_bound(self.infcx.tcx, self.binder_index, var, c.ty())
     }
 }
diff --git a/compiler/rustc_trait_selection/src/solve/eval_ctxt.rs b/compiler/rustc_trait_selection/src/solve/eval_ctxt.rs
index f91c67277..74dfbdddb 100644
--- a/compiler/rustc_trait_selection/src/solve/eval_ctxt.rs
+++ b/compiler/rustc_trait_selection/src/solve/eval_ctxt.rs
@@ -9,25 +9,32 @@ use rustc_infer::infer::{
 use rustc_infer::traits::query::NoSolution;
 use rustc_infer::traits::ObligationCause;
 use rustc_middle::infer::unify_key::{ConstVariableOrigin, ConstVariableOriginKind};
+use rustc_middle::traits::solve::inspect;
 use rustc_middle::traits::solve::{
-    CanonicalInput, CanonicalResponse, Certainty, MaybeCause, PredefinedOpaques,
-    PredefinedOpaquesData, QueryResult,
+    CanonicalInput, CanonicalResponse, Certainty, IsNormalizesToHack, MaybeCause,
+    PredefinedOpaques, PredefinedOpaquesData, QueryResult,
 };
 use rustc_middle::traits::DefiningAnchor;
 use rustc_middle::ty::{
-    self, Ty, TyCtxt, TypeFoldable, TypeSuperVisitable, TypeVisitable, TypeVisitableExt,
-    TypeVisitor,
+    self, OpaqueTypeKey, Ty, TyCtxt, TypeFoldable, TypeSuperVisitable, TypeVisitable,
+    TypeVisitableExt, TypeVisitor,
 };
+use rustc_session::config::DumpSolverProofTree;
 use rustc_span::DUMMY_SP;
+use std::io::Write;
 use std::ops::ControlFlow;
 
 use crate::traits::specialization_graph;
 
+use super::inspect::ProofTreeBuilder;
 use super::search_graph::{self, OverflowHandler};
 use super::SolverMode;
 use super::{search_graph::SearchGraph, Goal};
+pub use select::InferCtxtSelectExt;
 
 mod canonical;
+mod probe;
+mod select;
 
 pub struct EvalCtxt<'a, 'tcx> {
     /// The inference context that backs (mostly) inference and placeholder terms
@@ -73,12 +80,8 @@ pub struct EvalCtxt<'a, 'tcx> {
     // ambiguous goals. Instead, a probe needs to be introduced somewhere in the
     // evaluation code.
     tainted: Result<(), NoSolution>,
-}
 
-#[derive(Debug, Copy, Clone, PartialEq, Eq)]
-pub(super) enum IsNormalizesToHack {
-    Yes,
-    No,
+    inspect: ProofTreeBuilder<'tcx>,
 }
 
 #[derive(Debug, Clone)]
@@ -110,6 +113,26 @@ impl NestedGoals<'_> {
     }
 }
 
+#[derive(PartialEq, Eq, Debug, Hash, HashStable, Clone, Copy)]
+pub enum GenerateProofTree {
+    Yes(UseGlobalCache),
+    No,
+}
+
+#[derive(PartialEq, Eq, Debug, Hash, HashStable, Clone, Copy)]
+pub enum UseGlobalCache {
+    Yes,
+    No,
+}
+impl UseGlobalCache {
+    pub fn from_bool(use_cache: bool) -> Self {
+        match use_cache {
+            true => UseGlobalCache::Yes,
+            false => UseGlobalCache::No,
+        }
+    }
+}
+
 pub trait InferCtxtEvalExt<'tcx> {
     /// Evaluates a goal from **outside** of the trait solver.
     ///
@@ -118,7 +141,11 @@ pub trait InferCtxtEvalExt<'tcx> {
     fn evaluate_root_goal(
         &self,
         goal: Goal<'tcx, ty::Predicate<'tcx>>,
-    ) -> Result<(bool, Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution>;
+        generate_proof_tree: GenerateProofTree,
+    ) -> (
+        Result<(bool, Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution>,
+        Option<inspect::GoalEvaluation<'tcx>>,
+    );
 }
 
 impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> {
@@ -126,16 +153,39 @@ impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> {
     fn evaluate_root_goal(
         &self,
         goal: Goal<'tcx, ty::Predicate<'tcx>>,
-    ) -> Result<(bool, Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution> {
-        let mode = if self.intercrate { SolverMode::Coherence } else { SolverMode::Normal };
-        let mut search_graph = search_graph::SearchGraph::new(self.tcx, mode);
+        generate_proof_tree: GenerateProofTree,
+    ) -> (
+        Result<(bool, Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution>,
+        Option<inspect::GoalEvaluation<'tcx>>,
+    ) {
+        EvalCtxt::enter_root(self, generate_proof_tree, |ecx| {
+            ecx.evaluate_goal(IsNormalizesToHack::No, goal)
+        })
+    }
+}
+
+impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
+    pub(super) fn solver_mode(&self) -> SolverMode {
+        self.search_graph.solver_mode()
+    }
+
+    /// 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>(
+        infcx: &InferCtxt<'tcx>,
+        generate_proof_tree: GenerateProofTree,
+        f: impl FnOnce(&mut EvalCtxt<'_, 'tcx>) -> R,
+    ) -> (R, Option<inspect::GoalEvaluation<'tcx>>) {
+        let mode = if infcx.intercrate { SolverMode::Coherence } else { SolverMode::Normal };
+        let mut search_graph = search_graph::SearchGraph::new(infcx.tcx, mode);
 
         let mut ecx = EvalCtxt {
             search_graph: &mut search_graph,
-            infcx: self,
+            infcx: infcx,
             // Only relevant when canonicalizing the response,
             // which we don't do within this evaluation context.
-            predefined_opaques_in_body: self
+            predefined_opaques_in_body: infcx
                 .tcx
                 .mk_predefined_opaques_in_body(PredefinedOpaquesData::default()),
             // Only relevant when canonicalizing the response.
@@ -143,8 +193,18 @@ impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> {
             var_values: CanonicalVarValues::dummy(),
             nested_goals: NestedGoals::new(),
             tainted: Ok(()),
+            inspect: ProofTreeBuilder::new_maybe_root(infcx.tcx, generate_proof_tree),
         };
-        let result = ecx.evaluate_goal(IsNormalizesToHack::No, goal);
+        let result = f(&mut ecx);
+
+        let tree = ecx.inspect.finalize();
+        if let (Some(tree), DumpSolverProofTree::Always) =
+            (&tree, infcx.tcx.sess.opts.unstable_opts.dump_solver_proof_tree)
+        {
+            let mut lock = std::io::stdout().lock();
+            let _ = lock.write_fmt(format_args!("{tree:?}"));
+            let _ = lock.flush();
+        }
 
         assert!(
             ecx.nested_goals.is_empty(),
@@ -152,13 +212,68 @@ impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> {
         );
 
         assert!(search_graph.is_empty());
-        result
+        (result, tree)
     }
-}
 
-impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
-    pub(super) fn solver_mode(&self) -> SolverMode {
-        self.search_graph.solver_mode()
+    /// Creates a nested evaluation context that shares the same search graph as the
+    /// one passed in. This is suitable for evaluation, granted that the search graph
+    /// has had the nested goal recorded on its stack ([`SearchGraph::with_new_goal`]),
+    /// but it's preferable to use other methods that call this one rather than this
+    /// method directly.
+    ///
+    /// This function takes care of setting up the inference context, setting the anchor,
+    /// and registering opaques from the canonicalized input.
+    fn enter_canonical<R>(
+        tcx: TyCtxt<'tcx>,
+        search_graph: &'a mut search_graph::SearchGraph<'tcx>,
+        canonical_input: CanonicalInput<'tcx>,
+        goal_evaluation: &mut ProofTreeBuilder<'tcx>,
+        f: impl FnOnce(&mut EvalCtxt<'_, 'tcx>, Goal<'tcx, ty::Predicate<'tcx>>) -> R,
+    ) -> R {
+        let intercrate = match search_graph.solver_mode() {
+            SolverMode::Normal => false,
+            SolverMode::Coherence => true,
+        };
+        let (ref infcx, input, var_values) = tcx
+            .infer_ctxt()
+            .intercrate(intercrate)
+            .with_next_trait_solver(true)
+            .with_opaque_type_inference(canonical_input.value.anchor)
+            .build_with_canonical(DUMMY_SP, &canonical_input);
+
+        let mut ecx = EvalCtxt {
+            infcx,
+            var_values,
+            predefined_opaques_in_body: input.predefined_opaques_in_body,
+            max_input_universe: canonical_input.max_universe,
+            search_graph,
+            nested_goals: NestedGoals::new(),
+            tainted: Ok(()),
+            inspect: goal_evaluation.new_goal_evaluation_step(input),
+        };
+
+        for &(key, ty) in &input.predefined_opaques_in_body.opaque_types {
+            ecx.insert_hidden_type(key, input.goal.param_env, ty)
+                .expect("failed to prepopulate opaque types");
+        }
+
+        if !ecx.nested_goals.is_empty() {
+            panic!("prepopulating opaque types shouldn't add goals: {:?}", ecx.nested_goals);
+        }
+
+        let result = f(&mut ecx, input.goal);
+
+        goal_evaluation.goal_evaluation_step(ecx.inspect);
+
+        // When creating a query response we clone the opaque type constraints
+        // instead of taking them. This would cause an ICE here, since we have
+        // assertions against dropping an `InferCtxt` without taking opaques.
+        // FIXME: Once we remove support for the old impl we can remove this.
+        if input.anchor != DefiningAnchor::Error {
+            let _ = infcx.take_opaque_types();
+        }
+
+        result
     }
 
     /// The entry point of the solver.
@@ -170,58 +285,36 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
     /// Instead of calling this function directly, use either [EvalCtxt::evaluate_goal]
     /// if you're inside of the solver or [InferCtxtEvalExt::evaluate_root_goal] if you're
     /// outside of it.
-    #[instrument(level = "debug", skip(tcx, search_graph), ret)]
+    #[instrument(level = "debug", skip(tcx, search_graph, goal_evaluation), ret)]
     fn evaluate_canonical_goal(
         tcx: TyCtxt<'tcx>,
         search_graph: &'a mut search_graph::SearchGraph<'tcx>,
         canonical_input: CanonicalInput<'tcx>,
+        mut goal_evaluation: &mut ProofTreeBuilder<'tcx>,
     ) -> QueryResult<'tcx> {
+        goal_evaluation.canonicalized_goal(canonical_input);
+
         // Deal with overflow, caching, and coinduction.
         //
         // The actual solver logic happens in `ecx.compute_goal`.
-        search_graph.with_new_goal(tcx, canonical_input, |search_graph| {
-            let intercrate = match search_graph.solver_mode() {
-                SolverMode::Normal => false,
-                SolverMode::Coherence => true,
-            };
-            let (ref infcx, input, var_values) = tcx
-                .infer_ctxt()
-                .intercrate(intercrate)
-                .with_opaque_type_inference(canonical_input.value.anchor)
-                .build_with_canonical(DUMMY_SP, &canonical_input);
-
-            for &(a, b) in &input.predefined_opaques_in_body.opaque_types {
-                let InferOk { value: (), obligations } = infcx
-                    .register_hidden_type_in_new_solver(a, input.goal.param_env, b)
-                    .expect("expected opaque type instantiation to succeed");
-                // We're only registering opaques already defined by the caller,
-                // so we're not responsible for proving that they satisfy their
-                // item bounds, unless we use them in a normalizes-to goal,
-                // which is handled in `EvalCtxt::unify_existing_opaque_tys`.
-                let _ = obligations;
-            }
-            let mut ecx = EvalCtxt {
-                infcx,
-                var_values,
-                predefined_opaques_in_body: input.predefined_opaques_in_body,
-                max_input_universe: canonical_input.max_universe,
-                search_graph,
-                nested_goals: NestedGoals::new(),
-                tainted: Ok(()),
-            };
-
-            let result = ecx.compute_goal(input.goal);
-
-            // When creating a query response we clone the opaque type constraints
-            // instead of taking them. This would cause an ICE here, since we have
-            // assertions against dropping an `InferCtxt` without taking opaques.
-            // FIXME: Once we remove support for the old impl we can remove this.
-            if input.anchor != DefiningAnchor::Error {
-                let _ = infcx.take_opaque_types();
-            }
-
-            result
-        })
+        search_graph.with_new_goal(
+            tcx,
+            canonical_input,
+            goal_evaluation,
+            |search_graph, goal_evaluation| {
+                EvalCtxt::enter_canonical(
+                    tcx,
+                    search_graph,
+                    canonical_input,
+                    goal_evaluation,
+                    |ecx, goal| {
+                        let result = ecx.compute_goal(goal);
+                        ecx.inspect.query_result(result);
+                        result
+                    },
+                )
+            },
+        )
     }
 
     /// Recursively evaluates `goal`, returning whether any inference vars have
@@ -232,16 +325,37 @@ 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 canonical_response =
-            EvalCtxt::evaluate_canonical_goal(self.tcx(), self.search_graph, canonical_goal)?;
+        let mut goal_evaluation = self.inspect.new_goal_evaluation(goal, is_normalizes_to_hack);
+        let canonical_response = EvalCtxt::evaluate_canonical_goal(
+            self.tcx(),
+            self.search_graph,
+            canonical_goal,
+            &mut goal_evaluation,
+        );
+        goal_evaluation.query_result(canonical_response);
+        let canonical_response = match canonical_response {
+            Err(e) => {
+                self.inspect.goal_evaluation(goal_evaluation);
+                return Err(e);
+            }
+            Ok(response) => response,
+        };
 
         let has_changed = !canonical_response.value.var_values.is_identity()
             || !canonical_response.value.external_constraints.opaque_types.is_empty();
-        let (certainty, nested_goals) = self.instantiate_and_apply_query_response(
+        let (certainty, nested_goals) = match self.instantiate_and_apply_query_response(
             goal.param_env,
             orig_values,
             canonical_response,
-        )?;
+        ) {
+            Err(e) => {
+                self.inspect.goal_evaluation(goal_evaluation);
+                return Err(e);
+            }
+            Ok(response) => response,
+        };
+        goal_evaluation.returned_goals(&nested_goals);
+        self.inspect.goal_evaluation(goal_evaluation);
 
         if !has_changed && !nested_goals.is_empty() {
             bug!("an unchanged goal shouldn't have any side-effects on instantiation");
@@ -261,9 +375,17 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
         {
             debug!("rerunning goal to check result is stable");
             let (_orig_values, canonical_goal) = self.canonicalize_goal(goal);
-            let new_canonical_response =
-                EvalCtxt::evaluate_canonical_goal(self.tcx(), self.search_graph, canonical_goal)?;
-            if !new_canonical_response.value.var_values.is_identity() {
+            let new_canonical_response = EvalCtxt::evaluate_canonical_goal(
+                self.tcx(),
+                self.search_graph,
+                canonical_goal,
+                // FIXME(-Ztrait-solver=next): we do not track what happens in `evaluate_canonical_goal`
+                &mut ProofTreeBuilder::new_noop(),
+            )?;
+            // We only check for modulo regions as we convert all regions in
+            // the input to new existentials, even if they're expected to be
+            // `'static` or a placeholder region.
+            if !new_canonical_response.value.var_values.is_identity_modulo_regions() {
                 bug!(
                     "unstable result: re-canonicalized goal={canonical_goal:#?} \
                     first_response={canonical_response:#?} \
@@ -287,19 +409,19 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
         let kind = predicate.kind();
         if let Some(kind) = kind.no_bound_vars() {
             match kind {
-                ty::PredicateKind::Clause(ty::Clause::Trait(predicate)) => {
+                ty::PredicateKind::Clause(ty::ClauseKind::Trait(predicate)) => {
                     self.compute_trait_goal(Goal { param_env, predicate })
                 }
-                ty::PredicateKind::Clause(ty::Clause::Projection(predicate)) => {
+                ty::PredicateKind::Clause(ty::ClauseKind::Projection(predicate)) => {
                     self.compute_projection_goal(Goal { param_env, predicate })
                 }
-                ty::PredicateKind::Clause(ty::Clause::TypeOutlives(predicate)) => {
+                ty::PredicateKind::Clause(ty::ClauseKind::TypeOutlives(predicate)) => {
                     self.compute_type_outlives_goal(Goal { param_env, predicate })
                 }
-                ty::PredicateKind::Clause(ty::Clause::RegionOutlives(predicate)) => {
+                ty::PredicateKind::Clause(ty::ClauseKind::RegionOutlives(predicate)) => {
                     self.compute_region_outlives_goal(Goal { param_env, predicate })
                 }
-                ty::PredicateKind::Clause(ty::Clause::ConstArgHasType(ct, ty)) => {
+                ty::PredicateKind::Clause(ty::ClauseKind::ConstArgHasType(ct, ty)) => {
                     self.compute_const_arg_has_type_goal(Goal { param_env, predicate: (ct, ty) })
                 }
                 ty::PredicateKind::Subtype(predicate) => {
@@ -316,24 +438,23 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
                 ty::PredicateKind::ObjectSafe(trait_def_id) => {
                     self.compute_object_safe_goal(trait_def_id)
                 }
-                ty::PredicateKind::WellFormed(arg) => {
+                ty::PredicateKind::Clause(ty::ClauseKind::WellFormed(arg)) => {
                     self.compute_well_formed_goal(Goal { param_env, predicate: arg })
                 }
-                ty::PredicateKind::Ambiguous => {
-                    self.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS)
-                }
-                // FIXME: implement these predicates :)
-                ty::PredicateKind::ConstEvaluatable(_) | ty::PredicateKind::ConstEquate(_, _) => {
-                    self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
+                ty::PredicateKind::Clause(ty::ClauseKind::ConstEvaluatable(ct)) => {
+                    self.compute_const_evaluatable_goal(Goal { param_env, predicate: ct })
                 }
-                ty::PredicateKind::TypeWellFormedFromEnv(..) => {
-                    bug!("TypeWellFormedFromEnv is only used for Chalk")
+                ty::PredicateKind::ConstEquate(_, _) => {
+                    bug!("ConstEquate should not be emitted when `-Ztrait-solver=next` is active")
                 }
                 ty::PredicateKind::AliasRelate(lhs, rhs, direction) => self
                     .compute_alias_relate_goal(Goal {
                         param_env,
                         predicate: (lhs, rhs, direction),
                     }),
+                ty::PredicateKind::Ambiguous => {
+                    self.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS)
+                }
             }
         } else {
             let kind = self.infcx.instantiate_binder_with_placeholders(kind);
@@ -347,12 +468,17 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
     // 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);
+
         let mut goals = core::mem::replace(&mut self.nested_goals, NestedGoals::new());
         let mut new_goals = NestedGoals::new();
 
         let response = self.repeat_while_none(
             |_| Ok(Certainty::Maybe(MaybeCause::Overflow)),
             |this| {
+                this.inspect.evaluate_added_goals_loop_start();
+
                 let mut has_changed = Err(Certainty::Yes);
 
                 if let Some(goal) = goals.normalizes_to_hack_goal.take() {
@@ -441,29 +567,21 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
             },
         );
 
+        self.inspect.eval_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);
+
         self.nested_goals = goals;
         response
     }
 }
 
 impl<'tcx> EvalCtxt<'_, 'tcx> {
-    pub(super) fn probe<T>(&mut self, f: impl FnOnce(&mut EvalCtxt<'_, 'tcx>) -> T) -> T {
-        let mut ecx = EvalCtxt {
-            infcx: self.infcx,
-            var_values: self.var_values,
-            predefined_opaques_in_body: self.predefined_opaques_in_body,
-            max_input_universe: self.max_input_universe,
-            search_graph: self.search_graph,
-            nested_goals: self.nested_goals.clone(),
-            tainted: self.tainted,
-        };
-        self.infcx.probe(|_| f(&mut ecx))
-    }
-
     pub(super) fn tcx(&self) -> TyCtxt<'tcx> {
         self.infcx.tcx
     }
@@ -706,6 +824,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
         scope: Ty<'tcx>,
         assume: rustc_transmute::Assume,
     ) -> Result<Certainty, NoSolution> {
+        use rustc_transmute::Answer;
         // FIXME(transmutability): This really should be returning nested goals for `Answer::If*`
         match rustc_transmute::TransmuteTypeEnv::new(self.infcx).is_transmutable(
             ObligationCause::dummy(),
@@ -713,30 +832,53 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
             scope,
             assume,
         ) {
-            rustc_transmute::Answer::Yes => Ok(Certainty::Yes),
-            rustc_transmute::Answer::No(_)
-            | rustc_transmute::Answer::IfTransmutable { .. }
-            | rustc_transmute::Answer::IfAll(_)
-            | rustc_transmute::Answer::IfAny(_) => Err(NoSolution),
+            Answer::Yes => Ok(Certainty::Yes),
+            Answer::No(_) | Answer::If(_) => Err(NoSolution),
         }
     }
 
-    pub(super) fn can_define_opaque_ty(&mut self, def_id: LocalDefId) -> bool {
+    pub(super) fn can_define_opaque_ty(&self, def_id: LocalDefId) -> bool {
         self.infcx.opaque_type_origin(def_id).is_some()
     }
 
-    pub(super) fn register_opaque_ty(
+    pub(super) fn insert_hidden_type(
         &mut self,
-        a: ty::OpaqueTypeKey<'tcx>,
-        b: Ty<'tcx>,
+        opaque_type_key: OpaqueTypeKey<'tcx>,
         param_env: ty::ParamEnv<'tcx>,
+        hidden_ty: Ty<'tcx>,
     ) -> Result<(), NoSolution> {
-        let InferOk { value: (), obligations } =
-            self.infcx.register_hidden_type_in_new_solver(a, param_env, b)?;
-        self.add_goals(obligations.into_iter().map(|obligation| obligation.into()));
+        let mut obligations = Vec::new();
+        self.infcx.insert_hidden_type(
+            opaque_type_key,
+            &ObligationCause::dummy(),
+            param_env,
+            hidden_ty,
+            true,
+            &mut obligations,
+        )?;
+        self.add_goals(obligations.into_iter().map(|o| o.into()));
         Ok(())
     }
 
+    pub(super) fn add_item_bounds_for_hidden_type(
+        &mut self,
+        opaque_def_id: DefId,
+        opaque_substs: ty::SubstsRef<'tcx>,
+        param_env: ty::ParamEnv<'tcx>,
+        hidden_ty: Ty<'tcx>,
+    ) {
+        let mut obligations = Vec::new();
+        self.infcx.add_item_bounds_for_hidden_type(
+            opaque_def_id,
+            opaque_substs,
+            ObligationCause::dummy(),
+            param_env,
+            hidden_ty,
+            &mut obligations,
+        );
+        self.add_goals(obligations.into_iter().map(|o| o.into()));
+    }
+
     // Do something for each opaque/hidden pair defined with `def_id` in the
     // current inference context.
     pub(super) fn unify_existing_opaque_tys(
@@ -753,23 +895,37 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
             if candidate_key.def_id != key.def_id {
                 continue;
             }
-            values.extend(self.probe(|ecx| {
+            values.extend(self.probe_candidate("opaque type storage").enter(|ecx| {
                 for (a, b) in std::iter::zip(candidate_key.substs, key.substs) {
                     ecx.eq(param_env, a, b)?;
                 }
                 ecx.eq(param_env, candidate_ty, ty)?;
-                let mut obl = vec![];
-                ecx.infcx.add_item_bounds_for_hidden_type(
-                    candidate_key,
-                    ObligationCause::dummy(),
+                ecx.add_item_bounds_for_hidden_type(
+                    candidate_key.def_id.to_def_id(),
+                    candidate_key.substs,
                     param_env,
                     candidate_ty,
-                    &mut obl,
                 );
-                ecx.add_goals(obl.into_iter().map(Into::into));
                 ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
             }));
         }
         values
     }
+
+    // Try to evaluate a const, or return `None` if the const is too generic.
+    // This doesn't mean the const isn't evaluatable, though, and should be treated
+    // as an ambiguity rather than no-solution.
+    pub(super) fn try_const_eval_resolve(
+        &self,
+        param_env: ty::ParamEnv<'tcx>,
+        unevaluated: ty::UnevaluatedConst<'tcx>,
+        ty: Ty<'tcx>,
+    ) -> Option<ty::Const<'tcx>> {
+        use rustc_middle::mir::interpret::ErrorHandled;
+        match self.infcx.try_const_eval_resolve(param_env, unevaluated, ty, None) {
+            Ok(ct) => Some(ct),
+            Err(ErrorHandled::Reported(e)) => Some(ty::Const::new_error(self.tcx(), e.into(), ty)),
+            Err(ErrorHandled::TooGeneric) => None,
+        }
+    }
 }
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 fdb209fbf..637d45888 100644
--- a/compiler/rustc_trait_selection/src/solve/eval_ctxt/canonical.rs
+++ b/compiler/rustc_trait_selection/src/solve/eval_ctxt/canonical.rs
@@ -11,16 +11,16 @@
 use super::{CanonicalInput, Certainty, EvalCtxt, Goal};
 use crate::solve::canonicalize::{CanonicalizeMode, Canonicalizer};
 use crate::solve::{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::InferOk;
 use rustc_middle::traits::query::NoSolution;
 use rustc_middle::traits::solve::{
     ExternalConstraints, ExternalConstraintsData, MaybeCause, PredefinedOpaquesData, QueryInput,
 };
-use rustc_middle::ty::{self, BoundVar, GenericArgKind, Ty};
+use rustc_middle::ty::{self, BoundVar, GenericArgKind, Ty, TyCtxt, TypeFoldable};
 use rustc_span::DUMMY_SP;
 use std::iter;
 use std::ops::Deref;
@@ -28,10 +28,10 @@ use std::ops::Deref;
 impl<'tcx> EvalCtxt<'_, 'tcx> {
     /// Canonicalizes the goal remembering the original values
     /// for each bound variable.
-    pub(super) fn canonicalize_goal(
+    pub(super) fn canonicalize_goal<T: TypeFoldable<TyCtxt<'tcx>>>(
         &self,
-        goal: Goal<'tcx, ty::Predicate<'tcx>>,
-    ) -> (Vec<ty::GenericArg<'tcx>>, CanonicalInput<'tcx>) {
+        goal: Goal<'tcx, T>,
+    ) -> (Vec<ty::GenericArg<'tcx>>, CanonicalInput<'tcx, T>) {
         let mut orig_values = Default::default();
         let canonical_goal = Canonicalizer::canonicalize(
             self.infcx,
@@ -137,10 +137,17 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
 
     #[instrument(level = "debug", skip(self), ret)]
     fn compute_external_query_constraints(&self) -> Result<ExternalConstraints<'tcx>, NoSolution> {
+        // We only check for leaks from universes which were entered inside
+        // of the query.
+        self.infcx.leak_check(self.max_input_universe, None).map_err(|e| {
+            debug!(?e, "failed the leak check");
+            NoSolution
+        })?;
+
         // Cannot use `take_registered_region_obligations` as we may compute the response
         // inside of a `probe` whenever we have multiple choices inside of the solver.
         let region_obligations = self.infcx.inner.borrow().region_obligations().to_owned();
-        let region_constraints = self.infcx.with_region_constraints(|region_constraints| {
+        let mut region_constraints = self.infcx.with_region_constraints(|region_constraints| {
             make_query_region_constraints(
                 self.tcx(),
                 region_obligations
@@ -150,6 +157,9 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
             )
         });
 
+        let mut seen = FxHashSet::default();
+        region_constraints.outlives.retain(|outlives| seen.insert(*outlives));
+
         let mut opaque_types = self.infcx.clone_opaque_types_for_query_response();
         // Only return opaque type keys for newly-defined opaques
         opaque_types.retain(|(a, _)| {
@@ -310,12 +320,8 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
         param_env: ty::ParamEnv<'tcx>,
         opaque_types: &[(ty::OpaqueTypeKey<'tcx>, Ty<'tcx>)],
     ) -> Result<(), NoSolution> {
-        for &(a, b) in opaque_types {
-            let InferOk { value: (), obligations } =
-                self.infcx.register_hidden_type_in_new_solver(a, param_env, b)?;
-            // It's sound to drop these obligations, since the normalizes-to goal
-            // is responsible for proving these obligations.
-            let _ = obligations;
+        for &(key, ty) in opaque_types {
+            self.insert_hidden_type(key, param_env, ty)?;
         }
         Ok(())
     }
diff --git a/compiler/rustc_trait_selection/src/solve/eval_ctxt/probe.rs b/compiler/rustc_trait_selection/src/solve/eval_ctxt/probe.rs
new file mode 100644
index 000000000..4477ea7d5
--- /dev/null
+++ b/compiler/rustc_trait_selection/src/solve/eval_ctxt/probe.rs
@@ -0,0 +1,67 @@
+use super::EvalCtxt;
+use rustc_middle::traits::solve::{inspect, QueryResult};
+use std::marker::PhantomData;
+
+pub(in crate::solve) struct ProbeCtxt<'me, 'a, 'tcx, F, T> {
+    ecx: &'me mut EvalCtxt<'a, 'tcx>,
+    probe_kind: F,
+    _result: PhantomData<T>,
+}
+
+impl<'tcx, F, T> ProbeCtxt<'_, '_, 'tcx, F, T>
+where
+    F: FnOnce(&T) -> inspect::CandidateKind<'tcx>,
+{
+    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 mut nested_ecx = EvalCtxt {
+            infcx: outer_ecx.infcx,
+            var_values: outer_ecx.var_values,
+            predefined_opaques_in_body: outer_ecx.predefined_opaques_in_body,
+            max_input_universe: outer_ecx.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_goal_candidate(),
+        };
+        let r = nested_ecx.infcx.probe(|_| f(&mut nested_ecx));
+        if !outer_ecx.inspect.is_noop() {
+            let cand_kind = probe_kind(&r);
+            nested_ecx.inspect.candidate_kind(cand_kind);
+            outer_ecx.inspect.goal_candidate(nested_ecx.inspect);
+        }
+        r
+    }
+}
+
+impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
+    /// `probe_kind` is only called when proof tree building is enabled so it can be
+    /// as expensive as necessary to output the desired information.
+    pub(in crate::solve) fn probe<F, T>(&mut self, probe_kind: F) -> ProbeCtxt<'_, 'a, 'tcx, F, T>
+    where
+        F: FnOnce(&T) -> inspect::CandidateKind<'tcx>,
+    {
+        ProbeCtxt { ecx: self, probe_kind, _result: PhantomData }
+    }
+
+    pub(in crate::solve) fn probe_candidate(
+        &mut self,
+        name: &'static str,
+    ) -> ProbeCtxt<
+        '_,
+        'a,
+        'tcx,
+        impl FnOnce(&QueryResult<'tcx>) -> inspect::CandidateKind<'tcx>,
+        QueryResult<'tcx>,
+    > {
+        ProbeCtxt {
+            ecx: self,
+            probe_kind: move |result: &QueryResult<'tcx>| inspect::CandidateKind::Candidate {
+                name: name.to_string(),
+                result: *result,
+            },
+            _result: PhantomData,
+        }
+    }
+}
diff --git a/compiler/rustc_trait_selection/src/solve/eval_ctxt/select.rs b/compiler/rustc_trait_selection/src/solve/eval_ctxt/select.rs
new file mode 100644
index 000000000..bf6cbef8c
--- /dev/null
+++ b/compiler/rustc_trait_selection/src/solve/eval_ctxt/select.rs
@@ -0,0 +1,307 @@
+use std::ops::ControlFlow;
+
+use rustc_hir::def_id::DefId;
+use rustc_infer::infer::{DefineOpaqueTypes, InferCtxt, InferOk};
+use rustc_infer::traits::util::supertraits;
+use rustc_infer::traits::{
+    Obligation, PolyTraitObligation, PredicateObligation, Selection, SelectionResult,
+};
+use rustc_middle::traits::solve::{CanonicalInput, Certainty, Goal};
+use rustc_middle::traits::{
+    ImplSource, ImplSourceObjectData, ImplSourceTraitUpcastingData, ImplSourceUserDefinedData,
+    ObligationCause, SelectionError,
+};
+use rustc_middle::ty::{self, TyCtxt};
+use rustc_span::DUMMY_SP;
+
+use crate::solve::assembly::{BuiltinImplSource, Candidate, CandidateSource};
+use crate::solve::eval_ctxt::{EvalCtxt, GenerateProofTree};
+use crate::solve::inspect::ProofTreeBuilder;
+use crate::solve::search_graph::OverflowHandler;
+use crate::traits::vtable::{count_own_vtable_entries, prepare_vtable_segments, VtblSegment};
+
+pub trait InferCtxtSelectExt<'tcx> {
+    fn select_in_new_trait_solver(
+        &self,
+        obligation: &PolyTraitObligation<'tcx>,
+    ) -> SelectionResult<'tcx, Selection<'tcx>>;
+}
+
+impl<'tcx> InferCtxtSelectExt<'tcx> for InferCtxt<'tcx> {
+    fn select_in_new_trait_solver(
+        &self,
+        obligation: &PolyTraitObligation<'tcx>,
+    ) -> SelectionResult<'tcx, Selection<'tcx>> {
+        assert!(self.next_trait_solver());
+
+        let trait_goal = Goal::new(
+            self.tcx,
+            obligation.param_env,
+            self.instantiate_binder_with_placeholders(obligation.predicate),
+        );
+
+        let (result, _) = EvalCtxt::enter_root(self, GenerateProofTree::No, |ecx| {
+            let goal = Goal::new(ecx.tcx(), trait_goal.param_env, trait_goal.predicate);
+            let (orig_values, canonical_goal) = ecx.canonicalize_goal(goal);
+            let mut candidates = ecx.compute_canonical_trait_candidates(canonical_goal);
+
+            // pseudo-winnow
+            if candidates.len() == 0 {
+                return Err(SelectionError::Unimplemented);
+            } else if candidates.len() > 1 {
+                let mut i = 0;
+                while i < candidates.len() {
+                    let should_drop_i = (0..candidates.len()).filter(|&j| i != j).any(|j| {
+                        candidate_should_be_dropped_in_favor_of(
+                            ecx.tcx(),
+                            &candidates[i],
+                            &candidates[j],
+                        )
+                    });
+                    if should_drop_i {
+                        candidates.swap_remove(i);
+                    } else {
+                        i += 1;
+                        if i > 1 {
+                            return Ok(None);
+                        }
+                    }
+                }
+            }
+
+            let candidate = candidates.pop().unwrap();
+            let (certainty, nested_goals) = ecx
+                .instantiate_and_apply_query_response(
+                    trait_goal.param_env,
+                    orig_values,
+                    candidate.result,
+                )
+                .map_err(|_| SelectionError::Unimplemented)?;
+
+            Ok(Some((candidate, certainty, nested_goals)))
+        });
+
+        let (candidate, certainty, nested_goals) = match result {
+            Ok(Some((candidate, certainty, nested_goals))) => (candidate, certainty, nested_goals),
+            Ok(None) => return Ok(None),
+            Err(e) => return Err(e),
+        };
+
+        let nested_obligations: Vec<_> = nested_goals
+            .into_iter()
+            .map(|goal| {
+                Obligation::new(self.tcx, ObligationCause::dummy(), goal.param_env, goal.predicate)
+            })
+            .collect();
+
+        let goal = self.resolve_vars_if_possible(trait_goal);
+        match (certainty, candidate.source) {
+            // Rematching the implementation will instantiate the same nested goals that
+            // would have caused the ambiguity, so we can still make progress here regardless.
+            (_, CandidateSource::Impl(def_id)) => {
+                rematch_impl(self, goal, def_id, nested_obligations)
+            }
+
+            // Rematching the dyn upcast or object goal will instantiate the same nested
+            // goals that would have caused the ambiguity, so we can still make progress here
+            // regardless.
+            // FIXME: This doesn't actually check the object bounds hold here.
+            (
+                _,
+                CandidateSource::BuiltinImpl(
+                    BuiltinImplSource::Object | BuiltinImplSource::TraitUpcasting,
+                ),
+            ) => rematch_object(self, goal, nested_obligations),
+
+            // Technically some builtin impls have nested obligations, but if
+            // `Certainty::Yes`, then they should've all been verified and don't
+            // need re-checking.
+            (Certainty::Yes, CandidateSource::BuiltinImpl(BuiltinImplSource::Misc)) => {
+                Ok(Some(ImplSource::Builtin(nested_obligations)))
+            }
+
+            // It's fine not to do anything to rematch these, since there are no
+            // nested obligations.
+            (Certainty::Yes, CandidateSource::ParamEnv(_) | CandidateSource::AliasBound) => {
+                Ok(Some(ImplSource::Param(nested_obligations, ty::BoundConstness::NotConst)))
+            }
+
+            (_, CandidateSource::BuiltinImpl(BuiltinImplSource::Ambiguity))
+            | (Certainty::Maybe(_), _) => Ok(None),
+        }
+    }
+}
+
+impl<'tcx> EvalCtxt<'_, 'tcx> {
+    fn compute_canonical_trait_candidates(
+        &mut self,
+        canonical_input: CanonicalInput<'tcx>,
+    ) -> Vec<Candidate<'tcx>> {
+        // This doesn't record the canonical goal on the stack during the
+        // candidate assembly step, but that's fine. Selection is conceptually
+        // outside of the solver, and if there were any cycles, we'd encounter
+        // the cycle anyways one step later.
+        EvalCtxt::enter_canonical(
+            self.tcx(),
+            self.search_graph(),
+            canonical_input,
+            // FIXME: This is wrong, idk if we even want to track stuff here.
+            &mut ProofTreeBuilder::new_noop(),
+            |ecx, goal| {
+                let trait_goal = Goal {
+                    param_env: goal.param_env,
+                    predicate: goal
+                        .predicate
+                        .to_opt_poly_trait_pred()
+                        .expect("we canonicalized a trait goal")
+                        .no_bound_vars()
+                        .expect("we instantiated all bound vars"),
+                };
+                ecx.assemble_and_evaluate_candidates(trait_goal)
+            },
+        )
+    }
+}
+
+fn candidate_should_be_dropped_in_favor_of<'tcx>(
+    tcx: TyCtxt<'tcx>,
+    victim: &Candidate<'tcx>,
+    other: &Candidate<'tcx>,
+) -> bool {
+    match (victim.source, other.source) {
+        (CandidateSource::ParamEnv(victim_idx), CandidateSource::ParamEnv(other_idx)) => {
+            victim_idx >= other_idx
+        }
+        (_, CandidateSource::ParamEnv(_)) => true,
+
+        (
+            CandidateSource::BuiltinImpl(BuiltinImplSource::Object),
+            CandidateSource::BuiltinImpl(BuiltinImplSource::Object),
+        ) => false,
+        (_, CandidateSource::BuiltinImpl(BuiltinImplSource::Object)) => true,
+
+        (CandidateSource::Impl(victim_def_id), CandidateSource::Impl(other_def_id)) => {
+            tcx.specializes((other_def_id, victim_def_id))
+                && other.result.value.certainty == Certainty::Yes
+        }
+
+        _ => false,
+    }
+}
+
+fn rematch_impl<'tcx>(
+    infcx: &InferCtxt<'tcx>,
+    goal: Goal<'tcx, ty::TraitPredicate<'tcx>>,
+    impl_def_id: DefId,
+    mut nested: Vec<PredicateObligation<'tcx>>,
+) -> SelectionResult<'tcx, Selection<'tcx>> {
+    let substs = infcx.fresh_substs_for_item(DUMMY_SP, impl_def_id);
+    let impl_trait_ref = infcx.tcx.impl_trait_ref(impl_def_id).unwrap().subst(infcx.tcx, substs);
+
+    nested.extend(
+        infcx
+            .at(&ObligationCause::dummy(), goal.param_env)
+            .eq(DefineOpaqueTypes::No, goal.predicate.trait_ref, impl_trait_ref)
+            .map_err(|_| SelectionError::Unimplemented)?
+            .into_obligations(),
+    );
+
+    nested.extend(
+        infcx.tcx.predicates_of(impl_def_id).instantiate(infcx.tcx, substs).into_iter().map(
+            |(pred, _)| Obligation::new(infcx.tcx, ObligationCause::dummy(), goal.param_env, pred),
+        ),
+    );
+
+    Ok(Some(ImplSource::UserDefined(ImplSourceUserDefinedData { impl_def_id, substs, nested })))
+}
+
+fn rematch_object<'tcx>(
+    infcx: &InferCtxt<'tcx>,
+    goal: Goal<'tcx, ty::TraitPredicate<'tcx>>,
+    mut nested: Vec<PredicateObligation<'tcx>>,
+) -> SelectionResult<'tcx, Selection<'tcx>> {
+    let self_ty = goal.predicate.self_ty();
+    let ty::Dynamic(data, _, source_kind) = *self_ty.kind()
+    else {
+        bug!()
+    };
+    let source_trait_ref = data.principal().unwrap().with_self_ty(infcx.tcx, self_ty);
+
+    let (is_upcasting, target_trait_ref_unnormalized) = if Some(goal.predicate.def_id())
+        == infcx.tcx.lang_items().unsize_trait()
+    {
+        assert_eq!(source_kind, ty::Dyn, "cannot upcast dyn*");
+        if let ty::Dynamic(data, _, ty::Dyn) = goal.predicate.trait_ref.substs.type_at(1).kind() {
+            (true, data.principal().unwrap().with_self_ty(infcx.tcx, self_ty))
+        } else {
+            bug!()
+        }
+    } else {
+        (false, ty::Binder::dummy(goal.predicate.trait_ref))
+    };
+
+    let mut target_trait_ref = None;
+    for candidate_trait_ref in supertraits(infcx.tcx, source_trait_ref) {
+        let result = infcx.commit_if_ok(|_| {
+            infcx.at(&ObligationCause::dummy(), goal.param_env).eq(
+                DefineOpaqueTypes::No,
+                target_trait_ref_unnormalized,
+                candidate_trait_ref,
+            )
+
+            // FIXME: We probably should at least shallowly verify these...
+        });
+
+        match result {
+            Ok(InferOk { value: (), obligations }) => {
+                target_trait_ref = Some(candidate_trait_ref);
+                nested.extend(obligations);
+                break;
+            }
+            Err(_) => continue,
+        }
+    }
+
+    let target_trait_ref = target_trait_ref.unwrap();
+
+    let mut offset = 0;
+    let Some((vtable_base, vtable_vptr_slot)) =
+        prepare_vtable_segments(infcx.tcx, source_trait_ref, |segment| {
+            match segment {
+                VtblSegment::MetadataDSA => {
+                    offset += TyCtxt::COMMON_VTABLE_ENTRIES.len();
+                }
+                VtblSegment::TraitOwnEntries { trait_ref, emit_vptr } => {
+                    let own_vtable_entries = count_own_vtable_entries(infcx.tcx, trait_ref);
+
+                    if trait_ref == target_trait_ref {
+                        if emit_vptr {
+                            return ControlFlow::Break((
+                                offset,
+                                Some(offset + count_own_vtable_entries(infcx.tcx, trait_ref)),
+                            ));
+                        } else {
+                            return ControlFlow::Break((offset, None));
+                        }
+                    }
+
+                    offset += own_vtable_entries;
+                    if emit_vptr {
+                        offset += 1;
+                    }
+                }
+            }
+            ControlFlow::Continue(())
+        })
+    else {
+        bug!();
+    };
+
+    // If we're upcasting, get the offset of the vtable pointer, otherwise get
+    // the base of the vtable.
+    Ok(Some(if is_upcasting {
+        ImplSource::TraitUpcasting(ImplSourceTraitUpcastingData { vtable_vptr_slot, nested })
+    } else {
+        ImplSource::Object(ImplSourceObjectData { vtable_base, nested })
+    }))
+}
diff --git a/compiler/rustc_trait_selection/src/solve/fulfill.rs b/compiler/rustc_trait_selection/src/solve/fulfill.rs
index 4a403196c..88ee14c4d 100644
--- a/compiler/rustc_trait_selection/src/solve/fulfill.rs
+++ b/compiler/rustc_trait_selection/src/solve/fulfill.rs
@@ -10,6 +10,7 @@ use rustc_infer::traits::{
 use rustc_middle::ty;
 use rustc_middle::ty::error::{ExpectedFound, TypeError};
 
+use super::eval_ctxt::GenerateProofTree;
 use super::{Certainty, InferCtxtEvalExt};
 
 /// A trait engine using the new trait solver.
@@ -25,20 +26,28 @@ use super::{Certainty, InferCtxtEvalExt};
 /// here as this will have to deal with far more root goals than `evaluate_all`.
 pub struct FulfillmentCtxt<'tcx> {
     obligations: Vec<PredicateObligation<'tcx>>,
+
+    /// The snapshot in which this context was created. Using the context
+    /// outside of this snapshot leads to subtle bugs if the snapshot
+    /// gets rolled back. Because of this we explicitly check that we only
+    /// use the context in exactly this snapshot.
+    usable_in_snapshot: usize,
 }
 
 impl<'tcx> FulfillmentCtxt<'tcx> {
-    pub fn new() -> FulfillmentCtxt<'tcx> {
-        FulfillmentCtxt { obligations: Vec::new() }
+    pub fn new(infcx: &InferCtxt<'tcx>) -> FulfillmentCtxt<'tcx> {
+        FulfillmentCtxt { obligations: Vec::new(), usable_in_snapshot: infcx.num_open_snapshots() }
     }
 }
 
 impl<'tcx> TraitEngine<'tcx> for FulfillmentCtxt<'tcx> {
+    #[instrument(level = "debug", skip(self, infcx))]
     fn register_predicate_obligation(
         &mut self,
-        _infcx: &InferCtxt<'tcx>,
+        infcx: &InferCtxt<'tcx>,
         obligation: PredicateObligation<'tcx>,
     ) {
+        assert_eq!(self.usable_in_snapshot, infcx.num_open_snapshots());
         self.obligations.push(obligation);
     }
 
@@ -46,8 +55,11 @@ impl<'tcx> TraitEngine<'tcx> for FulfillmentCtxt<'tcx> {
         self.obligations
             .drain(..)
             .map(|obligation| {
-                let code =
-                    infcx.probe(|_| match infcx.evaluate_root_goal(obligation.clone().into()) {
+                let code = infcx.probe(|_| {
+                    match infcx
+                        .evaluate_root_goal(obligation.clone().into(), GenerateProofTree::No)
+                        .0
+                    {
                         Ok((_, Certainty::Maybe(MaybeCause::Ambiguity), _)) => {
                             FulfillmentErrorCode::CodeAmbiguity { overflow: false }
                         }
@@ -60,7 +72,8 @@ impl<'tcx> TraitEngine<'tcx> for FulfillmentCtxt<'tcx> {
                         Err(_) => {
                             bug!("did not expect selection error when collecting ambiguity errors")
                         }
-                    });
+                    }
+                });
 
                 FulfillmentError {
                     obligation: obligation.clone(),
@@ -72,6 +85,7 @@ impl<'tcx> TraitEngine<'tcx> for FulfillmentCtxt<'tcx> {
     }
 
     fn select_where_possible(&mut self, infcx: &InferCtxt<'tcx>) -> Vec<FulfillmentError<'tcx>> {
+        assert_eq!(self.usable_in_snapshot, infcx.num_open_snapshots());
         let mut errors = Vec::new();
         for i in 0.. {
             if !infcx.tcx.recursion_limit().value_within_limit(i) {
@@ -81,72 +95,61 @@ impl<'tcx> TraitEngine<'tcx> for FulfillmentCtxt<'tcx> {
             let mut has_changed = false;
             for obligation in mem::take(&mut self.obligations) {
                 let goal = obligation.clone().into();
-                let (changed, certainty, nested_goals) = match infcx.evaluate_root_goal(goal) {
-                    Ok(result) => result,
-                    Err(NoSolution) => {
-                        errors.push(FulfillmentError {
-                            obligation: obligation.clone(),
-                            code: match goal.predicate.kind().skip_binder() {
-                                ty::PredicateKind::Clause(ty::Clause::Projection(_)) => {
-                                    FulfillmentErrorCode::CodeProjectionError(
-                                        // FIXME: This could be a `Sorts` if the term is a type
-                                        MismatchedProjectionTypes { err: TypeError::Mismatch },
-                                    )
-                                }
-                                ty::PredicateKind::AliasRelate(_, _, _) => {
-                                    FulfillmentErrorCode::CodeProjectionError(
-                                        MismatchedProjectionTypes { err: TypeError::Mismatch },
-                                    )
-                                }
-                                ty::PredicateKind::Subtype(pred) => {
-                                    let (a, b) = infcx.instantiate_binder_with_placeholders(
-                                        goal.predicate.kind().rebind((pred.a, pred.b)),
-                                    );
-                                    let expected_found = ExpectedFound::new(true, a, b);
-                                    FulfillmentErrorCode::CodeSubtypeError(
-                                        expected_found,
-                                        TypeError::Sorts(expected_found),
-                                    )
-                                }
-                                ty::PredicateKind::Coerce(pred) => {
-                                    let (a, b) = infcx.instantiate_binder_with_placeholders(
-                                        goal.predicate.kind().rebind((pred.a, pred.b)),
-                                    );
-                                    let expected_found = ExpectedFound::new(false, a, b);
-                                    FulfillmentErrorCode::CodeSubtypeError(
-                                        expected_found,
-                                        TypeError::Sorts(expected_found),
-                                    )
-                                }
-                                ty::PredicateKind::ConstEquate(a, b) => {
-                                    let (a, b) = infcx.instantiate_binder_with_placeholders(
-                                        goal.predicate.kind().rebind((a, b)),
-                                    );
-                                    let expected_found = ExpectedFound::new(true, a, b);
-                                    FulfillmentErrorCode::CodeConstEquateError(
-                                        expected_found,
-                                        TypeError::ConstMismatch(expected_found),
-                                    )
-                                }
-                                ty::PredicateKind::Clause(_)
-                                | ty::PredicateKind::WellFormed(_)
-                                | ty::PredicateKind::ObjectSafe(_)
-                                | ty::PredicateKind::ClosureKind(_, _, _)
-                                | ty::PredicateKind::ConstEvaluatable(_)
-                                | ty::PredicateKind::Ambiguous => {
-                                    FulfillmentErrorCode::CodeSelectionError(
-                                        SelectionError::Unimplemented,
-                                    )
-                                }
-                                ty::PredicateKind::TypeWellFormedFromEnv(_) => {
-                                    bug!("unexpected goal: {goal:?}")
-                                }
-                            },
-                            root_obligation: obligation,
-                        });
-                        continue;
-                    }
-                };
+                let (changed, certainty, nested_goals) =
+                    match infcx.evaluate_root_goal(goal, GenerateProofTree::No).0 {
+                        Ok(result) => result,
+                        Err(NoSolution) => {
+                            errors.push(FulfillmentError {
+                                obligation: obligation.clone(),
+                                code: match goal.predicate.kind().skip_binder() {
+                                    ty::PredicateKind::Clause(ty::ClauseKind::Projection(_)) => {
+                                        FulfillmentErrorCode::CodeProjectionError(
+                                            // FIXME: This could be a `Sorts` if the term is a type
+                                            MismatchedProjectionTypes { err: TypeError::Mismatch },
+                                        )
+                                    }
+                                    ty::PredicateKind::AliasRelate(_, _, _) => {
+                                        FulfillmentErrorCode::CodeProjectionError(
+                                            MismatchedProjectionTypes { err: TypeError::Mismatch },
+                                        )
+                                    }
+                                    ty::PredicateKind::Subtype(pred) => {
+                                        let (a, b) = infcx.instantiate_binder_with_placeholders(
+                                            goal.predicate.kind().rebind((pred.a, pred.b)),
+                                        );
+                                        let expected_found = ExpectedFound::new(true, a, b);
+                                        FulfillmentErrorCode::CodeSubtypeError(
+                                            expected_found,
+                                            TypeError::Sorts(expected_found),
+                                        )
+                                    }
+                                    ty::PredicateKind::Coerce(pred) => {
+                                        let (a, b) = infcx.instantiate_binder_with_placeholders(
+                                            goal.predicate.kind().rebind((pred.a, pred.b)),
+                                        );
+                                        let expected_found = ExpectedFound::new(false, a, b);
+                                        FulfillmentErrorCode::CodeSubtypeError(
+                                            expected_found,
+                                            TypeError::Sorts(expected_found),
+                                        )
+                                    }
+                                    ty::PredicateKind::Clause(_)
+                                    | ty::PredicateKind::ObjectSafe(_)
+                                    | ty::PredicateKind::ClosureKind(_, _, _)
+                                    | ty::PredicateKind::Ambiguous => {
+                                        FulfillmentErrorCode::CodeSelectionError(
+                                            SelectionError::Unimplemented,
+                                        )
+                                    }
+                                    ty::PredicateKind::ConstEquate(..) => {
+                                        bug!("unexpected goal: {goal:?}")
+                                    }
+                                },
+                                root_obligation: obligation,
+                            });
+                            continue;
+                        }
+                    };
                 // Push any nested goals that we get from unifying our canonical response
                 // with our obligation onto the fulfillment context.
                 self.obligations.extend(nested_goals.into_iter().map(|goal| {
diff --git a/compiler/rustc_trait_selection/src/solve/inspect.rs b/compiler/rustc_trait_selection/src/solve/inspect.rs
new file mode 100644
index 000000000..2d6717fda
--- /dev/null
+++ b/compiler/rustc_trait_selection/src/solve/inspect.rs
@@ -0,0 +1,435 @@
+use rustc_middle::traits::query::NoSolution;
+use rustc_middle::traits::solve::inspect::{self, CacheHit, CandidateKind};
+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;
+
+#[derive(Eq, PartialEq, Debug, Hash, HashStable)]
+pub struct WipGoalEvaluation<'tcx> {
+    pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
+    pub canonicalized_goal: Option<CanonicalInput<'tcx>>,
+
+    pub evaluation_steps: Vec<WipGoalEvaluationStep<'tcx>>,
+
+    pub cache_hit: Option<CacheHit>,
+    pub is_normalizes_to_hack: IsNormalizesToHack,
+    pub returned_goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
+
+    pub result: Option<QueryResult<'tcx>>,
+}
+
+impl<'tcx> WipGoalEvaluation<'tcx> {
+    pub fn finalize(self) -> inspect::GoalEvaluation<'tcx> {
+        inspect::GoalEvaluation {
+            uncanonicalized_goal: self.uncanonicalized_goal,
+            canonicalized_goal: self.canonicalized_goal.unwrap(),
+            kind: match self.cache_hit {
+                Some(hit) => inspect::GoalEvaluationKind::CacheHit(hit),
+                None => inspect::GoalEvaluationKind::Uncached {
+                    revisions: self
+                        .evaluation_steps
+                        .into_iter()
+                        .map(WipGoalEvaluationStep::finalize)
+                        .collect(),
+                },
+            },
+            is_normalizes_to_hack: self.is_normalizes_to_hack,
+            returned_goals: self.returned_goals,
+            result: self.result.unwrap(),
+        }
+    }
+}
+
+#[derive(Eq, PartialEq, Debug, Hash, HashStable)]
+pub struct WipAddedGoalsEvaluation<'tcx> {
+    pub evaluations: Vec<Vec<WipGoalEvaluation<'tcx>>>,
+    pub result: Option<Result<Certainty, NoSolution>>,
+}
+
+impl<'tcx> WipAddedGoalsEvaluation<'tcx> {
+    pub fn finalize(self) -> inspect::AddedGoalsEvaluation<'tcx> {
+        inspect::AddedGoalsEvaluation {
+            evaluations: self
+                .evaluations
+                .into_iter()
+                .map(|evaluations| {
+                    evaluations.into_iter().map(WipGoalEvaluation::finalize).collect()
+                })
+                .collect(),
+            result: self.result.unwrap(),
+        }
+    }
+}
+
+#[derive(Eq, PartialEq, Debug, Hash, HashStable)]
+pub struct WipGoalEvaluationStep<'tcx> {
+    pub instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
+
+    pub nested_goal_evaluations: Vec<WipAddedGoalsEvaluation<'tcx>>,
+    pub candidates: Vec<WipGoalCandidate<'tcx>>,
+
+    pub result: Option<QueryResult<'tcx>>,
+}
+
+impl<'tcx> WipGoalEvaluationStep<'tcx> {
+    pub fn finalize(self) -> inspect::GoalEvaluationStep<'tcx> {
+        inspect::GoalEvaluationStep {
+            instantiated_goal: self.instantiated_goal,
+            nested_goal_evaluations: self
+                .nested_goal_evaluations
+                .into_iter()
+                .map(WipAddedGoalsEvaluation::finalize)
+                .collect(),
+            candidates: self.candidates.into_iter().map(WipGoalCandidate::finalize).collect(),
+            result: self.result.unwrap(),
+        }
+    }
+}
+
+#[derive(Eq, PartialEq, Debug, Hash, HashStable)]
+pub struct WipGoalCandidate<'tcx> {
+    pub nested_goal_evaluations: Vec<WipAddedGoalsEvaluation<'tcx>>,
+    pub candidates: Vec<WipGoalCandidate<'tcx>>,
+    pub kind: Option<CandidateKind<'tcx>>,
+}
+
+impl<'tcx> WipGoalCandidate<'tcx> {
+    pub fn finalize(self) -> inspect::GoalCandidate<'tcx> {
+        inspect::GoalCandidate {
+            nested_goal_evaluations: self
+                .nested_goal_evaluations
+                .into_iter()
+                .map(WipAddedGoalsEvaluation::finalize)
+                .collect(),
+            candidates: self.candidates.into_iter().map(WipGoalCandidate::finalize).collect(),
+            kind: self.kind.unwrap(),
+        }
+    }
+}
+
+#[derive(Debug)]
+pub enum DebugSolver<'tcx> {
+    Root,
+    GoalEvaluation(WipGoalEvaluation<'tcx>),
+    AddedGoalsEvaluation(WipAddedGoalsEvaluation<'tcx>),
+    GoalEvaluationStep(WipGoalEvaluationStep<'tcx>),
+    GoalCandidate(WipGoalCandidate<'tcx>),
+}
+
+impl<'tcx> From<WipGoalEvaluation<'tcx>> for DebugSolver<'tcx> {
+    fn from(g: WipGoalEvaluation<'tcx>) -> DebugSolver<'tcx> {
+        DebugSolver::GoalEvaluation(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<WipGoalCandidate<'tcx>> for DebugSolver<'tcx> {
+    fn from(g: WipGoalCandidate<'tcx>) -> DebugSolver<'tcx> {
+        DebugSolver::GoalCandidate(g)
+    }
+}
+
+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>>,
+        use_global_cache: UseGlobalCache,
+    ) -> ProofTreeBuilder<'tcx> {
+        ProofTreeBuilder {
+            state: Some(Box::new(BuilderData { tree: state.into(), use_global_cache })),
+        }
+    }
+
+    fn nested(&self, state: impl Into<DebugSolver<'tcx>>) -> Self {
+        match &self.state {
+            Some(prev_state) => Self {
+                state: Some(Box::new(BuilderData {
+                    tree: state.into(),
+                    use_global_cache: prev_state.use_global_cache,
+                })),
+            },
+            None => Self { state: None },
+        }
+    }
+
+    fn as_mut(&mut self) -> Option<&mut DebugSolver<'tcx>> {
+        self.state.as_mut().map(|boxed| &mut boxed.tree)
+    }
+
+    pub fn finalize(self) -> Option<inspect::GoalEvaluation<'tcx>> {
+        match self.state?.tree {
+            DebugSolver::GoalEvaluation(wip_goal_evaluation) => {
+                Some(wip_goal_evaluation.finalize())
+            }
+            root => unreachable!("unexpected proof tree builder root node: {:?}", root),
+        }
+    }
+
+    pub fn use_global_cache(&self) -> bool {
+        self.state
+            .as_ref()
+            .map(|state| matches!(state.use_global_cache, UseGlobalCache::Yes))
+            .unwrap_or(true)
+    }
+
+    pub fn new_maybe_root(
+        tcx: TyCtxt<'tcx>,
+        generate_proof_tree: GenerateProofTree,
+    ) -> ProofTreeBuilder<'tcx> {
+        let generate_proof_tree = match (
+            tcx.sess.opts.unstable_opts.dump_solver_proof_tree,
+            tcx.sess.opts.unstable_opts.dump_solver_proof_tree_use_cache,
+            generate_proof_tree,
+        ) {
+            (_, Some(use_cache), GenerateProofTree::Yes(_)) => {
+                GenerateProofTree::Yes(UseGlobalCache::from_bool(use_cache))
+            }
+
+            (DumpSolverProofTree::Always, use_cache, GenerateProofTree::No) => {
+                let use_cache = use_cache.unwrap_or(true);
+                GenerateProofTree::Yes(UseGlobalCache::from_bool(use_cache))
+            }
+
+            (_, None, GenerateProofTree::Yes(_)) => generate_proof_tree,
+            (DumpSolverProofTree::Never, _, _) => generate_proof_tree,
+            (DumpSolverProofTree::OnError, _, _) => generate_proof_tree,
+        };
+
+        match generate_proof_tree {
+            GenerateProofTree::No => ProofTreeBuilder::new_noop(),
+            GenerateProofTree::Yes(global_cache_disabled) => {
+                ProofTreeBuilder::new_root(global_cache_disabled)
+            }
+        }
+    }
+
+    pub fn new_root(use_global_cache: UseGlobalCache) -> ProofTreeBuilder<'tcx> {
+        ProofTreeBuilder::new(DebugSolver::Root, use_global_cache)
+    }
+
+    pub fn new_noop() -> ProofTreeBuilder<'tcx> {
+        ProofTreeBuilder { state: None }
+    }
+
+    pub fn is_noop(&self) -> bool {
+        self.state.is_none()
+    }
+
+    pub fn new_goal_evaluation(
+        &mut self,
+        goal: Goal<'tcx, ty::Predicate<'tcx>>,
+        is_normalizes_to_hack: IsNormalizesToHack,
+    ) -> ProofTreeBuilder<'tcx> {
+        if self.state.is_none() {
+            return ProofTreeBuilder { state: None };
+        }
+
+        self.nested(WipGoalEvaluation {
+            uncanonicalized_goal: goal,
+            canonicalized_goal: None,
+            evaluation_steps: vec![],
+            is_normalizes_to_hack,
+            cache_hit: None,
+            returned_goals: vec![],
+            result: None,
+        })
+    }
+
+    pub fn canonicalized_goal(&mut self, canonical_goal: CanonicalInput<'tcx>) {
+        if let Some(this) = self.as_mut() {
+            match this {
+                DebugSolver::GoalEvaluation(goal_evaluation) => {
+                    assert_eq!(goal_evaluation.canonicalized_goal.replace(canonical_goal), None);
+                }
+                _ => unreachable!(),
+            }
+        }
+    }
+
+    pub fn cache_hit(&mut self, cache_hit: CacheHit) {
+        if let Some(this) = self.as_mut() {
+            match this {
+                DebugSolver::GoalEvaluation(goal_evaluation) => {
+                    assert_eq!(goal_evaluation.cache_hit.replace(cache_hit), None);
+                }
+                _ => unreachable!(),
+            };
+        }
+    }
+
+    pub fn returned_goals(&mut self, goals: &[Goal<'tcx, ty::Predicate<'tcx>>]) {
+        if let Some(this) = self.as_mut() {
+            match this {
+                DebugSolver::GoalEvaluation(evaluation) => {
+                    assert!(evaluation.returned_goals.is_empty());
+                    evaluation.returned_goals.extend(goals);
+                }
+                _ => unreachable!(),
+            }
+        }
+    }
+    pub fn goal_evaluation(&mut self, goal_evaluation: ProofTreeBuilder<'tcx>) {
+        if let Some(this) = self.as_mut() {
+            match (this, goal_evaluation.state.unwrap().tree) {
+                (
+                    DebugSolver::AddedGoalsEvaluation(WipAddedGoalsEvaluation {
+                        evaluations, ..
+                    }),
+                    DebugSolver::GoalEvaluation(goal_evaluation),
+                ) => evaluations.last_mut().unwrap().push(goal_evaluation),
+                (this @ DebugSolver::Root, goal_evaluation) => *this = goal_evaluation,
+                _ => unreachable!(),
+            }
+        }
+    }
+
+    pub fn new_goal_evaluation_step(
+        &mut self,
+        instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
+    ) -> ProofTreeBuilder<'tcx> {
+        if self.state.is_none() {
+            return ProofTreeBuilder { state: None };
+        }
+
+        self.nested(WipGoalEvaluationStep {
+            instantiated_goal,
+            nested_goal_evaluations: vec![],
+            candidates: vec![],
+            result: None,
+        })
+    }
+    pub fn goal_evaluation_step(&mut self, goal_eval_step: ProofTreeBuilder<'tcx>) {
+        if let Some(this) = self.as_mut() {
+            match (this, goal_eval_step.state.unwrap().tree) {
+                (DebugSolver::GoalEvaluation(goal_eval), DebugSolver::GoalEvaluationStep(step)) => {
+                    goal_eval.evaluation_steps.push(step);
+                }
+                _ => unreachable!(),
+            }
+        }
+    }
+
+    pub fn new_goal_candidate(&mut self) -> ProofTreeBuilder<'tcx> {
+        if self.state.is_none() {
+            return ProofTreeBuilder { state: None };
+        }
+
+        self.nested(WipGoalCandidate {
+            nested_goal_evaluations: vec![],
+            candidates: vec![],
+            kind: None,
+        })
+    }
+
+    pub fn candidate_kind(&mut self, candidate_kind: CandidateKind<'tcx>) {
+        if let Some(this) = self.as_mut() {
+            match this {
+                DebugSolver::GoalCandidate(this) => {
+                    assert_eq!(this.kind.replace(candidate_kind), None)
+                }
+                _ => unreachable!(),
+            }
+        }
+    }
+
+    pub fn goal_candidate(&mut self, candidate: ProofTreeBuilder<'tcx>) {
+        if let Some(this) = self.as_mut() {
+            match (this, candidate.state.unwrap().tree) {
+                (
+                    DebugSolver::GoalCandidate(WipGoalCandidate { candidates, .. })
+                    | DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep { candidates, .. }),
+                    DebugSolver::GoalCandidate(candidate),
+                ) => candidates.push(candidate),
+                _ => unreachable!(),
+            }
+        }
+    }
+
+    pub fn new_evaluate_added_goals(&mut self) -> ProofTreeBuilder<'tcx> {
+        if self.state.is_none() {
+            return ProofTreeBuilder { state: None };
+        }
+
+        self.nested(WipAddedGoalsEvaluation { evaluations: vec![], result: None })
+    }
+
+    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 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 added_goals_evaluation(&mut self, goals_evaluation: ProofTreeBuilder<'tcx>) {
+        if let Some(this) = self.as_mut() {
+            match (this, goals_evaluation.state.unwrap().tree) {
+                (
+                    DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
+                        nested_goal_evaluations,
+                        ..
+                    })
+                    | DebugSolver::GoalCandidate(WipGoalCandidate {
+                        nested_goal_evaluations, ..
+                    }),
+                    DebugSolver::AddedGoalsEvaluation(added_goals_evaluation),
+                ) => nested_goal_evaluations.push(added_goals_evaluation),
+                _ => unreachable!(),
+            }
+        }
+    }
+
+    pub fn query_result(&mut self, result: QueryResult<'tcx>) {
+        if let Some(this) = self.as_mut() {
+            match this {
+                DebugSolver::GoalEvaluation(goal_evaluation) => {
+                    assert_eq!(goal_evaluation.result.replace(result), None);
+                }
+                DebugSolver::GoalEvaluationStep(evaluation_step) => {
+                    assert_eq!(evaluation_step.result.replace(result), None);
+                }
+                DebugSolver::Root
+                | DebugSolver::AddedGoalsEvaluation(_)
+                | DebugSolver::GoalCandidate(_) => unreachable!(),
+            }
+        }
+    }
+}
diff --git a/compiler/rustc_trait_selection/src/solve/mod.rs b/compiler/rustc_trait_selection/src/solve/mod.rs
index 56a254d9c..77809d8d2 100644
--- a/compiler/rustc_trait_selection/src/solve/mod.rs
+++ b/compiler/rustc_trait_selection/src/solve/mod.rs
@@ -20,17 +20,24 @@ use rustc_middle::ty::{
     CoercePredicate, RegionOutlivesPredicate, SubtypePredicate, TypeOutlivesPredicate,
 };
 
+mod alias_relate;
 mod assembly;
 mod canonicalize;
 mod eval_ctxt;
 mod fulfill;
+pub mod inspect;
+mod normalize;
 mod opaques;
 mod project_goals;
 mod search_graph;
 mod trait_goals;
+mod weak_types;
 
-pub use eval_ctxt::{EvalCtxt, InferCtxtEvalExt};
+pub use eval_ctxt::{
+    EvalCtxt, GenerateProofTree, InferCtxtEvalExt, InferCtxtSelectExt, UseGlobalCache,
+};
 pub use fulfill::FulfillmentCtxt;
+pub(crate) use normalize::deeply_normalize;
 
 #[derive(Debug, Clone, Copy)]
 enum SolverMode {
@@ -154,139 +161,40 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
         }
     }
 
-    #[instrument(level = "debug", skip(self), ret)]
-    fn compute_alias_relate_goal(
+    #[instrument(level = "debug", skip(self))]
+    fn compute_const_evaluatable_goal(
         &mut self,
-        goal: Goal<'tcx, (ty::Term<'tcx>, ty::Term<'tcx>, ty::AliasRelationDirection)>,
+        Goal { param_env, predicate: ct }: Goal<'tcx, ty::Const<'tcx>>,
     ) -> QueryResult<'tcx> {
-        let tcx = self.tcx();
-        // We may need to invert the alias relation direction if dealing an alias on the RHS.
-        #[derive(Debug)]
-        enum Invert {
-            No,
-            Yes,
-        }
-        let evaluate_normalizes_to =
-            |ecx: &mut EvalCtxt<'_, 'tcx>, alias, other, direction, invert| {
-                let span = tracing::span!(
-                    tracing::Level::DEBUG,
-                    "compute_alias_relate_goal(evaluate_normalizes_to)",
-                    ?alias,
-                    ?other,
-                    ?direction,
-                    ?invert
-                );
-                let _enter = span.enter();
-                let result = ecx.probe(|ecx| {
-                    let other = match direction {
-                        // This is purely an optimization.
-                        ty::AliasRelationDirection::Equate => other,
-
-                        ty::AliasRelationDirection::Subtype => {
-                            let fresh = ecx.next_term_infer_of_kind(other);
-                            let (sub, sup) = match invert {
-                                Invert::No => (fresh, other),
-                                Invert::Yes => (other, fresh),
-                            };
-                            ecx.sub(goal.param_env, sub, sup)?;
-                            fresh
-                        }
-                    };
-                    ecx.add_goal(goal.with(
-                        tcx,
-                        ty::Binder::dummy(ty::ProjectionPredicate {
-                            projection_ty: alias,
-                            term: other,
-                        }),
-                    ));
-                    ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
-                });
-                debug!(?result);
-                result
-            };
-
-        let (lhs, rhs, direction) = goal.predicate;
-
-        if lhs.is_infer() || rhs.is_infer() {
-            bug!(
-                "`AliasRelate` goal with an infer var on lhs or rhs which should have been instantiated"
-            );
-        }
-
-        match (lhs.to_alias_ty(tcx), rhs.to_alias_ty(tcx)) {
-            (None, None) => bug!("`AliasRelate` goal without an alias on either lhs or rhs"),
-
-            // RHS is not a projection, only way this is true is if LHS normalizes-to RHS
-            (Some(alias_lhs), None) => {
-                evaluate_normalizes_to(self, alias_lhs, rhs, direction, Invert::No)
-            }
-
-            // LHS is not a projection, only way this is true is if RHS normalizes-to LHS
-            (None, Some(alias_rhs)) => {
-                evaluate_normalizes_to(self, alias_rhs, lhs, direction, Invert::Yes)
-            }
-
-            (Some(alias_lhs), Some(alias_rhs)) => {
-                debug!("both sides are aliases");
-
-                let mut candidates = Vec::new();
-                // LHS normalizes-to RHS
-                candidates.extend(evaluate_normalizes_to(
-                    self,
-                    alias_lhs,
-                    rhs,
-                    direction,
-                    Invert::No,
-                ));
-                // RHS normalizes-to RHS
-                candidates.extend(evaluate_normalizes_to(
-                    self,
-                    alias_rhs,
-                    lhs,
-                    direction,
-                    Invert::Yes,
-                ));
-                // Relate via substs
-                let subst_relate_response = self.probe(|ecx| {
-                    let span = tracing::span!(
-                        tracing::Level::DEBUG,
-                        "compute_alias_relate_goal(relate_via_substs)",
-                        ?alias_lhs,
-                        ?alias_rhs,
-                        ?direction
-                    );
-                    let _enter = span.enter();
-
-                    match direction {
-                        ty::AliasRelationDirection::Equate => {
-                            ecx.eq(goal.param_env, alias_lhs, alias_rhs)?;
-                        }
-                        ty::AliasRelationDirection::Subtype => {
-                            ecx.sub(goal.param_env, alias_lhs, alias_rhs)?;
-                        }
-                    }
-
-                    ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
-                });
-                candidates.extend(subst_relate_response);
-                debug!(?candidates);
-
-                if let Some(merged) = self.try_merge_responses(&candidates) {
-                    Ok(merged)
+        match ct.kind() {
+            ty::ConstKind::Unevaluated(uv) => {
+                // We never return `NoSolution` here as `try_const_eval_resolve` emits an
+                // error itself when failing to evaluate, so emitting an additional fulfillment
+                // error in that case is unnecessary noise. This may change in the future once
+                // evaluation failures are allowed to impact selection, e.g. generic const
+                // expressions in impl headers or `where`-clauses.
+
+                // FIXME(generic_const_exprs): Implement handling for generic
+                // const expressions here.
+                if let Some(_normalized) = self.try_const_eval_resolve(param_env, uv, ct.ty()) {
+                    self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
                 } else {
-                    // When relating two aliases and we have ambiguity, we prefer
-                    // relating the generic arguments of the aliases over normalizing
-                    // them. This is necessary for inference during typeck.
-                    //
-                    // As this is incomplete, we must not do so during coherence.
-                    match (self.solver_mode(), subst_relate_response) {
-                        (SolverMode::Normal, Ok(response)) => Ok(response),
-                        (SolverMode::Normal, Err(NoSolution)) | (SolverMode::Coherence, _) => {
-                            self.flounder(&candidates)
-                        }
-                    }
+                    self.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS)
                 }
             }
+            ty::ConstKind::Infer(_) => {
+                self.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS)
+            }
+            ty::ConstKind::Placeholder(_) | ty::ConstKind::Value(_) | ty::ConstKind::Error(_) => {
+                self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
+            }
+            // We can freely ICE here as:
+            // - `Param` gets replaced with a placeholder during canonicalization
+            // - `Bound` cannot exist as we don't have a binder around the self Type
+            // - `Expr` is part of `feature(generic_const_exprs)` and is not implemented yet
+            ty::ConstKind::Param(_) | ty::ConstKind::Bound(_, _) | ty::ConstKind::Expr(_) => {
+                bug!("unexpect const kind: {:?}", ct)
+            }
         }
     }
 
diff --git a/compiler/rustc_trait_selection/src/solve/normalize.rs b/compiler/rustc_trait_selection/src/solve/normalize.rs
new file mode 100644
index 000000000..c388850d8
--- /dev/null
+++ b/compiler/rustc_trait_selection/src/solve/normalize.rs
@@ -0,0 +1,220 @@
+use crate::traits::error_reporting::TypeErrCtxtExt;
+use crate::traits::query::evaluate_obligation::InferCtxtExt;
+use crate::traits::{needs_normalization, BoundVarReplacer, PlaceholderReplacer};
+use rustc_data_structures::stack::ensure_sufficient_stack;
+use rustc_infer::infer::at::At;
+use rustc_infer::infer::type_variable::{TypeVariableOrigin, TypeVariableOriginKind};
+use rustc_infer::traits::TraitEngineExt;
+use rustc_infer::traits::{FulfillmentError, Obligation, TraitEngine};
+use rustc_middle::infer::unify_key::{ConstVariableOrigin, ConstVariableOriginKind};
+use rustc_middle::traits::Reveal;
+use rustc_middle::ty::{self, AliasTy, Ty, TyCtxt, UniverseIndex};
+use rustc_middle::ty::{FallibleTypeFolder, TypeSuperFoldable};
+use rustc_middle::ty::{TypeFoldable, TypeVisitableExt};
+
+use super::FulfillmentCtxt;
+
+/// Deeply normalize all aliases in `value`. This does not handle inference and expects
+/// its input to be already fully resolved.
+pub(crate) fn deeply_normalize<'tcx, T: TypeFoldable<TyCtxt<'tcx>>>(
+    at: At<'_, 'tcx>,
+    value: T,
+) -> Result<T, Vec<FulfillmentError<'tcx>>> {
+    let fulfill_cx = FulfillmentCtxt::new(at.infcx);
+    let mut folder = NormalizationFolder { at, fulfill_cx, depth: 0, universes: Vec::new() };
+
+    value.try_fold_with(&mut folder)
+}
+
+struct NormalizationFolder<'me, 'tcx> {
+    at: At<'me, 'tcx>,
+    fulfill_cx: FulfillmentCtxt<'tcx>,
+    depth: usize,
+    universes: Vec<Option<UniverseIndex>>,
+}
+
+impl<'tcx> NormalizationFolder<'_, 'tcx> {
+    fn normalize_alias_ty(
+        &mut self,
+        alias: AliasTy<'tcx>,
+    ) -> Result<Ty<'tcx>, Vec<FulfillmentError<'tcx>>> {
+        let infcx = self.at.infcx;
+        let tcx = infcx.tcx;
+        let recursion_limit = tcx.recursion_limit();
+        if !recursion_limit.value_within_limit(self.depth) {
+            self.at.infcx.err_ctxt().report_overflow_error(
+                &alias.to_ty(tcx),
+                self.at.cause.span,
+                true,
+                |_| {},
+            );
+        }
+
+        self.depth += 1;
+
+        let new_infer_ty = infcx.next_ty_var(TypeVariableOrigin {
+            kind: TypeVariableOriginKind::NormalizeProjectionType,
+            span: self.at.cause.span,
+        });
+        let obligation = Obligation::new(
+            tcx,
+            self.at.cause.clone(),
+            self.at.param_env,
+            ty::Binder::dummy(ty::ProjectionPredicate {
+                projection_ty: alias,
+                term: new_infer_ty.into(),
+            }),
+        );
+
+        // Do not emit an error if normalization is known to fail but instead
+        // keep the projection unnormalized. This is the case for projections
+        // with a `T: Trait` where-clause and opaque types outside of the defining
+        // scope.
+        let result = if infcx.predicate_may_hold(&obligation) {
+            self.fulfill_cx.register_predicate_obligation(infcx, obligation);
+            let errors = self.fulfill_cx.select_all_or_error(infcx);
+            if !errors.is_empty() {
+                return Err(errors);
+            }
+            let ty = infcx.resolve_vars_if_possible(new_infer_ty);
+            ty.try_fold_with(self)?
+        } else {
+            alias.to_ty(tcx).try_super_fold_with(self)?
+        };
+
+        self.depth -= 1;
+        Ok(result)
+    }
+
+    fn normalize_unevaluated_const(
+        &mut self,
+        ty: Ty<'tcx>,
+        uv: ty::UnevaluatedConst<'tcx>,
+    ) -> Result<ty::Const<'tcx>, Vec<FulfillmentError<'tcx>>> {
+        let infcx = self.at.infcx;
+        let tcx = infcx.tcx;
+        let recursion_limit = tcx.recursion_limit();
+        if !recursion_limit.value_within_limit(self.depth) {
+            self.at.infcx.err_ctxt().report_overflow_error(
+                &ty::Const::new_unevaluated(tcx, uv, ty),
+                self.at.cause.span,
+                true,
+                |_| {},
+            );
+        }
+
+        self.depth += 1;
+
+        let new_infer_ct = infcx.next_const_var(
+            ty,
+            ConstVariableOrigin {
+                kind: ConstVariableOriginKind::MiscVariable,
+                span: self.at.cause.span,
+            },
+        );
+        let obligation = Obligation::new(
+            tcx,
+            self.at.cause.clone(),
+            self.at.param_env,
+            ty::Binder::dummy(ty::ProjectionPredicate {
+                projection_ty: tcx.mk_alias_ty(uv.def, uv.substs),
+                term: new_infer_ct.into(),
+            }),
+        );
+
+        let result = if infcx.predicate_may_hold(&obligation) {
+            self.fulfill_cx.register_predicate_obligation(infcx, obligation);
+            let errors = self.fulfill_cx.select_all_or_error(infcx);
+            if !errors.is_empty() {
+                return Err(errors);
+            }
+            let ct = infcx.resolve_vars_if_possible(new_infer_ct);
+            ct.try_fold_with(self)?
+        } else {
+            ty::Const::new_unevaluated(tcx, uv, ty).try_super_fold_with(self)?
+        };
+
+        self.depth -= 1;
+        Ok(result)
+    }
+}
+
+impl<'tcx> FallibleTypeFolder<TyCtxt<'tcx>> for NormalizationFolder<'_, 'tcx> {
+    type Error = Vec<FulfillmentError<'tcx>>;
+
+    fn interner(&self) -> TyCtxt<'tcx> {
+        self.at.infcx.tcx
+    }
+
+    fn try_fold_binder<T: TypeFoldable<TyCtxt<'tcx>>>(
+        &mut self,
+        t: ty::Binder<'tcx, T>,
+    ) -> Result<ty::Binder<'tcx, T>, Self::Error> {
+        self.universes.push(None);
+        let t = t.try_super_fold_with(self)?;
+        self.universes.pop();
+        Ok(t)
+    }
+
+    fn try_fold_ty(&mut self, ty: Ty<'tcx>) -> Result<Ty<'tcx>, Self::Error> {
+        let reveal = self.at.param_env.reveal();
+        let infcx = self.at.infcx;
+        debug_assert_eq!(ty, infcx.shallow_resolve(ty));
+        if !needs_normalization(&ty, reveal) {
+            return Ok(ty);
+        }
+
+        // We don't normalize opaque types unless we have
+        // `Reveal::All`, even if we're in the defining scope.
+        let data = match *ty.kind() {
+            ty::Alias(kind, alias_ty) if kind != ty::Opaque || reveal == Reveal::All => alias_ty,
+            _ => return ty.try_super_fold_with(self),
+        };
+
+        if data.has_escaping_bound_vars() {
+            let (data, mapped_regions, mapped_types, mapped_consts) =
+                BoundVarReplacer::replace_bound_vars(infcx, &mut self.universes, data);
+            let result = ensure_sufficient_stack(|| self.normalize_alias_ty(data))?;
+            Ok(PlaceholderReplacer::replace_placeholders(
+                infcx,
+                mapped_regions,
+                mapped_types,
+                mapped_consts,
+                &mut self.universes,
+                result,
+            ))
+        } else {
+            ensure_sufficient_stack(|| self.normalize_alias_ty(data))
+        }
+    }
+
+    fn try_fold_const(&mut self, ct: ty::Const<'tcx>) -> Result<ty::Const<'tcx>, Self::Error> {
+        let reveal = self.at.param_env.reveal();
+        let infcx = self.at.infcx;
+        debug_assert_eq!(ct, infcx.shallow_resolve(ct));
+        if !needs_normalization(&ct, reveal) {
+            return Ok(ct);
+        }
+
+        let uv = match ct.kind() {
+            ty::ConstKind::Unevaluated(ct) => ct,
+            _ => return ct.try_super_fold_with(self),
+        };
+
+        if uv.has_escaping_bound_vars() {
+            let (uv, mapped_regions, mapped_types, mapped_consts) =
+                BoundVarReplacer::replace_bound_vars(infcx, &mut self.universes, uv);
+            let result = ensure_sufficient_stack(|| self.normalize_unevaluated_const(ct.ty(), uv))?;
+            Ok(PlaceholderReplacer::replace_placeholders(
+                infcx,
+                mapped_regions,
+                mapped_types,
+                mapped_consts,
+                &mut self.universes,
+                result,
+            ))
+        } else {
+            ensure_sufficient_stack(|| self.normalize_unevaluated_const(ct.ty(), uv))
+        }
+    }
+}
diff --git a/compiler/rustc_trait_selection/src/solve/opaques.rs b/compiler/rustc_trait_selection/src/solve/opaques.rs
index a5de4ddee..16194f5ad 100644
--- a/compiler/rustc_trait_selection/src/solve/opaques.rs
+++ b/compiler/rustc_trait_selection/src/solve/opaques.rs
@@ -20,8 +20,6 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
                 let Some(opaque_ty_def_id) = opaque_ty.def_id.as_local() else {
                     return Err(NoSolution);
                 };
-                let opaque_ty =
-                    ty::OpaqueTypeKey { def_id: opaque_ty_def_id, substs: opaque_ty.substs };
                 // FIXME: at some point we should call queries without defining
                 // new opaque types but having the existing opaque type definitions.
                 // This will require moving this below "Prefer opaques registered already".
@@ -41,7 +39,10 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
                     Ok(()) => {}
                 }
                 // Prefer opaques registered already.
-                let matches = self.unify_existing_opaque_tys(goal.param_env, opaque_ty, expected);
+                let opaque_type_key =
+                    ty::OpaqueTypeKey { def_id: opaque_ty_def_id, substs: opaque_ty.substs };
+                let matches =
+                    self.unify_existing_opaque_tys(goal.param_env, opaque_type_key, expected);
                 if !matches.is_empty() {
                     if let Some(response) = self.try_merge_responses(&matches) {
                         return Ok(response);
@@ -50,10 +51,24 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
                     }
                 }
                 // Otherwise, define a new opaque type
-                self.register_opaque_ty(opaque_ty, expected, goal.param_env)?;
+                self.insert_hidden_type(opaque_type_key, goal.param_env, expected)?;
+                self.add_item_bounds_for_hidden_type(
+                    opaque_ty.def_id,
+                    opaque_ty.substs,
+                    goal.param_env,
+                    expected,
+                );
                 self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
             }
             (Reveal::UserFacing, SolverMode::Coherence) => {
+                // An impossible opaque type bound is the only way this goal will fail
+                // e.g. assigning `impl Copy := NotCopy`
+                self.add_item_bounds_for_hidden_type(
+                    opaque_ty.def_id,
+                    opaque_ty.substs,
+                    goal.param_env,
+                    expected,
+                );
                 self.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS)
             }
             (Reveal::All, _) => {
diff --git a/compiler/rustc_trait_selection/src/solve/project_goals.rs b/compiler/rustc_trait_selection/src/solve/project_goals.rs
index 7d7dfa2c8..e53b784a7 100644
--- a/compiler/rustc_trait_selection/src/solve/project_goals.rs
+++ b/compiler/rustc_trait_selection/src/solve/project_goals.rs
@@ -9,6 +9,7 @@ use rustc_hir::LangItem;
 use rustc_infer::traits::query::NoSolution;
 use rustc_infer::traits::specialization_graph::LeafDef;
 use rustc_infer::traits::Reveal;
+use rustc_middle::traits::solve::inspect::CandidateKind;
 use rustc_middle::traits::solve::{CanonicalResponse, Certainty, Goal, QueryResult};
 use rustc_middle::ty::fast_reject::{DeepRejectCtxt, TreatParams};
 use rustc_middle::ty::ProjectionPredicate;
@@ -22,25 +23,66 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
         &mut self,
         goal: Goal<'tcx, ProjectionPredicate<'tcx>>,
     ) -> QueryResult<'tcx> {
-        match goal.predicate.projection_ty.kind(self.tcx()) {
-            ty::AliasKind::Projection => {
+        let def_id = goal.predicate.def_id();
+        match self.tcx().def_kind(def_id) {
+            DefKind::AssocTy | DefKind::AssocConst => {
                 // To only compute normalization once for each projection we only
-                // normalize if the expected term is an unconstrained inference variable.
+                // assemble normalization candidates if the expected term is an
+                // unconstrained inference variable.
+                //
+                // Why: For better cache hits, since if we have an unconstrained RHS then
+                // there are only as many cache keys as there are (canonicalized) alias
+                // types in each normalizes-to goal. This also weakens inference in a
+                // forwards-compatible way so we don't use the value of the RHS term to
+                // affect candidate assembly for projections.
                 //
                 // E.g. for `<T as Trait>::Assoc == u32` we recursively compute the goal
                 // `exists<U> <T as Trait>::Assoc == U` and then take the resulting type for
                 // `U` and equate it with `u32`. This means that we don't need a separate
-                // projection cache in the solver.
+                // projection cache in the solver, since we're piggybacking off of regular
+                // goal caching.
                 if self.term_is_fully_unconstrained(goal) {
-                    let candidates = self.assemble_and_evaluate_candidates(goal);
-                    self.merge_candidates(candidates)
+                    match self.tcx().associated_item(def_id).container {
+                        ty::AssocItemContainer::TraitContainer => {
+                            let candidates = self.assemble_and_evaluate_candidates(goal);
+                            self.merge_candidates(candidates)
+                        }
+                        ty::AssocItemContainer::ImplContainer => {
+                            bug!("IATs not supported here yet")
+                        }
+                    }
                 } else {
                     self.set_normalizes_to_hack_goal(goal);
                     self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
                 }
             }
-            ty::AliasKind::Opaque => self.normalize_opaque_type(goal),
-            ty::AliasKind::Inherent => bug!("IATs not supported here yet"),
+            DefKind::AnonConst => self.normalize_anon_const(goal),
+            DefKind::OpaqueTy => self.normalize_opaque_type(goal),
+            DefKind::TyAlias => self.normalize_weak_type(goal),
+            kind => bug!("unknown DefKind {} in projection goal: {goal:#?}", kind.descr(def_id)),
+        }
+    }
+
+    #[instrument(level = "debug", skip(self), ret)]
+    fn normalize_anon_const(
+        &mut self,
+        goal: Goal<'tcx, ty::ProjectionPredicate<'tcx>>,
+    ) -> QueryResult<'tcx> {
+        if let Some(normalized_const) = self.try_const_eval_resolve(
+            goal.param_env,
+            ty::UnevaluatedConst::new(
+                goal.predicate.projection_ty.def_id,
+                goal.predicate.projection_ty.substs,
+            ),
+            self.tcx()
+                .type_of(goal.predicate.projection_ty.def_id)
+                .no_bound_vars()
+                .expect("const ty should not rely on other generics"),
+        ) {
+            self.eq(goal.param_env, normalized_const, goal.predicate.term.ct().unwrap())?;
+            self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
+        } else {
+            self.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS)
         }
     }
 }
@@ -65,24 +107,26 @@ impl<'tcx> assembly::GoalKind<'tcx> for ProjectionPredicate<'tcx> {
     fn probe_and_match_goal_against_assumption(
         ecx: &mut EvalCtxt<'_, 'tcx>,
         goal: Goal<'tcx, Self>,
-        assumption: ty::Predicate<'tcx>,
+        assumption: ty::Clause<'tcx>,
         then: impl FnOnce(&mut EvalCtxt<'_, 'tcx>) -> QueryResult<'tcx>,
     ) -> QueryResult<'tcx> {
-        if let Some(poly_projection_pred) = assumption.to_opt_poly_projection_pred()
-            && poly_projection_pred.projection_def_id() == goal.predicate.def_id()
-        {
-            ecx.probe(|ecx| {
-                let assumption_projection_pred =
-                    ecx.instantiate_binder_with_infer(poly_projection_pred);
-                ecx.eq(
-                    goal.param_env,
-                    goal.predicate.projection_ty,
-                    assumption_projection_pred.projection_ty,
-                )?;
-                ecx.eq(goal.param_env, goal.predicate.term, assumption_projection_pred.term)
-                    .expect("expected goal term to be fully unconstrained");
-                then(ecx)
-            })
+        if let Some(projection_pred) = assumption.as_projection_clause() {
+            if projection_pred.projection_def_id() == goal.predicate.def_id() {
+                ecx.probe_candidate("assumption").enter(|ecx| {
+                    let assumption_projection_pred =
+                        ecx.instantiate_binder_with_infer(projection_pred);
+                    ecx.eq(
+                        goal.param_env,
+                        goal.predicate.projection_ty,
+                        assumption_projection_pred.projection_ty,
+                    )?;
+                    ecx.eq(goal.param_env, goal.predicate.term, assumption_projection_pred.term)
+                        .expect("expected goal term to be fully unconstrained");
+                    then(ecx)
+                })
+            } else {
+                Err(NoSolution)
+            }
         } else {
             Err(NoSolution)
         }
@@ -102,101 +146,100 @@ impl<'tcx> assembly::GoalKind<'tcx> for ProjectionPredicate<'tcx> {
             return Err(NoSolution);
         }
 
-        ecx.probe(|ecx| {
-            let impl_substs = ecx.fresh_substs_for_item(impl_def_id);
-            let impl_trait_ref = impl_trait_ref.subst(tcx, impl_substs);
-
-            ecx.eq(goal.param_env, goal_trait_ref, impl_trait_ref)?;
-
-            let where_clause_bounds = tcx
-                .predicates_of(impl_def_id)
-                .instantiate(tcx, impl_substs)
-                .predicates
-                .into_iter()
-                .map(|pred| goal.with(tcx, pred));
-            ecx.add_goals(where_clause_bounds);
-
-            // In case the associated item is hidden due to specialization, we have to
-            // return ambiguity this would otherwise be incomplete, resulting in
-            // unsoundness during coherence (#105782).
-            let Some(assoc_def) = fetch_eligible_assoc_item_def(
-                ecx,
-                goal.param_env,
-                goal_trait_ref,
-                goal.predicate.def_id(),
-                impl_def_id
-            )? else {
-                return ecx.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS);
-            };
+        ecx.probe(
+            |r| CandidateKind::Candidate { name: "impl".into(), result: *r }).enter(
+            |ecx| {
+                let impl_substs = ecx.fresh_substs_for_item(impl_def_id);
+                let impl_trait_ref = impl_trait_ref.subst(tcx, impl_substs);
+
+                ecx.eq(goal.param_env, goal_trait_ref, impl_trait_ref)?;
+
+                let where_clause_bounds = tcx
+                    .predicates_of(impl_def_id)
+                    .instantiate(tcx, impl_substs)
+                    .predicates
+                    .into_iter()
+                    .map(|pred| goal.with(tcx, pred));
+                ecx.add_goals(where_clause_bounds);
+
+                // In case the associated item is hidden due to specialization, we have to
+                // return ambiguity this would otherwise be incomplete, resulting in
+                // unsoundness during coherence (#105782).
+                let Some(assoc_def) = fetch_eligible_assoc_item_def(
+                    ecx,
+                    goal.param_env,
+                    goal_trait_ref,
+                    goal.predicate.def_id(),
+                    impl_def_id
+                )? else {
+                    return ecx.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS);
+                };
 
-            if !assoc_def.item.defaultness(tcx).has_value() {
-                let guar = tcx.sess.delay_span_bug(
-                    tcx.def_span(assoc_def.item.def_id),
-                    "missing value for assoc item in impl",
-                );
-                let error_term = match assoc_def.item.kind {
-                    ty::AssocKind::Const => tcx
-                        .const_error(
+                if !assoc_def.item.defaultness(tcx).has_value() {
+                    let guar = tcx.sess.delay_span_bug(
+                        tcx.def_span(assoc_def.item.def_id),
+                        "missing value for assoc item in impl",
+                    );
+                    let error_term = match assoc_def.item.kind {
+                        ty::AssocKind::Const => ty::Const::new_error(tcx,
+                            guar,
                             tcx.type_of(goal.predicate.def_id())
                                 .subst(tcx, goal.predicate.projection_ty.substs),
-                            guar,
-                        )
-                        .into(),
-                    ty::AssocKind::Type => tcx.ty_error(guar).into(),
-                    ty::AssocKind::Fn => unreachable!(),
-                };
-                ecx.eq(goal.param_env, goal.predicate.term, error_term)
-                    .expect("expected goal term to be fully unconstrained");
-                return ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes);
-            }
+                            )
+                            .into(),
+                        ty::AssocKind::Type => Ty::new_error(tcx,guar).into(),
+                        ty::AssocKind::Fn => unreachable!(),
+                    };
+                    ecx.eq(goal.param_env, goal.predicate.term, error_term)
+                        .expect("expected goal term to be fully unconstrained");
+                    return ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes);
+                }
 
-            // Getting the right substitutions here is complex, e.g. given:
-            // - a goal `<Vec<u32> as Trait<i32>>::Assoc<u64>`
-            // - the applicable impl `impl<T> Trait<i32> for Vec<T>`
-            // - and the impl which defines `Assoc` being `impl<T, U> Trait<U> for Vec<T>`
-            //
-            // We first rebase the goal substs onto the impl, going from `[Vec<u32>, i32, u64]`
-            // to `[u32, u64]`.
-            //
-            // And then map these substs to the substs of the defining impl of `Assoc`, going
-            // from `[u32, u64]` to `[u32, i32, u64]`.
-            let impl_substs_with_gat = goal.predicate.projection_ty.substs.rebase_onto(
-                tcx,
-                goal_trait_ref.def_id,
-                impl_substs,
-            );
-            let substs = ecx.translate_substs(
-                goal.param_env,
-                impl_def_id,
-                impl_substs_with_gat,
-                assoc_def.defining_node,
-            );
-
-            // Finally we construct the actual value of the associated type.
-            let is_const = matches!(tcx.def_kind(assoc_def.item.def_id), DefKind::AssocConst);
-            let ty = tcx.type_of(assoc_def.item.def_id);
-            let term: ty::EarlyBinder<ty::Term<'tcx>> = if is_const {
-                let identity_substs =
-                    ty::InternalSubsts::identity_for_item(tcx, assoc_def.item.def_id);
-                let did = assoc_def.item.def_id;
-                let kind =
-                    ty::ConstKind::Unevaluated(ty::UnevaluatedConst::new(did, identity_substs));
-                ty.map_bound(|ty| tcx.mk_const(kind, ty).into())
-            } else {
-                ty.map_bound(|ty| ty.into())
-            };
+                // Getting the right substitutions here is complex, e.g. given:
+                // - a goal `<Vec<u32> as Trait<i32>>::Assoc<u64>`
+                // - the applicable impl `impl<T> Trait<i32> for Vec<T>`
+                // - and the impl which defines `Assoc` being `impl<T, U> Trait<U> for Vec<T>`
+                //
+                // We first rebase the goal substs onto the impl, going from `[Vec<u32>, i32, u64]`
+                // to `[u32, u64]`.
+                //
+                // And then map these substs to the substs of the defining impl of `Assoc`, going
+                // from `[u32, u64]` to `[u32, i32, u64]`.
+                let impl_substs_with_gat = goal.predicate.projection_ty.substs.rebase_onto(
+                    tcx,
+                    goal_trait_ref.def_id,
+                    impl_substs,
+                );
+                let substs = ecx.translate_substs(
+                    goal.param_env,
+                    impl_def_id,
+                    impl_substs_with_gat,
+                    assoc_def.defining_node,
+                );
 
-            ecx.eq(goal.param_env, goal.predicate.term, term.subst(tcx, substs))
-                .expect("expected goal term to be fully unconstrained");
-            ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
-        })
+                // Finally we construct the actual value of the associated type.
+                let term = match assoc_def.item.kind {
+                    ty::AssocKind::Type => tcx.type_of(assoc_def.item.def_id).map_bound(|ty| ty.into()),
+                    ty::AssocKind::Const => bug!("associated const projection is not supported yet"),
+                    ty::AssocKind::Fn => unreachable!("we should never project to a fn"),
+                };
+
+                ecx.eq(goal.param_env, goal.predicate.term, term.subst(tcx, substs))
+                    .expect("expected goal term to be fully unconstrained");
+                ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
+            },
+        )
     }
 
     fn consider_auto_trait_candidate(
-        _ecx: &mut EvalCtxt<'_, 'tcx>,
+        ecx: &mut EvalCtxt<'_, 'tcx>,
         goal: Goal<'tcx, Self>,
     ) -> QueryResult<'tcx> {
-        bug!("auto traits do not have associated types: {:?}", goal);
+        ecx.tcx().sess.delay_span_bug(
+            ecx.tcx().def_span(goal.predicate.def_id()),
+            "associated types not allowed on auto traits",
+        );
+        Err(NoSolution)
     }
 
     fn consider_trait_alias_candidate(
@@ -280,7 +323,7 @@ impl<'tcx> assembly::GoalKind<'tcx> for ProjectionPredicate<'tcx> {
         goal: Goal<'tcx, Self>,
     ) -> QueryResult<'tcx> {
         let tcx = ecx.tcx();
-        ecx.probe(|ecx| {
+        ecx.probe_candidate("builtin pointee").enter(|ecx| {
             let metadata_ty = match goal.predicate.self_ty().kind() {
                 ty::Bool
                 | ty::Char
@@ -300,7 +343,7 @@ impl<'tcx> assembly::GoalKind<'tcx> for ProjectionPredicate<'tcx> {
                 | ty::Never
                 | ty::Foreign(..) => tcx.types.unit,
 
-                ty::Error(e) => tcx.ty_error(*e),
+                ty::Error(e) => Ty::new_error(tcx, *e),
 
                 ty::Str | ty::Slice(_) => tcx.types.usize,
 
@@ -323,7 +366,7 @@ impl<'tcx> assembly::GoalKind<'tcx> for ProjectionPredicate<'tcx> {
                 }
 
                 ty::Adt(def, substs) if def.is_struct() => {
-                    match def.non_enum_variant().fields.raw.last() {
+                    match def.non_enum_variant().tail_opt() {
                         None => tcx.types.unit,
                         Some(field_def) => {
                             let self_ty = field_def.ty(tcx, substs);
@@ -497,7 +540,7 @@ impl<'tcx> assembly::GoalKind<'tcx> for ProjectionPredicate<'tcx> {
             ),
         };
 
-        ecx.probe(|ecx| {
+        ecx.probe_candidate("builtin discriminant kind").enter(|ecx| {
             ecx.eq(goal.param_env, goal.predicate.term, discriminant_ty.into())
                 .expect("expected goal term to be fully unconstrained");
             ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
diff --git a/compiler/rustc_trait_selection/src/solve/search_graph/mod.rs b/compiler/rustc_trait_selection/src/solve/search_graph/mod.rs
index 19e4b2300..f00456e26 100644
--- a/compiler/rustc_trait_selection/src/solve/search_graph/mod.rs
+++ b/compiler/rustc_trait_selection/src/solve/search_graph/mod.rs
@@ -2,6 +2,7 @@ mod cache;
 mod overflow;
 
 pub(super) use overflow::OverflowHandler;
+use rustc_middle::traits::solve::inspect::CacheHit;
 
 use self::cache::ProvisionalEntry;
 use cache::ProvisionalCache;
@@ -12,6 +13,7 @@ use rustc_middle::traits::solve::{CanonicalInput, Certainty, MaybeCause, QueryRe
 use rustc_middle::ty::TyCtxt;
 use std::{collections::hash_map::Entry, mem};
 
+use super::inspect::ProofTreeBuilder;
 use super::SolverMode;
 
 rustc_index::newtype_index! {
@@ -88,11 +90,12 @@ impl<'tcx> SearchGraph<'tcx> {
     /// Tries putting the new goal on the stack, returning an error if it is already cached.
     ///
     /// This correctly updates the provisional cache if there is a cycle.
-    #[instrument(level = "debug", skip(self, tcx), ret)]
+    #[instrument(level = "debug", skip(self, tcx, inspect), ret)]
     fn try_push_stack(
         &mut self,
         tcx: TyCtxt<'tcx>,
         input: CanonicalInput<'tcx>,
+        inspect: &mut ProofTreeBuilder<'tcx>,
     ) -> Result<(), QueryResult<'tcx>> {
         // Look at the provisional cache to check for cycles.
         let cache = &mut self.provisional_cache;
@@ -119,6 +122,8 @@ impl<'tcx> SearchGraph<'tcx> {
             // Finally we can return either the provisional response for that goal if we have a
             // coinductive cycle or an ambiguous result if the cycle is inductive.
             Entry::Occupied(entry_index) => {
+                inspect.cache_hit(CacheHit::Provisional);
+
                 let entry_index = *entry_index.get();
 
                 let stack_depth = cache.depth(entry_index);
@@ -205,16 +210,18 @@ impl<'tcx> SearchGraph<'tcx> {
         &mut self,
         tcx: TyCtxt<'tcx>,
         canonical_input: CanonicalInput<'tcx>,
-        mut loop_body: impl FnMut(&mut Self) -> QueryResult<'tcx>,
+        inspect: &mut ProofTreeBuilder<'tcx>,
+        mut loop_body: impl FnMut(&mut Self, &mut ProofTreeBuilder<'tcx>) -> QueryResult<'tcx>,
     ) -> QueryResult<'tcx> {
-        if self.should_use_global_cache() {
+        if self.should_use_global_cache() && inspect.use_global_cache() {
             if let Some(result) = tcx.new_solver_evaluation_cache.get(&canonical_input, tcx) {
                 debug!(?canonical_input, ?result, "cache hit");
+                inspect.cache_hit(CacheHit::Global);
                 return result;
             }
         }
 
-        match self.try_push_stack(tcx, canonical_input) {
+        match self.try_push_stack(tcx, canonical_input, inspect) {
             Ok(()) => {}
             // Our goal is already on the stack, eager return.
             Err(response) => return response,
@@ -231,7 +238,7 @@ impl<'tcx> SearchGraph<'tcx> {
                     result
                 },
                 |this| {
-                    let result = loop_body(this);
+                    let result = loop_body(this, inspect);
                     this.try_finalize_goal(canonical_input, result).then(|| result)
                 },
             )
diff --git a/compiler/rustc_trait_selection/src/solve/trait_goals.rs b/compiler/rustc_trait_selection/src/solve/trait_goals.rs
index f722f2813..ef5f25b1f 100644
--- a/compiler/rustc_trait_selection/src/solve/trait_goals.rs
+++ b/compiler/rustc_trait_selection/src/solve/trait_goals.rs
@@ -7,6 +7,7 @@ use rustc_hir::{LangItem, Movability};
 use rustc_infer::traits::query::NoSolution;
 use rustc_infer::traits::util::supertraits;
 use rustc_middle::traits::solve::{CanonicalResponse, Certainty, Goal, QueryResult};
+use rustc_middle::traits::Reveal;
 use rustc_middle::ty::fast_reject::{DeepRejectCtxt, TreatParams, TreatProjections};
 use rustc_middle::ty::{self, ToPredicate, Ty, TyCtxt};
 use rustc_middle::ty::{TraitPredicate, TypeVisitableExt};
@@ -61,7 +62,7 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
             },
         };
 
-        ecx.probe(|ecx| {
+        ecx.probe_candidate("impl").enter(|ecx| {
             let impl_substs = ecx.fresh_substs_for_item(impl_def_id);
             let impl_trait_ref = impl_trait_ref.subst(tcx, impl_substs);
 
@@ -81,24 +82,26 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
     fn probe_and_match_goal_against_assumption(
         ecx: &mut EvalCtxt<'_, 'tcx>,
         goal: Goal<'tcx, Self>,
-        assumption: ty::Predicate<'tcx>,
+        assumption: ty::Clause<'tcx>,
         then: impl FnOnce(&mut EvalCtxt<'_, 'tcx>) -> QueryResult<'tcx>,
     ) -> QueryResult<'tcx> {
-        if let Some(poly_trait_pred) = assumption.to_opt_poly_trait_pred()
-            && poly_trait_pred.def_id() == goal.predicate.def_id()
-            && poly_trait_pred.polarity() == goal.predicate.polarity
-        {
-            // FIXME: Constness
-            ecx.probe(|ecx| {
-                let assumption_trait_pred =
-                    ecx.instantiate_binder_with_infer(poly_trait_pred);
-                ecx.eq(
-                    goal.param_env,
-                    goal.predicate.trait_ref,
-                    assumption_trait_pred.trait_ref,
-                )?;
-                then(ecx)
-            })
+        if let Some(trait_clause) = assumption.as_trait_clause() {
+            if trait_clause.def_id() == goal.predicate.def_id()
+                && trait_clause.polarity() == goal.predicate.polarity
+            {
+                // FIXME: Constness
+                ecx.probe_candidate("assumption").enter(|ecx| {
+                    let assumption_trait_pred = ecx.instantiate_binder_with_infer(trait_clause);
+                    ecx.eq(
+                        goal.param_env,
+                        goal.predicate.trait_ref,
+                        assumption_trait_pred.trait_ref,
+                    )?;
+                    then(ecx)
+                })
+            } else {
+                Err(NoSolution)
+            }
         } else {
             Err(NoSolution)
         }
@@ -116,6 +119,32 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
             return result;
         }
 
+        // Don't call `type_of` on a local TAIT that's in the defining scope,
+        // since that may require calling `typeck` on the same item we're
+        // currently type checking, which will result in a fatal cycle that
+        // ideally we want to avoid, since we can make progress on this goal
+        // via an alias bound or a locally-inferred hidden type instead.
+        //
+        // Also, don't call `type_of` on a TAIT in `Reveal::All` mode, since
+        // we already normalize the self type in
+        // `assemble_candidates_after_normalizing_self_ty`, and we'd
+        // just be registering an identical candidate here.
+        //
+        // Returning `Err(NoSolution)` here is ok in `SolverMode::Coherence`
+        // since we'll always be registering an ambiguous candidate in
+        // `assemble_candidates_after_normalizing_self_ty` due to normalizing
+        // the TAIT.
+        if let ty::Alias(ty::Opaque, opaque_ty) = goal.predicate.self_ty().kind() {
+            if matches!(goal.param_env.reveal(), Reveal::All)
+                || opaque_ty
+                    .def_id
+                    .as_local()
+                    .is_some_and(|def_id| ecx.can_define_opaque_ty(def_id))
+            {
+                return Err(NoSolution);
+            }
+        }
+
         ecx.probe_and_evaluate_goal_for_constituent_tys(
             goal,
             structural_traits::instantiate_constituent_tys_for_auto_trait,
@@ -132,7 +161,7 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
 
         let tcx = ecx.tcx();
 
-        ecx.probe(|ecx| {
+        ecx.probe_candidate("trait alias").enter(|ecx| {
             let nested_obligations = tcx
                 .predicates_of(goal.predicate.def_id())
                 .instantiate(tcx, goal.predicate.trait_ref.substs);
@@ -344,7 +373,7 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
         if b_ty.is_ty_var() {
             return ecx.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS);
         }
-        ecx.probe(|ecx| {
+        ecx.probe_candidate("builtin unsize").enter(|ecx| {
             match (a_ty.kind(), b_ty.kind()) {
                 // Trait upcasting, or `dyn Trait + Auto + 'a` -> `dyn Trait + 'b`
                 (&ty::Dynamic(_, _, ty::Dyn), &ty::Dynamic(_, _, ty::Dyn)) => {
@@ -396,12 +425,7 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
                         return Err(NoSolution);
                     }
 
-                    let tail_field = a_def
-                        .non_enum_variant()
-                        .fields
-                        .raw
-                        .last()
-                        .expect("expected unsized ADT to have a tail field");
+                    let tail_field = a_def.non_enum_variant().tail();
                     let tail_field_ty = tcx.type_of(tail_field.did);
 
                     let a_tail_ty = tail_field_ty.subst(tcx, a_substs);
@@ -414,7 +438,7 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
                         tcx.mk_substs_from_iter(a_substs.iter().enumerate().map(|(i, a)| {
                             if unsizing_params.contains(i as u32) { b_substs[i] } else { a }
                         }));
-                    let unsized_a_ty = tcx.mk_adt(a_def, new_a_substs);
+                    let unsized_a_ty = Ty::new_adt(tcx, a_def, new_a_substs);
 
                     // Finally, we require that `TailA: Unsize<TailB>` for the tail field
                     // types.
@@ -434,7 +458,7 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
 
                     // Substitute just the tail field of B., and require that they're equal.
                     let unsized_a_ty =
-                        tcx.mk_tup_from_iter(a_rest_tys.iter().chain([b_last_ty]).copied());
+                        Ty::new_tup_from_iter(tcx, a_rest_tys.iter().chain([b_last_ty]).copied());
                     ecx.eq(goal.param_env, unsized_a_ty, b_ty)?;
 
                     // Similar to ADTs, require that the rest of the fields are equal.
@@ -476,7 +500,7 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
         }
 
         let mut unsize_dyn_to_principal = |principal: Option<ty::PolyExistentialTraitRef<'tcx>>| {
-            ecx.probe(|ecx| -> Result<_, NoSolution> {
+            ecx.probe_candidate("upcast dyn to principle").enter(|ecx| -> Result<_, NoSolution> {
                 // Require that all of the trait predicates from A match B, except for
                 // the auto traits. We do this by constructing a new A type with B's
                 // auto traits, and equating these types.
@@ -493,7 +517,7 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
                             .map(ty::Binder::dummy),
                     );
                 let new_a_data = tcx.mk_poly_existential_predicates_from_iter(new_a_data);
-                let new_a_ty = tcx.mk_dynamic(new_a_data, b_region, ty::Dyn);
+                let new_a_ty = Ty::new_dynamic(tcx, new_a_data, b_region, ty::Dyn);
 
                 // We also require that A's lifetime outlives B's lifetime.
                 ecx.eq(goal.param_env, new_a_ty, b_ty)?;
@@ -618,7 +642,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
             ty::Dynamic(..)
             | ty::Param(..)
             | ty::Foreign(..)
-            | ty::Alias(ty::Projection | ty::Inherent, ..)
+            | ty::Alias(ty::Projection | ty::Weak | ty::Inherent, ..)
             | ty::Placeholder(..) => Some(Err(NoSolution)),
 
             ty::Infer(_) | ty::Bound(_, _) => bug!("unexpected type `{self_ty}`"),
@@ -698,7 +722,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
         goal: Goal<'tcx, TraitPredicate<'tcx>>,
         constituent_tys: impl Fn(&EvalCtxt<'_, 'tcx>, Ty<'tcx>) -> Result<Vec<Ty<'tcx>>, NoSolution>,
     ) -> QueryResult<'tcx> {
-        self.probe(|ecx| {
+        self.probe_candidate("constituent tys").enter(|ecx| {
             ecx.add_goals(
                 constituent_tys(ecx, goal.predicate.self_ty())?
                     .into_iter()
diff --git a/compiler/rustc_trait_selection/src/solve/weak_types.rs b/compiler/rustc_trait_selection/src/solve/weak_types.rs
new file mode 100644
index 000000000..b095b54c5
--- /dev/null
+++ b/compiler/rustc_trait_selection/src/solve/weak_types.rs
@@ -0,0 +1,19 @@
+use rustc_middle::traits::solve::{Certainty, Goal, QueryResult};
+use rustc_middle::ty;
+
+use super::EvalCtxt;
+
+impl<'tcx> EvalCtxt<'_, 'tcx> {
+    pub(super) fn normalize_weak_type(
+        &mut self,
+        goal: Goal<'tcx, ty::ProjectionPredicate<'tcx>>,
+    ) -> QueryResult<'tcx> {
+        let tcx = self.tcx();
+        let weak_ty = goal.predicate.projection_ty;
+        let expected = goal.predicate.term.ty().expect("no such thing as a const alias");
+
+        let actual = tcx.type_of(weak_ty.def_id).subst(tcx, weak_ty.substs);
+        self.eq(goal.param_env, expected, actual)?;
+        self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
+    }
+}