diff --git a/Cargo.lock b/Cargo.lock
index cdf6a4cc2de2f..b28eb4faa5b7d 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -3937,6 +3937,7 @@ dependencies = [
  "rustc_hir",
  "rustc_middle",
  "rustc_span",
+ "scoped-tls",
  "tracing",
 ]
 
diff --git a/compiler/rustc_session/src/config.rs b/compiler/rustc_session/src/config.rs
index 43846e65bcab2..119eadf64901b 100644
--- a/compiler/rustc_session/src/config.rs
+++ b/compiler/rustc_session/src/config.rs
@@ -743,6 +743,14 @@ pub enum TraitSolver {
     NextCoherence,
 }
 
+#[derive(Default, Debug, Copy, Clone, Hash, PartialEq, Eq)]
+pub enum DumpSolverProofTree {
+    Always,
+    OnError,
+    #[default]
+    Never,
+}
+
 pub enum Input {
     /// Load source code from a file.
     File(PathBuf),
diff --git a/compiler/rustc_session/src/options.rs b/compiler/rustc_session/src/options.rs
index 05d3e71074ac7..89fd7b4f8df2f 100644
--- a/compiler/rustc_session/src/options.rs
+++ b/compiler/rustc_session/src/options.rs
@@ -418,6 +418,7 @@ mod desc {
         "a `,` separated combination of `bti`, `b-key`, `pac-ret`, or `leaf`";
     pub const parse_proc_macro_execution_strategy: &str =
         "one of supported execution strategies (`same-thread`, or `cross-thread`)";
+    pub const parse_dump_solver_proof_tree: &str = "one of: `always`, `on-request`, `on-error`";
 }
 
 mod parse {
@@ -1237,6 +1238,19 @@ mod parse {
         };
         true
     }
+
+    pub(crate) fn parse_dump_solver_proof_tree(
+        slot: &mut DumpSolverProofTree,
+        v: Option<&str>,
+    ) -> bool {
+        match v {
+            None | Some("always") => *slot = DumpSolverProofTree::Always,
+            Some("never") => *slot = DumpSolverProofTree::Never,
+            Some("on-error") => *slot = DumpSolverProofTree::OnError,
+            _ => return false,
+        };
+        true
+    }
 }
 
 options! {
@@ -1462,8 +1476,11 @@ options! {
         "output statistics about monomorphization collection"),
     dump_mono_stats_format: DumpMonoStatsFormat = (DumpMonoStatsFormat::Markdown, parse_dump_mono_stats, [UNTRACKED],
         "the format to use for -Z dump-mono-stats (`markdown` (default) or `json`)"),
-    dump_solver_proof_tree: bool = (false, parse_bool, [UNTRACKED],
-        "dump a proof tree for every goal evaluated by the new trait solver"),
+    dump_solver_proof_tree: DumpSolverProofTree = (DumpSolverProofTree::Never, parse_dump_solver_proof_tree, [UNTRACKED],
+        "dump a proof tree for every goal evaluated by the new trait solver. If the flag is specified without any options after it
+        then it defaults to `always`. If the flag is not specified at all it defaults to `on-request`."),
+    dump_solver_proof_tree_use_cache: Option<bool> = (None, parse_opt_bool, [UNTRACKED],
+        "determines whether dumped proof trees use the global cache"),
     dwarf_version: Option<u32> = (None, parse_opt_number, [TRACKED],
         "version of DWARF debug information to emit (default: 2 or 4, depending on platform)"),
     dylib_lto: bool = (false, parse_bool, [UNTRACKED],
diff --git a/compiler/rustc_smir/Cargo.toml b/compiler/rustc_smir/Cargo.toml
index 80360a3c73f8d..a6e6de5f785a2 100644
--- a/compiler/rustc_smir/Cargo.toml
+++ b/compiler/rustc_smir/Cargo.toml
@@ -8,6 +8,7 @@ rustc_hir = { path = "../rustc_hir" }
 rustc_middle = { path = "../rustc_middle", optional = true }
 rustc_span = { path = "../rustc_span", optional = true }
 tracing = "0.1"
+scoped-tls = "1.0"
 
 [features]
 default = [
diff --git a/compiler/rustc_smir/src/lib.rs b/compiler/rustc_smir/src/lib.rs
index b00f0a1c15312..fb03633b99b31 100644
--- a/compiler/rustc_smir/src/lib.rs
+++ b/compiler/rustc_smir/src/lib.rs
@@ -19,3 +19,6 @@ pub mod stable_mir;
 
 // Make this module private for now since external users should not call these directly.
 mod rustc_smir;
+
+#[macro_use]
+extern crate scoped_tls;
diff --git a/compiler/rustc_smir/src/stable_mir/mod.rs b/compiler/rustc_smir/src/stable_mir/mod.rs
index 612777b9c7539..5e599a77bcda5 100644
--- a/compiler/rustc_smir/src/stable_mir/mod.rs
+++ b/compiler/rustc_smir/src/stable_mir/mod.rs
@@ -100,18 +100,17 @@ pub trait Context {
     fn rustc_tables(&mut self, f: &mut dyn FnMut(&mut Tables<'_>));
 }
 
-thread_local! {
-    /// A thread local variable that stores a pointer to the tables mapping between TyCtxt
-    /// datastructures and stable MIR datastructures.
-    static TLV: Cell<*mut ()> = const { Cell::new(std::ptr::null_mut()) };
-}
+// A thread local variable that stores a pointer to the tables mapping between TyCtxt
+// datastructures and stable MIR datastructures
+scoped_thread_local! (static TLV: Cell<*mut ()>);
 
 pub fn run(mut context: impl Context, f: impl FnOnce()) {
-    assert!(TLV.get().is_null());
+    assert!(!TLV.is_set());
     fn g<'a>(mut context: &mut (dyn Context + 'a), f: impl FnOnce()) {
-        TLV.set(&mut context as *mut &mut _ as _);
-        f();
-        TLV.replace(std::ptr::null_mut());
+        let ptr: *mut () = &mut context as *mut &mut _ as _;
+        TLV.set(&Cell::new(ptr), || {
+            f();
+        });
     }
     g(&mut context, f);
 }
@@ -119,9 +118,10 @@ pub fn run(mut context: impl Context, f: impl FnOnce()) {
 /// Loads the current context and calls a function with it.
 /// Do not nest these, as that will ICE.
 pub(crate) fn with<R>(f: impl FnOnce(&mut dyn Context) -> R) -> R {
-    let ptr = TLV.replace(std::ptr::null_mut()) as *mut &mut dyn Context;
-    assert!(!ptr.is_null());
-    let ret = f(unsafe { *ptr });
-    TLV.set(ptr as _);
-    ret
+    assert!(TLV.is_set());
+    TLV.with(|tlv| {
+        let ptr = tlv.get();
+        assert!(!ptr.is_null());
+        f(unsafe { *(ptr as *mut &mut dyn Context) })
+    })
 }
diff --git a/compiler/rustc_trait_selection/src/solve/assembly/mod.rs b/compiler/rustc_trait_selection/src/solve/assembly/mod.rs
index 15e08166a8b87..28138054ae5e4 100644
--- a/compiler/rustc_trait_selection/src/solve/assembly/mod.rs
+++ b/compiler/rustc_trait_selection/src/solve/assembly/mod.rs
@@ -331,11 +331,20 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
         candidates
     }
 
-    /// If the self type of a goal is an alias, 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.
     ///
-    /// 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
+    /// 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).
+    ///
+    /// 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,
diff --git a/compiler/rustc_trait_selection/src/solve/eval_ctxt.rs b/compiler/rustc_trait_selection/src/solve/eval_ctxt.rs
index 6b7be73b6317c..3e50829ec9773 100644
--- a/compiler/rustc_trait_selection/src/solve/eval_ctxt.rs
+++ b/compiler/rustc_trait_selection/src/solve/eval_ctxt.rs
@@ -19,7 +19,9 @@ use rustc_middle::ty::{
     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;
@@ -113,9 +115,23 @@ 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.
@@ -177,17 +193,17 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
             var_values: CanonicalVarValues::dummy(),
             nested_goals: NestedGoals::new(),
             tainted: Ok(()),
-            inspect: (infcx.tcx.sess.opts.unstable_opts.dump_solver_proof_tree
-                || matches!(generate_proof_tree, GenerateProofTree::Yes))
-            .then(ProofTreeBuilder::new_root)
-            .unwrap_or_else(ProofTreeBuilder::new_noop),
+            inspect: ProofTreeBuilder::new_maybe_root(infcx.tcx, generate_proof_tree),
         };
         let result = f(&mut ecx);
 
         let tree = ecx.inspect.finalize();
-        if let Some(tree) = &tree {
-            // module to allow more granular RUSTC_LOG filtering to just proof tree output
-            super::inspect::dump::print_tree(tree);
+        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!(
@@ -425,12 +441,8 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
                 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 this predicate :)
-                ty::PredicateKind::Clause(ty::ClauseKind::ConstEvaluatable(_)) => {
-                    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::ConstEquate(_, _) => {
                     bug!("ConstEquate should not be emitted when `-Ztrait-solver=next` is active")
@@ -440,6 +452,9 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
                         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);
diff --git a/compiler/rustc_trait_selection/src/solve/inspect.rs b/compiler/rustc_trait_selection/src/solve/inspect.rs
index 6d7804a8fad2d..2d6717fdad9fa 100644
--- a/compiler/rustc_trait_selection/src/solve/inspect.rs
+++ b/compiler/rustc_trait_selection/src/solve/inspect.rs
@@ -3,9 +3,11 @@ use rustc_middle::traits::solve::inspect::{self, CacheHit, CandidateKind};
 use rustc_middle::traits::solve::{
     CanonicalInput, Certainty, Goal, IsNormalizesToHack, QueryInput, QueryResult,
 };
-use rustc_middle::ty;
+use rustc_middle::ty::{self, TyCtxt};
+use rustc_session::config::DumpSolverProofTree;
 
-pub mod dump;
+use super::eval_ctxt::UseGlobalCache;
+use super::GenerateProofTree;
 
 #[derive(Eq, PartialEq, Debug, Hash, HashStable)]
 pub struct WipGoalEvaluation<'tcx> {
@@ -144,20 +146,42 @@ impl<'tcx> From<WipGoalCandidate<'tcx>> for DebugSolver<'tcx> {
 }
 
 pub struct ProofTreeBuilder<'tcx> {
-    state: Option<Box<DebugSolver<'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>>) -> ProofTreeBuilder<'tcx> {
-        ProofTreeBuilder { state: Some(Box::new(state.into())) }
+    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)
+        self.state.as_mut().map(|boxed| &mut boxed.tree)
     }
 
     pub fn finalize(self) -> Option<inspect::GoalEvaluation<'tcx>> {
-        match *(self.state?) {
+        match self.state?.tree {
             DebugSolver::GoalEvaluation(wip_goal_evaluation) => {
                 Some(wip_goal_evaluation.finalize())
             }
@@ -165,8 +189,46 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
         }
     }
 
-    pub fn new_root() -> ProofTreeBuilder<'tcx> {
-        ProofTreeBuilder::new(DebugSolver::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> {
@@ -186,7 +248,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
             return ProofTreeBuilder { state: None };
         }
 
-        ProofTreeBuilder::new(WipGoalEvaluation {
+        self.nested(WipGoalEvaluation {
             uncanonicalized_goal: goal,
             canonicalized_goal: None,
             evaluation_steps: vec![],
@@ -232,7 +294,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
     }
     pub fn goal_evaluation(&mut self, goal_evaluation: ProofTreeBuilder<'tcx>) {
         if let Some(this) = self.as_mut() {
-            match (this, *goal_evaluation.state.unwrap()) {
+            match (this, goal_evaluation.state.unwrap().tree) {
                 (
                     DebugSolver::AddedGoalsEvaluation(WipAddedGoalsEvaluation {
                         evaluations, ..
@@ -253,7 +315,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
             return ProofTreeBuilder { state: None };
         }
 
-        ProofTreeBuilder::new(WipGoalEvaluationStep {
+        self.nested(WipGoalEvaluationStep {
             instantiated_goal,
             nested_goal_evaluations: vec![],
             candidates: vec![],
@@ -262,7 +324,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
     }
     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()) {
+            match (this, goal_eval_step.state.unwrap().tree) {
                 (DebugSolver::GoalEvaluation(goal_eval), DebugSolver::GoalEvaluationStep(step)) => {
                     goal_eval.evaluation_steps.push(step);
                 }
@@ -276,7 +338,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
             return ProofTreeBuilder { state: None };
         }
 
-        ProofTreeBuilder::new(WipGoalCandidate {
+        self.nested(WipGoalCandidate {
             nested_goal_evaluations: vec![],
             candidates: vec![],
             kind: None,
@@ -296,7 +358,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
 
     pub fn goal_candidate(&mut self, candidate: ProofTreeBuilder<'tcx>) {
         if let Some(this) = self.as_mut() {
-            match (this, *candidate.state.unwrap()) {
+            match (this, candidate.state.unwrap().tree) {
                 (
                     DebugSolver::GoalCandidate(WipGoalCandidate { candidates, .. })
                     | DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep { candidates, .. }),
@@ -312,7 +374,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
             return ProofTreeBuilder { state: None };
         }
 
-        ProofTreeBuilder::new(WipAddedGoalsEvaluation { evaluations: vec![], result: None })
+        self.nested(WipAddedGoalsEvaluation { evaluations: vec![], result: None })
     }
 
     pub fn evaluate_added_goals_loop_start(&mut self) {
@@ -339,7 +401,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
 
     pub fn added_goals_evaluation(&mut self, goals_evaluation: ProofTreeBuilder<'tcx>) {
         if let Some(this) = self.as_mut() {
-            match (this, *goals_evaluation.state.unwrap()) {
+            match (this, goals_evaluation.state.unwrap().tree) {
                 (
                     DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
                         nested_goal_evaluations,
diff --git a/compiler/rustc_trait_selection/src/solve/inspect/dump.rs b/compiler/rustc_trait_selection/src/solve/inspect/dump.rs
deleted file mode 100644
index b755ee8621558..0000000000000
--- a/compiler/rustc_trait_selection/src/solve/inspect/dump.rs
+++ /dev/null
@@ -1,5 +0,0 @@
-use rustc_middle::traits::solve::inspect::GoalEvaluation;
-
-pub fn print_tree(tree: &GoalEvaluation<'_>) {
-    debug!(?tree);
-}
diff --git a/compiler/rustc_trait_selection/src/solve/mod.rs b/compiler/rustc_trait_selection/src/solve/mod.rs
index f3f78cdf09d6e..77809d8d2ba81 100644
--- a/compiler/rustc_trait_selection/src/solve/mod.rs
+++ b/compiler/rustc_trait_selection/src/solve/mod.rs
@@ -33,7 +33,9 @@ mod search_graph;
 mod trait_goals;
 mod weak_types;
 
-pub use eval_ctxt::{EvalCtxt, InferCtxtEvalExt, InferCtxtSelectExt};
+pub use eval_ctxt::{
+    EvalCtxt, GenerateProofTree, InferCtxtEvalExt, InferCtxtSelectExt, UseGlobalCache,
+};
 pub use fulfill::FulfillmentCtxt;
 pub(crate) use normalize::deeply_normalize;
 
@@ -159,6 +161,43 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
         }
     }
 
+    #[instrument(level = "debug", skip(self))]
+    fn compute_const_evaluatable_goal(
+        &mut self,
+        Goal { param_env, predicate: ct }: Goal<'tcx, ty::Const<'tcx>>,
+    ) -> QueryResult<'tcx> {
+        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 {
+                    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)
+            }
+        }
+    }
+
     #[instrument(level = "debug", skip(self), ret)]
     fn compute_const_arg_has_type_goal(
         &mut self,
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 d167ee46b3936..f00456e26df52 100644
--- a/compiler/rustc_trait_selection/src/solve/search_graph/mod.rs
+++ b/compiler/rustc_trait_selection/src/solve/search_graph/mod.rs
@@ -213,7 +213,7 @@ impl<'tcx> SearchGraph<'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);
diff --git a/compiler/rustc_trait_selection/src/traits/error_reporting/mod.rs b/compiler/rustc_trait_selection/src/traits/error_reporting/mod.rs
index 5fff645dd22af..2bab383ef5940 100644
--- a/compiler/rustc_trait_selection/src/traits/error_reporting/mod.rs
+++ b/compiler/rustc_trait_selection/src/traits/error_reporting/mod.rs
@@ -10,6 +10,7 @@ use super::{
 use crate::infer::error_reporting::{TyCategory, TypeAnnotationNeeded as ErrorCode};
 use crate::infer::type_variable::{TypeVariableOrigin, TypeVariableOriginKind};
 use crate::infer::{self, InferCtxt};
+use crate::solve::{GenerateProofTree, InferCtxtEvalExt, UseGlobalCache};
 use crate::traits::query::evaluate_obligation::InferCtxtExt as _;
 use crate::traits::query::normalize::QueryNormalizeExt as _;
 use crate::traits::specialize::to_pretty_impl_header;
@@ -28,6 +29,7 @@ use rustc_hir::{GenericParam, Item, Node};
 use rustc_infer::infer::error_reporting::TypeErrCtxt;
 use rustc_infer::infer::{InferOk, TypeTrace};
 use rustc_middle::traits::select::OverflowError;
+use rustc_middle::traits::solve::Goal;
 use rustc_middle::traits::SelectionOutputTypeParameterMismatch;
 use rustc_middle::ty::abstract_const::NotConstEvaluatable;
 use rustc_middle::ty::error::{ExpectedFound, TypeError};
@@ -37,13 +39,14 @@ use rustc_middle::ty::{
     self, SubtypePredicate, ToPolyTraitRef, ToPredicate, TraitRef, Ty, TyCtxt, TypeFoldable,
     TypeVisitable, TypeVisitableExt,
 };
-use rustc_session::config::TraitSolver;
+use rustc_session::config::{DumpSolverProofTree, TraitSolver};
 use rustc_session::Limit;
 use rustc_span::def_id::LOCAL_CRATE;
 use rustc_span::symbol::sym;
 use rustc_span::{ExpnKind, Span, DUMMY_SP};
 use std::borrow::Cow;
 use std::fmt;
+use std::io::Write;
 use std::iter;
 use std::ops::ControlFlow;
 use suggestions::TypeErrCtxtExt as _;
@@ -630,6 +633,11 @@ impl<'tcx> TypeErrCtxtExt<'tcx> for TypeErrCtxt<'_, 'tcx> {
         error: &SelectionError<'tcx>,
     ) {
         let tcx = self.tcx;
+
+        if tcx.sess.opts.unstable_opts.dump_solver_proof_tree == DumpSolverProofTree::OnError {
+            dump_proof_tree(root_obligation, self.infcx);
+        }
+
         let mut span = obligation.cause.span;
         // FIXME: statically guarantee this by tainting after the diagnostic is emitted
         self.set_tainted_by_errors(
@@ -1522,6 +1530,10 @@ impl<'tcx> InferCtxtPrivExt<'tcx> for TypeErrCtxt<'_, 'tcx> {
 
     #[instrument(skip(self), level = "debug")]
     fn report_fulfillment_error(&self, error: &FulfillmentError<'tcx>) {
+        if self.tcx.sess.opts.unstable_opts.dump_solver_proof_tree == DumpSolverProofTree::OnError {
+            dump_proof_tree(&error.root_obligation, self.infcx);
+        }
+
         match error.code {
             FulfillmentErrorCode::CodeSelectionError(ref selection_error) => {
                 self.report_selection_error(
@@ -3492,3 +3504,16 @@ pub enum DefIdOrName {
     DefId(DefId),
     Name(&'static str),
 }
+
+pub fn dump_proof_tree<'tcx>(o: &Obligation<'tcx, ty::Predicate<'tcx>>, infcx: &InferCtxt<'tcx>) {
+    infcx.probe(|_| {
+        let goal = Goal { predicate: o.predicate, param_env: o.param_env };
+        let tree = infcx
+            .evaluate_root_goal(goal, GenerateProofTree::Yes(UseGlobalCache::No))
+            .1
+            .expect("proof tree should have been generated");
+        let mut lock = std::io::stdout().lock();
+        let _ = lock.write_fmt(format_args!("{tree:?}"));
+        let _ = lock.flush();
+    });
+}
diff --git a/src/doc/rustc/src/platform-support.md b/src/doc/rustc/src/platform-support.md
index 6d1729e57b10f..e9487ef81e795 100644
--- a/src/doc/rustc/src/platform-support.md
+++ b/src/doc/rustc/src/platform-support.md
@@ -87,7 +87,7 @@ target | notes
 `aarch64-unknown-linux-musl` | ARM64 Linux with MUSL
 `arm-unknown-linux-gnueabi` | ARMv6 Linux (kernel 3.2, glibc 2.17)
 `arm-unknown-linux-gnueabihf` | ARMv6 Linux, hardfloat (kernel 3.2, glibc 2.17)
-`armv7-unknown-linux-gnueabihf` | ARMv7 Linux, hardfloat (kernel 3.2, glibc 2.17)
+`armv7-unknown-linux-gnueabihf` | ARMv7-A Linux, hardfloat (kernel 3.2, glibc 2.17)
 [`loongarch64-unknown-linux-gnu`](platform-support/loongarch-linux.md) | LoongArch64 Linux, LP64D ABI (kernel 5.19, glibc 2.36)
 `mips-unknown-linux-gnu` | MIPS Linux (kernel 4.4, glibc 2.23)
 `mips64-unknown-linux-gnuabi64` | MIPS64 Linux, n64 ABI (kernel 4.4, glibc 2.23)
@@ -133,17 +133,17 @@ target | std | notes
 `aarch64-unknown-none-softfloat` | * | Bare ARM64, softfloat
 `aarch64-unknown-none` | * | Bare ARM64, hardfloat
 [`aarch64-unknown-uefi`](platform-support/unknown-uefi.md) | * | ARM64 UEFI
-[`arm-linux-androideabi`](platform-support/android.md) | ✓ | ARMv7 Android
+[`arm-linux-androideabi`](platform-support/android.md) | ✓ | ARMv6 Android
 `arm-unknown-linux-musleabi` | ✓ | ARMv6 Linux with MUSL
 `arm-unknown-linux-musleabihf` | ✓ | ARMv6 Linux with MUSL, hardfloat
 `armebv7r-none-eabi` | * | Bare ARMv7-R, Big Endian
 `armebv7r-none-eabihf` | * | Bare ARMv7-R, Big Endian, hardfloat
 `armv5te-unknown-linux-gnueabi` | ✓ | ARMv5TE Linux (kernel 4.4, glibc 2.23)
 `armv5te-unknown-linux-musleabi` | ✓ | ARMv5TE Linux with MUSL
-[`armv7-linux-androideabi`](platform-support/android.md) | ✓ | ARMv7a Android
-`armv7-unknown-linux-gnueabi` | ✓ |ARMv7 Linux (kernel 4.15, glibc 2.27)
-`armv7-unknown-linux-musleabi` | ✓ |ARMv7 Linux with MUSL
-`armv7-unknown-linux-musleabihf` | ✓ | ARMv7 Linux with MUSL, hardfloat
+[`armv7-linux-androideabi`](platform-support/android.md) | ✓ | ARMv7-A Android
+`armv7-unknown-linux-gnueabi` | ✓ | ARMv7-A Linux (kernel 4.15, glibc 2.27)
+`armv7-unknown-linux-musleabi` | ✓ | ARMv7-A Linux with MUSL
+`armv7-unknown-linux-musleabihf` | ✓ | ARMv7-A Linux with MUSL, hardfloat
 `armv7a-none-eabi` | * | Bare ARMv7-A
 `armv7r-none-eabi` | * | Bare ARMv7-R
 `armv7r-none-eabihf` | * | Bare ARMv7-R, hardfloat
@@ -167,15 +167,15 @@ target | std | notes
 `riscv64imac-unknown-none-elf` | * | Bare RISC-V (RV64IMAC ISA)
 `sparc64-unknown-linux-gnu` | ✓ | SPARC Linux (kernel 4.4, glibc 2.23)
 `sparcv9-sun-solaris` | ✓ | SPARC Solaris 10/11, illumos
-`thumbv6m-none-eabi` | * | Bare Cortex-M0, M0+, M1
-`thumbv7em-none-eabi` | * | Bare Cortex-M4, M7
-`thumbv7em-none-eabihf` | * | Bare Cortex-M4F, M7F, FPU, hardfloat
-`thumbv7m-none-eabi` | * | Bare Cortex-M3
-[`thumbv7neon-linux-androideabi`](platform-support/android.md) | ✓ | Thumb2-mode ARMv7a Android with NEON
-`thumbv7neon-unknown-linux-gnueabihf` | ✓ | Thumb2-mode ARMv7a Linux with NEON (kernel 4.4, glibc 2.23)
-`thumbv8m.base-none-eabi` | * | ARMv8-M Baseline
-`thumbv8m.main-none-eabi` | * | ARMv8-M Mainline
-`thumbv8m.main-none-eabihf` | * | ARMv8-M Mainline, hardfloat
+`thumbv6m-none-eabi` | * | Bare ARMv6-M
+`thumbv7em-none-eabi` | * | Bare ARMv7E-M
+`thumbv7em-none-eabihf` | * | Bare ARMV7E-M, hardfloat
+`thumbv7m-none-eabi` | * | Bare ARMv7-M
+[`thumbv7neon-linux-androideabi`](platform-support/android.md) | ✓ | Thumb2-mode ARMv7-A Android with NEON
+`thumbv7neon-unknown-linux-gnueabihf` | ✓ | Thumb2-mode ARMv7-A Linux with NEON (kernel 4.4, glibc 2.23)
+`thumbv8m.base-none-eabi` | * | Bare ARMv8-M Baseline
+`thumbv8m.main-none-eabi` | * | Bare ARMv8-M Mainline
+`thumbv8m.main-none-eabihf` | * | Bare ARMv8-M Mainline, hardfloat
 `wasm32-unknown-emscripten` | ✓ | WebAssembly via Emscripten
 `wasm32-unknown-unknown` | ✓ | WebAssembly
 `wasm32-wasi` | ✓ | WebAssembly with WASI
@@ -234,26 +234,26 @@ target | std | host | notes
 [`aarch64_be-unknown-netbsd`](platform-support/netbsd.md) | ✓ | ✓ | ARM64 NetBSD (big-endian)
 [`arm64_32-apple-watchos`](platform-support/apple-watchos.md) | ✓ | | ARM Apple WatchOS 64-bit with 32-bit pointers
 [`armeb-unknown-linux-gnueabi`](platform-support/armeb-unknown-linux-gnueabi.md) | ✓ | ? | ARM BE8 the default ARM big-endian architecture since [ARMv6](https://developer.arm.com/documentation/101754/0616/armlink-Reference/armlink-Command-line-Options/--be8?lang=en).
-`armv4t-none-eabi` | * |  | ARMv4T A32
-`armv4t-unknown-linux-gnueabi` | ? |  |
-[`armv5te-none-eabi`](platform-support/armv5te-none-eabi.md) | * | | ARMv5TE A32
+`armv4t-none-eabi` | * |  | Bare ARMv4T
+`armv4t-unknown-linux-gnueabi` | ? |  | ARMv4T Linux
+[`armv5te-none-eabi`](platform-support/armv5te-none-eabi.md) | * | | Bare ARMv5TE
 `armv5te-unknown-linux-uclibceabi` | ? |  | ARMv5TE Linux with uClibc
 `armv6-unknown-freebsd` | ✓ | ✓ | ARMv6 FreeBSD
 [`armv6-unknown-netbsd-eabihf`](platform-support/netbsd.md) | ✓ | ✓ | ARMv6 NetBSD w/hard-float
 [`armv6k-nintendo-3ds`](platform-support/armv6k-nintendo-3ds.md) | ? |  | ARMv6K Nintendo 3DS, Horizon (Requires devkitARM toolchain)
-`armv7-apple-ios` | ✓ |  | ARMv7 iOS, Cortex-a8
-[`armv7-sony-vita-newlibeabihf`](platform-support/armv7-sony-vita-newlibeabihf.md) | ? |  | ARM Cortex-A9 Sony PlayStation Vita (requires VITASDK toolchain)
-[`armv7-unknown-linux-ohos`](platform-support/openharmony.md) | ✓ |  | ARMv7 OpenHarmony |
-[`armv7-unknown-linux-uclibceabi`](platform-support/armv7-unknown-linux-uclibceabi.md) | ✓ | ✓ | ARMv7 Linux with uClibc, softfloat
-[`armv7-unknown-linux-uclibceabihf`](platform-support/armv7-unknown-linux-uclibceabihf.md) | ✓ | ? | ARMv7 Linux with uClibc, hardfloat
-`armv7-unknown-freebsd` | ✓ | ✓ | ARMv7 FreeBSD
-[`armv7-unknown-netbsd-eabihf`](platform-support/netbsd.md) | ✓ | ✓ | ARMv7 NetBSD w/hard-float
-`armv7-wrs-vxworks-eabihf` | ? |  |
+`armv7-apple-ios` | ✓ |  | ARMv7-A Cortex-A8 iOS
+[`armv7-sony-vita-newlibeabihf`](platform-support/armv7-sony-vita-newlibeabihf.md) | ? |  | ARMv7-A Cortex-A9 Sony PlayStation Vita (requires VITASDK toolchain)
+[`armv7-unknown-linux-ohos`](platform-support/openharmony.md) | ✓ |  | ARMv7-A OpenHarmony |
+[`armv7-unknown-linux-uclibceabi`](platform-support/armv7-unknown-linux-uclibceabi.md) | ✓ | ✓ | ARMv7-A Linux with uClibc, softfloat
+[`armv7-unknown-linux-uclibceabihf`](platform-support/armv7-unknown-linux-uclibceabihf.md) | ✓ | ? | ARMv7-A Linux with uClibc, hardfloat
+`armv7-unknown-freebsd` | ✓ | ✓ | ARMv7-A FreeBSD
+[`armv7-unknown-netbsd-eabihf`](platform-support/netbsd.md) | ✓ | ✓ | ARMv7-A NetBSD w/hard-float
+`armv7-wrs-vxworks-eabihf` | ? |  | ARMv7-A for VxWorks
 [`armv7a-kmc-solid_asp3-eabi`](platform-support/kmc-solid.md) | ✓ |  | ARM SOLID with TOPPERS/ASP3
 [`armv7a-kmc-solid_asp3-eabihf`](platform-support/kmc-solid.md) | ✓ |  | ARM SOLID with TOPPERS/ASP3, hardfloat
-`armv7a-none-eabihf` | * | | ARM Cortex-A, hardfloat
-[`armv7k-apple-watchos`](platform-support/apple-watchos.md) | ✓ | | ARM Apple WatchOS
-`armv7s-apple-ios` | ✓ |  |
+`armv7a-none-eabihf` | * | | Bare ARMv7-A, hardfloat
+[`armv7k-apple-watchos`](platform-support/apple-watchos.md) | ✓ | | ARMv7-A Apple WatchOS
+`armv7s-apple-ios` | ✓ |  | ARMv7-A Apple-A6 Apple iOS
 `avr-unknown-gnu-atmega328` | * |  | AVR. Requires `-Z build-std=core`
 `bpfeb-unknown-none` | * |  | BPF (big endian)
 `bpfel-unknown-none` | * |  | BPF (little endian)
@@ -310,11 +310,11 @@ target | std | host | notes
 `sparc-unknown-linux-gnu` | ✓ |  | 32-bit SPARC Linux
 [`sparc64-unknown-netbsd`](platform-support/netbsd.md) | ✓ | ✓ | NetBSD/sparc64
 [`sparc64-unknown-openbsd`](platform-support/openbsd.md) | ✓ | ✓ | OpenBSD/sparc64
-`thumbv4t-none-eabi` | * |  | ARMv4T T32
-[`thumbv5te-none-eabi`](platform-support/armv5te-none-eabi.md) | * | | ARMv5TE T32
+`thumbv4t-none-eabi` | * |  | Thumb-mode Bare ARMv4T
+[`thumbv5te-none-eabi`](platform-support/armv5te-none-eabi.md) | * | | Thumb-mode Bare ARMv5TE
 `thumbv7a-pc-windows-msvc` | ? |  |
 `thumbv7a-uwp-windows-msvc` | ✓ |  |
-`thumbv7neon-unknown-linux-musleabihf` | ? |  | Thumb2-mode ARMv7a Linux with NEON, MUSL
+`thumbv7neon-unknown-linux-musleabihf` | ? |  | Thumb2-mode ARMv7-A Linux with NEON, MUSL
 [`wasm64-unknown-unknown`](platform-support/wasm64-unknown-unknown.md) | ? |  | WebAssembly
 `x86_64-apple-ios-macabi` | ✓ |  | Apple Catalyst on x86_64
 [`x86_64-apple-tvos`](platform-support/apple-tvos.md) | ? | | x86 64-bit tvOS
diff --git a/tests/ui/const-generics/defaults/default-param-wf-concrete.stderr b/tests/ui/const-generics/defaults/default-param-wf-concrete.next.stderr
similarity index 87%
rename from tests/ui/const-generics/defaults/default-param-wf-concrete.stderr
rename to tests/ui/const-generics/defaults/default-param-wf-concrete.next.stderr
index e8ebddade5c16..4259ce2b626fe 100644
--- a/tests/ui/const-generics/defaults/default-param-wf-concrete.stderr
+++ b/tests/ui/const-generics/defaults/default-param-wf-concrete.next.stderr
@@ -1,5 +1,5 @@
 error[E0080]: evaluation of constant value failed
-  --> $DIR/default-param-wf-concrete.rs:1:28
+  --> $DIR/default-param-wf-concrete.rs:4:28
    |
 LL | struct Foo<const N: u8 = { 255 + 1 }>;
    |                            ^^^^^^^ attempt to compute `u8::MAX + 1_u8`, which would overflow
diff --git a/tests/ui/const-generics/defaults/default-param-wf-concrete.old.stderr b/tests/ui/const-generics/defaults/default-param-wf-concrete.old.stderr
new file mode 100644
index 0000000000000..4259ce2b626fe
--- /dev/null
+++ b/tests/ui/const-generics/defaults/default-param-wf-concrete.old.stderr
@@ -0,0 +1,9 @@
+error[E0080]: evaluation of constant value failed
+  --> $DIR/default-param-wf-concrete.rs:4:28
+   |
+LL | struct Foo<const N: u8 = { 255 + 1 }>;
+   |                            ^^^^^^^ attempt to compute `u8::MAX + 1_u8`, which would overflow
+
+error: aborting due to previous error
+
+For more information about this error, try `rustc --explain E0080`.
diff --git a/tests/ui/const-generics/defaults/default-param-wf-concrete.rs b/tests/ui/const-generics/defaults/default-param-wf-concrete.rs
index 41a52c7eb0d83..09a00dd8e701b 100644
--- a/tests/ui/const-generics/defaults/default-param-wf-concrete.rs
+++ b/tests/ui/const-generics/defaults/default-param-wf-concrete.rs
@@ -1,3 +1,6 @@
+// revisions: old next
+//[next] compile-flags: -Ztrait-solver=next
+
 struct Foo<const N: u8 = { 255 + 1 }>;
 //~^ ERROR evaluation of constant value failed
 fn main() {}
diff --git a/tests/ui/consts/const-len-underflow-separate-spans.stderr b/tests/ui/consts/const-len-underflow-separate-spans.next.stderr
similarity index 78%
rename from tests/ui/consts/const-len-underflow-separate-spans.stderr
rename to tests/ui/consts/const-len-underflow-separate-spans.next.stderr
index 269553631cc67..d9208d0706af2 100644
--- a/tests/ui/consts/const-len-underflow-separate-spans.stderr
+++ b/tests/ui/consts/const-len-underflow-separate-spans.next.stderr
@@ -1,11 +1,11 @@
 error[E0080]: evaluation of constant value failed
-  --> $DIR/const-len-underflow-separate-spans.rs:7:20
+  --> $DIR/const-len-underflow-separate-spans.rs:10:20
    |
 LL | const LEN: usize = ONE - TWO;
    |                    ^^^^^^^^^ attempt to compute `1_usize - 2_usize`, which would overflow
 
 note: erroneous constant used
-  --> $DIR/const-len-underflow-separate-spans.rs:11:17
+  --> $DIR/const-len-underflow-separate-spans.rs:14:17
    |
 LL |     let a: [i8; LEN] = unimplemented!();
    |                 ^^^
diff --git a/tests/ui/consts/const-len-underflow-separate-spans.old.stderr b/tests/ui/consts/const-len-underflow-separate-spans.old.stderr
new file mode 100644
index 0000000000000..d9208d0706af2
--- /dev/null
+++ b/tests/ui/consts/const-len-underflow-separate-spans.old.stderr
@@ -0,0 +1,15 @@
+error[E0080]: evaluation of constant value failed
+  --> $DIR/const-len-underflow-separate-spans.rs:10:20
+   |
+LL | const LEN: usize = ONE - TWO;
+   |                    ^^^^^^^^^ attempt to compute `1_usize - 2_usize`, which would overflow
+
+note: erroneous constant used
+  --> $DIR/const-len-underflow-separate-spans.rs:14:17
+   |
+LL |     let a: [i8; LEN] = unimplemented!();
+   |                 ^^^
+
+error: aborting due to previous error
+
+For more information about this error, try `rustc --explain E0080`.
diff --git a/tests/ui/consts/const-len-underflow-separate-spans.rs b/tests/ui/consts/const-len-underflow-separate-spans.rs
index 4544c8876ae09..55704b641543b 100644
--- a/tests/ui/consts/const-len-underflow-separate-spans.rs
+++ b/tests/ui/consts/const-len-underflow-separate-spans.rs
@@ -2,6 +2,9 @@
 // spot (where the underflow occurred), while also providing the
 // overall context for what caused the evaluation.
 
+// revisions: old next
+//[next] compile-flags: -Ztrait-solver=next
+
 const ONE: usize = 1;
 const TWO: usize = 2;
 const LEN: usize = ONE - TWO;