about summary refs log tree commit diff
path: root/compiler
diff options
context:
space:
mode:
authorMichael Goulet <michael@errs.io>2024-05-17 12:16:36 -0400
committerMichael Goulet <michael@errs.io>2024-05-18 16:21:43 -0400
commit0f528a4c08bbff98a4fa4d2dc20b23822e1a2dee (patch)
tree9ff5454643bd617659c74f79d03a3d7507166690 /compiler
parent05e0f8740aacd7de77d515598da1f21a5c67866e (diff)
downloadrust-0f528a4c08bbff98a4fa4d2dc20b23822e1a2dee.tar.gz
rust-0f528a4c08bbff98a4fa4d2dc20b23822e1a2dee.zip
Uplift inspect into rustc_type_ir
Diffstat (limited to 'compiler')
-rw-r--r--compiler/rustc_middle/src/arena.rs2
-rw-r--r--compiler/rustc_middle/src/traits/mod.rs29
-rw-r--r--compiler/rustc_middle/src/traits/query.rs5
-rw-r--r--compiler/rustc_middle/src/traits/solve.rs161
-rw-r--r--compiler/rustc_middle/src/traits/solve/cache.rs6
-rw-r--r--compiler/rustc_middle/src/ty/context.rs10
-rw-r--r--compiler/rustc_trait_selection/src/solve/assembly/mod.rs8
-rw-r--r--compiler/rustc_trait_selection/src/solve/eval_ctxt/canonical.rs8
-rw-r--r--compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs5
-rw-r--r--compiler/rustc_trait_selection/src/solve/eval_ctxt/probe.rs33
-rw-r--r--compiler/rustc_trait_selection/src/solve/fulfill.rs27
-rw-r--r--compiler/rustc_trait_selection/src/solve/inspect/analyse.rs21
-rw-r--r--compiler/rustc_trait_selection/src/solve/inspect/build.rs28
-rw-r--r--compiler/rustc_trait_selection/src/solve/mod.rs2
-rw-r--r--compiler/rustc_trait_selection/src/solve/normalizes_to/mod.rs2
-rw-r--r--compiler/rustc_trait_selection/src/solve/trait_goals.rs6
-rw-r--r--compiler/rustc_type_ir/src/interner.rs5
-rw-r--r--compiler/rustc_type_ir/src/solve.rs200
-rw-r--r--compiler/rustc_type_ir/src/solve/inspect.rs (renamed from compiler/rustc_middle/src/traits/solve/inspect.rs)137
-rw-r--r--compiler/rustc_type_ir/src/solve/inspect/format.rs (renamed from compiler/rustc_middle/src/traits/solve/inspect/format.rs)22
20 files changed, 399 insertions, 318 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/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>];
diff --git a/compiler/rustc_trait_selection/src/solve/assembly/mod.rs b/compiler/rustc_trait_selection/src/solve/assembly/mod.rs
index 4074ecdd74e..b1dd6ae6611 100644
--- a/compiler/rustc_trait_selection/src/solve/assembly/mod.rs
+++ b/compiler/rustc_trait_selection/src/solve/assembly/mod.rs
@@ -25,7 +25,7 @@ pub(super) mod structural_traits;
 /// and the `result` when using the given `source`.
 #[derive(Debug, Clone)]
 pub(super) struct Candidate<'tcx> {
-    pub(super) source: CandidateSource,
+    pub(super) source: CandidateSource<'tcx>,
     pub(super) result: CanonicalResponse<'tcx>,
 }
 
@@ -47,7 +47,7 @@ pub(super) trait GoalKind<'tcx>:
     /// [`EvalCtxt::evaluate_added_goals_and_make_canonical_response`]).
     fn probe_and_match_goal_against_assumption(
         ecx: &mut EvalCtxt<'_, 'tcx>,
-        source: CandidateSource,
+        source: CandidateSource<'tcx>,
         goal: Goal<'tcx, Self>,
         assumption: ty::Clause<'tcx>,
         then: impl FnOnce(&mut EvalCtxt<'_, 'tcx>) -> QueryResult<'tcx>,
@@ -58,7 +58,7 @@ pub(super) trait GoalKind<'tcx>:
     /// goal by equating it with the assumption.
     fn probe_and_consider_implied_clause(
         ecx: &mut EvalCtxt<'_, 'tcx>,
-        parent_source: CandidateSource,
+        parent_source: CandidateSource<'tcx>,
         goal: Goal<'tcx, Self>,
         assumption: ty::Clause<'tcx>,
         requirements: impl IntoIterator<Item = (GoalSource, Goal<'tcx, ty::Predicate<'tcx>>)>,
@@ -76,7 +76,7 @@ pub(super) trait GoalKind<'tcx>:
     /// since they're not implied by the well-formedness of the object type.
     fn probe_and_consider_object_bound_candidate(
         ecx: &mut EvalCtxt<'_, 'tcx>,
-        source: CandidateSource,
+        source: CandidateSource<'tcx>,
         goal: Goal<'tcx, Self>,
         assumption: ty::Clause<'tcx>,
     ) -> Result<Candidate<'tcx>, NoSolution> {
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 2058650f288..52deb22098f 100644
--- a/compiler/rustc_trait_selection/src/solve/eval_ctxt/canonical.rs
+++ b/compiler/rustc_trait_selection/src/solve/eval_ctxt/canonical.rs
@@ -40,13 +40,13 @@ trait ResponseT<'tcx> {
     fn var_values(&self) -> CanonicalVarValues<'tcx>;
 }
 
-impl<'tcx> ResponseT<'tcx> for Response<'tcx> {
+impl<'tcx> ResponseT<'tcx> for Response<TyCtxt<'tcx>> {
     fn var_values(&self) -> CanonicalVarValues<'tcx> {
         self.var_values
     }
 }
 
-impl<'tcx, T> ResponseT<'tcx> for inspect::State<'tcx, T> {
+impl<'tcx, T> ResponseT<'tcx> for inspect::State<TyCtxt<'tcx>, T> {
     fn var_values(&self) -> CanonicalVarValues<'tcx> {
         self.var_values
     }
@@ -384,7 +384,7 @@ pub(in crate::solve) fn make_canonical_state<'tcx, T: TypeFoldable<TyCtxt<'tcx>>
     var_values: &[ty::GenericArg<'tcx>],
     max_input_universe: ty::UniverseIndex,
     data: T,
-) -> inspect::CanonicalState<'tcx, T> {
+) -> inspect::CanonicalState<TyCtxt<'tcx>, T> {
     let var_values = CanonicalVarValues { var_values: infcx.tcx.mk_args(var_values) };
     let state = inspect::State { var_values, data };
     let state = state.fold_with(&mut EagerResolver::new(infcx));
@@ -414,7 +414,7 @@ pub(in crate::solve) fn instantiate_canonical_state<'tcx, T: TypeFoldable<TyCtxt
     span: Span,
     param_env: ty::ParamEnv<'tcx>,
     orig_values: &mut Vec<ty::GenericArg<'tcx>>,
-    state: inspect::CanonicalState<'tcx, T>,
+    state: inspect::CanonicalState<TyCtxt<'tcx>, T>,
 ) -> T {
     // In case any fresh inference variables have been created between `state`
     // and the previous instantiation, extend `orig_values` for it.
diff --git a/compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs b/compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs
index dfb2bfc1b58..7ca15c1dd59 100644
--- a/compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs
+++ b/compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs
@@ -147,7 +147,8 @@ impl<'tcx> InferCtxt<'tcx> {
         &self,
         goal: Goal<'tcx, ty::Predicate<'tcx>>,
         generate_proof_tree: GenerateProofTree,
-    ) -> (Result<(bool, Certainty), NoSolution>, Option<inspect::GoalEvaluation<'tcx>>) {
+    ) -> (Result<(bool, Certainty), NoSolution>, Option<inspect::GoalEvaluation<TyCtxt<'tcx>>>)
+    {
         EvalCtxt::enter_root(self, generate_proof_tree, |ecx| {
             ecx.evaluate_goal(GoalEvaluationKind::Root, GoalSource::Misc, goal)
         })
@@ -170,7 +171,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
         infcx: &InferCtxt<'tcx>,
         generate_proof_tree: GenerateProofTree,
         f: impl FnOnce(&mut EvalCtxt<'_, 'tcx>) -> R,
-    ) -> (R, Option<inspect::GoalEvaluation<'tcx>>) {
+    ) -> (R, Option<inspect::GoalEvaluation<TyCtxt<'tcx>>>) {
         let mode = if infcx.intercrate { SolverMode::Coherence } else { SolverMode::Normal };
         let mut search_graph = search_graph::SearchGraph::new(mode);
 
diff --git a/compiler/rustc_trait_selection/src/solve/eval_ctxt/probe.rs b/compiler/rustc_trait_selection/src/solve/eval_ctxt/probe.rs
index 47109c8ad5d..9edc489754c 100644
--- a/compiler/rustc_trait_selection/src/solve/eval_ctxt/probe.rs
+++ b/compiler/rustc_trait_selection/src/solve/eval_ctxt/probe.rs
@@ -2,10 +2,9 @@ use crate::solve::assembly::Candidate;
 
 use super::EvalCtxt;
 use rustc_infer::traits::BuiltinImplSource;
-use rustc_middle::traits::{
-    query::NoSolution,
-    solve::{inspect, CandidateSource, QueryResult},
-};
+use rustc_middle::traits::query::NoSolution;
+use rustc_middle::traits::solve::{inspect, CandidateSource, QueryResult};
+use rustc_middle::ty::TyCtxt;
 use std::marker::PhantomData;
 
 pub(in crate::solve) struct ProbeCtxt<'me, 'a, 'tcx, F, T> {
@@ -16,7 +15,7 @@ pub(in crate::solve) struct ProbeCtxt<'me, 'a, 'tcx, F, T> {
 
 impl<'tcx, F, T> ProbeCtxt<'_, '_, 'tcx, F, T>
 where
-    F: FnOnce(&T) -> inspect::ProbeKind<'tcx>,
+    F: FnOnce(&T) -> inspect::ProbeKind<TyCtxt<'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;
@@ -51,12 +50,12 @@ where
 
 pub(in crate::solve) struct TraitProbeCtxt<'me, 'a, 'tcx, F> {
     cx: ProbeCtxt<'me, 'a, 'tcx, F, QueryResult<'tcx>>,
-    source: CandidateSource,
+    source: CandidateSource<'tcx>,
 }
 
 impl<'tcx, F> TraitProbeCtxt<'_, '_, 'tcx, F>
 where
-    F: FnOnce(&QueryResult<'tcx>) -> inspect::ProbeKind<'tcx>,
+    F: FnOnce(&QueryResult<'tcx>) -> inspect::ProbeKind<TyCtxt<'tcx>>,
 {
     #[instrument(level = "debug", skip_all, fields(source = ?self.source))]
     pub(in crate::solve) fn enter(
@@ -72,7 +71,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
     /// 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::ProbeKind<'tcx>,
+        F: FnOnce(&T) -> inspect::ProbeKind<TyCtxt<'tcx>>,
     {
         ProbeCtxt { ecx: self, probe_kind, _result: PhantomData }
     }
@@ -80,16 +79,24 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
     pub(in crate::solve) fn probe_builtin_trait_candidate(
         &mut self,
         source: BuiltinImplSource,
-    ) -> TraitProbeCtxt<'_, 'a, 'tcx, impl FnOnce(&QueryResult<'tcx>) -> inspect::ProbeKind<'tcx>>
-    {
+    ) -> TraitProbeCtxt<
+        '_,
+        'a,
+        'tcx,
+        impl FnOnce(&QueryResult<'tcx>) -> inspect::ProbeKind<TyCtxt<'tcx>>,
+    > {
         self.probe_trait_candidate(CandidateSource::BuiltinImpl(source))
     }
 
     pub(in crate::solve) fn probe_trait_candidate(
         &mut self,
-        source: CandidateSource,
-    ) -> TraitProbeCtxt<'_, 'a, 'tcx, impl FnOnce(&QueryResult<'tcx>) -> inspect::ProbeKind<'tcx>>
-    {
+        source: CandidateSource<'tcx>,
+    ) -> TraitProbeCtxt<
+        '_,
+        'a,
+        'tcx,
+        impl FnOnce(&QueryResult<'tcx>) -> inspect::ProbeKind<TyCtxt<'tcx>>,
+    > {
         TraitProbeCtxt {
             cx: ProbeCtxt {
                 ecx: self,
diff --git a/compiler/rustc_trait_selection/src/solve/fulfill.rs b/compiler/rustc_trait_selection/src/solve/fulfill.rs
index 625bcf33a16..4933080451d 100644
--- a/compiler/rustc_trait_selection/src/solve/fulfill.rs
+++ b/compiler/rustc_trait_selection/src/solve/fulfill.rs
@@ -3,7 +3,6 @@ use std::ops::ControlFlow;
 
 use rustc_infer::infer::InferCtxt;
 use rustc_infer::traits::query::NoSolution;
-use rustc_infer::traits::solve::inspect::ProbeKind;
 use rustc_infer::traits::solve::{CandidateSource, GoalSource, MaybeCause};
 use rustc_infer::traits::{
     self, FulfillmentError, FulfillmentErrorCode, MismatchedProjectionTypes, Obligation,
@@ -15,7 +14,7 @@ use rustc_middle::ty::{self, TyCtxt};
 use rustc_span::symbol::sym;
 
 use super::eval_ctxt::GenerateProofTree;
-use super::inspect::{InspectCandidate, InspectGoal, ProofTreeInferCtxtExt, ProofTreeVisitor};
+use super::inspect::{self, ProofTreeInferCtxtExt, ProofTreeVisitor};
 use super::{Certainty, InferCtxtEvalExt};
 
 /// A trait engine using the new trait solver.
@@ -319,8 +318,8 @@ impl<'tcx> BestObligation<'tcx> {
     /// *don't* hold and which have impl-where clauses that also don't hold.
     fn non_trivial_candidates<'a>(
         &self,
-        goal: &'a InspectGoal<'a, 'tcx>,
-    ) -> Vec<InspectCandidate<'a, 'tcx>> {
+        goal: &'a inspect::InspectGoal<'a, 'tcx>,
+    ) -> Vec<inspect::InspectCandidate<'a, 'tcx>> {
         let mut candidates = goal.candidates();
         match self.consider_ambiguities {
             true => {
@@ -370,15 +369,17 @@ impl<'tcx> ProofTreeVisitor<'tcx> for BestObligation<'tcx> {
         self.obligation.cause.span
     }
 
-    fn visit_goal(&mut self, goal: &super::inspect::InspectGoal<'_, 'tcx>) -> Self::Result {
+    fn visit_goal(&mut self, goal: &inspect::InspectGoal<'_, 'tcx>) -> Self::Result {
         let candidates = self.non_trivial_candidates(goal);
         let [candidate] = candidates.as_slice() else {
             return ControlFlow::Break(self.obligation.clone());
         };
 
         // Don't walk into impls that have `do_not_recommend`.
-        if let ProbeKind::TraitCandidate { source: CandidateSource::Impl(impl_def_id), result: _ } =
-            candidate.kind()
+        if let inspect::ProbeKind::TraitCandidate {
+            source: CandidateSource::Impl(impl_def_id),
+            result: _,
+        } = candidate.kind()
             && goal.infcx().tcx.has_attr(impl_def_id, sym::do_not_recommend)
         {
             return ControlFlow::Break(self.obligation.clone());
@@ -475,13 +476,16 @@ enum ChildMode<'tcx> {
 
 fn derive_cause<'tcx>(
     tcx: TyCtxt<'tcx>,
-    candidate_kind: ProbeKind<'tcx>,
+    candidate_kind: inspect::ProbeKind<TyCtxt<'tcx>>,
     mut cause: ObligationCause<'tcx>,
     idx: usize,
     parent_trait_pred: ty::PolyTraitPredicate<'tcx>,
 ) -> ObligationCause<'tcx> {
     match candidate_kind {
-        ProbeKind::TraitCandidate { source: CandidateSource::Impl(impl_def_id), result: _ } => {
+        inspect::ProbeKind::TraitCandidate {
+            source: CandidateSource::Impl(impl_def_id),
+            result: _,
+        } => {
             if let Some((_, span)) =
                 tcx.predicates_of(impl_def_id).instantiate_identity(tcx).iter().nth(idx)
             {
@@ -495,7 +499,10 @@ fn derive_cause<'tcx>(
                 })
             }
         }
-        ProbeKind::TraitCandidate { source: CandidateSource::BuiltinImpl(..), result: _ } => {
+        inspect::ProbeKind::TraitCandidate {
+            source: CandidateSource::BuiltinImpl(..),
+            result: _,
+        } => {
             cause = cause.derived_cause(parent_trait_pred, ObligationCauseCode::BuiltinDerived);
         }
         _ => {}
diff --git a/compiler/rustc_trait_selection/src/solve/inspect/analyse.rs b/compiler/rustc_trait_selection/src/solve/inspect/analyse.rs
index b71a1b339cb..e12c66b6928 100644
--- a/compiler/rustc_trait_selection/src/solve/inspect/analyse.rs
+++ b/compiler/rustc_trait_selection/src/solve/inspect/analyse.rs
@@ -18,7 +18,7 @@ use rustc_middle::traits::query::NoSolution;
 use rustc_middle::traits::solve::{inspect, QueryResult};
 use rustc_middle::traits::solve::{Certainty, Goal};
 use rustc_middle::traits::ObligationCause;
-use rustc_middle::ty::TypeFoldable;
+use rustc_middle::ty::{TyCtxt, TypeFoldable};
 use rustc_middle::{bug, ty};
 use rustc_span::{Span, DUMMY_SP};
 
@@ -37,7 +37,7 @@ pub struct InspectGoal<'a, 'tcx> {
     orig_values: Vec<ty::GenericArg<'tcx>>,
     goal: Goal<'tcx, ty::Predicate<'tcx>>,
     result: Result<Certainty, NoSolution>,
-    evaluation_kind: inspect::CanonicalGoalEvaluationKind<'tcx>,
+    evaluation_kind: inspect::CanonicalGoalEvaluationKind<TyCtxt<'tcx>>,
     normalizes_to_term_hack: Option<NormalizesToTermHack<'tcx>>,
     source: GoalSource,
 }
@@ -88,16 +88,17 @@ impl<'tcx> NormalizesToTermHack<'tcx> {
 
 pub struct InspectCandidate<'a, 'tcx> {
     goal: &'a InspectGoal<'a, 'tcx>,
-    kind: inspect::ProbeKind<'tcx>,
-    nested_goals: Vec<(GoalSource, inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>)>,
-    final_state: inspect::CanonicalState<'tcx, ()>,
-    impl_args: Option<inspect::CanonicalState<'tcx, ty::GenericArgsRef<'tcx>>>,
+    kind: inspect::ProbeKind<TyCtxt<'tcx>>,
+    nested_goals:
+        Vec<(GoalSource, inspect::CanonicalState<TyCtxt<'tcx>, Goal<'tcx, ty::Predicate<'tcx>>>)>,
+    final_state: inspect::CanonicalState<TyCtxt<'tcx>, ()>,
+    impl_args: Option<inspect::CanonicalState<TyCtxt<'tcx>, ty::GenericArgsRef<'tcx>>>,
     result: QueryResult<'tcx>,
     shallow_certainty: Certainty,
 }
 
 impl<'a, 'tcx> InspectCandidate<'a, 'tcx> {
-    pub fn kind(&self) -> inspect::ProbeKind<'tcx> {
+    pub fn kind(&self) -> inspect::ProbeKind<TyCtxt<'tcx>> {
         self.kind
     }
 
@@ -280,9 +281,9 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
         candidates: &mut Vec<InspectCandidate<'a, 'tcx>>,
         nested_goals: &mut Vec<(
             GoalSource,
-            inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>,
+            inspect::CanonicalState<TyCtxt<'tcx>, Goal<'tcx, ty::Predicate<'tcx>>>,
         )>,
-        probe: &inspect::Probe<'tcx>,
+        probe: &inspect::Probe<TyCtxt<'tcx>>,
     ) {
         let mut shallow_certainty = None;
         let mut impl_args = None;
@@ -387,7 +388,7 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
     fn new(
         infcx: &'a InferCtxt<'tcx>,
         depth: usize,
-        root: inspect::GoalEvaluation<'tcx>,
+        root: inspect::GoalEvaluation<TyCtxt<'tcx>>,
         normalizes_to_term_hack: Option<NormalizesToTermHack<'tcx>>,
         source: GoalSource,
     ) -> Self {
diff --git a/compiler/rustc_trait_selection/src/solve/inspect/build.rs b/compiler/rustc_trait_selection/src/solve/inspect/build.rs
index 9dd681f09e7..90caa2b3af1 100644
--- a/compiler/rustc_trait_selection/src/solve/inspect/build.rs
+++ b/compiler/rustc_trait_selection/src/solve/inspect/build.rs
@@ -80,7 +80,7 @@ struct WipGoalEvaluation<'tcx> {
 }
 
 impl<'tcx> WipGoalEvaluation<'tcx> {
-    fn finalize(self) -> inspect::GoalEvaluation<'tcx> {
+    fn finalize(self) -> inspect::GoalEvaluation<TyCtxt<'tcx>> {
         inspect::GoalEvaluation {
             uncanonicalized_goal: self.uncanonicalized_goal,
             kind: match self.kind {
@@ -105,7 +105,7 @@ pub(in crate::solve) enum WipCanonicalGoalEvaluationKind<'tcx> {
     Overflow,
     CycleInStack,
     ProvisionalCacheHit,
-    Interned { revisions: &'tcx [inspect::GoalEvaluationStep<'tcx>] },
+    Interned { revisions: &'tcx [inspect::GoalEvaluationStep<TyCtxt<'tcx>>] },
 }
 
 impl std::fmt::Debug for WipCanonicalGoalEvaluationKind<'_> {
@@ -130,7 +130,7 @@ struct WipCanonicalGoalEvaluation<'tcx> {
 }
 
 impl<'tcx> WipCanonicalGoalEvaluation<'tcx> {
-    fn finalize(self) -> inspect::CanonicalGoalEvaluation<'tcx> {
+    fn finalize(self) -> inspect::CanonicalGoalEvaluation<TyCtxt<'tcx>> {
         assert!(self.revisions.is_empty());
         let kind = match self.kind.unwrap() {
             WipCanonicalGoalEvaluationKind::Overflow => {
@@ -158,7 +158,7 @@ struct WipAddedGoalsEvaluation<'tcx> {
 }
 
 impl<'tcx> WipAddedGoalsEvaluation<'tcx> {
-    fn finalize(self) -> inspect::AddedGoalsEvaluation<'tcx> {
+    fn finalize(self) -> inspect::AddedGoalsEvaluation<TyCtxt<'tcx>> {
         inspect::AddedGoalsEvaluation {
             evaluations: self
                 .evaluations
@@ -209,7 +209,7 @@ impl<'tcx> WipGoalEvaluationStep<'tcx> {
         }
     }
 
-    fn finalize(self) -> inspect::GoalEvaluationStep<'tcx> {
+    fn finalize(self) -> inspect::GoalEvaluationStep<TyCtxt<'tcx>> {
         let evaluation = self.evaluation.finalize();
         match evaluation.kind {
             inspect::ProbeKind::Root { .. } => (),
@@ -223,12 +223,12 @@ impl<'tcx> WipGoalEvaluationStep<'tcx> {
 struct WipProbe<'tcx> {
     initial_num_var_values: usize,
     steps: Vec<WipProbeStep<'tcx>>,
-    kind: Option<inspect::ProbeKind<'tcx>>,
-    final_state: Option<inspect::CanonicalState<'tcx, ()>>,
+    kind: Option<inspect::ProbeKind<TyCtxt<'tcx>>>,
+    final_state: Option<inspect::CanonicalState<TyCtxt<'tcx>, ()>>,
 }
 
 impl<'tcx> WipProbe<'tcx> {
-    fn finalize(self) -> inspect::Probe<'tcx> {
+    fn finalize(self) -> inspect::Probe<TyCtxt<'tcx>> {
         inspect::Probe {
             steps: self.steps.into_iter().map(WipProbeStep::finalize).collect(),
             kind: self.kind.unwrap(),
@@ -239,15 +239,15 @@ impl<'tcx> WipProbe<'tcx> {
 
 #[derive(Eq, PartialEq, Debug)]
 enum WipProbeStep<'tcx> {
-    AddGoal(GoalSource, inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>),
+    AddGoal(GoalSource, inspect::CanonicalState<TyCtxt<'tcx>, Goal<'tcx, ty::Predicate<'tcx>>>),
     EvaluateGoals(WipAddedGoalsEvaluation<'tcx>),
     NestedProbe(WipProbe<'tcx>),
     MakeCanonicalResponse { shallow_certainty: Certainty },
-    RecordImplArgs { impl_args: inspect::CanonicalState<'tcx, ty::GenericArgsRef<'tcx>> },
+    RecordImplArgs { impl_args: inspect::CanonicalState<TyCtxt<'tcx>, ty::GenericArgsRef<'tcx>> },
 }
 
 impl<'tcx> WipProbeStep<'tcx> {
-    fn finalize(self) -> inspect::ProbeStep<'tcx> {
+    fn finalize(self) -> inspect::ProbeStep<TyCtxt<'tcx>> {
         match self {
             WipProbeStep::AddGoal(source, goal) => inspect::ProbeStep::AddGoal(source, goal),
             WipProbeStep::EvaluateGoals(eval) => inspect::ProbeStep::EvaluateGoals(eval.finalize()),
@@ -281,7 +281,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
         nested
     }
 
-    pub fn finalize(self) -> Option<inspect::GoalEvaluation<'tcx>> {
+    pub fn finalize(self) -> Option<inspect::GoalEvaluation<TyCtxt<'tcx>>> {
         match *self.state? {
             DebugSolver::GoalEvaluation(wip_goal_evaluation) => {
                 Some(wip_goal_evaluation.finalize())
@@ -356,7 +356,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
     pub fn finalize_evaluation(
         &mut self,
         tcx: TyCtxt<'tcx>,
-    ) -> Option<&'tcx [inspect::GoalEvaluationStep<'tcx>]> {
+    ) -> Option<&'tcx [inspect::GoalEvaluationStep<TyCtxt<'tcx>>]> {
         self.as_mut().map(|this| match this {
             DebugSolver::CanonicalGoalEvaluation(evaluation) => {
                 let revisions = mem::take(&mut evaluation.revisions)
@@ -474,7 +474,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
         }
     }
 
-    pub fn probe_kind(&mut self, probe_kind: inspect::ProbeKind<'tcx>) {
+    pub fn probe_kind(&mut self, probe_kind: inspect::ProbeKind<TyCtxt<'tcx>>) {
         match self.as_mut() {
             None => {}
             Some(DebugSolver::GoalEvaluationStep(state)) => {
diff --git a/compiler/rustc_trait_selection/src/solve/mod.rs b/compiler/rustc_trait_selection/src/solve/mod.rs
index 5a3c960d72d..b085d009d75 100644
--- a/compiler/rustc_trait_selection/src/solve/mod.rs
+++ b/compiler/rustc_trait_selection/src/solve/mod.rs
@@ -74,7 +74,7 @@ enum GoalEvaluationKind {
 }
 
 #[extension(trait CanonicalResponseExt)]
-impl<'tcx> Canonical<'tcx, Response<'tcx>> {
+impl<'tcx> Canonical<'tcx, Response<TyCtxt<'tcx>>> {
     fn has_no_inference_or_external_constraints(&self) -> bool {
         self.value.external_constraints.region_constraints.is_empty()
             && self.value.var_values.is_identity()
diff --git a/compiler/rustc_trait_selection/src/solve/normalizes_to/mod.rs b/compiler/rustc_trait_selection/src/solve/normalizes_to/mod.rs
index 7ab27374e7a..24baa2b5473 100644
--- a/compiler/rustc_trait_selection/src/solve/normalizes_to/mod.rs
+++ b/compiler/rustc_trait_selection/src/solve/normalizes_to/mod.rs
@@ -108,7 +108,7 @@ impl<'tcx> assembly::GoalKind<'tcx> for NormalizesTo<'tcx> {
 
     fn probe_and_match_goal_against_assumption(
         ecx: &mut EvalCtxt<'_, 'tcx>,
-        source: CandidateSource,
+        source: CandidateSource<'tcx>,
         goal: Goal<'tcx, Self>,
         assumption: ty::Clause<'tcx>,
         then: impl FnOnce(&mut EvalCtxt<'_, 'tcx>) -> QueryResult<'tcx>,
diff --git a/compiler/rustc_trait_selection/src/solve/trait_goals.rs b/compiler/rustc_trait_selection/src/solve/trait_goals.rs
index b46edb32f72..9139c75d399 100644
--- a/compiler/rustc_trait_selection/src/solve/trait_goals.rs
+++ b/compiler/rustc_trait_selection/src/solve/trait_goals.rs
@@ -103,7 +103,7 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
 
     fn probe_and_match_goal_against_assumption(
         ecx: &mut EvalCtxt<'_, 'tcx>,
-        source: CandidateSource,
+        source: CandidateSource<'tcx>,
         goal: Goal<'tcx, Self>,
         assumption: ty::Clause<'tcx>,
         then: impl FnOnce(&mut EvalCtxt<'_, 'tcx>) -> QueryResult<'tcx>,
@@ -821,7 +821,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
     fn consider_builtin_upcast_to_principal(
         &mut self,
         goal: Goal<'tcx, (Ty<'tcx>, Ty<'tcx>)>,
-        source: CandidateSource,
+        source: CandidateSource<'tcx>,
         a_data: &'tcx ty::List<ty::PolyExistentialPredicate<'tcx>>,
         a_region: ty::Region<'tcx>,
         b_data: &'tcx ty::List<ty::PolyExistentialPredicate<'tcx>>,
@@ -1149,7 +1149,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
     /// wrapped in one.
     fn probe_and_evaluate_goal_for_constituent_tys(
         &mut self,
-        source: CandidateSource,
+        source: CandidateSource<'tcx>,
         goal: Goal<'tcx, TraitPredicate<'tcx>>,
         constituent_tys: impl Fn(
             &EvalCtxt<'_, 'tcx>,
diff --git a/compiler/rustc_type_ir/src/interner.rs b/compiler/rustc_type_ir/src/interner.rs
index 69865602584..47ad62105f2 100644
--- a/compiler/rustc_type_ir/src/interner.rs
+++ b/compiler/rustc_type_ir/src/interner.rs
@@ -5,6 +5,7 @@ use std::ops::Deref;
 
 use crate::inherent::*;
 use crate::ir_print::IrPrint;
+use crate::solve::inspect::GoalEvaluationStep;
 use crate::visit::{Flags, TypeSuperVisitable, TypeVisitable};
 use crate::{
     AliasTerm, AliasTermKind, AliasTy, AliasTyKind, CanonicalVarInfo, CoercePredicate,
@@ -28,7 +29,6 @@ pub trait Interner:
     + IrPrint<FnSig<Self>>
 {
     type DefId: Copy + Debug + Hash + Eq;
-    type DefiningOpaqueTypes: Copy + Debug + Hash + Default + Eq + TypeVisitable<Self>;
     type AdtDef: Copy + Debug + Hash + Eq;
 
     type GenericArgs: GenericArgs<Self>;
@@ -44,6 +44,9 @@ pub trait Interner:
 
     type CanonicalVars: Copy + Debug + Hash + Eq + IntoIterator<Item = CanonicalVarInfo<Self>>;
     type PredefinedOpaques: Copy + Debug + Hash + Eq;
+    type DefiningOpaqueTypes: Copy + Debug + Hash + Default + Eq + TypeVisitable<Self>;
+    type ExternalConstraints: Copy + Debug + Hash + Eq;
+    type GoalEvaluationSteps: Copy + Debug + Hash + Eq + Deref<Target = [GoalEvaluationStep<Self>]>;
 
     // Kinds of tys
     type Ty: Ty<Self>;
diff --git a/compiler/rustc_type_ir/src/solve.rs b/compiler/rustc_type_ir/src/solve.rs
index 2a733dd02c2..ca8fedf8dad 100644
--- a/compiler/rustc_type_ir/src/solve.rs
+++ b/compiler/rustc_type_ir/src/solve.rs
@@ -1,3 +1,5 @@
+pub mod inspect;
+
 use std::fmt;
 use std::hash::Hash;
 
@@ -5,7 +7,22 @@ use std::hash::Hash;
 use rustc_macros::{HashStable_NoContext, TyDecodable, TyEncodable};
 use rustc_type_ir_macros::{Lift_Generic, TypeFoldable_Generic, TypeVisitable_Generic};
 
-use crate::{Interner, NormalizesTo, Upcast};
+use crate::{Canonical, CanonicalVarValues, Interner, NormalizesTo, Upcast};
+
+pub type CanonicalInput<I, T = <I as Interner>::Predicate> = Canonical<I, QueryInput<I, T>>;
+pub type CanonicalResponse<I> = Canonical<I, Response<I>>;
+/// 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<I> = Result<CanonicalResponse<I>, NoSolution>;
+
+#[derive(Copy, Clone, Debug, Hash, PartialEq, Eq)]
+#[derive(TypeFoldable_Generic, TypeVisitable_Generic)]
+#[cfg_attr(feature = "nightly", derive(HashStable_NoContext))]
+pub struct NoSolution;
 
 /// A goal is a statement, i.e. `predicate`, we want to prove
 /// given some assumptions, i.e. `param_env`.
@@ -78,3 +95,184 @@ pub struct QueryInput<I: Interner, P> {
     pub goal: Goal<I, P>,
     pub predefined_opaques_in_body: I::PredefinedOpaques,
 }
+
+/// Possible ways the given goal can be proven.
+#[derive(derivative::Derivative)]
+#[derivative(
+    Clone(bound = ""),
+    Copy(bound = ""),
+    Hash(bound = ""),
+    PartialEq(bound = ""),
+    Eq(bound = ""),
+    Debug(bound = "")
+)]
+pub enum CandidateSource<I: Interner> {
+    /// 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(I::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,
+}
+
+#[derive(Clone, Copy, Hash, PartialEq, Eq, Debug)]
+#[derive(TypeVisitable_Generic, TypeFoldable_Generic)]
+#[cfg_attr(feature = "nightly", derive(HashStable_NoContext, TyEncodable, TyDecodable))]
+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,
+}
+
+#[derive(derivative::Derivative)]
+#[derivative(
+    Clone(bound = ""),
+    Copy(bound = ""),
+    Hash(bound = ""),
+    PartialEq(bound = ""),
+    Eq(bound = ""),
+    Debug(bound = "")
+)]
+#[derive(TypeVisitable_Generic, TypeFoldable_Generic)]
+#[cfg_attr(feature = "nightly", derive(HashStable_NoContext))]
+pub struct Response<I: Interner> {
+    pub certainty: Certainty,
+    pub var_values: CanonicalVarValues<I>,
+    /// Additional constraints returned by this query.
+    pub external_constraints: I::ExternalConstraints,
+}
+
+#[derive(Clone, Copy, Hash, PartialEq, Eq, Debug)]
+#[derive(TypeVisitable_Generic, TypeFoldable_Generic)]
+#[cfg_attr(feature = "nightly", derive(HashStable_NoContext))]
+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(Clone, Copy, Hash, PartialEq, Eq, Debug)]
+#[derive(TypeVisitable_Generic, TypeFoldable_Generic)]
+#[cfg_attr(feature = "nightly", derive(HashStable_NoContext))]
+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 },
+        }
+    }
+}
diff --git a/compiler/rustc_middle/src/traits/solve/inspect.rs b/compiler/rustc_type_ir/src/solve/inspect.rs
index 9e944899026..c4f6ee2669b 100644
--- a/compiler/rustc_middle/src/traits/solve/inspect.rs
+++ b/compiler/rustc_type_ir/src/solve/inspect.rs
@@ -18,16 +18,19 @@
 //!
 //! [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};
+mod format;
+
 use std::fmt::{Debug, Write};
+use std::hash::Hash;
 
-mod format;
+use rustc_type_ir_macros::{TypeFoldable_Generic, TypeVisitable_Generic};
+
+use self::format::ProofTreeFormatter;
+use crate::solve::{
+    CandidateSource, CanonicalInput, Certainty, Goal, GoalSource, NoSolution, QueryInput,
+    QueryResult,
+};
+use crate::{Canonical, CanonicalVarValues, Interner};
 
 /// Some `data` together with information about how they relate to the input
 /// of the canonical query.
@@ -35,96 +38,113 @@ mod format;
 /// 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>,
+#[derive(derivative::Derivative)]
+#[derivative(
+    Clone(bound = "T: Clone"),
+    Copy(bound = "T: Copy"),
+    PartialEq(bound = "T: PartialEq"),
+    Eq(bound = "T: Eq"),
+    Hash(bound = "T: Hash"),
+    Debug(bound = "T: Debug")
+)]
+#[derive(TypeVisitable_Generic, TypeFoldable_Generic)]
+pub struct State<I: Interner, T> {
+    pub var_values: CanonicalVarValues<I>,
     pub data: T,
 }
 
-pub type CanonicalState<'tcx, T> = Canonical<'tcx, State<'tcx, T>>;
+pub type CanonicalState<I, T> = Canonical<I, State<I, 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>> },
+#[derive(derivative::Derivative)]
+#[derivative(PartialEq(bound = ""), Eq(bound = ""), Hash(bound = ""), Debug(bound = ""))]
+pub enum GoalEvaluationKind<I: Interner> {
+    Root { orig_values: Vec<I::GenericArg> },
     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(derivative::Derivative)]
+#[derivative(PartialEq(bound = ""), Eq(bound = ""), Hash(bound = ""))]
+pub struct GoalEvaluation<I: Interner> {
+    pub uncanonicalized_goal: Goal<I, I::Predicate>,
+    pub kind: GoalEvaluationKind<I>,
+    pub evaluation: CanonicalGoalEvaluation<I>,
 }
 
-#[derive(Eq, PartialEq, Debug)]
-pub struct CanonicalGoalEvaluation<'tcx> {
-    pub goal: CanonicalInput<'tcx>,
-    pub kind: CanonicalGoalEvaluationKind<'tcx>,
-    pub result: QueryResult<'tcx>,
+#[derive(derivative::Derivative)]
+#[derivative(PartialEq(bound = ""), Eq(bound = ""), Hash(bound = ""), Debug(bound = ""))]
+pub struct CanonicalGoalEvaluation<I: Interner> {
+    pub goal: CanonicalInput<I>,
+    pub kind: CanonicalGoalEvaluationKind<I>,
+    pub result: QueryResult<I>,
 }
 
-#[derive(Eq, PartialEq, Debug)]
-pub enum CanonicalGoalEvaluationKind<'tcx> {
+#[derive(derivative::Derivative)]
+#[derivative(PartialEq(bound = ""), Eq(bound = ""), Hash(bound = ""), Debug(bound = ""))]
+pub enum CanonicalGoalEvaluationKind<I: Interner> {
     Overflow,
     CycleInStack,
     ProvisionalCacheHit,
-    Evaluation { revisions: &'tcx [GoalEvaluationStep<'tcx>] },
+    Evaluation { revisions: I::GoalEvaluationSteps },
 }
-impl Debug for GoalEvaluation<'_> {
+impl<I: Interner> Debug for GoalEvaluation<I> {
     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>>>,
+#[derive(derivative::Derivative)]
+#[derivative(PartialEq(bound = ""), Eq(bound = ""), Hash(bound = ""), Debug(bound = ""))]
+pub struct AddedGoalsEvaluation<I: Interner> {
+    pub evaluations: Vec<Vec<GoalEvaluation<I>>>,
     pub result: Result<Certainty, NoSolution>,
 }
 
-#[derive(Eq, PartialEq, Debug)]
-pub struct GoalEvaluationStep<'tcx> {
-    pub instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
+#[derive(derivative::Derivative)]
+#[derivative(PartialEq(bound = ""), Eq(bound = ""), Hash(bound = ""), Debug(bound = ""))]
+pub struct GoalEvaluationStep<I: Interner> {
+    pub instantiated_goal: QueryInput<I, I::Predicate>,
 
     /// The actual evaluation of the goal, always `ProbeKind::Root`.
-    pub evaluation: Probe<'tcx>,
+    pub evaluation: Probe<I>,
 }
 
 /// 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> {
+#[derive(derivative::Derivative)]
+#[derivative(PartialEq(bound = ""), Eq(bound = ""), Hash(bound = ""))]
+pub struct Probe<I: Interner> {
     /// What happened inside of this probe in chronological order.
-    pub steps: Vec<ProbeStep<'tcx>>,
-    pub kind: ProbeKind<'tcx>,
-    pub final_state: CanonicalState<'tcx, ()>,
+    pub steps: Vec<ProbeStep<I>>,
+    pub kind: ProbeKind<I>,
+    pub final_state: CanonicalState<I, ()>,
 }
 
-impl Debug for Probe<'_> {
+impl<I: Interner> Debug for Probe<I> {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         ProofTreeFormatter::new(f).format_probe(self)
     }
 }
 
-#[derive(Eq, PartialEq)]
-pub enum ProbeStep<'tcx> {
+#[derive(derivative::Derivative)]
+#[derivative(PartialEq(bound = ""), Eq(bound = ""), Hash(bound = ""), Debug(bound = ""))]
+pub enum ProbeStep<I: Interner> {
     /// 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>>>),
+    AddGoal(GoalSource, CanonicalState<I, Goal<I, I::Predicate>>),
     /// The inside of a `EvalCtxt::try_evaluate_added_goals` call.
-    EvaluateGoals(AddedGoalsEvaluation<'tcx>),
+    EvaluateGoals(AddedGoalsEvaluation<I>),
     /// 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>),
+    NestedProbe(Probe<I>),
     /// A trait goal was satisfied by an impl candidate.
-    RecordImplArgs { impl_args: CanonicalState<'tcx, ty::GenericArgsRef<'tcx>> },
+    RecordImplArgs { impl_args: CanonicalState<I, I::GenericArgs> },
     /// 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;
@@ -136,16 +156,25 @@ pub enum ProbeStep<'tcx> {
 /// 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> {
+#[derive(derivative::Derivative)]
+#[derivative(
+    Clone(bound = ""),
+    Copy(bound = ""),
+    PartialEq(bound = ""),
+    Eq(bound = ""),
+    Hash(bound = ""),
+    Debug(bound = "")
+)]
+#[derive(TypeVisitable_Generic, TypeFoldable_Generic)]
+pub enum ProbeKind<I: Interner> {
     /// The root inference context while proving a goal.
-    Root { result: QueryResult<'tcx> },
+    Root { result: QueryResult<I> },
     /// Trying to normalize an alias by at least one step in `NormalizesTo`.
-    TryNormalizeNonRigid { result: QueryResult<'tcx> },
+    TryNormalizeNonRigid { result: QueryResult<I> },
     /// 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> },
+    TraitCandidate { source: CandidateSource<I>, result: QueryResult<I> },
     /// Used in the probe that wraps normalizing the non-self type for the unsize
     /// trait, which is also structurally matched on.
     UnsizeAssembly,
@@ -156,5 +185,5 @@ pub enum ProbeKind<'tcx> {
     /// 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> },
+    OpaqueTypeStorageLookup { result: QueryResult<I> },
 }
diff --git a/compiler/rustc_middle/src/traits/solve/inspect/format.rs b/compiler/rustc_type_ir/src/solve/inspect/format.rs
index 5b3c50cb973..44ade04cf98 100644
--- a/compiler/rustc_middle/src/traits/solve/inspect/format.rs
+++ b/compiler/rustc_type_ir/src/solve/inspect/format.rs
@@ -1,7 +1,10 @@
+use std::marker::PhantomData;
+
 use super::*;
 
-pub(super) struct ProofTreeFormatter<'a, 'b> {
+pub(super) struct ProofTreeFormatter<'a, 'b, I> {
     f: &'a mut (dyn Write + 'b),
+    _interner: PhantomData<I>,
 }
 
 enum IndentorState {
@@ -36,23 +39,24 @@ impl Write for Indentor<'_, '_> {
     }
 }
 
-impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
+impl<'a, 'b, I: Interner> ProofTreeFormatter<'a, 'b, I> {
     pub(super) fn new(f: &'a mut (dyn Write + 'b)) -> Self {
-        ProofTreeFormatter { f }
+        ProofTreeFormatter { f, _interner: PhantomData }
     }
 
     fn nested<F>(&mut self, func: F) -> std::fmt::Result
     where
-        F: FnOnce(&mut ProofTreeFormatter<'_, '_>) -> std::fmt::Result,
+        F: FnOnce(&mut ProofTreeFormatter<'_, '_, I>) -> std::fmt::Result,
     {
         write!(self.f, " {{")?;
         func(&mut ProofTreeFormatter {
             f: &mut Indentor { f: self.f, state: IndentorState::StartWithNewline },
+            _interner: PhantomData,
         })?;
         writeln!(self.f, "}}")
     }
 
-    pub(super) fn format_goal_evaluation(&mut self, eval: &GoalEvaluation<'_>) -> std::fmt::Result {
+    pub(super) fn format_goal_evaluation(&mut self, eval: &GoalEvaluation<I>) -> std::fmt::Result {
         let goal_text = match eval.kind {
             GoalEvaluationKind::Root { orig_values: _ } => "ROOT GOAL",
             GoalEvaluationKind::Nested => "GOAL",
@@ -63,7 +67,7 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
 
     pub(super) fn format_canonical_goal_evaluation(
         &mut self,
-        eval: &CanonicalGoalEvaluation<'_>,
+        eval: &CanonicalGoalEvaluation<I>,
     ) -> std::fmt::Result {
         writeln!(self.f, "GOAL: {:?}", eval.goal)?;
 
@@ -89,13 +93,13 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
 
     pub(super) fn format_evaluation_step(
         &mut self,
-        evaluation_step: &GoalEvaluationStep<'_>,
+        evaluation_step: &GoalEvaluationStep<I>,
     ) -> 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 {
+    pub(super) fn format_probe(&mut self, probe: &Probe<I>) -> std::fmt::Result {
         match &probe.kind {
             ProbeKind::Root { result } => {
                 write!(self.f, "ROOT RESULT: {result:?}")
@@ -150,7 +154,7 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
 
     pub(super) fn format_added_goals_evaluation(
         &mut self,
-        added_goals_evaluation: &AddedGoalsEvaluation<'_>,
+        added_goals_evaluation: &AddedGoalsEvaluation<I>,
     ) -> std::fmt::Result {
         writeln!(self.f, "TRY_EVALUATE_ADDED_GOALS: {:?}", added_goals_evaluation.result)?;