Make ProofTreeBuilder actually generic over interner

7 files changed, 102 insertions, 83 deletions

diff --git a/compiler/rustc_middle/src/ty/context.rs b/compiler/rustc_middle/src/ty/context.rs
index c09cb95de88..5a04324dc7d 100644
--- a/compiler/rustc_middle/src/ty/context.rs
+++ b/compiler/rustc_middle/src/ty/context.rs
@@ -218,6 +218,13 @@ impl<'tcx> Interner for TyCtxt<'tcx> {
         self.check_and_mk_args(def_id, args)
     }
 
+    fn intern_canonical_goal_evaluation_step(
+        self,
+        step: solve::inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>,
+    ) -> &'tcx solve::inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>> {
+        self.arena.alloc(step)
+    }
+
     fn parent(self, def_id: Self::DefId) -> Self::DefId {
         self.parent(def_id)
     }
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 fc10a8a43cc..4977807aa6c 100644
--- a/compiler/rustc_trait_selection/src/solve/eval_ctxt/canonical.rs
+++ b/compiler/rustc_trait_selection/src/solve/eval_ctxt/canonical.rs
@@ -16,7 +16,6 @@ use crate::solve::{
 use rustc_data_structures::fx::FxHashSet;
 use rustc_index::IndexVec;
 use rustc_infer::infer::canonical::query_response::make_query_region_constraints;
-use rustc_infer::infer::canonical::CanonicalVarValues;
 use rustc_infer::infer::canonical::{CanonicalExt, QueryRegionConstraints};
 use rustc_infer::infer::RegionVariableOrigin;
 use rustc_infer::infer::{InferCtxt, InferOk};
@@ -32,22 +31,24 @@ use rustc_middle::ty::{self, BoundVar, GenericArgKind, Ty, TyCtxt, TypeFoldable}
 use rustc_next_trait_solver::canonicalizer::{CanonicalizeMode, Canonicalizer};
 use rustc_next_trait_solver::resolve::EagerResolver;
 use rustc_span::{Span, DUMMY_SP};
+use rustc_type_ir::CanonicalVarValues;
+use rustc_type_ir::{InferCtxtLike, Interner};
 use std::assert_matches::assert_matches;
 use std::iter;
 use std::ops::Deref;
 
 trait ResponseT<'tcx> {
-    fn var_values(&self) -> CanonicalVarValues<'tcx>;
+    fn var_values(&self) -> CanonicalVarValues<TyCtxt<'tcx>>;
 }
 
 impl<'tcx> ResponseT<'tcx> for Response<TyCtxt<'tcx>> {
-    fn var_values(&self) -> CanonicalVarValues<'tcx> {
+    fn var_values(&self) -> CanonicalVarValues<TyCtxt<'tcx>> {
         self.var_values
     }
 }
 
 impl<'tcx, T> ResponseT<'tcx> for inspect::State<TyCtxt<'tcx>, T> {
-    fn var_values(&self) -> CanonicalVarValues<'tcx> {
+    fn var_values(&self) -> CanonicalVarValues<TyCtxt<'tcx>> {
         self.var_values
     }
 }
@@ -260,7 +261,7 @@ impl<'tcx> EvalCtxt<'_, InferCtxt<'tcx>> {
         infcx: &InferCtxt<'tcx>,
         original_values: &[ty::GenericArg<'tcx>],
         response: &Canonical<'tcx, T>,
-    ) -> CanonicalVarValues<'tcx> {
+    ) -> CanonicalVarValues<TyCtxt<'tcx>> {
         // FIXME: Longterm canonical queries should deal with all placeholders
         // created inside of the query directly instead of returning them to the
         // caller.
@@ -354,7 +355,7 @@ impl<'tcx> EvalCtxt<'_, InferCtxt<'tcx>> {
         infcx: &InferCtxt<'tcx>,
         param_env: ty::ParamEnv<'tcx>,
         original_values: &[ty::GenericArg<'tcx>],
-        var_values: CanonicalVarValues<'tcx>,
+        var_values: CanonicalVarValues<TyCtxt<'tcx>>,
     ) {
         assert_eq!(original_values.len(), var_values.len());
 
@@ -393,13 +394,18 @@ impl<'tcx> EvalCtxt<'_, InferCtxt<'tcx>> {
 /// evaluating a goal. The `var_values` not only include the bound variables
 /// of the query input, but also contain all unconstrained inference vars
 /// created while evaluating this goal.
-pub(in crate::solve) fn make_canonical_state<'tcx, T: TypeFoldable<TyCtxt<'tcx>>>(
-    infcx: &InferCtxt<'tcx>,
-    var_values: &[ty::GenericArg<'tcx>],
+pub(in crate::solve) fn make_canonical_state<Infcx, T, I>(
+    infcx: &Infcx,
+    var_values: &[I::GenericArg],
     max_input_universe: ty::UniverseIndex,
     data: T,
-) -> inspect::CanonicalState<TyCtxt<'tcx>, T> {
-    let var_values = CanonicalVarValues { var_values: infcx.tcx.mk_args(var_values) };
+) -> inspect::CanonicalState<I, T>
+where
+    Infcx: InferCtxtLike<Interner = I>,
+    I: Interner,
+    T: TypeFoldable<I>,
+{
+    let var_values = CanonicalVarValues { var_values: infcx.interner().mk_args(var_values) };
     let state = inspect::State { var_values, data };
     let state = state.fold_with(&mut EagerResolver::new(infcx));
     Canonicalizer::canonicalize(
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 72a4096f2aa..98ba3feeca1 100644
--- a/compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs
+++ b/compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs
@@ -98,7 +98,7 @@ pub struct EvalCtxt<
     // evaluation code.
     tainted: Result<(), NoSolution>,
 
-    pub(super) inspect: ProofTreeBuilder<I>,
+    pub(super) inspect: ProofTreeBuilder<Infcx>,
 }
 
 #[derive(derivative::Derivative)]
@@ -218,7 +218,7 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
         tcx: TyCtxt<'tcx>,
         search_graph: &'a mut search_graph::SearchGraph<TyCtxt<'tcx>>,
         canonical_input: CanonicalInput<'tcx>,
-        canonical_goal_evaluation: &mut ProofTreeBuilder<TyCtxt<'tcx>>,
+        canonical_goal_evaluation: &mut ProofTreeBuilder<InferCtxt<'tcx>>,
         f: impl FnOnce(&mut EvalCtxt<'_, InferCtxt<'tcx>>, Goal<'tcx, ty::Predicate<'tcx>>) -> R,
     ) -> R {
         let intercrate = match search_graph.solver_mode() {
@@ -280,7 +280,7 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
         tcx: TyCtxt<'tcx>,
         search_graph: &'a mut search_graph::SearchGraph<TyCtxt<'tcx>>,
         canonical_input: CanonicalInput<'tcx>,
-        goal_evaluation: &mut ProofTreeBuilder<TyCtxt<'tcx>>,
+        goal_evaluation: &mut ProofTreeBuilder<InferCtxt<'tcx>>,
     ) -> QueryResult<'tcx> {
         let mut canonical_goal_evaluation =
             goal_evaluation.new_canonical_goal_evaluation(canonical_input);
@@ -1114,7 +1114,7 @@ struct ReplaceAliasWithInfer<'me, 'a, 'tcx> {
 
 impl<'tcx> TypeFolder<TyCtxt<'tcx>> for ReplaceAliasWithInfer<'_, '_, 'tcx> {
     fn interner(&self) -> TyCtxt<'tcx> {
-        self.ecx.tcx()
+        self.ecx.interner()
     }
 
     fn fold_ty(&mut self, ty: Ty<'tcx>) -> Ty<'tcx> {
diff --git a/compiler/rustc_trait_selection/src/solve/inspect/build.rs b/compiler/rustc_trait_selection/src/solve/inspect/build.rs
index 3c633362648..84c04900ae4 100644
--- a/compiler/rustc_trait_selection/src/solve/inspect/build.rs
+++ b/compiler/rustc_trait_selection/src/solve/inspect/build.rs
@@ -3,18 +3,16 @@
 //! This code is *a bit* of a mess and can hopefully be
 //! mostly ignored. For a general overview of how it works,
 //! see the comment on [ProofTreeBuilder].
+use std::marker::PhantomData;
 use std::mem;
 
 use crate::solve::eval_ctxt::canonical;
 use crate::solve::{self, inspect, GenerateProofTree};
-use rustc_infer::infer::InferCtxt;
 use rustc_middle::bug;
-use rustc_middle::infer::canonical::CanonicalVarValues;
-use rustc_middle::ty::{self, TyCtxt};
 use rustc_next_trait_solver::solve::{
     CanonicalInput, Certainty, Goal, GoalSource, QueryInput, QueryResult,
 };
-use rustc_type_ir::Interner;
+use rustc_type_ir::{self as ty, InferCtxtLike, Interner};
 
 /// The core data structure when building proof trees.
 ///
@@ -36,7 +34,11 @@ use rustc_type_ir::Interner;
 /// trees. At the end of trait solving `ProofTreeBuilder::finalize`
 /// is called to recursively convert the whole structure to a
 /// finished proof tree.
-pub(in crate::solve) struct ProofTreeBuilder<I: Interner> {
+pub(in crate::solve) struct ProofTreeBuilder<
+    Infcx: InferCtxtLike<Interner = I>,
+    I: Interner = <Infcx as InferCtxtLike>::Interner,
+> {
+    _infcx: PhantomData<Infcx>,
     state: Option<Box<DebugSolver<I>>>,
 }
 
@@ -229,36 +231,36 @@ impl<I: Interner> WipProbeStep<I> {
     }
 }
 
-// FIXME: Genericize this impl.
-impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
-    fn new(state: impl Into<DebugSolver<TyCtxt<'tcx>>>) -> ProofTreeBuilder<TyCtxt<'tcx>> {
-        ProofTreeBuilder { state: Some(Box::new(state.into())) }
+impl<Infcx: InferCtxtLike<Interner = I>, I: Interner> ProofTreeBuilder<Infcx> {
+    fn new(state: impl Into<DebugSolver<I>>) -> ProofTreeBuilder<Infcx> {
+        ProofTreeBuilder { state: Some(Box::new(state.into())), _infcx: PhantomData }
     }
 
-    fn opt_nested<T: Into<DebugSolver<TyCtxt<'tcx>>>>(
-        &self,
-        state: impl FnOnce() -> Option<T>,
-    ) -> Self {
+    fn opt_nested<T: Into<DebugSolver<I>>>(&self, state: impl FnOnce() -> Option<T>) -> Self {
         ProofTreeBuilder {
             state: self.state.as_ref().and_then(|_| Some(state()?.into())).map(Box::new),
+            _infcx: PhantomData,
         }
     }
 
-    fn nested<T: Into<DebugSolver<TyCtxt<'tcx>>>>(&self, state: impl FnOnce() -> T) -> Self {
-        ProofTreeBuilder { state: self.state.as_ref().map(|_| Box::new(state().into())) }
+    fn nested<T: Into<DebugSolver<I>>>(&self, state: impl FnOnce() -> T) -> Self {
+        ProofTreeBuilder {
+            state: self.state.as_ref().map(|_| Box::new(state().into())),
+            _infcx: PhantomData,
+        }
     }
 
-    fn as_mut(&mut self) -> Option<&mut DebugSolver<TyCtxt<'tcx>>> {
+    fn as_mut(&mut self) -> Option<&mut DebugSolver<I>> {
         self.state.as_deref_mut()
     }
 
-    pub fn take_and_enter_probe(&mut self) -> ProofTreeBuilder<TyCtxt<'tcx>> {
-        let mut nested = ProofTreeBuilder { state: self.state.take() };
+    pub fn take_and_enter_probe(&mut self) -> ProofTreeBuilder<Infcx> {
+        let mut nested = ProofTreeBuilder { state: self.state.take(), _infcx: PhantomData };
         nested.enter_probe();
         nested
     }
 
-    pub fn finalize(self) -> Option<inspect::GoalEvaluation<TyCtxt<'tcx>>> {
+    pub fn finalize(self) -> Option<inspect::GoalEvaluation<I>> {
         match *self.state? {
             DebugSolver::GoalEvaluation(wip_goal_evaluation) => {
                 Some(wip_goal_evaluation.finalize())
@@ -267,21 +269,19 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
         }
     }
 
-    pub fn new_maybe_root(
-        generate_proof_tree: GenerateProofTree,
-    ) -> ProofTreeBuilder<TyCtxt<'tcx>> {
+    pub fn new_maybe_root(generate_proof_tree: GenerateProofTree) -> ProofTreeBuilder<Infcx> {
         match generate_proof_tree {
             GenerateProofTree::No => ProofTreeBuilder::new_noop(),
             GenerateProofTree::Yes => ProofTreeBuilder::new_root(),
         }
     }
 
-    pub fn new_root() -> ProofTreeBuilder<TyCtxt<'tcx>> {
+    pub fn new_root() -> ProofTreeBuilder<Infcx> {
         ProofTreeBuilder::new(DebugSolver::Root)
     }
 
-    pub fn new_noop() -> ProofTreeBuilder<TyCtxt<'tcx>> {
-        ProofTreeBuilder { state: None }
+    pub fn new_noop() -> ProofTreeBuilder<Infcx> {
+        ProofTreeBuilder { state: None, _infcx: PhantomData }
     }
 
     pub fn is_noop(&self) -> bool {
@@ -290,10 +290,10 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
 
     pub(in crate::solve) fn new_goal_evaluation(
         &mut self,
-        goal: Goal<TyCtxt<'tcx>, ty::Predicate<'tcx>>,
-        orig_values: &[ty::GenericArg<'tcx>],
+        goal: Goal<I, I::Predicate>,
+        orig_values: &[I::GenericArg],
         kind: solve::GoalEvaluationKind,
-    ) -> ProofTreeBuilder<TyCtxt<'tcx>> {
+    ) -> ProofTreeBuilder<Infcx> {
         self.opt_nested(|| match kind {
             solve::GoalEvaluationKind::Root => Some(WipGoalEvaluation {
                 uncanonicalized_goal: goal,
@@ -306,8 +306,8 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
 
     pub fn new_canonical_goal_evaluation(
         &mut self,
-        goal: CanonicalInput<TyCtxt<'tcx>>,
-    ) -> ProofTreeBuilder<TyCtxt<'tcx>> {
+        goal: CanonicalInput<I>,
+    ) -> ProofTreeBuilder<Infcx> {
         self.nested(|| WipCanonicalGoalEvaluation {
             goal,
             kind: None,
@@ -318,12 +318,13 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
 
     pub fn finalize_canonical_goal_evaluation(
         &mut self,
-        tcx: TyCtxt<'tcx>,
-    ) -> Option<&'tcx inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>> {
+        tcx: I,
+    ) -> Option<I::CanonicalGoalEvaluationStepRef> {
         self.as_mut().map(|this| match this {
             DebugSolver::CanonicalGoalEvaluation(evaluation) => {
                 let final_revision = mem::take(&mut evaluation.final_revision).unwrap();
-                let final_revision = &*tcx.arena.alloc(final_revision.finalize());
+                let final_revision =
+                    tcx.intern_canonical_goal_evaluation_step(final_revision.finalize());
                 let kind = WipCanonicalGoalEvaluationKind::Interned { final_revision };
                 assert_eq!(evaluation.kind.replace(kind), None);
                 final_revision
@@ -334,7 +335,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
 
     pub fn canonical_goal_evaluation(
         &mut self,
-        canonical_goal_evaluation: ProofTreeBuilder<TyCtxt<'tcx>>,
+        canonical_goal_evaluation: ProofTreeBuilder<Infcx>,
     ) {
         if let Some(this) = self.as_mut() {
             match (this, *canonical_goal_evaluation.state.unwrap()) {
@@ -350,10 +351,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
         }
     }
 
-    pub fn canonical_goal_evaluation_kind(
-        &mut self,
-        kind: WipCanonicalGoalEvaluationKind<TyCtxt<'tcx>>,
-    ) {
+    pub fn canonical_goal_evaluation_kind(&mut self, kind: WipCanonicalGoalEvaluationKind<I>) {
         if let Some(this) = self.as_mut() {
             match this {
                 DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
@@ -364,7 +362,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
         }
     }
 
-    pub fn goal_evaluation(&mut self, goal_evaluation: ProofTreeBuilder<TyCtxt<'tcx>>) {
+    pub fn goal_evaluation(&mut self, goal_evaluation: ProofTreeBuilder<Infcx>) {
         if let Some(this) = self.as_mut() {
             match this {
                 DebugSolver::Root => *this = *goal_evaluation.state.unwrap(),
@@ -378,9 +376,9 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
 
     pub fn new_goal_evaluation_step(
         &mut self,
-        var_values: CanonicalVarValues<'tcx>,
-        instantiated_goal: QueryInput<TyCtxt<'tcx>, ty::Predicate<'tcx>>,
-    ) -> ProofTreeBuilder<TyCtxt<'tcx>> {
+        var_values: ty::CanonicalVarValues<I>,
+        instantiated_goal: QueryInput<I, I::Predicate>,
+    ) -> ProofTreeBuilder<Infcx> {
         self.nested(|| WipCanonicalGoalEvaluationStep {
             var_values: var_values.var_values.to_vec(),
             instantiated_goal,
@@ -394,7 +392,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
         })
     }
 
-    pub fn goal_evaluation_step(&mut self, goal_evaluation_step: ProofTreeBuilder<TyCtxt<'tcx>>) {
+    pub fn goal_evaluation_step(&mut self, goal_evaluation_step: ProofTreeBuilder<Infcx>) {
         if let Some(this) = self.as_mut() {
             match (this, *goal_evaluation_step.state.unwrap()) {
                 (
@@ -408,7 +406,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
         }
     }
 
-    pub fn add_var_value<T: Into<ty::GenericArg<'tcx>>>(&mut self, arg: T) {
+    pub fn add_var_value<T: Into<I::GenericArg>>(&mut self, arg: T) {
         match self.as_mut() {
             None => {}
             Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
@@ -435,7 +433,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
         }
     }
 
-    pub fn probe_kind(&mut self, probe_kind: inspect::ProbeKind<TyCtxt<'tcx>>) {
+    pub fn probe_kind(&mut self, probe_kind: inspect::ProbeKind<I>) {
         match self.as_mut() {
             None => {}
             Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
@@ -446,11 +444,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
         }
     }
 
-    pub fn probe_final_state(
-        &mut self,
-        infcx: &InferCtxt<'tcx>,
-        max_input_universe: ty::UniverseIndex,
-    ) {
+    pub fn probe_final_state(&mut self, infcx: &Infcx, max_input_universe: ty::UniverseIndex) {
         match self.as_mut() {
             None => {}
             Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
@@ -469,24 +463,24 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
 
     pub fn add_normalizes_to_goal(
         &mut self,
-        infcx: &InferCtxt<'tcx>,
+        infcx: &Infcx,
         max_input_universe: ty::UniverseIndex,
-        goal: Goal<TyCtxt<'tcx>, ty::NormalizesTo<'tcx>>,
+        goal: Goal<I, ty::NormalizesTo<I>>,
     ) {
         self.add_goal(
             infcx,
             max_input_universe,
             GoalSource::Misc,
-            goal.with(infcx.tcx, goal.predicate),
+            goal.with(infcx.interner(), goal.predicate),
         );
     }
 
     pub fn add_goal(
         &mut self,
-        infcx: &InferCtxt<'tcx>,
+        infcx: &Infcx,
         max_input_universe: ty::UniverseIndex,
         source: GoalSource,
-        goal: Goal<TyCtxt<'tcx>, ty::Predicate<'tcx>>,
+        goal: Goal<I, I::Predicate>,
     ) {
         match self.as_mut() {
             None => {}
@@ -505,9 +499,9 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
 
     pub(crate) fn record_impl_args(
         &mut self,
-        infcx: &InferCtxt<'tcx>,
+        infcx: &Infcx,
         max_input_universe: ty::UniverseIndex,
-        impl_args: ty::GenericArgsRef<'tcx>,
+        impl_args: I::GenericArgs,
     ) {
         match self.as_mut() {
             Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
@@ -540,7 +534,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
         }
     }
 
-    pub fn finish_probe(mut self) -> ProofTreeBuilder<TyCtxt<'tcx>> {
+    pub fn finish_probe(mut self) -> ProofTreeBuilder<Infcx> {
         match self.as_mut() {
             None => {}
             Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
@@ -555,7 +549,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
         self
     }
 
-    pub fn query_result(&mut self, result: QueryResult<TyCtxt<'tcx>>) {
+    pub fn query_result(&mut self, result: QueryResult<I>) {
         if let Some(this) = self.as_mut() {
             match this {
                 DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
diff --git a/compiler/rustc_trait_selection/src/solve/search_graph.rs b/compiler/rustc_trait_selection/src/solve/search_graph.rs
index 6be623b6044..f1b8bf4676e 100644
--- a/compiler/rustc_trait_selection/src/solve/search_graph.rs
+++ b/compiler/rustc_trait_selection/src/solve/search_graph.rs
@@ -3,6 +3,7 @@ use std::mem;
 use rustc_data_structures::fx::{FxHashMap, FxHashSet};
 use rustc_index::Idx;
 use rustc_index::IndexVec;
+use rustc_infer::infer::InferCtxt;
 use rustc_middle::dep_graph::dep_kinds;
 use rustc_middle::traits::solve::CacheData;
 use rustc_middle::traits::solve::EvaluationCache;
@@ -261,10 +262,10 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
         &mut self,
         tcx: TyCtxt<'tcx>,
         input: CanonicalInput<TyCtxt<'tcx>>,
-        inspect: &mut ProofTreeBuilder<TyCtxt<'tcx>>,
+        inspect: &mut ProofTreeBuilder<InferCtxt<'tcx>>,
         mut prove_goal: impl FnMut(
             &mut Self,
-            &mut ProofTreeBuilder<TyCtxt<'tcx>>,
+            &mut ProofTreeBuilder<InferCtxt<'tcx>>,
         ) -> QueryResult<TyCtxt<'tcx>>,
     ) -> QueryResult<TyCtxt<'tcx>> {
         self.check_invariants();
@@ -426,7 +427,7 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
         tcx: TyCtxt<'tcx>,
         input: CanonicalInput<TyCtxt<'tcx>>,
         available_depth: Limit,
-        inspect: &mut ProofTreeBuilder<TyCtxt<'tcx>>,
+        inspect: &mut ProofTreeBuilder<InferCtxt<'tcx>>,
     ) -> Option<QueryResult<TyCtxt<'tcx>>> {
         let CacheData { result, proof_tree, additional_depth, encountered_overflow } = self
             .global_cache(tcx)
@@ -473,11 +474,11 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
         &mut self,
         tcx: TyCtxt<'tcx>,
         input: CanonicalInput<TyCtxt<'tcx>>,
-        inspect: &mut ProofTreeBuilder<TyCtxt<'tcx>>,
+        inspect: &mut ProofTreeBuilder<InferCtxt<'tcx>>,
         prove_goal: &mut F,
     ) -> StepResult<TyCtxt<'tcx>>
     where
-        F: FnMut(&mut Self, &mut ProofTreeBuilder<TyCtxt<'tcx>>) -> QueryResult<TyCtxt<'tcx>>,
+        F: FnMut(&mut Self, &mut ProofTreeBuilder<InferCtxt<'tcx>>) -> QueryResult<TyCtxt<'tcx>>,
     {
         let result = prove_goal(self, inspect);
         let stack_entry = self.pop_stack();
diff --git a/compiler/rustc_type_ir/src/inherent.rs b/compiler/rustc_type_ir/src/inherent.rs
index e7e893f27da..7b1dfecfee2 100644
--- a/compiler/rustc_type_ir/src/inherent.rs
+++ b/compiler/rustc_type_ir/src/inherent.rs
@@ -132,7 +132,14 @@ pub trait GenericArgs<I: Interner<GenericArgs = Self>>:
 }
 
 pub trait Predicate<I: Interner<Predicate = Self>>:
-    Copy + Debug + Hash + Eq + TypeSuperVisitable<I> + TypeSuperFoldable<I> + Flags
+    Copy
+    + Debug
+    + Hash
+    + Eq
+    + TypeSuperVisitable<I>
+    + TypeSuperFoldable<I>
+    + Flags
+    + UpcastFrom<I, ty::NormalizesTo<I>>
 {
     fn is_coinductive(self, interner: I) -> bool;
 }
diff --git a/compiler/rustc_type_ir/src/interner.rs b/compiler/rustc_type_ir/src/interner.rs
index e49db171a53..2a228c973d3 100644
--- a/compiler/rustc_type_ir/src/interner.rs
+++ b/compiler/rustc_type_ir/src/interner.rs
@@ -3,6 +3,7 @@ use std::fmt::Debug;
 use std::hash::Hash;
 use std::ops::Deref;
 
+use crate::fold::TypeFoldable;
 use crate::inherent::*;
 use crate::ir_print::IrPrint;
 use crate::solve::inspect::CanonicalGoalEvaluationStep;
@@ -90,7 +91,7 @@ pub trait Interner:
     type PlaceholderRegion: PlaceholderLike;
 
     // Predicates
-    type ParamEnv: Copy + Debug + Hash + Eq;
+    type ParamEnv: Copy + Debug + Hash + Eq + TypeFoldable<Self>;
     type Predicate: Predicate<Self>;
     type Clause: Clause<Self>;
     type Clauses: Copy + Debug + Hash + Eq + TypeSuperVisitable<Self> + Flags;
@@ -114,15 +115,18 @@ pub trait Interner:
     ) -> (ty::TraitRef<Self>, Self::OwnItemArgs);
 
     fn mk_args(self, args: &[Self::GenericArg]) -> Self::GenericArgs;
-
     fn mk_args_from_iter(self, args: impl Iterator<Item = Self::GenericArg>) -> Self::GenericArgs;
-
     fn check_and_mk_args(
         self,
         def_id: Self::DefId,
         args: impl IntoIterator<Item: Into<Self::GenericArg>>,
     ) -> Self::GenericArgs;
 
+    fn intern_canonical_goal_evaluation_step(
+        self,
+        step: CanonicalGoalEvaluationStep<Self>,
+    ) -> Self::CanonicalGoalEvaluationStepRef;
+
     fn parent(self, def_id: Self::DefId) -> Self::DefId;
 
     fn recursion_limit(self) -> usize;