Uplift inspect into rustc_type_ir

8 files changed, 22 insertions, 520 deletions

diff --git a/compiler/rustc_middle/src/arena.rs b/compiler/rustc_middle/src/arena.rs
index 13719268737..7392eb6c2bb 100644
--- a/compiler/rustc_middle/src/arena.rs
+++ b/compiler/rustc_middle/src/arena.rs
@@ -61,7 +61,7 @@ macro_rules! arena_types {
             [] dtorck_constraint: rustc_middle::traits::query::DropckConstraint<'tcx>,
             [] candidate_step: rustc_middle::traits::query::CandidateStep<'tcx>,
             [] autoderef_bad_ty: rustc_middle::traits::query::MethodAutoderefBadTy<'tcx>,
-            [] canonical_goal_evaluation: rustc_middle::traits::solve::inspect::GoalEvaluationStep<'tcx>,
+            [] canonical_goal_evaluation: rustc_next_trait_solver::solve::inspect::GoalEvaluationStep<rustc_middle::ty::TyCtxt<'tcx>>,
             [] query_region_constraints: rustc_middle::infer::canonical::QueryRegionConstraints<'tcx>,
             [] type_op_subtype:
                 rustc_middle::infer::canonical::Canonical<'tcx,
diff --git a/compiler/rustc_middle/src/traits/mod.rs b/compiler/rustc_middle/src/traits/mod.rs
index fb796bf87a1..62e71c4db11 100644
--- a/compiler/rustc_middle/src/traits/mod.rs
+++ b/compiler/rustc_middle/src/traits/mod.rs
@@ -9,7 +9,6 @@ pub mod specialization_graph;
 mod structural_impls;
 pub mod util;
 
-use crate::infer::canonical::Canonical;
 use crate::mir::ConstraintCategory;
 use crate::ty::abstract_const::NotConstEvaluatable;
 use crate::ty::GenericArgsRef;
@@ -32,6 +31,8 @@ use std::borrow::Cow;
 use std::hash::{Hash, Hasher};
 
 pub use self::select::{EvaluationCache, EvaluationResult, OverflowError, SelectionCache};
+// FIXME: Remove this import and import via `solve::`
+pub use rustc_next_trait_solver::solve::BuiltinImplSource;
 
 /// Depending on the stage of compilation, we want projection to be
 /// more or less conservative.
@@ -736,32 +737,6 @@ pub struct ImplSourceUserDefinedData<'tcx, N> {
     pub nested: Vec<N>,
 }
 
-#[derive(Copy, Clone, PartialEq, Eq, TyEncodable, TyDecodable, HashStable, Debug)]
-pub enum BuiltinImplSource {
-    /// Some builtin impl we don't need to differentiate. This should be used
-    /// unless more specific information is necessary.
-    Misc,
-    /// A builtin impl for trait objects.
-    ///
-    /// The vtable is formed by concatenating together the method lists of
-    /// the base object trait and all supertraits, pointers to supertrait vtable will
-    /// be provided when necessary; this is the start of `upcast_trait_ref`'s methods
-    /// in that vtable.
-    Object { vtable_base: usize },
-    /// The vtable is formed by concatenating together the method lists of
-    /// the base object trait and all supertraits, pointers to supertrait vtable will
-    /// be provided when necessary; this is the position of `upcast_trait_ref`'s vtable
-    /// within that vtable.
-    TraitUpcasting { vtable_vptr_slot: Option<usize> },
-    /// Unsizing a tuple like `(A, B, ..., X)` to `(A, B, ..., Y)` if `X` unsizes to `Y`.
-    ///
-    /// This needs to be a separate variant as it is still unstable and we need to emit
-    /// a feature error when using it on stable.
-    TupleUnsizing,
-}
-
-TrivialTypeTraversalImpls! { BuiltinImplSource }
-
 #[derive(Clone, Debug, PartialEq, Eq, Hash, HashStable, PartialOrd, Ord)]
 pub enum ObjectSafetyViolation {
     /// `Self: Sized` declared on the trait.
diff --git a/compiler/rustc_middle/src/traits/query.rs b/compiler/rustc_middle/src/traits/query.rs
index 70f3532e3ab..66e50307733 100644
--- a/compiler/rustc_middle/src/traits/query.rs
+++ b/compiler/rustc_middle/src/traits/query.rs
@@ -12,6 +12,8 @@ use crate::ty::GenericArg;
 use crate::ty::{self, Ty, TyCtxt};
 use rustc_macros::{HashStable, TypeFoldable, TypeVisitable};
 use rustc_span::Span;
+// FIXME: Remove this import and import via `traits::solve`.
+pub use rustc_next_trait_solver::solve::NoSolution;
 
 pub mod type_op {
     use crate::ty::fold::TypeFoldable;
@@ -89,9 +91,6 @@ pub type CanonicalTypeOpProvePredicateGoal<'tcx> =
 pub type CanonicalTypeOpNormalizeGoal<'tcx, T> =
     Canonical<'tcx, ty::ParamEnvAnd<'tcx, type_op::Normalize<T>>>;
 
-#[derive(Copy, Clone, Debug, Hash, HashStable, PartialEq, Eq)]
-pub struct NoSolution;
-
 impl<'tcx> From<TypeError<'tcx>> for NoSolution {
     fn from(_: TypeError<'tcx>) -> NoSolution {
         NoSolution
diff --git a/compiler/rustc_middle/src/traits/solve.rs b/compiler/rustc_middle/src/traits/solve.rs
index efb99047d38..c8c16ec1e2c 100644
--- a/compiler/rustc_middle/src/traits/solve.rs
+++ b/compiler/rustc_middle/src/traits/solve.rs
@@ -3,92 +3,22 @@ use rustc_data_structures::intern::Interned;
 use rustc_macros::{HashStable, TypeFoldable, TypeVisitable};
 use rustc_next_trait_solver as ir;
 pub use rustc_next_trait_solver::solve::*;
-use rustc_span::def_id::DefId;
 
-use crate::infer::canonical::{CanonicalVarValues, QueryRegionConstraints};
-use crate::traits::query::NoSolution;
-use crate::traits::Canonical;
+use crate::infer::canonical::QueryRegionConstraints;
 use crate::ty::{
     self, FallibleTypeFolder, Ty, TyCtxt, TypeFoldable, TypeFolder, TypeVisitable, TypeVisitor,
 };
 
-use super::BuiltinImplSource;
-
 mod cache;
-pub mod inspect;
 
 pub use cache::{CacheData, EvaluationCache};
 
-pub type Goal<'tcx, P> = ir_solve::Goal<TyCtxt<'tcx>, P>;
-pub type QueryInput<'tcx, P> = ir_solve::QueryInput<TyCtxt<'tcx>, P>;
-
-#[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, HashStable, TypeFoldable, TypeVisitable)]
-pub struct Response<'tcx> {
-    pub certainty: Certainty,
-    pub var_values: CanonicalVarValues<'tcx>,
-    /// Additional constraints returned by this query.
-    pub external_constraints: ExternalConstraints<'tcx>,
-}
-
-#[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, HashStable, TypeFoldable, TypeVisitable)]
-pub enum Certainty {
-    Yes,
-    Maybe(MaybeCause),
-}
-
-impl Certainty {
-    pub const AMBIGUOUS: Certainty = Certainty::Maybe(MaybeCause::Ambiguity);
-
-    /// Use this function to merge the certainty of multiple nested subgoals.
-    ///
-    /// Given an impl like `impl<T: Foo + Bar> Baz for T {}`, we have 2 nested
-    /// subgoals whenever we use the impl as a candidate: `T: Foo` and `T: Bar`.
-    /// If evaluating `T: Foo` results in ambiguity and `T: Bar` results in
-    /// success, we merge these two responses. This results in ambiguity.
-    ///
-    /// If we unify ambiguity with overflow, we return overflow. This doesn't matter
-    /// inside of the solver as we do not distinguish ambiguity from overflow. It does
-    /// however matter for diagnostics. If `T: Foo` resulted in overflow and `T: Bar`
-    /// in ambiguity without changing the inference state, we still want to tell the
-    /// user that `T: Baz` results in overflow.
-    pub fn unify_with(self, other: Certainty) -> Certainty {
-        match (self, other) {
-            (Certainty::Yes, Certainty::Yes) => Certainty::Yes,
-            (Certainty::Yes, Certainty::Maybe(_)) => other,
-            (Certainty::Maybe(_), Certainty::Yes) => self,
-            (Certainty::Maybe(a), Certainty::Maybe(b)) => Certainty::Maybe(a.unify_with(b)),
-        }
-    }
-
-    pub const fn overflow(suggest_increasing_limit: bool) -> Certainty {
-        Certainty::Maybe(MaybeCause::Overflow { suggest_increasing_limit })
-    }
-}
-
-/// Why we failed to evaluate a goal.
-#[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, HashStable, TypeFoldable, TypeVisitable)]
-pub enum MaybeCause {
-    /// We failed due to ambiguity. This ambiguity can either
-    /// be a true ambiguity, i.e. there are multiple different answers,
-    /// or we hit a case where we just don't bother, e.g. `?x: Trait` goals.
-    Ambiguity,
-    /// We gave up due to an overflow, most often by hitting the recursion limit.
-    Overflow { suggest_increasing_limit: bool },
-}
-
-impl MaybeCause {
-    fn unify_with(self, other: MaybeCause) -> MaybeCause {
-        match (self, other) {
-            (MaybeCause::Ambiguity, MaybeCause::Ambiguity) => MaybeCause::Ambiguity,
-            (MaybeCause::Ambiguity, MaybeCause::Overflow { .. }) => other,
-            (MaybeCause::Overflow { .. }, MaybeCause::Ambiguity) => self,
-            (
-                MaybeCause::Overflow { suggest_increasing_limit: a },
-                MaybeCause::Overflow { suggest_increasing_limit: b },
-            ) => MaybeCause::Overflow { suggest_increasing_limit: a || b },
-        }
-    }
-}
+pub type Goal<'tcx, P> = ir::solve::Goal<TyCtxt<'tcx>, P>;
+pub type QueryInput<'tcx, P> = ir::solve::QueryInput<TyCtxt<'tcx>, P>;
+pub type QueryResult<'tcx> = ir::solve::QueryResult<TyCtxt<'tcx>>;
+pub type CandidateSource<'tcx> = ir::solve::CandidateSource<TyCtxt<'tcx>>;
+pub type CanonicalInput<'tcx, P = ty::Predicate<'tcx>> = ir::solve::CanonicalInput<TyCtxt<'tcx>, P>;
+pub type CanonicalResponse<'tcx> = ir::solve::CanonicalResponse<TyCtxt<'tcx>>;
 
 /// Additional constraints returned on success.
 #[derive(Debug, PartialEq, Eq, Clone, Hash, HashStable, Default)]
@@ -107,18 +37,6 @@ impl<'tcx> std::ops::Deref for PredefinedOpaques<'tcx> {
     }
 }
 
-pub type CanonicalInput<'tcx, T = ty::Predicate<'tcx>> = Canonical<'tcx, QueryInput<'tcx, T>>;
-
-pub type CanonicalResponse<'tcx> = Canonical<'tcx, Response<'tcx>>;
-
-/// The result of evaluating a canonical query.
-///
-/// FIXME: We use a different type than the existing canonical queries. This is because
-/// we need to add a `Certainty` for `overflow` and may want to restructure this code without
-/// having to worry about changes to currently used code. Once we've made progress on this
-/// solver, merge the two responses again.
-pub type QueryResult<'tcx> = Result<CanonicalResponse<'tcx>, NoSolution>;
-
 #[derive(Debug, PartialEq, Eq, Copy, Clone, Hash, HashStable)]
 pub struct ExternalConstraints<'tcx>(pub(crate) Interned<'tcx, ExternalConstraintsData<'tcx>>);
 
@@ -225,68 +143,3 @@ impl<'tcx> TypeVisitable<TyCtxt<'tcx>> for PredefinedOpaques<'tcx> {
         self.opaque_types.visit_with(visitor)
     }
 }
-
-/// Possible ways the given goal can be proven.
-#[derive(Debug, Clone, Copy, PartialEq, Eq)]
-pub enum CandidateSource {
-    /// A user written impl.
-    ///
-    /// ## Examples
-    ///
-    /// ```rust
-    /// fn main() {
-    ///     let x: Vec<u32> = Vec::new();
-    ///     // This uses the impl from the standard library to prove `Vec<T>: Clone`.
-    ///     let y = x.clone();
-    /// }
-    /// ```
-    Impl(DefId),
-    /// A builtin impl generated by the compiler. When adding a new special
-    /// trait, try to use actual impls whenever possible. Builtin impls should
-    /// only be used in cases where the impl cannot be manually be written.
-    ///
-    /// 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.
-    BuiltinImpl(BuiltinImplSource),
-    /// An assumption from the environment.
-    ///
-    /// More precisely we've used the `n-th` assumption in the `param_env`.
-    ///
-    /// ## Examples
-    ///
-    /// ```rust
-    /// fn is_clone<T: Clone>(x: T) -> (T, T) {
-    ///     // This uses the assumption `T: Clone` from the `where`-bounds
-    ///     // to prove `T: Clone`.
-    ///     (x.clone(), x)
-    /// }
-    /// ```
-    ParamEnv(usize),
-    /// If the self type is an alias type, e.g. an opaque type or a projection,
-    /// we know the bounds on that alias to hold even without knowing its concrete
-    /// underlying type.
-    ///
-    /// More precisely this candidate is using the `n-th` bound in the `item_bounds` of
-    /// the self type.
-    ///
-    /// ## Examples
-    ///
-    /// ```rust
-    /// trait Trait {
-    ///     type Assoc: Clone;
-    /// }
-    ///
-    /// fn foo<T: Trait>(x: <T as Trait>::Assoc) {
-    ///     // We prove `<T as Trait>::Assoc` by looking at the bounds on `Assoc` in
-    ///     // in the trait definition.
-    ///     let _y = x.clone();
-    /// }
-    /// ```
-    AliasBound,
-    /// A candidate that is registered only during coherence to represent some
-    /// yet-unknown impl that could be produced downstream without violating orphan
-    /// rules.
-    // FIXME: Merge this with the forced ambiguity candidates, so those don't use `Misc`.
-    CoherenceUnknowable,
-}
diff --git a/compiler/rustc_middle/src/traits/solve/cache.rs b/compiler/rustc_middle/src/traits/solve/cache.rs
index 4f90af0a27c..03ce7cf98cf 100644
--- a/compiler/rustc_middle/src/traits/solve/cache.rs
+++ b/compiler/rustc_middle/src/traits/solve/cache.rs
@@ -17,7 +17,7 @@ pub struct EvaluationCache<'tcx> {
 #[derive(PartialEq, Eq)]
 pub struct CacheData<'tcx> {
     pub result: QueryResult<'tcx>,
-    pub proof_tree: Option<&'tcx [inspect::GoalEvaluationStep<'tcx>]>,
+    pub proof_tree: Option<&'tcx [inspect::GoalEvaluationStep<TyCtxt<'tcx>>]>,
     pub reached_depth: usize,
     pub encountered_overflow: bool,
 }
@@ -28,7 +28,7 @@ impl<'tcx> EvaluationCache<'tcx> {
         &self,
         tcx: TyCtxt<'tcx>,
         key: CanonicalInput<'tcx>,
-        proof_tree: Option<&'tcx [inspect::GoalEvaluationStep<'tcx>]>,
+        proof_tree: Option<&'tcx [inspect::GoalEvaluationStep<TyCtxt<'tcx>>]>,
         reached_depth: usize,
         encountered_overflow: bool,
         cycle_participants: FxHashSet<CanonicalInput<'tcx>>,
@@ -105,7 +105,7 @@ struct Success<'tcx> {
 #[derive(Clone, Copy)]
 pub struct QueryData<'tcx> {
     pub result: QueryResult<'tcx>,
-    pub proof_tree: Option<&'tcx [inspect::GoalEvaluationStep<'tcx>]>,
+    pub proof_tree: Option<&'tcx [inspect::GoalEvaluationStep<TyCtxt<'tcx>>]>,
 }
 
 /// The cache entry for a goal `CanonicalInput`.
diff --git a/compiler/rustc_middle/src/traits/solve/inspect.rs b/compiler/rustc_middle/src/traits/solve/inspect.rs
deleted file mode 100644
index 9e944899026..00000000000
--- a/compiler/rustc_middle/src/traits/solve/inspect.rs
+++ /dev/null
@@ -1,160 +0,0 @@
-//! Data structure used to inspect trait solver behavior.
-//!
-//! During trait solving we optionally build "proof trees", the root of
-//! which is a [GoalEvaluation] with [GoalEvaluationKind::Root]. These
-//! trees are used to improve the debug experience and are also used by
-//! the compiler itself to provide necessary context for error messages.
-//!
-//! Because each nested goal in the solver gets [canonicalized] separately
-//! and we discard inference progress via "probes", we cannot mechanically
-//! use proof trees without somehow "lifting up" data local to the current
-//! `InferCtxt`. Any data used mechanically is therefore canonicalized and
-//! stored as [CanonicalState]. As printing canonicalized data worsens the
-//! debugging dumps, we do not simply canonicalize everything.
-//!
-//! This means proof trees contain inference variables and placeholders
-//! local to a different `InferCtxt` which must not be used with the
-//! current one.
-//!
-//! [canonicalized]: https://rustc-dev-guide.rust-lang.org/solve/canonicalization.html
-
-use super::{
-    CandidateSource, Canonical, CanonicalInput, Certainty, Goal, GoalSource, NoSolution,
-    QueryInput, QueryResult,
-};
-use crate::{infer::canonical::CanonicalVarValues, ty};
-use format::ProofTreeFormatter;
-use rustc_macros::{TypeFoldable, TypeVisitable};
-use std::fmt::{Debug, Write};
-
-mod format;
-
-/// Some `data` together with information about how they relate to the input
-/// of the canonical query.
-///
-/// This is only ever used as [CanonicalState]. Any type information in proof
-/// trees used mechanically has to be canonicalized as we otherwise leak
-/// inference variables from a nested `InferCtxt`.
-#[derive(Debug, Clone, Copy, Eq, PartialEq, TypeFoldable, TypeVisitable)]
-pub struct State<'tcx, T> {
-    pub var_values: CanonicalVarValues<'tcx>,
-    pub data: T,
-}
-
-pub type CanonicalState<'tcx, T> = Canonical<'tcx, State<'tcx, T>>;
-
-/// When evaluating the root goals we also store the
-/// original values for the `CanonicalVarValues` of the
-/// canonicalized goal. We use this to map any [CanonicalState]
-/// from the local `InferCtxt` of the solver query to
-/// the `InferCtxt` of the caller.
-#[derive(Eq, PartialEq)]
-pub enum GoalEvaluationKind<'tcx> {
-    Root { orig_values: Vec<ty::GenericArg<'tcx>> },
-    Nested,
-}
-
-#[derive(Eq, PartialEq)]
-pub struct GoalEvaluation<'tcx> {
-    pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
-    pub kind: GoalEvaluationKind<'tcx>,
-    pub evaluation: CanonicalGoalEvaluation<'tcx>,
-}
-
-#[derive(Eq, PartialEq, Debug)]
-pub struct CanonicalGoalEvaluation<'tcx> {
-    pub goal: CanonicalInput<'tcx>,
-    pub kind: CanonicalGoalEvaluationKind<'tcx>,
-    pub result: QueryResult<'tcx>,
-}
-
-#[derive(Eq, PartialEq, Debug)]
-pub enum CanonicalGoalEvaluationKind<'tcx> {
-    Overflow,
-    CycleInStack,
-    ProvisionalCacheHit,
-    Evaluation { revisions: &'tcx [GoalEvaluationStep<'tcx>] },
-}
-impl Debug for GoalEvaluation<'_> {
-    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        ProofTreeFormatter::new(f).format_goal_evaluation(self)
-    }
-}
-
-#[derive(Eq, PartialEq)]
-pub struct AddedGoalsEvaluation<'tcx> {
-    pub evaluations: Vec<Vec<GoalEvaluation<'tcx>>>,
-    pub result: Result<Certainty, NoSolution>,
-}
-
-#[derive(Eq, PartialEq, Debug)]
-pub struct GoalEvaluationStep<'tcx> {
-    pub instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
-
-    /// The actual evaluation of the goal, always `ProbeKind::Root`.
-    pub evaluation: Probe<'tcx>,
-}
-
-/// A self-contained computation during trait solving. This either
-/// corresponds to a `EvalCtxt::probe(_X)` call or the root evaluation
-/// of a goal.
-#[derive(Eq, PartialEq)]
-pub struct Probe<'tcx> {
-    /// What happened inside of this probe in chronological order.
-    pub steps: Vec<ProbeStep<'tcx>>,
-    pub kind: ProbeKind<'tcx>,
-    pub final_state: CanonicalState<'tcx, ()>,
-}
-
-impl Debug for Probe<'_> {
-    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        ProofTreeFormatter::new(f).format_probe(self)
-    }
-}
-
-#[derive(Eq, PartialEq)]
-pub enum ProbeStep<'tcx> {
-    /// We added a goal to the `EvalCtxt` which will get proven
-    /// the next time `EvalCtxt::try_evaluate_added_goals` is called.
-    AddGoal(GoalSource, CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>),
-    /// The inside of a `EvalCtxt::try_evaluate_added_goals` call.
-    EvaluateGoals(AddedGoalsEvaluation<'tcx>),
-    /// A call to `probe` while proving the current goal. This is
-    /// used whenever there are multiple candidates to prove the
-    /// current goalby .
-    NestedProbe(Probe<'tcx>),
-    /// A trait goal was satisfied by an impl candidate.
-    RecordImplArgs { impl_args: CanonicalState<'tcx, ty::GenericArgsRef<'tcx>> },
-    /// A call to `EvalCtxt::evaluate_added_goals_make_canonical_response` with
-    /// `Certainty` was made. This is the certainty passed in, so it's not unified
-    /// with the certainty of the `try_evaluate_added_goals` that is done within;
-    /// if it's `Certainty::Yes`, then we can trust that the candidate is "finished"
-    /// and we didn't force ambiguity for some reason.
-    MakeCanonicalResponse { shallow_certainty: Certainty },
-}
-
-/// What kind of probe we're in. In case the probe represents a candidate, or
-/// the final result of the current goal - via [ProbeKind::Root] - we also
-/// store the [QueryResult].
-#[derive(Debug, PartialEq, Eq, Clone, Copy)]
-pub enum ProbeKind<'tcx> {
-    /// The root inference context while proving a goal.
-    Root { result: QueryResult<'tcx> },
-    /// Trying to normalize an alias by at least one step in `NormalizesTo`.
-    TryNormalizeNonRigid { result: QueryResult<'tcx> },
-    /// Probe entered when normalizing the self ty during candidate assembly
-    NormalizedSelfTyAssembly,
-    /// A candidate for proving a trait or alias-relate goal.
-    TraitCandidate { source: CandidateSource, result: QueryResult<'tcx> },
-    /// Used in the probe that wraps normalizing the non-self type for the unsize
-    /// trait, which is also structurally matched on.
-    UnsizeAssembly,
-    /// During upcasting from some source object to target object type, used to
-    /// do a probe to find out what projection type(s) may be used to prove that
-    /// the source type upholds all of the target type's object bounds.
-    UpcastProjectionCompatibility,
-    /// Looking for param-env candidates that satisfy the trait ref for a projection.
-    ShadowedEnvProbing,
-    /// Try to unify an opaque type with an existing key in the storage.
-    OpaqueTypeStorageLookup { result: QueryResult<'tcx> },
-}
diff --git a/compiler/rustc_middle/src/traits/solve/inspect/format.rs b/compiler/rustc_middle/src/traits/solve/inspect/format.rs
deleted file mode 100644
index 5b3c50cb973..00000000000
--- a/compiler/rustc_middle/src/traits/solve/inspect/format.rs
+++ /dev/null
@@ -1,169 +0,0 @@
-use super::*;
-
-pub(super) struct ProofTreeFormatter<'a, 'b> {
-    f: &'a mut (dyn Write + 'b),
-}
-
-enum IndentorState {
-    StartWithNewline,
-    OnNewline,
-    Inline,
-}
-
-/// A formatter which adds 4 spaces of indentation to its input before
-/// passing it on to its nested formatter.
-///
-/// We can use this for arbitrary levels of indentation by nesting it.
-struct Indentor<'a, 'b> {
-    f: &'a mut (dyn Write + 'b),
-    state: IndentorState,
-}
-
-impl Write for Indentor<'_, '_> {
-    fn write_str(&mut self, s: &str) -> std::fmt::Result {
-        for line in s.split_inclusive('\n') {
-            match self.state {
-                IndentorState::StartWithNewline => self.f.write_str("\n    ")?,
-                IndentorState::OnNewline => self.f.write_str("    ")?,
-                IndentorState::Inline => {}
-            }
-            self.state =
-                if line.ends_with('\n') { IndentorState::OnNewline } else { IndentorState::Inline };
-            self.f.write_str(line)?;
-        }
-
-        Ok(())
-    }
-}
-
-impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
-    pub(super) fn new(f: &'a mut (dyn Write + 'b)) -> Self {
-        ProofTreeFormatter { f }
-    }
-
-    fn nested<F>(&mut self, func: F) -> std::fmt::Result
-    where
-        F: FnOnce(&mut ProofTreeFormatter<'_, '_>) -> std::fmt::Result,
-    {
-        write!(self.f, " {{")?;
-        func(&mut ProofTreeFormatter {
-            f: &mut Indentor { f: self.f, state: IndentorState::StartWithNewline },
-        })?;
-        writeln!(self.f, "}}")
-    }
-
-    pub(super) fn format_goal_evaluation(&mut self, eval: &GoalEvaluation<'_>) -> std::fmt::Result {
-        let goal_text = match eval.kind {
-            GoalEvaluationKind::Root { orig_values: _ } => "ROOT GOAL",
-            GoalEvaluationKind::Nested => "GOAL",
-        };
-        write!(self.f, "{}: {:?}", goal_text, eval.uncanonicalized_goal)?;
-        self.nested(|this| this.format_canonical_goal_evaluation(&eval.evaluation))
-    }
-
-    pub(super) fn format_canonical_goal_evaluation(
-        &mut self,
-        eval: &CanonicalGoalEvaluation<'_>,
-    ) -> std::fmt::Result {
-        writeln!(self.f, "GOAL: {:?}", eval.goal)?;
-
-        match &eval.kind {
-            CanonicalGoalEvaluationKind::Overflow => {
-                writeln!(self.f, "OVERFLOW: {:?}", eval.result)
-            }
-            CanonicalGoalEvaluationKind::CycleInStack => {
-                writeln!(self.f, "CYCLE IN STACK: {:?}", eval.result)
-            }
-            CanonicalGoalEvaluationKind::ProvisionalCacheHit => {
-                writeln!(self.f, "PROVISIONAL CACHE HIT: {:?}", eval.result)
-            }
-            CanonicalGoalEvaluationKind::Evaluation { revisions } => {
-                for (n, step) in revisions.iter().enumerate() {
-                    write!(self.f, "REVISION {n}")?;
-                    self.nested(|this| this.format_evaluation_step(step))?;
-                }
-                writeln!(self.f, "RESULT: {:?}", eval.result)
-            }
-        }
-    }
-
-    pub(super) fn format_evaluation_step(
-        &mut self,
-        evaluation_step: &GoalEvaluationStep<'_>,
-    ) -> std::fmt::Result {
-        writeln!(self.f, "INSTANTIATED: {:?}", evaluation_step.instantiated_goal)?;
-        self.format_probe(&evaluation_step.evaluation)
-    }
-
-    pub(super) fn format_probe(&mut self, probe: &Probe<'_>) -> std::fmt::Result {
-        match &probe.kind {
-            ProbeKind::Root { result } => {
-                write!(self.f, "ROOT RESULT: {result:?}")
-            }
-            ProbeKind::TryNormalizeNonRigid { result } => {
-                write!(self.f, "TRY NORMALIZE NON-RIGID: {result:?}")
-            }
-            ProbeKind::NormalizedSelfTyAssembly => {
-                write!(self.f, "NORMALIZING SELF TY FOR ASSEMBLY:")
-            }
-            ProbeKind::UnsizeAssembly => {
-                write!(self.f, "ASSEMBLING CANDIDATES FOR UNSIZING:")
-            }
-            ProbeKind::UpcastProjectionCompatibility => {
-                write!(self.f, "PROBING FOR PROJECTION COMPATIBILITY FOR UPCASTING:")
-            }
-            ProbeKind::OpaqueTypeStorageLookup { result } => {
-                write!(self.f, "PROBING FOR AN EXISTING OPAQUE: {result:?}")
-            }
-            ProbeKind::TraitCandidate { source, result } => {
-                write!(self.f, "CANDIDATE {source:?}: {result:?}")
-            }
-            ProbeKind::ShadowedEnvProbing => {
-                write!(self.f, "PROBING FOR IMPLS SHADOWED BY PARAM-ENV CANDIDATE:")
-            }
-        }?;
-
-        self.nested(|this| {
-            for step in &probe.steps {
-                match step {
-                    ProbeStep::AddGoal(source, goal) => {
-                        let source = match source {
-                            GoalSource::Misc => "misc",
-                            GoalSource::ImplWhereBound => "impl where-bound",
-                            GoalSource::InstantiateHigherRanked => "higher-ranked goal",
-                        };
-                        writeln!(this.f, "ADDED GOAL ({source}): {goal:?}")?
-                    }
-                    ProbeStep::EvaluateGoals(eval) => this.format_added_goals_evaluation(eval)?,
-                    ProbeStep::NestedProbe(probe) => this.format_probe(probe)?,
-                    ProbeStep::MakeCanonicalResponse { shallow_certainty } => {
-                        writeln!(this.f, "EVALUATE GOALS AND MAKE RESPONSE: {shallow_certainty:?}")?
-                    }
-                    ProbeStep::RecordImplArgs { impl_args } => {
-                        writeln!(this.f, "RECORDED IMPL ARGS: {impl_args:?}")?
-                    }
-                }
-            }
-            Ok(())
-        })
-    }
-
-    pub(super) fn format_added_goals_evaluation(
-        &mut self,
-        added_goals_evaluation: &AddedGoalsEvaluation<'_>,
-    ) -> std::fmt::Result {
-        writeln!(self.f, "TRY_EVALUATE_ADDED_GOALS: {:?}", added_goals_evaluation.result)?;
-
-        for (n, iterations) in added_goals_evaluation.evaluations.iter().enumerate() {
-            write!(self.f, "ITERATION {n}")?;
-            self.nested(|this| {
-                for goal_evaluation in iterations {
-                    this.format_goal_evaluation(goal_evaluation)?;
-                }
-                Ok(())
-            })?;
-        }
-
-        Ok(())
-    }
-}
diff --git a/compiler/rustc_middle/src/ty/context.rs b/compiler/rustc_middle/src/ty/context.rs
index 1d3bc8b4bbe..b913577ad88 100644
--- a/compiler/rustc_middle/src/ty/context.rs
+++ b/compiler/rustc_middle/src/ty/context.rs
@@ -89,19 +89,23 @@ use std::ops::{Bound, Deref};
 #[allow(rustc::usage_of_ty_tykind)]
 impl<'tcx> Interner for TyCtxt<'tcx> {
     type DefId = DefId;
-    type DefiningOpaqueTypes = &'tcx ty::List<LocalDefId>;
-    type PredefinedOpaques = solve::PredefinedOpaques<'tcx>;
     type AdtDef = ty::AdtDef<'tcx>;
+
     type GenericArgs = ty::GenericArgsRef<'tcx>;
     type OwnItemArgs = &'tcx [ty::GenericArg<'tcx>];
     type GenericArg = ty::GenericArg<'tcx>;
-
     type Term = ty::Term<'tcx>;
+
     type Binder<T: TypeVisitable<TyCtxt<'tcx>>> = Binder<'tcx, T>;
     type BoundVars = &'tcx List<ty::BoundVariableKind>;
     type BoundVar = ty::BoundVariableKind;
 
     type CanonicalVars = CanonicalVarInfos<'tcx>;
+    type PredefinedOpaques = solve::PredefinedOpaques<'tcx>;
+    type DefiningOpaqueTypes = &'tcx ty::List<LocalDefId>;
+    type ExternalConstraints = ExternalConstraints<'tcx>;
+    type GoalEvaluationSteps = &'tcx [solve::inspect::GoalEvaluationStep<TyCtxt<'tcx>>];
+
     type Ty = Ty<'tcx>;
     type Tys = &'tcx List<Ty<'tcx>>;
     type FnInputTys = &'tcx [Ty<'tcx>];