diff --git a/compiler/rustc_middle/src/ty/mod.rs b/compiler/rustc_middle/src/ty/mod.rs
index 25d0d7b71da6f..830ae7dd00a6a 100644
--- a/compiler/rustc_middle/src/ty/mod.rs
+++ b/compiler/rustc_middle/src/ty/mod.rs
@@ -971,7 +971,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 inherent::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/assembly/mod.rs b/compiler/rustc_next_trait_solver/src/solve/assembly/mod.rs
index 198ccb000f345..02f6439b77fb7 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::TraitGoalProvenVia;
 use crate::delegate::SolverDelegate;
 use crate::solve::inspect::ProbeKind;
 use crate::solve::{
@@ -337,15 +338,6 @@ where
 
         self.assemble_param_env_candidates(goal, &mut candidates);
 
-        match self.typing_mode() {
-            TypingMode::Coherence => {}
-            TypingMode::Analysis { .. }
-            | TypingMode::PostBorrowckAnalysis { .. }
-            | TypingMode::PostAnalysis => {
-                self.discard_impls_shadowed_by_env(goal, &mut candidates);
-            }
-        }
-
         candidates
     }
 
@@ -500,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),
@@ -733,72 +725,64 @@ 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.
+    /// We sadly can't simply take all possible candidates for normalization goals
+    /// and check whether they result in the same constraints. We want to make sure
+    /// that trying to normalize an alias doesn't result in constraints which aren't
+    /// otherwise required.
+    ///
+    /// Most notably, when proving a trait goal by via a where-bound, we should not
+    /// normalize via impls which have stricter region constraints than the where-bound:
+    ///
+    /// ```rust
+    /// trait Trait<'a> {
+    ///     type Assoc;
+    /// }
+    ///
+    /// impl<'a, T: 'a> Trait<'a> for T {
+    ///     type Assoc = u32;
+    /// }
+    ///
+    /// fn with_bound<'a, T: Trait<'a>>(_value: T::Assoc) {}
+    /// ```
     ///
-    ///  <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>>(
+    /// The where-bound of `with_bound` doesn't specify the associated type, so we would
+    /// only be able to normalize `<T as Trait<'a>>::Assoc` by using the impl. This impl
+    /// adds a `T: 'a` bound however, which would result in a region error. Given that the
+    /// user explicitly wrote that `T: Trait<'a>` holds, this is undesirable and we instead
+    /// treat the alias as rigid.
+    ///
+    /// See trait-system-refactor-initiative#124 for more details.
+    #[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<TraitGoalProvenVia>,
+        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
+            TraitGoalProvenVia::ParamEnv | TraitGoalProvenVia::AliasBound => candidates
+                .iter()
+                .filter(|c| {
+                    matches!(c.source, CandidateSource::AliasBound | CandidateSource::ParamEnv(_))
+                })
+                .map(|c| c.result)
+                .collect(),
+            TraitGoalProvenVia::Misc => 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 70ceb22bfea58..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 })
diff --git a/compiler/rustc_next_trait_solver/src/solve/mod.rs b/compiler/rustc_next_trait_solver/src/solve/mod.rs
index ebf1013db1ecb..37678bfd8805f 100644
--- a/compiler/rustc_next_trait_solver/src/solve/mod.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/mod.rs
@@ -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.
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 63dbee2640bff..b886719222510 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
@@ -88,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/trait_goals.rs b/compiler/rustc_next_trait_solver/src/solve/trait_goals.rs
index 12df35d30b8f3..886cdec034552 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};
@@ -1147,13 +1148,101 @@ where
             ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
         })
     }
+}
+
+/// How we've proven this trait goal.
+///
+/// This is used by `NormalizesTo` goals to only normalize
+/// by using the same 'kind of candidate' we've used to prove
+/// its corresponding trait goal. Most notably, we do not
+/// normalize by using an impl if the trait goal has been
+/// proven via a `ParamEnv` candidate.
+///
+/// This is necessary to avoid unnecessary region constraints,
+/// see trait-system-refactor-initiative#125 for more details.
+#[derive(Debug, Clone, Copy)]
+pub(super) enum TraitGoalProvenVia {
+    /// We've proven the trait goal by something which is
+    /// is not a non-global where-bound or an alias-bound.
+    ///
+    /// This means we don't disable any candidates during
+    /// normalization.
+    Misc,
+    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<TraitGoalProvenVia>), 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(TraitGoalProvenVia::Misc)))
+            } 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(TraitGoalProvenVia::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(TraitGoalProvenVia::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(TraitGoalProvenVia::Misc)))
+        } 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<TraitGoalProvenVia>), NoSolution> {
         let candidates = self.assemble_and_evaluate_candidates(goal);
-        self.merge_candidates(candidates)
+        self.merge_trait_candidates(goal, candidates)
     }
 }
diff --git a/compiler/rustc_type_ir/src/inherent.rs b/compiler/rustc_type_ir/src/inherent.rs
index f45c94127bd00..2db40accda39b 100644
--- a/compiler/rustc_type_ir/src/inherent.rs
+++ b/compiler/rustc_type_ir/src/inherent.rs
@@ -543,7 +543,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/tests/crashes/133639.rs b/tests/crashes/133639.rs
deleted file mode 100644
index d522b0730cf86..0000000000000
--- a/tests/crashes/133639.rs
+++ /dev/null
@@ -1,33 +0,0 @@
-//@ known-bug: #133639
-
-#![feature(with_negative_coherence)]
-#![feature(min_specialization)]
-#![feature(generic_const_exprs)]
-
-#![crate_type = "lib"]
-use std::str::FromStr;
-
-struct a<const b: bool>;
-
-trait c {}
-
-impl<const d: u32> FromStr for e<d>
-where
-    a<{ d <= 2 }>: c,
-{
-    type Err = ();
-    fn from_str(f: &str) -> Result<Self, Self::Err> {
-        unimplemented!()
-    }
-}
-struct e<const d: u32>;
-
-impl<const d: u32> FromStr for e<d>
-where
-    a<{ d <= 2 }>: c,
-{
-    type Err = ();
-    fn from_str(f: &str) -> Result<Self, Self::Err> {
-        unimplemented!()
-    }
-}
diff --git a/tests/ui/const-generics/generic_const_exprs/specialization-fuzzing-ice-133639.rs b/tests/ui/const-generics/generic_const_exprs/specialization-fuzzing-ice-133639.rs
new file mode 100644
index 0000000000000..d3ae863bee968
--- /dev/null
+++ b/tests/ui/const-generics/generic_const_exprs/specialization-fuzzing-ice-133639.rs
@@ -0,0 +1,19 @@
+//@ check-pass
+
+// Regression test for #133639.
+
+#![feature(with_negative_coherence)]
+#![feature(min_specialization)]
+#![feature(generic_const_exprs)]
+//~^ WARNING the feature `generic_const_exprs` is incomplete
+
+#![crate_type = "lib"]
+trait Trait {}
+struct A<const B: bool>;
+
+trait C {}
+
+impl<const D: u32> Trait for E<D> where A<{ D <= 2 }>: C {}
+struct E<const D: u32>;
+
+impl<const D: u32> Trait for E<D> where A<{ D <= 2 }>: C {}
diff --git a/tests/ui/const-generics/generic_const_exprs/specialization-fuzzing-ice-133639.stderr b/tests/ui/const-generics/generic_const_exprs/specialization-fuzzing-ice-133639.stderr
new file mode 100644
index 0000000000000..f17b248d856d4
--- /dev/null
+++ b/tests/ui/const-generics/generic_const_exprs/specialization-fuzzing-ice-133639.stderr
@@ -0,0 +1,11 @@
+warning: the feature `generic_const_exprs` is incomplete and may not be safe to use and/or cause compiler crashes
+  --> $DIR/specialization-fuzzing-ice-133639.rs:7:12
+   |
+LL | #![feature(generic_const_exprs)]
+   |            ^^^^^^^^^^^^^^^^^^^
+   |
+   = note: see issue #76560 <https://github.com/rust-lang/rust/issues/76560> for more information
+   = note: `#[warn(incomplete_features)]` on by default
+
+warning: 1 warning emitted
+
diff --git a/tests/ui/const-generics/min_const_generics/param-env-eager-norm-dedup.rs b/tests/ui/const-generics/min_const_generics/param-env-eager-norm-dedup.rs
index 9600b3875ba48..2e97e3fe0044e 100644
--- a/tests/ui/const-generics/min_const_generics/param-env-eager-norm-dedup.rs
+++ b/tests/ui/const-generics/min_const_generics/param-env-eager-norm-dedup.rs
@@ -1,3 +1,6 @@
+//@ revisions: current next
+//@ ignore-compare-mode-next-solver (explicit revisions)
+//@[next] compile-flags: -Znext-solver
 //@ check-pass
 
 // This caused a regression in a crater run in #132325.
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 9e04e90a98ac0..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:15: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 479f59843557f..57cbe16911824 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,12 +1,12 @@
 error: item does not constrain `Foo::{opaque#0}`, but has it in its signature
-  --> $DIR/norm-before-method-resolution-opaque-type.rs:15:4
+  --> $DIR/norm-before-method-resolution-opaque-type.rs:16: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;
    |            ^^^^^^^^^^
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 ffbfc622bb012..43207d8927649 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> {
@@ -14,7 +15,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/generalize/occurs-check-nested-alias.rs b/tests/ui/traits/next-solver/generalize/occurs-check-nested-alias.rs
index 00dc7a9d337d9..fbf4cadc678d5 100644
--- a/tests/ui/traits/next-solver/generalize/occurs-check-nested-alias.rs
+++ b/tests/ui/traits/next-solver/generalize/occurs-check-nested-alias.rs
@@ -37,9 +37,4 @@ fn foo<T: Unnormalizable>() {
     // result in a cyclic type. However, we can still unify these types by first
     // normalizing the inner associated type. Emitting an error here would be incomplete.
     drop::<T>(t);
-
-    // FIXME(-Znext-solver): This line is necessary due to an unrelated solver bug
-    // and should get removed in the future.
-    //   https://github.com/rust-lang/trait-system-refactor-initiative/issues/96
-    drop::<Inv<<T as Unnormalizable>::Assoc>>(u);
 }
diff --git a/tests/ui/traits/winnowing/global-non-global-env-1.rs b/tests/ui/traits/winnowing/global-non-global-env-1.rs
index d232d32dddffd..75c184b65bf04 100644
--- a/tests/ui/traits/winnowing/global-non-global-env-1.rs
+++ b/tests/ui/traits/winnowing/global-non-global-env-1.rs
@@ -1,3 +1,6 @@
+//@ revisions: current next
+//@ ignore-compare-mode-next-solver (explicit revisions)
+//@[next] compile-flags: -Znext-solver
 //@ check-pass
 
 // A regression test for an edge case of candidate selection
diff --git a/tests/ui/traits/winnowing/global-non-global-env-2.rs b/tests/ui/traits/winnowing/global-non-global-env-2.rs
index c73d0f06cd95b..128ec2a40dab0 100644
--- a/tests/ui/traits/winnowing/global-non-global-env-2.rs
+++ b/tests/ui/traits/winnowing/global-non-global-env-2.rs
@@ -1,3 +1,6 @@
+//@ revisions: current next
+//@ ignore-compare-mode-next-solver (explicit revisions)
+//@[next] compile-flags: -Znext-solver
 //@ check-pass
 
 // A regression test for an edge case of candidate selection
diff --git a/tests/ui/traits/winnowing/global-non-global-env-3.rs b/tests/ui/traits/winnowing/global-non-global-env-3.rs
index 008d07e41446a..7e5dbd4ba8ec8 100644
--- a/tests/ui/traits/winnowing/global-non-global-env-3.rs
+++ b/tests/ui/traits/winnowing/global-non-global-env-3.rs
@@ -1,3 +1,6 @@
+//@ revisions: current next
+//@ ignore-compare-mode-next-solver (explicit revisions)
+//@[next] compile-flags: -Znext-solver
 //@ check-pass
 
 // A regression test for an edge case of candidate selection
diff --git a/tests/ui/traits/winnowing/global-non-global-env-4.rs b/tests/ui/traits/winnowing/global-non-global-env-4.rs
index 74793620c9e7d..2dc082be45c5e 100644
--- a/tests/ui/traits/winnowing/global-non-global-env-4.rs
+++ b/tests/ui/traits/winnowing/global-non-global-env-4.rs
@@ -1,3 +1,6 @@
+//@ revisions: current next
+//@ ignore-compare-mode-next-solver (explicit revisions)
+//@[next] compile-flags: -Znext-solver
 //@ check-pass
 
 // A regression test for an edge case of candidate selection