diff --git a/compiler/rustc_borrowck/src/type_check/canonical.rs b/compiler/rustc_borrowck/src/type_check/canonical.rs
index 68b843d4d0d7a..585d0eabf5b97 100644
--- a/compiler/rustc_borrowck/src/type_check/canonical.rs
+++ b/compiler/rustc_borrowck/src/type_check/canonical.rs
@@ -7,6 +7,7 @@ use rustc_middle::mir::ConstraintCategory;
 use rustc_middle::ty::{self, Ty, TyCtxt, TypeFoldable, Upcast};
 use rustc_span::Span;
 use rustc_span::def_id::DefId;
+use rustc_trait_selection::solve::NoSolution;
 use rustc_trait_selection::traits::ObligationCause;
 use rustc_trait_selection::traits::query::type_op::custom::CustomTypeOp;
 use rustc_trait_selection::traits::query::type_op::{self, TypeOpOutput};
@@ -177,6 +178,7 @@ impl<'a, 'tcx> TypeChecker<'a, 'tcx> {
         if self.infcx.next_trait_solver() {
             let body = self.body;
             let param_env = self.infcx.param_env;
+            // FIXME: Make this into a real type op?
             self.fully_perform_op(
                 location.to_locations(),
                 ConstraintCategory::Boring,
@@ -213,6 +215,40 @@ impl<'a, 'tcx> TypeChecker<'a, 'tcx> {
         }
     }
 
+    #[instrument(skip(self), level = "debug")]
+    pub(super) fn structurally_resolve(
+        &mut self,
+        ty: Ty<'tcx>,
+        location: impl NormalizeLocation,
+    ) -> Ty<'tcx> {
+        if self.infcx.next_trait_solver() {
+            let body = self.body;
+            let param_env = self.infcx.param_env;
+            // FIXME: Make this into a real type op?
+            self.fully_perform_op(
+                location.to_locations(),
+                ConstraintCategory::Boring,
+                CustomTypeOp::new(
+                    |ocx| {
+                        ocx.structurally_normalize(
+                            &ObligationCause::misc(
+                                location.to_locations().span(body),
+                                body.source.def_id().expect_local(),
+                            ),
+                            param_env,
+                            ty,
+                        )
+                        .map_err(|_| NoSolution)
+                    },
+                    "normalizing struct tail",
+                ),
+            )
+            .unwrap_or_else(|guar| Ty::new_error(self.tcx(), guar))
+        } else {
+            self.normalize(ty, location)
+        }
+    }
+
     #[instrument(skip(self), level = "debug")]
     pub(super) fn ascribe_user_type(
         &mut self,
diff --git a/compiler/rustc_borrowck/src/type_check/mod.rs b/compiler/rustc_borrowck/src/type_check/mod.rs
index 3a7ed711f681e..2c666953b7cbc 100644
--- a/compiler/rustc_borrowck/src/type_check/mod.rs
+++ b/compiler/rustc_borrowck/src/type_check/mod.rs
@@ -1075,7 +1075,7 @@ impl<'a, 'tcx> TypeChecker<'a, 'tcx> {
                 proj,
                 |this, field, ()| {
                     let ty = this.field_ty(tcx, field);
-                    self.normalize(ty, locations)
+                    self.structurally_resolve(ty, locations)
                 },
                 |_, _| unreachable!(),
             );
diff --git a/compiler/rustc_hir_analysis/src/check/check.rs b/compiler/rustc_hir_analysis/src/check/check.rs
index c66572a937726..97fcc3078a4bf 100644
--- a/compiler/rustc_hir_analysis/src/check/check.rs
+++ b/compiler/rustc_hir_analysis/src/check/check.rs
@@ -322,8 +322,12 @@ fn check_opaque_meets_bounds<'tcx>(
     };
     let param_env = tcx.param_env(defining_use_anchor);
 
-    // FIXME(#132279): This should eventually use the already defined hidden types.
-    let infcx = tcx.infer_ctxt().build(TypingMode::analysis_in_body(tcx, defining_use_anchor));
+    // FIXME(#132279): Once `PostBorrowckAnalysis` is supported in the old solver, this branch should be removed.
+    let infcx = tcx.infer_ctxt().build(if tcx.next_trait_solver_globally() {
+        TypingMode::post_borrowck_analysis(tcx, defining_use_anchor)
+    } else {
+        TypingMode::analysis_in_body(tcx, defining_use_anchor)
+    });
     let ocx = ObligationCtxt::new_with_diagnostics(&infcx);
 
     let args = match origin {
@@ -417,7 +421,11 @@ fn check_opaque_meets_bounds<'tcx>(
     let outlives_env = OutlivesEnvironment::with_bounds(param_env, implied_bounds);
     ocx.resolve_regions_and_report_errors(defining_use_anchor, &outlives_env)?;
 
-    if let hir::OpaqueTyOrigin::FnReturn { .. } | hir::OpaqueTyOrigin::AsyncFn { .. } = origin {
+    if infcx.next_trait_solver() {
+        Ok(())
+    } else if let hir::OpaqueTyOrigin::FnReturn { .. } | hir::OpaqueTyOrigin::AsyncFn { .. } =
+        origin
+    {
         // HACK: this should also fall through to the hidden type check below, but the original
         // implementation had a bug where equivalent lifetimes are not identical. This caused us
         // to reject existing stable code that is otherwise completely fine. The real fix is to
diff --git a/compiler/rustc_hir_typeck/src/_match.rs b/compiler/rustc_hir_typeck/src/_match.rs
index bfdf764d299b4..7e3cb7914a9f7 100644
--- a/compiler/rustc_hir_typeck/src/_match.rs
+++ b/compiler/rustc_hir_typeck/src/_match.rs
@@ -57,7 +57,7 @@ impl<'a, 'tcx> FnCtxt<'a, 'tcx> {
         // type in that case)
         let mut all_arms_diverge = Diverges::WarnedAlways;
 
-        let expected = orig_expected.adjust_for_branches(self);
+        let expected = orig_expected.adjust_for_branches(self, expr.span);
         debug!(?expected);
 
         let mut coercion = {
diff --git a/compiler/rustc_hir_typeck/src/expectation.rs b/compiler/rustc_hir_typeck/src/expectation.rs
index 4653458b5ddcc..93fa6f863d17f 100644
--- a/compiler/rustc_hir_typeck/src/expectation.rs
+++ b/compiler/rustc_hir_typeck/src/expectation.rs
@@ -39,10 +39,14 @@ impl<'a, 'tcx> Expectation<'tcx> {
     // an expected type. Otherwise, we might write parts of the type
     // when checking the 'then' block which are incompatible with the
     // 'else' branch.
-    pub(super) fn adjust_for_branches(&self, fcx: &FnCtxt<'a, 'tcx>) -> Expectation<'tcx> {
+    pub(super) fn adjust_for_branches(
+        &self,
+        fcx: &FnCtxt<'a, 'tcx>,
+        span: Span,
+    ) -> Expectation<'tcx> {
         match *self {
             ExpectHasType(ety) => {
-                let ety = fcx.shallow_resolve(ety);
+                let ety = fcx.try_structurally_resolve_type(span, ety);
                 if !ety.is_ty_var() { ExpectHasType(ety) } else { NoExpectation }
             }
             ExpectRvalueLikeUnsized(ety) => ExpectRvalueLikeUnsized(ety),
diff --git a/compiler/rustc_hir_typeck/src/expr.rs b/compiler/rustc_hir_typeck/src/expr.rs
index 6599b49baa3cd..40543ed67bb10 100644
--- a/compiler/rustc_hir_typeck/src/expr.rs
+++ b/compiler/rustc_hir_typeck/src/expr.rs
@@ -68,7 +68,9 @@ impl<'a, 'tcx> FnCtxt<'a, 'tcx> {
 
         // While we don't allow *arbitrary* coercions here, we *do* allow
         // coercions from ! to `expected`.
-        if ty.is_never() && self.expr_guaranteed_to_constitute_read_for_never(expr) {
+        if self.try_structurally_resolve_type(expr.span, ty).is_never()
+            && self.expr_guaranteed_to_constitute_read_for_never(expr)
+        {
             if let Some(_) = self.typeck_results.borrow().adjustments().get(expr.hir_id) {
                 let reported = self.dcx().span_delayed_bug(
                     expr.span,
@@ -274,7 +276,9 @@ impl<'a, 'tcx> FnCtxt<'a, 'tcx> {
         // unless it's a place expression that isn't being read from, in which case
         // diverging would be unsound since we may never actually read the `!`.
         // e.g. `let _ = *never_ptr;` with `never_ptr: *const !`.
-        if ty.is_never() && self.expr_guaranteed_to_constitute_read_for_never(expr) {
+        if self.try_structurally_resolve_type(expr.span, ty).is_never()
+            && self.expr_guaranteed_to_constitute_read_for_never(expr)
+        {
             self.diverges.set(self.diverges.get() | Diverges::always(expr.span));
         }
 
@@ -1290,7 +1294,7 @@ impl<'a, 'tcx> FnCtxt<'a, 'tcx> {
         let cond_diverges = self.diverges.get();
         self.diverges.set(Diverges::Maybe);
 
-        let expected = orig_expected.adjust_for_branches(self);
+        let expected = orig_expected.adjust_for_branches(self, sp);
         let then_ty = self.check_expr_with_expectation(then_expr, expected);
         let then_diverges = self.diverges.get();
         self.diverges.set(Diverges::Maybe);
diff --git a/compiler/rustc_hir_typeck/src/method/probe.rs b/compiler/rustc_hir_typeck/src/method/probe.rs
index 640729576fcc6..ee9a0d9961c1f 100644
--- a/compiler/rustc_hir_typeck/src/method/probe.rs
+++ b/compiler/rustc_hir_typeck/src/method/probe.rs
@@ -1574,7 +1574,8 @@ impl<'a, 'tcx> ProbeContext<'a, 'tcx> {
                         // Thus we need to prevent them from trying to match the `&_` autoref
                         // candidates that get created for `&self` trait methods.
                         ty::Alias(ty::Opaque, alias_ty)
-                            if self.infcx.can_define_opaque_ty(alias_ty.def_id)
+                            if !self.next_trait_solver()
+                                && self.infcx.can_define_opaque_ty(alias_ty.def_id)
                                 && !xform_self_ty.is_ty_var() =>
                         {
                             return ProbeResult::NoMatch;
@@ -1642,6 +1643,25 @@ impl<'a, 'tcx> ProbeContext<'a, 'tcx> {
                 }
             }
 
+            // In the new solver, check the well-formedness of the return type.
+            // This emulates, in a way, the predicates that fall out of
+            // normalizing the return type in the old solver.
+            //
+            // We alternatively could check the predicates of the method itself hold,
+            // but we intentionally do not do this in the old solver b/c of cycles,
+            // and doing it in the new solver would be stronger. This should be fixed
+            // in the future, since it likely leads to much better method winnowing.
+            if let Some(xform_ret_ty) = xform_ret_ty
+                && self.infcx.next_trait_solver()
+            {
+                ocx.register_obligation(traits::Obligation::new(
+                    self.tcx,
+                    cause.clone(),
+                    self.param_env,
+                    ty::ClauseKind::WellFormed(xform_ret_ty.into()),
+                ));
+            }
+
             // Evaluate those obligations to see if they might possibly hold.
             for error in ocx.select_where_possible() {
                 result = ProbeResult::NoMatch;
diff --git a/compiler/rustc_hir_typeck/src/upvar.rs b/compiler/rustc_hir_typeck/src/upvar.rs
index d50eff0deb0bc..b0c020dd7cbed 100644
--- a/compiler/rustc_hir_typeck/src/upvar.rs
+++ b/compiler/rustc_hir_typeck/src/upvar.rs
@@ -1802,7 +1802,8 @@ impl<'a, 'tcx> FnCtxt<'a, 'tcx> {
         let mut is_mutbl = bm.1;
 
         for pointer_ty in place.deref_tys() {
-            match pointer_ty.kind() {
+            match self.structurally_resolve_type(self.tcx.hir().span(var_hir_id), pointer_ty).kind()
+            {
                 // We don't capture derefs of raw ptrs
                 ty::RawPtr(_, _) => unreachable!(),
 
@@ -1816,7 +1817,11 @@ impl<'a, 'tcx> FnCtxt<'a, 'tcx> {
                 // Dereferencing a box doesn't change mutability
                 ty::Adt(def, ..) if def.is_box() => {}
 
-                unexpected_ty => bug!("deref of unexpected pointer type {:?}", unexpected_ty),
+                unexpected_ty => span_bug!(
+                    self.tcx.hir().span(var_hir_id),
+                    "deref of unexpected pointer type {:?}",
+                    unexpected_ty
+                ),
             }
         }
 
diff --git a/compiler/rustc_infer/src/infer/context.rs b/compiler/rustc_infer/src/infer/context.rs
index 1968ed347529f..5fc9b679c8acf 100644
--- a/compiler/rustc_infer/src/infer/context.rs
+++ b/compiler/rustc_infer/src/infer/context.rs
@@ -7,7 +7,7 @@ use rustc_middle::ty::relate::combine::PredicateEmittingRelation;
 use rustc_middle::ty::{self, Ty, TyCtxt};
 use rustc_span::{DUMMY_SP, ErrorGuaranteed};
 
-use super::{BoundRegionConversionTime, InferCtxt, SubregionOrigin};
+use super::{BoundRegionConversionTime, InferCtxt, RegionVariableOrigin, SubregionOrigin};
 
 impl<'tcx> rustc_type_ir::InferCtxtLike for InferCtxt<'tcx> {
     type Interner = TyCtxt<'tcx>;
@@ -87,6 +87,10 @@ impl<'tcx> rustc_type_ir::InferCtxtLike for InferCtxt<'tcx> {
         self.inner.borrow_mut().unwrap_region_constraints().opportunistic_resolve_var(self.tcx, vid)
     }
 
+    fn next_region_infer(&self) -> ty::Region<'tcx> {
+        self.next_region_var(RegionVariableOrigin::MiscVariable(DUMMY_SP))
+    }
+
     fn next_ty_infer(&self) -> Ty<'tcx> {
         self.next_ty_var(DUMMY_SP)
     }
diff --git a/compiler/rustc_infer/src/infer/mod.rs b/compiler/rustc_infer/src/infer/mod.rs
index 555c1022a8a1c..3bcf7e4d3e4e7 100644
--- a/compiler/rustc_infer/src/infer/mod.rs
+++ b/compiler/rustc_infer/src/infer/mod.rs
@@ -990,11 +990,17 @@ impl<'tcx> InferCtxt<'tcx> {
 
     #[inline(always)]
     pub fn can_define_opaque_ty(&self, id: impl Into<DefId>) -> bool {
+        debug_assert!(!self.next_trait_solver());
         match self.typing_mode() {
             TypingMode::Analysis { defining_opaque_types } => {
                 id.into().as_local().is_some_and(|def_id| defining_opaque_types.contains(&def_id))
             }
-            TypingMode::Coherence | TypingMode::PostAnalysis => false,
+            // FIXME(#132279): This function is quite weird in post-analysis
+            // and post-borrowck analysis mode. We may need to modify its uses
+            // to support PostBorrowckAnalysis in the old solver as well.
+            TypingMode::Coherence
+            | TypingMode::PostBorrowckAnalysis { .. }
+            | TypingMode::PostAnalysis => false,
         }
     }
 
@@ -1276,7 +1282,6 @@ impl<'tcx> InferCtxt<'tcx> {
     /// using canonicalization or carrying this inference context around.
     pub fn typing_env(&self, param_env: ty::ParamEnv<'tcx>) -> ty::TypingEnv<'tcx> {
         let typing_mode = match self.typing_mode() {
-            ty::TypingMode::Coherence => ty::TypingMode::Coherence,
             // FIXME(#132279): This erases the `defining_opaque_types` as it isn't possible
             // to handle them without proper canonicalization. This means we may cause cycle
             // errors and fail to reveal opaques while inside of bodies. We should rename this
@@ -1284,7 +1289,9 @@ impl<'tcx> InferCtxt<'tcx> {
             ty::TypingMode::Analysis { defining_opaque_types: _ } => {
                 TypingMode::non_body_analysis()
             }
-            ty::TypingMode::PostAnalysis => ty::TypingMode::PostAnalysis,
+            mode @ (ty::TypingMode::Coherence
+            | ty::TypingMode::PostBorrowckAnalysis { .. }
+            | ty::TypingMode::PostAnalysis) => mode,
         };
         ty::TypingEnv { typing_mode, param_env }
     }
diff --git a/compiler/rustc_infer/src/infer/opaque_types/mod.rs b/compiler/rustc_infer/src/infer/opaque_types/mod.rs
index a608ea1ad579f..b64686afd2340 100644
--- a/compiler/rustc_infer/src/infer/opaque_types/mod.rs
+++ b/compiler/rustc_infer/src/infer/opaque_types/mod.rs
@@ -98,6 +98,7 @@ impl<'tcx> InferCtxt<'tcx> {
         span: Span,
         param_env: ty::ParamEnv<'tcx>,
     ) -> Result<Vec<Goal<'tcx, ty::Predicate<'tcx>>>, TypeError<'tcx>> {
+        debug_assert!(!self.next_trait_solver());
         let process = |a: Ty<'tcx>, b: Ty<'tcx>| match *a.kind() {
             ty::Alias(ty::Opaque, ty::AliasTy { def_id, args, .. }) if def_id.is_local() => {
                 let def_id = def_id.expect_local();
@@ -546,7 +547,9 @@ impl<'tcx> InferCtxt<'tcx> {
                     );
                 }
             }
-            ty::TypingMode::PostAnalysis => bug!("insert hidden type post-analysis"),
+            mode @ (ty::TypingMode::PostBorrowckAnalysis { .. } | ty::TypingMode::PostAnalysis) => {
+                bug!("insert hidden type in {mode:?}")
+            }
         }
 
         Ok(())
diff --git a/compiler/rustc_middle/src/ty/context.rs b/compiler/rustc_middle/src/ty/context.rs
index 5bf62a17c8e08..5d3f4a28bc199 100644
--- a/compiler/rustc_middle/src/ty/context.rs
+++ b/compiler/rustc_middle/src/ty/context.rs
@@ -632,6 +632,14 @@ impl<'tcx> Interner for TyCtxt<'tcx> {
     fn opaque_types_defined_by(self, defining_anchor: LocalDefId) -> Self::DefiningOpaqueTypes {
         self.opaque_types_defined_by(defining_anchor)
     }
+
+    fn fold_regions<T: TypeFoldable<TyCtxt<'tcx>>>(
+        self,
+        value: T,
+        f: impl FnMut(ty::Region<'tcx>, ty::DebruijnIndex) -> ty::Region<'tcx>,
+    ) -> T {
+        self.fold_regions(value, f)
+    }
 }
 
 macro_rules! bidirectional_lang_item_map {
diff --git a/compiler/rustc_middle/src/ty/fold.rs b/compiler/rustc_middle/src/ty/fold.rs
index 7adbd556141fe..1e9e3354e9d19 100644
--- a/compiler/rustc_middle/src/ty/fold.rs
+++ b/compiler/rustc_middle/src/ty/fold.rs
@@ -55,14 +55,11 @@ where
 
 impl<'tcx> TyCtxt<'tcx> {
     /// Folds the escaping and free regions in `value` using `f`.
-    pub fn fold_regions<T>(
+    pub fn fold_regions<T: TypeFoldable<TyCtxt<'tcx>>>(
         self,
         value: T,
         mut f: impl FnMut(ty::Region<'tcx>, ty::DebruijnIndex) -> ty::Region<'tcx>,
-    ) -> T
-    where
-        T: TypeFoldable<TyCtxt<'tcx>>,
-    {
+    ) -> T {
         value.fold_with(&mut RegionFolder::new(self, &mut f))
     }
 }
diff --git a/compiler/rustc_middle/src/ty/mod.rs b/compiler/rustc_middle/src/ty/mod.rs
index c7a2223ecd78b..4492f35525dcb 100644
--- a/compiler/rustc_middle/src/ty/mod.rs
+++ b/compiler/rustc_middle/src/ty/mod.rs
@@ -23,6 +23,11 @@ pub use adt::*;
 pub use assoc::*;
 pub use generic_args::{GenericArgKind, TermKind, *};
 pub use generics::*;
+// Can't use a glob import here as it would cause
+// ambiguity when importing the actual types implementing
+// the inherent traits from this module.
+#[allow(rustc::non_glob_import_of_type_ir_inherent)]
+use inherent::SliceLike;
 pub use intrinsic::IntrinsicDef;
 use rustc_abi::{Align, FieldIdx, Integer, IntegerType, ReprFlags, ReprOptions, VariantIdx};
 use rustc_ast::expand::StrippedCfgItem;
@@ -970,7 +975,7 @@ pub struct ParamEnv<'tcx> {
 }
 
 impl<'tcx> rustc_type_ir::inherent::ParamEnv<TyCtxt<'tcx>> for ParamEnv<'tcx> {
-    fn caller_bounds(self) -> impl IntoIterator<Item = ty::Clause<'tcx>> {
+    fn caller_bounds(self) -> impl SliceLike<Item = ty::Clause<'tcx>> {
         self.caller_bounds()
     }
 }
diff --git a/compiler/rustc_next_trait_solver/src/canonicalizer.rs b/compiler/rustc_next_trait_solver/src/canonicalizer.rs
index 63608f9e85615..2f7301d8fe515 100644
--- a/compiler/rustc_next_trait_solver/src/canonicalizer.rs
+++ b/compiler/rustc_next_trait_solver/src/canonicalizer.rs
@@ -3,6 +3,7 @@ use std::cmp::Ordering;
 use rustc_type_ir::data_structures::HashMap;
 use rustc_type_ir::fold::{TypeFoldable, TypeFolder, TypeSuperFoldable};
 use rustc_type_ir::inherent::*;
+use rustc_type_ir::solve::{Goal, QueryInput};
 use rustc_type_ir::visit::TypeVisitableExt;
 use rustc_type_ir::{
     self as ty, Canonical, CanonicalTyVarKind, CanonicalVarInfo, CanonicalVarKind, InferCtxtLike,
@@ -17,8 +18,11 @@ use crate::delegate::SolverDelegate;
 /// while canonicalizing the response happens in the context of the
 /// query.
 #[derive(Debug, Clone, Copy)]
-pub enum CanonicalizeMode {
-    Input,
+enum CanonicalizeMode {
+    /// When canonicalizing the `param_env`, we keep `'static` as merging
+    /// trait candidates relies on it when deciding whether a where-bound
+    /// is trivial.
+    Input { keep_static: bool },
     /// FIXME: We currently return region constraints referring to
     /// placeholders and inference variables from a binder instantiated
     /// inside of the query.
@@ -59,15 +63,15 @@ pub struct Canonicalizer<'a, D: SolverDelegate<Interner = I>, I: Interner> {
 }
 
 impl<'a, D: SolverDelegate<Interner = I>, I: Interner> Canonicalizer<'a, D, I> {
-    pub fn canonicalize<T: TypeFoldable<I>>(
+    pub fn canonicalize_response<T: TypeFoldable<I>>(
         delegate: &'a D,
-        canonicalize_mode: CanonicalizeMode,
+        max_input_universe: ty::UniverseIndex,
         variables: &'a mut Vec<I::GenericArg>,
         value: T,
     ) -> ty::Canonical<I, T> {
         let mut canonicalizer = Canonicalizer {
             delegate,
-            canonicalize_mode,
+            canonicalize_mode: CanonicalizeMode::Response { max_input_universe },
 
             variables,
             variable_lookup_table: Default::default(),
@@ -80,9 +84,67 @@ impl<'a, D: SolverDelegate<Interner = I>, I: Interner> Canonicalizer<'a, D, I> {
         let value = value.fold_with(&mut canonicalizer);
         assert!(!value.has_infer(), "unexpected infer in {value:?}");
         assert!(!value.has_placeholders(), "unexpected placeholders in {value:?}");
-
         let (max_universe, variables) = canonicalizer.finalize();
+        Canonical { max_universe, variables, value }
+    }
+
+    /// When canonicalizing query inputs, we keep `'static` in the `param_env`
+    /// but erase it everywhere else. We generally don't want to depend on region
+    /// identity, so while it should not matter whether `'static` is kept in the
+    /// value or opaque type storage as well, this prevents us from accidentally
+    /// relying on it in the future.
+    ///
+    /// We want to keep the option of canonicalizing `'static` to an existential
+    /// variable in the future by changing the way we detect global where-bounds.
+    pub fn canonicalize_input<P: TypeFoldable<I>>(
+        delegate: &'a D,
+        variables: &'a mut Vec<I::GenericArg>,
+        input: QueryInput<I, P>,
+    ) -> ty::Canonical<I, QueryInput<I, P>> {
+        // First canonicalize the `param_env` while keeping `'static`
+        let mut env_canonicalizer = Canonicalizer {
+            delegate,
+            canonicalize_mode: CanonicalizeMode::Input { keep_static: true },
+
+            variables,
+            variable_lookup_table: Default::default(),
+            primitive_var_infos: Vec::new(),
+            binder_index: ty::INNERMOST,
+
+            cache: Default::default(),
+        };
+        let param_env = input.goal.param_env.fold_with(&mut env_canonicalizer);
+        debug_assert_eq!(env_canonicalizer.binder_index, ty::INNERMOST);
+        // Then canonicalize the rest of the input without keeping `'static`
+        // while *mostly* reusing the canonicalizer from above.
+        let mut rest_canonicalizer = Canonicalizer {
+            delegate,
+            canonicalize_mode: CanonicalizeMode::Input { keep_static: false },
+
+            variables: env_canonicalizer.variables,
+            // We're able to reuse the `variable_lookup_table` as whether or not
+            // it already contains an entry for `'static` does not matter.
+            variable_lookup_table: env_canonicalizer.variable_lookup_table,
+            primitive_var_infos: env_canonicalizer.primitive_var_infos,
+            binder_index: ty::INNERMOST,
 
+            // We do not reuse the cache as it may contain entries whose canonicalized
+            // value contains `'static`. While we could alternatively handle this by
+            // checking for `'static` when using cached entries, this does not
+            // feel worth the effort. I do not expect that a `ParamEnv` will ever
+            // contain large enough types for caching to be necessary.
+            cache: Default::default(),
+        };
+
+        let predicate = input.goal.predicate.fold_with(&mut rest_canonicalizer);
+        let goal = Goal { param_env, predicate };
+        let predefined_opaques_in_body =
+            input.predefined_opaques_in_body.fold_with(&mut rest_canonicalizer);
+        let value = QueryInput { goal, predefined_opaques_in_body };
+
+        assert!(!value.has_infer(), "unexpected infer in {value:?}");
+        assert!(!value.has_placeholders(), "unexpected placeholders in {value:?}");
+        let (max_universe, variables) = rest_canonicalizer.finalize();
         Canonical { max_universe, variables, value }
     }
 
@@ -126,7 +188,7 @@ impl<'a, D: SolverDelegate<Interner = I>, I: Interner> Canonicalizer<'a, D, I> {
             // all information which should not matter for the solver.
             //
             // For this we compress universes as much as possible.
-            CanonicalizeMode::Input => {}
+            CanonicalizeMode::Input { .. } => {}
             // When canonicalizing a response we map a universes already entered
             // by the caller to the root universe and only return useful universe
             // information for placeholders and inference variables created inside
@@ -290,17 +352,15 @@ impl<'a, D: SolverDelegate<Interner = I>, I: Interner> Canonicalizer<'a, D, I> {
                 }
             },
             ty::Placeholder(placeholder) => match self.canonicalize_mode {
-                CanonicalizeMode::Input => CanonicalVarKind::PlaceholderTy(PlaceholderLike::new(
-                    placeholder.universe(),
-                    self.variables.len().into(),
-                )),
+                CanonicalizeMode::Input { .. } => CanonicalVarKind::PlaceholderTy(
+                    PlaceholderLike::new(placeholder.universe(), self.variables.len().into()),
+                ),
                 CanonicalizeMode::Response { .. } => CanonicalVarKind::PlaceholderTy(placeholder),
             },
             ty::Param(_) => match self.canonicalize_mode {
-                CanonicalizeMode::Input => CanonicalVarKind::PlaceholderTy(PlaceholderLike::new(
-                    ty::UniverseIndex::ROOT,
-                    self.variables.len().into(),
-                )),
+                CanonicalizeMode::Input { .. } => CanonicalVarKind::PlaceholderTy(
+                    PlaceholderLike::new(ty::UniverseIndex::ROOT, self.variables.len().into()),
+                ),
                 CanonicalizeMode::Response { .. } => panic!("param ty in response: {t:?}"),
             },
             ty::Bool
@@ -357,21 +417,30 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> TypeFolder<I> for Canonicaliz
         let kind = match r.kind() {
             ty::ReBound(..) => return r,
 
-            // We may encounter `ReStatic` in item signatures or the hidden type
-            // of an opaque. `ReErased` should only be encountered in the hidden
+            // We don't canonicalize `ReStatic` in the `param_env` as we use it
+            // when checking whether a `ParamEnv` candidate is global.
+            ty::ReStatic => match self.canonicalize_mode {
+                CanonicalizeMode::Input { keep_static: false } => {
+                    CanonicalVarKind::Region(ty::UniverseIndex::ROOT)
+                }
+                CanonicalizeMode::Input { keep_static: true }
+                | CanonicalizeMode::Response { .. } => return r,
+            },
+
+            // `ReErased` should only be encountered in the hidden
             // type of an opaque for regions that are ignored for the purposes of
             // captures.
             //
             // FIXME: We should investigate the perf implications of not uniquifying
             // `ReErased`. We may be able to short-circuit registering region
             // obligations if we encounter a `ReErased` on one side, for example.
-            ty::ReStatic | ty::ReErased | ty::ReError(_) => match self.canonicalize_mode {
-                CanonicalizeMode::Input => CanonicalVarKind::Region(ty::UniverseIndex::ROOT),
+            ty::ReErased | ty::ReError(_) => match self.canonicalize_mode {
+                CanonicalizeMode::Input { .. } => CanonicalVarKind::Region(ty::UniverseIndex::ROOT),
                 CanonicalizeMode::Response { .. } => return r,
             },
 
             ty::ReEarlyParam(_) | ty::ReLateParam(_) => match self.canonicalize_mode {
-                CanonicalizeMode::Input => CanonicalVarKind::Region(ty::UniverseIndex::ROOT),
+                CanonicalizeMode::Input { .. } => CanonicalVarKind::Region(ty::UniverseIndex::ROOT),
                 CanonicalizeMode::Response { .. } => {
                     panic!("unexpected region in response: {r:?}")
                 }
@@ -379,7 +448,7 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> TypeFolder<I> for Canonicaliz
 
             ty::RePlaceholder(placeholder) => match self.canonicalize_mode {
                 // We canonicalize placeholder regions as existentials in query inputs.
-                CanonicalizeMode::Input => CanonicalVarKind::Region(ty::UniverseIndex::ROOT),
+                CanonicalizeMode::Input { .. } => CanonicalVarKind::Region(ty::UniverseIndex::ROOT),
                 CanonicalizeMode::Response { max_input_universe } => {
                     // If we have a placeholder region inside of a query, it must be from
                     // a new universe.
@@ -397,7 +466,9 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> TypeFolder<I> for Canonicaliz
                     "region vid should have been resolved fully before canonicalization"
                 );
                 match self.canonicalize_mode {
-                    CanonicalizeMode::Input => CanonicalVarKind::Region(ty::UniverseIndex::ROOT),
+                    CanonicalizeMode::Input { keep_static: _ } => {
+                        CanonicalVarKind::Region(ty::UniverseIndex::ROOT)
+                    }
                     CanonicalizeMode::Response { .. } => {
                         CanonicalVarKind::Region(self.delegate.universe_of_lt(vid).unwrap())
                     }
@@ -434,7 +505,7 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> TypeFolder<I> for Canonicaliz
                 ty::InferConst::Fresh(_) => todo!(),
             },
             ty::ConstKind::Placeholder(placeholder) => match self.canonicalize_mode {
-                CanonicalizeMode::Input => CanonicalVarKind::PlaceholderConst(
+                CanonicalizeMode::Input { .. } => CanonicalVarKind::PlaceholderConst(
                     PlaceholderLike::new(placeholder.universe(), self.variables.len().into()),
                 ),
                 CanonicalizeMode::Response { .. } => {
@@ -442,7 +513,7 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> TypeFolder<I> for Canonicaliz
                 }
             },
             ty::ConstKind::Param(_) => match self.canonicalize_mode {
-                CanonicalizeMode::Input => CanonicalVarKind::PlaceholderConst(
+                CanonicalizeMode::Input { .. } => CanonicalVarKind::PlaceholderConst(
                     PlaceholderLike::new(ty::UniverseIndex::ROOT, self.variables.len().into()),
                 ),
                 CanonicalizeMode::Response { .. } => panic!("param ty in response: {c:?}"),
diff --git a/compiler/rustc_next_trait_solver/src/solve/alias_relate.rs b/compiler/rustc_next_trait_solver/src/solve/alias_relate.rs
index d8c1dc8b4e9f3..9f29e247e8c62 100644
--- a/compiler/rustc_next_trait_solver/src/solve/alias_relate.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/alias_relate.rs
@@ -15,12 +15,19 @@
 //! (3.) Otherwise, if we end with two rigid (non-projection) or infer types,
 //! relate them structurally.
 
+use rustc_type_ir::data_structures::HashSet;
 use rustc_type_ir::inherent::*;
+use rustc_type_ir::visit::{TypeSuperVisitable, TypeVisitable, TypeVisitableExt, TypeVisitor};
 use rustc_type_ir::{self as ty, Interner};
 use tracing::{instrument, trace};
 
 use crate::delegate::SolverDelegate;
-use crate::solve::{Certainty, EvalCtxt, Goal, QueryResult};
+use crate::solve::{Certainty, EvalCtxt, Goal, NoSolution, QueryResult};
+
+enum IgnoreAliases {
+    Yes,
+    No,
+}
 
 impl<D, I> EvalCtxt<'_, D>
 where
@@ -36,6 +43,12 @@ where
         let Goal { param_env, predicate: (lhs, rhs, direction) } = goal;
         debug_assert!(lhs.to_alias_term().is_some() || rhs.to_alias_term().is_some());
 
+        if self.alias_cannot_name_placeholder_in_rigid(param_env, lhs, rhs)
+            || self.alias_cannot_name_placeholder_in_rigid(param_env, rhs, lhs)
+        {
+            return Err(NoSolution);
+        }
+
         // Structurally normalize the lhs.
         let lhs = if let Some(alias) = lhs.to_alias_term() {
             let term = self.next_term_infer_of_kind(lhs);
@@ -96,4 +109,100 @@ where
             }
         }
     }
+
+    /// In case a rigid term refers to a placeholder which is not referenced by the
+    /// alias, the alias cannot be normalized to that rigid term unless it contains
+    /// either inference variables or these placeholders are referenced in a term
+    /// of a `Projection`-clause in the environment.
+    fn alias_cannot_name_placeholder_in_rigid(
+        &mut self,
+        param_env: I::ParamEnv,
+        rigid_term: I::Term,
+        alias: I::Term,
+    ) -> bool {
+        // Check that the rigid term is actually rigid.
+        if rigid_term.to_alias_term().is_some() || alias.to_alias_term().is_none() {
+            return false;
+        }
+
+        // If the alias has any type or const inference variables,
+        // do not try to apply the fast path as these inference variables
+        // may resolve to something containing placeholders.
+        if alias.has_non_region_infer() {
+            return false;
+        }
+
+        let mut referenced_placeholders =
+            self.collect_placeholders_in_term(rigid_term, IgnoreAliases::Yes);
+        for clause in param_env.caller_bounds().iter() {
+            match clause.kind().skip_binder() {
+                ty::ClauseKind::Projection(ty::ProjectionPredicate { term, .. }) => {
+                    if term.has_non_region_infer() {
+                        return false;
+                    }
+
+                    let env_term_placeholders =
+                        self.collect_placeholders_in_term(term, IgnoreAliases::No);
+                    #[allow(rustc::potential_query_instability)]
+                    referenced_placeholders.retain(|p| !env_term_placeholders.contains(p));
+                }
+                ty::ClauseKind::Trait(_)
+                | ty::ClauseKind::HostEffect(_)
+                | ty::ClauseKind::TypeOutlives(_)
+                | ty::ClauseKind::RegionOutlives(_)
+                | ty::ClauseKind::ConstArgHasType(..)
+                | ty::ClauseKind::WellFormed(_)
+                | ty::ClauseKind::ConstEvaluatable(_) => continue,
+            }
+        }
+
+        if referenced_placeholders.is_empty() {
+            return false;
+        }
+
+        let alias_placeholders = self.collect_placeholders_in_term(alias, IgnoreAliases::No);
+        // If the rigid term references a placeholder not mentioned by the alias,
+        // they can never unify.
+        !referenced_placeholders.is_subset(&alias_placeholders)
+    }
+
+    fn collect_placeholders_in_term(
+        &mut self,
+        term: I::Term,
+        ignore_aliases: IgnoreAliases,
+    ) -> HashSet<I::Term> {
+        // Fast path to avoid walking the term.
+        if !term.has_placeholders() {
+            return Default::default();
+        }
+
+        struct PlaceholderCollector<I: Interner> {
+            ignore_aliases: IgnoreAliases,
+            placeholders: HashSet<I::Term>,
+        }
+        impl<I: Interner> TypeVisitor<I> for PlaceholderCollector<I> {
+            type Result = ();
+
+            fn visit_ty(&mut self, t: I::Ty) {
+                match t.kind() {
+                    ty::Placeholder(_) => drop(self.placeholders.insert(t.into())),
+                    ty::Alias(..) if matches!(self.ignore_aliases, IgnoreAliases::Yes) => {}
+                    _ => t.super_visit_with(self),
+                }
+            }
+
+            fn visit_const(&mut self, ct: I::Const) {
+                match ct.kind() {
+                    ty::ConstKind::Placeholder(_) => drop(self.placeholders.insert(ct.into())),
+                    ty::ConstKind::Unevaluated(_) | ty::ConstKind::Expr(_)
+                        if matches!(self.ignore_aliases, IgnoreAliases::Yes) => {}
+                    _ => ct.super_visit_with(self),
+                }
+            }
+        }
+
+        let mut visitor = PlaceholderCollector { ignore_aliases, placeholders: Default::default() };
+        term.visit_with(&mut visitor);
+        visitor.placeholders
+    }
 }
diff --git a/compiler/rustc_next_trait_solver/src/solve/assembly/mod.rs b/compiler/rustc_next_trait_solver/src/solve/assembly/mod.rs
index adac35b57cd70..9d85259eb593d 100644
--- a/compiler/rustc_next_trait_solver/src/solve/assembly/mod.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/assembly/mod.rs
@@ -11,6 +11,7 @@ use rustc_type_ir::visit::TypeVisitableExt as _;
 use rustc_type_ir::{self as ty, Interner, TypingMode, Upcast as _, elaborate};
 use tracing::{debug, instrument};
 
+use super::trait_goals::ProvenVia;
 use crate::delegate::SolverDelegate;
 use crate::solve::inspect::ProbeKind;
 use crate::solve::{
@@ -337,13 +338,6 @@ where
 
         self.assemble_param_env_candidates(goal, &mut candidates);
 
-        match self.typing_mode() {
-            TypingMode::Coherence => {}
-            TypingMode::Analysis { .. } | TypingMode::PostAnalysis => {
-                self.discard_impls_shadowed_by_env(goal, &mut candidates);
-            }
-        }
-
         candidates
     }
 
@@ -498,7 +492,7 @@ where
         goal: Goal<I, G>,
         candidates: &mut Vec<Candidate<I>>,
     ) {
-        for (i, assumption) in goal.param_env.caller_bounds().into_iter().enumerate() {
+        for (i, assumption) in goal.param_env.caller_bounds().iter().enumerate() {
             candidates.extend(G::probe_and_consider_implied_clause(
                 self,
                 CandidateSource::ParamEnv(i),
@@ -731,72 +725,38 @@ where
         })
     }
 
-    /// If there's a where-bound for the current goal, do not use any impl candidates
-    /// to prove the current goal. Most importantly, if there is a where-bound which does
-    /// not specify any associated types, we do not allow normalizing the associated type
-    /// by using an impl, even if it would apply.
-    ///
-    ///  <https://github.com/rust-lang/trait-system-refactor-initiative/issues/76>
-    // FIXME(@lcnr): The current structure here makes me unhappy and feels ugly. idk how
-    // to improve this however. However, this should make it fairly straightforward to refine
-    // the filtering going forward, so it seems alright-ish for now.
-    #[instrument(level = "debug", skip(self, goal))]
-    fn discard_impls_shadowed_by_env<G: GoalKind<D>>(
+    // TODO comments
+    #[instrument(level = "debug", skip(self), ret)]
+    pub(super) fn merge_candidates(
         &mut self,
-        goal: Goal<I, G>,
-        candidates: &mut Vec<Candidate<I>>,
-    ) {
-        let cx = self.cx();
-        let trait_goal: Goal<I, ty::TraitPredicate<I>> =
-            goal.with(cx, goal.predicate.trait_ref(cx));
-
-        let mut trait_candidates_from_env = vec![];
-        self.probe(|_| ProbeKind::ShadowedEnvProbing).enter(|ecx| {
-            ecx.assemble_param_env_candidates(trait_goal, &mut trait_candidates_from_env);
-            ecx.assemble_alias_bound_candidates(trait_goal, &mut trait_candidates_from_env);
-        });
+        proven_via: Option<ProvenVia>,
+        candidates: Vec<Candidate<I>>,
+    ) -> QueryResult<I> {
+        let Some(proven_via) = proven_via else {
+            // We don't care about overflow. If proving the trait goal overflowed, then
+            // it's enough to report an overflow error for that, we don't also have to
+            // overflow during normalization.
+            return Ok(self.make_ambiguous_response_no_constraints(MaybeCause::Ambiguity));
+        };
 
-        if !trait_candidates_from_env.is_empty() {
-            let trait_env_result = self.merge_candidates(trait_candidates_from_env);
-            match trait_env_result.unwrap().value.certainty {
-                // If proving the trait goal succeeds by using the env,
-                // we freely drop all impl candidates.
-                //
-                // FIXME(@lcnr): It feels like this could easily hide
-                // a forced ambiguity candidate added earlier.
-                // This feels dangerous.
-                Certainty::Yes => {
-                    candidates.retain(|c| match c.source {
-                        CandidateSource::Impl(_) | CandidateSource::BuiltinImpl(_) => {
-                            debug!(?c, "discard impl candidate");
-                            false
-                        }
-                        CandidateSource::ParamEnv(_) | CandidateSource::AliasBound => true,
-                        CandidateSource::CoherenceUnknowable => panic!("uh oh"),
-                    });
-                }
-                // If it is still ambiguous we instead just force the whole goal
-                // to be ambig and wait for inference constraints. See
-                // tests/ui/traits/next-solver/env-shadows-impls/ambig-env-no-shadow.rs
-                Certainty::Maybe(cause) => {
-                    debug!(?cause, "force ambiguity");
-                    *candidates = self.forced_ambiguity(cause).into_iter().collect();
-                }
-            }
-        }
-    }
+        let responses: Vec<_> = match proven_via {
+            // Even when a trait bound has been proven using a where-bound, we
+            // still need to consider alias-bounds for normalization, see
+            // tests/ui/next-solver/alias-bound-shadowed-by-env.rs.
+            //
+            // FIXME(const_trait_impl): should this behavior also be used by
+            // constness checking. Doing so is *at least theoretically* breaking,
+            // see github.com/rust-lang/rust/issues/133044#issuecomment-2500709754
+            ProvenVia::ParamEnv | ProvenVia::AliasBound => candidates
+                .iter()
+                .filter(|c| {
+                    matches!(c.source, CandidateSource::AliasBound | CandidateSource::ParamEnv(_))
+                })
+                .map(|c| c.result)
+                .collect(),
+            ProvenVia::Impl => candidates.iter().map(|c| c.result).collect(),
+        };
 
-    /// If there are multiple ways to prove a trait or projection goal, we have
-    /// to somehow try to merge the candidates into one. If that fails, we return
-    /// ambiguity.
-    #[instrument(level = "debug", skip(self), ret)]
-    pub(super) fn merge_candidates(&mut self, candidates: Vec<Candidate<I>>) -> QueryResult<I> {
-        // First try merging all candidates. This is complete and fully sound.
-        let responses = candidates.iter().map(|c| c.result).collect::<Vec<_>>();
-        if let Some(result) = self.try_merge_responses(&responses) {
-            return Ok(result);
-        } else {
-            self.flounder(&responses)
-        }
+        self.try_merge_responses(&responses).map_or_else(|| self.flounder(&responses), Ok)
     }
 }
diff --git a/compiler/rustc_next_trait_solver/src/solve/effect_goals.rs b/compiler/rustc_next_trait_solver/src/solve/effect_goals.rs
index 81b5199002b23..ce7552e30f0fe 100644
--- a/compiler/rustc_next_trait_solver/src/solve/effect_goals.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/effect_goals.rs
@@ -4,6 +4,7 @@
 use rustc_type_ir::fast_reject::DeepRejectCtxt;
 use rustc_type_ir::inherent::*;
 use rustc_type_ir::lang_items::TraitSolverLangItem;
+use rustc_type_ir::solve::inspect::ProbeKind;
 use rustc_type_ir::{self as ty, Interner, elaborate};
 use tracing::instrument;
 
@@ -391,6 +392,11 @@ where
         goal: Goal<I, ty::HostEffectPredicate<I>>,
     ) -> QueryResult<I> {
         let candidates = self.assemble_and_evaluate_candidates(goal);
-        self.merge_candidates(candidates)
+        let (_, proven_via) = self.probe(|_| ProbeKind::ShadowedEnvProbing).enter(|ecx| {
+            let trait_goal: Goal<I, ty::TraitPredicate<I>> =
+                goal.with(ecx.cx(), goal.predicate.trait_ref);
+            ecx.compute_trait_goal(trait_goal)
+        })?;
+        self.merge_candidates(proven_via, candidates)
     }
 }
diff --git a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/canonical.rs b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/canonical.rs
index a143af13688ba..e99cd3d272700 100644
--- a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/canonical.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/canonical.rs
@@ -18,7 +18,7 @@ use rustc_type_ir::relate::solver_relating::RelateExt;
 use rustc_type_ir::{self as ty, Canonical, CanonicalVarValues, InferCtxtLike, Interner};
 use tracing::{debug, instrument, trace};
 
-use crate::canonicalizer::{CanonicalizeMode, Canonicalizer};
+use crate::canonicalizer::Canonicalizer;
 use crate::delegate::SolverDelegate;
 use crate::resolve::EagerResolver;
 use crate::solve::eval_ctxt::NestedGoals;
@@ -60,17 +60,13 @@ where
             (goal, opaque_types).fold_with(&mut EagerResolver::new(self.delegate));
 
         let mut orig_values = Default::default();
-        let canonical = Canonicalizer::canonicalize(
-            self.delegate,
-            CanonicalizeMode::Input,
-            &mut orig_values,
-            QueryInput {
+        let canonical =
+            Canonicalizer::canonicalize_input(self.delegate, &mut orig_values, QueryInput {
                 goal,
                 predefined_opaques_in_body: self
                     .cx()
                     .mk_predefined_opaques_in_body(PredefinedOpaquesData { opaque_types }),
-            },
-        );
+            });
         let query_input = ty::CanonicalQueryInput { canonical, typing_mode: self.typing_mode() };
         (orig_values, query_input)
     }
@@ -148,9 +144,9 @@ where
             .region_constraints
             .retain(|outlives| outlives.0.as_region().map_or(true, |re| re != outlives.1));
 
-        let canonical = Canonicalizer::canonicalize(
+        let canonical = Canonicalizer::canonicalize_response(
             self.delegate,
-            CanonicalizeMode::Response { max_input_universe: self.max_input_universe },
+            self.max_input_universe,
             &mut Default::default(),
             Response {
                 var_values,
@@ -428,12 +424,7 @@ where
     let var_values = CanonicalVarValues { var_values: delegate.cx().mk_args(var_values) };
     let state = inspect::State { var_values, data };
     let state = state.fold_with(&mut EagerResolver::new(delegate));
-    Canonicalizer::canonicalize(
-        delegate,
-        CanonicalizeMode::Response { max_input_universe },
-        &mut vec![],
-        state,
-    )
+    Canonicalizer::canonicalize_response(delegate, max_input_universe, &mut vec![], state)
 }
 
 // FIXME: needs to be pub to be accessed by downstream
diff --git a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs
index 40d1576256eb9..8c74490e0e0ee 100644
--- a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs
@@ -440,7 +440,7 @@ where
         if let Some(kind) = kind.no_bound_vars() {
             match kind {
                 ty::PredicateKind::Clause(ty::ClauseKind::Trait(predicate)) => {
-                    self.compute_trait_goal(Goal { param_env, predicate })
+                    self.compute_trait_goal(Goal { param_env, predicate }).map(|(r, _via)| r)
                 }
                 ty::PredicateKind::Clause(ty::ClauseKind::HostEffect(predicate)) => {
                     self.compute_host_effect_goal(Goal { param_env, predicate })
@@ -644,6 +644,12 @@ where
         }
     }
 
+    pub(super) fn next_region_var(&mut self) -> I::Region {
+        let region = self.delegate.next_region_infer();
+        self.inspect.add_var_value(region);
+        region
+    }
+
     pub(super) fn next_ty_infer(&mut self) -> I::Ty {
         let ty = self.delegate.next_ty_infer();
         self.inspect.add_var_value(ty);
diff --git a/compiler/rustc_next_trait_solver/src/solve/mod.rs b/compiler/rustc_next_trait_solver/src/solve/mod.rs
index 5c54656cc59f5..37678bfd8805f 100644
--- a/compiler/rustc_next_trait_solver/src/solve/mod.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/mod.rs
@@ -23,7 +23,7 @@ mod trait_goals;
 
 use rustc_type_ir::inherent::*;
 pub use rustc_type_ir::solve::*;
-use rustc_type_ir::{self as ty, Interner};
+use rustc_type_ir::{self as ty, Interner, TypingMode};
 use tracing::instrument;
 
 pub use self::eval_ctxt::{EvalCtxt, GenerateProofTree, SolverDelegateEvalExt};
@@ -243,22 +243,27 @@ where
             .copied()
     }
 
+    fn bail_with_ambiguity(&mut self, responses: &[CanonicalResponse<I>]) -> CanonicalResponse<I> {
+        debug_assert!(!responses.is_empty());
+        if let Certainty::Maybe(maybe_cause) =
+            responses.iter().fold(Certainty::AMBIGUOUS, |certainty, response| {
+                certainty.unify_with(response.value.certainty)
+            })
+        {
+            self.make_ambiguous_response_no_constraints(maybe_cause)
+        } else {
+            panic!("expected flounder response to be ambiguous")
+        }
+    }
+
     /// If we fail to merge responses we flounder and return overflow or ambiguity.
     #[instrument(level = "trace", skip(self), ret)]
     fn flounder(&mut self, responses: &[CanonicalResponse<I>]) -> QueryResult<I> {
         if responses.is_empty() {
             return Err(NoSolution);
+        } else {
+            Ok(self.bail_with_ambiguity(responses))
         }
-
-        let Certainty::Maybe(maybe_cause) =
-            responses.iter().fold(Certainty::AMBIGUOUS, |certainty, response| {
-                certainty.unify_with(response.value.certainty)
-            })
-        else {
-            panic!("expected flounder response to be ambiguous")
-        };
-
-        Ok(self.make_ambiguous_response_no_constraints(maybe_cause))
     }
 
     /// Normalize a type for when it is structurally matched on.
@@ -321,6 +326,19 @@ where
             Ok(ct)
         }
     }
+
+    fn opaque_type_is_rigid(&self, def_id: I::DefId) -> bool {
+        match self.typing_mode() {
+            // Opaques are never rigid outside of analysis mode.
+            TypingMode::Coherence | TypingMode::PostAnalysis => false,
+            // During analysis, opaques are rigid unless they may be defined by
+            // the current body.
+            TypingMode::Analysis { defining_opaque_types: non_rigid_opaques }
+            | TypingMode::PostBorrowckAnalysis { defined_opaque_types: non_rigid_opaques } => {
+                !def_id.as_local().is_some_and(|def_id| non_rigid_opaques.contains(&def_id))
+            }
+        }
+    }
 }
 
 fn response_no_constraints_raw<I: Interner>(
diff --git a/compiler/rustc_next_trait_solver/src/solve/normalizes_to/mod.rs b/compiler/rustc_next_trait_solver/src/solve/normalizes_to/mod.rs
index 33bd1cf2f56ee..ded7f994e261a 100644
--- a/compiler/rustc_next_trait_solver/src/solve/normalizes_to/mod.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/normalizes_to/mod.rs
@@ -6,7 +6,7 @@ mod weak_types;
 use rustc_type_ir::fast_reject::DeepRejectCtxt;
 use rustc_type_ir::inherent::*;
 use rustc_type_ir::lang_items::TraitSolverLangItem;
-use rustc_type_ir::{self as ty, Interner, NormalizesTo, TypingMode, Upcast as _};
+use rustc_type_ir::{self as ty, Interner, NormalizesTo, Upcast as _};
 use tracing::instrument;
 
 use crate::delegate::SolverDelegate;
@@ -71,21 +71,10 @@ where
                 Ok(())
             }
             ty::AliasTermKind::OpaqueTy => {
-                match self.typing_mode() {
-                    // Opaques are never rigid outside of analysis mode.
-                    TypingMode::Coherence | TypingMode::PostAnalysis => Err(NoSolution),
-                    // During analysis, opaques are only rigid if we may not define it.
-                    TypingMode::Analysis { defining_opaque_types } => {
-                        if rigid_alias
-                            .def_id
-                            .as_local()
-                            .is_some_and(|def_id| defining_opaque_types.contains(&def_id))
-                        {
-                            Err(NoSolution)
-                        } else {
-                            Ok(())
-                        }
-                    }
+                if self.opaque_type_is_rigid(rigid_alias.def_id) {
+                    Ok(())
+                } else {
+                    Err(NoSolution)
                 }
             }
             // FIXME(generic_const_exprs): we would need to support generic consts here
@@ -99,10 +88,17 @@ where
     /// returns `NoSolution`.
     #[instrument(level = "trace", skip(self), ret)]
     fn normalize_at_least_one_step(&mut self, goal: Goal<I, NormalizesTo<I>>) -> QueryResult<I> {
-        match goal.predicate.alias.kind(self.cx()) {
+        let cx = self.cx();
+        match goal.predicate.alias.kind(cx) {
             ty::AliasTermKind::ProjectionTy | ty::AliasTermKind::ProjectionConst => {
                 let candidates = self.assemble_and_evaluate_candidates(goal);
-                self.merge_candidates(candidates)
+                let (_, proven_via) =
+                    self.probe(|_| ProbeKind::ShadowedEnvProbing).enter(|ecx| {
+                        let trait_goal: Goal<I, ty::TraitPredicate<I>> =
+                            goal.with(cx, goal.predicate.alias.trait_ref(cx));
+                        ecx.compute_trait_goal(trait_goal)
+                    })?;
+                self.merge_candidates(proven_via, candidates)
             }
             ty::AliasTermKind::InherentTy => self.normalize_inherent_associated_type(goal),
             ty::AliasTermKind::OpaqueTy => self.normalize_opaque_type(goal),
diff --git a/compiler/rustc_next_trait_solver/src/solve/normalizes_to/opaque_types.rs b/compiler/rustc_next_trait_solver/src/solve/normalizes_to/opaque_types.rs
index 336bcb9df33a6..be739b264129a 100644
--- a/compiler/rustc_next_trait_solver/src/solve/normalizes_to/opaque_types.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/normalizes_to/opaque_types.rs
@@ -95,6 +95,26 @@ where
                 );
                 self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
             }
+            TypingMode::PostBorrowckAnalysis { defined_opaque_types } => {
+                let Some(def_id) = opaque_ty.def_id.as_local() else {
+                    return Err(NoSolution);
+                };
+
+                if !defined_opaque_types.contains(&def_id) {
+                    return Err(NoSolution);
+                }
+
+                let actual = cx.type_of(opaque_ty.def_id).instantiate(cx, opaque_ty.args);
+                // FIXME: Actually use a proper binder here instead of relying on `ReErased`.
+                //
+                // This is also probably unsound or sth :shrug:
+                let actual = cx.fold_regions(actual, |re, _dbi| match re.kind() {
+                    ty::ReErased => self.next_region_var(),
+                    _ => re,
+                });
+                self.eq(goal.param_env, expected, actual)?;
+                self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
+            }
             TypingMode::PostAnalysis => {
                 // FIXME: Add an assertion that opaque type storage is empty.
                 let actual = cx.type_of(opaque_ty.def_id).instantiate(cx, opaque_ty.args);
diff --git a/compiler/rustc_next_trait_solver/src/solve/trait_goals.rs b/compiler/rustc_next_trait_solver/src/solve/trait_goals.rs
index 096dc32ccc926..cba3611779c90 100644
--- a/compiler/rustc_next_trait_solver/src/solve/trait_goals.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/trait_goals.rs
@@ -5,6 +5,7 @@ use rustc_type_ir::data_structures::IndexSet;
 use rustc_type_ir::fast_reject::DeepRejectCtxt;
 use rustc_type_ir::inherent::*;
 use rustc_type_ir::lang_items::TraitSolverLangItem;
+use rustc_type_ir::solve::CanonicalResponse;
 use rustc_type_ir::visit::TypeVisitableExt as _;
 use rustc_type_ir::{self as ty, Interner, TraitPredicate, TypingMode, Upcast as _, elaborate};
 use tracing::{instrument, trace};
@@ -69,7 +70,9 @@ where
             // it's not a real impl.
             (ty::ImplPolarity::Reservation, _) => match ecx.typing_mode() {
                 TypingMode::Coherence => Certainty::AMBIGUOUS,
-                TypingMode::Analysis { .. } | TypingMode::PostAnalysis => return Err(NoSolution),
+                TypingMode::Analysis { .. }
+                | TypingMode::PostBorrowckAnalysis { .. }
+                | TypingMode::PostAnalysis => return Err(NoSolution),
             },
 
             // Impl matches polarity
@@ -174,20 +177,7 @@ where
         // ideally we want to avoid, since we can make progress on this goal
         // via an alias bound or a locally-inferred hidden type instead.
         if let ty::Alias(ty::Opaque, opaque_ty) = goal.predicate.self_ty().kind() {
-            match ecx.typing_mode() {
-                TypingMode::Coherence | TypingMode::PostAnalysis => {
-                    unreachable!("rigid opaque outside of analysis: {goal:?}");
-                }
-                TypingMode::Analysis { defining_opaque_types } => {
-                    if opaque_ty
-                        .def_id
-                        .as_local()
-                        .is_some_and(|def_id| defining_opaque_types.contains(&def_id))
-                    {
-                        return Err(NoSolution);
-                    }
-                }
-            }
+            debug_assert!(ecx.opaque_type_is_rigid(opaque_ty.def_id));
         }
 
         ecx.probe_and_evaluate_goal_for_constituent_tys(
@@ -1150,13 +1140,86 @@ where
             ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
         })
     }
+}
+
+/// How we've proven this trait goal.
+#[derive(Debug, Clone, Copy)]
+pub(super) enum ProvenVia {
+    Impl,
+    ParamEnv,
+    AliasBound,
+}
+
+impl<D, I> EvalCtxt<'_, D>
+where
+    D: SolverDelegate<Interner = I>,
+    I: Interner,
+{
+    pub(super) fn merge_trait_candidates(
+        &mut self,
+        goal: Goal<I, TraitPredicate<I>>,
+        candidates: Vec<Candidate<I>>,
+    ) -> Result<(CanonicalResponse<I>, Option<ProvenVia>), NoSolution> {
+        if let TypingMode::Coherence = self.typing_mode() {
+            let all_candidates: Vec<_> = candidates.into_iter().map(|c| c.result).collect();
+            return if let Some(response) = self.try_merge_responses(&all_candidates) {
+                Ok((response, Some(ProvenVia::Impl)))
+            } else {
+                self.flounder(&all_candidates).map(|r| (r, None))
+            };
+        }
+        // FIXME: prefer trivial builtin impls
+
+        // If there are non-global where-bounds, prefer where-bounds
+        // (including global ones) over everything else.
+        let has_non_global_where_bounds = candidates.iter().any(|c| match c.source {
+            CandidateSource::ParamEnv(idx) => {
+                let where_bound = goal.param_env.caller_bounds().get(idx);
+                where_bound.has_bound_vars() || !where_bound.is_global()
+            }
+            _ => false,
+        });
+        if has_non_global_where_bounds {
+            let where_bounds: Vec<_> = candidates
+                .iter()
+                .filter(|c| matches!(c.source, CandidateSource::ParamEnv(_)))
+                .map(|c| c.result)
+                .collect();
+
+            return if let Some(response) = self.try_merge_responses(&where_bounds) {
+                Ok((response, Some(ProvenVia::ParamEnv)))
+            } else {
+                Ok((self.bail_with_ambiguity(&where_bounds), None))
+            };
+        }
+
+        if candidates.iter().any(|c| matches!(c.source, CandidateSource::AliasBound)) {
+            let alias_bounds: Vec<_> = candidates
+                .iter()
+                .filter(|c| matches!(c.source, CandidateSource::AliasBound))
+                .map(|c| c.result)
+                .collect();
+            return if let Some(response) = self.try_merge_responses(&alias_bounds) {
+                Ok((response, Some(ProvenVia::AliasBound)))
+            } else {
+                Ok((self.bail_with_ambiguity(&alias_bounds), None))
+            };
+        }
+
+        let all_candidates: Vec<_> = candidates.into_iter().map(|c| c.result).collect();
+        if let Some(response) = self.try_merge_responses(&all_candidates) {
+            Ok((response, Some(ProvenVia::Impl)))
+        } else {
+            self.flounder(&all_candidates).map(|r| (r, None))
+        }
+    }
 
     #[instrument(level = "trace", skip(self))]
     pub(super) fn compute_trait_goal(
         &mut self,
         goal: Goal<I, TraitPredicate<I>>,
-    ) -> QueryResult<I> {
+    ) -> Result<(CanonicalResponse<I>, Option<ProvenVia>), NoSolution> {
         let candidates = self.assemble_and_evaluate_candidates(goal);
-        self.merge_candidates(candidates)
+        self.merge_trait_candidates(goal, candidates)
     }
 }
diff --git a/compiler/rustc_session/src/config.rs b/compiler/rustc_session/src/config.rs
index 0124397ea46f3..19d657c203276 100644
--- a/compiler/rustc_session/src/config.rs
+++ b/compiler/rustc_session/src/config.rs
@@ -846,7 +846,7 @@ pub struct NextSolverConfig {
 }
 impl Default for NextSolverConfig {
     fn default() -> Self {
-        NextSolverConfig { coherence: true, globally: false }
+        NextSolverConfig { coherence: true, globally: true }
     }
 }
 
diff --git a/compiler/rustc_trait_selection/src/solve/delegate.rs b/compiler/rustc_trait_selection/src/solve/delegate.rs
index 09bba24ba6130..97cde67799c2c 100644
--- a/compiler/rustc_trait_selection/src/solve/delegate.rs
+++ b/compiler/rustc_trait_selection/src/solve/delegate.rs
@@ -205,7 +205,9 @@ impl<'tcx> rustc_next_trait_solver::delegate::SolverDelegate for SolverDelegate<
             // transmute checking and polymorphic MIR optimizations could
             // get a result which isn't correct for all monomorphizations.
             match self.typing_mode() {
-                TypingMode::Coherence | TypingMode::Analysis { .. } => false,
+                TypingMode::Coherence
+                | TypingMode::Analysis { .. }
+                | TypingMode::PostBorrowckAnalysis { .. } => false,
                 TypingMode::PostAnalysis => {
                     let poly_trait_ref = self.resolve_vars_if_possible(goal_trait_ref);
                     !poly_trait_ref.still_further_specializable()
diff --git a/compiler/rustc_trait_selection/src/traits/coherence.rs b/compiler/rustc_trait_selection/src/traits/coherence.rs
index a98871b2d60a4..af65a4741b739 100644
--- a/compiler/rustc_trait_selection/src/traits/coherence.rs
+++ b/compiler/rustc_trait_selection/src/traits/coherence.rs
@@ -98,7 +98,7 @@ pub fn overlapping_impls(
     // Before doing expensive operations like entering an inference context, do
     // a quick check via fast_reject to tell if the impl headers could possibly
     // unify.
-    let drcx = DeepRejectCtxt::relate_infer_infer(tcx);
+    let mut drcx = DeepRejectCtxt::relate_infer_infer(tcx);
     let impl1_ref = tcx.impl_trait_ref(impl1_def_id);
     let impl2_ref = tcx.impl_trait_ref(impl2_def_id);
     let may_overlap = match (impl1_ref, impl2_ref) {
diff --git a/compiler/rustc_trait_selection/src/traits/effects.rs b/compiler/rustc_trait_selection/src/traits/effects.rs
index 07fb2efb7fed3..e1f1cb27c3618 100644
--- a/compiler/rustc_trait_selection/src/traits/effects.rs
+++ b/compiler/rustc_trait_selection/src/traits/effects.rs
@@ -79,7 +79,7 @@ fn evaluate_host_effect_from_bounds<'tcx>(
     obligation: &HostEffectObligation<'tcx>,
 ) -> Result<ThinVec<PredicateObligation<'tcx>>, EvaluationFailure> {
     let infcx = selcx.infcx;
-    let drcx = DeepRejectCtxt::relate_rigid_rigid(selcx.tcx());
+    let mut drcx = DeepRejectCtxt::relate_rigid_rigid(selcx.tcx());
     let mut candidate = None;
 
     for predicate in obligation.param_env.caller_bounds() {
diff --git a/compiler/rustc_trait_selection/src/traits/normalize.rs b/compiler/rustc_trait_selection/src/traits/normalize.rs
index 4d3d8c66e62b0..91b37ded23b9f 100644
--- a/compiler/rustc_trait_selection/src/traits/normalize.rs
+++ b/compiler/rustc_trait_selection/src/traits/normalize.rs
@@ -66,7 +66,7 @@ impl<'tcx> At<'_, 'tcx> {
             let value = self
                 .normalize(value)
                 .into_value_registering_obligations(self.infcx, &mut *fulfill_cx);
-            let errors = fulfill_cx.select_where_possible(self.infcx);
+            let errors = fulfill_cx.select_all_or_error(self.infcx);
             let value = self.infcx.resolve_vars_if_possible(value);
             if errors.is_empty() { Ok(value) } else { Err(errors) }
         }
@@ -118,9 +118,10 @@ pub(super) fn needs_normalization<'tcx, T: TypeVisitable<TyCtxt<'tcx>>>(
     // Opaques are treated as rigid outside of `TypingMode::PostAnalysis`,
     // so we can ignore those.
     match infcx.typing_mode() {
-        TypingMode::Coherence | TypingMode::Analysis { defining_opaque_types: _ } => {
-            flags.remove(ty::TypeFlags::HAS_TY_OPAQUE)
-        }
+        // FIXME(#132279): We likely want to reveal opaques during post borrowck analysis
+        TypingMode::Coherence
+        | TypingMode::Analysis { defining_opaque_types: _ }
+        | TypingMode::PostBorrowckAnalysis { .. } => flags.remove(ty::TypeFlags::HAS_TY_OPAQUE),
         TypingMode::PostAnalysis => {}
     }
 
@@ -213,9 +214,10 @@ impl<'a, 'b, 'tcx> TypeFolder<TyCtxt<'tcx>> for AssocTypeNormalizer<'a, 'b, 'tcx
             ty::Opaque => {
                 // Only normalize `impl Trait` outside of type inference, usually in codegen.
                 match self.selcx.infcx.typing_mode() {
-                    TypingMode::Coherence | TypingMode::Analysis { defining_opaque_types: _ } => {
-                        ty.super_fold_with(self)
-                    }
+                    // FIXME(#132279): We likely want to reveal opaques during post borrowck analysis
+                    TypingMode::Coherence
+                    | TypingMode::Analysis { defining_opaque_types: _ }
+                    | TypingMode::PostBorrowckAnalysis { .. } => ty.super_fold_with(self),
                     TypingMode::PostAnalysis => {
                         let recursion_limit = self.cx().recursion_limit();
                         if !recursion_limit.value_within_limit(self.depth) {
diff --git a/compiler/rustc_trait_selection/src/traits/project.rs b/compiler/rustc_trait_selection/src/traits/project.rs
index 2864f277df578..56eaa9707af50 100644
--- a/compiler/rustc_trait_selection/src/traits/project.rs
+++ b/compiler/rustc_trait_selection/src/traits/project.rs
@@ -866,7 +866,7 @@ fn assemble_candidates_from_predicates<'cx, 'tcx>(
     potentially_unnormalized_candidates: bool,
 ) {
     let infcx = selcx.infcx;
-    let drcx = DeepRejectCtxt::relate_rigid_rigid(selcx.tcx());
+    let mut drcx = DeepRejectCtxt::relate_rigid_rigid(selcx.tcx());
     for predicate in env_predicates {
         let bound_predicate = predicate.kind();
         if let ty::ClauseKind::Projection(data) = predicate.kind().skip_binder() {
@@ -975,7 +975,9 @@ fn assemble_candidates_from_impls<'cx, 'tcx>(
                     // transmute checking and polymorphic MIR optimizations could
                     // get a result which isn't correct for all monomorphizations.
                     match selcx.infcx.typing_mode() {
-                        TypingMode::Coherence | TypingMode::Analysis { .. } => {
+                        TypingMode::Coherence
+                        | TypingMode::Analysis { .. }
+                        | TypingMode::PostBorrowckAnalysis { .. } => {
                             debug!(
                                 assoc_ty = ?selcx.tcx().def_path_str(node_item.item.def_id),
                                 ?obligation.predicate,
diff --git a/compiler/rustc_trait_selection/src/traits/query/normalize.rs b/compiler/rustc_trait_selection/src/traits/query/normalize.rs
index 22cfbb2c84032..525f4e618a070 100644
--- a/compiler/rustc_trait_selection/src/traits/query/normalize.rs
+++ b/compiler/rustc_trait_selection/src/traits/query/normalize.rs
@@ -216,9 +216,9 @@ impl<'a, 'tcx> FallibleTypeFolder<TyCtxt<'tcx>> for QueryNormalizer<'a, 'tcx> {
             ty::Opaque => {
                 // Only normalize `impl Trait` outside of type inference, usually in codegen.
                 match self.infcx.typing_mode() {
-                    TypingMode::Coherence | TypingMode::Analysis { defining_opaque_types: _ } => {
-                        ty.try_super_fold_with(self)?
-                    }
+                    TypingMode::Coherence
+                    | TypingMode::Analysis { defining_opaque_types: _ }
+                    | TypingMode::PostBorrowckAnalysis { .. } => ty.try_super_fold_with(self)?,
 
                     TypingMode::PostAnalysis => {
                         let args = data.args.try_fold_with(self)?;
diff --git a/compiler/rustc_trait_selection/src/traits/query/type_op/implied_outlives_bounds.rs b/compiler/rustc_trait_selection/src/traits/query/type_op/implied_outlives_bounds.rs
index c6e41e57f0cec..224a727147276 100644
--- a/compiler/rustc_trait_selection/src/traits/query/type_op/implied_outlives_bounds.rs
+++ b/compiler/rustc_trait_selection/src/traits/query/type_op/implied_outlives_bounds.rs
@@ -59,12 +59,13 @@ pub fn compute_implied_outlives_bounds_inner<'tcx>(
     param_env: ty::ParamEnv<'tcx>,
     ty: Ty<'tcx>,
 ) -> Result<Vec<OutlivesBound<'tcx>>, NoSolution> {
-    let normalize_op = |ty| {
-        let ty = ocx.normalize(&ObligationCause::dummy(), param_env, ty);
+    let normalize_op = |ty| -> Result<_, NoSolution> {
+        let ty = ocx
+            .deeply_normalize(&ObligationCause::dummy(), param_env, ty)
+            .map_err(|_| NoSolution)?;
         if !ocx.select_all_or_error().is_empty() {
             return Err(NoSolution);
         }
-        let ty = ocx.infcx.resolve_vars_if_possible(ty);
         let ty = OpportunisticRegionResolver::new(&ocx.infcx).fold_ty(ty);
         Ok(ty)
     };
diff --git a/compiler/rustc_trait_selection/src/traits/select/candidate_assembly.rs b/compiler/rustc_trait_selection/src/traits/select/candidate_assembly.rs
index 32b4567aba4f0..8503af4fbd219 100644
--- a/compiler/rustc_trait_selection/src/traits/select/candidate_assembly.rs
+++ b/compiler/rustc_trait_selection/src/traits/select/candidate_assembly.rs
@@ -232,7 +232,7 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {
             .filter(|p| p.def_id() == stack.obligation.predicate.def_id())
             .filter(|p| p.polarity() == stack.obligation.predicate.polarity());
 
-        let drcx = DeepRejectCtxt::relate_rigid_rigid(self.tcx());
+        let mut drcx = DeepRejectCtxt::relate_rigid_rigid(self.tcx());
         let obligation_args = stack.obligation.predicate.skip_binder().trait_ref.args;
         // Keep only those bounds which may apply, and propagate overflow if it occurs.
         for bound in bounds {
@@ -548,7 +548,7 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {
         obligation: &PolyTraitObligation<'tcx>,
         candidates: &mut SelectionCandidateSet<'tcx>,
     ) {
-        let drcx = DeepRejectCtxt::relate_rigid_infer(self.tcx());
+        let mut drcx = DeepRejectCtxt::relate_rigid_infer(self.tcx());
         let obligation_args = obligation.predicate.skip_binder().trait_ref.args;
         self.tcx().for_each_relevant_impl(
             obligation.predicate.def_id(),
diff --git a/compiler/rustc_trait_selection/src/traits/select/mod.rs b/compiler/rustc_trait_selection/src/traits/select/mod.rs
index 3b64a47181a6c..8e083da63be93 100644
--- a/compiler/rustc_trait_selection/src/traits/select/mod.rs
+++ b/compiler/rustc_trait_selection/src/traits/select/mod.rs
@@ -1470,7 +1470,9 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {
         let obligation = &stack.obligation;
         match self.infcx.typing_mode() {
             TypingMode::Coherence => {}
-            TypingMode::Analysis { .. } | TypingMode::PostAnalysis => return Ok(()),
+            TypingMode::Analysis { .. }
+            | TypingMode::PostBorrowckAnalysis { .. }
+            | TypingMode::PostAnalysis => return Ok(()),
         }
 
         debug!("is_knowable()");
@@ -1517,6 +1519,9 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {
             TypingMode::Analysis { defining_opaque_types } => {
                 defining_opaque_types.is_empty() || !pred.has_opaque_types()
             }
+            // The hidden types of `defined_opaque_types` is not local to the current
+            // inference context, so we can freely move this to the global cache.
+            TypingMode::PostBorrowckAnalysis { defined_opaque_types: _ } => true,
             // The global cache is only used if there are no opaque types in
             // the defining scope or we're outside of analysis.
             //
diff --git a/compiler/rustc_ty_utils/src/instance.rs b/compiler/rustc_ty_utils/src/instance.rs
index 8798772e398d7..1a98c85bee9fb 100644
--- a/compiler/rustc_ty_utils/src/instance.rs
+++ b/compiler/rustc_ty_utils/src/instance.rs
@@ -149,7 +149,8 @@ fn resolve_associated_item<'tcx>(
                 // get a result which isn't correct for all monomorphizations.
                 match typing_env.typing_mode {
                     ty::TypingMode::Coherence
-                    | ty::TypingMode::Analysis { defining_opaque_types: _ } => false,
+                    | ty::TypingMode::Analysis { .. }
+                    | ty::TypingMode::PostBorrowckAnalysis { .. } => false,
                     ty::TypingMode::PostAnalysis => !trait_ref.still_further_specializable(),
                 }
             };
diff --git a/compiler/rustc_type_ir/src/fast_reject.rs b/compiler/rustc_type_ir/src/fast_reject.rs
index 2c8e47bcbca2a..531c901876ef8 100644
--- a/compiler/rustc_type_ir/src/fast_reject.rs
+++ b/compiler/rustc_type_ir/src/fast_reject.rs
@@ -11,6 +11,7 @@ use rustc_data_structures::stable_hasher::{HashStable, StableHasher, ToStableHas
 #[cfg(feature = "nightly")]
 use rustc_macros::{HashStable_NoContext, TyDecodable, TyEncodable};
 
+use crate::data_structures::DelayedSet;
 use crate::inherent::*;
 use crate::visit::TypeVisitableExt as _;
 use crate::{self as ty, Interner};
@@ -181,33 +182,34 @@ impl<DefId> SimplifiedType<DefId> {
 /// We also use this function during coherence. For coherence the
 /// impls only have to overlap for some value, so we treat parameters
 /// on both sides like inference variables.
-#[derive(Debug, Clone, Copy)]
+#[derive(Debug)]
 pub struct DeepRejectCtxt<
     I: Interner,
     const INSTANTIATE_LHS_WITH_INFER: bool,
     const INSTANTIATE_RHS_WITH_INFER: bool,
 > {
     _interner: PhantomData<I>,
+    cache: DelayedSet<(I::Ty, I::Ty)>,
 }
 
 impl<I: Interner> DeepRejectCtxt<I, false, false> {
     /// Treat parameters in both the lhs and the rhs as rigid.
     pub fn relate_rigid_rigid(_interner: I) -> DeepRejectCtxt<I, false, false> {
-        DeepRejectCtxt { _interner: PhantomData }
+        DeepRejectCtxt { _interner: PhantomData, cache: Default::default() }
     }
 }
 
 impl<I: Interner> DeepRejectCtxt<I, true, true> {
     /// Treat parameters in both the lhs and the rhs as infer vars.
     pub fn relate_infer_infer(_interner: I) -> DeepRejectCtxt<I, true, true> {
-        DeepRejectCtxt { _interner: PhantomData }
+        DeepRejectCtxt { _interner: PhantomData, cache: Default::default() }
     }
 }
 
 impl<I: Interner> DeepRejectCtxt<I, false, true> {
     /// Treat parameters in the lhs as rigid, and in rhs as infer vars.
     pub fn relate_rigid_infer(_interner: I) -> DeepRejectCtxt<I, false, true> {
-        DeepRejectCtxt { _interner: PhantomData }
+        DeepRejectCtxt { _interner: PhantomData, cache: Default::default() }
     }
 }
 
@@ -215,7 +217,7 @@ impl<I: Interner, const INSTANTIATE_LHS_WITH_INFER: bool, const INSTANTIATE_RHS_
     DeepRejectCtxt<I, INSTANTIATE_LHS_WITH_INFER, INSTANTIATE_RHS_WITH_INFER>
 {
     pub fn args_may_unify(
-        self,
+        &mut self,
         obligation_args: I::GenericArgs,
         impl_args: I::GenericArgs,
     ) -> bool {
@@ -234,17 +236,32 @@ impl<I: Interner, const INSTANTIATE_LHS_WITH_INFER: bool, const INSTANTIATE_RHS_
         })
     }
 
-    pub fn types_may_unify(self, lhs: I::Ty, rhs: I::Ty) -> bool {
+    pub fn types_may_unify(&mut self, lhs: I::Ty, rhs: I::Ty) -> bool {
+        if self.cache.contains(&(lhs, rhs)) {
+            return true;
+        }
+
         match rhs.kind() {
             // Start by checking whether the `rhs` type may unify with
             // pretty much everything. Just return `true` in that case.
             ty::Param(_) => {
                 if INSTANTIATE_RHS_WITH_INFER {
+                    self.cache.insert((lhs, rhs));
+                    return true;
+                }
+            }
+            ty::Error(_) | ty::Alias(..) | ty::Bound(..) => {
+                self.cache.insert((lhs, rhs));
+                return true;
+            }
+            ty::Infer(var) => {
+                if self.var_and_ty_may_unify(var, lhs) {
+                    self.cache.insert((lhs, rhs));
                     return true;
+                } else {
+                    return false;
                 }
             }
-            ty::Error(_) | ty::Alias(..) | ty::Bound(..) => return true,
-            ty::Infer(var) => return self.var_and_ty_may_unify(var, lhs),
 
             // These types only unify with inference variables or their own
             // variant.
@@ -274,7 +291,7 @@ impl<I: Interner, const INSTANTIATE_LHS_WITH_INFER: bool, const INSTANTIATE_RHS_
         };
 
         // For purely rigid types, use structural equivalence.
-        match lhs.kind() {
+        let may_unify = match lhs.kind() {
             ty::Ref(_, lhs_ty, lhs_mutbl) => match rhs.kind() {
                 ty::Ref(_, rhs_ty, rhs_mutbl) => {
                     lhs_mutbl == rhs_mutbl && self.types_may_unify(lhs_ty, rhs_ty)
@@ -414,10 +431,16 @@ impl<I: Interner, const INSTANTIATE_LHS_WITH_INFER: bool, const INSTANTIATE_RHS_
             }
 
             ty::Error(..) => true,
+        };
+
+        if may_unify {
+            self.cache.insert((lhs, rhs));
         }
+
+        may_unify
     }
 
-    pub fn consts_may_unify(self, lhs: I::Const, rhs: I::Const) -> bool {
+    pub fn consts_may_unify(&mut self, lhs: I::Const, rhs: I::Const) -> bool {
         match rhs.kind() {
             ty::ConstKind::Param(_) => {
                 if INSTANTIATE_RHS_WITH_INFER {
@@ -465,7 +488,7 @@ impl<I: Interner, const INSTANTIATE_LHS_WITH_INFER: bool, const INSTANTIATE_RHS_
         }
     }
 
-    fn var_and_ty_may_unify(self, var: ty::InferTy, ty: I::Ty) -> bool {
+    fn var_and_ty_may_unify(&mut self, var: ty::InferTy, ty: I::Ty) -> bool {
         if !ty.is_known_rigid() {
             return true;
         }
diff --git a/compiler/rustc_type_ir/src/infer_ctxt.rs b/compiler/rustc_type_ir/src/infer_ctxt.rs
index 13ad505bc0483..a892b88c2c636 100644
--- a/compiler/rustc_type_ir/src/infer_ctxt.rs
+++ b/compiler/rustc_type_ir/src/infer_ctxt.rs
@@ -63,6 +63,12 @@ pub enum TypingMode<I: Interner> {
     /// }
     /// ```
     Analysis { defining_opaque_types: I::DefiningOpaqueTypes },
+    /// Any analysis after borrowck for a given body should be able to use all the
+    /// hidden types defined by borrowck, without being able to define any new ones.
+    ///
+    /// This is currently only used by the new solver, but should be implemented in
+    /// the old solver as well.
+    PostBorrowckAnalysis { defined_opaque_types: I::DefiningOpaqueTypes },
     /// After analysis, mostly during codegen and MIR optimizations, we're able to
     /// reveal all opaque types. As the concrete type should *never* be observable
     /// directly by the user, this should not be used by checks which may expose
@@ -85,6 +91,12 @@ impl<I: Interner> TypingMode<I> {
     pub fn analysis_in_body(cx: I, body_def_id: I::LocalDefId) -> TypingMode<I> {
         TypingMode::Analysis { defining_opaque_types: cx.opaque_types_defined_by(body_def_id) }
     }
+
+    pub fn post_borrowck_analysis(cx: I, body_def_id: I::LocalDefId) -> TypingMode<I> {
+        TypingMode::PostBorrowckAnalysis {
+            defined_opaque_types: cx.opaque_types_defined_by(body_def_id),
+        }
+    }
 }
 
 pub trait InferCtxtLike: Sized {
@@ -126,6 +138,7 @@ pub trait InferCtxtLike: Sized {
         vid: ty::RegionVid,
     ) -> <Self::Interner as Interner>::Region;
 
+    fn next_region_infer(&self) -> <Self::Interner as Interner>::Region;
     fn next_ty_infer(&self) -> <Self::Interner as Interner>::Ty;
     fn next_const_infer(&self) -> <Self::Interner as Interner>::Const;
     fn fresh_args_for_item(
diff --git a/compiler/rustc_type_ir/src/inherent.rs b/compiler/rustc_type_ir/src/inherent.rs
index a201f2b1c11f1..2028f2a28aab8 100644
--- a/compiler/rustc_type_ir/src/inherent.rs
+++ b/compiler/rustc_type_ir/src/inherent.rs
@@ -540,7 +540,7 @@ pub trait AdtDef<I: Interner>: Copy + Debug + Hash + Eq {
 }
 
 pub trait ParamEnv<I: Interner>: Copy + Debug + Hash + Eq + TypeFoldable<I> {
-    fn caller_bounds(self) -> impl IntoIterator<Item = I::Clause>;
+    fn caller_bounds(self) -> impl SliceLike<Item = I::Clause>;
 }
 
 pub trait Features<I: Interner>: Copy {
diff --git a/compiler/rustc_type_ir/src/interner.rs b/compiler/rustc_type_ir/src/interner.rs
index 0ae688848ebfc..1be93115d70e1 100644
--- a/compiler/rustc_type_ir/src/interner.rs
+++ b/compiler/rustc_type_ir/src/interner.rs
@@ -297,6 +297,12 @@ pub trait Interner:
         self,
         defining_anchor: Self::LocalDefId,
     ) -> Self::DefiningOpaqueTypes;
+
+    fn fold_regions<T: TypeFoldable<Self>>(
+        self,
+        value: T,
+        f: impl FnMut(Self::Region, ty::DebruijnIndex) -> Self::Region,
+    ) -> T;
 }
 
 /// Imagine you have a function `F: FnOnce(&[T]) -> R`, plus an iterator `iter`
diff --git a/compiler/rustc_type_ir/src/relate/combine.rs b/compiler/rustc_type_ir/src/relate/combine.rs
index c8abfee314e23..d49f8d3093db7 100644
--- a/compiler/rustc_type_ir/src/relate/combine.rs
+++ b/compiler/rustc_type_ir/src/relate/combine.rs
@@ -136,9 +136,9 @@ where
                     relation.register_predicates([ty::Binder::dummy(ty::PredicateKind::Ambiguous)]);
                     Ok(a)
                 }
-                TypingMode::Analysis { .. } | TypingMode::PostAnalysis => {
-                    structurally_relate_tys(relation, a, b)
-                }
+                TypingMode::Analysis { .. }
+                | TypingMode::PostBorrowckAnalysis { .. }
+                | TypingMode::PostAnalysis => structurally_relate_tys(relation, a, b),
             }
         }
 
diff --git a/src/librustdoc/html/render/write_shared.rs b/src/librustdoc/html/render/write_shared.rs
index c82f7e9aaf927..a178fcd3c276b 100644
--- a/src/librustdoc/html/render/write_shared.rs
+++ b/src/librustdoc/html/render/write_shared.rs
@@ -918,7 +918,7 @@ impl<'cx, 'cache, 'item> DocVisitor<'item> for TypeImplCollector<'cx, 'cache, 'i
             // Be aware of `tests/rustdoc/type-alias/deeply-nested-112515.rs` which might regress.
             let Some(impl_did) = impl_item_id.as_def_id() else { continue };
             let for_ty = self.cx.tcx().type_of(impl_did).skip_binder();
-            let reject_cx = DeepRejectCtxt::relate_infer_infer(self.cx.tcx());
+            let mut reject_cx = DeepRejectCtxt::relate_infer_infer(self.cx.tcx());
             if !reject_cx.types_may_unify(aliased_ty, for_ty) {
                 continue;
             }
diff --git a/tests/ui/higher-ranked/trait-bounds/normalize-under-binder/norm-before-method-resolution-opaque-type.next.stderr b/tests/ui/higher-ranked/trait-bounds/normalize-under-binder/norm-before-method-resolution-opaque-type.next.stderr
deleted file mode 100644
index 72646b7bc768b..0000000000000
--- a/tests/ui/higher-ranked/trait-bounds/normalize-under-binder/norm-before-method-resolution-opaque-type.next.stderr
+++ /dev/null
@@ -1,9 +0,0 @@
-error[E0284]: type annotations needed: cannot satisfy `Foo == _`
-  --> $DIR/norm-before-method-resolution-opaque-type.rs:16:19
-   |
-LL | fn weird_bound<X>(x: &<X as Trait<'static>>::Out<Foo>) -> X
-   |                   ^ cannot satisfy `Foo == _`
-
-error: aborting due to 1 previous error
-
-For more information about this error, try `rustc --explain E0284`.
diff --git a/tests/ui/higher-ranked/trait-bounds/normalize-under-binder/norm-before-method-resolution-opaque-type.old.stderr b/tests/ui/higher-ranked/trait-bounds/normalize-under-binder/norm-before-method-resolution-opaque-type.old.stderr
index dbd0d5dc73323..52a300a7b8600 100644
--- a/tests/ui/higher-ranked/trait-bounds/normalize-under-binder/norm-before-method-resolution-opaque-type.old.stderr
+++ b/tests/ui/higher-ranked/trait-bounds/normalize-under-binder/norm-before-method-resolution-opaque-type.old.stderr
@@ -1,18 +1,18 @@
 error: item does not constrain `Foo::{opaque#0}`, but has it in its signature
-  --> $DIR/norm-before-method-resolution-opaque-type.rs:16:4
+  --> $DIR/norm-before-method-resolution-opaque-type.rs:17:4
    |
 LL | fn weird_bound<X>(x: &<X as Trait<'static>>::Out<Foo>) -> X
    |    ^^^^^^^^^^^
    |
    = note: consider moving the opaque type's declaration and defining uses into a separate module
 note: this opaque type is in the signature
-  --> $DIR/norm-before-method-resolution-opaque-type.rs:13:12
+  --> $DIR/norm-before-method-resolution-opaque-type.rs:14:12
    |
 LL | type Foo = impl Sized;
    |            ^^^^^^^^^^
 
 error: unconstrained opaque type
-  --> $DIR/norm-before-method-resolution-opaque-type.rs:13:12
+  --> $DIR/norm-before-method-resolution-opaque-type.rs:14:12
    |
 LL | type Foo = impl Sized;
    |            ^^^^^^^^^^
diff --git a/tests/ui/higher-ranked/trait-bounds/normalize-under-binder/norm-before-method-resolution-opaque-type.rs b/tests/ui/higher-ranked/trait-bounds/normalize-under-binder/norm-before-method-resolution-opaque-type.rs
index cf752f814c90c..4d7555b9d1265 100644
--- a/tests/ui/higher-ranked/trait-bounds/normalize-under-binder/norm-before-method-resolution-opaque-type.rs
+++ b/tests/ui/higher-ranked/trait-bounds/normalize-under-binder/norm-before-method-resolution-opaque-type.rs
@@ -1,5 +1,6 @@
 //@ revisions: old next
 //@[next] compile-flags: -Znext-solver
+//@[next] check-pass
 
 #![feature(type_alias_impl_trait)]
 trait Trait<'a> {
@@ -15,7 +16,6 @@ type Foo = impl Sized;
 
 fn weird_bound<X>(x: &<X as Trait<'static>>::Out<Foo>) -> X
 //[old]~^ ERROR: item does not constrain
-//[next]~^^ ERROR: cannot satisfy `Foo == _`
 where
     for<'a> X: Trait<'a>,
     for<'a> <X as Trait<'a>>::Out<()>: Copy,
diff --git a/tests/ui/traits/next-solver/non-wf-ret.rs b/tests/ui/traits/next-solver/non-wf-ret.rs
new file mode 100644
index 0000000000000..626f82c811c28
--- /dev/null
+++ b/tests/ui/traits/next-solver/non-wf-ret.rs
@@ -0,0 +1,54 @@
+//@ check-pass
+//@ compile-flags: -Znext-solver
+
+#![feature(extern_types)]
+
+use std::ops::Deref;
+
+extern "C" {
+    type OpaqueListContents;
+}
+
+pub struct List<T> {
+    skel: [T; 0],
+    opaque: OpaqueListContents,
+}
+
+impl<'a, T: Copy> IntoIterator for &'a List<T> {
+    type Item = T;
+    type IntoIter = std::iter::Copied<<&'a [T] as IntoIterator>::IntoIter>;
+
+    fn into_iter(self) -> Self::IntoIter {
+        todo!()
+    }
+}
+
+impl<T> Deref for List<T> {
+    type Target = [T];
+
+    fn deref(&self) -> &[T] {
+        todo!()
+    }
+}
+
+impl<T> List<T> {
+    fn iter(&self) -> <&Self as IntoIterator>::IntoIter
+    where
+        T: Copy,
+    {
+        todo!()
+    }
+}
+
+fn test<Q>(t: &List<Q>) {
+    // Checking that `<&List<Q> as IntoIterator>::IntoIter` is WF
+    // will disqualify the inherent method, since normalizing it
+    // requires `Q: Copy` which does not hold. and allow us to fall
+    // through to the deref'd `<[Q]>::iter` method which works.
+    //
+    // In the old solver, the same behavior is achieved by just
+    // eagerly normalizing the return type.
+    t.iter();
+}
+
+fn main() {}
diff --git a/tests/ui/traits/next-solver/normalize-in-implied_outlives_bounds.rs b/tests/ui/traits/next-solver/normalize-in-implied_outlives_bounds.rs
new file mode 100644
index 0000000000000..1dca19d28e9ac
--- /dev/null
+++ b/tests/ui/traits/next-solver/normalize-in-implied_outlives_bounds.rs
@@ -0,0 +1,46 @@
+//@ check-pass
+//@ compile-flags: -Znext-solver
+
+// Minimized example from `rustc_type_ir` that demonstrates a missing deep normalization
+// in the new solver when computing the implies outlives bounds of an impl.
+
+use std::marker::PhantomData;
+use std::ops::Deref;
+
+pub struct SearchGraph<D: Delegate, X = <D as Delegate>::Cx> {
+    d: PhantomData<D>,
+    x: PhantomData<X>,
+}
+
+pub trait Delegate {
+    type Cx;
+}
+
+struct SearchGraphDelegate<D: SolverDelegate> {
+    _marker: PhantomData<D>,
+}
+
+impl<D> Delegate for SearchGraphDelegate<D>
+where
+    D: SolverDelegate,
+{
+    type Cx = D::Interner;
+}
+
+pub trait SolverDelegate {
+    type Interner;
+}
+
+struct EvalCtxt<'a, D, I>
+where
+    D: SolverDelegate<Interner = I>,
+{
+    search_graph: &'a SearchGraph<SearchGraphDelegate<D>>,
+}
+
+impl<'a, D, I> EvalCtxt<'a, D, <D as SolverDelegate>::Interner>
+where
+    D: SolverDelegate<Interner = I>
+{}
+
+fn main() {}
diff --git a/tests/ui/traits/next-solver/dont-remap-tait-substs.rs b/tests/ui/traits/next-solver/opaques/dont-remap-tait-substs.rs
similarity index 100%
rename from tests/ui/traits/next-solver/dont-remap-tait-substs.rs
rename to tests/ui/traits/next-solver/opaques/dont-remap-tait-substs.rs
diff --git a/tests/ui/traits/next-solver/dont-type_of-tait-in-defining-scope.is_send.stderr b/tests/ui/traits/next-solver/opaques/dont-type_of-tait-in-defining-scope.is_send.stderr
similarity index 100%
rename from tests/ui/traits/next-solver/dont-type_of-tait-in-defining-scope.is_send.stderr
rename to tests/ui/traits/next-solver/opaques/dont-type_of-tait-in-defining-scope.is_send.stderr
diff --git a/tests/ui/traits/next-solver/dont-type_of-tait-in-defining-scope.not_send.stderr b/tests/ui/traits/next-solver/opaques/dont-type_of-tait-in-defining-scope.not_send.stderr
similarity index 100%
rename from tests/ui/traits/next-solver/dont-type_of-tait-in-defining-scope.not_send.stderr
rename to tests/ui/traits/next-solver/opaques/dont-type_of-tait-in-defining-scope.not_send.stderr
diff --git a/tests/ui/traits/next-solver/dont-type_of-tait-in-defining-scope.rs b/tests/ui/traits/next-solver/opaques/dont-type_of-tait-in-defining-scope.rs
similarity index 100%
rename from tests/ui/traits/next-solver/dont-type_of-tait-in-defining-scope.rs
rename to tests/ui/traits/next-solver/opaques/dont-type_of-tait-in-defining-scope.rs
diff --git a/tests/ui/traits/next-solver/opaques/no-define-in-wf-check.current.stderr b/tests/ui/traits/next-solver/opaques/no-define-in-wf-check.current.stderr
new file mode 100644
index 0000000000000..9a28dc093c1be
--- /dev/null
+++ b/tests/ui/traits/next-solver/opaques/no-define-in-wf-check.current.stderr
@@ -0,0 +1,34 @@
+error: unconstrained opaque type
+  --> $DIR/no-define-in-wf-check.rs:19:18
+   |
+LL |     type Tait1 = impl Sized;
+   |                  ^^^^^^^^^^
+   |
+   = note: `Tait1` must be used in combination with a concrete type within the same module
+
+error: unconstrained opaque type
+  --> $DIR/no-define-in-wf-check.rs:27:18
+   |
+LL |     type Tait1 = impl Sized;
+   |                  ^^^^^^^^^^
+   |
+   = note: `Tait1` must be used in combination with a concrete type within the same module
+
+error: unconstrained opaque type
+  --> $DIR/no-define-in-wf-check.rs:36:18
+   |
+LL |     type Tait1 = impl Sized;
+   |                  ^^^^^^^^^^
+   |
+   = note: `Tait1` must be used in combination with a concrete type within the same module
+
+error: unconstrained opaque type
+  --> $DIR/no-define-in-wf-check.rs:47:18
+   |
+LL |     type Tait1 = impl Sized;
+   |                  ^^^^^^^^^^
+   |
+   = note: `Tait1` must be used in combination with a concrete type within the same module
+
+error: aborting due to 4 previous errors
+
diff --git a/tests/ui/traits/next-solver/opaques/no-define-in-wf-check.rs b/tests/ui/traits/next-solver/opaques/no-define-in-wf-check.rs
new file mode 100644
index 0000000000000..dd6df097da1bb
--- /dev/null
+++ b/tests/ui/traits/next-solver/opaques/no-define-in-wf-check.rs
@@ -0,0 +1,66 @@
+//@ revisions: current next
+//@ ignore-compare-mode-next-solver (explicit revisions)
+//@[next] compile-flags: -Znext-solver
+//@[next] check-pass
+
+// Regression test for trait-system-refactor-initiative#106. We previously
+// tried to define other opaques while checking that opaques are well-formed.
+//
+// This resulted in undesirable ambiguity
+
+#![feature(type_alias_impl_trait)]
+
+mod ex0 {
+    fn foo() -> (impl Sized, impl Sized) {
+        ((), ())
+    }
+}
+mod ex1 {
+    type Tait1 = impl Sized;
+    //[current]~^ ERROR unconstrained opaque type
+    fn foo(x: Tait1) -> impl Sized {
+        let () = x;
+    }
+}
+
+mod ex2 {
+    type Tait1 = impl Sized;
+    //[current]~^ ERROR unconstrained opaque type
+    type Tait2 = impl Sized;
+    fn foo(x: Tait1) -> Tait2 {
+        let () = x;
+    }
+}
+
+mod ex3 {
+    type Tait1 = impl Sized;
+    //[current]~^ ERROR unconstrained opaque type
+    trait Something<T> {}
+    impl<T, U> Something<U> for T {}
+    type Tait2 = impl Something<Tait1>;
+    fn foo(x: Tait1) -> Tait2 {
+        let () = x;
+    }
+}
+
+mod ex4 {
+    type Tait1 = impl Sized;
+    //[current]~^ ERROR unconstrained opaque type
+    trait Trait<U> {
+        type Assoc;
+    }
+
+    impl<T, U> Trait<U> for T {
+        type Assoc = T;
+    }
+
+    // ambiguity when checking that `Tait2` is wf
+    //
+    // ambiguity proving `(): Trait<Tait1>`.
+    type Tait2 = impl Trait<(), Assoc = impl Trait<Tait1>>;
+    fn foo(x: Tait1) -> Tait2 {
+        let () = x;
+    }
+}
+
+fn main() {}
diff --git a/tests/ui/traits/next-solver/select-alias-bound-as-param.rs b/tests/ui/traits/next-solver/opaques/select-alias-bound-as-param.rs
similarity index 100%
rename from tests/ui/traits/next-solver/select-alias-bound-as-param.rs
rename to tests/ui/traits/next-solver/opaques/select-alias-bound-as-param.rs
diff --git a/tests/ui/traits/next-solver/structurally-normalize-in-borrowck-field-projection.rs b/tests/ui/traits/next-solver/structurally-normalize-in-borrowck-field-projection.rs
new file mode 100644
index 0000000000000..c72bb8a04fcdc
--- /dev/null
+++ b/tests/ui/traits/next-solver/structurally-normalize-in-borrowck-field-projection.rs
@@ -0,0 +1,32 @@
+//@ check-pass
+//@ compile-flags: -Znext-solver
+
+trait Interner: Sized {
+    type Value;
+}
+
+enum Kind<I: Interner> {
+    Value(I::Value),
+}
+
+struct Intern;
+
+impl Interner for Intern {
+    type Value = Wrap<u32>;
+}
+
+struct Wrap<T>(T);
+
+type KindAlias = Kind<Intern>;
+
+pub trait PrettyPrinter: Sized {
+    fn hello(c: KindAlias) {
+        match c {
+            KindAlias::Value(Wrap(v)) => {
+                println!("{v:?}");
+            }
+        }
+    }
+}
+
+fn main() {}
diff --git a/tests/ui/traits/next-solver/typeck/resolve-before-checking-builtin-ptr.rs b/tests/ui/traits/next-solver/typeck/resolve-before-checking-builtin-ptr.rs
new file mode 100644
index 0000000000000..d47f705a8ab6d
--- /dev/null
+++ b/tests/ui/traits/next-solver/typeck/resolve-before-checking-builtin-ptr.rs
@@ -0,0 +1,20 @@
+//@ check-pass
+//@ compile-flags: -Znext-solver
+
+trait Mirror {
+    type Assoc;
+}
+impl<T> Mirror for T {
+    type Assoc = T;
+}
+
+struct Place {
+    field: <&'static [u8] as Mirror>::Assoc,
+}
+
+fn main() {
+    let local = Place { field: &[] };
+    let z = || {
+        let y = &local.field[0];
+    };
+}
diff --git a/tests/ui/traits/next-solver/typeck/resolve-before-checking-never.rs b/tests/ui/traits/next-solver/typeck/resolve-before-checking-never.rs
new file mode 100644
index 0000000000000..6df1fd5d4ba16
--- /dev/null
+++ b/tests/ui/traits/next-solver/typeck/resolve-before-checking-never.rs
@@ -0,0 +1,20 @@
+//@ check-pass
+//@ compile-flags: -Znext-solver
+
+#![feature(never_type)]
+
+trait Mirror {
+    type Assoc;
+}
+impl<T> Mirror for T {
+    type Assoc = T;
+}
+
+fn diverge() -> <! as Mirror>::Assoc { todo!() }
+
+fn main() {
+    let close = || {
+        diverge();
+    };
+    let x: u32 = close();
+}