diff --git a/.typos.toml b/.typos.toml
index 99464150dab4..e954b08fb1e1 100644
--- a/.typos.toml
+++ b/.typos.toml
@@ -33,6 +33,7 @@ trivias = "trivias"
 thir = "thir"
 jod = "jod"
 tructure = "tructure"
+taits = "taits"
 
 [default.extend-identifiers]
 anc = "anc"
diff --git a/crates/hir-ty/src/autoderef.rs b/crates/hir-ty/src/autoderef.rs
index 6dd3cdb745aa..392b0b040825 100644
--- a/crates/hir-ty/src/autoderef.rs
+++ b/crates/hir-ty/src/autoderef.rs
@@ -38,7 +38,7 @@ pub fn autoderef<'db>(
     env: Arc<TraitEnvironment<'db>>,
     ty: Canonical<'db, Ty<'db>>,
 ) -> impl Iterator<Item = Ty<'db>> + use<'db> {
-    let mut table = InferenceTable::new(db, env);
+    let mut table = InferenceTable::new(db, env, None);
     let ty = table.instantiate_canonical(ty);
     let mut autoderef = Autoderef::new_no_tracking(&mut table, ty);
     let mut v = Vec::new();
diff --git a/crates/hir-ty/src/infer.rs b/crates/hir-ty/src/infer.rs
index 361e66522df6..016edb2310eb 100644
--- a/crates/hir-ty/src/infer.rs
+++ b/crates/hir-ty/src/infer.rs
@@ -21,6 +21,7 @@ pub(crate) mod diagnostics;
 mod expr;
 mod fallback;
 mod mutability;
+mod opaques;
 mod pat;
 mod path;
 pub(crate) mod unify;
@@ -31,8 +32,7 @@ use base_db::Crate;
 use either::Either;
 use hir_def::{
     AdtId, AssocItemId, ConstId, DefWithBodyId, FieldId, FunctionId, GenericDefId, GenericParamId,
-    ImplId, ItemContainerId, LocalFieldId, Lookup, TraitId, TupleFieldId, TupleId, TypeAliasId,
-    VariantId,
+    ItemContainerId, LocalFieldId, Lookup, TraitId, TupleFieldId, TupleId, TypeAliasId, VariantId,
     expr_store::{Body, ExpressionStore, HygieneId, path::Path},
     hir::{BindingAnnotation, BindingId, ExprId, ExprOrPatId, LabelId, PatId},
     lang_item::{LangItem, LangItemTarget, lang_item},
@@ -44,11 +44,11 @@ use hir_def::{
 use hir_expand::{mod_path::ModPath, name::Name};
 use indexmap::IndexSet;
 use intern::sym;
-use la_arena::{ArenaMap, Entry};
+use la_arena::ArenaMap;
 use rustc_ast_ir::Mutability;
 use rustc_hash::{FxHashMap, FxHashSet};
 use rustc_type_ir::{
-    AliasTyKind, Flags, TypeFlags, TypeFoldable, TypeSuperVisitable, TypeVisitable, TypeVisitor,
+    AliasTyKind, TypeFoldable,
     inherent::{AdtDef, IntoKind, Region as _, SliceLike, Ty as _},
 };
 use stdx::never;
@@ -61,7 +61,6 @@ use crate::{
         coerce::{CoerceMany, DynamicCoerceMany},
         diagnostics::{Diagnostics, InferenceTyLoweringContext as TyLoweringContext},
         expr::ExprIsRead,
-        unify::InferenceTable,
     },
     lower::{
         ImplTraitIdx, ImplTraitLoweringMode, LifetimeElisionKind, diagnostics::TyLoweringDiagnostic,
@@ -69,10 +68,7 @@ use crate::{
     mir::MirSpan,
     next_solver::{
         AliasTy, Const, DbInterner, ErrorGuaranteed, GenericArg, GenericArgs, Region, Ty, TyKind,
-        Tys,
-        abi::Safety,
-        fold::fold_tys,
-        infer::traits::{Obligation, ObligationCause},
+        Tys, abi::Safety, infer::traits::ObligationCause,
     },
     traits::FnTrait,
     utils::TargetFeatureIsSafeInTarget,
@@ -132,6 +128,8 @@ pub(crate) fn infer_query(db: &dyn HirDatabase, def: DefWithBodyId) -> Arc<Infer
 
     ctx.infer_mut_body();
 
+    ctx.handle_opaque_type_uses();
+
     ctx.type_inference_fallback();
 
     // Comment from rustc:
@@ -148,6 +146,10 @@ pub(crate) fn infer_query(db: &dyn HirDatabase, def: DefWithBodyId) -> Arc<Infer
 
     ctx.infer_closures();
 
+    ctx.table.select_obligations_where_possible();
+
+    ctx.handle_opaque_type_uses();
+
     Arc::new(ctx.resolve_all())
 }
 
@@ -454,7 +456,7 @@ pub struct InferenceResult<'db> {
     /// unresolved or missing subpatterns or subpatterns of mismatched types.
     pub(crate) type_of_pat: ArenaMap<PatId, Ty<'db>>,
     pub(crate) type_of_binding: ArenaMap<BindingId, Ty<'db>>,
-    pub(crate) type_of_rpit: ArenaMap<ImplTraitIdx<'db>, Ty<'db>>,
+    pub(crate) type_of_opaque: FxHashMap<InternedOpaqueTyId, Ty<'db>>,
     type_mismatches: FxHashMap<ExprOrPatId, TypeMismatch<'db>>,
     /// Whether there are any type-mismatching errors in the result.
     // FIXME: This isn't as useful as initially thought due to us falling back placeholders to
@@ -499,7 +501,7 @@ impl<'db> InferenceResult<'db> {
             type_of_expr: Default::default(),
             type_of_pat: Default::default(),
             type_of_binding: Default::default(),
-            type_of_rpit: Default::default(),
+            type_of_opaque: Default::default(),
             type_mismatches: Default::default(),
             has_errors: Default::default(),
             error_ty,
@@ -640,8 +642,14 @@ impl<'db> InferenceResult<'db> {
     // This method is consumed by external tools to run rust-analyzer as a library. Don't remove, please.
     pub fn return_position_impl_trait_types(
         &self,
+        db: &'db dyn HirDatabase,
     ) -> impl Iterator<Item = (ImplTraitIdx<'db>, Ty<'db>)> {
-        self.type_of_rpit.iter().map(|(k, v)| (k, *v))
+        self.type_of_opaque.iter().filter_map(move |(&id, &ty)| {
+            let ImplTraitId::ReturnTypeImplTrait(_, rpit_idx) = id.loc(db) else {
+                return None;
+            };
+            Some((rpit_idx, ty))
+        })
     }
 }
 
@@ -707,6 +715,7 @@ struct InternedStandardTypes<'db> {
 
     re_static: Region<'db>,
     re_error: Region<'db>,
+    re_erased: Region<'db>,
 
     empty_args: GenericArgs<'db>,
     empty_tys: Tys<'db>,
@@ -742,6 +751,7 @@ impl<'db> InternedStandardTypes<'db> {
 
             re_static,
             re_error: Region::error(interner),
+            re_erased: Region::new_erased(interner),
 
             empty_args: GenericArgs::new_from_iter(interner, []),
             empty_tys: Tys::new_from_iter(interner, []),
@@ -848,11 +858,6 @@ fn find_continuable<'a, 'db>(
     }
 }
 
-enum ImplTraitReplacingMode<'db> {
-    ReturnPosition(FxHashSet<Ty<'db>>),
-    TypeAlias,
-}
-
 impl<'body, 'db> InferenceContext<'body, 'db> {
     fn new(
         db: &'db dyn HirDatabase,
@@ -861,7 +866,7 @@ impl<'body, 'db> InferenceContext<'body, 'db> {
         resolver: Resolver<'db>,
     ) -> Self {
         let trait_env = db.trait_environment_for_body(owner);
-        let table = unify::InferenceTable::new(db, trait_env);
+        let table = unify::InferenceTable::new(db, trait_env, Some(owner));
         let types = InternedStandardTypes::new(table.interner());
         InferenceContext {
             result: InferenceResult::new(types.error),
@@ -952,7 +957,7 @@ impl<'body, 'db> InferenceContext<'body, 'db> {
     // `InferenceResult` in the middle of inference. See the fixme comment in `consteval::eval_to_const`. If you
     // used this function for another workaround, mention it here. If you really need this function and believe that
     // there is no problem in it being `pub(crate)`, remove this comment.
-    pub(crate) fn resolve_all(self) -> InferenceResult<'db> {
+    fn resolve_all(self) -> InferenceResult<'db> {
         let InferenceContext {
             mut table, mut result, tuple_field_accesses_rev, diagnostics, ..
         } = self;
@@ -967,7 +972,7 @@ impl<'body, 'db> InferenceContext<'body, 'db> {
             type_of_expr,
             type_of_pat,
             type_of_binding,
-            type_of_rpit,
+            type_of_opaque,
             type_mismatches,
             has_errors,
             error_ty: _,
@@ -999,11 +1004,7 @@ impl<'body, 'db> InferenceContext<'body, 'db> {
             *has_errors = *has_errors || ty.references_non_lt_error();
         }
         type_of_binding.shrink_to_fit();
-        for ty in type_of_rpit.values_mut() {
-            *ty = table.resolve_completely(*ty);
-            *has_errors = *has_errors || ty.references_non_lt_error();
-        }
-        type_of_rpit.shrink_to_fit();
+        type_of_opaque.shrink_to_fit();
 
         *has_errors |= !type_mismatches.is_empty();
 
@@ -1084,9 +1085,6 @@ impl<'body, 'db> InferenceContext<'body, 'db> {
             LifetimeElisionKind::for_const(self.interner(), id.loc(self.db).container),
         );
 
-        // Constants might be defining usage sites of TAITs.
-        self.make_tait_coercion_table(iter::once(return_ty));
-
         self.return_ty = return_ty;
     }
 
@@ -1098,9 +1096,6 @@ impl<'body, 'db> InferenceContext<'body, 'db> {
             LifetimeElisionKind::Elided(self.types.re_static),
         );
 
-        // Statics might be defining usage sites of TAITs.
-        self.make_tait_coercion_table(iter::once(return_ty));
-
         self.return_ty = return_ty;
     }
 
@@ -1138,16 +1133,12 @@ impl<'body, 'db> InferenceContext<'body, 'db> {
             let ty = self.process_user_written_ty(ty);
             self.write_binding_ty(self_param, ty);
         }
-        let mut tait_candidates = FxHashSet::default();
         for (ty, pat) in param_tys.zip(&*self.body.params) {
             let ty = self.process_user_written_ty(ty);
 
             self.infer_top_pat(*pat, ty, None);
-            if ty.flags().intersects(TypeFlags::HAS_TY_OPAQUE.union(TypeFlags::HAS_TY_INFER)) {
-                tait_candidates.insert(ty);
-            }
         }
-        let return_ty = match data.ret_type {
+        self.return_ty = match data.ret_type {
             Some(return_ty) => {
                 let return_ty = self.with_ty_lowering(
                     &data.store,
@@ -1158,45 +1149,12 @@ impl<'body, 'db> InferenceContext<'body, 'db> {
                         ctx.lower_ty(return_ty)
                     },
                 );
-                let return_ty = self.insert_type_vars(return_ty);
-                if let Some(rpits) = self.db.return_type_impl_traits(func) {
-                    let mut mode = ImplTraitReplacingMode::ReturnPosition(FxHashSet::default());
-                    let result = self.insert_inference_vars_for_impl_trait(return_ty, &mut mode);
-                    if let ImplTraitReplacingMode::ReturnPosition(taits) = mode {
-                        tait_candidates.extend(taits);
-                    }
-                    let rpits = (*rpits).as_ref().skip_binder();
-                    for (id, _) in rpits.impl_traits.iter() {
-                        if let Entry::Vacant(e) = self.result.type_of_rpit.entry(id) {
-                            never!("Missed RPIT in `insert_inference_vars_for_rpit`");
-                            e.insert(self.types.error);
-                        }
-                    }
-                    result
-                } else {
-                    return_ty
-                }
+                self.process_user_written_ty(return_ty)
             }
             None => self.types.unit,
         };
 
-        self.return_ty = self.process_user_written_ty(return_ty);
         self.return_coercion = Some(CoerceMany::new(self.return_ty));
-
-        // Functions might be defining usage sites of TAITs.
-        // To define an TAITs, that TAIT must appear in the function's signatures.
-        // So, it suffices to check for params and return types.
-        fold_tys(self.interner(), self.return_ty, |ty| {
-            match ty.kind() {
-                TyKind::Alias(AliasTyKind::Opaque, _) | TyKind::Infer(..) => {
-                    tait_candidates.insert(self.return_ty);
-                }
-                _ => {}
-            }
-            ty
-        });
-
-        self.make_tait_coercion_table(tait_candidates.iter().copied());
     }
 
     #[inline]
@@ -1204,193 +1162,6 @@ impl<'body, 'db> InferenceContext<'body, 'db> {
         self.table.interner()
     }
 
-    fn insert_inference_vars_for_impl_trait<T>(
-        &mut self,
-        t: T,
-        mode: &mut ImplTraitReplacingMode<'db>,
-    ) -> T
-    where
-        T: TypeFoldable<DbInterner<'db>>,
-    {
-        fold_tys(self.interner(), t, |ty| {
-            let ty = self.table.try_structurally_resolve_type(ty);
-            let opaque_ty_id = match ty.kind() {
-                TyKind::Alias(AliasTyKind::Opaque, alias_ty) => alias_ty.def_id.expect_opaque_ty(),
-                _ => return ty,
-            };
-            let (impl_traits, idx) = match self.db.lookup_intern_impl_trait_id(opaque_ty_id) {
-                // We don't replace opaque types from other kind with inference vars
-                // because `insert_inference_vars_for_impl_traits` for each kinds
-                // and unreplaced opaque types of other kind are resolved while
-                // inferencing because of `tait_coercion_table`.
-                ImplTraitId::ReturnTypeImplTrait(def, idx) => {
-                    if matches!(mode, ImplTraitReplacingMode::TypeAlias) {
-                        // RPITs don't have `tait_coercion_table`, so use inserted inference
-                        // vars for them.
-                        if let Some(ty) = self.result.type_of_rpit.get(idx) {
-                            return *ty;
-                        }
-                        return ty;
-                    }
-                    (self.db.return_type_impl_traits(def), idx)
-                }
-                ImplTraitId::TypeAliasImplTrait(def, idx) => {
-                    if let ImplTraitReplacingMode::ReturnPosition(taits) = mode {
-                        // Gather TAITs while replacing RPITs because TAITs inside RPITs
-                        // may not visited while replacing TAITs
-                        taits.insert(ty);
-                        return ty;
-                    }
-                    (self.db.type_alias_impl_traits(def), idx)
-                }
-            };
-            let Some(impl_traits) = impl_traits else {
-                return ty;
-            };
-            let bounds =
-                (*impl_traits).as_ref().map_bound(|its| its.impl_traits[idx].predicates.as_slice());
-            let var = match self.result.type_of_rpit.entry(idx) {
-                Entry::Occupied(entry) => return *entry.get(),
-                Entry::Vacant(entry) => *entry.insert(self.table.next_ty_var()),
-            };
-            for clause in bounds.iter_identity_copied() {
-                let clause = self.insert_inference_vars_for_impl_trait(clause, mode);
-                self.table.register_predicate(Obligation::new(
-                    self.interner(),
-                    ObligationCause::new(),
-                    self.table.trait_env.env,
-                    clause,
-                ));
-            }
-            var
-        })
-    }
-
-    /// The coercion of a non-inference var into an opaque type should fail,
-    /// but not in the defining sites of the TAITs.
-    /// In such cases, we insert an proxy inference var for each TAIT,
-    /// and coerce into it instead of TAIT itself.
-    ///
-    /// The inference var stretagy is effective because;
-    ///
-    /// - It can still unify types that coerced into TAITs
-    /// - We are pushing `impl Trait` bounds into it
-    ///
-    /// This function inserts a map that maps the opaque type to that proxy inference var.
-    fn make_tait_coercion_table(&mut self, tait_candidates: impl Iterator<Item = Ty<'db>>) {
-        struct TypeAliasImplTraitCollector<'a, 'db> {
-            db: &'a dyn HirDatabase,
-            table: &'a mut InferenceTable<'db>,
-            assocs: FxHashMap<InternedOpaqueTyId, (ImplId, Ty<'db>)>,
-            non_assocs: FxHashMap<InternedOpaqueTyId, Ty<'db>>,
-        }
-
-        impl<'db> TypeVisitor<DbInterner<'db>> for TypeAliasImplTraitCollector<'_, 'db> {
-            type Result = ();
-
-            fn visit_ty(&mut self, ty: Ty<'db>) {
-                let ty = self.table.try_structurally_resolve_type(ty);
-
-                if let TyKind::Alias(AliasTyKind::Opaque, alias_ty) = ty.kind()
-                    && let id = alias_ty.def_id.expect_opaque_ty()
-                    && let ImplTraitId::TypeAliasImplTrait(alias_id, _) =
-                        self.db.lookup_intern_impl_trait_id(id)
-                {
-                    let loc = self.db.lookup_intern_type_alias(alias_id);
-                    match loc.container {
-                        ItemContainerId::ImplId(impl_id) => {
-                            self.assocs.insert(id, (impl_id, ty));
-                        }
-                        ItemContainerId::ModuleId(..) | ItemContainerId::ExternBlockId(..) => {
-                            self.non_assocs.insert(id, ty);
-                        }
-                        _ => {}
-                    }
-                }
-
-                ty.super_visit_with(self)
-            }
-        }
-
-        let mut collector = TypeAliasImplTraitCollector {
-            db: self.db,
-            table: &mut self.table,
-            assocs: FxHashMap::default(),
-            non_assocs: FxHashMap::default(),
-        };
-        for ty in tait_candidates {
-            ty.visit_with(&mut collector);
-        }
-
-        // Non-assoc TAITs can be define-used everywhere as long as they are
-        // in function signatures or const types, etc
-        let mut taits = collector.non_assocs;
-
-        // assoc TAITs(ATPITs) can be only define-used inside their impl block.
-        // They cannot be define-used in inner items like in the following;
-        //
-        // ```
-        // impl Trait for Struct {
-        //     type Assoc = impl Default;
-        //
-        //     fn assoc_fn() -> Self::Assoc {
-        //         let foo: Self::Assoc = true; // Allowed here
-        //
-        //         fn inner() -> Self::Assoc {
-        //              false                   // Not allowed here
-        //         }
-        //
-        //         foo
-        //     }
-        // }
-        // ```
-        let impl_id = match self.owner {
-            DefWithBodyId::FunctionId(it) => {
-                let loc = self.db.lookup_intern_function(it);
-                if let ItemContainerId::ImplId(impl_id) = loc.container {
-                    Some(impl_id)
-                } else {
-                    None
-                }
-            }
-            DefWithBodyId::ConstId(it) => {
-                let loc = self.db.lookup_intern_const(it);
-                if let ItemContainerId::ImplId(impl_id) = loc.container {
-                    Some(impl_id)
-                } else {
-                    None
-                }
-            }
-            _ => None,
-        };
-
-        if let Some(impl_id) = impl_id {
-            taits.extend(collector.assocs.into_iter().filter_map(|(id, (impl_, ty))| {
-                if impl_ == impl_id { Some((id, ty)) } else { None }
-            }));
-        }
-
-        let tait_coercion_table: FxHashMap<_, _> = taits
-            .into_iter()
-            .filter_map(|(id, ty)| {
-                if let ImplTraitId::TypeAliasImplTrait(..) = self.db.lookup_intern_impl_trait_id(id)
-                {
-                    let ty = self.insert_inference_vars_for_impl_trait(
-                        ty,
-                        &mut ImplTraitReplacingMode::TypeAlias,
-                    );
-                    Some((id, ty))
-                } else {
-                    None
-                }
-            })
-            .collect();
-
-        if !tait_coercion_table.is_empty() {
-            self.table.tait_coercion_table = Some(tait_coercion_table);
-        }
-    }
-
     fn infer_body(&mut self) {
         match self.return_coercion {
             Some(_) => self.infer_return(self.body.body_expr),
@@ -2006,12 +1777,15 @@ impl<'body, 'db> InferenceContext<'body, 'db> {
         Some(struct_.into())
     }
 
-    fn get_traits_in_scope(&self) -> Either<FxHashSet<TraitId>, &FxHashSet<TraitId>> {
-        let mut b_traits = self.resolver.traits_in_scope_from_block_scopes().peekable();
+    fn get_traits_in_scope<'a>(
+        resolver: &Resolver<'db>,
+        traits_in_scope: &'a FxHashSet<TraitId>,
+    ) -> Either<FxHashSet<TraitId>, &'a FxHashSet<TraitId>> {
+        let mut b_traits = resolver.traits_in_scope_from_block_scopes().peekable();
         if b_traits.peek().is_some() {
-            Either::Left(self.traits_in_scope.iter().copied().chain(b_traits).collect())
+            Either::Left(traits_in_scope.iter().copied().chain(b_traits).collect())
         } else {
-            Either::Right(&self.traits_in_scope)
+            Either::Right(traits_in_scope)
         }
     }
 }
diff --git a/crates/hir-ty/src/infer/coerce.rs b/crates/hir-ty/src/infer/coerce.rs
index 78889ccb89a2..40de9234abc5 100644
--- a/crates/hir-ty/src/infer/coerce.rs
+++ b/crates/hir-ty/src/infer/coerce.rs
@@ -60,8 +60,7 @@ use crate::{
     next_solver::{
         Binder, BoundConst, BoundRegion, BoundRegionKind, BoundTy, BoundTyKind, CallableIdWrapper,
         Canonical, ClauseKind, CoercePredicate, Const, ConstKind, DbInterner, ErrorGuaranteed,
-        GenericArgs, PolyFnSig, PredicateKind, Region, RegionKind, SolverDefId, TraitRef, Ty,
-        TyKind,
+        GenericArgs, PolyFnSig, PredicateKind, Region, RegionKind, TraitRef, Ty, TyKind,
         infer::{
             InferCtxt, InferOk, InferResult,
             relate::RelateResult,
@@ -223,24 +222,6 @@ impl<'a, 'b, 'db> Coerce<'a, 'b, 'db> {
             }
         }
 
-        // If we are coercing into a TAIT, coerce into its proxy inference var, instead.
-        // FIXME(next-solver): This should not be here. This is not how rustc does thing, and it also not allows us
-        // to normalize opaques defined in our scopes. Instead, we should properly register
-        // `TypingMode::Analysis::defining_opaque_types_and_generators`, and rely on the solver to reveal
-        // them for us (we'll also need some global-like registry for the values, something we cannot
-        // really implement, therefore we can really support only RPITs and ITIAT or the new `#[define_opaque]`
-        // TAIT, not the old global TAIT).
-        let mut b = b;
-        if let Some(tait_table) = &self.table.tait_coercion_table
-            && let TyKind::Alias(rustc_type_ir::Opaque, opaque_ty) = b.kind()
-            && let SolverDefId::InternedOpaqueTyId(opaque_ty_id) = opaque_ty.def_id
-            && !matches!(a.kind(), TyKind::Infer(..) | TyKind::Alias(rustc_type_ir::Opaque, _))
-            && let Some(ty) = tait_table.get(&opaque_ty_id)
-        {
-            b = self.table.shallow_resolve(*ty);
-        }
-        let b = b;
-
         // Coercing *from* an unresolved inference variable means that
         // we have no information about the source type. This will always
         // ultimately fall back to some form of subtyping.
@@ -1528,7 +1509,7 @@ fn coerce<'db>(
     env: Arc<TraitEnvironment<'db>>,
     tys: &Canonical<'db, (Ty<'db>, Ty<'db>)>,
 ) -> Result<(Vec<Adjustment<'db>>, Ty<'db>), TypeError<DbInterner<'db>>> {
-    let mut table = InferenceTable::new(db, env);
+    let mut table = InferenceTable::new(db, env, None);
     let interner = table.interner();
     let ((ty1_with_vars, ty2_with_vars), vars) = table.infer_ctxt.instantiate_canonical(tys);
 
diff --git a/crates/hir-ty/src/infer/expr.rs b/crates/hir-ty/src/infer/expr.rs
index fd4e374d9c89..b7ab109b3b9d 100644
--- a/crates/hir-ty/src/infer/expr.rs
+++ b/crates/hir-ty/src/infer/expr.rs
@@ -1458,10 +1458,11 @@ impl<'db> InferenceContext<'_, 'db> {
     ) -> Ty<'db> {
         let coerce_ty = expected.coercion_target_type(&mut self.table);
         let g = self.resolver.update_to_inner_scope(self.db, self.owner, expr);
-        let prev_env = block_id.map(|block_id| {
+        let prev_state = block_id.map(|block_id| {
             let prev_env = self.table.trait_env.clone();
             TraitEnvironment::with_block(&mut self.table.trait_env, block_id);
-            prev_env
+            let prev_block = self.table.infer_ctxt.interner.block.replace(block_id);
+            (prev_env, prev_block)
         });
 
         let (break_ty, ty) =
@@ -1576,8 +1577,9 @@ impl<'db> InferenceContext<'_, 'db> {
                 }
             });
         self.resolver.reset_to_guard(g);
-        if let Some(prev_env) = prev_env {
+        if let Some((prev_env, prev_block)) = prev_state {
             self.table.trait_env = prev_env;
+            self.table.infer_ctxt.interner.block = prev_block;
         }
 
         break_ty.unwrap_or(ty)
@@ -1689,10 +1691,11 @@ impl<'db> InferenceContext<'_, 'db> {
                 // work out while people are typing
                 let canonicalized_receiver = self.canonicalize(receiver_ty);
                 let resolved = method_resolution::lookup_method(
-                    self.db,
                     &canonicalized_receiver,
-                    self.table.trait_env.clone(),
-                    self.get_traits_in_scope().as_ref().left_or_else(|&it| it),
+                    &mut self.table,
+                    Self::get_traits_in_scope(&self.resolver, &self.traits_in_scope)
+                        .as_ref()
+                        .left_or_else(|&it| it),
                     VisibleFromModule::Filter(self.resolver.module()),
                     name,
                 );
@@ -1844,10 +1847,11 @@ impl<'db> InferenceContext<'_, 'db> {
         let canonicalized_receiver = self.canonicalize(receiver_ty);
 
         let resolved = method_resolution::lookup_method(
-            self.db,
             &canonicalized_receiver,
-            self.table.trait_env.clone(),
-            self.get_traits_in_scope().as_ref().left_or_else(|&it| it),
+            &mut self.table,
+            Self::get_traits_in_scope(&self.resolver, &self.traits_in_scope)
+                .as_ref()
+                .left_or_else(|&it| it),
             VisibleFromModule::Filter(self.resolver.module()),
             method_name,
         );
@@ -1892,9 +1896,10 @@ impl<'db> InferenceContext<'_, 'db> {
 
                 let assoc_func_with_same_name = method_resolution::iterate_method_candidates(
                     &canonicalized_receiver,
-                    self.db,
-                    self.table.trait_env.clone(),
-                    self.get_traits_in_scope().as_ref().left_or_else(|&it| it),
+                    &mut self.table,
+                    Self::get_traits_in_scope(&self.resolver, &self.traits_in_scope)
+                        .as_ref()
+                        .left_or_else(|&it| it),
                     VisibleFromModule::Filter(self.resolver.module()),
                     Some(method_name),
                     method_resolution::LookupMode::Path,
diff --git a/crates/hir-ty/src/infer/opaques.rs b/crates/hir-ty/src/infer/opaques.rs
new file mode 100644
index 000000000000..f7719f50ac3e
--- /dev/null
+++ b/crates/hir-ty/src/infer/opaques.rs
@@ -0,0 +1,147 @@
+//! Defining opaque types via inference.
+
+use rustc_type_ir::{TypeVisitableExt, fold_regions};
+use tracing::{debug, instrument};
+
+use crate::{
+    infer::InferenceContext,
+    next_solver::{
+        EarlyBinder, OpaqueTypeKey, SolverDefId, TypingMode,
+        infer::{opaque_types::OpaqueHiddenType, traits::ObligationCause},
+    },
+};
+
+impl<'db> InferenceContext<'_, 'db> {
+    /// This takes all the opaque type uses during HIR typeck. It first computes
+    /// the concrete hidden type by iterating over all defining uses.
+    ///
+    /// A use during HIR typeck is defining if all non-lifetime arguments are
+    /// unique generic parameters and the hidden type does not reference any
+    /// inference variables.
+    ///
+    /// It then uses these defining uses to guide inference for all other uses.
+    #[instrument(level = "debug", skip(self))]
+    pub(super) fn handle_opaque_type_uses(&mut self) {
+        // We clone the opaques instead of stealing them here as they are still used for
+        // normalization in the next generation trait solver.
+        let opaque_types: Vec<_> = self.table.infer_ctxt.clone_opaque_types();
+
+        self.compute_definition_site_hidden_types(opaque_types);
+    }
+}
+
+#[expect(unused, reason = "rustc has this")]
+#[derive(Copy, Clone, Debug)]
+enum UsageKind<'db> {
+    None,
+    NonDefiningUse(OpaqueTypeKey<'db>, OpaqueHiddenType<'db>),
+    UnconstrainedHiddenType(OpaqueHiddenType<'db>),
+    HasDefiningUse(OpaqueHiddenType<'db>),
+}
+
+impl<'db> UsageKind<'db> {
+    fn merge(&mut self, other: UsageKind<'db>) {
+        match (&*self, &other) {
+            (UsageKind::HasDefiningUse(_), _) | (_, UsageKind::None) => unreachable!(),
+            (UsageKind::None, _) => *self = other,
+            // When mergining non-defining uses, prefer earlier ones. This means
+            // the error happens as early as possible.
+            (
+                UsageKind::NonDefiningUse(..) | UsageKind::UnconstrainedHiddenType(..),
+                UsageKind::NonDefiningUse(..),
+            ) => {}
+            // When merging unconstrained hidden types, we prefer later ones. This is
+            // used as in most cases, the defining use is the final return statement
+            // of our function, and other uses with defining arguments are likely not
+            // intended to be defining.
+            (
+                UsageKind::NonDefiningUse(..) | UsageKind::UnconstrainedHiddenType(..),
+                UsageKind::UnconstrainedHiddenType(..) | UsageKind::HasDefiningUse(_),
+            ) => *self = other,
+        }
+    }
+}
+
+impl<'db> InferenceContext<'_, 'db> {
+    fn compute_definition_site_hidden_types(
+        &mut self,
+        mut opaque_types: Vec<(OpaqueTypeKey<'db>, OpaqueHiddenType<'db>)>,
+    ) {
+        for entry in opaque_types.iter_mut() {
+            *entry = self.table.infer_ctxt.resolve_vars_if_possible(*entry);
+        }
+        debug!(?opaque_types);
+
+        let interner = self.interner();
+        let TypingMode::Analysis { defining_opaque_types_and_generators } =
+            self.table.infer_ctxt.typing_mode()
+        else {
+            unreachable!();
+        };
+
+        for def_id in defining_opaque_types_and_generators {
+            let def_id = match def_id {
+                SolverDefId::InternedOpaqueTyId(it) => it,
+                _ => continue,
+            };
+
+            // We do actually need to check this the second pass (we can't just
+            // store this), because we can go from `UnconstrainedHiddenType` to
+            // `HasDefiningUse` (because of fallback)
+            let mut usage_kind = UsageKind::None;
+            for &(opaque_type_key, hidden_type) in &opaque_types {
+                if opaque_type_key.def_id != def_id.into() {
+                    continue;
+                }
+
+                usage_kind.merge(self.consider_opaque_type_use(opaque_type_key, hidden_type));
+
+                if let UsageKind::HasDefiningUse(..) = usage_kind {
+                    break;
+                }
+            }
+
+            if let UsageKind::HasDefiningUse(ty) = usage_kind {
+                for &(opaque_type_key, hidden_type) in &opaque_types {
+                    if opaque_type_key.def_id != def_id.into() {
+                        continue;
+                    }
+
+                    let expected =
+                        EarlyBinder::bind(ty.ty).instantiate(interner, opaque_type_key.args);
+                    self.demand_eqtype(expected, hidden_type.ty);
+                }
+
+                self.result.type_of_opaque.insert(def_id, ty.ty);
+
+                continue;
+            }
+
+            self.result.type_of_opaque.insert(def_id, self.types.error);
+        }
+    }
+
+    #[tracing::instrument(skip(self), ret)]
+    fn consider_opaque_type_use(
+        &self,
+        opaque_type_key: OpaqueTypeKey<'db>,
+        hidden_type: OpaqueHiddenType<'db>,
+    ) -> UsageKind<'db> {
+        // We ignore uses of the opaque if they have any inference variables
+        // as this can frequently happen with recursive calls.
+        //
+        // See `tests/ui/traits/next-solver/opaques/universal-args-non-defining.rs`.
+        if hidden_type.ty.has_non_region_infer() {
+            return UsageKind::UnconstrainedHiddenType(hidden_type);
+        }
+
+        let cause = ObligationCause::new();
+        let at = self.table.infer_ctxt.at(&cause, self.table.trait_env.env);
+        let hidden_type = match at.deeply_normalize(hidden_type) {
+            Ok(hidden_type) => hidden_type,
+            Err(_errors) => OpaqueHiddenType { ty: self.types.error },
+        };
+        let hidden_type = fold_regions(self.interner(), hidden_type, |_, _| self.types.re_erased);
+        UsageKind::HasDefiningUse(hidden_type)
+    }
+}
diff --git a/crates/hir-ty/src/infer/path.rs b/crates/hir-ty/src/infer/path.rs
index 2dae7cb04ffa..9ade8420138d 100644
--- a/crates/hir-ty/src/infer/path.rs
+++ b/crates/hir-ty/src/infer/path.rs
@@ -310,9 +310,10 @@ impl<'db> InferenceContext<'_, 'db> {
         let mut not_visible = None;
         let res = method_resolution::iterate_method_candidates(
             &canonical_ty,
-            self.db,
-            self.table.trait_env.clone(),
-            self.get_traits_in_scope().as_ref().left_or_else(|&it| it),
+            &mut self.table,
+            Self::get_traits_in_scope(&self.resolver, &self.traits_in_scope)
+                .as_ref()
+                .left_or_else(|&it| it),
             VisibleFromModule::Filter(self.resolver.module()),
             Some(name),
             method_resolution::LookupMode::Path,
diff --git a/crates/hir-ty/src/infer/unify.rs b/crates/hir-ty/src/infer/unify.rs
index a18cdda559d0..0f582a1c2313 100644
--- a/crates/hir-ty/src/infer/unify.rs
+++ b/crates/hir-ty/src/infer/unify.rs
@@ -2,10 +2,10 @@
 
 use std::fmt;
 
-use hir_def::{AdtId, GenericParamId, lang_item::LangItem};
+use hir_def::{AdtId, DefWithBodyId, GenericParamId, lang_item::LangItem};
 use hir_expand::name::Name;
 use intern::sym;
-use rustc_hash::{FxHashMap, FxHashSet};
+use rustc_hash::FxHashSet;
 use rustc_type_ir::{
     DebruijnIndex, InferConst, InferTy, RegionVid, TyVid, TypeFoldable, TypeFolder,
     TypeSuperFoldable, TypeVisitableExt, UpcastFrom,
@@ -17,12 +17,12 @@ use triomphe::Arc;
 
 use crate::{
     TraitEnvironment,
-    db::{HirDatabase, InternedOpaqueTyId},
+    db::HirDatabase,
     infer::InferenceContext,
     next_solver::{
         self, AliasTy, Binder, Canonical, ClauseKind, Const, ConstKind, DbInterner,
         ErrorGuaranteed, GenericArg, GenericArgs, Predicate, PredicateKind, Region, RegionKind,
-        SolverDefId, SolverDefIds, TraitRef, Ty, TyKind, TypingMode,
+        SolverDefId, TraitRef, Ty, TyKind, TypingMode,
         fulfill::{FulfillmentCtxt, NextSolverError},
         infer::{
             DbInternerInferExt, InferCtxt, InferOk, InferResult,
@@ -139,10 +139,7 @@ fn could_unify_impl<'db>(
     select: for<'a> fn(&mut ObligationCtxt<'a, 'db>) -> Vec<NextSolverError<'db>>,
 ) -> bool {
     let interner = DbInterner::new_with(db, Some(env.krate), env.block);
-    // FIXME(next-solver): I believe this should use `PostAnalysis` (this is only used for IDE things),
-    // but this causes some bug because of our incorrect impl of `type_of_opaque_hir_typeck()` for TAIT
-    // and async blocks.
-    let infcx = interner.infer_ctxt().build(TypingMode::non_body_analysis());
+    let infcx = interner.infer_ctxt().build(TypingMode::PostAnalysis);
     let cause = ObligationCause::dummy();
     let at = infcx.at(&cause, env.env);
     let ((ty1_with_vars, ty2_with_vars), _) = infcx.instantiate_canonical(tys);
@@ -158,7 +155,6 @@ fn could_unify_impl<'db>(
 pub(crate) struct InferenceTable<'db> {
     pub(crate) db: &'db dyn HirDatabase,
     pub(crate) trait_env: Arc<TraitEnvironment<'db>>,
-    pub(crate) tait_coercion_table: Option<FxHashMap<InternedOpaqueTyId, Ty<'db>>>,
     pub(crate) infer_ctxt: InferCtxt<'db>,
     pub(super) fulfillment_cx: FulfillmentCtxt<'db>,
     pub(super) diverging_type_vars: FxHashSet<Ty<'db>>,
@@ -170,15 +166,23 @@ pub(crate) struct InferenceTableSnapshot<'db> {
 }
 
 impl<'db> InferenceTable<'db> {
-    pub(crate) fn new(db: &'db dyn HirDatabase, trait_env: Arc<TraitEnvironment<'db>>) -> Self {
+    /// Inside hir-ty you should use this for inference only, and always pass `owner`.
+    /// Outside it, always pass `owner = None`.
+    pub(crate) fn new(
+        db: &'db dyn HirDatabase,
+        trait_env: Arc<TraitEnvironment<'db>>,
+        owner: Option<DefWithBodyId>,
+    ) -> Self {
         let interner = DbInterner::new_with(db, Some(trait_env.krate), trait_env.block);
-        let infer_ctxt = interner.infer_ctxt().build(rustc_type_ir::TypingMode::Analysis {
-            defining_opaque_types_and_generators: SolverDefIds::new_from_iter(interner, []),
-        });
+        let typing_mode = match owner {
+            Some(owner) => TypingMode::typeck_for_body(interner, owner.into()),
+            // IDE things wants to reveal opaque types.
+            None => TypingMode::PostAnalysis,
+        };
+        let infer_ctxt = interner.infer_ctxt().build(typing_mode);
         InferenceTable {
             db,
             trait_env,
-            tait_coercion_table: None,
             fulfillment_cx: FulfillmentCtxt::new(&infer_ctxt),
             infer_ctxt,
             diverging_type_vars: FxHashSet::default(),
@@ -698,40 +702,7 @@ impl<'db> InferenceTable<'db> {
     where
         T: TypeFoldable<DbInterner<'db>>,
     {
-        struct Folder<'a, 'db> {
-            table: &'a mut InferenceTable<'db>,
-        }
-        impl<'db> TypeFolder<DbInterner<'db>> for Folder<'_, 'db> {
-            fn cx(&self) -> DbInterner<'db> {
-                self.table.interner()
-            }
-
-            fn fold_ty(&mut self, ty: Ty<'db>) -> Ty<'db> {
-                if !ty.references_error() {
-                    return ty;
-                }
-
-                if ty.is_ty_error() { self.table.next_ty_var() } else { ty.super_fold_with(self) }
-            }
-
-            fn fold_const(&mut self, ct: Const<'db>) -> Const<'db> {
-                if !ct.references_error() {
-                    return ct;
-                }
-
-                if ct.is_ct_error() {
-                    self.table.next_const_var()
-                } else {
-                    ct.super_fold_with(self)
-                }
-            }
-
-            fn fold_region(&mut self, r: Region<'db>) -> Region<'db> {
-                if r.is_error() { self.table.next_region_var() } else { r }
-            }
-        }
-
-        ty.fold_with(&mut Folder { table: self })
+        self.infer_ctxt.insert_type_vars(ty)
     }
 
     /// Replaces `Ty::Error` by a new type var, so we can maybe still infer it.
diff --git a/crates/hir-ty/src/lib.rs b/crates/hir-ty/src/lib.rs
index 25579e04ed01..fdacc1d899dc 100644
--- a/crates/hir-ty/src/lib.rs
+++ b/crates/hir-ty/src/lib.rs
@@ -27,9 +27,11 @@ mod infer;
 mod inhabitedness;
 mod lower;
 pub mod next_solver;
+mod opaques;
 mod specialization;
 mod target_feature;
 mod utils;
+mod variance;
 
 pub mod autoderef;
 pub mod consteval;
@@ -50,7 +52,6 @@ pub mod traits;
 mod test_db;
 #[cfg(test)]
 mod tests;
-mod variance;
 
 use std::hash::Hash;
 
@@ -471,6 +472,7 @@ where
     }
 }
 
+/// To be used from `hir` only.
 pub fn callable_sig_from_fn_trait<'db>(
     self_ty: Ty<'db>,
     trait_env: Arc<TraitEnvironment<'db>>,
@@ -482,7 +484,7 @@ pub fn callable_sig_from_fn_trait<'db>(
         .trait_items(db)
         .associated_type_by_name(&Name::new_symbol_root(sym::Output))?;
 
-    let mut table = InferenceTable::new(db, trait_env.clone());
+    let mut table = InferenceTable::new(db, trait_env.clone(), None);
 
     // Register two obligations:
     // - Self: FnOnce<?args_ty>
diff --git a/crates/hir-ty/src/method_resolution.rs b/crates/hir-ty/src/method_resolution.rs
index cec63566338f..1e3089736205 100644
--- a/crates/hir-ty/src/method_resolution.rs
+++ b/crates/hir-ty/src/method_resolution.rs
@@ -489,9 +489,8 @@ pub fn def_crates<'db>(
 
 /// Look up the method with the given name.
 pub(crate) fn lookup_method<'db>(
-    db: &'db dyn HirDatabase,
     ty: &Canonical<'db, Ty<'db>>,
-    env: Arc<TraitEnvironment<'db>>,
+    table: &mut InferenceTable<'db>,
     traits_in_scope: &FxHashSet<TraitId>,
     visible_from_module: VisibleFromModule,
     name: &Name,
@@ -499,8 +498,7 @@ pub(crate) fn lookup_method<'db>(
     let mut not_visible = None;
     let res = iterate_method_candidates(
         ty,
-        db,
-        env,
+        table,
         traits_in_scope,
         visible_from_module,
         Some(name),
@@ -656,8 +654,7 @@ impl ReceiverAdjustments {
 // FIXME add a context type here?
 pub(crate) fn iterate_method_candidates<'db, T>(
     ty: &Canonical<'db, Ty<'db>>,
-    db: &'db dyn HirDatabase,
-    env: Arc<TraitEnvironment<'db>>,
+    table: &mut InferenceTable<'db>,
     traits_in_scope: &FxHashSet<TraitId>,
     visible_from_module: VisibleFromModule,
     name: Option<&Name>,
@@ -665,10 +662,9 @@ pub(crate) fn iterate_method_candidates<'db, T>(
     mut callback: impl FnMut(ReceiverAdjustments, AssocItemId, bool) -> Option<T>,
 ) -> Option<T> {
     let mut slot = None;
-    _ = iterate_method_candidates_dyn(
+    _ = iterate_method_candidates_dyn_impl(
         ty,
-        db,
-        env,
+        table,
         traits_in_scope,
         visible_from_module,
         name,
@@ -985,6 +981,7 @@ pub fn check_orphan_rules<'db>(db: &'db dyn HirDatabase, impl_: ImplId) -> bool
     is_not_orphan
 }
 
+/// To be used from `hir` only.
 pub fn iterate_path_candidates<'db>(
     ty: &Canonical<'db, Ty<'db>>,
     db: &'db dyn HirDatabase,
@@ -1007,6 +1004,7 @@ pub fn iterate_path_candidates<'db>(
     )
 }
 
+/// To be used from `hir` only.
 pub fn iterate_method_candidates_dyn<'db>(
     ty: &Canonical<'db, Ty<'db>>,
     db: &'db dyn HirDatabase,
@@ -1016,6 +1014,26 @@ pub fn iterate_method_candidates_dyn<'db>(
     name: Option<&Name>,
     mode: LookupMode,
     callback: &mut dyn MethodCandidateCallback,
+) -> ControlFlow<()> {
+    iterate_method_candidates_dyn_impl(
+        ty,
+        &mut InferenceTable::new(db, env, None),
+        traits_in_scope,
+        visible_from_module,
+        name,
+        mode,
+        callback,
+    )
+}
+
+fn iterate_method_candidates_dyn_impl<'db>(
+    ty: &Canonical<'db, Ty<'db>>,
+    table: &mut InferenceTable<'db>,
+    traits_in_scope: &FxHashSet<TraitId>,
+    visible_from_module: VisibleFromModule,
+    name: Option<&Name>,
+    mode: LookupMode,
+    callback: &mut dyn MethodCandidateCallback,
 ) -> ControlFlow<()> {
     let _p = tracing::info_span!(
         "iterate_method_candidates_dyn",
@@ -1046,28 +1064,28 @@ pub fn iterate_method_candidates_dyn<'db>(
             // the methods by autoderef order of *receiver types*, not *self
             // types*.
 
-            let mut table = InferenceTable::new(db, env);
-            let ty = table.instantiate_canonical(*ty);
-            let deref_chain = autoderef_method_receiver(&mut table, ty);
-
-            deref_chain.into_iter().try_for_each(|(receiver_ty, adj)| {
-                iterate_method_candidates_with_autoref(
-                    &mut table,
-                    receiver_ty,
-                    adj,
-                    traits_in_scope,
-                    visible_from_module,
-                    name,
-                    callback,
-                )
+            table.run_in_snapshot(|table| {
+                let ty = table.instantiate_canonical(*ty);
+                let deref_chain = autoderef_method_receiver(table, ty);
+
+                deref_chain.into_iter().try_for_each(|(receiver_ty, adj)| {
+                    iterate_method_candidates_with_autoref(
+                        table,
+                        receiver_ty,
+                        adj,
+                        traits_in_scope,
+                        visible_from_module,
+                        name,
+                        callback,
+                    )
+                })
             })
         }
         LookupMode::Path => {
             // No autoderef for path lookups
             iterate_method_candidates_for_self_ty(
                 ty,
-                db,
-                env,
+                table,
                 traits_in_scope,
                 visible_from_module,
                 name,
@@ -1250,39 +1268,39 @@ fn iterate_method_candidates_by_receiver<'db>(
 #[tracing::instrument(skip_all, fields(name = ?name))]
 fn iterate_method_candidates_for_self_ty<'db>(
     self_ty: &Canonical<'db, Ty<'db>>,
-    db: &'db dyn HirDatabase,
-    env: Arc<TraitEnvironment<'db>>,
+    table: &mut InferenceTable<'db>,
     traits_in_scope: &FxHashSet<TraitId>,
     visible_from_module: VisibleFromModule,
     name: Option<&Name>,
     callback: &mut dyn MethodCandidateCallback,
 ) -> ControlFlow<()> {
-    let mut table = InferenceTable::new(db, env);
-    let self_ty = table.instantiate_canonical(*self_ty);
-    iterate_inherent_methods(
-        self_ty,
-        &mut table,
-        name,
-        None,
-        None,
-        visible_from_module,
-        LookupMode::Path,
-        &mut |adjustments, item, is_visible| {
-            callback.on_inherent_method(adjustments, item, is_visible)
-        },
-    )?;
-    iterate_trait_method_candidates(
-        self_ty,
-        &mut table,
-        traits_in_scope,
-        name,
-        None,
-        None,
-        LookupMode::Path,
-        &mut |adjustments, item, is_visible| {
-            callback.on_trait_method(adjustments, item, is_visible)
-        },
-    )
+    table.run_in_snapshot(|table| {
+        let self_ty = table.instantiate_canonical(*self_ty);
+        iterate_inherent_methods(
+            self_ty,
+            table,
+            name,
+            None,
+            None,
+            visible_from_module,
+            LookupMode::Path,
+            &mut |adjustments, item, is_visible| {
+                callback.on_inherent_method(adjustments, item, is_visible)
+            },
+        )?;
+        iterate_trait_method_candidates(
+            self_ty,
+            table,
+            traits_in_scope,
+            name,
+            None,
+            None,
+            LookupMode::Path,
+            &mut |adjustments, item, is_visible| {
+                callback.on_trait_method(adjustments, item, is_visible)
+            },
+        )
+    })
 }
 
 #[tracing::instrument(skip_all, fields(name = ?name, visible_from_module, receiver_ty))]
diff --git a/crates/hir-ty/src/mir/borrowck.rs b/crates/hir-ty/src/mir/borrowck.rs
index db16c943968f..01892657bc21 100644
--- a/crates/hir-ty/src/mir/borrowck.rs
+++ b/crates/hir-ty/src/mir/borrowck.rs
@@ -17,7 +17,7 @@ use crate::{
     display::DisplayTarget,
     mir::OperandKind,
     next_solver::{
-        DbInterner, GenericArgs, SolverDefIds, Ty, TypingMode,
+        DbInterner, GenericArgs, Ty, TypingMode,
         infer::{DbInternerInferExt, InferCtxt},
     },
 };
@@ -100,11 +100,11 @@ pub fn borrowck_query<'db>(
     let interner = DbInterner::new_with(db, Some(module.krate()), module.containing_block());
     let env = db.trait_environment_for_body(def);
     let mut res = vec![];
+    // This calculates opaques defining scope which is a bit costly therefore is put outside `all_mir_bodies()`.
+    let typing_mode = TypingMode::borrowck(interner, def.into());
     all_mir_bodies(db, def, |body| {
         // FIXME(next-solver): Opaques.
-        let infcx = interner.infer_ctxt().build(TypingMode::Borrowck {
-            defining_opaque_types: SolverDefIds::new_from_iter(interner, []),
-        });
+        let infcx = interner.infer_ctxt().build(typing_mode);
         res.push(BorrowckResult {
             mutability_of_locals: mutability_of_locals(&infcx, &body),
             moved_out_of_ref: moved_out_of_ref(&infcx, &env, &body),
diff --git a/crates/hir-ty/src/next_solver/def_id.rs b/crates/hir-ty/src/next_solver/def_id.rs
index 0ff0b086a087..77f21062b473 100644
--- a/crates/hir-ty/src/next_solver/def_id.rs
+++ b/crates/hir-ty/src/next_solver/def_id.rs
@@ -154,6 +154,29 @@ impl From<DefWithBodyId> for SolverDefId {
     }
 }
 
+impl TryFrom<SolverDefId> for DefWithBodyId {
+    type Error = ();
+
+    #[inline]
+    fn try_from(value: SolverDefId) -> Result<Self, Self::Error> {
+        let id = match value {
+            SolverDefId::ConstId(id) => id.into(),
+            SolverDefId::FunctionId(id) => id.into(),
+            SolverDefId::StaticId(id) => id.into(),
+            SolverDefId::EnumVariantId(id) | SolverDefId::Ctor(Ctor::Enum(id)) => id.into(),
+            SolverDefId::InternedOpaqueTyId(_)
+            | SolverDefId::TraitId(_)
+            | SolverDefId::TypeAliasId(_)
+            | SolverDefId::ImplId(_)
+            | SolverDefId::InternedClosureId(_)
+            | SolverDefId::InternedCoroutineId(_)
+            | SolverDefId::Ctor(Ctor::Struct(_))
+            | SolverDefId::AdtId(_) => return Err(()),
+        };
+        Ok(id)
+    }
+}
+
 impl TryFrom<SolverDefId> for GenericDefId {
     type Error = ();
 
diff --git a/crates/hir-ty/src/next_solver/generic_arg.rs b/crates/hir-ty/src/next_solver/generic_arg.rs
index 90bd44aee86f..dedd6a1a6da5 100644
--- a/crates/hir-ty/src/next_solver/generic_arg.rs
+++ b/crates/hir-ty/src/next_solver/generic_arg.rs
@@ -63,6 +63,14 @@ impl<'db> GenericArg<'db> {
         }
     }
 
+    #[inline]
+    pub(crate) fn expect_region(self) -> Region<'db> {
+        match self {
+            GenericArg::Lifetime(region) => region,
+            _ => panic!("expected a region, got {self:?}"),
+        }
+    }
+
     pub fn error_from_id(interner: DbInterner<'db>, id: GenericParamId) -> GenericArg<'db> {
         match id {
             GenericParamId::TypeParamId(_) => Ty::new_error(interner, ErrorGuaranteed).into(),
diff --git a/crates/hir-ty/src/next_solver/infer/mod.rs b/crates/hir-ty/src/next_solver/infer/mod.rs
index 36c6c48c5a0b..7b8f52bf7203 100644
--- a/crates/hir-ty/src/next_solver/infer/mod.rs
+++ b/crates/hir-ty/src/next_solver/infer/mod.rs
@@ -13,27 +13,27 @@ use opaque_types::{OpaqueHiddenType, OpaqueTypeStorage};
 use region_constraints::{RegionConstraintCollector, RegionConstraintStorage};
 use rustc_next_trait_solver::solve::SolverDelegateEvalExt;
 use rustc_pattern_analysis::Captures;
-use rustc_type_ir::TypeFoldable;
-use rustc_type_ir::error::{ExpectedFound, TypeError};
-use rustc_type_ir::inherent::{
-    Const as _, GenericArg as _, GenericArgs as _, IntoKind, SliceLike, Term as _, Ty as _,
-};
 use rustc_type_ir::{
     ClosureKind, ConstVid, FloatVarValue, FloatVid, GenericArgKind, InferConst, InferTy,
-    IntVarValue, IntVid, OutlivesPredicate, RegionVid, TyVid, UniverseIndex,
+    IntVarValue, IntVid, OutlivesPredicate, RegionVid, TermKind, TyVid, TypeFoldable, TypeFolder,
+    TypeSuperFoldable, TypeVisitableExt, UniverseIndex,
+    error::{ExpectedFound, TypeError},
+    inherent::{
+        Const as _, GenericArg as _, GenericArgs as _, IntoKind, SliceLike, Term as _, Ty as _,
+    },
 };
-use rustc_type_ir::{TermKind, TypeVisitableExt};
 use snapshot::undo_log::InferCtxtUndoLogs;
 use tracing::{debug, instrument};
 use traits::{ObligationCause, PredicateObligations};
 use type_variable::TypeVariableOrigin;
 use unify_key::{ConstVariableOrigin, ConstVariableValue, ConstVidKey};
 
-use crate::next_solver::fold::BoundVarReplacerDelegate;
-use crate::next_solver::infer::select::EvaluationResult;
-use crate::next_solver::infer::traits::PredicateObligation;
-use crate::next_solver::obligation_ctxt::ObligationCtxt;
-use crate::next_solver::{BoundConst, BoundRegion, BoundTy, BoundVarKind, Goal, SolverContext};
+use crate::next_solver::{
+    BoundConst, BoundRegion, BoundTy, BoundVarKind, Goal, SolverContext,
+    fold::BoundVarReplacerDelegate,
+    infer::{select::EvaluationResult, traits::PredicateObligation},
+    obligation_ctxt::ObligationCtxt,
+};
 
 use super::{
     AliasTerm, Binder, CanonicalQueryInput, CanonicalVarValues, Const, ConstKind, DbInterner,
@@ -46,7 +46,7 @@ use super::{
 pub mod at;
 pub mod canonical;
 mod context;
-mod opaque_types;
+pub mod opaque_types;
 pub mod region_constraints;
 pub mod relate;
 pub mod resolve;
@@ -400,6 +400,46 @@ impl<'db> InferCtxt<'db> {
         ))
     }
 
+    pub(crate) fn insert_type_vars<T>(&self, ty: T) -> T
+    where
+        T: TypeFoldable<DbInterner<'db>>,
+    {
+        struct Folder<'a, 'db> {
+            infcx: &'a InferCtxt<'db>,
+        }
+        impl<'db> TypeFolder<DbInterner<'db>> for Folder<'_, 'db> {
+            fn cx(&self) -> DbInterner<'db> {
+                self.infcx.interner
+            }
+
+            fn fold_ty(&mut self, ty: Ty<'db>) -> Ty<'db> {
+                if !ty.references_error() {
+                    return ty;
+                }
+
+                if ty.is_ty_error() { self.infcx.next_ty_var() } else { ty.super_fold_with(self) }
+            }
+
+            fn fold_const(&mut self, ct: Const<'db>) -> Const<'db> {
+                if !ct.references_error() {
+                    return ct;
+                }
+
+                if ct.is_ct_error() {
+                    self.infcx.next_const_var()
+                } else {
+                    ct.super_fold_with(self)
+                }
+            }
+
+            fn fold_region(&mut self, r: Region<'db>) -> Region<'db> {
+                if r.is_error() { self.infcx.next_region_var() } else { r }
+            }
+        }
+
+        ty.fold_with(&mut Folder { infcx: self })
+    }
+
     /// Evaluates whether the predicate can be satisfied in the given
     /// `ParamEnv`, and returns `false` if not certain. However, this is
     /// not entirely accurate if inference variables are involved.
diff --git a/crates/hir-ty/src/next_solver/infer/opaque_types/mod.rs b/crates/hir-ty/src/next_solver/infer/opaque_types/mod.rs
index 06d998488e15..6b6104b2d903 100644
--- a/crates/hir-ty/src/next_solver/infer/opaque_types/mod.rs
+++ b/crates/hir-ty/src/next_solver/infer/opaque_types/mod.rs
@@ -4,9 +4,11 @@ pub(crate) mod table;
 
 pub(crate) use table::{OpaqueTypeStorage, OpaqueTypeTable};
 
+use macros::{TypeFoldable, TypeVisitable};
+
 use crate::next_solver::{OpaqueTypeKey, Ty, infer::InferCtxt};
 
-#[derive(Copy, Clone, Debug)]
+#[derive(Copy, Clone, Debug, TypeVisitable, TypeFoldable)]
 pub struct OpaqueHiddenType<'db> {
     pub ty: Ty<'db>,
 }
diff --git a/crates/hir-ty/src/next_solver/infer/opaque_types/table.rs b/crates/hir-ty/src/next_solver/infer/opaque_types/table.rs
index 0f8b23870fd0..00177d21ac76 100644
--- a/crates/hir-ty/src/next_solver/infer/opaque_types/table.rs
+++ b/crates/hir-ty/src/next_solver/infer/opaque_types/table.rs
@@ -122,14 +122,6 @@ impl<'db> OpaqueTypeStorage<'db> {
     }
 }
 
-impl<'db> Drop for OpaqueTypeStorage<'db> {
-    fn drop(&mut self) {
-        if !self.opaque_types.is_empty() {
-            panic!("{:?}", self.opaque_types)
-        }
-    }
-}
-
 pub(crate) struct OpaqueTypeTable<'a, 'db> {
     storage: &'a mut OpaqueTypeStorage<'db>,
 
diff --git a/crates/hir-ty/src/next_solver/interner.rs b/crates/hir-ty/src/next_solver/interner.rs
index c1ccbaf78a70..b18e08bea49b 100644
--- a/crates/hir-ty/src/next_solver/interner.rs
+++ b/crates/hir-ty/src/next_solver/interner.rs
@@ -7,8 +7,8 @@ pub use tls_db::{attach_db, attach_db_allow_change, with_attached_db};
 
 use base_db::Crate;
 use hir_def::{
-    AdtId, AttrDefId, BlockId, CallableDefId, EnumVariantId, ItemContainerId, StructId, UnionId,
-    VariantId,
+    AdtId, AttrDefId, BlockId, CallableDefId, DefWithBodyId, EnumVariantId, ItemContainerId,
+    StructId, UnionId, VariantId,
     lang_item::LangItem,
     signatures::{FieldData, FnFlags, ImplFlags, StructFlags, TraitFlags},
 };
@@ -29,7 +29,7 @@ use rustc_type_ir::{
 
 use crate::{
     FnAbi,
-    db::{HirDatabase, InternedCoroutine},
+    db::{HirDatabase, InternedCoroutine, InternedCoroutineId},
     method_resolution::{ALL_FLOAT_FPS, ALL_INT_FPS, TyFingerprint},
     next_solver::{
         AdtIdWrapper, BoundConst, CallableIdWrapper, CanonicalVarKind, ClosureIdWrapper,
@@ -96,7 +96,7 @@ macro_rules! _interned_vec_nolifetime_salsa {
         }
     };
     ($name:ident, $ty:ty, nofold) => {
-        #[salsa::interned(constructor = new_, debug)]
+        #[salsa::interned(constructor = new_)]
         pub struct $name {
             #[returns(ref)]
             inner_: smallvec::SmallVec<[$ty; 2]>,
@@ -119,6 +119,12 @@ macro_rules! _interned_vec_nolifetime_salsa {
             }
         }
 
+        impl<'db> std::fmt::Debug for $name<'db> {
+            fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+                self.as_slice().fmt(fmt)
+            }
+        }
+
         impl<'db> rustc_type_ir::inherent::SliceLike for $name<'db> {
             type Item = $ty;
 
@@ -1866,9 +1872,42 @@ impl<'db> Interner for DbInterner<'db> {
         Binder::bind_with_vars(inner, bound_vars)
     }
 
-    fn opaque_types_defined_by(self, _defining_anchor: Self::LocalDefId) -> Self::LocalDefIds {
-        // FIXME(next-solver)
-        SolverDefIds::new_from_iter(self, [])
+    fn opaque_types_defined_by(self, def_id: Self::LocalDefId) -> Self::LocalDefIds {
+        let Ok(def_id) = DefWithBodyId::try_from(def_id) else {
+            return SolverDefIds::default();
+        };
+        let mut result = Vec::new();
+        crate::opaques::opaque_types_defined_by(self.db, def_id, &mut result);
+        SolverDefIds::new_from_iter(self, result)
+    }
+
+    fn opaque_types_and_coroutines_defined_by(self, def_id: Self::LocalDefId) -> Self::LocalDefIds {
+        let Ok(def_id) = DefWithBodyId::try_from(def_id) else {
+            return SolverDefIds::default();
+        };
+        let mut result = Vec::new();
+
+        crate::opaques::opaque_types_defined_by(self.db, def_id, &mut result);
+
+        // Collect coroutines.
+        let body = self.db.body(def_id);
+        body.exprs().for_each(|(expr_id, expr)| {
+            if matches!(
+                expr,
+                hir_def::hir::Expr::Async { .. }
+                    | hir_def::hir::Expr::Closure {
+                        closure_kind: hir_def::hir::ClosureKind::Async
+                            | hir_def::hir::ClosureKind::Coroutine(_),
+                        ..
+                    }
+            ) {
+                let coroutine =
+                    InternedCoroutineId::new(self.db, InternedCoroutine(def_id, expr_id));
+                result.push(coroutine.into());
+            }
+        });
+
+        SolverDefIds::new_from_iter(self, result)
     }
 
     fn alias_has_const_conditions(self, _def_id: Self::DefId) -> bool {
@@ -1913,12 +1952,10 @@ impl<'db> Interner for DbInterner<'db> {
                 let impl_trait_id = self.db().lookup_intern_impl_trait_id(opaque);
                 match impl_trait_id {
                     crate::ImplTraitId::ReturnTypeImplTrait(func, idx) => {
-                        let infer = self.db().infer(func.into());
-                        EarlyBinder::bind(infer.type_of_rpit[idx])
+                        crate::opaques::rpit_hidden_types(self.db, func)[idx]
                     }
-                    crate::ImplTraitId::TypeAliasImplTrait(..) => {
-                        // FIXME(next-solver)
-                        EarlyBinder::bind(Ty::new_error(self, ErrorGuaranteed))
+                    crate::ImplTraitId::TypeAliasImplTrait(type_alias, idx) => {
+                        crate::opaques::tait_hidden_types(self.db, type_alias)[idx]
                     }
                 }
             }
@@ -1969,13 +2006,6 @@ impl<'db> Interner for DbInterner<'db> {
         true
     }
 
-    fn opaque_types_and_coroutines_defined_by(
-        self,
-        _defining_anchor: Self::LocalDefId,
-    ) -> Self::LocalDefIds {
-        Default::default()
-    }
-
     type Probe = rustc_type_ir::solve::inspect::Probe<DbInterner<'db>>;
     fn mk_probe(self, probe: rustc_type_ir::solve::inspect::Probe<Self>) -> Self::Probe {
         probe
diff --git a/crates/hir-ty/src/next_solver/solver.rs b/crates/hir-ty/src/next_solver/solver.rs
index 487d164f8691..7b96b4008fec 100644
--- a/crates/hir-ty/src/next_solver/solver.rs
+++ b/crates/hir-ty/src/next_solver/solver.rs
@@ -2,17 +2,22 @@
 
 use hir_def::{AssocItemId, GeneralConstId};
 use rustc_next_trait_solver::delegate::SolverDelegate;
-use rustc_type_ir::GenericArgKind;
-use rustc_type_ir::lang_items::SolverTraitLangItem;
 use rustc_type_ir::{
-    InferCtxtLike, Interner, PredicatePolarity, TypeFlags, TypeVisitableExt,
-    inherent::{IntoKind, Term as _, Ty as _},
+    AliasTyKind, GenericArgKind, InferCtxtLike, Interner, PredicatePolarity, TypeFlags,
+    TypeVisitableExt,
+    inherent::{IntoKind, SliceLike, Term as _, Ty as _},
+    lang_items::SolverTraitLangItem,
     solve::{Certainty, NoSolution},
 };
+use tracing::debug;
 
-use crate::next_solver::{CanonicalVarKind, ImplIdWrapper};
-use crate::next_solver::{
-    ClauseKind, CoercePredicate, PredicateKind, SubtypePredicate, util::sizedness_fast_path,
+use crate::{
+    ImplTraitId,
+    next_solver::{
+        AliasTy, CanonicalVarKind, Clause, ClauseKind, CoercePredicate, GenericArgs, ImplIdWrapper,
+        ParamEnv, Predicate, PredicateKind, SubtypePredicate, Ty, TyKind, fold::fold_tys,
+        util::sizedness_fast_path,
+    },
 };
 
 use super::{
@@ -76,7 +81,7 @@ impl<'db> SolverDelegate for SolverContext<'db> {
 
     fn well_formed_goals(
         &self,
-        _param_env: <Self::Interner as rustc_type_ir::Interner>::ParamEnv,
+        _param_env: ParamEnv<'db>,
         _arg: <Self::Interner as rustc_type_ir::Interner>::Term,
     ) -> Option<
         Vec<
@@ -125,18 +130,60 @@ impl<'db> SolverDelegate for SolverContext<'db> {
 
     fn add_item_bounds_for_hidden_type(
         &self,
-        _def_id: <Self::Interner as rustc_type_ir::Interner>::DefId,
-        _args: <Self::Interner as rustc_type_ir::Interner>::GenericArgs,
-        _param_env: <Self::Interner as rustc_type_ir::Interner>::ParamEnv,
-        _hidden_ty: <Self::Interner as rustc_type_ir::Interner>::Ty,
-        _goals: &mut Vec<
-            rustc_type_ir::solve::Goal<
-                Self::Interner,
-                <Self::Interner as rustc_type_ir::Interner>::Predicate,
-            >,
-        >,
+        def_id: SolverDefId,
+        args: GenericArgs<'db>,
+        param_env: ParamEnv<'db>,
+        hidden_ty: Ty<'db>,
+        goals: &mut Vec<Goal<'db, Predicate<'db>>>,
     ) {
-        unimplemented!()
+        let interner = self.interner;
+        let opaque_id = def_id.expect_opaque_ty();
+        // Require that the hidden type is well-formed. We have to
+        // make sure we wf-check the hidden type to fix #114728.
+        //
+        // However, we don't check that all types are well-formed.
+        // We only do so for types provided by the user or if they are
+        // "used", e.g. for method selection.
+        //
+        // This means we never check the wf requirements of the hidden
+        // type during MIR borrowck, causing us to infer the wrong
+        // lifetime for its member constraints which then results in
+        // unexpected region errors.
+        goals.push(Goal::new(interner, param_env, ClauseKind::WellFormed(hidden_ty.into())));
+
+        let replace_opaques_in = |clause: Clause<'db>| {
+            fold_tys(interner, clause, |ty| match ty.kind() {
+                // Replace all other mentions of the same opaque type with the hidden type,
+                // as the bounds must hold on the hidden type after all.
+                TyKind::Alias(
+                    AliasTyKind::Opaque,
+                    AliasTy { def_id: def_id2, args: args2, .. },
+                ) if def_id == def_id2 && args == args2 => hidden_ty,
+                _ => ty,
+            })
+        };
+
+        let db = interner.db;
+        let (opaques_table, opaque_idx) = match opaque_id.loc(db) {
+            ImplTraitId::ReturnTypeImplTrait(func, opaque_idx) => {
+                (db.return_type_impl_traits(func), opaque_idx)
+            }
+            ImplTraitId::TypeAliasImplTrait(type_alias, opaque_idx) => {
+                (db.type_alias_impl_traits(type_alias), opaque_idx)
+            }
+        };
+        let item_bounds = opaques_table
+            .as_deref()
+            .unwrap()
+            .as_ref()
+            .map_bound(|table| &table.impl_traits[opaque_idx].predicates);
+        for predicate in item_bounds.iter_instantiated_copied(interner, args.as_slice()) {
+            let predicate = replace_opaques_in(predicate);
+
+            // Require that the predicate holds for the concrete type.
+            debug!(?predicate);
+            goals.push(Goal::new(interner, param_env, predicate));
+        }
     }
 
     fn fetch_eligible_assoc_item(
@@ -190,8 +237,8 @@ impl<'db> SolverDelegate for SolverContext<'db> {
 
     fn is_transmutable(
         &self,
-        _dst: <Self::Interner as rustc_type_ir::Interner>::Ty,
-        _src: <Self::Interner as rustc_type_ir::Interner>::Ty,
+        _dst: Ty<'db>,
+        _src: Ty<'db>,
         _assume: <Self::Interner as rustc_type_ir::Interner>::Const,
     ) -> Result<Certainty, NoSolution> {
         unimplemented!()
@@ -199,7 +246,7 @@ impl<'db> SolverDelegate for SolverContext<'db> {
 
     fn evaluate_const(
         &self,
-        _param_env: <Self::Interner as rustc_type_ir::Interner>::ParamEnv,
+        _param_env: ParamEnv<'db>,
         uv: rustc_type_ir::UnevaluatedConst<Self::Interner>,
     ) -> Option<<Self::Interner as rustc_type_ir::Interner>::Const> {
         let c = match uv.def {
diff --git a/crates/hir-ty/src/opaques.rs b/crates/hir-ty/src/opaques.rs
new file mode 100644
index 000000000000..8531f2437739
--- /dev/null
+++ b/crates/hir-ty/src/opaques.rs
@@ -0,0 +1,199 @@
+//! Handling of opaque types, detection of defining scope and hidden type.
+
+use hir_def::{
+    AssocItemId, AssocItemLoc, DefWithBodyId, FunctionId, HasModule, ItemContainerId, TypeAliasId,
+};
+use hir_expand::name::Name;
+use la_arena::ArenaMap;
+use rustc_type_ir::inherent::Ty as _;
+use syntax::ast;
+use triomphe::Arc;
+
+use crate::{
+    ImplTraitId,
+    db::{HirDatabase, InternedOpaqueTyId},
+    lower::{ImplTraitIdx, ImplTraits},
+    next_solver::{
+        DbInterner, EarlyBinder, ErrorGuaranteed, SolverDefId, Ty, TypingMode,
+        infer::{DbInternerInferExt, traits::ObligationCause},
+        obligation_ctxt::ObligationCtxt,
+    },
+};
+
+pub(crate) fn opaque_types_defined_by(
+    db: &dyn HirDatabase,
+    def_id: DefWithBodyId,
+    result: &mut Vec<SolverDefId>,
+) {
+    if let DefWithBodyId::FunctionId(func) = def_id {
+        // A function may define its own RPITs.
+        extend_with_opaques(
+            db,
+            db.return_type_impl_traits(func),
+            |opaque_idx| ImplTraitId::ReturnTypeImplTrait(func, opaque_idx),
+            result,
+        );
+    }
+
+    let extend_with_taits = |type_alias| {
+        extend_with_opaques(
+            db,
+            db.type_alias_impl_traits(type_alias),
+            |opaque_idx| ImplTraitId::TypeAliasImplTrait(type_alias, opaque_idx),
+            result,
+        );
+    };
+
+    // Collect opaques from assoc items.
+    let extend_with_atpit_from_assoc_items = |assoc_items: &[(Name, AssocItemId)]| {
+        assoc_items
+            .iter()
+            .filter_map(|&(_, assoc_id)| match assoc_id {
+                AssocItemId::TypeAliasId(it) => Some(it),
+                AssocItemId::FunctionId(_) | AssocItemId::ConstId(_) => None,
+            })
+            .for_each(extend_with_taits);
+    };
+    let extend_with_atpit_from_container = |container| match container {
+        ItemContainerId::ImplId(impl_id) => {
+            if db.impl_signature(impl_id).target_trait.is_some() {
+                extend_with_atpit_from_assoc_items(&impl_id.impl_items(db).items);
+            }
+        }
+        ItemContainerId::TraitId(trait_id) => {
+            extend_with_atpit_from_assoc_items(&trait_id.trait_items(db).items);
+        }
+        _ => {}
+    };
+    match def_id {
+        DefWithBodyId::ConstId(id) => extend_with_atpit_from_container(id.loc(db).container),
+        DefWithBodyId::FunctionId(id) => extend_with_atpit_from_container(id.loc(db).container),
+        DefWithBodyId::StaticId(_) | DefWithBodyId::VariantId(_) => {}
+    }
+
+    // FIXME: Collect opaques from `#[define_opaque]`.
+
+    fn extend_with_opaques<'db>(
+        db: &'db dyn HirDatabase,
+        opaques: Option<Arc<EarlyBinder<'db, ImplTraits<'db>>>>,
+        mut make_impl_trait: impl FnMut(ImplTraitIdx<'db>) -> ImplTraitId<'db>,
+        result: &mut Vec<SolverDefId>,
+    ) {
+        if let Some(opaques) = opaques {
+            for (opaque_idx, _) in (*opaques).as_ref().skip_binder().impl_traits.iter() {
+                let opaque_id = InternedOpaqueTyId::new(db, make_impl_trait(opaque_idx));
+                result.push(opaque_id.into());
+            }
+        }
+    }
+}
+
+// These are firewall queries to prevent drawing dependencies between infers:
+
+#[salsa::tracked(returns(ref), unsafe(non_update_return_type))]
+pub(crate) fn rpit_hidden_types<'db>(
+    db: &'db dyn HirDatabase,
+    function: FunctionId,
+) -> ArenaMap<ImplTraitIdx<'db>, EarlyBinder<'db, Ty<'db>>> {
+    let infer = db.infer(function.into());
+    let mut result = ArenaMap::new();
+    for (opaque, hidden_type) in infer.return_position_impl_trait_types(db) {
+        result.insert(opaque, EarlyBinder::bind(hidden_type));
+    }
+    result.shrink_to_fit();
+    result
+}
+
+#[salsa::tracked(returns(ref), unsafe(non_update_return_type))]
+pub(crate) fn tait_hidden_types<'db>(
+    db: &'db dyn HirDatabase,
+    type_alias: TypeAliasId,
+) -> ArenaMap<ImplTraitIdx<'db>, EarlyBinder<'db, Ty<'db>>> {
+    let loc = type_alias.loc(db);
+    let module = loc.module(db);
+    let interner = DbInterner::new_with(db, Some(module.krate()), module.containing_block());
+    let infcx = interner.infer_ctxt().build(TypingMode::non_body_analysis());
+    let mut ocx = ObligationCtxt::new(&infcx);
+    let cause = ObligationCause::dummy();
+    let param_env = db.trait_environment(type_alias.into()).env;
+
+    let defining_bodies = tait_defining_bodies(db, &loc);
+
+    let taits_count = db
+        .type_alias_impl_traits(type_alias)
+        .map_or(0, |taits| (*taits).as_ref().skip_binder().impl_traits.len());
+
+    let mut result = ArenaMap::with_capacity(taits_count);
+    for defining_body in defining_bodies {
+        let infer = db.infer(defining_body);
+        for (&opaque, &hidden_type) in &infer.type_of_opaque {
+            let ImplTraitId::TypeAliasImplTrait(opaque_owner, opaque_idx) = opaque.loc(db) else {
+                continue;
+            };
+            if opaque_owner != type_alias {
+                continue;
+            }
+            // In the presence of errors, we attempt to create a unified type from all
+            // types. rustc doesn't do that, but this should improve the experience.
+            let hidden_type = infcx.insert_type_vars(hidden_type);
+            match result.entry(opaque_idx) {
+                la_arena::Entry::Vacant(entry) => {
+                    entry.insert(EarlyBinder::bind(hidden_type));
+                }
+                la_arena::Entry::Occupied(entry) => {
+                    _ = ocx.eq(&cause, param_env, entry.get().instantiate_identity(), hidden_type);
+                }
+            }
+        }
+    }
+
+    _ = ocx.try_evaluate_obligations();
+
+    // Fill missing entries.
+    for idx in 0..taits_count {
+        let idx = la_arena::Idx::from_raw(la_arena::RawIdx::from_u32(idx as u32));
+        match result.entry(idx) {
+            la_arena::Entry::Vacant(entry) => {
+                entry.insert(EarlyBinder::bind(Ty::new_error(interner, ErrorGuaranteed)));
+            }
+            la_arena::Entry::Occupied(mut entry) => {
+                *entry.get_mut() = entry.get().map_bound(|hidden_type| {
+                    infcx.resolve_vars_if_possible(hidden_type).replace_infer_with_error(interner)
+                });
+            }
+        }
+    }
+
+    result
+}
+
+fn tait_defining_bodies(
+    db: &dyn HirDatabase,
+    loc: &AssocItemLoc<ast::TypeAlias>,
+) -> Vec<DefWithBodyId> {
+    let from_assoc_items = |assoc_items: &[(Name, AssocItemId)]| {
+        // Associated Type Position Impl Trait.
+        assoc_items
+            .iter()
+            .filter_map(|&(_, assoc_id)| match assoc_id {
+                AssocItemId::FunctionId(it) => Some(it.into()),
+                AssocItemId::ConstId(it) => Some(it.into()),
+                AssocItemId::TypeAliasId(_) => None,
+            })
+            .collect()
+    };
+    match loc.container {
+        ItemContainerId::ImplId(impl_id) => {
+            if db.impl_signature(impl_id).target_trait.is_some() {
+                return from_assoc_items(&impl_id.impl_items(db).items);
+            }
+        }
+        ItemContainerId::TraitId(trait_id) => {
+            return from_assoc_items(&trait_id.trait_items(db).items);
+        }
+        _ => {}
+    }
+
+    // FIXME: Support general TAITs, or decisively decide not to.
+    Vec::new()
+}
diff --git a/crates/hir-ty/src/tests/incremental.rs b/crates/hir-ty/src/tests/incremental.rs
index bc4701970c76..14ec161c91c8 100644
--- a/crates/hir-ty/src/tests/incremental.rs
+++ b/crates/hir-ty/src/tests/incremental.rs
@@ -591,6 +591,7 @@ fn main() {
                 "function_signature_shim",
                 "function_signature_with_source_map_shim",
                 "trait_environment_shim",
+                "return_type_impl_traits_shim",
                 "expr_scopes_shim",
                 "struct_signature_shim",
                 "struct_signature_with_source_map_shim",
@@ -686,6 +687,7 @@ fn main() {
                 "return_type_impl_traits_shim",
                 "infer_shim",
                 "function_signature_with_source_map_shim",
+                "return_type_impl_traits_shim",
                 "expr_scopes_shim",
                 "struct_signature_with_source_map_shim",
                 "generic_predicates_shim",
diff --git a/crates/hir-ty/src/tests/opaque_types.rs b/crates/hir-ty/src/tests/opaque_types.rs
index 5cdd170198ba..ca986336ff30 100644
--- a/crates/hir-ty/src/tests/opaque_types.rs
+++ b/crates/hir-ty/src/tests/opaque_types.rs
@@ -31,7 +31,6 @@ fn test() {
 }
 
 #[test]
-#[ignore = "FIXME(next-solver): This currently generates a type mismatch, need to switch opaque type handling to the solver"]
 fn associated_type_impl_traits_complex() {
     check_types(
         r#"
@@ -116,6 +115,7 @@ fn foo() {
     );
 }
 
+#[ignore = "FIXME(next-solver): TAIT support was removed, need to rework it to work with `#[define_opaque]`"]
 #[test]
 fn type_alias_impl_trait_simple() {
     check_no_mismatches(
@@ -135,9 +135,6 @@ 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 {}
diff --git a/crates/hir-ty/src/tests/regression.rs b/crates/hir-ty/src/tests/regression.rs
index 7c79393e65ac..c71cd80d2989 100644
--- a/crates/hir-ty/src/tests/regression.rs
+++ b/crates/hir-ty/src/tests/regression.rs
@@ -725,7 +725,7 @@ fn issue_4885() {
             138..146 'bar(key)': impl Future<Output = <K as Foo<R>>::Bar>
             142..145 'key': &'? K
             162..165 'key': &'? K
-            224..227 '{ }': ()
+            224..227 '{ }': impl Future<Output = <K as Foo<R>>::Bar>
         "#]],
     );
 }
diff --git a/crates/hir-ty/src/tests/regression/new_solver.rs b/crates/hir-ty/src/tests/regression/new_solver.rs
index 5983ec764790..dfbdd25645f7 100644
--- a/crates/hir-ty/src/tests/regression/new_solver.rs
+++ b/crates/hir-ty/src/tests/regression/new_solver.rs
@@ -180,7 +180,7 @@ impl<'a> IntoIterator for &'a Grid {
     "#,
         expect![[r#"
             150..154 'self': &'a Grid
-            174..181 '{     }': impl Iterator<Item = &'a ()>
+            174..181 '{     }': <&'a Grid as IntoIterator>::IntoIter
         "#]],
     );
 }
diff --git a/crates/hir-ty/src/tests/traits.rs b/crates/hir-ty/src/tests/traits.rs
index f72ca22fd229..c0e439310e98 100644
--- a/crates/hir-ty/src/tests/traits.rs
+++ b/crates/hir-ty/src/tests/traits.rs
@@ -1211,7 +1211,7 @@ fn test(x: impl Trait<u64>, y: &impl Trait<u64>) {
         expect![[r#"
             29..33 'self': &'? Self
             54..58 'self': &'? Self
-            98..100 '{}': ()
+            98..100 '{}': impl Trait<u64>
             110..111 'x': impl Trait<u64>
             130..131 'y': &'? impl Trait<u64>
             151..268 '{     ...2(); }': ()
@@ -1373,11 +1373,11 @@ fn test() {
         expect![[r#"
             49..53 'self': &'? mut Self
             101..105 'self': &'? Self
-            184..195 '{ loop {} }': ({unknown}, {unknown})
+            184..195 '{ loop {} }': (impl Iterator<Item = impl Trait<u32>>, impl Trait<u64>)
             186..193 'loop {}': !
             191..193 '{}': ()
             206..207 't': T
-            268..279 '{ loop {} }': ({unknown}, {unknown})
+            268..279 '{ loop {} }': (impl Iterator<Item = impl Trait<T>>, impl Trait<T>)
             270..277 'loop {}': !
             275..277 '{}': ()
             291..413 '{     ...o(); }': ()
@@ -1419,7 +1419,7 @@ fn foo<const C: u8, T>() -> (impl FnOnce(&str, T), impl Trait<u8>) {
 }
 "#,
         expect![[r#"
-            134..165 '{     ...(C)) }': (impl FnOnce(&'? str, T), Bar<u8>)
+            134..165 '{     ...(C)) }': (impl FnOnce(&'? str, T), impl Trait<u8>)
             140..163 '(|inpu...ar(C))': (impl FnOnce(&'? str, T), Bar<u8>)
             141..154 '|input, t| {}': impl FnOnce(&'? str, T)
             142..147 'input': &'? str
@@ -1441,7 +1441,7 @@ fn return_pos_impl_trait_in_projection() {
 trait Future { type Output; }
 impl Future for () { type Output = i32; }
 type Foo<F> = (<F as Future>::Output, F);
-fn foo<X>() -> Foo<impl Future<Output = ()>> {
+fn foo<X>() -> Foo<impl Future<Output = i32>> {
     (0, ())
 }
 "#,
diff --git a/crates/hir-ty/src/traits.rs b/crates/hir-ty/src/traits.rs
index 7f6d4ff17f9f..00c8eb774580 100644
--- a/crates/hir-ty/src/traits.rs
+++ b/crates/hir-ty/src/traits.rs
@@ -107,24 +107,26 @@ pub fn next_trait_solve_canonical_in_ctxt<'db>(
     infer_ctxt: &InferCtxt<'db>,
     goal: Canonical<'db, Goal<'db, Predicate<'db>>>,
 ) -> NextTraitSolveResult {
-    let context = SolverContext(infer_ctxt.clone());
+    infer_ctxt.probe(|_| {
+        let context = <&SolverContext<'db>>::from(infer_ctxt);
 
-    tracing::info!(?goal);
+        tracing::info!(?goal);
 
-    let (goal, var_values) = context.instantiate_canonical(&goal);
-    tracing::info!(?var_values);
+        let (goal, var_values) = context.instantiate_canonical(&goal);
+        tracing::info!(?var_values);
 
-    let res = context.evaluate_root_goal(goal, Span::dummy(), None);
+        let res = context.evaluate_root_goal(goal, Span::dummy(), None);
 
-    let res = res.map(|r| (r.has_changed, r.certainty));
+        let res = res.map(|r| (r.has_changed, r.certainty));
 
-    tracing::debug!("solve_nextsolver({:?}) => {:?}", goal, res);
+        tracing::debug!("solve_nextsolver({:?}) => {:?}", goal, res);
 
-    match res {
-        Err(_) => NextTraitSolveResult::NoSolution,
-        Ok((_, Certainty::Yes)) => NextTraitSolveResult::Certain,
-        Ok((_, Certainty::Maybe { .. })) => NextTraitSolveResult::Uncertain,
-    }
+        match res {
+            Err(_) => NextTraitSolveResult::NoSolution,
+            Ok((_, Certainty::Yes)) => NextTraitSolveResult::Certain,
+            Ok((_, Certainty::Maybe { .. })) => NextTraitSolveResult::Uncertain,
+        }
+    })
 }
 
 /// Solve a trait goal using next trait solver.
diff --git a/crates/hir/src/lib.rs b/crates/hir/src/lib.rs
index 2bb2f80ecc05..f2faf99fc9e8 100644
--- a/crates/hir/src/lib.rs
+++ b/crates/hir/src/lib.rs
@@ -5136,10 +5136,7 @@ impl<'db> Type<'db> {
             AliasTy::new(interner, alias.id.into(), args),
         );
 
-        // FIXME(next-solver): This needs to be `PostAnalysis`, but this currently causes errors due to our incorrect
-        // handling of opaques. `non_body_analysis()` will also cause errors (from not revealing opaques inside their
-        // defining places), so we choose between two bad options.
-        let infcx = interner.infer_ctxt().build(TypingMode::non_body_analysis());
+        let infcx = interner.infer_ctxt().build(TypingMode::PostAnalysis);
         let ty = structurally_normalize_ty(&infcx, projection, self.env.clone());
         if ty.is_ty_error() { None } else { Some(self.derived(ty)) }
     }
@@ -5758,8 +5755,7 @@ impl<'db> Type<'db> {
 
     pub fn drop_glue(&self, db: &'db dyn HirDatabase) -> DropGlue {
         let interner = DbInterner::new_with(db, Some(self.env.krate), self.env.block);
-        // FIXME: This should be `PostAnalysis` I believe.
-        let infcx = interner.infer_ctxt().build(TypingMode::non_body_analysis());
+        let infcx = interner.infer_ctxt().build(TypingMode::PostAnalysis);
         hir_ty::drop::has_drop_glue(&infcx, self.ty, self.env.clone())
     }
 }
diff --git a/crates/ide/src/hover/tests.rs b/crates/ide/src/hover/tests.rs
index 91fb4d0a6715..3a195314a781 100644
--- a/crates/ide/src/hover/tests.rs
+++ b/crates/ide/src/hover/tests.rs
@@ -10809,7 +10809,7 @@ type Foo$0 = impl Sized;
 
             ---
 
-            needs Drop
+            no Drop
         "#]],
     );
     check(
diff --git a/crates/ide/src/signature_help.rs b/crates/ide/src/signature_help.rs
index 5f7e12cf53f8..e927fd57ae96 100644
--- a/crates/ide/src/signature_help.rs
+++ b/crates/ide/src/signature_help.rs
@@ -1996,6 +1996,12 @@ fn f<T, F: FnMut(&T, u16) -> &T>(f: F) {
 
     #[test]
     fn regression_13579() {
+        // FIXME(next-solver): There should be signature help available here.
+        // The reason it is not is because of a trait solver bug. Since `Error` is not provided
+        // nor it can be inferred, it becomes an error type. The bug is that the solver ignores
+        // predicates on error types, and they do not guide infer vars, not allowing us to infer
+        // that `take`'s return type is callable.
+        // https://github.com/rust-lang/rust/pull/146602 should fix the solver bug.
         check(
             r#"
 fn f() {
@@ -2008,9 +2014,7 @@ fn take<C, Error>(
     move || count
 }
 "#,
-            expect![[r#"
-                impl Fn() -> i32
-            "#]],
+            expect![""],
         );
     }