diff --git a/crates/hir-ty/src/autoderef.rs b/crates/hir-ty/src/autoderef.rs
index 4ea0156e1248..82696a5c94da 100644
--- a/crates/hir-ty/src/autoderef.rs
+++ b/crates/hir-ty/src/autoderef.rs
@@ -13,7 +13,7 @@ use triomphe::Arc;
 
 use crate::{
     Canonical, Goal, Interner, ProjectionTyExt, TraitEnvironment, Ty, TyBuilder, TyKind,
-    db::HirDatabase, infer::unify::InferenceTable,
+    db::HirDatabase, infer::unify::InferenceTable, next_solver::mapping::ChalkToNextSolver,
 };
 
 const AUTODEREF_RECURSION_LIMIT: usize = 20;
@@ -98,7 +98,7 @@ impl<'table, 'db> Autoderef<'table, 'db> {
         explicit: bool,
         use_receiver_trait: bool,
     ) -> Self {
-        let ty = table.resolve_ty_shallow(&ty);
+        let ty = table.structurally_resolve_type(&ty);
         Autoderef { table, ty, at_start: true, steps: Vec::new(), explicit, use_receiver_trait }
     }
 
@@ -114,7 +114,7 @@ impl<'table, 'db> Autoderef<'table, 'db, usize> {
         explicit: bool,
         use_receiver_trait: bool,
     ) -> Self {
-        let ty = table.resolve_ty_shallow(&ty);
+        let ty = table.structurally_resolve_type(&ty);
         Autoderef { table, ty, at_start: true, steps: 0, explicit, use_receiver_trait }
     }
 }
@@ -160,7 +160,7 @@ pub(crate) fn autoderef_step(
     use_receiver_trait: bool,
 ) -> Option<(AutoderefKind, Ty)> {
     if let Some(derefed) = builtin_deref(table.db, &ty, explicit) {
-        Some((AutoderefKind::Builtin, table.resolve_ty_shallow(derefed)))
+        Some((AutoderefKind::Builtin, table.structurally_resolve_type(derefed)))
     } else {
         Some((AutoderefKind::Overloaded, deref_by_trait(table, ty, use_receiver_trait)?))
     }
@@ -187,7 +187,7 @@ pub(crate) fn deref_by_trait(
     use_receiver_trait: bool,
 ) -> Option<Ty> {
     let _p = tracing::info_span!("deref_by_trait").entered();
-    if table.resolve_ty_shallow(&ty).inference_var(Interner).is_some() {
+    if table.structurally_resolve_type(&ty).inference_var(Interner).is_some() {
         // don't try to deref unknown variables
         return None;
     }
@@ -229,8 +229,8 @@ pub(crate) fn deref_by_trait(
         return None;
     }
 
-    table.register_obligation(implements_goal);
+    table.register_obligation(implements_goal.to_nextsolver(table.interner));
 
     let result = table.normalize_projection_ty(projection);
-    Some(table.resolve_ty_shallow(&result))
+    Some(table.structurally_resolve_type(&result))
 }
diff --git a/crates/hir-ty/src/chalk_ext.rs b/crates/hir-ty/src/chalk_ext.rs
index 33ae099c690e..9f0ea14a8063 100644
--- a/crates/hir-ty/src/chalk_ext.rs
+++ b/crates/hir-ty/src/chalk_ext.rs
@@ -245,26 +245,30 @@ impl TyExt for Ty {
     }
 
     fn impl_trait_bounds(&self, db: &dyn HirDatabase) -> Option<Vec<QuantifiedWhereClause>> {
+        let handle_async_block_type_impl_trait = |def: DefWithBodyId| {
+            let krate = def.module(db).krate();
+            if let Some(future_trait) = LangItem::Future.resolve_trait(db, krate) {
+                // This is only used by type walking.
+                // Parameters will be walked outside, and projection predicate is not used.
+                // So just provide the Future trait.
+                let impl_bound = Binders::empty(
+                    Interner,
+                    WhereClause::Implemented(TraitRef {
+                        trait_id: to_chalk_trait_id(future_trait),
+                        substitution: Substitution::empty(Interner),
+                    }),
+                );
+                Some(vec![impl_bound])
+            } else {
+                None
+            }
+        };
+
         match self.kind(Interner) {
             TyKind::OpaqueType(opaque_ty_id, subst) => {
                 match db.lookup_intern_impl_trait_id((*opaque_ty_id).into()) {
                     ImplTraitId::AsyncBlockTypeImplTrait(def, _expr) => {
-                        let krate = def.module(db).krate();
-                        if let Some(future_trait) = LangItem::Future.resolve_trait(db, krate) {
-                            // This is only used by type walking.
-                            // Parameters will be walked outside, and projection predicate is not used.
-                            // So just provide the Future trait.
-                            let impl_bound = Binders::empty(
-                                Interner,
-                                WhereClause::Implemented(TraitRef {
-                                    trait_id: to_chalk_trait_id(future_trait),
-                                    substitution: Substitution::empty(Interner),
-                                }),
-                            );
-                            Some(vec![impl_bound])
-                        } else {
-                            None
-                        }
+                        handle_async_block_type_impl_trait(def)
                     }
                     ImplTraitId::ReturnTypeImplTrait(func, idx) => {
                         db.return_type_impl_traits(func).map(|it| {
@@ -299,8 +303,9 @@ impl TyExt for Ty {
                             data.substitute(Interner, &opaque_ty.substitution)
                         })
                     }
-                    // It always has an parameter for Future::Output type.
-                    ImplTraitId::AsyncBlockTypeImplTrait(..) => unreachable!(),
+                    ImplTraitId::AsyncBlockTypeImplTrait(def, _) => {
+                        return handle_async_block_type_impl_trait(def);
+                    }
                 };
 
                 predicates.map(|it| it.into_value_and_skipped_binders().0)
diff --git a/crates/hir-ty/src/consteval_nextsolver.rs b/crates/hir-ty/src/consteval_nextsolver.rs
index 4f95c9a13acd..6e07d3afe552 100644
--- a/crates/hir-ty/src/consteval_nextsolver.rs
+++ b/crates/hir-ty/src/consteval_nextsolver.rs
@@ -27,7 +27,7 @@ use crate::{
     next_solver::{
         Const, ConstBytes, ConstKind, DbInterner, ErrorGuaranteed, GenericArg, GenericArgs,
         ParamConst, SolverDefId, Ty, ValueConst,
-        mapping::{ChalkToNextSolver, convert_args_for_result, convert_binder_to_early_binder},
+        mapping::{ChalkToNextSolver, NextSolverToChalk, convert_binder_to_early_binder},
     },
 };
 
@@ -145,7 +145,7 @@ pub fn try_const_usize<'db>(db: &'db dyn HirDatabase, c: Const<'db>) -> Option<u
                 SolverDefId::StaticId(id) => GeneralConstId::StaticId(id),
                 _ => unreachable!(),
             };
-            let subst = convert_args_for_result(interner, unevaluated_const.args.as_slice());
+            let subst = unevaluated_const.args.to_chalk(interner);
             let ec = db.const_eval(c, subst, None).ok()?.to_nextsolver(interner);
             try_const_usize(db, ec)
         }
@@ -168,7 +168,7 @@ pub fn try_const_isize<'db>(db: &'db dyn HirDatabase, c: &Const<'db>) -> Option<
                 SolverDefId::StaticId(id) => GeneralConstId::StaticId(id),
                 _ => unreachable!(),
             };
-            let subst = convert_args_for_result(interner, unevaluated_const.args.as_slice());
+            let subst = unevaluated_const.args.to_chalk(interner);
             let ec = db.const_eval(c, subst, None).ok()?.to_nextsolver(interner);
             try_const_isize(db, &ec)
         }
diff --git a/crates/hir-ty/src/infer.rs b/crates/hir-ty/src/infer.rs
index 71b33a0e9035..265d1f8541cc 100644
--- a/crates/hir-ty/src/infer.rs
+++ b/crates/hir-ty/src/infer.rs
@@ -55,10 +55,9 @@ use stdx::{always, never};
 use triomphe::Arc;
 
 use crate::{
-    AliasEq, AliasTy, Binders, ClosureId, Const, DomainGoal, GenericArg, Goal, ImplTraitId,
-    ImplTraitIdx, InEnvironment, IncorrectGenericsLenKind, Interner, Lifetime, OpaqueTyId,
-    ParamLoweringMode, PathLoweringDiagnostic, ProjectionTy, Substitution, TraitEnvironment, Ty,
-    TyBuilder, TyExt,
+    AliasEq, AliasTy, Binders, ClosureId, Const, DomainGoal, GenericArg, ImplTraitId, ImplTraitIdx,
+    IncorrectGenericsLenKind, Interner, Lifetime, OpaqueTyId, ParamLoweringMode,
+    PathLoweringDiagnostic, ProjectionTy, Substitution, TraitEnvironment, Ty, TyBuilder, TyExt,
     db::HirDatabase,
     fold_tys,
     generics::Generics,
@@ -70,6 +69,7 @@ use crate::{
     },
     lower::{ImplTraitLoweringMode, LifetimeElisionKind, diagnostics::TyLoweringDiagnostic},
     mir::MirSpan,
+    next_solver::{self, mapping::ChalkToNextSolver},
     static_lifetime, to_assoc_type_id,
     traits::FnTrait,
     utils::UnevaluatedConstEvaluatorFolder,
@@ -182,13 +182,13 @@ impl BindingMode {
 }
 
 #[derive(Debug)]
-pub(crate) struct InferOk<T> {
+pub(crate) struct InferOk<'db, T> {
     value: T,
-    goals: Vec<InEnvironment<Goal>>,
+    goals: Vec<next_solver::Goal<'db, next_solver::Predicate<'db>>>,
 }
 
-impl<T> InferOk<T> {
-    fn map<U>(self, f: impl FnOnce(T) -> U) -> InferOk<U> {
+impl<'db, T> InferOk<'db, T> {
+    fn map<U>(self, f: impl FnOnce(T) -> U) -> InferOk<'db, U> {
         InferOk { value: f(self.value), goals: self.goals }
     }
 }
@@ -203,7 +203,7 @@ pub enum InferenceTyDiagnosticSource {
 
 #[derive(Debug)]
 pub(crate) struct TypeError;
-pub(crate) type InferResult<T> = Result<InferOk<T>, TypeError>;
+pub(crate) type InferResult<'db, T> = Result<InferOk<'db, T>, TypeError>;
 
 #[derive(Debug, PartialEq, Eq, Clone)]
 pub enum InferenceDiagnostic {
@@ -832,6 +832,7 @@ impl<'db> InferenceContext<'db> {
             coercion_casts,
             diagnostics: _,
         } = &mut result;
+        table.resolve_obligations_as_possible();
         table.fallback_if_possible();
 
         // Comment from rustc:
@@ -1480,7 +1481,8 @@ impl<'db> InferenceContext<'db> {
     }
 
     fn push_obligation(&mut self, o: DomainGoal) {
-        self.table.register_obligation(o.cast(Interner));
+        let goal: crate::Goal = o.cast(Interner);
+        self.table.register_obligation(goal.to_nextsolver(self.table.interner));
     }
 
     fn unify(&mut self, ty1: &Ty, ty2: &Ty) -> bool {
@@ -1746,7 +1748,7 @@ impl<'db> InferenceContext<'db> {
 
                     ty = self.table.insert_type_vars(ty);
                     ty = self.table.normalize_associated_types_in(ty);
-                    ty = self.table.resolve_ty_shallow(&ty);
+                    ty = self.table.structurally_resolve_type(&ty);
                     if ty.is_unknown() {
                         return (self.err_ty(), None);
                     }
@@ -1817,7 +1819,7 @@ impl<'db> InferenceContext<'db> {
         let ty = match ty.kind(Interner) {
             TyKind::Alias(AliasTy::Projection(proj_ty)) => {
                 let ty = self.table.normalize_projection_ty(proj_ty.clone());
-                self.table.resolve_ty_shallow(&ty)
+                self.table.structurally_resolve_type(&ty)
             }
             _ => ty,
         };
@@ -2047,7 +2049,7 @@ impl Expectation {
     fn adjust_for_branches(&self, table: &mut unify::InferenceTable<'_>) -> Expectation {
         match self {
             Expectation::HasType(ety) => {
-                let ety = table.resolve_ty_shallow(ety);
+                let ety = table.structurally_resolve_type(ety);
                 if ety.is_ty_var() { Expectation::None } else { Expectation::HasType(ety) }
             }
             Expectation::RValueLikeUnsized(ety) => Expectation::RValueLikeUnsized(ety.clone()),
diff --git a/crates/hir-ty/src/infer/closure.rs b/crates/hir-ty/src/infer/closure.rs
index 9ef046afdb3d..5a69ad68b58e 100644
--- a/crates/hir-ty/src/infer/closure.rs
+++ b/crates/hir-ty/src/infer/closure.rs
@@ -39,6 +39,7 @@ use crate::{
     infer::{BreakableKind, CoerceMany, Diverges, coerce::CoerceNever},
     make_binders,
     mir::{BorrowKind, MirSpan, MutBorrowKind, ProjectionElem},
+    next_solver::mapping::ChalkToNextSolver,
     to_assoc_type_id,
     traits::FnTrait,
     utils::{self, elaborate_clause_supertraits},
@@ -437,10 +438,10 @@ impl InferenceContext<'_> {
             associated_ty_id: to_assoc_type_id(future_output),
             substitution: Substitution::from1(Interner, ret_param_future.clone()),
         });
-        self.table.register_obligation(
+        let goal: crate::Goal =
             crate::AliasEq { alias: future_projection, ty: ret_param_future_output.clone() }
-                .cast(Interner),
-        );
+                .cast(Interner);
+        self.table.register_obligation(goal.to_nextsolver(self.table.interner));
 
         Some(FnSubst(Substitution::from_iter(
             Interner,
@@ -568,7 +569,10 @@ impl InferenceContext<'_> {
         let supplied_sig = self.supplied_sig_of_closure(body, ret_type, arg_types, closure_kind);
 
         let snapshot = self.table.snapshot();
-        if !self.table.unify(&expected_sig.substitution, &supplied_sig.expected_sig.substitution) {
+        if !self.table.unify::<_, crate::next_solver::GenericArgs<'_>>(
+            &expected_sig.substitution.0,
+            &supplied_sig.expected_sig.substitution.0,
+        ) {
             self.table.rollback_to(snapshot);
         }
 
diff --git a/crates/hir-ty/src/infer/coerce.rs b/crates/hir-ty/src/infer/coerce.rs
index 631a91bac481..df516662bfd3 100644
--- a/crates/hir-ty/src/infer/coerce.rs
+++ b/crates/hir-ty/src/infer/coerce.rs
@@ -7,27 +7,28 @@
 
 use std::iter;
 
-use chalk_ir::{BoundVar, Goal, Mutability, TyKind, TyVariableKind, cast::Cast};
+use chalk_ir::{BoundVar, Mutability, TyKind, TyVariableKind, cast::Cast};
 use hir_def::{hir::ExprId, lang_item::LangItem};
+use rustc_type_ir::solve::Certainty;
 use stdx::always;
 use triomphe::Arc;
 
 use crate::{
-    Canonical, DomainGoal, FnAbi, FnPointer, FnSig, InEnvironment, Interner, Lifetime,
-    Substitution, TraitEnvironment, Ty, TyBuilder, TyExt,
+    Canonical, FnAbi, FnPointer, FnSig, Goal, Interner, Lifetime, Substitution, TraitEnvironment,
+    Ty, TyBuilder, TyExt,
     autoderef::{Autoderef, AutoderefKind},
     db::HirDatabase,
     infer::{
         Adjust, Adjustment, AutoBorrow, InferOk, InferenceContext, OverloadedDeref, PointerCast,
         TypeError, TypeMismatch,
     },
-    traits::NextTraitSolveResult,
+    next_solver,
     utils::ClosureSubst,
 };
 
 use super::unify::InferenceTable;
 
-pub(crate) type CoerceResult = Result<InferOk<(Vec<Adjustment>, Ty)>, TypeError>;
+pub(crate) type CoerceResult<'db> = Result<InferOk<'db, (Vec<Adjustment>, Ty)>, TypeError>;
 
 /// Do not require any adjustments, i.e. coerce `x -> x`.
 fn identity(_: Ty) -> Vec<Adjustment> {
@@ -39,11 +40,11 @@ fn simple(kind: Adjust) -> impl FnOnce(Ty) -> Vec<Adjustment> {
 }
 
 /// This always returns `Ok(...)`.
-fn success(
+fn success<'db>(
     adj: Vec<Adjustment>,
     target: Ty,
-    goals: Vec<InEnvironment<Goal<Interner>>>,
-) -> CoerceResult {
+    goals: Vec<next_solver::Goal<'db, next_solver::Predicate<'db>>>,
+) -> CoerceResult<'db> {
     Ok(InferOk { goals, value: (adj, target) })
 }
 
@@ -109,9 +110,9 @@ impl CoerceMany {
     ///    coerce both to function pointers;
     ///  - if we were concerned with lifetime subtyping, we'd need to look for a
     ///    least upper bound.
-    pub(super) fn coerce(
+    pub(super) fn coerce<'db>(
         &mut self,
-        ctx: &mut InferenceContext<'_>,
+        ctx: &mut InferenceContext<'db>,
         expr: Option<ExprId>,
         expr_ty: &Ty,
         cause: CoercionCause,
@@ -278,7 +279,7 @@ impl InferenceContext<'_> {
     }
 }
 
-impl InferenceTable<'_> {
+impl<'db> InferenceTable<'db> {
     /// Unify two types, but may coerce the first one to the second one
     /// using "implicit coercion rules" if needed.
     pub(crate) fn coerce(
@@ -287,8 +288,8 @@ impl InferenceTable<'_> {
         to_ty: &Ty,
         coerce_never: CoerceNever,
     ) -> Result<(Vec<Adjustment>, Ty), TypeError> {
-        let from_ty = self.resolve_ty_shallow(from_ty);
-        let to_ty = self.resolve_ty_shallow(to_ty);
+        let from_ty = self.structurally_resolve_type(from_ty);
+        let to_ty = self.structurally_resolve_type(to_ty);
         match self.coerce_inner(from_ty, &to_ty, coerce_never) {
             Ok(InferOk { value: (adjustments, ty), goals }) => {
                 self.register_infer_ok(InferOk { value: (), goals });
@@ -301,10 +302,15 @@ impl InferenceTable<'_> {
         }
     }
 
-    fn coerce_inner(&mut self, from_ty: Ty, to_ty: &Ty, coerce_never: CoerceNever) -> CoerceResult {
+    fn coerce_inner(
+        &mut self,
+        from_ty: Ty,
+        to_ty: &Ty,
+        coerce_never: CoerceNever,
+    ) -> CoerceResult<'db> {
         if from_ty.is_never() {
             if let TyKind::InferenceVar(tv, TyVariableKind::General) = to_ty.kind(Interner) {
-                self.set_diverging(*tv, true);
+                self.set_diverging(*tv, TyVariableKind::General);
             }
             if coerce_never == CoerceNever::Yes {
                 // Subtle: If we are coercing from `!` to `?T`, where `?T` is an unbound
@@ -372,7 +378,7 @@ impl InferenceTable<'_> {
     }
 
     /// Unify two types (using sub or lub) and produce a specific coercion.
-    fn unify_and<F>(&mut self, t1: &Ty, t2: &Ty, f: F) -> CoerceResult
+    fn unify_and<F>(&mut self, t1: &Ty, t2: &Ty, f: F) -> CoerceResult<'db>
     where
         F: FnOnce(Ty) -> Vec<Adjustment>,
     {
@@ -380,7 +386,7 @@ impl InferenceTable<'_> {
             .and_then(|InferOk { goals, .. }| success(f(t1.clone()), t1.clone(), goals))
     }
 
-    fn coerce_ptr(&mut self, from_ty: Ty, to_ty: &Ty, to_mt: Mutability) -> CoerceResult {
+    fn coerce_ptr(&mut self, from_ty: Ty, to_ty: &Ty, to_mt: Mutability) -> CoerceResult<'db> {
         let (is_ref, from_mt, from_inner) = match from_ty.kind(Interner) {
             TyKind::Ref(mt, _, ty) => (true, mt, ty),
             TyKind::Raw(mt, ty) => (false, mt, ty),
@@ -422,7 +428,7 @@ impl InferenceTable<'_> {
         to_ty: &Ty,
         to_mt: Mutability,
         to_lt: &Lifetime,
-    ) -> CoerceResult {
+    ) -> CoerceResult<'db> {
         let (_from_lt, from_mt) = match from_ty.kind(Interner) {
             TyKind::Ref(mt, lt, _) => {
                 coerce_mutabilities(*mt, to_mt)?;
@@ -526,7 +532,7 @@ impl InferenceTable<'_> {
     }
 
     /// Attempts to coerce from the type of a Rust function item into a function pointer.
-    fn coerce_from_fn_item(&mut self, from_ty: Ty, to_ty: &Ty) -> CoerceResult {
+    fn coerce_from_fn_item(&mut self, from_ty: Ty, to_ty: &Ty) -> CoerceResult<'db> {
         match to_ty.kind(Interner) {
             TyKind::Function(_) => {
                 let from_sig = from_ty.callable_sig(self.db).expect("FnDef had no sig");
@@ -568,7 +574,7 @@ impl InferenceTable<'_> {
         from_ty: Ty,
         from_f: &FnPointer,
         to_ty: &Ty,
-    ) -> CoerceResult {
+    ) -> CoerceResult<'db> {
         self.coerce_from_safe_fn(
             from_ty,
             from_f,
@@ -585,7 +591,7 @@ impl InferenceTable<'_> {
         to_ty: &Ty,
         to_unsafe: F,
         normal: G,
-    ) -> CoerceResult
+    ) -> CoerceResult<'db>
     where
         F: FnOnce(Ty) -> Vec<Adjustment>,
         G: FnOnce(Ty) -> Vec<Adjustment>,
@@ -608,7 +614,7 @@ impl InferenceTable<'_> {
         from_ty: Ty,
         from_substs: &Substitution,
         to_ty: &Ty,
-    ) -> CoerceResult {
+    ) -> CoerceResult<'db> {
         match to_ty.kind(Interner) {
             // if from_substs is non-capturing (FIXME)
             TyKind::Function(fn_ty) => {
@@ -633,7 +639,7 @@ impl InferenceTable<'_> {
     /// Coerce a type using `from_ty: CoerceUnsized<ty_ty>`
     ///
     /// See: <https://doc.rust-lang.org/nightly/std/marker/trait.CoerceUnsized.html>
-    fn try_coerce_unsized(&mut self, from_ty: &Ty, to_ty: &Ty) -> CoerceResult {
+    fn try_coerce_unsized(&mut self, from_ty: &Ty, to_ty: &Ty) -> CoerceResult<'db> {
         // These 'if' statements require some explanation.
         // The `CoerceUnsized` trait is special - it is only
         // possible to write `impl CoerceUnsized<B> for A` where
@@ -707,41 +713,12 @@ impl InferenceTable<'_> {
             b.push(coerce_from).push(to_ty.clone()).build()
         };
 
-        let goal: InEnvironment<DomainGoal> =
-            InEnvironment::new(&self.trait_env.env, coerce_unsized_tref.cast(Interner));
-
-        let canonicalized = self.canonicalize_with_free_vars(goal);
-
-        // FIXME: rustc's coerce_unsized is more specialized -- it only tries to
-        // solve `CoerceUnsized` and `Unsize` goals at this point and leaves the
-        // rest for later. Also, there's some logic about sized type variables.
-        // Need to find out in what cases this is necessary
-        let solution = self.db.trait_solve(
-            krate,
-            self.trait_env.block,
-            canonicalized.value.clone().cast(Interner),
-        );
-
-        match solution {
-            // FIXME: this is a weaker guarantee than Chalk's `Guidance::Unique`
-            // was. Chalk's unique guidance at least guarantees that the real solution
-            // is some "subset" of the solutions matching the guidance, but the
-            // substs for `Certainty::No` don't have that same guarantee (I think).
-            NextTraitSolveResult::Certain(v) => {
-                canonicalized.apply_solution(
-                    self,
-                    Canonical {
-                        binders: v.binders,
-                        // FIXME handle constraints
-                        value: v.value.subst,
-                    },
-                );
-            }
-            // ...so, should think about how to get some actually get some guidance here
-            NextTraitSolveResult::Uncertain(..) | NextTraitSolveResult::NoSolution => {
-                return Err(TypeError);
-            }
-        }
+        let goal: Goal = coerce_unsized_tref.cast(Interner);
+
+        self.commit_if_ok(|table| match table.solve_obligation(goal) {
+            Ok(Certainty::Yes) => Ok(()),
+            _ => Err(TypeError),
+        })?;
 
         let unsize =
             Adjustment { kind: Adjust::Pointer(PointerCast::Unsize), target: to_ty.clone() };
diff --git a/crates/hir-ty/src/infer/expr.rs b/crates/hir-ty/src/infer/expr.rs
index 261c02386822..bfeb5bae851a 100644
--- a/crates/hir-ty/src/infer/expr.rs
+++ b/crates/hir-ty/src/infer/expr.rs
@@ -24,8 +24,8 @@ use syntax::ast::RangeOp;
 
 use crate::{
     Adjust, Adjustment, AdtId, AutoBorrow, Binders, CallableDefId, CallableSig, DeclContext,
-    DeclOrigin, IncorrectGenericsLenKind, Interner, Rawness, Scalar, Substitution,
-    TraitEnvironment, TraitRef, Ty, TyBuilder, TyExt, TyKind,
+    DeclOrigin, IncorrectGenericsLenKind, Interner, LifetimeElisionKind, Rawness, Scalar,
+    Substitution, TraitEnvironment, TraitRef, Ty, TyBuilder, TyExt, TyKind,
     autoderef::{Autoderef, builtin_deref, deref_by_trait},
     consteval,
     generics::generics,
@@ -37,11 +37,12 @@ use crate::{
     },
     lang_items::lang_items_for_bin_op,
     lower::{
-        LifetimeElisionKind, ParamLoweringMode, lower_to_chalk_mutability,
+        ParamLoweringMode, lower_to_chalk_mutability,
         path::{GenericArgsLowerer, TypeLikeConst, substs_from_args_and_bindings},
     },
     mapping::{ToChalk, from_chalk},
     method_resolution::{self, VisibleFromModule},
+    next_solver::mapping::ChalkToNextSolver,
     primitive::{self, UintTy},
     static_lifetime, to_chalk_trait_id,
     traits::FnTrait,
@@ -402,7 +403,7 @@ impl InferenceContext<'_> {
                     let matchee_diverges = mem::replace(&mut self.diverges, Diverges::Maybe);
                     let mut all_arms_diverge = Diverges::Always;
                     for arm in arms.iter() {
-                        let input_ty = self.resolve_ty_shallow(&input_ty);
+                        let input_ty = self.table.structurally_resolve_type(&input_ty);
                         self.infer_top_pat(arm.pat, &input_ty, None);
                     }
 
@@ -652,7 +653,7 @@ impl InferenceContext<'_> {
             &Expr::Box { expr } => self.infer_expr_box(expr, expected),
             Expr::UnaryOp { expr, op } => {
                 let inner_ty = self.infer_expr_inner(*expr, &Expectation::none(), ExprIsRead::Yes);
-                let inner_ty = self.resolve_ty_shallow(&inner_ty);
+                let inner_ty = self.table.structurally_resolve_type(&inner_ty);
                 // FIXME: Note down method resolution her
                 match op {
                     UnaryOp::Deref => {
@@ -670,7 +671,7 @@ impl InferenceContext<'_> {
                             );
                         }
                         if let Some(derefed) = builtin_deref(self.table.db, &inner_ty, true) {
-                            self.resolve_ty_shallow(derefed)
+                            self.table.structurally_resolve_type(derefed)
                         } else {
                             deref_by_trait(&mut self.table, inner_ty, false)
                                 .unwrap_or_else(|| self.err_ty())
@@ -826,10 +827,10 @@ impl InferenceContext<'_> {
                 let index_ty = self.infer_expr(*index, &Expectation::none(), ExprIsRead::Yes);
 
                 if let Some(index_trait) = self.resolve_lang_trait(LangItem::Index) {
-                    let canonicalized = self.canonicalize(base_ty.clone());
+                    let canonicalized =
+                        self.canonicalize(base_ty.clone().to_nextsolver(self.table.interner));
                     let receiver_adjustments = method_resolution::resolve_indexing_op(
-                        self.db,
-                        self.table.trait_env.clone(),
+                        &mut self.table,
                         canonicalized,
                         index_trait,
                     );
@@ -932,6 +933,7 @@ impl InferenceContext<'_> {
                     }
                     None => {
                         let expected_ty = expected.to_option(&mut self.table);
+                        tracing::debug!(?expected_ty);
                         let opt_ty = match expected_ty.as_ref().map(|it| it.kind(Interner)) {
                             Some(TyKind::Scalar(Scalar::Int(_) | Scalar::Uint(_))) => expected_ty,
                             Some(TyKind::Scalar(Scalar::Char)) => {
@@ -1001,7 +1003,7 @@ impl InferenceContext<'_> {
                     // allows them to be inferred based on how they are used later in the
                     // function.
                     if is_input {
-                        let ty = this.resolve_ty_shallow(&ty);
+                        let ty = this.table.structurally_resolve_type(&ty);
                         match ty.kind(Interner) {
                             TyKind::FnDef(def, parameters) => {
                                 let fnptr_ty = TyKind::Function(
@@ -1423,9 +1425,10 @@ impl InferenceContext<'_> {
             // use knowledge of built-in binary ops, which can sometimes help inference
             let builtin_ret = self.enforce_builtin_binop_types(&lhs_ty, &rhs_ty, op);
             self.unify(&builtin_ret, &ret_ty);
+            builtin_ret
+        } else {
+            ret_ty
         }
-
-        ret_ty
     }
 
     fn infer_block(
@@ -1678,7 +1681,8 @@ impl InferenceContext<'_> {
             None => {
                 // no field found, lets attempt to resolve it like a function so that IDE things
                 // work out while people are typing
-                let canonicalized_receiver = self.canonicalize(receiver_ty.clone());
+                let canonicalized_receiver =
+                    self.canonicalize(receiver_ty.clone().to_nextsolver(self.table.interner));
                 let resolved = method_resolution::lookup_method(
                     self.db,
                     &canonicalized_receiver,
@@ -1824,7 +1828,8 @@ impl InferenceContext<'_> {
         expected: &Expectation,
     ) -> Ty {
         let receiver_ty = self.infer_expr_inner(receiver, &Expectation::none(), ExprIsRead::Yes);
-        let canonicalized_receiver = self.canonicalize(receiver_ty.clone());
+        let canonicalized_receiver =
+            self.canonicalize(receiver_ty.clone().to_nextsolver(self.table.interner));
 
         let resolved = method_resolution::lookup_method(
             self.db,
@@ -2234,7 +2239,7 @@ impl InferenceContext<'_> {
     }
 
     fn register_obligations_for_call(&mut self, callable_ty: &Ty) {
-        let callable_ty = self.resolve_ty_shallow(callable_ty);
+        let callable_ty = self.table.structurally_resolve_type(callable_ty);
         if let TyKind::FnDef(fn_def, parameters) = callable_ty.kind(Interner) {
             let def: CallableDefId = from_chalk(self.db, *fn_def);
             let generic_predicates =
@@ -2323,9 +2328,9 @@ impl InferenceContext<'_> {
 
     /// Dereferences a single level of immutable referencing.
     fn deref_ty_if_possible(&mut self, ty: &Ty) -> Ty {
-        let ty = self.resolve_ty_shallow(ty);
+        let ty = self.table.structurally_resolve_type(ty);
         match ty.kind(Interner) {
-            TyKind::Ref(Mutability::Not, _, inner) => self.resolve_ty_shallow(inner),
+            TyKind::Ref(Mutability::Not, _, inner) => self.table.structurally_resolve_type(inner),
             _ => ty,
         }
     }
diff --git a/crates/hir-ty/src/infer/pat.rs b/crates/hir-ty/src/infer/pat.rs
index 707bec0fce4c..16489e3068f3 100644
--- a/crates/hir-ty/src/infer/pat.rs
+++ b/crates/hir-ty/src/infer/pat.rs
@@ -190,7 +190,7 @@ impl InferenceContext<'_> {
         subs: &[PatId],
         decl: Option<DeclContext>,
     ) -> Ty {
-        let expected = self.resolve_ty_shallow(expected);
+        let expected = self.table.structurally_resolve_type(expected);
         let expectations = match expected.as_tuple() {
             Some(parameters) => parameters.as_slice(Interner),
             _ => &[],
@@ -238,7 +238,7 @@ impl InferenceContext<'_> {
         mut default_bm: BindingMode,
         decl: Option<DeclContext>,
     ) -> Ty {
-        let mut expected = self.resolve_ty_shallow(expected);
+        let mut expected = self.table.structurally_resolve_type(expected);
 
         if matches!(&self.body[pat], Pat::Ref { .. }) || self.inside_assignment {
             cov_mark::hit!(match_ergonomics_ref);
@@ -251,7 +251,7 @@ impl InferenceContext<'_> {
             let mut pat_adjustments = Vec::new();
             while let Some((inner, _lifetime, mutability)) = expected.as_reference() {
                 pat_adjustments.push(expected.clone());
-                expected = self.resolve_ty_shallow(inner);
+                expected = self.table.structurally_resolve_type(inner);
                 default_bm = match default_bm {
                     BindingMode::Move => BindingMode::Ref(mutability),
                     BindingMode::Ref(Mutability::Not) => BindingMode::Ref(Mutability::Not),
@@ -494,7 +494,7 @@ impl InferenceContext<'_> {
         default_bm: BindingMode,
         decl: Option<DeclContext>,
     ) -> Ty {
-        let expected = self.resolve_ty_shallow(expected);
+        let expected = self.table.structurally_resolve_type(expected);
 
         // If `expected` is an infer ty, we try to equate it to an array if the given pattern
         // allows it. See issue #16609
@@ -506,7 +506,7 @@ impl InferenceContext<'_> {
             self.unify(&expected, &resolved_array_ty);
         }
 
-        let expected = self.resolve_ty_shallow(&expected);
+        let expected = self.table.structurally_resolve_type(&expected);
         let elem_ty = match expected.kind(Interner) {
             TyKind::Array(st, _) | TyKind::Slice(st) => st.clone(),
             _ => self.err_ty(),
@@ -542,7 +542,7 @@ impl InferenceContext<'_> {
         if let Expr::Literal(Literal::ByteString(_)) = self.body[expr]
             && let Some((inner, ..)) = expected.as_reference()
         {
-            let inner = self.resolve_ty_shallow(inner);
+            let inner = self.table.structurally_resolve_type(inner);
             if matches!(inner.kind(Interner), TyKind::Slice(_)) {
                 let elem_ty = TyKind::Scalar(Scalar::Uint(UintTy::U8)).intern(Interner);
                 let slice_ty = TyKind::Slice(elem_ty).intern(Interner);
diff --git a/crates/hir-ty/src/infer/path.rs b/crates/hir-ty/src/infer/path.rs
index bc8648ecdd94..1f62f9c4aa11 100644
--- a/crates/hir-ty/src/infer/path.rs
+++ b/crates/hir-ty/src/infer/path.rs
@@ -10,14 +10,14 @@ use hir_expand::name::Name;
 use stdx::never;
 
 use crate::{
-    InferenceDiagnostic, Interner, Substitution, TraitRef, TraitRefExt, Ty, TyBuilder, TyExt,
-    TyKind, ValueTyDefId,
+    InferenceDiagnostic, Interner, LifetimeElisionKind, Substitution, TraitRef, TraitRefExt, Ty,
+    TyBuilder, TyExt, TyKind, ValueTyDefId,
     builder::ParamKind,
     consteval, error_lifetime,
     generics::generics,
     infer::diagnostics::InferenceTyLoweringContext as TyLoweringContext,
-    lower::LifetimeElisionKind,
     method_resolution::{self, VisibleFromModule},
+    next_solver::mapping::ChalkToNextSolver,
     to_chalk_trait_id,
 };
 
@@ -322,7 +322,7 @@ impl InferenceContext<'_> {
             return Some(result);
         }
 
-        let canonical_ty = self.canonicalize(ty.clone());
+        let canonical_ty = self.canonicalize(ty.clone().to_nextsolver(self.table.interner));
 
         let mut not_visible = None;
         let res = method_resolution::iterate_method_candidates(
@@ -392,7 +392,7 @@ impl InferenceContext<'_> {
         name: &Name,
         id: ExprOrPatId,
     ) -> Option<(ValueNs, Substitution)> {
-        let ty = self.resolve_ty_shallow(ty);
+        let ty = self.table.structurally_resolve_type(ty);
         let (enum_id, subst) = match ty.as_adt() {
             Some((AdtId::EnumId(e), subst)) => (e, subst),
             _ => return None,
diff --git a/crates/hir-ty/src/infer/unify.rs b/crates/hir-ty/src/infer/unify.rs
index bb4782bd4194..ec4b7ee85dc6 100644
--- a/crates/hir-ty/src/infer/unify.rs
+++ b/crates/hir-ty/src/infer/unify.rs
@@ -3,16 +3,21 @@
 use std::{fmt, mem};
 
 use chalk_ir::{
-    CanonicalVarKind, FloatTy, IntTy, TyVariableKind, UniverseIndex, cast::Cast,
-    fold::TypeFoldable, interner::HasInterner, zip::Zip,
+    CanonicalVarKind, FloatTy, IntTy, TyVariableKind, cast::Cast, fold::TypeFoldable,
+    interner::HasInterner,
 };
-use chalk_solve::infer::ParameterEnaVariableExt;
 use either::Either;
-use ena::unify::UnifyKey;
 use hir_def::{AdtId, lang_item::LangItem};
 use hir_expand::name::Name;
 use intern::sym;
-use rustc_hash::FxHashMap;
+use rustc_hash::{FxHashMap, FxHashSet};
+use rustc_next_trait_solver::solve::HasChanged;
+use rustc_type_ir::{
+    AliasRelationDirection, FloatVid, IntVid, TyVid,
+    inherent::{Span, Term as _},
+    relate::{Relate, solver_relating::RelateExt},
+    solve::{Certainty, NoSolution},
+};
 use smallvec::SmallVec;
 use triomphe::Arc;
 
@@ -24,14 +29,25 @@ use crate::{
     TraitRef, Ty, TyBuilder, TyExt, TyKind, VariableKind, WhereClause,
     consteval::unknown_const,
     db::HirDatabase,
-    fold_generic_args, fold_tys_and_consts, to_chalk_trait_id,
-    traits::{FnTrait, NextTraitSolveResult},
+    fold_generic_args, fold_tys_and_consts,
+    next_solver::{
+        self, Binder, DbInterner, ParamEnvAnd, Predicate, PredicateKind, SolverDefIds, Term,
+        infer::{
+            DbInternerInferExt, InferCtxt, canonical::canonicalizer::OriginalQueryValues,
+            snapshot::CombinedSnapshot,
+        },
+        mapping::{ChalkToNextSolver, InferenceVarExt, NextSolverToChalk},
+    },
+    to_chalk_trait_id,
+    traits::{
+        FnTrait, NextTraitSolveResult, next_trait_solve_canonical_in_ctxt, next_trait_solve_in_ctxt,
+    },
 };
 
-impl InferenceContext<'_> {
-    pub(super) fn canonicalize<T>(&mut self, t: T) -> Canonical<T>
+impl<'db> InferenceContext<'db> {
+    pub(super) fn canonicalize<T>(&mut self, t: T) -> rustc_type_ir::Canonical<DbInterner<'db>, T>
     where
-        T: TypeFoldable<Interner> + HasInterner<Interner = Interner>,
+        T: rustc_type_ir::TypeFoldable<DbInterner<'db>>,
     {
         self.table.canonicalize(t)
     }
@@ -42,11 +58,11 @@ impl InferenceContext<'_> {
     ) -> SmallVec<[WhereClause; 4]> {
         self.table.resolve_obligations_as_possible();
 
-        let root = self.table.var_unification_table.inference_var_root(self_ty);
+        let root = InferenceVar::from_vid(self.table.infer_ctxt.root_var(self_ty.to_vid()));
         let pending_obligations = mem::take(&mut self.table.pending_obligations);
         let obligations = pending_obligations
             .iter()
-            .filter_map(|obligation| match obligation.value.value.goal.data(Interner) {
+            .filter_map(|obligation| match obligation.to_chalk(self.table.interner).goal.data(Interner) {
                 GoalData::DomainGoal(DomainGoal::Holds(clause)) => {
                     let ty = match clause {
                         WhereClause::AliasEq(AliasEq {
@@ -59,18 +75,9 @@ impl InferenceContext<'_> {
                         WhereClause::TypeOutlives(to) => to.ty.clone(),
                         _ => return None,
                     };
-
-                    let uncanonical =
-                        chalk_ir::Substitute::apply(&obligation.free_vars, ty, Interner);
-                    if matches!(
-                        self.resolve_ty_shallow(&uncanonical).kind(Interner),
-                        TyKind::InferenceVar(iv, TyVariableKind::General) if *iv == root,
-                    ) {
-                        Some(chalk_ir::Substitute::apply(
-                            &obligation.free_vars,
-                            clause.clone(),
-                            Interner,
-                        ))
+                    let ty = self.resolve_ty_shallow(&ty);
+                    if matches!(ty.kind(Interner), TyKind::InferenceVar(iv, TyVariableKind::General) if *iv == root) {
+                        Some(clause.clone())
                     } else {
                         None
                     }
@@ -84,51 +91,6 @@ impl InferenceContext<'_> {
     }
 }
 
-#[derive(Debug, Clone)]
-pub(crate) struct Canonicalized<T>
-where
-    T: HasInterner<Interner = Interner>,
-{
-    pub(crate) value: Canonical<T>,
-    free_vars: Vec<GenericArg>,
-}
-
-impl<T: HasInterner<Interner = Interner>> Canonicalized<T> {
-    pub(crate) fn apply_solution(
-        &self,
-        ctx: &mut InferenceTable<'_>,
-        solution: Canonical<Substitution>,
-    ) {
-        // the solution may contain new variables, which we need to convert to new inference vars
-        let new_vars = Substitution::from_iter(
-            Interner,
-            solution.binders.iter(Interner).map(|k| match &k.kind {
-                VariableKind::Ty(TyVariableKind::General) => ctx.new_type_var().cast(Interner),
-                VariableKind::Ty(TyVariableKind::Integer) => ctx.new_integer_var().cast(Interner),
-                VariableKind::Ty(TyVariableKind::Float) => ctx.new_float_var().cast(Interner),
-                // Chalk can sometimes return new lifetime variables. We just replace them by errors
-                // for now.
-                VariableKind::Lifetime => ctx.new_lifetime_var().cast(Interner),
-                VariableKind::Const(ty) => ctx.new_const_var(ty.clone()).cast(Interner),
-            }),
-        );
-        for (i, v) in solution.value.iter(Interner).enumerate() {
-            let var = &self.free_vars[i];
-            if let Some(ty) = v.ty(Interner) {
-                // eagerly replace projections in the type; we may be getting types
-                // e.g. from where clauses where this hasn't happened yet
-                let ty = ctx.normalize_associated_types_in(new_vars.apply(ty.clone(), Interner));
-                tracing::debug!("unifying {:?} {:?}", var, ty);
-                ctx.unify(var.assert_ty_ref(Interner), &ty);
-            } else {
-                let v = new_vars.apply(v.clone(), Interner);
-                tracing::debug!("try_unifying {:?} {:?}", var, v);
-                let _ = ctx.try_unify(var, &v);
-            }
-        }
-    }
-}
-
 /// Check if types unify.
 ///
 /// Note that we consider placeholder types to unify with everything.
@@ -224,37 +186,36 @@ bitflags::bitflags! {
     }
 }
 
-type ChalkInferenceTable = chalk_solve::infer::InferenceTable<Interner>;
-
 #[derive(Clone)]
 pub(crate) struct InferenceTable<'a> {
     pub(crate) db: &'a dyn HirDatabase,
+    pub(crate) interner: DbInterner<'a>,
     pub(crate) trait_env: Arc<TraitEnvironment>,
     pub(crate) tait_coercion_table: Option<FxHashMap<OpaqueTyId, Ty>>,
-    var_unification_table: ChalkInferenceTable,
-    type_variable_table: SmallVec<[TypeVariableFlags; 16]>,
-    pending_obligations: Vec<Canonicalized<InEnvironment<Goal>>>,
-    /// Double buffer used in [`Self::resolve_obligations_as_possible`] to cut down on
-    /// temporary allocations.
-    resolve_obligations_buffer: Vec<Canonicalized<InEnvironment<Goal>>>,
+    pub(crate) infer_ctxt: InferCtxt<'a>,
+    diverging_tys: FxHashSet<Ty>,
+    pending_obligations: Vec<next_solver::Goal<'a, next_solver::Predicate<'a>>>,
 }
 
-pub(crate) struct InferenceTableSnapshot {
-    var_table_snapshot: chalk_solve::infer::InferenceSnapshot<Interner>,
-    type_variable_table: SmallVec<[TypeVariableFlags; 16]>,
-    pending_obligations: Vec<Canonicalized<InEnvironment<Goal>>>,
+pub(crate) struct InferenceTableSnapshot<'a> {
+    ctxt_snapshot: CombinedSnapshot,
+    diverging_tys: FxHashSet<Ty>,
+    pending_obligations: Vec<next_solver::Goal<'a, next_solver::Predicate<'a>>>,
 }
 
 impl<'a> InferenceTable<'a> {
     pub(crate) fn new(db: &'a dyn HirDatabase, trait_env: Arc<TraitEnvironment>) -> Self {
+        let interner = DbInterner::new_with(db, Some(trait_env.krate), trait_env.block);
         InferenceTable {
             db,
+            interner,
             trait_env,
             tait_coercion_table: None,
-            var_unification_table: ChalkInferenceTable::new(),
-            type_variable_table: SmallVec::new(),
+            infer_ctxt: interner.infer_ctxt().build(rustc_type_ir::TypingMode::Analysis {
+                defining_opaque_types_and_generators: SolverDefIds::new_from_iter(interner, []),
+            }),
+            diverging_tys: FxHashSet::default(),
             pending_obligations: Vec::new(),
-            resolve_obligations_buffer: Vec::new(),
         }
     }
 
@@ -265,29 +226,58 @@ impl<'a> InferenceTable<'a> {
     /// marked as diverging if necessary, so that resolving them gives the right
     /// result.
     pub(super) fn propagate_diverging_flag(&mut self) {
-        for i in 0..self.type_variable_table.len() {
-            if !self.type_variable_table[i].contains(TypeVariableFlags::DIVERGING) {
-                continue;
+        let mut new_tys = FxHashSet::default();
+        for ty in self.diverging_tys.iter() {
+            match ty.kind(Interner) {
+                TyKind::InferenceVar(var, kind) => match kind {
+                    TyVariableKind::General => {
+                        let root = InferenceVar::from(
+                            self.infer_ctxt.root_var(TyVid::from_u32(var.index())).as_u32(),
+                        );
+                        if root.index() != var.index() {
+                            new_tys.insert(TyKind::InferenceVar(root, *kind).intern(Interner));
+                        }
+                    }
+                    TyVariableKind::Integer => {
+                        let root = InferenceVar::from(
+                            self.infer_ctxt
+                                .inner
+                                .borrow_mut()
+                                .int_unification_table()
+                                .find(IntVid::from_usize(var.index() as usize))
+                                .as_u32(),
+                        );
+                        if root.index() != var.index() {
+                            new_tys.insert(TyKind::InferenceVar(root, *kind).intern(Interner));
+                        }
+                    }
+                    TyVariableKind::Float => {
+                        let root = InferenceVar::from(
+                            self.infer_ctxt
+                                .inner
+                                .borrow_mut()
+                                .float_unification_table()
+                                .find(FloatVid::from_usize(var.index() as usize))
+                                .as_u32(),
+                        );
+                        if root.index() != var.index() {
+                            new_tys.insert(TyKind::InferenceVar(root, *kind).intern(Interner));
+                        }
+                    }
+                },
+                _ => {}
             }
-            let v = InferenceVar::from(i as u32);
-            let root = self.var_unification_table.inference_var_root(v);
-            self.modify_type_variable_flag(root, |f| {
-                *f |= TypeVariableFlags::DIVERGING;
-            });
         }
+        self.diverging_tys.extend(new_tys);
     }
 
-    pub(super) fn set_diverging(&mut self, iv: InferenceVar, diverging: bool) {
-        self.modify_type_variable_flag(iv, |f| {
-            f.set(TypeVariableFlags::DIVERGING, diverging);
-        });
+    pub(super) fn set_diverging(&mut self, iv: InferenceVar, kind: TyVariableKind) {
+        self.diverging_tys.insert(TyKind::InferenceVar(iv, kind).intern(Interner));
     }
 
     fn fallback_value(&self, iv: InferenceVar, kind: TyVariableKind) -> Ty {
-        let is_diverging = self
-            .type_variable_table
-            .get(iv.index() as usize)
-            .is_some_and(|data| data.contains(TypeVariableFlags::DIVERGING));
+        let is_diverging =
+            self.diverging_tys.contains(&TyKind::InferenceVar(iv, kind).intern(Interner));
         if is_diverging {
             return TyKind::Never.intern(Interner);
         }
@@ -299,30 +289,14 @@ impl<'a> InferenceTable<'a> {
         .intern(Interner)
     }
 
-    pub(crate) fn canonicalize_with_free_vars<T>(&mut self, t: T) -> Canonicalized<T>
-    where
-        T: TypeFoldable<Interner> + HasInterner<Interner = Interner>,
-    {
-        // try to resolve obligations before canonicalizing, since this might
-        // result in new knowledge about variables
-        self.resolve_obligations_as_possible();
-        let result = self.var_unification_table.canonicalize(Interner, t);
-        let free_vars = result
-            .free_vars
-            .into_iter()
-            .map(|free_var| free_var.to_generic_arg(Interner))
-            .collect();
-        Canonicalized { value: result.quantified, free_vars }
-    }
-
-    pub(crate) fn canonicalize<T>(&mut self, t: T) -> Canonical<T>
+    pub(crate) fn canonicalize<T>(&mut self, t: T) -> rustc_type_ir::Canonical<DbInterner<'a>, T>
     where
-        T: TypeFoldable<Interner> + HasInterner<Interner = Interner>,
+        T: rustc_type_ir::TypeFoldable<DbInterner<'a>>,
     {
         // try to resolve obligations before canonicalizing, since this might
         // result in new knowledge about variables
         self.resolve_obligations_as_possible();
-        self.var_unification_table.canonicalize(Interner, t).quantified
+        self.infer_ctxt.canonicalize_response(t)
     }
 
     /// Recurses through the given type, normalizing associated types mentioned
@@ -348,6 +322,7 @@ impl<'a> InferenceTable<'a> {
                             self.resolve_ty_shallow(&ty)
                         }
                         TyKind::AssociatedType(id, subst) => {
+                            // return Either::Left(self.resolve_ty_shallow(&ty));
                             if ty.data(Interner).flags.intersects(
                                 chalk_ir::TypeFlags::HAS_TY_INFER
                                     | chalk_ir::TypeFlags::HAS_CT_INFER,
@@ -370,49 +345,45 @@ impl<'a> InferenceTable<'a> {
                                 )),
                             );
                             let in_env = InEnvironment::new(&self.trait_env.env, goal);
+                            let goal = in_env.to_nextsolver(self.interner);
+                            let goal =
+                                ParamEnvAnd { param_env: goal.param_env, value: goal.predicate };
 
-                            let canonicalized = {
+                            let (canonical_goal, orig_values) = {
+                                let mut orig_values = OriginalQueryValues::default();
                                 let result =
-                                    self.var_unification_table.canonicalize(Interner, in_env);
-                                let free_vars = result
-                                    .free_vars
-                                    .into_iter()
-                                    .map(|free_var| free_var.to_generic_arg(Interner))
-                                    .collect();
-                                Canonicalized { value: result.quantified, free_vars }
+                                    self.infer_ctxt.canonicalize_query(goal, &mut orig_values);
+                                (result.canonical, orig_values)
+                            };
+                            let canonical_goal = rustc_type_ir::Canonical {
+                                max_universe: canonical_goal.max_universe,
+                                variables: canonical_goal.variables,
+                                value: crate::next_solver::Goal {
+                                    param_env: canonical_goal.value.param_env,
+                                    predicate: canonical_goal.value.value,
+                                },
                             };
-                            let solution = self.db.trait_solve(
-                                self.trait_env.krate,
-                                self.trait_env.block,
-                                canonicalized.value.clone(),
+                            let solution = next_trait_solve_canonical_in_ctxt(
+                                &self.infer_ctxt,
+                                canonical_goal,
                             );
                             if let NextTraitSolveResult::Certain(canonical_subst) = solution {
-                                // This is not great :) But let's just assert this for now and come back to it later.
-                                if canonical_subst.value.subst.len(Interner) != 1 {
+                                let subst = self.instantiate_canonical(canonical_subst).subst;
+                                if subst.len(Interner) != orig_values.var_values.len() {
                                     ty
                                 } else {
-                                    let normalized = canonical_subst.value.subst.as_slice(Interner)
-                                        [0]
-                                    .assert_ty_ref(Interner);
-                                    match normalized.kind(Interner) {
-                                        TyKind::Alias(AliasTy::Projection(proj_ty)) => {
-                                            if id == &proj_ty.associated_ty_id
-                                                && subst == &proj_ty.substitution
-                                            {
-                                                ty
-                                            } else {
-                                                normalized.clone()
-                                            }
-                                        }
-                                        TyKind::AssociatedType(new_id, new_subst) => {
-                                            if new_id == id && new_subst == subst {
-                                                ty
+                                    let target_ty = var.to_nextsolver(self.interner);
+                                    subst
+                                        .iter(Interner)
+                                        .zip(orig_values.var_values.iter())
+                                        .find_map(|(new, orig)| {
+                                            if orig.ty() == Some(target_ty) {
+                                                Some(new.assert_ty_ref(Interner).clone())
                                             } else {
-                                                normalized.clone()
+                                                None
                                             }
-                                        }
-                                        _ => normalized.clone(),
-                                    }
+                                        })
+                                        .unwrap_or(ty)
                                 }
                             } else {
                                 ty
@@ -507,43 +478,32 @@ impl<'a> InferenceTable<'a> {
     pub(crate) fn normalize_projection_ty(&mut self, proj_ty: ProjectionTy) -> Ty {
         let var = self.new_type_var();
         let alias_eq = AliasEq { alias: AliasTy::Projection(proj_ty), ty: var.clone() };
-        let obligation = alias_eq.cast(Interner);
-        self.register_obligation(obligation);
+        let obligation: Goal = alias_eq.cast(Interner);
+        self.register_obligation(obligation.to_nextsolver(self.interner));
         var
     }
 
-    fn modify_type_variable_flag<F>(&mut self, var: InferenceVar, cb: F)
-    where
-        F: FnOnce(&mut TypeVariableFlags),
-    {
-        let idx = var.index() as usize;
-        if self.type_variable_table.len() <= idx {
-            self.extend_type_variable_table(idx);
-        }
-        if let Some(f) = self.type_variable_table.get_mut(idx) {
-            cb(f);
-        }
-    }
-    fn extend_type_variable_table(&mut self, to_index: usize) {
-        let count = to_index - self.type_variable_table.len() + 1;
-        self.type_variable_table.extend(std::iter::repeat_n(TypeVariableFlags::default(), count));
-    }
-
     fn new_var(&mut self, kind: TyVariableKind, diverging: bool) -> Ty {
-        let var = self.var_unification_table.new_variable(UniverseIndex::ROOT);
-        // Chalk might have created some type variables for its own purposes that we don't know about...
-        self.extend_type_variable_table(var.index() as usize);
-        assert_eq!(var.index() as usize, self.type_variable_table.len() - 1);
-        let flags = self.type_variable_table.get_mut(var.index() as usize).unwrap();
+        let var = match kind {
+            TyVariableKind::General => {
+                let var = self.infer_ctxt.next_ty_vid();
+                InferenceVar::from(var.as_u32())
+            }
+            TyVariableKind::Integer => {
+                let var = self.infer_ctxt.next_int_vid();
+                InferenceVar::from(var.as_u32())
+            }
+            TyVariableKind::Float => {
+                let var = self.infer_ctxt.next_float_vid();
+                InferenceVar::from(var.as_u32())
+            }
+        };
+
+        let ty = var.to_ty(Interner, kind);
         if diverging {
-            *flags |= TypeVariableFlags::DIVERGING;
-        }
-        if matches!(kind, TyVariableKind::Integer) {
-            *flags |= TypeVariableFlags::INTEGER;
-        } else if matches!(kind, TyVariableKind::Float) {
-            *flags |= TypeVariableFlags::FLOAT;
+            self.diverging_tys.insert(ty.clone());
         }
-        var.to_ty_with_kind(Interner, kind)
+        ty
     }
 
     pub(crate) fn new_type_var(&mut self) -> Ty {
@@ -563,12 +523,14 @@ impl<'a> InferenceTable<'a> {
     }
 
     pub(crate) fn new_const_var(&mut self, ty: Ty) -> Const {
-        let var = self.var_unification_table.new_variable(UniverseIndex::ROOT);
+        let var = self.infer_ctxt.next_const_vid();
+        let var = InferenceVar::from(var.as_u32());
         var.to_const(Interner, ty)
     }
 
     pub(crate) fn new_lifetime_var(&mut self) -> Lifetime {
-        let var = self.var_unification_table.new_variable(UniverseIndex::ROOT);
+        let var = self.infer_ctxt.next_region_vid();
+        let var = InferenceVar::from(var.as_u32());
         var.to_lifetime(Interner)
     }
 
@@ -580,16 +542,18 @@ impl<'a> InferenceTable<'a> {
     where
         T: HasInterner<Interner = Interner> + TypeFoldable<Interner>,
     {
-        self.resolve_with_fallback_inner(&mut Vec::new(), t, &fallback)
+        self.resolve_with_fallback_inner(t, &fallback)
     }
 
     pub(crate) fn fresh_subst(&mut self, binders: &[CanonicalVarKind<Interner>]) -> Substitution {
         Substitution::from_iter(
             Interner,
-            binders.iter().map(|kind| {
-                let param_infer_var =
-                    kind.map_ref(|&ui| self.var_unification_table.new_variable(ui));
-                param_infer_var.to_generic_arg(Interner)
+            binders.iter().map(|kind| match &kind.kind {
+                chalk_ir::VariableKind::Ty(ty_variable_kind) => {
+                    self.new_var(*ty_variable_kind, false).cast(Interner)
+                }
+                chalk_ir::VariableKind::Lifetime => self.new_lifetime_var().cast(Interner),
+                chalk_ir::VariableKind::Const(ty) => self.new_const_var(ty.clone()).cast(Interner),
             }),
         )
     }
@@ -602,15 +566,25 @@ impl<'a> InferenceTable<'a> {
         subst.apply(canonical.value, Interner)
     }
 
+    pub(crate) fn instantiate_canonical_ns<T>(
+        &mut self,
+        canonical: rustc_type_ir::Canonical<DbInterner<'a>, T>,
+    ) -> T
+    where
+        T: rustc_type_ir::TypeFoldable<DbInterner<'a>>,
+    {
+        self.infer_ctxt.instantiate_canonical(&canonical).0
+    }
+
     fn resolve_with_fallback_inner<T>(
         &mut self,
-        var_stack: &mut Vec<InferenceVar>,
         t: T,
         fallback: &dyn Fn(InferenceVar, VariableKind, GenericArg, DebruijnIndex) -> GenericArg,
     ) -> T
     where
         T: HasInterner<Interner = Interner> + TypeFoldable<Interner>,
     {
+        let var_stack = &mut vec![];
         t.fold_with(
             &mut resolve::Resolver { table: self, var_stack, fallback },
             DebruijnIndex::INNERMOST,
@@ -623,6 +597,7 @@ impl<'a> InferenceTable<'a> {
     {
         let t = self.resolve_with_fallback(t, &|_, _, d, _| d);
         let t = self.normalize_associated_types_in(t);
+        // let t = self.resolve_opaque_tys_in(t);
         // Resolve again, because maybe normalization inserted infer vars.
         self.resolve_with_fallback(t, &|_, _, d, _| d)
     }
@@ -639,29 +614,26 @@ impl<'a> InferenceTable<'a> {
         let int_fallback = TyKind::Scalar(Scalar::Int(IntTy::I32)).intern(Interner);
         let float_fallback = TyKind::Scalar(Scalar::Float(FloatTy::F64)).intern(Interner);
 
-        let scalar_vars: Vec<_> = self
-            .type_variable_table
-            .iter()
-            .enumerate()
-            .filter_map(|(index, flags)| {
-                let kind = if flags.contains(TypeVariableFlags::INTEGER) {
-                    TyVariableKind::Integer
-                } else if flags.contains(TypeVariableFlags::FLOAT) {
-                    TyVariableKind::Float
-                } else {
-                    return None;
+        let int_vars = self.infer_ctxt.inner.borrow_mut().int_unification_table().len();
+        for v in 0..int_vars {
+            let var = InferenceVar::from(v as u32).to_ty(Interner, TyVariableKind::Integer);
+            let maybe_resolved = self.resolve_ty_shallow(&var);
+            if let TyKind::InferenceVar(_, kind) = maybe_resolved.kind(Interner) {
+                // I don't think we can ever unify these vars with float vars, but keep this here for now
+                let fallback = match kind {
+                    TyVariableKind::Integer => &int_fallback,
+                    TyVariableKind::Float => &float_fallback,
+                    TyVariableKind::General => unreachable!(),
                 };
-
-                // FIXME: This is not really the nicest way to get `InferenceVar`s. Can we get them
-                // without directly constructing them from `index`?
-                let var = InferenceVar::from(index as u32).to_ty(Interner, kind);
-                Some(var)
-            })
-            .collect();
-
-        for var in scalar_vars {
+                self.unify(&var, fallback);
+            }
+        }
+        let float_vars = self.infer_ctxt.inner.borrow_mut().float_unification_table().len();
+        for v in 0..float_vars {
+            let var = InferenceVar::from(v as u32).to_ty(Interner, TyVariableKind::Float);
             let maybe_resolved = self.resolve_ty_shallow(&var);
             if let TyKind::InferenceVar(_, kind) = maybe_resolved.kind(Interner) {
+                // I don't think we can ever unify these vars with float vars, but keep this here for now
                 let fallback = match kind {
                     TyVariableKind::Integer => &int_fallback,
                     TyVariableKind::Float => &float_fallback,
@@ -673,7 +645,11 @@ impl<'a> InferenceTable<'a> {
     }
 
     /// Unify two relatable values (e.g. `Ty`) and register new trait goals that arise from that.
-    pub(crate) fn unify<T: ?Sized + Zip<Interner>>(&mut self, ty1: &T, ty2: &T) -> bool {
+    pub(crate) fn unify<T: ChalkToNextSolver<'a, U>, U: Relate<DbInterner<'a>>>(
+        &mut self,
+        ty1: &T,
+        ty2: &T,
+    ) -> bool {
         let result = match self.try_unify(ty1, ty2) {
             Ok(r) => r,
             Err(_) => return false,
@@ -683,58 +659,116 @@ impl<'a> InferenceTable<'a> {
     }
 
     /// Unify two relatable values (e.g. `Ty`) and check whether trait goals which arise from that could be fulfilled
-    pub(crate) fn unify_deeply<T: ?Sized + Zip<Interner>>(&mut self, ty1: &T, ty2: &T) -> bool {
+    pub(crate) fn unify_deeply<T: ChalkToNextSolver<'a, U>, U: Relate<DbInterner<'a>>>(
+        &mut self,
+        ty1: &T,
+        ty2: &T,
+    ) -> bool {
         let result = match self.try_unify(ty1, ty2) {
             Ok(r) => r,
             Err(_) => return false,
         };
-        result.goals.iter().all(|goal| {
-            let canonicalized = self.canonicalize_with_free_vars(goal.clone());
-            self.try_resolve_obligation(&canonicalized).certain()
+        result.goals.into_iter().all(|goal| {
+            matches!(next_trait_solve_in_ctxt(&self.infer_ctxt, goal), Ok((_, Certainty::Yes)))
         })
     }
 
     /// Unify two relatable values (e.g. `Ty`) and return new trait goals arising from it, so the
     /// caller needs to deal with them.
-    pub(crate) fn try_unify<T: ?Sized + Zip<Interner>>(
+    pub(crate) fn try_unify<T: ChalkToNextSolver<'a, U>, U: Relate<DbInterner<'a>>>(
         &mut self,
         t1: &T,
         t2: &T,
-    ) -> InferResult<()> {
-        match self.var_unification_table.relate(
-            Interner,
-            &self.db,
-            &self.trait_env.env,
-            chalk_ir::Variance::Invariant,
-            t1,
-            t2,
-        ) {
-            Ok(result) => Ok(InferOk { goals: result.goals, value: () }),
-            Err(chalk_ir::NoSolution) => Err(TypeError),
+    ) -> InferResult<'a, ()> {
+        let param_env = self.trait_env.env.to_nextsolver(self.interner);
+        let lhs = t1.to_nextsolver(self.interner);
+        let rhs = t2.to_nextsolver(self.interner);
+        let variance = rustc_type_ir::Variance::Invariant;
+        let span = crate::next_solver::Span::dummy();
+        match self.infer_ctxt.relate(param_env, lhs, variance, rhs, span) {
+            Ok(goals) => Ok(InferOk { goals, value: () }),
+            Err(_) => Err(TypeError),
         }
     }
 
     /// If `ty` is a type variable with known type, returns that type;
     /// otherwise, return ty.
+    #[tracing::instrument(skip(self))]
     pub(crate) fn resolve_ty_shallow(&mut self, ty: &Ty) -> Ty {
         if !ty.data(Interner).flags.intersects(chalk_ir::TypeFlags::HAS_FREE_LOCAL_NAMES) {
             return ty.clone();
         }
+        self.infer_ctxt
+            .resolve_vars_if_possible(ty.to_nextsolver(self.interner))
+            .to_chalk(self.interner)
+    }
+
+    pub(crate) fn resolve_vars_with_obligations<T>(&mut self, t: T) -> T
+    where
+        T: rustc_type_ir::TypeFoldable<DbInterner<'a>>,
+    {
+        use rustc_type_ir::TypeVisitableExt;
+
+        if !t.has_non_region_infer() {
+            return t;
+        }
+
+        let t = self.infer_ctxt.resolve_vars_if_possible(t);
+
+        if !t.has_non_region_infer() {
+            return t;
+        }
+
+        self.resolve_obligations_as_possible();
+        self.infer_ctxt.resolve_vars_if_possible(t)
+    }
+
+    pub(crate) fn structurally_resolve_type(&mut self, ty: &Ty) -> Ty {
+        if let TyKind::Alias(..) = ty.kind(Interner) {
+            self.structurally_normalize_ty(ty)
+        } else {
+            self.resolve_vars_with_obligations(ty.to_nextsolver(self.interner))
+                .to_chalk(self.interner)
+        }
+    }
+
+    fn structurally_normalize_ty(&mut self, ty: &Ty) -> Ty {
+        self.structurally_normalize_term(ty.to_nextsolver(self.interner).into())
+            .expect_ty()
+            .to_chalk(self.interner)
+    }
+
+    fn structurally_normalize_term(&mut self, term: Term<'a>) -> Term<'a> {
+        if term.to_alias_term().is_none() {
+            return term;
+        }
+
+        let new_infer = self.infer_ctxt.next_term_var_of_kind(term);
+
+        self.register_obligation(Predicate::new(
+            self.interner,
+            Binder::dummy(PredicateKind::AliasRelate(
+                term,
+                new_infer,
+                AliasRelationDirection::Equate,
+            )),
+        ));
         self.resolve_obligations_as_possible();
-        self.var_unification_table.normalize_ty_shallow(Interner, ty).unwrap_or_else(|| ty.clone())
+        let res = self.infer_ctxt.resolve_vars_if_possible(new_infer);
+        if res == new_infer { term } else { res }
     }
 
-    pub(crate) fn snapshot(&mut self) -> InferenceTableSnapshot {
-        let var_table_snapshot = self.var_unification_table.snapshot();
-        let type_variable_table = self.type_variable_table.clone();
+    pub(crate) fn snapshot(&mut self) -> InferenceTableSnapshot<'a> {
+        let ctxt_snapshot = self.infer_ctxt.start_snapshot();
+        let diverging_tys = self.diverging_tys.clone();
         let pending_obligations = self.pending_obligations.clone();
-        InferenceTableSnapshot { var_table_snapshot, pending_obligations, type_variable_table }
+        InferenceTableSnapshot { ctxt_snapshot, pending_obligations, diverging_tys }
     }
 
     #[tracing::instrument(skip_all)]
-    pub(crate) fn rollback_to(&mut self, snapshot: InferenceTableSnapshot) {
-        self.var_unification_table.rollback_to(snapshot.var_table_snapshot);
-        self.type_variable_table = snapshot.type_variable_table;
+    pub(crate) fn rollback_to(&mut self, snapshot: InferenceTableSnapshot<'a>) {
+        self.infer_ctxt.rollback_to(snapshot.ctxt_snapshot);
+        self.diverging_tys = snapshot.diverging_tys;
         self.pending_obligations = snapshot.pending_obligations;
     }
 
@@ -746,94 +780,95 @@ impl<'a> InferenceTable<'a> {
         result
     }
 
+    pub(crate) fn commit_if_ok<T, E>(
+        &mut self,
+        f: impl FnOnce(&mut InferenceTable<'_>) -> Result<T, E>,
+    ) -> Result<T, E> {
+        let snapshot = self.snapshot();
+        let result = f(self);
+        match result {
+            Ok(_) => {}
+            Err(_) => {
+                self.rollback_to(snapshot);
+            }
+        }
+        result
+    }
+
     /// Checks an obligation without registering it. Useful mostly to check
     /// whether a trait *might* be implemented before deciding to 'lock in' the
     /// choice (during e.g. method resolution or deref).
     #[tracing::instrument(level = "debug", skip(self))]
     pub(crate) fn try_obligation(&mut self, goal: Goal) -> NextTraitSolveResult {
         let in_env = InEnvironment::new(&self.trait_env.env, goal);
-        let canonicalized = self.canonicalize(in_env);
+        let canonicalized = self.canonicalize(in_env.to_nextsolver(self.interner));
 
-        self.db.trait_solve(self.trait_env.krate, self.trait_env.block, canonicalized)
+        next_trait_solve_canonical_in_ctxt(&self.infer_ctxt, canonicalized)
     }
 
-    pub(crate) fn register_obligation(&mut self, goal: Goal) {
-        let in_env = InEnvironment::new(&self.trait_env.env, goal);
-        self.register_obligation_in_env(in_env)
+    #[tracing::instrument(level = "debug", skip(self))]
+    pub(crate) fn solve_obligation(&mut self, goal: Goal) -> Result<Certainty, NoSolution> {
+        let goal = InEnvironment::new(&self.trait_env.env, goal);
+        let goal = goal.to_nextsolver(self.interner);
+        let result = next_trait_solve_in_ctxt(&self.infer_ctxt, goal);
+        result.map(|m| m.1)
+    }
+
+    pub(crate) fn register_obligation(&mut self, predicate: Predicate<'a>) {
+        let goal = next_solver::Goal {
+            param_env: self.trait_env.env.to_nextsolver(self.interner),
+            predicate,
+        };
+        self.register_obligation_in_env(goal)
     }
 
     #[tracing::instrument(level = "debug", skip(self))]
-    fn register_obligation_in_env(&mut self, goal: InEnvironment<Goal>) {
-        match goal.goal.data(Interner) {
-            chalk_ir::GoalData::DomainGoal(chalk_ir::DomainGoal::Holds(
-                chalk_ir::WhereClause::AliasEq(chalk_ir::AliasEq { alias, ty }),
-            )) => {
-                if ty.inference_var(Interner).is_some() {
-                    match alias {
-                        chalk_ir::AliasTy::Opaque(opaque) => {
-                            if self.unify(
-                                &chalk_ir::TyKind::OpaqueType(
-                                    opaque.opaque_ty_id,
-                                    opaque.substitution.clone(),
-                                )
-                                .intern(Interner),
-                                ty,
-                            ) {
-                                return;
-                            }
-                        }
-                        _ => {}
-                    }
-                }
+    fn register_obligation_in_env(
+        &mut self,
+        goal: next_solver::Goal<'a, next_solver::Predicate<'a>>,
+    ) {
+        let result = next_trait_solve_in_ctxt(&self.infer_ctxt, goal);
+        tracing::debug!(?result);
+        match result {
+            Ok((_, Certainty::Yes)) => {}
+            Err(rustc_type_ir::solve::NoSolution) => {}
+            Ok((_, Certainty::Maybe(_))) => {
+                self.pending_obligations.push(goal);
             }
-            _ => {}
-        }
-        let canonicalized = {
-            let result = self.var_unification_table.canonicalize(Interner, goal);
-            let free_vars = result
-                .free_vars
-                .into_iter()
-                .map(|free_var| free_var.to_generic_arg(Interner))
-                .collect();
-            Canonicalized { value: result.quantified, free_vars }
-        };
-        tracing::debug!(?canonicalized);
-        let solution = self.try_resolve_obligation(&canonicalized);
-        tracing::debug!(?solution);
-        if solution.uncertain() {
-            self.pending_obligations.push(canonicalized);
         }
     }
 
-    pub(crate) fn register_infer_ok<T>(&mut self, infer_ok: InferOk<T>) {
+    pub(crate) fn register_infer_ok<T>(&mut self, infer_ok: InferOk<'a, T>) {
         infer_ok.goals.into_iter().for_each(|goal| self.register_obligation_in_env(goal));
     }
 
     pub(crate) fn resolve_obligations_as_possible(&mut self) {
         let _span = tracing::info_span!("resolve_obligations_as_possible").entered();
         let mut changed = true;
-        let mut obligations = mem::take(&mut self.resolve_obligations_buffer);
         while mem::take(&mut changed) {
-            mem::swap(&mut self.pending_obligations, &mut obligations);
-
-            for canonicalized in obligations.drain(..) {
-                tracing::debug!(obligation = ?canonicalized);
-                if !self.check_changed(&canonicalized) {
-                    tracing::debug!("not changed");
-                    self.pending_obligations.push(canonicalized);
-                    continue;
+            let mut obligations = mem::take(&mut self.pending_obligations);
+
+            for goal in obligations.drain(..) {
+                tracing::debug!(obligation = ?goal);
+
+                let result = next_trait_solve_in_ctxt(&self.infer_ctxt, goal);
+                let (has_changed, certainty) = match result {
+                    Ok(result) => result,
+                    Err(_) => {
+                        continue;
+                    }
+                };
+
+                if matches!(has_changed, HasChanged::Yes) {
+                    changed = true;
+                }
+
+                match certainty {
+                    Certainty::Yes => {}
+                    Certainty::Maybe(_) => self.pending_obligations.push(goal),
                 }
-                changed = true;
-                let uncanonical = chalk_ir::Substitute::apply(
-                    &canonicalized.free_vars,
-                    canonicalized.value.value,
-                    Interner,
-                );
-                self.register_obligation_in_env(uncanonical);
             }
         }
-        self.resolve_obligations_buffer = obligations;
-        self.resolve_obligations_buffer.clear();
     }
 
     pub(crate) fn fudge_inference<T: TypeFoldable<Interner>>(
@@ -904,59 +939,6 @@ impl<'a> InferenceTable<'a> {
             .fold_with(&mut VarFudger { table: self, highest_known_var }, DebruijnIndex::INNERMOST)
     }
 
-    /// This checks whether any of the free variables in the `canonicalized`
-    /// have changed (either been unified with another variable, or with a
-    /// value). If this is not the case, we don't need to try to solve the goal
-    /// again -- it'll give the same result as last time.
-    fn check_changed(&mut self, canonicalized: &Canonicalized<InEnvironment<Goal>>) -> bool {
-        canonicalized.free_vars.iter().any(|var| {
-            let iv = match var.data(Interner) {
-                GenericArgData::Ty(ty) => ty.inference_var(Interner),
-                GenericArgData::Lifetime(lt) => lt.inference_var(Interner),
-                GenericArgData::Const(c) => c.inference_var(Interner),
-            }
-            .expect("free var is not inference var");
-            if self.var_unification_table.probe_var(iv).is_some() {
-                return true;
-            }
-            let root = self.var_unification_table.inference_var_root(iv);
-            iv != root
-        })
-    }
-
-    #[tracing::instrument(level = "debug", skip(self))]
-    fn try_resolve_obligation(
-        &mut self,
-        canonicalized: &Canonicalized<InEnvironment<Goal>>,
-    ) -> NextTraitSolveResult {
-        let solution = self.db.trait_solve(
-            self.trait_env.krate,
-            self.trait_env.block,
-            canonicalized.value.clone(),
-        );
-
-        tracing::debug!(?solution, ?canonicalized);
-        match &solution {
-            NextTraitSolveResult::Certain(v) => {
-                canonicalized.apply_solution(
-                    self,
-                    Canonical {
-                        binders: v.binders.clone(),
-                        // FIXME handle constraints
-                        value: v.value.subst.clone(),
-                    },
-                );
-            }
-            // ...so, should think about how to get some actually get some guidance here
-            NextTraitSolveResult::Uncertain(v) => {
-                canonicalized.apply_solution(self, v.clone());
-            }
-            NextTraitSolveResult::NoSolution => {}
-        }
-
-        solution
-    }
-
     pub(crate) fn callable_sig(
         &mut self,
         ty: &Ty,
@@ -1014,33 +996,15 @@ impl<'a> InferenceTable<'a> {
             .fill_with_unknown()
             .build();
 
-            let trait_env = self.trait_env.env.clone();
-            let obligation = InEnvironment {
-                goal: trait_ref.clone().cast(Interner),
-                environment: trait_env.clone(),
-            };
-            let canonical = self.canonicalize(obligation.clone());
-            if !self
-                .db
-                .trait_solve(krate, self.trait_env.block, canonical.cast(Interner))
-                .no_solution()
-            {
-                self.register_obligation(obligation.goal);
+            let goal: Goal = trait_ref.clone().cast(Interner);
+            if !self.try_obligation(goal.clone()).no_solution() {
+                self.register_obligation(goal.to_nextsolver(self.interner));
                 let return_ty = self.normalize_projection_ty(projection);
                 for &fn_x in subtraits {
                     let fn_x_trait = fn_x.get_id(self.db, krate)?;
                     trait_ref.trait_id = to_chalk_trait_id(fn_x_trait);
-                    let obligation: chalk_ir::InEnvironment<chalk_ir::Goal<Interner>> =
-                        InEnvironment {
-                            goal: trait_ref.clone().cast(Interner),
-                            environment: trait_env.clone(),
-                        };
-                    let canonical = self.canonicalize(obligation.clone());
-                    if !self
-                        .db
-                        .trait_solve(krate, self.trait_env.block, canonical.cast(Interner))
-                        .no_solution()
-                    {
+                    let goal = trait_ref.clone().cast(Interner);
+                    if !self.try_obligation(goal).no_solution() {
                         return Some((fn_x, arg_tys, return_ty));
                     }
                 }
@@ -1074,7 +1038,7 @@ impl<'a> InferenceTable<'a> {
         match ty.kind(Interner) {
             TyKind::Error => self.new_type_var(),
             TyKind::InferenceVar(..) => {
-                let ty_resolved = self.resolve_ty_shallow(&ty);
+                let ty_resolved = self.structurally_resolve_type(&ty);
                 if ty_resolved.is_unknown() { self.new_type_var() } else { ty }
             }
             _ => ty,
@@ -1165,7 +1129,7 @@ impl<'a> InferenceTable<'a> {
 
 impl fmt::Debug for InferenceTable<'_> {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        f.debug_struct("InferenceTable").field("num_vars", &self.type_variable_table.len()).finish()
+        f.debug_struct("InferenceTable").finish()
     }
 }
 
@@ -1174,11 +1138,19 @@ mod resolve {
     use crate::{
         ConcreteConst, Const, ConstData, ConstScalar, ConstValue, DebruijnIndex, GenericArg,
         InferenceVar, Interner, Lifetime, Ty, TyVariableKind, VariableKind,
+        next_solver::mapping::NextSolverToChalk,
     };
     use chalk_ir::{
         cast::Cast,
         fold::{TypeFoldable, TypeFolder},
     };
+    use rustc_type_ir::{FloatVid, IntVid, TyVid};
+
+    #[derive(Copy, Clone, PartialEq, Eq)]
+    pub(super) enum VarKind {
+        Ty(TyVariableKind),
+        Const,
+    }
 
     #[derive(chalk_derive::FallibleTypeFolder)]
     #[has_interner(Interner)]
@@ -1188,7 +1160,7 @@ mod resolve {
         F: Fn(InferenceVar, VariableKind, GenericArg, DebruijnIndex) -> GenericArg,
     > {
         pub(super) table: &'a mut InferenceTable<'b>,
-        pub(super) var_stack: &'a mut Vec<InferenceVar>,
+        pub(super) var_stack: &'a mut Vec<(InferenceVar, VarKind)>,
         pub(super) fallback: F,
     }
     impl<F> TypeFolder<Interner> for Resolver<'_, '_, F>
@@ -1209,25 +1181,91 @@ mod resolve {
             kind: TyVariableKind,
             outer_binder: DebruijnIndex,
         ) -> Ty {
-            let var = self.table.var_unification_table.inference_var_root(var);
-            if self.var_stack.contains(&var) {
-                // recursive type
-                let default = self.table.fallback_value(var, kind).cast(Interner);
-                return (self.fallback)(var, VariableKind::Ty(kind), default, outer_binder)
-                    .assert_ty_ref(Interner)
-                    .clone();
-            }
-            if let Some(known_ty) = self.table.var_unification_table.probe_var(var) {
-                // known_ty may contain other variables that are known by now
-                self.var_stack.push(var);
-                let result = known_ty.fold_with(self, outer_binder);
-                self.var_stack.pop();
-                result.assert_ty_ref(Interner).clone()
-            } else {
-                let default = self.table.fallback_value(var, kind).cast(Interner);
-                (self.fallback)(var, VariableKind::Ty(kind), default, outer_binder)
-                    .assert_ty_ref(Interner)
-                    .clone()
+            match kind {
+                TyVariableKind::General => {
+                    let vid = self.table.infer_ctxt.root_var(TyVid::from(var.index()));
+                    let var = InferenceVar::from(vid.as_u32());
+                    if self.var_stack.contains(&(var, VarKind::Ty(kind))) {
+                        // recursive type
+                        let default = self.table.fallback_value(var, kind).cast(Interner);
+                        return (self.fallback)(var, VariableKind::Ty(kind), default, outer_binder)
+                            .assert_ty_ref(Interner)
+                            .clone();
+                    }
+                    if let Ok(known_ty) = self.table.infer_ctxt.probe_ty_var(vid) {
+                        let known_ty: Ty = known_ty.to_chalk(self.table.interner);
+                        // known_ty may contain other variables that are known by now
+                        self.var_stack.push((var, VarKind::Ty(kind)));
+                        let result = known_ty.fold_with(self, outer_binder);
+                        self.var_stack.pop();
+                        result
+                    } else {
+                        let default = self.table.fallback_value(var, kind).cast(Interner);
+                        (self.fallback)(var, VariableKind::Ty(kind), default, outer_binder)
+                            .assert_ty_ref(Interner)
+                            .clone()
+                    }
+                }
+                TyVariableKind::Integer => {
+                    let vid = self
+                        .table
+                        .infer_ctxt
+                        .inner
+                        .borrow_mut()
+                        .int_unification_table()
+                        .find(IntVid::from(var.index()));
+                    let var = InferenceVar::from(vid.as_u32());
+                    if self.var_stack.contains(&(var, VarKind::Ty(kind))) {
+                        // recursive type
+                        let default = self.table.fallback_value(var, kind).cast(Interner);
+                        return (self.fallback)(var, VariableKind::Ty(kind), default, outer_binder)
+                            .assert_ty_ref(Interner)
+                            .clone();
+                    }
+                    if let Some(known_ty) = self.table.infer_ctxt.resolve_int_var(vid) {
+                        let known_ty: Ty = known_ty.to_chalk(self.table.interner);
+                        // known_ty may contain other variables that are known by now
+                        self.var_stack.push((var, VarKind::Ty(kind)));
+                        let result = known_ty.fold_with(self, outer_binder);
+                        self.var_stack.pop();
+                        result
+                    } else {
+                        let default = self.table.fallback_value(var, kind).cast(Interner);
+                        (self.fallback)(var, VariableKind::Ty(kind), default, outer_binder)
+                            .assert_ty_ref(Interner)
+                            .clone()
+                    }
+                }
+                TyVariableKind::Float => {
+                    let vid = self
+                        .table
+                        .infer_ctxt
+                        .inner
+                        .borrow_mut()
+                        .float_unification_table()
+                        .find(FloatVid::from(var.index()));
+                    let var = InferenceVar::from(vid.as_u32());
+                    if self.var_stack.contains(&(var, VarKind::Ty(kind))) {
+                        // recursive type
+                        let default = self.table.fallback_value(var, kind).cast(Interner);
+                        return (self.fallback)(var, VariableKind::Ty(kind), default, outer_binder)
+                            .assert_ty_ref(Interner)
+                            .clone();
+                    }
+                    if let Some(known_ty) = self.table.infer_ctxt.resolve_float_var(vid) {
+                        let known_ty: Ty = known_ty.to_chalk(self.table.interner);
+                        // known_ty may contain other variables that are known by now
+                        self.var_stack.push((var, VarKind::Ty(kind)));
+                        let result = known_ty.fold_with(self, outer_binder);
+                        self.var_stack.pop();
+                        result
+                    } else {
+                        let default = self.table.fallback_value(var, kind).cast(Interner);
+                        (self.fallback)(var, VariableKind::Ty(kind), default, outer_binder)
+                            .assert_ty_ref(Interner)
+                            .clone()
+                    }
+                }
             }
         }
 
@@ -1237,25 +1275,30 @@ mod resolve {
             var: InferenceVar,
             outer_binder: DebruijnIndex,
         ) -> Const {
-            let var = self.table.var_unification_table.inference_var_root(var);
+            let vid = self
+                .table
+                .infer_ctxt
+                .root_const_var(rustc_type_ir::ConstVid::from_u32(var.index()));
+            let var = InferenceVar::from(vid.as_u32());
             let default = ConstData {
                 ty: ty.clone(),
                 value: ConstValue::Concrete(ConcreteConst { interned: ConstScalar::Unknown }),
             }
             .intern(Interner)
             .cast(Interner);
-            if self.var_stack.contains(&var) {
+            if self.var_stack.contains(&(var, VarKind::Const)) {
                 // recursive
                 return (self.fallback)(var, VariableKind::Const(ty), default, outer_binder)
                     .assert_const_ref(Interner)
                     .clone();
             }
-            if let Some(known_ty) = self.table.var_unification_table.probe_var(var) {
+            if let Ok(known_const) = self.table.infer_ctxt.probe_const_var(vid) {
+                let known_const: Const = known_const.to_chalk(self.table.interner);
                 // known_ty may contain other variables that are known by now
-                self.var_stack.push(var);
-                let result = known_ty.fold_with(self, outer_binder);
+                self.var_stack.push((var, VarKind::Const));
+                let result = known_const.fold_with(self, outer_binder);
                 self.var_stack.pop();
-                result.assert_const_ref(Interner).clone()
+                result
             } else {
                 (self.fallback)(var, VariableKind::Const(ty), default, outer_binder)
                     .assert_const_ref(Interner)
diff --git a/crates/hir-ty/src/lib.rs b/crates/hir-ty/src/lib.rs
index c16bbb7b9922..659bc5ade3c7 100644
--- a/crates/hir-ty/src/lib.rs
+++ b/crates/hir-ty/src/lib.rs
@@ -101,7 +101,10 @@ use crate::{
     display::{DisplayTarget, HirDisplay},
     generics::Generics,
     infer::unify::InferenceTable,
-    next_solver::{DbInterner, mapping::convert_ty_for_result},
+    next_solver::{
+        DbInterner,
+        mapping::{ChalkToNextSolver, convert_ty_for_result},
+    },
 };
 
 pub use autoderef::autoderef;
@@ -957,23 +960,15 @@ pub fn callable_sig_from_fn_trait(
     )
     .build();
 
-    let block = trait_env.block;
-    let trait_env = trait_env.env.clone();
-    let obligation =
-        InEnvironment { goal: trait_ref.clone().cast(Interner), environment: trait_env.clone() };
-    let canonical = table.canonicalize(obligation.clone());
-    if !db.trait_solve(krate, block, canonical.cast(Interner)).no_solution() {
-        table.register_obligation(obligation.goal);
+    let goal: Goal = trait_ref.clone().cast(Interner);
+    let pred = goal.to_nextsolver(table.interner);
+    if !table.try_obligation(goal).no_solution() {
+        table.register_obligation(pred);
         let return_ty = table.normalize_projection_ty(projection);
         for fn_x in [FnTrait::Fn, FnTrait::FnMut, FnTrait::FnOnce] {
             let fn_x_trait = fn_x.get_id(db, krate)?;
             trait_ref.trait_id = to_chalk_trait_id(fn_x_trait);
-            let obligation: chalk_ir::InEnvironment<chalk_ir::Goal<Interner>> = InEnvironment {
-                goal: trait_ref.clone().cast(Interner),
-                environment: trait_env.clone(),
-            };
-            let canonical = table.canonicalize(obligation.clone());
-            if !db.trait_solve(krate, block, canonical.cast(Interner)).no_solution() {
+            if !table.try_obligation(trait_ref.clone().cast(Interner)).no_solution() {
                 let ret_ty = table.resolve_completely(return_ty);
                 let args_ty = table.resolve_completely(args_ty);
                 let params = args_ty
diff --git a/crates/hir-ty/src/method_resolution.rs b/crates/hir-ty/src/method_resolution.rs
index f0be352fdd15..fa80567b1ecc 100644
--- a/crates/hir-ty/src/method_resolution.rs
+++ b/crates/hir-ty/src/method_resolution.rs
@@ -16,24 +16,30 @@ use hir_def::{
 use hir_expand::name::Name;
 use intern::sym;
 use rustc_hash::{FxHashMap, FxHashSet};
-use rustc_type_ir::inherent::{IntoKind, SliceLike};
+use rustc_type_ir::inherent::{IntoKind, SliceLike, Ty as _};
 use smallvec::{SmallVec, smallvec};
 use stdx::never;
 use triomphe::Arc;
 
 use crate::{
-    AdtId, Canonical, CanonicalVarKinds, DebruijnIndex, DynTyExt, ForeignDefId, GenericArgData,
-    Goal, InEnvironment, Interner, Mutability, Scalar, Substitution, TraitEnvironment, TraitRef,
-    TraitRefExt, Ty, TyBuilder, TyExt, TyKind, TyVariableKind, VariableKind, WhereClause,
+    AdtId, AliasTy, Canonical, CanonicalVarKinds, DebruijnIndex, DynTyExt, ForeignDefId,
+    GenericArgData, Goal, InEnvironment, Interner, Mutability, Scalar, Substitution,
+    TraitEnvironment, TraitRef, TraitRefExt, Ty, TyBuilder, TyExt, TyKind, TyVariableKind,
+    VariableKind, WhereClause,
     autoderef::{self, AutoderefKind},
     db::HirDatabase,
-    error_lifetime, from_chalk_trait_id, from_foreign_def_id,
+    from_chalk_trait_id, from_foreign_def_id,
     infer::{Adjust, Adjustment, OverloadedDeref, PointerCast, unify::InferenceTable},
     lang_items::is_box,
-    next_solver::SolverDefId,
+    next_solver::{
+        self, SolverDefId,
+        fulfill::FulfillmentCtxt,
+        infer::DefineOpaqueTypes,
+        mapping::{ChalkToNextSolver, NextSolverToChalk},
+    },
     primitive::{FloatTy, IntTy, UintTy},
     to_chalk_trait_id,
-    traits::NextTraitSolveResult,
+    traits::next_trait_solve_canonical_in_ctxt,
     utils::all_super_traits,
 };
 
@@ -101,6 +107,7 @@ impl TyFingerprint {
             }
             TyKind::AssociatedType(_, _)
             | TyKind::OpaqueType(_, _)
+            | TyKind::Alias(AliasTy::Opaque(_))
             | TyKind::FnDef(_, _)
             | TyKind::Closure(_, _)
             | TyKind::Coroutine(..)
@@ -118,7 +125,7 @@ impl TyFingerprint {
     }
 
     /// Creates a TyFingerprint for looking up a trait impl.
-    pub fn for_trait_impl_ns<'db>(ty: &crate::next_solver::Ty<'db>) -> Option<TyFingerprint> {
+    pub fn for_trait_impl_ns<'db>(ty: &next_solver::Ty<'db>) -> Option<TyFingerprint> {
         use rustc_type_ir::TyKind;
         let fp = match (*ty).kind() {
             TyKind::Str => TyFingerprint::Str,
@@ -533,9 +540,9 @@ pub fn def_crates(db: &dyn HirDatabase, ty: &Ty, cur_crate: Crate) -> Option<Sma
 }
 
 /// Look up the method with the given name.
-pub(crate) fn lookup_method(
-    db: &dyn HirDatabase,
-    ty: &Canonical<Ty>,
+pub(crate) fn lookup_method<'db>(
+    db: &'db dyn HirDatabase,
+    ty: &next_solver::Canonical<'db, crate::next_solver::Ty<'db>>,
     env: Arc<TraitEnvironment>,
     traits_in_scope: &FxHashSet<TraitId>,
     visible_from_module: VisibleFromModule,
@@ -617,7 +624,7 @@ pub struct ReceiverAdjustments {
 
 impl ReceiverAdjustments {
     pub(crate) fn apply(&self, table: &mut InferenceTable<'_>, ty: Ty) -> (Ty, Vec<Adjustment>) {
-        let mut ty = table.resolve_ty_shallow(&ty);
+        let mut ty = table.structurally_resolve_type(&ty);
         let mut adjust = Vec::new();
         for _ in 0..self.autoderefs {
             match autoderef::autoderef_step(table, ty.clone(), true, false) {
@@ -697,9 +704,9 @@ impl ReceiverAdjustments {
 // This would be nicer if it just returned an iterator, but that runs into
 // lifetime problems, because we need to borrow temp `CrateImplDefs`.
 // FIXME add a context type here?
-pub(crate) fn iterate_method_candidates<T>(
-    ty: &Canonical<Ty>,
-    db: &dyn HirDatabase,
+pub(crate) fn iterate_method_candidates<'db, T>(
+    ty: &next_solver::Canonical<'db, crate::next_solver::Ty<'db>>,
+    db: &'db dyn HirDatabase,
     env: Arc<TraitEnvironment>,
     traits_in_scope: &FxHashSet<TraitId>,
     visible_from_module: VisibleFromModule,
@@ -899,7 +906,7 @@ fn find_matching_impl(
                 if table.try_obligation(goal.clone()).no_solution() {
                     return None;
                 }
-                table.register_obligation(goal);
+                table.register_obligation(goal.to_nextsolver(table.interner));
             }
             Some((impl_.impl_items(db), table.resolve_completely(impl_substs)))
         })
@@ -1046,9 +1053,9 @@ pub fn check_orphan_rules(db: &dyn HirDatabase, impl_: ImplId) -> bool {
     is_not_orphan
 }
 
-pub fn iterate_path_candidates(
-    ty: &Canonical<Ty>,
-    db: &dyn HirDatabase,
+pub fn iterate_path_candidates<'db>(
+    ty: &next_solver::Canonical<'db, crate::next_solver::Ty<'db>>,
+    db: &'db dyn HirDatabase,
     env: Arc<TraitEnvironment>,
     traits_in_scope: &FxHashSet<TraitId>,
     visible_from_module: VisibleFromModule,
@@ -1068,9 +1075,9 @@ pub fn iterate_path_candidates(
     )
 }
 
-pub fn iterate_method_candidates_dyn(
-    ty: &Canonical<Ty>,
-    db: &dyn HirDatabase,
+pub fn iterate_method_candidates_dyn<'db>(
+    ty: &next_solver::Canonical<'db, crate::next_solver::Ty<'db>>,
+    db: &'db dyn HirDatabase,
     env: Arc<TraitEnvironment>,
     traits_in_scope: &FxHashSet<TraitId>,
     visible_from_module: VisibleFromModule,
@@ -1108,7 +1115,7 @@ pub fn iterate_method_candidates_dyn(
             // types*.
 
             let mut table = InferenceTable::new(db, env);
-            let ty = table.instantiate_canonical(ty.clone());
+            let ty = table.instantiate_canonical_ns(*ty);
             let deref_chain = autoderef_method_receiver(&mut table, ty);
 
             deref_chain.into_iter().try_for_each(|(receiver_ty, adj)| {
@@ -1139,19 +1146,16 @@ pub fn iterate_method_candidates_dyn(
 }
 
 #[tracing::instrument(skip_all, fields(name = ?name))]
-fn iterate_method_candidates_with_autoref(
-    table: &mut InferenceTable<'_>,
-    receiver_ty: Canonical<Ty>,
+fn iterate_method_candidates_with_autoref<'db>(
+    table: &mut InferenceTable<'db>,
+    receiver_ty: next_solver::Canonical<'db, crate::next_solver::Ty<'db>>,
     first_adjustment: ReceiverAdjustments,
     traits_in_scope: &FxHashSet<TraitId>,
     visible_from_module: VisibleFromModule,
     name: Option<&Name>,
     callback: &mut dyn MethodCandidateCallback,
 ) -> ControlFlow<()> {
-    if receiver_ty.value.is_general_var(Interner, &receiver_ty.binders) {
-        // don't try to resolve methods on unknown types
-        return ControlFlow::Continue(());
-    }
+    let interner = table.interner;
 
     let mut iterate_method_candidates_by_receiver = move |receiver_ty, first_adjustment| {
         iterate_method_candidates_by_receiver(
@@ -1166,18 +1170,27 @@ fn iterate_method_candidates_with_autoref(
     };
 
     let mut maybe_reborrowed = first_adjustment.clone();
-    if let Some((_, _, m)) = receiver_ty.value.as_reference() {
+    if let rustc_type_ir::TyKind::Ref(_, _, m) = receiver_ty.value.kind() {
+        let m = match m {
+            rustc_ast_ir::Mutability::Mut => chalk_ir::Mutability::Mut,
+            rustc_ast_ir::Mutability::Not => chalk_ir::Mutability::Not,
+        };
         // Prefer reborrow of references to move
         maybe_reborrowed.autoref = Some(AutorefOrPtrAdjustment::Autoref(m));
         maybe_reborrowed.autoderefs += 1;
     }
 
-    iterate_method_candidates_by_receiver(receiver_ty.clone(), maybe_reborrowed)?;
+    iterate_method_candidates_by_receiver(receiver_ty, maybe_reborrowed)?;
 
-    let refed = Canonical {
-        value: TyKind::Ref(Mutability::Not, error_lifetime(), receiver_ty.value.clone())
-            .intern(Interner),
-        binders: receiver_ty.binders.clone(),
+    let refed = next_solver::Canonical {
+        max_universe: receiver_ty.max_universe,
+        variables: receiver_ty.variables,
+        value: next_solver::Ty::new_ref(
+            interner,
+            next_solver::Region::error(interner),
+            receiver_ty.value,
+            rustc_ast_ir::Mutability::Not,
+        ),
     };
 
     iterate_method_candidates_by_receiver(
@@ -1185,10 +1198,15 @@ fn iterate_method_candidates_with_autoref(
         first_adjustment.with_autoref(AutorefOrPtrAdjustment::Autoref(Mutability::Not)),
     )?;
 
-    let ref_muted = Canonical {
-        value: TyKind::Ref(Mutability::Mut, error_lifetime(), receiver_ty.value.clone())
-            .intern(Interner),
-        binders: receiver_ty.binders.clone(),
+    let ref_muted = next_solver::Canonical {
+        max_universe: receiver_ty.max_universe,
+        variables: receiver_ty.variables,
+        value: next_solver::Ty::new_ref(
+            interner,
+            next_solver::Region::error(interner),
+            receiver_ty.value,
+            rustc_ast_ir::Mutability::Mut,
+        ),
     };
 
     iterate_method_candidates_by_receiver(
@@ -1196,10 +1214,13 @@ fn iterate_method_candidates_with_autoref(
         first_adjustment.with_autoref(AutorefOrPtrAdjustment::Autoref(Mutability::Mut)),
     )?;
 
-    if let Some((ty, Mutability::Mut)) = receiver_ty.value.as_raw_ptr() {
-        let const_ptr_ty = Canonical {
-            value: TyKind::Raw(Mutability::Not, ty.clone()).intern(Interner),
-            binders: receiver_ty.binders,
+    if let rustc_type_ir::TyKind::RawPtr(ty, rustc_ast_ir::Mutability::Mut) =
+        receiver_ty.value.kind()
+    {
+        let const_ptr_ty = rustc_type_ir::Canonical {
+            max_universe: rustc_type_ir::UniverseIndex::ZERO,
+            value: next_solver::Ty::new_ptr(interner, ty, rustc_ast_ir::Mutability::Not),
+            variables: receiver_ty.variables,
         };
         iterate_method_candidates_by_receiver(
             const_ptr_ty,
@@ -1250,16 +1271,17 @@ where
 }
 
 #[tracing::instrument(skip_all, fields(name = ?name))]
-fn iterate_method_candidates_by_receiver(
-    table: &mut InferenceTable<'_>,
-    receiver_ty: Canonical<Ty>,
+fn iterate_method_candidates_by_receiver<'db>(
+    table: &mut InferenceTable<'db>,
+    receiver_ty: next_solver::Canonical<'db, crate::next_solver::Ty<'db>>,
     receiver_adjustments: ReceiverAdjustments,
     traits_in_scope: &FxHashSet<TraitId>,
     visible_from_module: VisibleFromModule,
     name: Option<&Name>,
     callback: &mut dyn MethodCandidateCallback,
 ) -> ControlFlow<()> {
-    let receiver_ty = table.instantiate_canonical(receiver_ty);
+    let receiver_ty = table.instantiate_canonical_ns(receiver_ty);
+    let receiver_ty: crate::Ty = receiver_ty.to_chalk(table.interner);
     // We're looking for methods with *receiver* type receiver_ty. These could
     // be found in any of the derefs of receiver_ty, so we have to go through
     // that, including raw derefs.
@@ -1274,6 +1296,7 @@ fn iterate_method_candidates_by_receiver(
                 Some(&receiver_ty),
                 Some(receiver_adjustments.clone()),
                 visible_from_module,
+                LookupMode::MethodCall,
                 &mut |adjustments, item, is_visible| {
                     callback.on_inherent_method(adjustments, item, is_visible)
                 },
@@ -1297,6 +1320,7 @@ fn iterate_method_candidates_by_receiver(
                 name,
                 Some(&receiver_ty),
                 Some(receiver_adjustments.clone()),
+                LookupMode::MethodCall,
                 &mut |adjustments, item, is_visible| {
                     callback.on_trait_method(adjustments, item, is_visible)
                 },
@@ -1307,9 +1331,9 @@ fn iterate_method_candidates_by_receiver(
 }
 
 #[tracing::instrument(skip_all, fields(name = ?name))]
-fn iterate_method_candidates_for_self_ty(
-    self_ty: &Canonical<Ty>,
-    db: &dyn HirDatabase,
+fn iterate_method_candidates_for_self_ty<'db>(
+    self_ty: &next_solver::Canonical<'db, crate::next_solver::Ty<'db>>,
+    db: &'db dyn HirDatabase,
     env: Arc<TraitEnvironment>,
     traits_in_scope: &FxHashSet<TraitId>,
     visible_from_module: VisibleFromModule,
@@ -1317,7 +1341,7 @@ fn iterate_method_candidates_for_self_ty(
     callback: &mut dyn MethodCandidateCallback,
 ) -> ControlFlow<()> {
     let mut table = InferenceTable::new(db, env);
-    let self_ty = table.instantiate_canonical(self_ty.clone());
+    let self_ty = table.instantiate_canonical_ns(*self_ty).to_chalk(table.interner);
     iterate_inherent_methods(
         &self_ty,
         &mut table,
@@ -1325,6 +1349,7 @@ fn iterate_method_candidates_for_self_ty(
         None,
         None,
         visible_from_module,
+        LookupMode::Path,
         &mut |adjustments, item, is_visible| {
             callback.on_inherent_method(adjustments, item, is_visible)
         },
@@ -1336,6 +1361,7 @@ fn iterate_method_candidates_for_self_ty(
         name,
         None,
         None,
+        LookupMode::Path,
         &mut |adjustments, item, is_visible| {
             callback.on_trait_method(adjustments, item, is_visible)
         },
@@ -1350,12 +1376,13 @@ fn iterate_trait_method_candidates(
     name: Option<&Name>,
     receiver_ty: Option<&Ty>,
     receiver_adjustments: Option<ReceiverAdjustments>,
+    mode: LookupMode,
     callback: &mut dyn FnMut(ReceiverAdjustments, AssocItemId, bool) -> ControlFlow<()>,
 ) -> ControlFlow<()> {
     let db = table.db;
 
-    let canonical_self_ty = table.canonicalize(self_ty.clone());
-    let TraitEnvironment { krate, block, .. } = *table.trait_env;
+    let canonical_self_ty = table.canonicalize(self_ty.clone().to_nextsolver(table.interner));
+    let TraitEnvironment { krate, .. } = *table.trait_env;
 
     'traits: for &t in traits_in_scope {
         let data = db.trait_signature(t);
@@ -1395,15 +1422,22 @@ fn iterate_trait_method_candidates(
         for &(_, item) in t.trait_items(db).items.iter() {
             // Don't pass a `visible_from_module` down to `is_valid_candidate`,
             // since only inherent methods should be included into visibility checking.
-            let visible =
-                match is_valid_trait_method_candidate(table, t, name, receiver_ty, item, self_ty) {
-                    IsValidCandidate::Yes => true,
-                    IsValidCandidate::NotVisible => false,
-                    IsValidCandidate::No => continue,
-                };
+            let visible = match is_valid_trait_method_candidate(
+                table,
+                t,
+                name,
+                receiver_ty,
+                item,
+                self_ty,
+                mode,
+            ) {
+                IsValidCandidate::Yes => true,
+                IsValidCandidate::NotVisible => false,
+                IsValidCandidate::No => continue,
+            };
             if !known_implemented {
-                let goal = generic_implements_goal(db, &table.trait_env, t, &canonical_self_ty);
-                if db.trait_solve(krate, block, goal.cast(Interner)).no_solution() {
+                let goal = generic_implements_goal_ns(table, t, canonical_self_ty);
+                if next_trait_solve_canonical_in_ctxt(&table.infer_ctxt, goal).no_solution() {
                     continue 'traits;
                 }
             }
@@ -1422,6 +1456,7 @@ fn iterate_inherent_methods(
     receiver_ty: Option<&Ty>,
     receiver_adjustments: Option<ReceiverAdjustments>,
     visible_from_module: VisibleFromModule,
+    mode: LookupMode,
     callback: &mut dyn FnMut(ReceiverAdjustments, AssocItemId, bool) -> ControlFlow<()>,
 ) -> ControlFlow<()> {
     let db = table.db;
@@ -1445,6 +1480,7 @@ fn iterate_inherent_methods(
                 receiver_adjustments.clone(),
                 callback,
                 traits,
+                mode,
             )?;
         }
         TyKind::Dyn(_) => {
@@ -1458,6 +1494,7 @@ fn iterate_inherent_methods(
                     receiver_adjustments.clone(),
                     callback,
                     traits.into_iter(),
+                    mode,
                 )?;
             }
         }
@@ -1516,6 +1553,7 @@ fn iterate_inherent_methods(
         receiver_adjustments: Option<ReceiverAdjustments>,
         callback: &mut dyn FnMut(ReceiverAdjustments, AssocItemId, bool) -> ControlFlow<()>,
         traits: impl Iterator<Item = TraitId>,
+        mode: LookupMode,
     ) -> ControlFlow<()> {
         let db = table.db;
         for t in traits {
@@ -1529,6 +1567,7 @@ fn iterate_inherent_methods(
                     receiver_ty,
                     item,
                     self_ty,
+                    mode,
                 ) {
                     IsValidCandidate::Yes => true,
                     IsValidCandidate::NotVisible => false,
@@ -1575,21 +1614,17 @@ fn iterate_inherent_methods(
 }
 
 /// Returns the receiver type for the index trait call.
-pub(crate) fn resolve_indexing_op(
-    db: &dyn HirDatabase,
-    env: Arc<TraitEnvironment>,
-    ty: Canonical<Ty>,
+pub(crate) fn resolve_indexing_op<'db>(
+    table: &mut InferenceTable<'db>,
+    ty: next_solver::Canonical<'db, next_solver::Ty<'db>>,
     index_trait: TraitId,
 ) -> Option<ReceiverAdjustments> {
-    let mut table = InferenceTable::new(db, env);
-    let ty = table.instantiate_canonical(ty);
-    let deref_chain = autoderef_method_receiver(&mut table, ty);
+    let ty = table.instantiate_canonical_ns(ty);
+    let deref_chain = autoderef_method_receiver(table, ty);
     for (ty, adj) in deref_chain {
-        let goal = generic_implements_goal(db, &table.trait_env, index_trait, &ty);
-        if !db
-            .trait_solve(table.trait_env.krate, table.trait_env.block, goal.cast(Interner))
-            .no_solution()
-        {
+        //let goal = generic_implements_goal_ns(db, &table.trait_env, index_trait, &ty);
+        let goal = generic_implements_goal_ns(table, index_trait, ty);
+        if !next_trait_solve_canonical_in_ctxt(&table.infer_ctxt, goal).no_solution() {
             return Some(adj);
         }
     }
@@ -1669,6 +1704,7 @@ fn is_valid_trait_method_candidate(
     receiver_ty: Option<&Ty>,
     item: AssocItemId,
     self_ty: &Ty,
+    mode: LookupMode,
 ) -> IsValidCandidate {
     let db = table.db;
     match item {
@@ -1696,6 +1732,35 @@ fn is_valid_trait_method_candidate(
                     let expected_receiver =
                         sig.map(|s| s.params()[0].clone()).substitute(Interner, &fn_subst);
 
+                    // FIXME: Clean up this mess with some context struct like rustc's `ProbeContext`
+                    let variance = match mode {
+                        LookupMode::MethodCall => rustc_type_ir::Variance::Covariant,
+                        LookupMode::Path => rustc_type_ir::Variance::Invariant,
+                    };
+                    let res = table
+                        .infer_ctxt
+                        .at(
+                            &next_solver::infer::traits::ObligationCause::dummy(),
+                            table.trait_env.env.to_nextsolver(table.interner),
+                        )
+                        .relate(
+                            DefineOpaqueTypes::No,
+                            expected_receiver.to_nextsolver(table.interner),
+                            variance,
+                            receiver_ty.to_nextsolver(table.interner),
+                        );
+                    let Ok(infer_ok) = res else {
+                        return IsValidCandidate::No;
+                    };
+
+                    if !infer_ok.obligations.is_empty() {
+                        let mut ctxt = FulfillmentCtxt::new(&table.infer_ctxt);
+                        for pred in infer_ok.into_obligations() {
+                            ctxt.register_predicate_obligation(&table.infer_ctxt, pred);
+                        }
+                        check_that!(ctxt.select_all_or_error(&table.infer_ctxt).is_empty());
+                    }
+
                     check_that!(table.unify(receiver_ty, &expected_receiver));
                 }
 
@@ -1773,26 +1838,11 @@ fn is_valid_impl_fn_candidate(
         });
 
         for goal in goals.clone() {
-            let in_env = InEnvironment::new(&table.trait_env.env, goal);
-            let canonicalized = table.canonicalize_with_free_vars(in_env);
-            let solution = table.db.trait_solve(
-                table.trait_env.krate,
-                table.trait_env.block,
-                canonicalized.value.clone(),
-            );
-
-            match solution {
-                NextTraitSolveResult::Certain(canonical_subst) => {
-                    canonicalized.apply_solution(
-                        table,
-                        Canonical {
-                            binders: canonical_subst.binders,
-                            value: canonical_subst.value.subst,
-                        },
-                    );
+            match table.solve_obligation(goal) {
+                Ok(_) => {}
+                Err(_) => {
+                    return IsValidCandidate::No;
                 }
-                NextTraitSolveResult::Uncertain(..) => {}
-                NextTraitSolveResult::NoSolution => return IsValidCandidate::No,
             }
         }
 
@@ -1857,25 +1907,49 @@ fn generic_implements_goal(
     Canonical { binders, value }
 }
 
-fn autoderef_method_receiver(
-    table: &mut InferenceTable<'_>,
-    ty: Ty,
-) -> Vec<(Canonical<Ty>, ReceiverAdjustments)> {
-    let mut deref_chain: Vec<_> = Vec::new();
-    let mut autoderef = autoderef::Autoderef::new_no_tracking(table, ty, false, true);
+/// This creates Substs for a trait with the given Self type and type variables
+/// for all other parameters, to query the trait solver with it.
+#[tracing::instrument(skip_all)]
+fn generic_implements_goal_ns<'db>(
+    table: &mut InferenceTable<'db>,
+    trait_: TraitId,
+    self_ty: next_solver::Canonical<'db, crate::next_solver::Ty<'db>>,
+) -> next_solver::Canonical<'db, next_solver::Goal<'db, crate::next_solver::Predicate<'db>>> {
+    let args = table.infer_ctxt.fresh_args_for_item(SolverDefId::TraitId(trait_));
+    let self_ty = table.instantiate_canonical_ns(self_ty);
+    let trait_ref =
+        rustc_type_ir::TraitRef::new_from_args(table.infer_ctxt.interner, trait_.into(), args)
+            .with_replaced_self_ty(table.infer_ctxt.interner, self_ty);
+    let goal = next_solver::Goal::new(
+        table.infer_ctxt.interner,
+        table.trait_env.env.to_nextsolver(table.infer_ctxt.interner),
+        trait_ref,
+    );
+
+    table.canonicalize(goal)
+}
+
+fn autoderef_method_receiver<'db>(
+    table: &mut InferenceTable<'db>,
+    ty: next_solver::Ty<'db>,
+) -> Vec<(next_solver::Canonical<'db, crate::next_solver::Ty<'db>>, ReceiverAdjustments)> {
+    let interner = table.interner;
+    let mut deref_chain = Vec::new();
+    let mut autoderef =
+        autoderef::Autoderef::new_no_tracking(table, ty.to_chalk(interner), false, true);
     while let Some((ty, derefs)) = autoderef.next() {
         deref_chain.push((
-            autoderef.table.canonicalize(ty),
+            autoderef.table.canonicalize(ty.to_nextsolver(interner)),
             ReceiverAdjustments { autoref: None, autoderefs: derefs, unsize_array: false },
         ));
     }
     // As a last step, we can do array unsizing (that's the only unsizing that rustc does for method receivers!)
-    if let Some((TyKind::Array(parameters, _), binders, adj)) =
-        deref_chain.last().map(|(ty, adj)| (ty.value.kind(Interner), ty.binders.clone(), adj))
+    if let Some((rustc_type_ir::Array(parameters, _), variables, max_universe, adj)) =
+        deref_chain.last().map(|d| (d.0.value.kind(), d.0.variables, d.0.max_universe, d.1.clone()))
     {
-        let unsized_ty = TyKind::Slice(parameters.clone()).intern(Interner);
+        let unsized_ty = next_solver::Ty::new_slice(interner, parameters);
         deref_chain.push((
-            Canonical { value: unsized_ty, binders },
+            next_solver::Canonical { max_universe, value: unsized_ty, variables },
             ReceiverAdjustments { unsize_array: true, ..adj.clone() },
         ));
     }
diff --git a/crates/hir-ty/src/mir.rs b/crates/hir-ty/src/mir.rs
index 8c48a16537a2..6465099dffd7 100644
--- a/crates/hir-ty/src/mir.rs
+++ b/crates/hir-ty/src/mir.rs
@@ -34,8 +34,7 @@ pub use eval::{
 };
 pub use lower::{MirLowerError, lower_to_mir, mir_body_for_closure_query, mir_body_query};
 pub use monomorphization::{
-    monomorphize_mir_body_bad, monomorphized_mir_body_for_closure_query,
-    monomorphized_mir_body_query,
+    monomorphized_mir_body_for_closure_query, monomorphized_mir_body_query,
 };
 use rustc_hash::FxHashMap;
 use smallvec::{SmallVec, smallvec};
diff --git a/crates/hir-ty/src/mir/monomorphization.rs b/crates/hir-ty/src/mir/monomorphization.rs
index b0b922316914..555b87850924 100644
--- a/crates/hir-ty/src/mir/monomorphization.rs
+++ b/crates/hir-ty/src/mir/monomorphization.rs
@@ -38,7 +38,6 @@ struct Filler<'a> {
     trait_env: Arc<TraitEnvironment>,
     subst: &'a Substitution,
     generics: Option<Generics>,
-    owner: DefWithBodyId,
 }
 impl FallibleTypeFolder<Interner> for Filler<'_> {
     type Error = MirLowerError;
@@ -66,7 +65,11 @@ impl FallibleTypeFolder<Interner> for Filler<'_> {
                 }))
                 .intern(Interner))
             }
-            TyKind::OpaqueType(id, subst) => {
+            TyKind::Alias(chalk_ir::AliasTy::Opaque(chalk_ir::OpaqueTy {
+                opaque_ty_id: id,
+                substitution: subst,
+            }))
+            | TyKind::OpaqueType(id, subst) => {
                 let impl_trait_id = self.db.lookup_intern_impl_trait_id((*id).into());
                 let subst = subst.clone().try_fold_with(self.as_dyn(), outer_binder)?;
                 match impl_trait_id {
@@ -74,7 +77,6 @@ impl FallibleTypeFolder<Interner> for Filler<'_> {
                         let infer = self.db.infer(func.into());
                         let filler = &mut Filler {
                             db: self.db,
-                            owner: self.owner,
                             trait_env: self.trait_env.clone(),
                             subst: &subst,
                             generics: Some(generics(self.db, func.into())),
@@ -306,7 +308,7 @@ pub fn monomorphized_mir_body_query(
     trait_env: Arc<crate::TraitEnvironment>,
 ) -> Result<Arc<MirBody>, MirLowerError> {
     let generics = owner.as_generic_def_id(db).map(|g_def| generics(db, g_def));
-    let filler = &mut Filler { db, subst: &subst, trait_env, generics, owner };
+    let filler = &mut Filler { db, subst: &subst, trait_env, generics };
     let body = db.mir_body(owner)?;
     let mut body = (*body).clone();
     filler.fill_body(&mut body)?;
@@ -330,23 +332,9 @@ pub fn monomorphized_mir_body_for_closure_query(
 ) -> Result<Arc<MirBody>, MirLowerError> {
     let InternedClosure(owner, _) = db.lookup_intern_closure(closure);
     let generics = owner.as_generic_def_id(db).map(|g_def| generics(db, g_def));
-    let filler = &mut Filler { db, subst: &subst, trait_env, generics, owner };
+    let filler = &mut Filler { db, subst: &subst, trait_env, generics };
     let body = db.mir_body_for_closure(closure)?;
     let mut body = (*body).clone();
     filler.fill_body(&mut body)?;
     Ok(Arc::new(body))
 }
-
-// FIXME: remove this function. Monomorphization is a time consuming job and should always be a query.
-pub fn monomorphize_mir_body_bad(
-    db: &dyn HirDatabase,
-    mut body: MirBody,
-    subst: Substitution,
-    trait_env: Arc<crate::TraitEnvironment>,
-) -> Result<MirBody, MirLowerError> {
-    let owner = body.owner;
-    let generics = owner.as_generic_def_id(db).map(|g_def| generics(db, g_def));
-    let filler = &mut Filler { db, subst: &subst, trait_env, generics, owner };
-    filler.fill_body(&mut body)?;
-    Ok(body)
-}
diff --git a/crates/hir-ty/src/next_solver.rs b/crates/hir-ty/src/next_solver.rs
index 21762aa66a85..0225deebe4f3 100644
--- a/crates/hir-ty/src/next_solver.rs
+++ b/crates/hir-ty/src/next_solver.rs
@@ -5,11 +5,10 @@ pub mod abi;
 mod consts;
 mod def_id;
 pub mod fold;
-mod fulfill;
+pub mod fulfill;
 mod generic_arg;
 pub mod generics;
 pub mod infer;
-//mod infer_new;
 pub mod interner;
 mod ir_print;
 pub mod mapping;
@@ -24,7 +23,6 @@ pub mod util;
 pub use consts::*;
 pub use def_id::*;
 pub use generic_arg::*;
-//pub use infer_new::*;
 pub use interner::*;
 pub use opaques::*;
 pub use predicate::*;
diff --git a/crates/hir-ty/src/next_solver/infer/canonical/canonicalizer.rs b/crates/hir-ty/src/next_solver/infer/canonical/canonicalizer.rs
new file mode 100644
index 000000000000..5d11525cd199
--- /dev/null
+++ b/crates/hir-ty/src/next_solver/infer/canonical/canonicalizer.rs
@@ -0,0 +1,779 @@
+//! This module contains code to canonicalize values into a `Canonical<'db, T>`.
+//!
+//! For an overview of what canonicalization is and how it fits into
+//! rustc, check out the [chapter in the rustc dev guide][c].
+//!
+//! [c]: https://rust-lang.github.io/chalk/book/canonical_queries/canonicalization.html
+
+use rustc_hash::FxHashMap;
+use rustc_index::Idx;
+use rustc_type_ir::InferTy::{self, FloatVar, IntVar, TyVar};
+use rustc_type_ir::inherent::{Const as _, IntoKind as _, Region as _, SliceLike, Ty as _};
+use rustc_type_ir::{
+    BoundVar, CanonicalQueryInput, CanonicalTyVarKind, DebruijnIndex, Flags, InferConst,
+    RegionKind, TypeFlags, TypeFoldable, TypeFolder, TypeSuperFoldable, TypeVisitableExt,
+    UniverseIndex,
+};
+use smallvec::SmallVec;
+use tracing::debug;
+
+use crate::next_solver::infer::InferCtxt;
+use crate::next_solver::{
+    Binder, BoundConst, BoundRegion, BoundRegionKind, BoundTy, Canonical, CanonicalVarKind,
+    CanonicalVars, Const, ConstKind, DbInterner, GenericArg, ParamEnvAnd, Placeholder, Region, Ty,
+    TyKind,
+};
+
+/// When we canonicalize a value to form a query, we wind up replacing
+/// various parts of it with canonical variables. This struct stores
+/// those replaced bits to remember for when we process the query
+/// result.
+#[derive(Clone, Debug)]
+pub struct OriginalQueryValues<'db> {
+    /// Map from the universes that appear in the query to the universes in the
+    /// caller context. For all queries except `evaluate_goal` (used by Chalk),
+    /// we only ever put ROOT values into the query, so this map is very
+    /// simple.
+    pub universe_map: SmallVec<[UniverseIndex; 4]>,
+
+    /// This is equivalent to `CanonicalVarValues`, but using a
+    /// `SmallVec` yields a significant performance win.
+    pub var_values: SmallVec<[GenericArg<'db>; 8]>,
+}
+
+impl<'db> Default for OriginalQueryValues<'db> {
+    fn default() -> Self {
+        let mut universe_map = SmallVec::default();
+        universe_map.push(UniverseIndex::ROOT);
+
+        Self { universe_map, var_values: SmallVec::default() }
+    }
+}
+
+impl<'db> InferCtxt<'db> {
+    /// Canonicalizes a query value `V`. When we canonicalize a query,
+    /// we not only canonicalize unbound inference variables, but we
+    /// *also* replace all free regions whatsoever. So for example a
+    /// query like `T: Trait<'static>` would be canonicalized to
+    ///
+    /// ```text
+    /// T: Trait<'?0>
+    /// ```
+    ///
+    /// with a mapping M that maps `'?0` to `'static`.
+    ///
+    /// To get a good understanding of what is happening here, check
+    /// out the [chapter in the rustc dev guide][c].
+    ///
+    /// [c]: https://rust-lang.github.io/chalk/book/canonical_queries/canonicalization.html#canonicalizing-the-query
+    pub fn canonicalize_query<V>(
+        &self,
+        value: ParamEnvAnd<'db, V>,
+        query_state: &mut OriginalQueryValues<'db>,
+    ) -> CanonicalQueryInput<DbInterner<'db>, ParamEnvAnd<'db, V>>
+    where
+        V: TypeFoldable<DbInterner<'db>>,
+    {
+        let (param_env, value) = value.into_parts();
+        // FIXME(#118965): We don't canonicalize the static lifetimes that appear in the
+        // `param_env` because they are treated differently by trait selection.
+        let canonical_param_env = Canonicalizer::canonicalize(
+            param_env,
+            self,
+            self.interner,
+            &CanonicalizeFreeRegionsOtherThanStatic,
+            query_state,
+        );
+
+        let canonical = Canonicalizer::canonicalize_with_base(
+            canonical_param_env,
+            value,
+            self,
+            self.interner,
+            &CanonicalizeAllFreeRegions,
+            query_state,
+        )
+        .unchecked_map(|(param_env, value)| ParamEnvAnd { param_env, value });
+        CanonicalQueryInput { canonical, typing_mode: self.typing_mode() }
+    }
+
+    /// Canonicalizes a query *response* `V`. When we canonicalize a
+    /// query response, we only canonicalize unbound inference
+    /// variables, and we leave other free regions alone. So,
+    /// continuing with the example from `canonicalize_query`, if
+    /// there was an input query `T: Trait<'static>`, it would have
+    /// been canonicalized to
+    ///
+    /// ```text
+    /// T: Trait<'?0>
+    /// ```
+    ///
+    /// with a mapping M that maps `'?0` to `'static`. But if we found that there
+    /// exists only one possible impl of `Trait`, and it looks like
+    /// ```ignore (illustrative)
+    /// impl<T> Trait<'static> for T { .. }
+    /// ```
+    /// then we would prepare a query result R that (among other
+    /// things) includes a mapping to `'?0 := 'static`. When
+    /// canonicalizing this query result R, we would leave this
+    /// reference to `'static` alone.
+    ///
+    /// To get a good understanding of what is happening here, check
+    /// out the [chapter in the rustc dev guide][c].
+    ///
+    /// [c]: https://rust-lang.github.io/chalk/book/canonical_queries/canonicalization.html#canonicalizing-the-query-result
+    pub fn canonicalize_response<V>(&self, value: V) -> Canonical<'db, V>
+    where
+        V: TypeFoldable<DbInterner<'db>>,
+    {
+        let mut query_state = OriginalQueryValues::default();
+        Canonicalizer::canonicalize(
+            value,
+            self,
+            self.interner,
+            &CanonicalizeQueryResponse,
+            &mut query_state,
+        )
+    }
+
+    pub fn canonicalize_user_type_annotation<V>(&self, value: V) -> Canonical<'db, V>
+    where
+        V: TypeFoldable<DbInterner<'db>>,
+    {
+        let mut query_state = OriginalQueryValues::default();
+        Canonicalizer::canonicalize(
+            value,
+            self,
+            self.interner,
+            &CanonicalizeUserTypeAnnotation,
+            &mut query_state,
+        )
+    }
+}
+
+/// Controls how we canonicalize "free regions" that are not inference
+/// variables. This depends on what we are canonicalizing *for* --
+/// e.g., if we are canonicalizing to create a query, we want to
+/// replace those with inference variables, since we want to make a
+/// maximally general query. But if we are canonicalizing a *query
+/// response*, then we don't typically replace free regions, as they
+/// must have been introduced from other parts of the system.
+trait CanonicalizeMode {
+    fn canonicalize_free_region<'db>(
+        &self,
+        canonicalizer: &mut Canonicalizer<'_, 'db>,
+        r: Region<'db>,
+    ) -> Region<'db>;
+
+    fn any(&self) -> bool;
+
+    // Do we preserve universe of variables.
+    fn preserve_universes(&self) -> bool;
+}
+
+struct CanonicalizeQueryResponse;
+
+impl CanonicalizeMode for CanonicalizeQueryResponse {
+    fn canonicalize_free_region<'db>(
+        &self,
+        canonicalizer: &mut Canonicalizer<'_, 'db>,
+        mut r: Region<'db>,
+    ) -> Region<'db> {
+        let infcx = canonicalizer.infcx;
+
+        if let RegionKind::ReVar(vid) = r.kind() {
+            r = infcx
+                .inner
+                .borrow_mut()
+                .unwrap_region_constraints()
+                .opportunistic_resolve_var(canonicalizer.tcx, vid);
+            debug!(
+                "canonical: region var found with vid {vid:?}, \
+                     opportunistically resolved to {r:?}",
+            );
+        };
+
+        match r.kind() {
+            RegionKind::ReLateParam(_)
+            | RegionKind::ReErased
+            | RegionKind::ReStatic
+            | RegionKind::ReEarlyParam(..)
+            | RegionKind::ReError(..) => r,
+
+            RegionKind::RePlaceholder(placeholder) => canonicalizer
+                .canonical_var_for_region(CanonicalVarKind::PlaceholderRegion(placeholder), r),
+
+            RegionKind::ReVar(vid) => {
+                let universe = infcx
+                    .inner
+                    .borrow_mut()
+                    .unwrap_region_constraints()
+                    .probe_value(vid)
+                    .unwrap_err();
+                canonicalizer.canonical_var_for_region(CanonicalVarKind::Region(universe), r)
+            }
+
+            _ => {
+                // Other than `'static` or `'empty`, the query
+                // response should be executing in a fully
+                // canonicalized environment, so there shouldn't be
+                // any other region names it can come up.
+                //
+                // rust-lang/rust#57464: `impl Trait` can leak local
+                // scopes (in manner violating typeck). Therefore, use
+                // `delayed_bug` to allow type error over an ICE.
+                panic!("unexpected region in query response: `{r:?}`");
+            }
+        }
+    }
+
+    fn any(&self) -> bool {
+        false
+    }
+
+    fn preserve_universes(&self) -> bool {
+        true
+    }
+}
+
+struct CanonicalizeUserTypeAnnotation;
+
+impl CanonicalizeMode for CanonicalizeUserTypeAnnotation {
+    fn canonicalize_free_region<'db>(
+        &self,
+        canonicalizer: &mut Canonicalizer<'_, 'db>,
+        r: Region<'db>,
+    ) -> Region<'db> {
+        match r.kind() {
+            RegionKind::ReEarlyParam(_)
+            | RegionKind::ReLateParam(_)
+            | RegionKind::ReErased
+            | RegionKind::ReStatic
+            | RegionKind::ReError(_) => r,
+            RegionKind::ReVar(_) => canonicalizer.canonical_var_for_region_in_root_universe(r),
+            RegionKind::RePlaceholder(..) | RegionKind::ReBound(..) => {
+                // We only expect region names that the user can type.
+                panic!("unexpected region in query response: `{r:?}`")
+            }
+        }
+    }
+
+    fn any(&self) -> bool {
+        false
+    }
+
+    fn preserve_universes(&self) -> bool {
+        false
+    }
+}
+
+struct CanonicalizeAllFreeRegions;
+
+impl CanonicalizeMode for CanonicalizeAllFreeRegions {
+    fn canonicalize_free_region<'db>(
+        &self,
+        canonicalizer: &mut Canonicalizer<'_, 'db>,
+        r: Region<'db>,
+    ) -> Region<'db> {
+        canonicalizer.canonical_var_for_region_in_root_universe(r)
+    }
+
+    fn any(&self) -> bool {
+        true
+    }
+
+    fn preserve_universes(&self) -> bool {
+        false
+    }
+}
+
+struct CanonicalizeFreeRegionsOtherThanStatic;
+
+impl CanonicalizeMode for CanonicalizeFreeRegionsOtherThanStatic {
+    fn canonicalize_free_region<'db>(
+        &self,
+        canonicalizer: &mut Canonicalizer<'_, 'db>,
+        r: Region<'db>,
+    ) -> Region<'db> {
+        if r.is_static() { r } else { canonicalizer.canonical_var_for_region_in_root_universe(r) }
+    }
+
+    fn any(&self) -> bool {
+        true
+    }
+
+    fn preserve_universes(&self) -> bool {
+        false
+    }
+}
+
+struct Canonicalizer<'cx, 'db> {
+    /// Set to `None` to disable the resolution of inference variables.
+    infcx: &'cx InferCtxt<'db>,
+    tcx: DbInterner<'db>,
+    variables: SmallVec<[CanonicalVarKind<'db>; 8]>,
+    query_state: &'cx mut OriginalQueryValues<'db>,
+    // Note that indices is only used once `var_values` is big enough to be
+    // heap-allocated.
+    indices: FxHashMap<GenericArg<'db>, BoundVar>,
+    canonicalize_mode: &'cx dyn CanonicalizeMode,
+    needs_canonical_flags: TypeFlags,
+
+    binder_index: DebruijnIndex,
+}
+
+impl<'cx, 'db> TypeFolder<DbInterner<'db>> for Canonicalizer<'cx, 'db> {
+    fn cx(&self) -> DbInterner<'db> {
+        self.tcx
+    }
+
+    fn fold_binder<T>(&mut self, t: Binder<'db, T>) -> Binder<'db, T>
+    where
+        T: TypeFoldable<DbInterner<'db>>,
+    {
+        self.binder_index.shift_in(1);
+        let t = t.super_fold_with(self);
+        self.binder_index.shift_out(1);
+        t
+    }
+
+    fn fold_region(&mut self, r: Region<'db>) -> Region<'db> {
+        match r.kind() {
+            RegionKind::ReBound(index, ..) => {
+                if index >= self.binder_index {
+                    panic!("escaping late-bound region during canonicalization");
+                } else {
+                    r
+                }
+            }
+
+            RegionKind::ReStatic
+            | RegionKind::ReEarlyParam(..)
+            | RegionKind::ReError(_)
+            | RegionKind::ReLateParam(_)
+            | RegionKind::RePlaceholder(..)
+            | RegionKind::ReVar(_)
+            | RegionKind::ReErased => self.canonicalize_mode.canonicalize_free_region(self, r),
+        }
+    }
+
+    fn fold_ty(&mut self, mut t: Ty<'db>) -> Ty<'db> {
+        match t.kind() {
+            TyKind::Infer(TyVar(mut vid)) => {
+                // We need to canonicalize the *root* of our ty var.
+                // This is so that our canonical response correctly reflects
+                // any equated inference vars correctly!
+                let root_vid = self.infcx.root_var(vid);
+                if root_vid != vid {
+                    t = Ty::new_var(self.tcx, root_vid);
+                    vid = root_vid;
+                }
+
+                debug!("canonical: type var found with vid {:?}", vid);
+                match self.infcx.probe_ty_var(vid) {
+                    // `t` could be a float / int variable; canonicalize that instead.
+                    Ok(t) => {
+                        debug!("(resolved to {:?})", t);
+                        self.fold_ty(t)
+                    }
+
+                    // `TyVar(vid)` is unresolved, track its universe index in the canonicalized
+                    // result.
+                    Err(mut ui) => {
+                        if !self.canonicalize_mode.preserve_universes() {
+                            // FIXME: perf problem described in #55921.
+                            ui = UniverseIndex::ROOT;
+                        }
+                        self.canonicalize_ty_var(
+                            CanonicalVarKind::Ty(CanonicalTyVarKind::General(ui)),
+                            t,
+                        )
+                    }
+                }
+            }
+
+            TyKind::Infer(IntVar(vid)) => {
+                let nt = self.infcx.opportunistic_resolve_int_var(vid);
+                if nt != t {
+                    self.fold_ty(nt)
+                } else {
+                    self.canonicalize_ty_var(CanonicalVarKind::Ty(CanonicalTyVarKind::Int), t)
+                }
+            }
+            TyKind::Infer(FloatVar(vid)) => {
+                let nt = self.infcx.opportunistic_resolve_float_var(vid);
+                if nt != t {
+                    self.fold_ty(nt)
+                } else {
+                    self.canonicalize_ty_var(CanonicalVarKind::Ty(CanonicalTyVarKind::Float), t)
+                }
+            }
+
+            TyKind::Infer(
+                InferTy::FreshTy(_) | InferTy::FreshIntTy(_) | InferTy::FreshFloatTy(_),
+            ) => {
+                panic!("encountered a fresh type during canonicalization")
+            }
+
+            TyKind::Placeholder(mut placeholder) => {
+                if !self.canonicalize_mode.preserve_universes() {
+                    placeholder.universe = UniverseIndex::ROOT;
+                }
+                self.canonicalize_ty_var(CanonicalVarKind::PlaceholderTy(placeholder), t)
+            }
+
+            TyKind::Bound(debruijn, _) => {
+                if debruijn >= self.binder_index {
+                    panic!("escaping bound type during canonicalization")
+                } else {
+                    t
+                }
+            }
+
+            TyKind::Closure(..)
+            | TyKind::CoroutineClosure(..)
+            | TyKind::Coroutine(..)
+            | TyKind::CoroutineWitness(..)
+            | TyKind::Bool
+            | TyKind::Char
+            | TyKind::Int(..)
+            | TyKind::Uint(..)
+            | TyKind::Float(..)
+            | TyKind::Adt(..)
+            | TyKind::Str
+            | TyKind::Error(_)
+            | TyKind::Array(..)
+            | TyKind::Slice(..)
+            | TyKind::RawPtr(..)
+            | TyKind::Ref(..)
+            | TyKind::FnDef(..)
+            | TyKind::FnPtr(..)
+            | TyKind::Dynamic(..)
+            | TyKind::UnsafeBinder(_)
+            | TyKind::Never
+            | TyKind::Tuple(..)
+            | TyKind::Alias(..)
+            | TyKind::Foreign(..)
+            | TyKind::Pat(..)
+            | TyKind::Param(..) => {
+                if t.flags().intersects(self.needs_canonical_flags) {
+                    t.super_fold_with(self)
+                } else {
+                    t
+                }
+            }
+        }
+    }
+
+    fn fold_const(&mut self, mut ct: Const<'db>) -> Const<'db> {
+        match ct.kind() {
+            ConstKind::Infer(InferConst::Var(mut vid)) => {
+                // We need to canonicalize the *root* of our const var.
+                // This is so that our canonical response correctly reflects
+                // any equated inference vars correctly!
+                let root_vid = self.infcx.root_const_var(vid);
+                if root_vid != vid {
+                    ct = Const::new_var(self.tcx, root_vid);
+                    vid = root_vid;
+                }
+
+                debug!("canonical: const var found with vid {:?}", vid);
+                match self.infcx.probe_const_var(vid) {
+                    Ok(c) => {
+                        debug!("(resolved to {:?})", c);
+                        return self.fold_const(c);
+                    }
+
+                    // `ConstVar(vid)` is unresolved, track its universe index in the
+                    // canonicalized result
+                    Err(mut ui) => {
+                        if !self.canonicalize_mode.preserve_universes() {
+                            // FIXME: perf problem described in #55921.
+                            ui = UniverseIndex::ROOT;
+                        }
+                        return self.canonicalize_const_var(CanonicalVarKind::Const(ui), ct);
+                    }
+                }
+            }
+            ConstKind::Infer(InferConst::Fresh(_)) => {
+                panic!("encountered a fresh const during canonicalization")
+            }
+            ConstKind::Bound(debruijn, _) => {
+                if debruijn >= self.binder_index {
+                    panic!("escaping bound const during canonicalization")
+                } else {
+                    return ct;
+                }
+            }
+            ConstKind::Placeholder(placeholder) => {
+                return self
+                    .canonicalize_const_var(CanonicalVarKind::PlaceholderConst(placeholder), ct);
+            }
+            _ => {}
+        }
+
+        if ct.flags().intersects(self.needs_canonical_flags) {
+            ct.super_fold_with(self)
+        } else {
+            ct
+        }
+    }
+}
+
+impl<'cx, 'db> Canonicalizer<'cx, 'db> {
+    /// The main `canonicalize` method, shared impl of
+    /// `canonicalize_query` and `canonicalize_response`.
+    fn canonicalize<V>(
+        value: V,
+        infcx: &InferCtxt<'db>,
+        tcx: DbInterner<'db>,
+        canonicalize_region_mode: &dyn CanonicalizeMode,
+        query_state: &mut OriginalQueryValues<'db>,
+    ) -> Canonical<'db, V>
+    where
+        V: TypeFoldable<DbInterner<'db>>,
+    {
+        let base = Canonical {
+            max_universe: UniverseIndex::ROOT,
+            variables: CanonicalVars::new_from_iter(tcx, []),
+            value: (),
+        };
+        Canonicalizer::canonicalize_with_base(
+            base,
+            value,
+            infcx,
+            tcx,
+            canonicalize_region_mode,
+            query_state,
+        )
+        .unchecked_map(|((), val)| val)
+    }
+
+    fn canonicalize_with_base<U, V>(
+        base: Canonical<'db, U>,
+        value: V,
+        infcx: &InferCtxt<'db>,
+        tcx: DbInterner<'db>,
+        canonicalize_region_mode: &dyn CanonicalizeMode,
+        query_state: &mut OriginalQueryValues<'db>,
+    ) -> Canonical<'db, (U, V)>
+    where
+        V: TypeFoldable<DbInterner<'db>>,
+    {
+        let needs_canonical_flags = if canonicalize_region_mode.any() {
+            TypeFlags::HAS_INFER | TypeFlags::HAS_PLACEHOLDER | TypeFlags::HAS_FREE_REGIONS
+        } else {
+            TypeFlags::HAS_INFER | TypeFlags::HAS_PLACEHOLDER
+        };
+
+        // Fast path: nothing that needs to be canonicalized.
+        if !value.has_type_flags(needs_canonical_flags) {
+            return base.unchecked_map(|b| (b, value));
+        }
+
+        let mut canonicalizer = Canonicalizer {
+            infcx,
+            tcx,
+            canonicalize_mode: canonicalize_region_mode,
+            needs_canonical_flags,
+            variables: SmallVec::from_slice(base.variables.as_slice()),
+            query_state,
+            indices: FxHashMap::default(),
+            binder_index: DebruijnIndex::ZERO,
+        };
+        if canonicalizer.query_state.var_values.spilled() {
+            canonicalizer.indices = canonicalizer
+                .query_state
+                .var_values
+                .iter()
+                .enumerate()
+                .map(|(i, &kind)| (kind, BoundVar::from(i)))
+                .collect();
+        }
+        let out_value = value.fold_with(&mut canonicalizer);
+
+        // Once we have canonicalized `out_value`, it should not
+        // contain anything that ties it to this inference context
+        // anymore.
+        debug_assert!(!out_value.has_infer() && !out_value.has_placeholders());
+
+        let canonical_variables =
+            CanonicalVars::new_from_iter(tcx, canonicalizer.universe_canonicalized_variables());
+
+        let max_universe = canonical_variables
+            .iter()
+            .map(|cvar| cvar.universe())
+            .max()
+            .unwrap_or(UniverseIndex::ROOT);
+
+        Canonical { max_universe, variables: canonical_variables, value: (base.value, out_value) }
+    }
+
+    /// Creates a canonical variable replacing `kind` from the input,
+    /// or returns an existing variable if `kind` has already been
+    /// seen. `kind` is expected to be an unbound variable (or
+    /// potentially a free region).
+    fn canonical_var(&mut self, info: CanonicalVarKind<'db>, kind: GenericArg<'db>) -> BoundVar {
+        let Canonicalizer { variables, query_state, indices, .. } = self;
+
+        let var_values = &mut query_state.var_values;
+
+        let universe = info.universe();
+        if universe != UniverseIndex::ROOT {
+            assert!(self.canonicalize_mode.preserve_universes());
+
+            // Insert universe into the universe map. To preserve the order of the
+            // universes in the value being canonicalized, we don't update the
+            // universe in `info` until we have finished canonicalizing.
+            match query_state.universe_map.binary_search(&universe) {
+                Err(idx) => query_state.universe_map.insert(idx, universe),
+                Ok(_) => {}
+            }
+        }
+
+        // This code is hot. `variables` and `var_values` are usually small
+        // (fewer than 8 elements ~95% of the time). They are SmallVec's to
+        // avoid allocations in those cases. We also don't use `indices` to
+        // determine if a kind has been seen before until the limit of 8 has
+        // been exceeded, to also avoid allocations for `indices`.
+        if !var_values.spilled() {
+            // `var_values` is stack-allocated. `indices` isn't used yet. Do a
+            // direct linear search of `var_values`.
+            if let Some(idx) = var_values.iter().position(|&k| k == kind) {
+                // `kind` is already present in `var_values`.
+                BoundVar::new(idx)
+            } else {
+                // `kind` isn't present in `var_values`. Append it. Likewise
+                // for `info` and `variables`.
+                variables.push(info);
+                var_values.push(kind);
+                assert_eq!(variables.len(), var_values.len());
+
+                // If `var_values` has become big enough to be heap-allocated,
+                // fill up `indices` to facilitate subsequent lookups.
+                if var_values.spilled() {
+                    assert!(indices.is_empty());
+                    *indices = var_values
+                        .iter()
+                        .enumerate()
+                        .map(|(i, &kind)| (kind, BoundVar::new(i)))
+                        .collect();
+                }
+                // The cv is the index of the appended element.
+                BoundVar::new(var_values.len() - 1)
+            }
+        } else {
+            // `var_values` is large. Do a hashmap search via `indices`.
+            *indices.entry(kind).or_insert_with(|| {
+                variables.push(info);
+                var_values.push(kind);
+                assert_eq!(variables.len(), var_values.len());
+                BoundVar::new(variables.len() - 1)
+            })
+        }
+    }
+
+    /// Replaces the universe indexes used in `var_values` with their index in
+    /// `query_state.universe_map`. This minimizes the maximum universe used in
+    /// the canonicalized value.
+    fn universe_canonicalized_variables(self) -> SmallVec<[CanonicalVarKind<'db>; 8]> {
+        if self.query_state.universe_map.len() == 1 {
+            return self.variables;
+        }
+
+        let reverse_universe_map: FxHashMap<UniverseIndex, UniverseIndex> = self
+            .query_state
+            .universe_map
+            .iter()
+            .enumerate()
+            .map(|(idx, universe)| (*universe, UniverseIndex::from_usize(idx)))
+            .collect();
+
+        self.variables
+            .iter()
+            .map(|v| match *v {
+                CanonicalVarKind::Ty(CanonicalTyVarKind::Int | CanonicalTyVarKind::Float) => *v,
+                CanonicalVarKind::Ty(CanonicalTyVarKind::General(u)) => {
+                    CanonicalVarKind::Ty(CanonicalTyVarKind::General(reverse_universe_map[&u]))
+                }
+                CanonicalVarKind::Region(u) => CanonicalVarKind::Region(reverse_universe_map[&u]),
+                CanonicalVarKind::Const(u) => CanonicalVarKind::Const(reverse_universe_map[&u]),
+                CanonicalVarKind::PlaceholderTy(placeholder) => {
+                    CanonicalVarKind::PlaceholderTy(Placeholder {
+                        universe: reverse_universe_map[&placeholder.universe],
+                        ..placeholder
+                    })
+                }
+                CanonicalVarKind::PlaceholderRegion(placeholder) => {
+                    CanonicalVarKind::PlaceholderRegion(Placeholder {
+                        universe: reverse_universe_map[&placeholder.universe],
+                        ..placeholder
+                    })
+                }
+                CanonicalVarKind::PlaceholderConst(placeholder) => {
+                    CanonicalVarKind::PlaceholderConst(Placeholder {
+                        universe: reverse_universe_map[&placeholder.universe],
+                        ..placeholder
+                    })
+                }
+            })
+            .collect()
+    }
+
+    /// Shorthand helper that creates a canonical region variable for
+    /// `r` (always in the root universe). The reason that we always
+    /// put these variables into the root universe is because this
+    /// method is used during **query construction:** in that case, we
+    /// are taking all the regions and just putting them into the most
+    /// generic context we can. This may generate solutions that don't
+    /// fit (e.g., that equate some region variable with a placeholder
+    /// it can't name) on the caller side, but that's ok, the caller
+    /// can figure that out. In the meantime, it maximizes our
+    /// caching.
+    ///
+    /// (This works because unification never fails -- and hence trait
+    /// selection is never affected -- due to a universe mismatch.)
+    fn canonical_var_for_region_in_root_universe(&mut self, r: Region<'db>) -> Region<'db> {
+        self.canonical_var_for_region(CanonicalVarKind::Region(UniverseIndex::ROOT), r)
+    }
+
+    /// Creates a canonical variable (with the given `info`)
+    /// representing the region `r`; return a region referencing it.
+    fn canonical_var_for_region(
+        &mut self,
+        info: CanonicalVarKind<'db>,
+        r: Region<'db>,
+    ) -> Region<'db> {
+        let var = self.canonical_var(info, r.into());
+        let br = BoundRegion { var, kind: BoundRegionKind::Anon };
+        Region::new_bound(self.cx(), self.binder_index, br)
+    }
+
+    /// Given a type variable `ty_var` of the given kind, first check
+    /// if `ty_var` is bound to anything; if so, canonicalize
+    /// *that*. Otherwise, create a new canonical variable for
+    /// `ty_var`.
+    fn canonicalize_ty_var(&mut self, info: CanonicalVarKind<'db>, ty_var: Ty<'db>) -> Ty<'db> {
+        debug_assert_eq!(ty_var, self.infcx.shallow_resolve(ty_var));
+        let var = self.canonical_var(info, ty_var.into());
+        Ty::new_bound(
+            self.tcx,
+            self.binder_index,
+            BoundTy { kind: crate::next_solver::BoundTyKind::Anon, var },
+        )
+    }
+
+    /// Given a type variable `const_var` of the given kind, first check
+    /// if `const_var` is bound to anything; if so, canonicalize
+    /// *that*. Otherwise, create a new canonical variable for
+    /// `const_var`.
+    fn canonicalize_const_var(
+        &mut self,
+        info: CanonicalVarKind<'db>,
+        const_var: Const<'db>,
+    ) -> Const<'db> {
+        debug_assert_eq!(const_var, self.infcx.shallow_resolve_const(const_var));
+        let var = self.canonical_var(info, const_var.into());
+        Const::new_bound(self.tcx, self.binder_index, BoundConst { var })
+    }
+}
diff --git a/crates/hir-ty/src/next_solver/infer/canonical/mod.rs b/crates/hir-ty/src/next_solver/infer/canonical/mod.rs
index 4457e1340d58..ec41111ed815 100644
--- a/crates/hir-ty/src/next_solver/infer/canonical/mod.rs
+++ b/crates/hir-ty/src/next_solver/infer/canonical/mod.rs
@@ -42,6 +42,7 @@ use rustc_type_ir::{
     },
 };
 
+pub mod canonicalizer;
 pub mod instantiate;
 
 impl<'db> InferCtxt<'db> {
diff --git a/crates/hir-ty/src/next_solver/infer/mod.rs b/crates/hir-ty/src/next_solver/infer/mod.rs
index 585719144ef4..2630f2a8cc4e 100644
--- a/crates/hir-ty/src/next_solver/infer/mod.rs
+++ b/crates/hir-ty/src/next_solver/infer/mod.rs
@@ -190,12 +190,13 @@ impl<'db> InferCtxtInner<'db> {
     }
 
     #[inline]
-    fn int_unification_table(&mut self) -> UnificationTable<'_, 'db, IntVid> {
+    pub(crate) fn int_unification_table(&mut self) -> UnificationTable<'_, 'db, IntVid> {
+        tracing::debug!(?self.int_unification_storage);
         self.int_unification_storage.with_log(&mut self.undo_log)
     }
 
     #[inline]
-    fn float_unification_table(&mut self) -> UnificationTable<'_, 'db, FloatVid> {
+    pub(crate) fn float_unification_table(&mut self) -> UnificationTable<'_, 'db, FloatVid> {
         self.float_unification_storage.with_log(&mut self.undo_log)
     }
 
@@ -213,6 +214,7 @@ impl<'db> InferCtxtInner<'db> {
     }
 }
 
+#[derive(Clone)]
 pub struct InferCtxt<'db> {
     pub interner: DbInterner<'db>,
 
@@ -500,6 +502,13 @@ impl<'db> InferCtxt<'db> {
         self.next_ty_var_with_origin(TypeVariableOrigin { param_def_id: None })
     }
 
+    pub fn next_ty_vid(&self) -> TyVid {
+        self.inner
+            .borrow_mut()
+            .type_variables()
+            .new_var(self.universe(), TypeVariableOrigin { param_def_id: None })
+    }
+
     pub fn next_ty_var_with_origin(&self, origin: TypeVariableOrigin) -> Ty<'db> {
         let vid = self.inner.borrow_mut().type_variables().new_var(self.universe(), origin);
         Ty::new_var(self.interner, vid)
@@ -519,6 +528,17 @@ impl<'db> InferCtxt<'db> {
         self.next_const_var_with_origin(ConstVariableOrigin { param_def_id: None })
     }
 
+    pub fn next_const_vid(&self) -> ConstVid {
+        self.inner
+            .borrow_mut()
+            .const_unification_table()
+            .new_key(ConstVariableValue::Unknown {
+                origin: ConstVariableOrigin { param_def_id: None },
+                universe: self.universe(),
+            })
+            .vid
+    }
+
     pub fn next_const_var_with_origin(&self, origin: ConstVariableOrigin) -> Const<'db> {
         let vid = self
             .inner
@@ -546,10 +566,16 @@ impl<'db> InferCtxt<'db> {
         Ty::new_int_var(self.interner, next_int_var_id)
     }
 
+    pub fn next_int_vid(&self) -> IntVid {
+        self.inner.borrow_mut().int_unification_table().new_key(IntVarValue::Unknown)
+    }
+
     pub fn next_float_var(&self) -> Ty<'db> {
-        let next_float_var_id =
-            self.inner.borrow_mut().float_unification_table().new_key(FloatVarValue::Unknown);
-        Ty::new_float_var(self.interner, next_float_var_id)
+        Ty::new_float_var(self.interner, self.next_float_vid())
+    }
+
+    pub fn next_float_vid(&self) -> FloatVid {
+        self.inner.borrow_mut().float_unification_table().new_key(FloatVarValue::Unknown)
     }
 
     /// Creates a fresh region variable with the next available index.
@@ -559,6 +585,10 @@ impl<'db> InferCtxt<'db> {
         self.next_region_var_in_universe(self.universe())
     }
 
+    pub fn next_region_vid(&self) -> RegionVid {
+        self.inner.borrow_mut().unwrap_region_constraints().new_region_var(self.universe())
+    }
+
     /// Creates a fresh region variable with the next available index
     /// in the given universe; typically, you can use
     /// `next_region_var` and just use the maximal universe.
@@ -782,6 +812,16 @@ impl<'db> InferCtxt<'db> {
         }
     }
 
+    pub fn resolve_int_var(&self, vid: IntVid) -> Option<Ty<'db>> {
+        let mut inner = self.inner.borrow_mut();
+        let value = inner.int_unification_table().probe_value(vid);
+        match value {
+            IntVarValue::IntType(ty) => Some(Ty::new_int(self.interner, ty)),
+            IntVarValue::UintType(ty) => Some(Ty::new_uint(self.interner, ty)),
+            IntVarValue::Unknown => None,
+        }
+    }
+
     /// Resolves a float var to a rigid int type, if it was constrained to one,
     /// or else the root float var in the unification table.
     pub fn opportunistic_resolve_float_var(&self, vid: FloatVid) -> Ty<'db> {
@@ -795,6 +835,15 @@ impl<'db> InferCtxt<'db> {
         }
     }
 
+    pub fn resolve_float_var(&self, vid: FloatVid) -> Option<Ty<'db>> {
+        let mut inner = self.inner.borrow_mut();
+        let value = inner.float_unification_table().probe_value(vid);
+        match value {
+            FloatVarValue::Known(ty) => Some(Ty::new_float(self.interner, ty)),
+            FloatVarValue::Unknown => None,
+        }
+    }
+
     /// Where possible, replaces type/const variables in
     /// `value` with their final value. Note that region variables
     /// are unaffected. If a type/const variable has not been unified, it
diff --git a/crates/hir-ty/src/next_solver/infer/snapshot/mod.rs b/crates/hir-ty/src/next_solver/infer/snapshot/mod.rs
index eb426205575a..8c7dfb25e07f 100644
--- a/crates/hir-ty/src/next_solver/infer/snapshot/mod.rs
+++ b/crates/hir-ty/src/next_solver/infer/snapshot/mod.rs
@@ -46,7 +46,7 @@ impl<'db> InferCtxt<'db> {
         UndoLogs::<UndoLog<'db>>::num_open_snapshots(&self.inner.borrow_mut().undo_log)
     }
 
-    fn start_snapshot(&self) -> CombinedSnapshot {
+    pub(crate) fn start_snapshot(&self) -> CombinedSnapshot {
         debug!("start_snapshot()");
 
         let mut inner = self.inner.borrow_mut();
@@ -59,7 +59,7 @@ impl<'db> InferCtxt<'db> {
     }
 
     #[instrument(skip(self, snapshot), level = "debug")]
-    fn rollback_to(&self, snapshot: CombinedSnapshot) {
+    pub(crate) fn rollback_to(&self, snapshot: CombinedSnapshot) {
         let CombinedSnapshot { undo_snapshot, region_constraints_snapshot, universe } = snapshot;
 
         self.universe.set(universe);
diff --git a/crates/hir-ty/src/next_solver/mapping.rs b/crates/hir-ty/src/next_solver/mapping.rs
index dc54ee7d5878..f66b8dace30a 100644
--- a/crates/hir-ty/src/next_solver/mapping.rs
+++ b/crates/hir-ty/src/next_solver/mapping.rs
@@ -2,8 +2,8 @@
 
 use base_db::Crate;
 use chalk_ir::{
-    CanonicalVarKind, CanonicalVarKinds, ForeignDefId, InferenceVar, Substitution, TyVariableKind,
-    WellFormed, fold::Shift, interner::HasInterner,
+    CanonicalVarKind, CanonicalVarKinds, FnPointer, InferenceVar, Substitution, TyVariableKind,
+    WellFormed, cast::Cast, fold::Shift, interner::HasInterner,
 };
 use hir_def::{
     CallableDefId, ConstParamId, FunctionId, GeneralConstId, LifetimeParamId, TypeAliasId,
@@ -24,12 +24,12 @@ use salsa::{Id, plumbing::AsId};
 
 use crate::next_solver::BoundConst;
 use crate::{
-    ConcreteConst, ConstScalar, ImplTraitId, Interner, MemoryMap,
+    ConstScalar, ImplTraitId, Interner, MemoryMap,
     db::{
         HirDatabase, InternedClosureId, InternedCoroutineId, InternedLifetimeParamId,
         InternedOpaqueTyId, InternedTypeOrConstParamId,
     },
-    from_assoc_type_id, from_chalk_trait_id,
+    from_assoc_type_id, from_chalk_trait_id, from_foreign_def_id,
     mapping::ToChalk,
     next_solver::{
         Binder, ClauseKind, ConstBytes, TraitPredicate, UnevaluatedConst,
@@ -143,6 +143,10 @@ pub trait ChalkToNextSolver<'db, Out> {
     fn to_nextsolver(&self, interner: DbInterner<'db>) -> Out;
 }
 
+pub trait NextSolverToChalk<'db, Out> {
+    fn to_chalk(self, interner: DbInterner<'db>) -> Out;
+}
+
 impl<'db> ChalkToNextSolver<'db, Ty<'db>> for chalk_ir::Ty<Interner> {
     fn to_nextsolver(&self, interner: DbInterner<'db>) -> Ty<'db> {
         Ty::new(
@@ -429,6 +433,12 @@ impl<'db> ChalkToNextSolver<'db, Ty<'db>> for chalk_ir::Ty<Interner> {
     }
 }
 
+impl<'db> NextSolverToChalk<'db, chalk_ir::Ty<Interner>> for Ty<'db> {
+    fn to_chalk(self, interner: DbInterner<'db>) -> chalk_ir::Ty<Interner> {
+        convert_ty_for_result(interner, self)
+    }
+}
+
 impl<'db> ChalkToNextSolver<'db, Region<'db>> for chalk_ir::Lifetime<Interner> {
     fn to_nextsolver(&self, interner: DbInterner<'db>) -> Region<'db> {
         Region::new(
@@ -463,6 +473,12 @@ impl<'db> ChalkToNextSolver<'db, Region<'db>> for chalk_ir::Lifetime<Interner> {
     }
 }
 
+impl<'db> NextSolverToChalk<'db, chalk_ir::Lifetime<Interner>> for Region<'db> {
+    fn to_chalk(self, interner: DbInterner<'db>) -> chalk_ir::Lifetime<Interner> {
+        convert_region_for_result(interner, self)
+    }
+}
+
 impl<'db> ChalkToNextSolver<'db, Const<'db>> for chalk_ir::Const<Interner> {
     fn to_nextsolver(&self, interner: DbInterner<'db>) -> Const<'db> {
         let data = self.data(Interner);
@@ -507,6 +523,12 @@ impl<'db> ChalkToNextSolver<'db, Const<'db>> for chalk_ir::Const<Interner> {
     }
 }
 
+impl<'db> NextSolverToChalk<'db, chalk_ir::Const<Interner>> for Const<'db> {
+    fn to_chalk(self, interner: DbInterner<'db>) -> chalk_ir::Const<Interner> {
+        convert_const_for_result(interner, self)
+    }
+}
+
 impl<'db> ChalkToNextSolver<'db, rustc_type_ir::FnSigTys<DbInterner<'db>>>
     for chalk_ir::FnSubst<Interner>
 {
@@ -566,6 +588,7 @@ impl<'db> ChalkToNextSolver<'db, GenericArg<'db>> for chalk_ir::GenericArg<Inter
         }
     }
 }
+
 impl<'db> ChalkToNextSolver<'db, GenericArgs<'db>> for chalk_ir::Substitution<Interner> {
     fn to_nextsolver(&self, interner: DbInterner<'db>) -> GenericArgs<'db> {
         GenericArgs::new_from_iter(
@@ -575,6 +598,12 @@ impl<'db> ChalkToNextSolver<'db, GenericArgs<'db>> for chalk_ir::Substitution<In
     }
 }
 
+impl<'db> NextSolverToChalk<'db, chalk_ir::Substitution<Interner>> for GenericArgs<'db> {
+    fn to_chalk(self, interner: DbInterner<'db>) -> chalk_ir::Substitution<Interner> {
+        convert_args_for_result(interner, self.as_slice())
+    }
+}
+
 impl<'db> ChalkToNextSolver<'db, Tys<'db>> for chalk_ir::Substitution<Interner> {
     fn to_nextsolver(&self, interner: DbInterner<'db>) -> Tys<'db> {
         Tys::new_from_iter(
@@ -591,17 +620,29 @@ impl<'db> ChalkToNextSolver<'db, Tys<'db>> for chalk_ir::Substitution<Interner>
 }
 
 impl<'db> ChalkToNextSolver<'db, rustc_type_ir::DebruijnIndex> for chalk_ir::DebruijnIndex {
-    fn to_nextsolver(&self, interner: DbInterner<'db>) -> rustc_type_ir::DebruijnIndex {
+    fn to_nextsolver(&self, _interner: DbInterner<'db>) -> rustc_type_ir::DebruijnIndex {
         rustc_type_ir::DebruijnIndex::from_u32(self.depth())
     }
 }
 
+impl<'db> NextSolverToChalk<'db, chalk_ir::DebruijnIndex> for rustc_type_ir::DebruijnIndex {
+    fn to_chalk(self, _interner: DbInterner<'db>) -> chalk_ir::DebruijnIndex {
+        chalk_ir::DebruijnIndex::new(self.index() as u32)
+    }
+}
+
 impl<'db> ChalkToNextSolver<'db, rustc_type_ir::UniverseIndex> for chalk_ir::UniverseIndex {
-    fn to_nextsolver(&self, interner: DbInterner<'db>) -> rustc_type_ir::UniverseIndex {
+    fn to_nextsolver(&self, _interner: DbInterner<'db>) -> rustc_type_ir::UniverseIndex {
         rustc_type_ir::UniverseIndex::from_u32(self.counter as u32)
     }
 }
 
+impl<'db> NextSolverToChalk<'db, chalk_ir::UniverseIndex> for rustc_type_ir::UniverseIndex {
+    fn to_chalk(self, _interner: DbInterner<'db>) -> chalk_ir::UniverseIndex {
+        chalk_ir::UniverseIndex { counter: self.index() }
+    }
+}
+
 impl<'db> ChalkToNextSolver<'db, rustc_type_ir::InferTy>
     for (chalk_ir::InferenceVar, chalk_ir::TyVariableKind)
 {
@@ -640,14 +681,55 @@ impl<'db> ChalkToNextSolver<'db, rustc_type_ir::Variance> for crate::Variance {
     }
 }
 
-impl<'db> ChalkToNextSolver<'db, Canonical<'db, Goal<DbInterner<'db>, Predicate<'db>>>>
-    for chalk_ir::Canonical<chalk_ir::InEnvironment<chalk_ir::Goal<Interner>>>
+impl<'db> ChalkToNextSolver<'db, rustc_type_ir::Variance> for chalk_ir::Variance {
+    fn to_nextsolver(&self, interner: DbInterner<'db>) -> rustc_type_ir::Variance {
+        match self {
+            chalk_ir::Variance::Covariant => rustc_type_ir::Variance::Covariant,
+            chalk_ir::Variance::Invariant => rustc_type_ir::Variance::Invariant,
+            chalk_ir::Variance::Contravariant => rustc_type_ir::Variance::Contravariant,
+        }
+    }
+}
+
+impl<'db> ChalkToNextSolver<'db, VariancesOf> for chalk_ir::Variances<Interner> {
+    fn to_nextsolver(&self, interner: DbInterner<'db>) -> VariancesOf {
+        VariancesOf::new_from_iter(
+            interner,
+            self.as_slice(Interner).iter().map(|v| v.to_nextsolver(interner)),
+        )
+    }
+}
+
+impl<'db> ChalkToNextSolver<'db, Goal<DbInterner<'db>, Predicate<'db>>>
+    for chalk_ir::InEnvironment<chalk_ir::Goal<Interner>>
 {
-    fn to_nextsolver(
-        &self,
+    fn to_nextsolver(&self, interner: DbInterner<'db>) -> Goal<DbInterner<'db>, Predicate<'db>> {
+        Goal::new(
+            interner,
+            self.environment.to_nextsolver(interner),
+            self.goal.to_nextsolver(interner),
+        )
+    }
+}
+
+impl<'db> NextSolverToChalk<'db, chalk_ir::InEnvironment<chalk_ir::Goal<Interner>>>
+    for Goal<DbInterner<'db>, Predicate<'db>>
+{
+    fn to_chalk(
+        self,
         interner: DbInterner<'db>,
-    ) -> Canonical<'db, Goal<DbInterner<'db>, Predicate<'db>>> {
-        let param_env = self.value.environment.to_nextsolver(interner);
+    ) -> chalk_ir::InEnvironment<chalk_ir::Goal<Interner>> {
+        chalk_ir::InEnvironment {
+            environment: self.param_env.to_chalk(interner),
+            goal: self.predicate.to_chalk(interner),
+        }
+    }
+}
+
+impl<'db, T: HasInterner<Interner = Interner> + ChalkToNextSolver<'db, U>, U>
+    ChalkToNextSolver<'db, Canonical<'db, U>> for chalk_ir::Canonical<T>
+{
+    fn to_nextsolver(&self, interner: DbInterner<'db>) -> Canonical<'db, U> {
         let variables = CanonicalVars::new_from_iter(
             interner,
             self.binders.iter(Interner).map(|k| match &k.kind {
@@ -672,12 +754,55 @@ impl<'db> ChalkToNextSolver<'db, Canonical<'db, Goal<DbInterner<'db>, Predicate<
         );
         Canonical {
             max_universe: UniverseIndex::ROOT,
-            value: Goal::new(interner, param_env, self.value.goal.to_nextsolver(interner)),
+            value: self.value.to_nextsolver(interner),
             variables,
         }
     }
 }
 
+impl<'db, T: NextSolverToChalk<'db, U>, U: HasInterner<Interner = Interner>>
+    NextSolverToChalk<'db, chalk_ir::Canonical<U>> for Canonical<'db, T>
+{
+    fn to_chalk(self, interner: DbInterner<'db>) -> chalk_ir::Canonical<U> {
+        let binders = chalk_ir::CanonicalVarKinds::from_iter(
+            Interner,
+            self.variables.iter().map(|v| match v {
+                rustc_type_ir::CanonicalVarKind::Ty(
+                    rustc_type_ir::CanonicalTyVarKind::General(ui),
+                ) => chalk_ir::CanonicalVarKind::new(
+                    chalk_ir::VariableKind::Ty(TyVariableKind::General),
+                    chalk_ir::UniverseIndex { counter: ui.as_usize() },
+                ),
+                rustc_type_ir::CanonicalVarKind::Ty(rustc_type_ir::CanonicalTyVarKind::Int) => {
+                    chalk_ir::CanonicalVarKind::new(
+                        chalk_ir::VariableKind::Ty(TyVariableKind::Integer),
+                        chalk_ir::UniverseIndex::root(),
+                    )
+                }
+                rustc_type_ir::CanonicalVarKind::Ty(rustc_type_ir::CanonicalTyVarKind::Float) => {
+                    chalk_ir::CanonicalVarKind::new(
+                        chalk_ir::VariableKind::Ty(TyVariableKind::Float),
+                        chalk_ir::UniverseIndex::root(),
+                    )
+                }
+                rustc_type_ir::CanonicalVarKind::Region(ui) => chalk_ir::CanonicalVarKind::new(
+                    chalk_ir::VariableKind::Lifetime,
+                    chalk_ir::UniverseIndex { counter: ui.as_usize() },
+                ),
+                rustc_type_ir::CanonicalVarKind::Const(ui) => chalk_ir::CanonicalVarKind::new(
+                    chalk_ir::VariableKind::Const(chalk_ir::TyKind::Error.intern(Interner)),
+                    chalk_ir::UniverseIndex { counter: ui.as_usize() },
+                ),
+                rustc_type_ir::CanonicalVarKind::PlaceholderTy(_) => unimplemented!(),
+                rustc_type_ir::CanonicalVarKind::PlaceholderRegion(_) => unimplemented!(),
+                rustc_type_ir::CanonicalVarKind::PlaceholderConst(_) => unimplemented!(),
+            }),
+        );
+        let value = self.value.to_chalk(interner);
+        chalk_ir::Canonical { binders, value }
+    }
+}
+
 impl<'db> ChalkToNextSolver<'db, Predicate<'db>> for chalk_ir::Goal<Interner> {
     fn to_nextsolver(&self, interner: DbInterner<'db>) -> Predicate<'db> {
         match self.data(Interner) {
@@ -693,7 +818,23 @@ impl<'db> ChalkToNextSolver<'db, Predicate<'db>> for chalk_ir::Goal<Interner> {
             }
             chalk_ir::GoalData::All(goals) => panic!("Should not be constructed."),
             chalk_ir::GoalData::Not(goal) => panic!("Should not be constructed."),
-            chalk_ir::GoalData::EqGoal(eq_goal) => panic!("Should not be constructed."),
+            chalk_ir::GoalData::EqGoal(eq_goal) => {
+                let arg_to_term = |g: &chalk_ir::GenericArg<Interner>| match g.data(Interner) {
+                    chalk_ir::GenericArgData::Ty(ty) => Term::Ty(ty.to_nextsolver(interner)),
+                    chalk_ir::GenericArgData::Const(const_) => {
+                        Term::Const(const_.to_nextsolver(interner))
+                    }
+                    chalk_ir::GenericArgData::Lifetime(lifetime) => unreachable!(),
+                };
+                let pred_kind = PredicateKind::AliasRelate(
+                    arg_to_term(&eq_goal.a),
+                    arg_to_term(&eq_goal.b),
+                    rustc_type_ir::AliasRelationDirection::Equate,
+                );
+                let pred_kind =
+                    Binder::bind_with_vars(pred_kind, BoundVarKinds::new_from_iter(interner, []));
+                Predicate::new(interner, pred_kind)
+            }
             chalk_ir::GoalData::SubtypeGoal(subtype_goal) => {
                 let subtype_predicate = SubtypePredicate {
                     a: subtype_goal.a.to_nextsolver(interner),
@@ -720,6 +861,12 @@ impl<'db> ChalkToNextSolver<'db, Predicate<'db>> for chalk_ir::Goal<Interner> {
     }
 }
 
+impl<'db> NextSolverToChalk<'db, chalk_ir::Goal<Interner>> for Predicate<'db> {
+    fn to_chalk(self, interner: DbInterner<'db>) -> chalk_ir::Goal<Interner> {
+        chalk_ir::Goal::new(Interner, self.kind().skip_binder().to_chalk(interner))
+    }
+}
+
 impl<'db> ChalkToNextSolver<'db, ParamEnv<'db>> for chalk_ir::Environment<Interner> {
     fn to_nextsolver(&self, interner: DbInterner<'db>) -> ParamEnv<'db> {
         let clauses = Clauses::new_from_iter(
@@ -732,12 +879,38 @@ impl<'db> ChalkToNextSolver<'db, ParamEnv<'db>> for chalk_ir::Environment<Intern
     }
 }
 
+impl<'db> NextSolverToChalk<'db, chalk_ir::Environment<Interner>> for ParamEnv<'db> {
+    fn to_chalk(self, interner: DbInterner<'db>) -> chalk_ir::Environment<Interner> {
+        let clauses = chalk_ir::ProgramClauses::from_iter(
+            Interner,
+            self.clauses.iter().filter_map(|c| -> Option<chalk_ir::ProgramClause<Interner>> {
+                c.to_chalk(interner)
+            }),
+        );
+        chalk_ir::Environment { clauses }
+    }
+}
+
 impl<'db> ChalkToNextSolver<'db, Clause<'db>> for chalk_ir::ProgramClause<Interner> {
     fn to_nextsolver(&self, interner: DbInterner<'db>) -> Clause<'db> {
         Clause(Predicate::new(interner, self.data(Interner).0.to_nextsolver(interner)))
     }
 }
 
+impl<'db> NextSolverToChalk<'db, Option<chalk_ir::ProgramClause<Interner>>> for Clause<'db> {
+    fn to_chalk(self, interner: DbInterner<'db>) -> Option<chalk_ir::ProgramClause<Interner>> {
+        let value: chalk_ir::ProgramClauseImplication<Interner> =
+            <PredicateKind<'db> as NextSolverToChalk<
+                'db,
+                Option<chalk_ir::ProgramClauseImplication<Interner>>,
+            >>::to_chalk(self.0.kind().skip_binder(), interner)?;
+        Some(chalk_ir::ProgramClause::new(
+            Interner,
+            chalk_ir::ProgramClauseData(chalk_ir::Binders::empty(Interner, value)),
+        ))
+    }
+}
+
 impl<'db> ChalkToNextSolver<'db, PredicateKind<'db>>
     for chalk_ir::ProgramClauseImplication<Interner>
 {
@@ -748,6 +921,26 @@ impl<'db> ChalkToNextSolver<'db, PredicateKind<'db>>
     }
 }
 
+impl<'db> NextSolverToChalk<'db, Option<chalk_ir::ProgramClauseImplication<Interner>>>
+    for PredicateKind<'db>
+{
+    fn to_chalk(
+        self,
+        interner: DbInterner<'db>,
+    ) -> Option<chalk_ir::ProgramClauseImplication<Interner>> {
+        let chalk_ir::GoalData::DomainGoal(consequence) = self.to_chalk(interner) else {
+            return None;
+        };
+
+        Some(chalk_ir::ProgramClauseImplication {
+            consequence,
+            conditions: chalk_ir::Goals::empty(Interner),
+            constraints: chalk_ir::Constraints::empty(Interner),
+            priority: chalk_ir::ClausePriority::High,
+        })
+    }
+}
+
 impl<'db> ChalkToNextSolver<'db, PredicateKind<'db>> for chalk_ir::DomainGoal<Interner> {
     fn to_nextsolver(&self, interner: DbInterner<'db>) -> PredicateKind<'db> {
         match self {
@@ -866,6 +1059,85 @@ impl<'db> ChalkToNextSolver<'db, PredicateKind<'db>> for chalk_ir::DomainGoal<In
     }
 }
 
+impl<'db> NextSolverToChalk<'db, chalk_ir::GoalData<Interner>> for PredicateKind<'db> {
+    fn to_chalk(self, interner: DbInterner<'db>) -> chalk_ir::GoalData<Interner> {
+        match self {
+            rustc_type_ir::PredicateKind::Clause(rustc_type_ir::ClauseKind::Trait(trait_pred)) => {
+                let trait_ref = trait_pred.trait_ref.to_chalk(interner);
+                let where_clause = chalk_ir::WhereClause::Implemented(trait_ref);
+                chalk_ir::GoalData::DomainGoal(chalk_ir::DomainGoal::Holds(where_clause))
+            }
+            rustc_type_ir::PredicateKind::Clause(rustc_type_ir::ClauseKind::Projection(
+                proj_predicate,
+            )) => {
+                let associated_ty_id = match proj_predicate.def_id() {
+                    SolverDefId::TypeAliasId(id) => to_assoc_type_id(id),
+                    _ => unreachable!(),
+                };
+                let substitution = proj_predicate.projection_term.args.to_chalk(interner);
+                let alias = chalk_ir::AliasTy::Projection(chalk_ir::ProjectionTy {
+                    associated_ty_id,
+                    substitution,
+                });
+                let ty = match proj_predicate.term.kind() {
+                    rustc_type_ir::TermKind::Ty(ty) => ty,
+                    rustc_type_ir::TermKind::Const(_) => unimplemented!(),
+                };
+                let ty = ty.to_chalk(interner);
+                let alias_eq = chalk_ir::AliasEq { alias, ty };
+                let where_clause = chalk_ir::WhereClause::AliasEq(alias_eq);
+                chalk_ir::GoalData::DomainGoal(chalk_ir::DomainGoal::Holds(where_clause))
+            }
+            rustc_type_ir::PredicateKind::Clause(rustc_type_ir::ClauseKind::TypeOutlives(
+                outlives,
+            )) => {
+                let lifetime = outlives.1.to_chalk(interner);
+                let ty = outlives.0.to_chalk(interner);
+                let where_clause =
+                    chalk_ir::WhereClause::TypeOutlives(chalk_ir::TypeOutlives { lifetime, ty });
+                chalk_ir::GoalData::DomainGoal(chalk_ir::DomainGoal::Holds(where_clause))
+            }
+            rustc_type_ir::PredicateKind::Clause(rustc_type_ir::ClauseKind::RegionOutlives(
+                outlives,
+            )) => {
+                let a = outlives.0.to_chalk(interner);
+                let b = outlives.1.to_chalk(interner);
+                let where_clause =
+                    chalk_ir::WhereClause::LifetimeOutlives(chalk_ir::LifetimeOutlives { a, b });
+                chalk_ir::GoalData::DomainGoal(chalk_ir::DomainGoal::Holds(where_clause))
+            }
+            rustc_type_ir::PredicateKind::AliasRelate(
+                alias_term,
+                target_term,
+                alias_relation_direction,
+            ) => {
+                let term_to_generic_arg = |term: Term<'db>| match term {
+                    Term::Ty(ty) => chalk_ir::GenericArg::new(
+                        Interner,
+                        chalk_ir::GenericArgData::Ty(ty.to_chalk(interner)),
+                    ),
+                    Term::Const(const_) => chalk_ir::GenericArg::new(
+                        Interner,
+                        chalk_ir::GenericArgData::Const(const_.to_chalk(interner)),
+                    ),
+                };
+
+                chalk_ir::GoalData::EqGoal(chalk_ir::EqGoal {
+                    a: term_to_generic_arg(alias_term),
+                    b: term_to_generic_arg(target_term),
+                })
+            }
+            rustc_type_ir::PredicateKind::Clause(_) => unimplemented!(),
+            rustc_type_ir::PredicateKind::DynCompatible(_) => unimplemented!(),
+            rustc_type_ir::PredicateKind::Subtype(_) => unimplemented!(),
+            rustc_type_ir::PredicateKind::Coerce(_) => unimplemented!(),
+            rustc_type_ir::PredicateKind::ConstEquate(_, _) => unimplemented!(),
+            rustc_type_ir::PredicateKind::Ambiguous => unimplemented!(),
+            rustc_type_ir::PredicateKind::NormalizesTo(_) => unimplemented!(),
+        }
+    }
+}
+
 impl<'db> ChalkToNextSolver<'db, TraitRef<'db>> for chalk_ir::TraitRef<Interner> {
     fn to_nextsolver(&self, interner: DbInterner<'db>) -> TraitRef<'db> {
         let args = self.substitution.to_nextsolver(interner);
@@ -873,6 +1145,14 @@ impl<'db> ChalkToNextSolver<'db, TraitRef<'db>> for chalk_ir::TraitRef<Interner>
     }
 }
 
+impl<'db> NextSolverToChalk<'db, chalk_ir::TraitRef<Interner>> for TraitRef<'db> {
+    fn to_chalk(self, interner: DbInterner<'db>) -> chalk_ir::TraitRef<Interner> {
+        let trait_id = to_chalk_trait_id(self.def_id.0);
+        let substitution = self.args.to_chalk(interner);
+        chalk_ir::TraitRef { trait_id, substitution }
+    }
+}
+
 impl<'db> ChalkToNextSolver<'db, PredicateKind<'db>> for chalk_ir::WhereClause<Interner> {
     fn to_nextsolver(&self, interner: DbInterner<'db>) -> PredicateKind<'db> {
         match self {
@@ -913,52 +1193,23 @@ impl<'db> ChalkToNextSolver<'db, PredicateKind<'db>> for chalk_ir::WhereClause<I
     }
 }
 
+impl<'db, I> NextSolverToChalk<'db, chalk_ir::ConstrainedSubst<Interner>> for I
+where
+    I: IntoIterator<Item = GenericArg<'db>>,
+{
+    fn to_chalk(self, interner: DbInterner<'db>) -> chalk_ir::ConstrainedSubst<Interner> {
+        chalk_ir::ConstrainedSubst {
+            constraints: chalk_ir::Constraints::empty(Interner),
+            subst: GenericArgs::new_from_iter(interner, self).to_chalk(interner),
+        }
+    }
+}
+
 pub fn convert_canonical_args_for_result<'db>(
     interner: DbInterner<'db>,
     args: Canonical<'db, Vec<GenericArg<'db>>>,
 ) -> chalk_ir::Canonical<chalk_ir::ConstrainedSubst<Interner>> {
-    let Canonical { value, variables, max_universe } = args;
-    let binders = CanonicalVarKinds::from_iter(
-        Interner,
-        variables.iter().map(|v| match v {
-            rustc_type_ir::CanonicalVarKind::Ty(rustc_type_ir::CanonicalTyVarKind::General(_)) => {
-                CanonicalVarKind::new(
-                    chalk_ir::VariableKind::Ty(TyVariableKind::General),
-                    chalk_ir::UniverseIndex::ROOT,
-                )
-            }
-            rustc_type_ir::CanonicalVarKind::Ty(rustc_type_ir::CanonicalTyVarKind::Int) => {
-                CanonicalVarKind::new(
-                    chalk_ir::VariableKind::Ty(TyVariableKind::Integer),
-                    chalk_ir::UniverseIndex::ROOT,
-                )
-            }
-            rustc_type_ir::CanonicalVarKind::Ty(rustc_type_ir::CanonicalTyVarKind::Float) => {
-                CanonicalVarKind::new(
-                    chalk_ir::VariableKind::Ty(TyVariableKind::Float),
-                    chalk_ir::UniverseIndex::ROOT,
-                )
-            }
-            rustc_type_ir::CanonicalVarKind::Region(universe_index) => CanonicalVarKind::new(
-                chalk_ir::VariableKind::Lifetime,
-                chalk_ir::UniverseIndex::ROOT,
-            ),
-            rustc_type_ir::CanonicalVarKind::Const(universe_index) => CanonicalVarKind::new(
-                chalk_ir::VariableKind::Const(crate::TyKind::Error.intern(Interner)),
-                chalk_ir::UniverseIndex::ROOT,
-            ),
-            rustc_type_ir::CanonicalVarKind::PlaceholderTy(_) => unimplemented!(),
-            rustc_type_ir::CanonicalVarKind::PlaceholderRegion(_) => unimplemented!(),
-            rustc_type_ir::CanonicalVarKind::PlaceholderConst(_) => unimplemented!(),
-        }),
-    );
-    chalk_ir::Canonical {
-        binders,
-        value: chalk_ir::ConstrainedSubst {
-            constraints: chalk_ir::Constraints::empty(Interner),
-            subst: convert_args_for_result(interner, &value),
-        },
-    }
+    args.to_chalk(interner)
 }
 
 pub fn convert_args_for_result<'db>(
@@ -1419,3 +1670,17 @@ pub fn convert_region_for_result<'db>(
     };
     chalk_ir::Lifetime::new(Interner, lifetime)
 }
+
+pub trait InferenceVarExt {
+    fn to_vid(self) -> rustc_type_ir::TyVid;
+    fn from_vid(vid: rustc_type_ir::TyVid) -> InferenceVar;
+}
+
+impl InferenceVarExt for InferenceVar {
+    fn to_vid(self) -> rustc_type_ir::TyVid {
+        rustc_type_ir::TyVid::from_u32(self.index())
+    }
+    fn from_vid(vid: rustc_type_ir::TyVid) -> InferenceVar {
+        InferenceVar::from(vid.as_u32())
+    }
+}
diff --git a/crates/hir-ty/src/next_solver/solver.rs b/crates/hir-ty/src/next_solver/solver.rs
index 1d0ee0e488dc..385149d78432 100644
--- a/crates/hir-ty/src/next_solver/solver.rs
+++ b/crates/hir-ty/src/next_solver/solver.rs
@@ -9,12 +9,12 @@ use rustc_type_ir::{
     solve::{Certainty, NoSolution},
 };
 
+use crate::next_solver::mapping::NextSolverToChalk;
 use crate::{
     TraitRefExt,
     db::HirDatabase,
     next_solver::{
-        ClauseKind, CoercePredicate, PredicateKind, SubtypePredicate,
-        mapping::{ChalkToNextSolver, convert_args_for_result},
+        ClauseKind, CoercePredicate, PredicateKind, SubtypePredicate, mapping::ChalkToNextSolver,
         util::sizedness_fast_path,
     },
 };
@@ -200,7 +200,7 @@ impl<'db> SolverDelegate for SolverContext<'db> {
             SolverDefId::StaticId(c) => GeneralConstId::StaticId(c),
             _ => unreachable!(),
         };
-        let subst = convert_args_for_result(self.interner, uv.args.as_slice());
+        let subst = uv.args.to_chalk(self.interner);
         let ec = self.cx().db.const_eval(c, subst, None).ok()?;
         Some(ec.to_nextsolver(self.interner))
     }
diff --git a/crates/hir-ty/src/tests/coercion.rs b/crates/hir-ty/src/tests/coercion.rs
index 3b7d4d2184a5..7ec5231a7341 100644
--- a/crates/hir-ty/src/tests/coercion.rs
+++ b/crates/hir-ty/src/tests/coercion.rs
@@ -49,7 +49,7 @@ fn let_stmt_coerce() {
 //- minicore: coerce_unsized
 fn test() {
     let x: &[isize] = &[1];
-                   // ^^^^ adjustments: Deref(None), Borrow(Ref('?2, Not)), Pointer(Unsize)
+                   // ^^^^ adjustments: Deref(None), Borrow(Ref('?1, Not)), Pointer(Unsize)
     let x: *const [isize] = &[1];
                          // ^^^^ adjustments: Deref(None), Borrow(RawPtr(Not)), Pointer(Unsize)
 }
@@ -96,7 +96,7 @@ fn foo<T>(x: &[T]) -> &[T] { x }
 fn test() {
     let x = if true {
         foo(&[1])
-         // ^^^^ adjustments: Deref(None), Borrow(Ref('?11, Not)), Pointer(Unsize)
+         // ^^^^ adjustments: Deref(None), Borrow(Ref('?1, Not)), Pointer(Unsize)
     } else {
         &[1]
     };
@@ -148,7 +148,7 @@ fn foo<T>(x: &[T]) -> &[T] { x }
 fn test(i: i32) {
     let x = match i {
         2 => foo(&[2]),
-              // ^^^^ adjustments: Deref(None), Borrow(Ref('?11, Not)), Pointer(Unsize)
+              // ^^^^ adjustments: Deref(None), Borrow(Ref('?1, Not)), Pointer(Unsize)
         1 => &[1],
         _ => &[3],
     };
@@ -881,7 +881,7 @@ fn adjust_index() {
 fn test() {
     let x = [1, 2, 3];
     x[2] = 6;
- // ^ adjustments: Borrow(Ref('?8, Mut))
+ // ^ adjustments: Borrow(Ref('?0, Mut))
 }
     ",
     );
@@ -906,11 +906,11 @@ impl core::ops::IndexMut<usize> for StructMut {
 }
 fn test() {
     Struct[0];
- // ^^^^^^ adjustments: Borrow(Ref('?2, Not))
+ // ^^^^^^ adjustments: Borrow(Ref('?0, Not))
     StructMut[0];
- // ^^^^^^^^^ adjustments: Borrow(Ref('?5, Not))
+ // ^^^^^^^^^ adjustments: Borrow(Ref('?1, Not))
     &mut StructMut[0];
-      // ^^^^^^^^^ adjustments: Borrow(Ref('?8, Mut))
+      // ^^^^^^^^^ adjustments: Borrow(Ref('?2, Mut))
 }",
     );
 }
diff --git a/crates/hir-ty/src/tests/incremental.rs b/crates/hir-ty/src/tests/incremental.rs
index df9061d23bf5..d79639b93727 100644
--- a/crates/hir-ty/src/tests/incremental.rs
+++ b/crates/hir-ty/src/tests/incremental.rs
@@ -589,6 +589,7 @@ fn main() {
                 "attrs_shim",
                 "attrs_shim",
                 "return_type_impl_traits_shim",
+                "generic_predicates_ns_shim",
                 "infer_shim",
                 "function_signature_shim",
                 "function_signature_with_source_map_shim",
@@ -605,8 +606,6 @@ fn main() {
                 "impl_signature_shim",
                 "impl_signature_with_source_map_shim",
                 "callable_item_signature_shim",
-                "adt_variance_shim",
-                "variances_of_shim",
                 "trait_impls_in_deps_shim",
                 "trait_impls_in_crate_shim",
                 "impl_trait_with_diagnostics_shim",
@@ -615,7 +614,6 @@ fn main() {
                 "impl_trait_with_diagnostics_ns_shim",
                 "impl_self_ty_with_diagnostics_ns_shim",
                 "generic_predicates_ns_shim",
-                "generic_predicates_ns_shim",
                 "value_ty_shim",
                 "generic_predicates_shim",
                 "lang_item",
@@ -691,6 +689,7 @@ fn main() {
                 "attrs_shim",
                 "attrs_shim",
                 "return_type_impl_traits_shim",
+                "generic_predicates_ns_shim",
                 "infer_shim",
                 "function_signature_with_source_map_shim",
                 "expr_scopes_shim",
@@ -706,7 +705,6 @@ fn main() {
                 "impl_trait_with_diagnostics_ns_shim",
                 "impl_self_ty_with_diagnostics_ns_shim",
                 "generic_predicates_ns_shim",
-                "generic_predicates_ns_shim",
                 "generic_predicates_shim",
             ]
         "#]],
diff --git a/crates/hir-ty/src/tests/macros.rs b/crates/hir-ty/src/tests/macros.rs
index 5d088e40cded..6490554b22b7 100644
--- a/crates/hir-ty/src/tests/macros.rs
+++ b/crates/hir-ty/src/tests/macros.rs
@@ -202,7 +202,7 @@ fn expr_macro_def_expanded_in_various_places() {
             100..119 'for _ ...!() {}': {unknown}
             100..119 'for _ ...!() {}': &'? mut {unknown}
             100..119 'for _ ...!() {}': fn next<{unknown}>(&'? mut {unknown}) -> Option<<{unknown} as Iterator>::Item>
-            100..119 'for _ ...!() {}': Option<{unknown}>
+            100..119 'for _ ...!() {}': Option<<{unknown} as Iterator>::Item>
             100..119 'for _ ...!() {}': ()
             100..119 'for _ ...!() {}': ()
             100..119 'for _ ...!() {}': ()
@@ -296,7 +296,7 @@ fn expr_macro_rules_expanded_in_various_places() {
             114..133 'for _ ...!() {}': {unknown}
             114..133 'for _ ...!() {}': &'? mut {unknown}
             114..133 'for _ ...!() {}': fn next<{unknown}>(&'? mut {unknown}) -> Option<<{unknown} as Iterator>::Item>
-            114..133 'for _ ...!() {}': Option<{unknown}>
+            114..133 'for _ ...!() {}': Option<<{unknown} as Iterator>::Item>
             114..133 'for _ ...!() {}': ()
             114..133 'for _ ...!() {}': ()
             114..133 'for _ ...!() {}': ()
diff --git a/crates/hir-ty/src/tests/method_resolution.rs b/crates/hir-ty/src/tests/method_resolution.rs
index f09b3ef6bfd0..d50daf0f0d5b 100644
--- a/crates/hir-ty/src/tests/method_resolution.rs
+++ b/crates/hir-ty/src/tests/method_resolution.rs
@@ -1876,9 +1876,9 @@ impl Foo {
 }
 fn test() {
     Foo.foo();
-  //^^^ adjustments: Borrow(Ref('?1, Not))
+  //^^^ adjustments: Borrow(Ref('?0, Not))
     (&Foo).foo();
-  // ^^^^ adjustments: Deref(None), Borrow(Ref('?3, Not))
+  // ^^^^ adjustments: Deref(None), Borrow(Ref('?2, Not))
 }
 "#,
     );
@@ -1892,7 +1892,7 @@ fn receiver_adjustment_unsize_array() {
 fn test() {
     let a = [1, 2, 3];
     a.len();
-} //^ adjustments: Borrow(Ref('?7, Not)), Pointer(Unsize)
+} //^ adjustments: Borrow(Ref('?0, Not)), Pointer(Unsize)
 "#,
     );
 }
@@ -2105,7 +2105,7 @@ impl Foo {
 }
 fn test() {
     Box::new(Foo).foo();
-  //^^^^^^^^^^^^^ adjustments: Deref(None), Borrow(Ref('?5, Not))
+  //^^^^^^^^^^^^^ adjustments: Deref(None), Borrow(Ref('?0, Not))
 }
 "#,
     );
@@ -2123,7 +2123,7 @@ impl Foo {
 use core::mem::ManuallyDrop;
 fn test() {
     ManuallyDrop::new(Foo).foo();
-  //^^^^^^^^^^^^^^^^^^^^^^ adjustments: Deref(Some(OverloadedDeref(Some(Not)))), Borrow(Ref('?6, Not))
+  //^^^^^^^^^^^^^^^^^^^^^^ adjustments: Deref(Some(OverloadedDeref(Some(Not)))), Borrow(Ref('?0, Not))
 }
 "#,
     );
diff --git a/crates/hir-ty/src/tests/never_type.rs b/crates/hir-ty/src/tests/never_type.rs
index 6a9135622deb..baca7f2318e2 100644
--- a/crates/hir-ty/src/tests/never_type.rs
+++ b/crates/hir-ty/src/tests/never_type.rs
@@ -362,12 +362,12 @@ fn diverging_expression_3_break() {
             140..141 'x': u32
             149..175 '{ for ...; }; }': u32
             151..172 'for a ...eak; }': fn into_iter<{unknown}>({unknown}) -> <{unknown} as IntoIterator>::IntoIter
-            151..172 'for a ...eak; }': {unknown}
+            151..172 'for a ...eak; }': <{unknown} as IntoIterator>::IntoIter
             151..172 'for a ...eak; }': !
-            151..172 'for a ...eak; }': {unknown}
-            151..172 'for a ...eak; }': &'? mut {unknown}
+            151..172 'for a ...eak; }': <{unknown} as IntoIterator>::IntoIter
+            151..172 'for a ...eak; }': &'? mut <{unknown} as IntoIterator>::IntoIter
             151..172 'for a ...eak; }': fn next<{unknown}>(&'? mut {unknown}) -> Option<<{unknown} as Iterator>::Item>
-            151..172 'for a ...eak; }': Option<{unknown}>
+            151..172 'for a ...eak; }': Option<<{unknown} as Iterator>::Item>
             151..172 'for a ...eak; }': ()
             151..172 'for a ...eak; }': ()
             151..172 'for a ...eak; }': ()
@@ -379,12 +379,12 @@ fn diverging_expression_3_break() {
             226..227 'x': u32
             235..253 '{ for ... {}; }': u32
             237..250 'for a in b {}': fn into_iter<{unknown}>({unknown}) -> <{unknown} as IntoIterator>::IntoIter
-            237..250 'for a in b {}': {unknown}
+            237..250 'for a in b {}': <{unknown} as IntoIterator>::IntoIter
             237..250 'for a in b {}': !
-            237..250 'for a in b {}': {unknown}
-            237..250 'for a in b {}': &'? mut {unknown}
+            237..250 'for a in b {}': <{unknown} as IntoIterator>::IntoIter
+            237..250 'for a in b {}': &'? mut <{unknown} as IntoIterator>::IntoIter
             237..250 'for a in b {}': fn next<{unknown}>(&'? mut {unknown}) -> Option<<{unknown} as Iterator>::Item>
-            237..250 'for a in b {}': Option<{unknown}>
+            237..250 'for a in b {}': Option<<{unknown} as Iterator>::Item>
             237..250 'for a in b {}': ()
             237..250 'for a in b {}': ()
             237..250 'for a in b {}': ()
@@ -395,12 +395,12 @@ fn diverging_expression_3_break() {
             304..305 'x': u32
             313..340 '{ for ...; }; }': u32
             315..337 'for a ...urn; }': fn into_iter<{unknown}>({unknown}) -> <{unknown} as IntoIterator>::IntoIter
-            315..337 'for a ...urn; }': {unknown}
+            315..337 'for a ...urn; }': <{unknown} as IntoIterator>::IntoIter
             315..337 'for a ...urn; }': !
-            315..337 'for a ...urn; }': {unknown}
-            315..337 'for a ...urn; }': &'? mut {unknown}
+            315..337 'for a ...urn; }': <{unknown} as IntoIterator>::IntoIter
+            315..337 'for a ...urn; }': &'? mut <{unknown} as IntoIterator>::IntoIter
             315..337 'for a ...urn; }': fn next<{unknown}>(&'? mut {unknown}) -> Option<<{unknown} as Iterator>::Item>
-            315..337 'for a ...urn; }': Option<{unknown}>
+            315..337 'for a ...urn; }': Option<<{unknown} as Iterator>::Item>
             315..337 'for a ...urn; }': ()
             315..337 'for a ...urn; }': ()
             315..337 'for a ...urn; }': ()
diff --git a/crates/hir-ty/src/tests/opaque_types.rs b/crates/hir-ty/src/tests/opaque_types.rs
index 11d1a58e5367..256ca7defb78 100644
--- a/crates/hir-ty/src/tests/opaque_types.rs
+++ b/crates/hir-ty/src/tests/opaque_types.rs
@@ -134,6 +134,9 @@ static ALIAS: AliasTy = {
 "#,
     );
 
+    // FIXME(next-solver): This should emit type mismatch error but leaving it for now
+    // as we should fully migrate into next-solver without chalk-ir and TAIT should be
+    // reworked on r-a to handle `#[define_opaque(T)]`
     check_infer_with_mismatches(
         r#"
 trait Trait {}
@@ -155,7 +158,6 @@ static ALIAS: i32 = {
             191..193 '_a': impl Trait + ?Sized
             205..211 'Struct': Struct
             217..218 '5': i32
-            205..211: expected impl Trait + ?Sized, got Struct
         "#]],
     )
 }
diff --git a/crates/hir-ty/src/tests/patterns.rs b/crates/hir-ty/src/tests/patterns.rs
index 4949d4016bf1..60a2641e1a20 100644
--- a/crates/hir-ty/src/tests/patterns.rs
+++ b/crates/hir-ty/src/tests/patterns.rs
@@ -48,12 +48,12 @@ fn infer_pattern() {
             83..84 '1': i32
             86..93 '"hello"': &'static str
             101..151 'for (e...     }': fn into_iter<{unknown}>({unknown}) -> <{unknown} as IntoIterator>::IntoIter
-            101..151 'for (e...     }': {unknown}
+            101..151 'for (e...     }': <{unknown} as IntoIterator>::IntoIter
             101..151 'for (e...     }': !
-            101..151 'for (e...     }': {unknown}
-            101..151 'for (e...     }': &'? mut {unknown}
+            101..151 'for (e...     }': <{unknown} as IntoIterator>::IntoIter
+            101..151 'for (e...     }': &'? mut <{unknown} as IntoIterator>::IntoIter
             101..151 'for (e...     }': fn next<{unknown}>(&'? mut {unknown}) -> Option<<{unknown} as Iterator>::Item>
-            101..151 'for (e...     }': Option<({unknown}, {unknown})>
+            101..151 'for (e...     }': Option<<{unknown} as Iterator>::Item>
             101..151 'for (e...     }': ()
             101..151 'for (e...     }': ()
             101..151 'for (e...     }': ()
@@ -719,28 +719,28 @@ fn test() {
             51..58 'loop {}': !
             56..58 '{}': ()
             72..171 '{     ... x); }': ()
-            78..81 'foo': fn foo<&'? (i32, &'? str), i32, impl FnOnce(&'? (i32, &'? str)) -> i32>(&'? (i32, &'? str), impl FnOnce(&'? (i32, &'? str)) -> i32) -> i32
+            78..81 'foo': fn foo<&'? (i32, &'static str), i32, impl FnOnce(&'? (i32, &'static str)) -> i32>(&'? (i32, &'static str), impl FnOnce(&'? (i32, &'static str)) -> i32) -> i32
             78..105 'foo(&(...y)| x)': i32
             82..91 '&(1, "a")': &'? (i32, &'static str)
             83..91 '(1, "a")': (i32, &'static str)
             84..85 '1': i32
             87..90 '"a"': &'static str
-            93..104 '|&(x, y)| x': impl FnOnce(&'? (i32, &'? str)) -> i32
-            94..101 '&(x, y)': &'? (i32, &'? str)
-            95..101 '(x, y)': (i32, &'? str)
+            93..104 '|&(x, y)| x': impl FnOnce(&'? (i32, &'static str)) -> i32
+            94..101 '&(x, y)': &'? (i32, &'static str)
+            95..101 '(x, y)': (i32, &'static str)
             96..97 'x': i32
-            99..100 'y': &'? str
+            99..100 'y': &'static str
             103..104 'x': i32
-            142..145 'foo': fn foo<&'? (i32, &'? str), &'? i32, impl FnOnce(&'? (i32, &'? str)) -> &'? i32>(&'? (i32, &'? str), impl FnOnce(&'? (i32, &'? str)) -> &'? i32) -> &'? i32
+            142..145 'foo': fn foo<&'? (i32, &'static str), &'? i32, impl FnOnce(&'? (i32, &'static str)) -> &'? i32>(&'? (i32, &'static str), impl FnOnce(&'? (i32, &'static str)) -> &'? i32) -> &'? i32
             142..168 'foo(&(...y)| x)': &'? i32
             146..155 '&(1, "a")': &'? (i32, &'static str)
             147..155 '(1, "a")': (i32, &'static str)
             148..149 '1': i32
             151..154 '"a"': &'static str
-            157..167 '|(x, y)| x': impl FnOnce(&'? (i32, &'? str)) -> &'? i32
-            158..164 '(x, y)': (i32, &'? str)
+            157..167 '|(x, y)| x': impl FnOnce(&'? (i32, &'static str)) -> &'? i32
+            158..164 '(x, y)': (i32, &'static str)
             159..160 'x': &'? i32
-            162..163 'y': &'? &'? str
+            162..163 'y': &'? &'static str
             166..167 'x': &'? i32
         "#]],
     );
diff --git a/crates/hir-ty/src/tests/regression.rs b/crates/hir-ty/src/tests/regression.rs
index 6a3f2286215f..eacc4603ea1a 100644
--- a/crates/hir-ty/src/tests/regression.rs
+++ b/crates/hir-ty/src/tests/regression.rs
@@ -268,12 +268,12 @@ fn infer_std_crash_5() {
         expect![[r#"
             26..322 '{     ...   } }': ()
             32..320 'for co...     }': fn into_iter<{unknown}>({unknown}) -> <{unknown} as IntoIterator>::IntoIter
-            32..320 'for co...     }': {unknown}
+            32..320 'for co...     }': <{unknown} as IntoIterator>::IntoIter
             32..320 'for co...     }': !
-            32..320 'for co...     }': {unknown}
-            32..320 'for co...     }': &'? mut {unknown}
+            32..320 'for co...     }': <{unknown} as IntoIterator>::IntoIter
+            32..320 'for co...     }': &'? mut <{unknown} as IntoIterator>::IntoIter
             32..320 'for co...     }': fn next<{unknown}>(&'? mut {unknown}) -> Option<<{unknown} as Iterator>::Item>
-            32..320 'for co...     }': Option<{unknown}>
+            32..320 'for co...     }': Option<<{unknown} as Iterator>::Item>
             32..320 'for co...     }': ()
             32..320 'for co...     }': ()
             32..320 'for co...     }': ()
@@ -628,7 +628,7 @@ fn issue_4053_diesel_where_clauses() {
             65..69 'self': Self
             267..271 'self': Self
             466..470 'self': SelectStatement<F, S, D, W, O, LOf, {unknown}, {unknown}>
-            488..522 '{     ...     }': ()
+            488..522 '{     ...     }': <SelectStatement<F, S, D, W, O, LOf, {unknown}, {unknown}> as BoxedDsl<DB>>::Output
             498..502 'self': SelectStatement<F, S, D, W, O, LOf, {unknown}, {unknown}>
             498..508 'self.order': O
             498..515 'self.o...into()': dyn QueryFragment<DB> + '?
@@ -1248,7 +1248,7 @@ fn test() {
             16..66 'for _ ...     }': {unknown}
             16..66 'for _ ...     }': &'? mut {unknown}
             16..66 'for _ ...     }': fn next<{unknown}>(&'? mut {unknown}) -> Option<<{unknown} as Iterator>::Item>
-            16..66 'for _ ...     }': Option<{unknown}>
+            16..66 'for _ ...     }': Option<<{unknown} as Iterator>::Item>
             16..66 'for _ ...     }': ()
             16..66 'for _ ...     }': ()
             16..66 'for _ ...     }': ()
diff --git a/crates/hir-ty/src/tests/regression/new_solver.rs b/crates/hir-ty/src/tests/regression/new_solver.rs
index e4ee52f45eb7..97473bbabba0 100644
--- a/crates/hir-ty/src/tests/regression/new_solver.rs
+++ b/crates/hir-ty/src/tests/regression/new_solver.rs
@@ -20,7 +20,7 @@ impl<'a> IntoIterator for &'a Grid {
     "#,
         expect![[r#"
             150..154 'self': &'a Grid
-            174..181 '{     }': impl Iterator<Item = &'a ()>
+            174..181 '{     }': impl Iterator<Item = &'? ()>
         "#]],
     );
 }
diff --git a/crates/hir-ty/src/tests/simple.rs b/crates/hir-ty/src/tests/simple.rs
index a995a45f6e75..e7357ed5aa78 100644
--- a/crates/hir-ty/src/tests/simple.rs
+++ b/crates/hir-ty/src/tests/simple.rs
@@ -1954,6 +1954,8 @@ fn closure_return_inferred() {
     );
 }
 
+// FIXME(next-solver): `&'? str` in 231..262 seems suspicious.
+// Should revisit this once we fully migrated into next-solver without chalk-ir.
 #[test]
 fn coroutine_types_inferred() {
     check_infer(
@@ -1998,7 +2000,7 @@ fn test() {
             225..360 'match ...     }': ()
             231..239 'Pin::new': fn new<&'? mut |usize| yields i64 -> &'static str>(&'? mut |usize| yields i64 -> &'static str) -> Pin<&'? mut |usize| yields i64 -> &'static str>
             231..247 'Pin::n...mut g)': Pin<&'? mut |usize| yields i64 -> &'static str>
-            231..262 'Pin::n...usize)': CoroutineState<i64, &'static str>
+            231..262 'Pin::n...usize)': CoroutineState<i64, &'? str>
             240..246 '&mut g': &'? mut |usize| yields i64 -> &'static str
             245..246 'g': |usize| yields i64 -> &'static str
             255..261 '0usize': usize
diff --git a/crates/hir-ty/src/tests/traits.rs b/crates/hir-ty/src/tests/traits.rs
index a311e579744d..7a946f7ec7ce 100644
--- a/crates/hir-ty/src/tests/traits.rs
+++ b/crates/hir-ty/src/tests/traits.rs
@@ -1,6 +1,8 @@
 use cov_mark::check;
 use expect_test::expect;
 
+use crate::tests::infer_with_mismatches;
+
 use super::{check, check_infer, check_infer_with_mismatches, check_no_mismatches, check_types};
 
 #[test]
@@ -2460,7 +2462,7 @@ use core::ops::Index;
 
 type Key<S: UnificationStoreBase> = <S as UnificationStoreBase>::Key;
 
-pub trait UnificationStoreBase: Index<Output = Key<Self>> {
+pub trait UnificationStoreBase: Index<usize, Output = Key<Self>> {
     type Key;
 
     fn len(&self) -> usize;
@@ -3634,8 +3636,7 @@ fn minimized() {
 
 #[test]
 fn no_builtin_binop_expectation_for_general_ty_var() {
-    // FIXME: Ideally type mismatch should be reported on `take_u32(42 - p)`.
-    check_types(
+    infer_with_mismatches(
         r#"
 //- minicore: add
 use core::ops::Add;
@@ -3659,6 +3660,7 @@ fn minimized() {
     take_u32(42 + p);
 }
 "#,
+        true,
     );
 }
 
@@ -4188,6 +4190,8 @@ fn g<P: PointerFamily>(p: <P as PointerFamily>::Pointer<i32>) {
     );
 }
 
+// FIXME(next-solver): Was `&'a T` but now getting error lifetime.
+// This might be fixed once we migrate into next-solver fully without chalk-ir in lowering.
 #[test]
 fn gats_with_impl_trait() {
     // FIXME: the last function (`fn i()`) is not valid Rust as of this writing because you cannot
@@ -4211,21 +4215,21 @@ fn f<T>(v: impl Trait) {
 }
 fn g<'a, T: 'a>(v: impl Trait<Assoc<T> = &'a T>) {
     let a = v.get::<T>();
-      //^ &'a T
+      //^ &'? T
     let a = v.get::<()>();
       //^ <impl Trait<Assoc<T> = &'a T> as Trait>::Assoc<()>
 }
 fn h<'a>(v: impl Trait<Assoc<i32> = &'a i32> + Trait<Assoc<i64> = &'a i64>) {
     let a = v.get::<i32>();
-      //^ &'a i32
+      //^ &'? i32
     let a = v.get::<i64>();
-      //^ &'a i64
+      //^ &'? i64
 }
 fn i<'a>(v: impl Trait<Assoc<i32> = &'a i32, Assoc<i64> = &'a i64>) {
     let a = v.get::<i32>();
-      //^ &'a i32
+      //^ &'? i32
     let a = v.get::<i64>();
-      //^ &'a i64
+      //^ &'? i64
 }
     "#,
     );
@@ -4255,8 +4259,8 @@ fn f<'a>(v: &dyn Trait<Assoc<i32> = &'a i32>) {
             127..128 'v': &'? (dyn Trait<Assoc<i32> = &'a i32> + '?)
             164..195 '{     ...f(); }': ()
             170..171 'v': &'? (dyn Trait<Assoc<i32> = &'a i32> + '?)
-            170..184 'v.get::<i32>()': {unknown}
-            170..192 'v.get:...eref()': &'? {unknown}
+            170..184 'v.get::<i32>()': <dyn Trait<Assoc<i32> = &'a i32> + '? as Trait>::Assoc<i32>
+            170..192 'v.get:...eref()': {unknown}
         "#]],
     );
 }
@@ -4931,6 +4935,8 @@ fn main() {
     );
 }
 
+// FIXME(next-solver): Was `<D as Deserializer<'de>>::Error` but now getting error lifetime.
+// This might be fixed once we migrate into next-solver fully without chalk-ir in lowering.
 #[test]
 fn new_solver_crash_1() {
     check_infer(
@@ -4947,7 +4953,7 @@ where
 "#,
         expect![[r#"
             84..86 'de': D
-            135..138 '{ }': <D as Deserializer<'de>>::Error
+            135..138 '{ }': <D as Deserializer<'?>>::Error
         "#]],
     );
 }
diff --git a/crates/hir-ty/src/traits.rs b/crates/hir-ty/src/traits.rs
index 51cf5be1372c..a6377243ed98 100644
--- a/crates/hir-ty/src/traits.rs
+++ b/crates/hir-ty/src/traits.rs
@@ -1,6 +1,7 @@
 //! Trait solving using Chalk.
 
 use core::fmt;
+use std::hash::Hash;
 
 use chalk_ir::{DebruijnIndex, GoalData, fold::TypeFoldable};
 use chalk_solve::rust_ir;
@@ -25,7 +26,7 @@ use crate::{
     db::HirDatabase,
     infer::unify::InferenceTable,
     next_solver::{
-        DbInterner, GenericArg, SolverContext, Span,
+        DbInterner, GenericArg, Predicate, SolverContext, Span,
         infer::{DbInternerInferExt, InferCtxt},
         mapping::{ChalkToNextSolver, convert_canonical_args_for_result},
         util::mini_canonicalize,
@@ -231,7 +232,6 @@ impl NextTraitSolveResult {
     }
 }
 
-/// Solve a trait goal using Chalk.
 pub fn next_trait_solve(
     db: &dyn HirDatabase,
     krate: Crate,
@@ -290,6 +290,42 @@ pub fn next_trait_solve(
     }
 }
 
+pub fn next_trait_solve_canonical_in_ctxt<'db>(
+    infer_ctxt: &InferCtxt<'db>,
+    goal: crate::next_solver::Canonical<'db, crate::next_solver::Goal<'db, Predicate<'db>>>,
+) -> NextTraitSolveResult {
+    let context = SolverContext(infer_ctxt.clone());
+
+    tracing::info!(?goal);
+
+    let (goal, var_values) = context.instantiate_canonical(&goal);
+    tracing::info!(?var_values);
+
+    let res = context.evaluate_root_goal(goal, Span::dummy(), None);
+
+    let vars =
+        var_values.var_values.iter().map(|g| context.0.resolve_vars_if_possible(g)).collect();
+    let canonical_var_values = mini_canonicalize(context, vars);
+
+    let res = res.map(|r| (r.has_changed, r.certainty, canonical_var_values));
+
+    tracing::debug!("solve_nextsolver({:?}) => {:?}", goal, res);
+
+    match res {
+        Err(_) => NextTraitSolveResult::NoSolution,
+        Ok((_, Certainty::Yes, args)) => NextTraitSolveResult::Certain(
+            convert_canonical_args_for_result(infer_ctxt.interner, args),
+        ),
+        Ok((_, Certainty::Maybe(_), args)) => {
+            let subst = convert_canonical_args_for_result(infer_ctxt.interner, args);
+            NextTraitSolveResult::Uncertain(chalk_ir::Canonical {
+                binders: subst.binders,
+                value: subst.value.subst,
+            })
+        }
+    }
+}
+
 /// Solve a trait goal using Chalk.
 pub fn next_trait_solve_in_ctxt<'db, 'a>(
     infer_ctxt: &'a InferCtxt<'db>,
diff --git a/crates/hir/src/attrs.rs b/crates/hir/src/attrs.rs
index 928753ef0ede..c230bbad0bc4 100644
--- a/crates/hir/src/attrs.rs
+++ b/crates/hir/src/attrs.rs
@@ -14,7 +14,11 @@ use hir_expand::{
     mod_path::{ModPath, PathKind},
     name::Name,
 };
-use hir_ty::{db::HirDatabase, method_resolution};
+use hir_ty::{
+    db::HirDatabase,
+    method_resolution,
+    next_solver::{DbInterner, mapping::ChalkToNextSolver},
+};
 
 use crate::{
     Adt, AsAssocItem, AssocItem, BuiltinType, Const, ConstParam, DocLinkDef, Enum, ExternCrateDecl,
@@ -271,7 +275,11 @@ fn resolve_impl_trait_item<'db>(
     //
     // FIXME: resolve type aliases (which are not yielded by iterate_path_candidates)
     _ = method_resolution::iterate_path_candidates(
-        &canonical,
+        &canonical.to_nextsolver(DbInterner::new_with(
+            db,
+            Some(environment.krate),
+            environment.block,
+        )),
         db,
         environment,
         &traits_in_scope,
diff --git a/crates/hir/src/lib.rs b/crates/hir/src/lib.rs
index 6eb8a8bf60fd..52ab808d2284 100644
--- a/crates/hir/src/lib.rs
+++ b/crates/hir/src/lib.rs
@@ -5611,7 +5611,11 @@ impl<'db> Type<'db> {
             .map_or_else(|| TraitEnvironment::empty(krate.id), |d| db.trait_environment(d));
 
         _ = method_resolution::iterate_method_candidates_dyn(
-            &canonical,
+            &canonical.to_nextsolver(DbInterner::new_with(
+                db,
+                Some(environment.krate),
+                environment.block,
+            )),
             db,
             environment,
             traits_in_scope,
@@ -5698,7 +5702,11 @@ impl<'db> Type<'db> {
             .map_or_else(|| TraitEnvironment::empty(krate.id), |d| db.trait_environment(d));
 
         _ = method_resolution::iterate_path_candidates(
-            &canonical,
+            &canonical.to_nextsolver(DbInterner::new_with(
+                db,
+                Some(environment.krate),
+                environment.block,
+            )),
             db,
             environment,
             traits_in_scope,
diff --git a/crates/ide-completion/src/context/tests.rs b/crates/ide-completion/src/context/tests.rs
index 6121c61ea3f4..445afa75f3f4 100644
--- a/crates/ide-completion/src/context/tests.rs
+++ b/crates/ide-completion/src/context/tests.rs
@@ -10,7 +10,8 @@ use crate::{
 fn check_expected_type_and_name(#[rust_analyzer::rust_fixture] ra_fixture: &str, expect: Expect) {
     let (db, pos) = position(ra_fixture);
     let config = TEST_CONFIG;
-    let (completion_context, _analysis) = CompletionContext::new(&db, pos, &config).unwrap();
+    let (completion_context, _analysis) =
+        salsa::attach(&db, || CompletionContext::new(&db, pos, &config).unwrap());
 
     let ty = completion_context
         .expected_type
diff --git a/crates/ide-diagnostics/src/handlers/type_mismatch.rs b/crates/ide-diagnostics/src/handlers/type_mismatch.rs
index ac54ac0950f3..8613581292f7 100644
--- a/crates/ide-diagnostics/src/handlers/type_mismatch.rs
+++ b/crates/ide-diagnostics/src/handlers/type_mismatch.rs
@@ -526,8 +526,7 @@ fn main() {
             fn run(_t: Rate<5>) {
             }
             fn main() {
-                run(f()) // FIXME: remove this error
-                  //^^^ error: expected Rate<5>, found Rate<_>
+                run(f())
             }
 "#,
         );
diff --git a/crates/ide-ssr/src/tests.rs b/crates/ide-ssr/src/tests.rs
index 46b633b8a325..875b4d9b06ce 100644
--- a/crates/ide-ssr/src/tests.rs
+++ b/crates/ide-ssr/src/tests.rs
@@ -2,7 +2,10 @@ use expect_test::{Expect, expect};
 use hir::{FilePosition, FileRange};
 use ide_db::{
     EditionedFileId, FxHashSet,
-    base_db::{SourceDatabase, salsa::Durability},
+    base_db::{
+        SourceDatabase,
+        salsa::{self, Durability},
+    },
 };
 use test_utils::RangeOrOffset;
 use triomphe::Arc;
@@ -116,7 +119,7 @@ fn assert_ssr_transforms(rules: &[&str], input: &str, expected: Expect) {
         let rule: SsrRule = rule.parse().unwrap();
         match_finder.add_rule(rule).unwrap();
     }
-    let edits = match_finder.edits();
+    let edits = salsa::attach(&db, || match_finder.edits());
     if edits.is_empty() {
         panic!("No edits were made");
     }
@@ -155,8 +158,12 @@ fn assert_matches(pattern: &str, code: &str, expected: &[&str]) {
     )
     .unwrap();
     match_finder.add_search_pattern(pattern.parse().unwrap()).unwrap();
-    let matched_strings: Vec<String> =
-        match_finder.matches().flattened().matches.iter().map(|m| m.matched_text()).collect();
+    let matched_strings: Vec<String> = salsa::attach(&db, || match_finder.matches())
+        .flattened()
+        .matches
+        .iter()
+        .map(|m| m.matched_text())
+        .collect();
     if matched_strings != expected && !expected.is_empty() {
         print_match_debug_info(&match_finder, position.file_id, expected[0]);
     }
diff --git a/crates/ide/src/doc_links/tests.rs b/crates/ide/src/doc_links/tests.rs
index 11518d1fbf30..72436307d2ce 100644
--- a/crates/ide/src/doc_links/tests.rs
+++ b/crates/ide/src/doc_links/tests.rs
@@ -47,7 +47,8 @@ fn check_rewrite(#[rust_analyzer::rust_fixture] ra_fixture: &str, expect: Expect
     let (analysis, position) = fixture::position(ra_fixture);
     let sema = &Semantics::new(&analysis.db);
     let (cursor_def, docs, range) = def_under_cursor(sema, &position);
-    let res = rewrite_links(sema.db, docs.as_str(), cursor_def, Some(range));
+    let res =
+        salsa::attach(sema.db, || rewrite_links(sema.db, docs.as_str(), cursor_def, Some(range)));
     expect.assert_eq(&res)
 }