about summary refs log tree commit diff
diff options
context:
space:
mode:
-rw-r--r--compiler/rustc_borrowck/src/type_check/relate_tys.rs7
-rw-r--r--compiler/rustc_hir_typeck/src/coercion.rs26
-rw-r--r--compiler/rustc_hir_typeck/src/fn_ctxt/_impl.rs1
-rw-r--r--compiler/rustc_infer/src/infer/at.rs18
-rw-r--r--compiler/rustc_infer/src/infer/mod.rs1
-rw-r--r--compiler/rustc_infer/src/infer/relate/combine.rs58
-rw-r--r--compiler/rustc_infer/src/infer/relate/equate.rs13
-rw-r--r--compiler/rustc_infer/src/infer/relate/generalize.rs53
-rw-r--r--compiler/rustc_infer/src/infer/relate/glb.rs9
-rw-r--r--compiler/rustc_infer/src/infer/relate/lub.rs9
-rw-r--r--compiler/rustc_infer/src/infer/relate/mod.rs12
-rw-r--r--compiler/rustc_infer/src/infer/relate/sub.rs9
-rw-r--r--compiler/rustc_middle/src/traits/solve/inspect.rs2
-rw-r--r--compiler/rustc_middle/src/traits/solve/inspect/format.rs15
-rw-r--r--compiler/rustc_next_trait_solver/src/canonicalizer.rs38
-rw-r--r--compiler/rustc_trait_selection/src/solve/alias_relate.rs67
-rw-r--r--compiler/rustc_trait_selection/src/solve/assembly/mod.rs7
-rw-r--r--compiler/rustc_trait_selection/src/solve/eval_ctxt/canonical.rs74
-rw-r--r--compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs179
-rw-r--r--compiler/rustc_trait_selection/src/solve/eval_ctxt/select.rs59
-rw-r--r--compiler/rustc_trait_selection/src/solve/fulfill.rs25
-rw-r--r--compiler/rustc_trait_selection/src/solve/inspect/analyse.rs13
-rw-r--r--compiler/rustc_trait_selection/src/solve/inspect/build.rs14
-rw-r--r--compiler/rustc_trait_selection/src/solve/mod.rs1
-rw-r--r--compiler/rustc_trait_selection/src/solve/normalizes_to/mod.rs54
-rw-r--r--tests/ui/coherence/occurs-check/associated-type.next.stderr4
-rw-r--r--tests/ui/coherence/occurs-check/opaques.next.stderr6
-rw-r--r--tests/ui/impl-trait/auto-trait-coherence.next.stderr4
-rw-r--r--tests/ui/impl-trait/auto-trait-coherence.rs3
-rw-r--r--tests/ui/impl-trait/two_tait_defining_each_other2.current.stderr2
-rw-r--r--tests/ui/impl-trait/two_tait_defining_each_other2.next.stderr8
-rw-r--r--tests/ui/impl-trait/two_tait_defining_each_other2.rs2
-rw-r--r--tests/ui/traits/next-solver/assembly/candidates-equal-modulo-norm-1.rs26
-rw-r--r--tests/ui/traits/next-solver/assembly/candidates-equal-modulo-norm-2.rs26
-rw-r--r--tests/ui/traits/next-solver/coherence/trait_ref_is_knowable-norm-overflow.rs2
-rw-r--r--tests/ui/traits/next-solver/coherence/trait_ref_is_knowable-norm-overflow.stderr4
-rw-r--r--tests/ui/traits/next-solver/coherence/trait_ref_is_knowable-normalization-3.rs2
-rw-r--r--tests/ui/traits/next-solver/generalize/generalize-proj-new-universe-index-2.rs4
-rw-r--r--tests/ui/traits/next-solver/generalize/generalize-proj-new-universe-index-2.stderr19
-rw-r--r--tests/ui/traits/next-solver/generalize/instantiate-canonical-occurs-check-failure.rs29
-rw-r--r--tests/ui/traits/next-solver/generalize/occurs-check-nested-alias.next.stderr9
-rw-r--r--tests/ui/traits/next-solver/generalize/occurs-check-nested-alias.rs34
-rw-r--r--tests/ui/traits/next-solver/issue-118950-root-region.stderr4
43 files changed, 586 insertions, 366 deletions
diff --git a/compiler/rustc_borrowck/src/type_check/relate_tys.rs b/compiler/rustc_borrowck/src/type_check/relate_tys.rs
index 61b803ea38d..00296aa38da 100644
--- a/compiler/rustc_borrowck/src/type_check/relate_tys.rs
+++ b/compiler/rustc_borrowck/src/type_check/relate_tys.rs
@@ -1,7 +1,8 @@
 use rustc_data_structures::fx::FxHashMap;
 use rustc_errors::ErrorGuaranteed;
 use rustc_infer::infer::type_variable::{TypeVariableOrigin, TypeVariableOriginKind};
-use rustc_infer::infer::{NllRegionVariableOrigin, ObligationEmittingRelation};
+use rustc_infer::infer::NllRegionVariableOrigin;
+use rustc_infer::infer::{ObligationEmittingRelation, StructurallyRelateAliases};
 use rustc_infer::traits::{Obligation, PredicateObligations};
 use rustc_middle::mir::ConstraintCategory;
 use rustc_middle::traits::query::NoSolution;
@@ -548,6 +549,10 @@ impl<'bccx, 'tcx> ObligationEmittingRelation<'tcx> for NllTypeRelating<'_, 'bccx
         self.locations.span(self.type_checker.body)
     }
 
+    fn structurally_relate_aliases(&self) -> StructurallyRelateAliases {
+        StructurallyRelateAliases::No
+    }
+
     fn param_env(&self) -> ty::ParamEnv<'tcx> {
         self.type_checker.param_env
     }
diff --git a/compiler/rustc_hir_typeck/src/coercion.rs b/compiler/rustc_hir_typeck/src/coercion.rs
index 9f6175eac13..ba3000d8037 100644
--- a/compiler/rustc_hir_typeck/src/coercion.rs
+++ b/compiler/rustc_hir_typeck/src/coercion.rs
@@ -44,6 +44,8 @@ use rustc_hir::Expr;
 use rustc_hir_analysis::astconv::AstConv;
 use rustc_infer::infer::type_variable::{TypeVariableOrigin, TypeVariableOriginKind};
 use rustc_infer::infer::{Coercion, DefineOpaqueTypes, InferOk, InferResult};
+use rustc_infer::traits::TraitEngine;
+use rustc_infer::traits::TraitEngineExt as _;
 use rustc_infer::traits::{Obligation, PredicateObligation};
 use rustc_middle::lint::in_external_macro;
 use rustc_middle::traits::BuiltinImplSource;
@@ -61,6 +63,7 @@ use rustc_target::spec::abi::Abi;
 use rustc_trait_selection::infer::InferCtxtExt as _;
 use rustc_trait_selection::traits::error_reporting::TypeErrCtxtExt as _;
 use rustc_trait_selection::traits::query::evaluate_obligation::InferCtxtExt;
+use rustc_trait_selection::traits::TraitEngineExt as _;
 use rustc_trait_selection::traits::{
     self, NormalizeExt, ObligationCause, ObligationCauseCode, ObligationCtxt,
 };
@@ -157,17 +160,19 @@ impl<'f, 'tcx> Coerce<'f, 'tcx> {
             // In the new solver, lazy norm may allow us to shallowly equate
             // more types, but we emit possibly impossible-to-satisfy obligations.
             // Filter these cases out to make sure our coercion is more accurate.
-            if self.next_trait_solver() {
-                if let Ok(res) = &res {
-                    for obligation in &res.obligations {
-                        if !self.predicate_may_hold(obligation) {
-                            return Err(TypeError::Mismatch);
-                        }
+            match res {
+                Ok(InferOk { value, obligations }) if self.next_trait_solver() => {
+                    let mut fulfill_cx = <dyn TraitEngine<'tcx>>::new(self);
+                    fulfill_cx.register_predicate_obligations(self, obligations);
+                    let errs = fulfill_cx.select_where_possible(self);
+                    if errs.is_empty() {
+                        Ok(InferOk { value, obligations: fulfill_cx.pending_obligations() })
+                    } else {
+                        Err(TypeError::Mismatch)
                     }
                 }
+                res => res,
             }
-
-            res
         })
     }
 
@@ -625,19 +630,18 @@ impl<'f, 'tcx> Coerce<'f, 'tcx> {
         let traits = [coerce_unsized_did, unsize_did];
         while !queue.is_empty() {
             let obligation = queue.remove(0);
-            debug!("coerce_unsized resolve step: {:?}", obligation);
             let trait_pred = match obligation.predicate.kind().no_bound_vars() {
                 Some(ty::PredicateKind::Clause(ty::ClauseKind::Trait(trait_pred)))
                     if traits.contains(&trait_pred.def_id()) =>
                 {
-                    trait_pred
+                    self.resolve_vars_if_possible(trait_pred)
                 }
                 _ => {
                     coercion.obligations.push(obligation);
                     continue;
                 }
             };
-            let trait_pred = self.resolve_vars_if_possible(trait_pred);
+            debug!("coerce_unsized resolve step: {:?}", trait_pred);
             match selcx.select(&obligation.with(selcx.tcx(), trait_pred)) {
                 // Uncertain or unimplemented.
                 Ok(None) => {
diff --git a/compiler/rustc_hir_typeck/src/fn_ctxt/_impl.rs b/compiler/rustc_hir_typeck/src/fn_ctxt/_impl.rs
index 7d448820ceb..cc591fcf8c4 100644
--- a/compiler/rustc_hir_typeck/src/fn_ctxt/_impl.rs
+++ b/compiler/rustc_hir_typeck/src/fn_ctxt/_impl.rs
@@ -1516,6 +1516,7 @@ impl<'a, 'tcx> FnCtxt<'a, 'tcx> {
     /// In case there is still ambiguity, the returned type may be an inference
     /// variable. This is different from `structurally_resolve_type` which errors
     /// in this case.
+    #[instrument(level = "debug", skip(self, sp), ret)]
     pub fn try_structurally_resolve_type(&self, sp: Span, ty: Ty<'tcx>) -> Ty<'tcx> {
         let ty = self.resolve_vars_with_obligations(ty);
 
diff --git a/compiler/rustc_infer/src/infer/at.rs b/compiler/rustc_infer/src/infer/at.rs
index 05b9479c7b0..cc09a094688 100644
--- a/compiler/rustc_infer/src/infer/at.rs
+++ b/compiler/rustc_infer/src/infer/at.rs
@@ -302,7 +302,23 @@ impl<'a, 'tcx> Trace<'a, 'tcx> {
         let Trace { at, trace, a_is_expected } = self;
         let mut fields = at.infcx.combine_fields(trace, at.param_env, define_opaque_types);
         fields
-            .equate(a_is_expected)
+            .equate(StructurallyRelateAliases::No, a_is_expected)
+            .relate(a, b)
+            .map(move |_| InferOk { value: (), obligations: fields.obligations })
+    }
+
+    /// Equates `a` and `b` while structurally relating aliases. This should only
+    /// be used inside of the next generation trait solver when relating rigid aliases.
+    #[instrument(skip(self), level = "debug")]
+    pub fn eq_structurally_relating_aliases<T>(self, a: T, b: T) -> InferResult<'tcx, ()>
+    where
+        T: Relate<'tcx>,
+    {
+        let Trace { at, trace, a_is_expected } = self;
+        debug_assert!(at.infcx.next_trait_solver());
+        let mut fields = at.infcx.combine_fields(trace, at.param_env, DefineOpaqueTypes::No);
+        fields
+            .equate(StructurallyRelateAliases::Yes, a_is_expected)
             .relate(a, b)
             .map(move |_| InferOk { value: (), obligations: fields.obligations })
     }
diff --git a/compiler/rustc_infer/src/infer/mod.rs b/compiler/rustc_infer/src/infer/mod.rs
index c30f42c1656..89dbc36906d 100644
--- a/compiler/rustc_infer/src/infer/mod.rs
+++ b/compiler/rustc_infer/src/infer/mod.rs
@@ -54,6 +54,7 @@ use self::region_constraints::{
     RegionConstraintCollector, RegionConstraintStorage, RegionSnapshot,
 };
 pub use self::relate::combine::CombineFields;
+pub use self::relate::StructurallyRelateAliases;
 use self::type_variable::{TypeVariableOrigin, TypeVariableOriginKind};
 
 pub mod at;
diff --git a/compiler/rustc_infer/src/infer/relate/combine.rs b/compiler/rustc_infer/src/infer/relate/combine.rs
index f7690831c2a..0852bb4f993 100644
--- a/compiler/rustc_infer/src/infer/relate/combine.rs
+++ b/compiler/rustc_infer/src/infer/relate/combine.rs
@@ -26,6 +26,7 @@ use super::equate::Equate;
 use super::glb::Glb;
 use super::lub::Lub;
 use super::sub::Sub;
+use super::StructurallyRelateAliases;
 use crate::infer::{DefineOpaqueTypes, InferCtxt, TypeTrace};
 use crate::traits::{Obligation, PredicateObligations};
 use rustc_middle::infer::canonical::OriginalQueryValues;
@@ -116,8 +117,15 @@ impl<'tcx> InferCtxt<'tcx> {
             }
 
             (_, ty::Alias(..)) | (ty::Alias(..), _) if self.next_trait_solver() => {
-                relation.register_type_relate_obligation(a, b);
-                Ok(a)
+                match relation.structurally_relate_aliases() {
+                    StructurallyRelateAliases::Yes => {
+                        ty::relate::structurally_relate_tys(relation, a, b)
+                    }
+                    StructurallyRelateAliases::No => {
+                        relation.register_type_relate_obligation(a, b);
+                        Ok(a)
+                    }
+                }
             }
 
             // All other cases of inference are errors
@@ -240,19 +248,26 @@ impl<'tcx> InferCtxt<'tcx> {
             (ty::ConstKind::Unevaluated(..), _) | (_, ty::ConstKind::Unevaluated(..))
                 if self.tcx.features().generic_const_exprs || self.next_trait_solver() =>
             {
-                let (a, b) = if relation.a_is_expected() { (a, b) } else { (b, a) };
-
-                relation.register_predicates([if self.next_trait_solver() {
-                    ty::PredicateKind::AliasRelate(
-                        a.into(),
-                        b.into(),
-                        ty::AliasRelationDirection::Equate,
-                    )
-                } else {
-                    ty::PredicateKind::ConstEquate(a, b)
-                }]);
-
-                Ok(b)
+                match relation.structurally_relate_aliases() {
+                    StructurallyRelateAliases::No => {
+                        let (a, b) = if relation.a_is_expected() { (a, b) } else { (b, a) };
+
+                        relation.register_predicates([if self.next_trait_solver() {
+                            ty::PredicateKind::AliasRelate(
+                                a.into(),
+                                b.into(),
+                                ty::AliasRelationDirection::Equate,
+                            )
+                        } else {
+                            ty::PredicateKind::ConstEquate(a, b)
+                        }]);
+
+                        Ok(b)
+                    }
+                    StructurallyRelateAliases::Yes => {
+                        ty::relate::structurally_relate_consts(relation, a, b)
+                    }
+                }
             }
             _ => ty::relate::structurally_relate_consts(relation, a, b),
         }
@@ -303,8 +318,12 @@ impl<'infcx, 'tcx> CombineFields<'infcx, 'tcx> {
         self.infcx.tcx
     }
 
-    pub fn equate<'a>(&'a mut self, a_is_expected: bool) -> Equate<'a, 'infcx, 'tcx> {
-        Equate::new(self, a_is_expected)
+    pub fn equate<'a>(
+        &'a mut self,
+        structurally_relate_aliases: StructurallyRelateAliases,
+        a_is_expected: bool,
+    ) -> Equate<'a, 'infcx, 'tcx> {
+        Equate::new(self, structurally_relate_aliases, a_is_expected)
     }
 
     pub fn sub<'a>(&'a mut self, a_is_expected: bool) -> Sub<'a, 'infcx, 'tcx> {
@@ -335,6 +354,11 @@ pub trait ObligationEmittingRelation<'tcx>: TypeRelation<'tcx> {
 
     fn param_env(&self) -> ty::ParamEnv<'tcx>;
 
+    /// Whether aliases should be related structurally. This is pretty much
+    /// always `No` unless you're equating in some specific locations of the
+    /// new solver. See the comments in these use-cases for more details.
+    fn structurally_relate_aliases(&self) -> StructurallyRelateAliases;
+
     /// Register obligations that must hold in order for this relation to hold
     fn register_obligations(&mut self, obligations: PredicateObligations<'tcx>);
 
diff --git a/compiler/rustc_infer/src/infer/relate/equate.rs b/compiler/rustc_infer/src/infer/relate/equate.rs
index aefa9a5a0d6..43d6aef3e15 100644
--- a/compiler/rustc_infer/src/infer/relate/equate.rs
+++ b/compiler/rustc_infer/src/infer/relate/equate.rs
@@ -1,4 +1,5 @@
 use super::combine::{CombineFields, ObligationEmittingRelation};
+use super::StructurallyRelateAliases;
 use crate::infer::{DefineOpaqueTypes, SubregionOrigin};
 use crate::traits::PredicateObligations;
 
@@ -13,15 +14,17 @@ use rustc_span::Span;
 /// Ensures `a` is made equal to `b`. Returns `a` on success.
 pub struct Equate<'combine, 'infcx, 'tcx> {
     fields: &'combine mut CombineFields<'infcx, 'tcx>,
+    structurally_relate_aliases: StructurallyRelateAliases,
     a_is_expected: bool,
 }
 
 impl<'combine, 'infcx, 'tcx> Equate<'combine, 'infcx, 'tcx> {
     pub fn new(
         fields: &'combine mut CombineFields<'infcx, 'tcx>,
+        structurally_relate_aliases: StructurallyRelateAliases,
         a_is_expected: bool,
     ) -> Equate<'combine, 'infcx, 'tcx> {
-        Equate { fields, a_is_expected }
+        Equate { fields, structurally_relate_aliases, a_is_expected }
     }
 }
 
@@ -99,7 +102,7 @@ impl<'tcx> TypeRelation<'tcx> for Equate<'_, '_, 'tcx> {
                 &ty::Alias(ty::Opaque, ty::AliasTy { def_id: a_def_id, .. }),
                 &ty::Alias(ty::Opaque, ty::AliasTy { def_id: b_def_id, .. }),
             ) if a_def_id == b_def_id => {
-                self.fields.infcx.super_combine_tys(self, a, b)?;
+                infcx.super_combine_tys(self, a, b)?;
             }
             (&ty::Alias(ty::Opaque, ty::AliasTy { def_id, .. }), _)
             | (_, &ty::Alias(ty::Opaque, ty::AliasTy { def_id, .. }))
@@ -120,7 +123,7 @@ impl<'tcx> TypeRelation<'tcx> for Equate<'_, '_, 'tcx> {
                 );
             }
             _ => {
-                self.fields.infcx.super_combine_tys(self, a, b)?;
+                infcx.super_combine_tys(self, a, b)?;
             }
         }
 
@@ -180,6 +183,10 @@ impl<'tcx> ObligationEmittingRelation<'tcx> for Equate<'_, '_, 'tcx> {
         self.fields.trace.span()
     }
 
+    fn structurally_relate_aliases(&self) -> StructurallyRelateAliases {
+        self.structurally_relate_aliases
+    }
+
     fn param_env(&self) -> ty::ParamEnv<'tcx> {
         self.fields.param_env
     }
diff --git a/compiler/rustc_infer/src/infer/relate/generalize.rs b/compiler/rustc_infer/src/infer/relate/generalize.rs
index 2e1ea19078c..e84d4ceaea8 100644
--- a/compiler/rustc_infer/src/infer/relate/generalize.rs
+++ b/compiler/rustc_infer/src/infer/relate/generalize.rs
@@ -1,5 +1,6 @@
 use std::mem;
 
+use super::StructurallyRelateAliases;
 use crate::infer::type_variable::{TypeVariableOrigin, TypeVariableOriginKind, TypeVariableValue};
 use crate::infer::{InferCtxt, ObligationEmittingRelation, RegionVariableOrigin};
 use rustc_data_structures::sso::SsoHashMap;
@@ -45,8 +46,14 @@ impl<'tcx> InferCtxt<'tcx> {
         // region/type inference variables.
         //
         // We then relate `generalized_ty <: source_ty`,adding constraints like `'x: '?2` and `?1 <: ?3`.
-        let Generalization { value_may_be_infer: generalized_ty, has_unconstrained_ty_var } =
-            self.generalize(relation.span(), target_vid, instantiation_variance, source_ty)?;
+        let Generalization { value_may_be_infer: generalized_ty, has_unconstrained_ty_var } = self
+            .generalize(
+                relation.span(),
+                relation.structurally_relate_aliases(),
+                target_vid,
+                instantiation_variance,
+                source_ty,
+            )?;
 
         // Constrain `b_vid` to the generalized type `generalized_ty`.
         if let &ty::Infer(ty::TyVar(generalized_vid)) = generalized_ty.kind() {
@@ -178,8 +185,14 @@ impl<'tcx> InferCtxt<'tcx> {
     ) -> RelateResult<'tcx, ()> {
         // FIXME(generic_const_exprs): Occurs check failures for unevaluated
         // constants and generic expressions are not yet handled correctly.
-        let Generalization { value_may_be_infer: generalized_ct, has_unconstrained_ty_var } =
-            self.generalize(relation.span(), target_vid, ty::Variance::Invariant, source_ct)?;
+        let Generalization { value_may_be_infer: generalized_ct, has_unconstrained_ty_var } = self
+            .generalize(
+                relation.span(),
+                relation.structurally_relate_aliases(),
+                target_vid,
+                ty::Variance::Invariant,
+                source_ct,
+            )?;
 
         debug_assert!(!generalized_ct.is_ct_infer());
         if has_unconstrained_ty_var {
@@ -217,6 +230,7 @@ impl<'tcx> InferCtxt<'tcx> {
     fn generalize<T: Into<Term<'tcx>> + Relate<'tcx>>(
         &self,
         span: Span,
+        structurally_relate_aliases: StructurallyRelateAliases,
         target_vid: impl Into<ty::TermVid>,
         ambient_variance: ty::Variance,
         source_term: T,
@@ -237,6 +251,7 @@ impl<'tcx> InferCtxt<'tcx> {
         let mut generalizer = Generalizer {
             infcx: self,
             span,
+            structurally_relate_aliases,
             root_vid,
             for_universe,
             ambient_variance,
@@ -270,6 +285,10 @@ struct Generalizer<'me, 'tcx> {
 
     span: Span,
 
+    /// Whether aliases should be related structurally. If not, we have to
+    /// be careful when generalizing aliases.
+    structurally_relate_aliases: StructurallyRelateAliases,
+
     /// The vid of the type variable that is in the process of being
     /// instantiated. If we find this within the value we are folding,
     /// that means we would have created a cyclic value.
@@ -314,13 +333,30 @@ impl<'tcx> Generalizer<'_, 'tcx> {
     /// to normalize the alias after all.
     ///
     /// We handle this by lazily equating the alias and generalizing
-    /// it to an inference variable.
+    /// it to an inference variable. In the new solver, we always
+    /// generalize to an infer var unless the alias contains escaping
+    /// bound variables.
     ///
-    /// This is incomplete and will hopefully soon get fixed by #119106.
+    /// Correctly handling aliases with escaping bound variables is
+    /// difficult and currently incomplete in two opposite ways:
+    /// - if we get an occurs check failure in the alias, replace it with a new infer var.
+    ///   This causes us to later emit an alias-relate goal and is incomplete in case the
+    ///   alias normalizes to type containing one of the bound variables.
+    /// - if the alias contains an inference variable not nameable by `for_universe`, we
+    ///   continue generalizing the alias. This ends up pulling down the universe of the
+    ///   inference variable and is incomplete in case the alias would normalize to a type
+    ///   which does not mention that inference variable.
     fn generalize_alias_ty(
         &mut self,
         alias: ty::AliasTy<'tcx>,
     ) -> Result<Ty<'tcx>, TypeError<'tcx>> {
+        if self.infcx.next_trait_solver() && !alias.has_escaping_bound_vars() {
+            return Ok(self.infcx.next_ty_var_in_universe(
+                TypeVariableOrigin { kind: TypeVariableOriginKind::MiscVariable, span: self.span },
+                self.for_universe,
+            ));
+        }
+
         let is_nested_alias = mem::replace(&mut self.in_alias, true);
         let result = match self.relate(alias, alias) {
             Ok(alias) => Ok(alias.to_ty(self.tcx())),
@@ -490,7 +526,10 @@ impl<'tcx> TypeRelation<'tcx> for Generalizer<'_, 'tcx> {
                 }
             }
 
-            ty::Alias(_, data) => self.generalize_alias_ty(data),
+            ty::Alias(_, data) => match self.structurally_relate_aliases {
+                StructurallyRelateAliases::No => self.generalize_alias_ty(data),
+                StructurallyRelateAliases::Yes => relate::structurally_relate_tys(self, t, t),
+            },
 
             _ => relate::structurally_relate_tys(self, t, t),
         }?;
diff --git a/compiler/rustc_infer/src/infer/relate/glb.rs b/compiler/rustc_infer/src/infer/relate/glb.rs
index 6cf51354599..52a2f4c7347 100644
--- a/compiler/rustc_infer/src/infer/relate/glb.rs
+++ b/compiler/rustc_infer/src/infer/relate/glb.rs
@@ -6,6 +6,7 @@ use rustc_span::Span;
 
 use super::combine::{CombineFields, ObligationEmittingRelation};
 use super::lattice::{self, LatticeDir};
+use super::StructurallyRelateAliases;
 use crate::infer::{DefineOpaqueTypes, InferCtxt, SubregionOrigin};
 use crate::traits::{ObligationCause, PredicateObligations};
 
@@ -45,7 +46,9 @@ impl<'tcx> TypeRelation<'tcx> for Glb<'_, '_, 'tcx> {
         b: T,
     ) -> RelateResult<'tcx, T> {
         match variance {
-            ty::Invariant => self.fields.equate(self.a_is_expected).relate(a, b),
+            ty::Invariant => {
+                self.fields.equate(StructurallyRelateAliases::No, self.a_is_expected).relate(a, b)
+            }
             ty::Covariant => self.relate(a, b),
             // FIXME(#41044) -- not correct, need test
             ty::Bivariant => Ok(a),
@@ -139,6 +142,10 @@ impl<'tcx> ObligationEmittingRelation<'tcx> for Glb<'_, '_, 'tcx> {
         self.fields.trace.span()
     }
 
+    fn structurally_relate_aliases(&self) -> StructurallyRelateAliases {
+        StructurallyRelateAliases::No
+    }
+
     fn param_env(&self) -> ty::ParamEnv<'tcx> {
         self.fields.param_env
     }
diff --git a/compiler/rustc_infer/src/infer/relate/lub.rs b/compiler/rustc_infer/src/infer/relate/lub.rs
index 5b4f80fd73a..fa0da64ca65 100644
--- a/compiler/rustc_infer/src/infer/relate/lub.rs
+++ b/compiler/rustc_infer/src/infer/relate/lub.rs
@@ -2,6 +2,7 @@
 
 use super::combine::{CombineFields, ObligationEmittingRelation};
 use super::lattice::{self, LatticeDir};
+use super::StructurallyRelateAliases;
 use crate::infer::{DefineOpaqueTypes, InferCtxt, SubregionOrigin};
 use crate::traits::{ObligationCause, PredicateObligations};
 
@@ -45,7 +46,9 @@ impl<'tcx> TypeRelation<'tcx> for Lub<'_, '_, 'tcx> {
         b: T,
     ) -> RelateResult<'tcx, T> {
         match variance {
-            ty::Invariant => self.fields.equate(self.a_is_expected).relate(a, b),
+            ty::Invariant => {
+                self.fields.equate(StructurallyRelateAliases::No, self.a_is_expected).relate(a, b)
+            }
             ty::Covariant => self.relate(a, b),
             // FIXME(#41044) -- not correct, need test
             ty::Bivariant => Ok(a),
@@ -139,6 +142,10 @@ impl<'tcx> ObligationEmittingRelation<'tcx> for Lub<'_, '_, 'tcx> {
         self.fields.trace.span()
     }
 
+    fn structurally_relate_aliases(&self) -> StructurallyRelateAliases {
+        StructurallyRelateAliases::No
+    }
+
     fn param_env(&self) -> ty::ParamEnv<'tcx> {
         self.fields.param_env
     }
diff --git a/compiler/rustc_infer/src/infer/relate/mod.rs b/compiler/rustc_infer/src/infer/relate/mod.rs
index 1207377e857..8619cc502ad 100644
--- a/compiler/rustc_infer/src/infer/relate/mod.rs
+++ b/compiler/rustc_infer/src/infer/relate/mod.rs
@@ -9,3 +9,15 @@ mod higher_ranked;
 mod lattice;
 mod lub;
 mod sub;
+
+/// Whether aliases should be related structurally or not. Used
+/// to adjust the behavior of generalization and combine.
+///
+/// This should always be `No` unless in a few special-cases when
+/// instantiating canonical responses and in the new solver. Each
+/// such case should have a comment explaining why it is used.
+#[derive(Debug, Copy, Clone)]
+pub enum StructurallyRelateAliases {
+    Yes,
+    No,
+}
diff --git a/compiler/rustc_infer/src/infer/relate/sub.rs b/compiler/rustc_infer/src/infer/relate/sub.rs
index 5bd3a238a67..2cc8d0d3b10 100644
--- a/compiler/rustc_infer/src/infer/relate/sub.rs
+++ b/compiler/rustc_infer/src/infer/relate/sub.rs
@@ -1,4 +1,5 @@
 use super::combine::CombineFields;
+use super::StructurallyRelateAliases;
 use crate::infer::{DefineOpaqueTypes, ObligationEmittingRelation, SubregionOrigin};
 use crate::traits::{Obligation, PredicateObligations};
 
@@ -64,7 +65,9 @@ impl<'tcx> TypeRelation<'tcx> for Sub<'_, '_, 'tcx> {
         b: T,
     ) -> RelateResult<'tcx, T> {
         match variance {
-            ty::Invariant => self.fields.equate(self.a_is_expected).relate(a, b),
+            ty::Invariant => {
+                self.fields.equate(StructurallyRelateAliases::No, self.a_is_expected).relate(a, b)
+            }
             ty::Covariant => self.relate(a, b),
             ty::Bivariant => Ok(a),
             ty::Contravariant => self.with_expected_switched(|this| this.relate(b, a)),
@@ -204,6 +207,10 @@ impl<'tcx> ObligationEmittingRelation<'tcx> for Sub<'_, '_, 'tcx> {
         self.fields.trace.span()
     }
 
+    fn structurally_relate_aliases(&self) -> StructurallyRelateAliases {
+        StructurallyRelateAliases::No
+    }
+
     fn param_env(&self) -> ty::ParamEnv<'tcx> {
         self.fields.param_env
     }
diff --git a/compiler/rustc_middle/src/traits/solve/inspect.rs b/compiler/rustc_middle/src/traits/solve/inspect.rs
index e94ad4aa539..90180af3b16 100644
--- a/compiler/rustc_middle/src/traits/solve/inspect.rs
+++ b/compiler/rustc_middle/src/traits/solve/inspect.rs
@@ -58,8 +58,6 @@ pub struct GoalEvaluation<'tcx> {
     pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
     pub kind: GoalEvaluationKind<'tcx>,
     pub evaluation: CanonicalGoalEvaluation<'tcx>,
-    /// The nested goals from instantiating the query response.
-    pub returned_goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
 }
 
 #[derive(Eq, PartialEq)]
diff --git a/compiler/rustc_middle/src/traits/solve/inspect/format.rs b/compiler/rustc_middle/src/traits/solve/inspect/format.rs
index 54db8dbd336..89c5eb517e5 100644
--- a/compiler/rustc_middle/src/traits/solve/inspect/format.rs
+++ b/compiler/rustc_middle/src/traits/solve/inspect/format.rs
@@ -48,20 +48,7 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
             },
         };
         writeln!(self.f, "{}: {:?}", goal_text, eval.uncanonicalized_goal)?;
-        self.nested(|this| this.format_canonical_goal_evaluation(&eval.evaluation))?;
-        if eval.returned_goals.len() > 0 {
-            writeln!(self.f, "NESTED GOALS ADDED TO CALLER: [")?;
-            self.nested(|this| {
-                for goal in eval.returned_goals.iter() {
-                    writeln!(this.f, "ADDED GOAL: {goal:?},")?;
-                }
-                Ok(())
-            })?;
-
-            writeln!(self.f, "]")
-        } else {
-            Ok(())
-        }
+        self.nested(|this| this.format_canonical_goal_evaluation(&eval.evaluation))
     }
 
     pub(super) fn format_canonical_goal_evaluation(
diff --git a/compiler/rustc_next_trait_solver/src/canonicalizer.rs b/compiler/rustc_next_trait_solver/src/canonicalizer.rs
index cd434fecce2..7b73e2aebf0 100644
--- a/compiler/rustc_next_trait_solver/src/canonicalizer.rs
+++ b/compiler/rustc_next_trait_solver/src/canonicalizer.rs
@@ -108,21 +108,22 @@ impl<'a, Infcx: InferCtxtLike<Interner = I>, I: Interner> Canonicalizer<'a, Infc
         // universes `n`, this algorithm compresses them in place so that:
         //
         // - the new universe indices are as small as possible
-        // - we only create a new universe if we would otherwise put a placeholder in
-        //   the same compressed universe as an existential which cannot name it
+        // - we create a new universe if we would otherwise
+        //   1. put existentials from a different universe into the same one
+        //   2. put a placeholder in the same universe as an existential which cannot name it
         //
         // Let's walk through an example:
         // - var_infos: [E0, U1, E5, U2, E2, E6, U6], curr_compressed_uv: 0, next_orig_uv: 0
         // - var_infos: [E0, U1, E5, U2, E2, E6, U6], curr_compressed_uv: 0, next_orig_uv: 1
         // - var_infos: [E0, U1, E5, U2, E2, E6, U6], curr_compressed_uv: 1, next_orig_uv: 2
         // - var_infos: [E0, U1, E5, U1, E1, E6, U6], curr_compressed_uv: 1, next_orig_uv: 5
-        // - var_infos: [E0, U1, E1, U1, E1, E6, U6], curr_compressed_uv: 1, next_orig_uv: 6
-        // - var_infos: [E0, U1, E1, U1, E1, E2, U2], curr_compressed_uv: 2, next_orig_uv: -
+        // - var_infos: [E0, U1, E2, U1, E1, E6, U6], curr_compressed_uv: 2, next_orig_uv: 6
+        // - var_infos: [E0, U1, E1, U1, E1, E3, U3], curr_compressed_uv: 2, next_orig_uv: -
         //
         // This algorithm runs in `O(n²)` where `n` is the number of different universe
         // indices in the input. This should be fine as `n` is expected to be small.
         let mut curr_compressed_uv = ty::UniverseIndex::ROOT;
-        let mut existential_in_new_uv = false;
+        let mut existential_in_new_uv = None;
         let mut next_orig_uv = Some(ty::UniverseIndex::ROOT);
         while let Some(orig_uv) = next_orig_uv.take() {
             let mut update_uv = |var: &mut CanonicalVarInfo<I>, orig_uv, is_existential| {
@@ -131,14 +132,29 @@ impl<'a, Infcx: InferCtxtLike<Interner = I>, I: Interner> Canonicalizer<'a, Infc
                     Ordering::Less => (), // Already updated
                     Ordering::Equal => {
                         if is_existential {
-                            existential_in_new_uv = true;
-                        } else if existential_in_new_uv {
+                            if existential_in_new_uv.is_some_and(|uv| uv < orig_uv) {
+                                // Condition 1.
+                                //
+                                // We already put an existential from a outer universe
+                                // into the current compressed universe, so we need to
+                                // create a new one.
+                                curr_compressed_uv = curr_compressed_uv.next_universe();
+                            }
+
+                            // `curr_compressed_uv` will now contain an existential from
+                            // `orig_uv`. Trying to canonicalizing an existential from
+                            // a higher universe has to therefore use a new compressed
+                            // universe.
+                            existential_in_new_uv = Some(orig_uv);
+                        } else if existential_in_new_uv.is_some() {
+                            // Condition 2.
+                            //
                             //  `var` is a placeholder from a universe which is not nameable
                             // by an existential which we already put into the compressed
                             // universe `curr_compressed_uv`. We therefore have to create a
                             // new universe for `var`.
                             curr_compressed_uv = curr_compressed_uv.next_universe();
-                            existential_in_new_uv = false;
+                            existential_in_new_uv = None;
                         }
 
                         *var = var.with_updated_universe(curr_compressed_uv);
@@ -174,8 +190,14 @@ impl<'a, Infcx: InferCtxtLike<Interner = I>, I: Interner> Canonicalizer<'a, Infc
             }
         }
 
+        // We uniquify regions and always put them into their own universe
+        let mut first_region = true;
         for var in var_infos.iter_mut() {
             if var.is_region() {
+                if first_region {
+                    first_region = false;
+                    curr_compressed_uv = curr_compressed_uv.next_universe();
+                }
                 assert!(var.is_existential());
                 *var = var.with_updated_universe(curr_compressed_uv);
             }
diff --git a/compiler/rustc_trait_selection/src/solve/alias_relate.rs b/compiler/rustc_trait_selection/src/solve/alias_relate.rs
index 81be5c09164..afd9d95cb57 100644
--- a/compiler/rustc_trait_selection/src/solve/alias_relate.rs
+++ b/compiler/rustc_trait_selection/src/solve/alias_relate.rs
@@ -8,8 +8,9 @@
 //!
 //! (1.) If we end up with two rigid aliases, then we relate them structurally.
 //!
-//! (2.) If we end up with an infer var and a rigid alias, then
-//! we assign the alias to the infer var.
+//! (2.) If we end up with an infer var and a rigid alias, then we instantiate
+//! the infer var with the constructor of the alias and then recursively relate
+//! the terms.
 //!
 //! (3.) Otherwise, if we end with two rigid (non-projection) or infer types,
 //! relate them structurally.
@@ -53,22 +54,15 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
                 self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
             }
 
-            (Some(_), None) => {
-                if rhs.is_infer() {
-                    self.relate(param_env, lhs, variance, rhs)?;
-                    self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
-                } else {
-                    Err(NoSolution)
-                }
-            }
-            (None, Some(_)) => {
-                if lhs.is_infer() {
-                    self.relate(param_env, lhs, variance, rhs)?;
-                    self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
-                } else {
-                    Err(NoSolution)
-                }
+            (Some(alias), None) => {
+                self.relate_rigid_alias_non_alias(param_env, alias, variance, rhs)
             }
+            (None, Some(alias)) => self.relate_rigid_alias_non_alias(
+                param_env,
+                alias,
+                variance.xform(ty::Variance::Contravariant),
+                lhs,
+            ),
 
             (Some(alias_lhs), Some(alias_rhs)) => {
                 self.relate(param_env, alias_lhs, variance, alias_rhs)?;
@@ -77,6 +71,39 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
         }
     }
 
+    /// Relate a rigid alias with another type. This is the same as
+    /// an ordinary relate except that we treat the outer most alias
+    /// constructor as rigid.
+    #[instrument(level = "debug", skip(self, param_env), ret)]
+    fn relate_rigid_alias_non_alias(
+        &mut self,
+        param_env: ty::ParamEnv<'tcx>,
+        alias: ty::AliasTy<'tcx>,
+        variance: ty::Variance,
+        term: ty::Term<'tcx>,
+    ) -> QueryResult<'tcx> {
+        // NOTE: this check is purely an optimization, the structural eq would
+        // always fail if the term is not an inference variable.
+        if term.is_infer() {
+            let tcx = self.tcx();
+            // We need to relate `alias` to `term` treating only the outermost
+            // constructor as rigid, relating any contained generic arguments as
+            // normal. We do this by first structurally equating the `term`
+            // with the alias constructor instantiated with unconstrained infer vars,
+            // and then relate this with the whole `alias`.
+            //
+            // Alternatively we could modify `Equate` for this case by adding another
+            // variant to `StructurallyRelateAliases`.
+            let identity_args = self.fresh_args_for_item(alias.def_id);
+            let rigid_ctor = ty::AliasTy::new(tcx, alias.def_id, identity_args);
+            self.eq_structurally_relating_aliases(param_env, term, rigid_ctor.to_ty(tcx).into())?;
+            self.eq(param_env, alias, rigid_ctor)?;
+            self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
+        } else {
+            Err(NoSolution)
+        }
+    }
+
     // FIXME: This needs a name that reflects that it's okay to bottom-out with an inference var.
     /// Normalize the `term` to equate it later.
     #[instrument(level = "debug", skip(self, param_env), ret)]
@@ -105,6 +132,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
         }
     }
 
+    #[instrument(level = "debug", skip(self, param_env), ret)]
     fn try_normalize_ty_recur(
         &mut self,
         param_env: ty::ParamEnv<'tcx>,
@@ -128,10 +156,9 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
             );
             this.add_goal(GoalSource::Misc, normalizes_to_goal);
             this.try_evaluate_added_goals()?;
-            let ty = this.resolve_vars_if_possible(normalized_ty);
-            Ok(this.try_normalize_ty_recur(param_env, depth + 1, ty))
+            Ok(this.resolve_vars_if_possible(normalized_ty))
         }) {
-            Ok(ty) => ty,
+            Ok(ty) => self.try_normalize_ty_recur(param_env, depth + 1, ty),
             Err(NoSolution) => Some(ty),
         }
     }
diff --git a/compiler/rustc_trait_selection/src/solve/assembly/mod.rs b/compiler/rustc_trait_selection/src/solve/assembly/mod.rs
index 8e66b1d580f..4c4cd2af779 100644
--- a/compiler/rustc_trait_selection/src/solve/assembly/mod.rs
+++ b/compiler/rustc_trait_selection/src/solve/assembly/mod.rs
@@ -777,6 +777,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
     // 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<'tcx>>(
         &mut self,
         goal: Goal<'tcx, G>,
@@ -799,7 +800,10 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
                 // This feels dangerous.
                 Certainty::Yes => {
                     candidates.retain(|c| match c.source {
-                        CandidateSource::Impl(_) | CandidateSource::BuiltinImpl(_) => false,
+                        CandidateSource::Impl(_) | CandidateSource::BuiltinImpl(_) => {
+                            debug!(?c, "discard impl candidate");
+                            false
+                        }
                         CandidateSource::ParamEnv(_) | CandidateSource::AliasBound => true,
                     });
                 }
@@ -807,6 +811,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
                 // 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);
                 }
             }
diff --git a/compiler/rustc_trait_selection/src/solve/eval_ctxt/canonical.rs b/compiler/rustc_trait_selection/src/solve/eval_ctxt/canonical.rs
index 1a6aa3f144c..251b0a193f1 100644
--- a/compiler/rustc_trait_selection/src/solve/eval_ctxt/canonical.rs
+++ b/compiler/rustc_trait_selection/src/solve/eval_ctxt/canonical.rs
@@ -18,7 +18,7 @@ use rustc_infer::infer::canonical::query_response::make_query_region_constraints
 use rustc_infer::infer::canonical::CanonicalVarValues;
 use rustc_infer::infer::canonical::{CanonicalExt, QueryRegionConstraints};
 use rustc_infer::infer::resolve::EagerResolver;
-use rustc_infer::infer::{DefineOpaqueTypes, InferCtxt, InferOk};
+use rustc_infer::infer::{InferCtxt, InferOk};
 use rustc_middle::infer::canonical::Canonical;
 use rustc_middle::traits::query::NoSolution;
 use rustc_middle::traits::solve::{
@@ -80,7 +80,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
     ///   the values inferred while solving the instantiated goal.
     /// - `external_constraints`: additional constraints which aren't expressible
     ///   using simple unification of inference variables.
-    #[instrument(level = "debug", skip(self))]
+    #[instrument(level = "debug", skip(self), ret)]
     pub(in crate::solve) fn evaluate_added_goals_and_make_canonical_response(
         &mut self,
         certainty: Certainty,
@@ -191,7 +191,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
         param_env: ty::ParamEnv<'tcx>,
         original_values: Vec<ty::GenericArg<'tcx>>,
         response: CanonicalResponse<'tcx>,
-    ) -> Result<(Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution> {
+    ) -> Certainty {
         let instantiation = Self::compute_query_response_instantiation_values(
             self.infcx,
             &original_values,
@@ -201,15 +201,13 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
         let Response { var_values, external_constraints, certainty } =
             response.instantiate(self.tcx(), &instantiation);
 
-        let nested_goals =
-            Self::unify_query_var_values(self.infcx, param_env, &original_values, var_values)?;
+        Self::unify_query_var_values(self.infcx, param_env, &original_values, var_values);
 
         let ExternalConstraintsData { region_constraints, opaque_types } =
             external_constraints.deref();
         self.register_region_constraints(region_constraints);
-        self.register_opaque_types(param_env, opaque_types)?;
-
-        Ok((certainty, nested_goals))
+        self.register_new_opaque_types(param_env, opaque_types);
+        certainty
     }
 
     /// This returns the canoncial variable values to instantiate the bound variables of
@@ -296,32 +294,36 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
         CanonicalVarValues { var_values }
     }
 
-    #[instrument(level = "debug", skip(infcx, param_env), ret)]
+    /// Unify the `original_values` with the `var_values` returned by the canonical query..
+    ///
+    /// This assumes that this unification will always succeed. This is the case when
+    /// applying a query response right away. However, calling a canonical query, doing any
+    /// other kind of trait solving, and only then instantiating the result of the query
+    /// can cause the instantiation to fail. This is not supported and we ICE in this case.
+    ///
+    /// We always structurally instantiate aliases. Relating aliases needs to be different
+    /// depending on whether the alias is *rigid* or not. We're only really able to tell
+    /// whether an alias is rigid by using the trait solver. When instantiating a response
+    /// from the solver we assume that the solver correctly handled aliases and therefore
+    /// always relate them structurally here.
+    #[instrument(level = "debug", skip(infcx), ret)]
     fn unify_query_var_values(
         infcx: &InferCtxt<'tcx>,
         param_env: ty::ParamEnv<'tcx>,
         original_values: &[ty::GenericArg<'tcx>],
         var_values: CanonicalVarValues<'tcx>,
-    ) -> Result<Vec<Goal<'tcx, ty::Predicate<'tcx>>>, NoSolution> {
+    ) {
         assert_eq!(original_values.len(), var_values.len());
 
-        let mut nested_goals = vec![];
+        let cause = ObligationCause::dummy();
         for (&orig, response) in iter::zip(original_values, var_values.var_values) {
-            nested_goals.extend(
-                infcx
-                    .at(&ObligationCause::dummy(), param_env)
-                    .eq(DefineOpaqueTypes::No, orig, response)
-                    .map(|InferOk { value: (), obligations }| {
-                        obligations.into_iter().map(|o| Goal::from(o))
-                    })
-                    .map_err(|e| {
-                        debug!(?e, "failed to equate");
-                        NoSolution
-                    })?,
-            );
+            let InferOk { value: (), obligations } = infcx
+                .at(&cause, param_env)
+                .trace(orig, response)
+                .eq_structurally_relating_aliases(orig, response)
+                .unwrap();
+            assert!(obligations.is_empty());
         }
-
-        Ok(nested_goals)
     }
 
     fn register_region_constraints(&mut self, region_constraints: &QueryRegionConstraints<'tcx>) {
@@ -333,21 +335,17 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
             }
         }
 
-        for member_constraint in &region_constraints.member_constraints {
-            // FIXME: Deal with member constraints :<
-            let _ = member_constraint;
-        }
+        assert!(region_constraints.member_constraints.is_empty());
     }
 
-    fn register_opaque_types(
+    fn register_new_opaque_types(
         &mut self,
         param_env: ty::ParamEnv<'tcx>,
         opaque_types: &[(ty::OpaqueTypeKey<'tcx>, Ty<'tcx>)],
-    ) -> Result<(), NoSolution> {
+    ) {
         for &(key, ty) in opaque_types {
-            self.insert_hidden_type(key, param_env, ty)?;
+            self.insert_hidden_type(key, param_env, ty).unwrap();
         }
-        Ok(())
     }
 }
 
@@ -366,19 +364,21 @@ impl<'tcx> inspect::ProofTreeBuilder<'tcx> {
         )
     }
 
+    /// Instantiate a `CanonicalState`. This assumes that unifying the var values
+    /// trivially succeeds. Adding any inference constraints which weren't present when
+    /// originally computing the canonical query can result in bugs.
     pub fn instantiate_canonical_state<T: TypeFoldable<TyCtxt<'tcx>>>(
         infcx: &InferCtxt<'tcx>,
         param_env: ty::ParamEnv<'tcx>,
         original_values: &[ty::GenericArg<'tcx>],
         state: inspect::CanonicalState<'tcx, T>,
-    ) -> Result<(Vec<Goal<'tcx, ty::Predicate<'tcx>>>, T), NoSolution> {
+    ) -> T {
         let instantiation =
             EvalCtxt::compute_query_response_instantiation_values(infcx, original_values, &state);
 
         let inspect::State { var_values, data } = state.instantiate(infcx.tcx, &instantiation);
 
-        let nested_goals =
-            EvalCtxt::unify_query_var_values(infcx, param_env, original_values, var_values)?;
-        Ok((nested_goals, data))
+        EvalCtxt::unify_query_var_values(infcx, param_env, original_values, var_values);
+        data
     }
 }
diff --git a/compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs b/compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs
index 5c1e8bf616f..ed428bb8e66 100644
--- a/compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs
+++ b/compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs
@@ -17,8 +17,8 @@ use rustc_middle::traits::solve::{
 };
 use rustc_middle::traits::{specialization_graph, DefiningAnchor};
 use rustc_middle::ty::{
-    self, OpaqueTypeKey, Ty, TyCtxt, TypeFoldable, TypeSuperVisitable, TypeVisitable,
-    TypeVisitableExt, TypeVisitor,
+    self, InferCtxtLike, OpaqueTypeKey, Ty, TyCtxt, TypeFoldable, TypeSuperVisitable,
+    TypeVisitable, TypeVisitableExt, TypeVisitor,
 };
 use rustc_session::config::DumpSolverProofTree;
 use rustc_span::DUMMY_SP;
@@ -142,10 +142,7 @@ impl<'tcx> InferCtxt<'tcx> {
         &self,
         goal: Goal<'tcx, ty::Predicate<'tcx>>,
         generate_proof_tree: GenerateProofTree,
-    ) -> (
-        Result<(bool, Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution>,
-        Option<inspect::GoalEvaluation<'tcx>>,
-    ) {
+    ) -> (Result<(bool, Certainty), NoSolution>, Option<inspect::GoalEvaluation<'tcx>>) {
         EvalCtxt::enter_root(self, generate_proof_tree, |ecx| {
             ecx.evaluate_goal(GoalEvaluationKind::Root, GoalSource::Misc, goal)
         })
@@ -327,7 +324,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
         goal_evaluation_kind: GoalEvaluationKind,
         source: GoalSource,
         goal: Goal<'tcx, ty::Predicate<'tcx>>,
-    ) -> Result<(bool, Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution> {
+    ) -> Result<(bool, Certainty), NoSolution> {
         let (orig_values, canonical_goal) = self.canonicalize_goal(goal);
         let mut goal_evaluation =
             self.inspect.new_goal_evaluation(goal, &orig_values, goal_evaluation_kind);
@@ -345,26 +342,13 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
             Ok(response) => response,
         };
 
-        let (certainty, has_changed, nested_goals) = match self
-            .instantiate_response_discarding_overflow(
-                goal.param_env,
-                source,
-                orig_values,
-                canonical_response,
-            ) {
-            Err(e) => {
-                self.inspect.goal_evaluation(goal_evaluation);
-                return Err(e);
-            }
-            Ok(response) => response,
-        };
-        goal_evaluation.returned_goals(&nested_goals);
+        let (certainty, has_changed) = self.instantiate_response_discarding_overflow(
+            goal.param_env,
+            source,
+            orig_values,
+            canonical_response,
+        );
         self.inspect.goal_evaluation(goal_evaluation);
-
-        if !has_changed && !nested_goals.is_empty() {
-            bug!("an unchanged goal shouldn't have any side-effects on instantiation");
-        }
-
         // FIXME: We previously had an assert here that checked that recomputing
         // a goal after applying its constraints did not change its response.
         //
@@ -375,7 +359,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
         // Once we have decided on how to handle trait-system-refactor-initiative#75,
         // we should re-add an assert here.
 
-        Ok((has_changed, certainty, nested_goals))
+        Ok((has_changed, certainty))
     }
 
     fn instantiate_response_discarding_overflow(
@@ -384,7 +368,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
         source: GoalSource,
         original_values: Vec<ty::GenericArg<'tcx>>,
         response: CanonicalResponse<'tcx>,
-    ) -> Result<(Certainty, bool, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution> {
+    ) -> (Certainty, bool) {
         // The old solver did not evaluate nested goals when normalizing.
         // It returned the selection constraints allowing a `Projection`
         // obligation to not hold in coherence while avoiding the fatal error
@@ -405,14 +389,14 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
         };
 
         if response.value.certainty == Certainty::OVERFLOW && !keep_overflow_constraints() {
-            Ok((Certainty::OVERFLOW, false, Vec::new()))
+            (Certainty::OVERFLOW, false)
         } else {
             let has_changed = !response.value.var_values.is_identity_modulo_regions()
                 || !response.value.external_constraints.opaque_types.is_empty();
 
-            let (certainty, nested_goals) =
-                self.instantiate_and_apply_query_response(param_env, original_values, response)?;
-            Ok((certainty, has_changed, nested_goals))
+            let certainty =
+                self.instantiate_and_apply_query_response(param_env, original_values, response);
+            (certainty, has_changed)
         }
     }
 
@@ -537,12 +521,11 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
                 ty::NormalizesTo { alias: goal.predicate.alias, term: unconstrained_rhs },
             );
 
-            let (_, certainty, instantiate_goals) = self.evaluate_goal(
+            let (_, certainty) = self.evaluate_goal(
                 GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::Yes },
                 GoalSource::Misc,
                 unconstrained_goal,
             )?;
-            self.nested_goals.goals.extend(with_misc_source(instantiate_goals));
 
             // Finally, equate the goal's RHS with the unconstrained var.
             // We put the nested goals from this into goals instead of
@@ -573,12 +556,11 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
         }
 
         for (source, goal) in goals.goals.drain(..) {
-            let (has_changed, certainty, instantiate_goals) = self.evaluate_goal(
+            let (has_changed, certainty) = self.evaluate_goal(
                 GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::No },
                 source,
                 goal,
             )?;
-            self.nested_goals.goals.extend(with_misc_source(instantiate_goals));
             if has_changed {
                 unchanged_certainty = None;
             }
@@ -626,76 +608,101 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
 
     /// Is the projection predicate is of the form `exists<T> <Ty as Trait>::Assoc = T`.
     ///
-    /// This is the case if the `term` is an inference variable in the innermost universe
-    /// and does not occur in any other part of the predicate.
+    /// This is the case if the `term` does not occur in any other part of the predicate
+    /// and is able to name all other placeholder and inference variables.
     #[instrument(level = "debug", skip(self), ret)]
     pub(super) fn term_is_fully_unconstrained(
         &self,
         goal: Goal<'tcx, ty::NormalizesTo<'tcx>>,
     ) -> bool {
-        let term_is_infer = match goal.predicate.term.unpack() {
+        let universe_of_term = match goal.predicate.term.unpack() {
             ty::TermKind::Ty(ty) => {
                 if let &ty::Infer(ty::TyVar(vid)) = ty.kind() {
-                    match self.infcx.probe_ty_var(vid) {
-                        Ok(value) => bug!("resolved var in query: {goal:?} {value:?}"),
-                        Err(universe) => universe == self.infcx.universe(),
-                    }
+                    self.infcx.universe_of_ty(vid).unwrap()
                 } else {
-                    false
+                    return false;
                 }
             }
             ty::TermKind::Const(ct) => {
                 if let ty::ConstKind::Infer(ty::InferConst::Var(vid)) = ct.kind() {
-                    match self.infcx.probe_const_var(vid) {
-                        Ok(value) => bug!("resolved var in query: {goal:?} {value:?}"),
-                        Err(universe) => universe == self.infcx.universe(),
-                    }
+                    self.infcx.universe_of_ct(vid).unwrap()
                 } else {
-                    false
+                    return false;
                 }
             }
         };
 
-        // Guard against `<T as Trait<?0>>::Assoc = ?0>`.
-        struct ContainsTerm<'a, 'tcx> {
+        struct ContainsTermOrNotNameable<'a, 'tcx> {
             term: ty::Term<'tcx>,
+            universe_of_term: ty::UniverseIndex,
             infcx: &'a InferCtxt<'tcx>,
         }
-        impl<'tcx> TypeVisitor<TyCtxt<'tcx>> for ContainsTerm<'_, 'tcx> {
+
+        impl<'a, 'tcx> ContainsTermOrNotNameable<'a, 'tcx> {
+            fn check_nameable(&self, universe: ty::UniverseIndex) -> ControlFlow<()> {
+                if self.universe_of_term.can_name(universe) {
+                    ControlFlow::Continue(())
+                } else {
+                    ControlFlow::Break(())
+                }
+            }
+        }
+
+        impl<'tcx> TypeVisitor<TyCtxt<'tcx>> for ContainsTermOrNotNameable<'_, 'tcx> {
             type BreakTy = ();
             fn visit_ty(&mut self, t: Ty<'tcx>) -> ControlFlow<Self::BreakTy> {
-                if let Some(vid) = t.ty_vid()
-                    && let ty::TermKind::Ty(term) = self.term.unpack()
-                    && let Some(term_vid) = term.ty_vid()
-                    && self.infcx.root_var(vid) == self.infcx.root_var(term_vid)
-                {
-                    ControlFlow::Break(())
-                } else if t.has_non_region_infer() {
-                    t.super_visit_with(self)
-                } else {
-                    ControlFlow::Continue(())
+                match *t.kind() {
+                    ty::Infer(ty::TyVar(vid)) => {
+                        if let ty::TermKind::Ty(term) = self.term.unpack()
+                            && let Some(term_vid) = term.ty_vid()
+                            && self.infcx.root_var(vid) == self.infcx.root_var(term_vid)
+                        {
+                            ControlFlow::Break(())
+                        } else {
+                            self.check_nameable(self.infcx.universe_of_ty(vid).unwrap())
+                        }
+                    }
+                    ty::Placeholder(p) => self.check_nameable(p.universe),
+                    _ => {
+                        if t.has_non_region_infer() || t.has_placeholders() {
+                            t.super_visit_with(self)
+                        } else {
+                            ControlFlow::Continue(())
+                        }
+                    }
                 }
             }
 
             fn visit_const(&mut self, c: ty::Const<'tcx>) -> ControlFlow<Self::BreakTy> {
-                if let ty::ConstKind::Infer(ty::InferConst::Var(vid)) = c.kind()
-                    && let ty::TermKind::Const(term) = self.term.unpack()
-                    && let ty::ConstKind::Infer(ty::InferConst::Var(term_vid)) = term.kind()
-                    && self.infcx.root_const_var(vid) == self.infcx.root_const_var(term_vid)
-                {
-                    ControlFlow::Break(())
-                } else if c.has_non_region_infer() {
-                    c.super_visit_with(self)
-                } else {
-                    ControlFlow::Continue(())
+                match c.kind() {
+                    ty::ConstKind::Infer(ty::InferConst::Var(vid)) => {
+                        if let ty::TermKind::Const(term) = self.term.unpack()
+                            && let ty::ConstKind::Infer(ty::InferConst::Var(term_vid)) = term.kind()
+                            && self.infcx.root_const_var(vid) == self.infcx.root_const_var(term_vid)
+                        {
+                            ControlFlow::Break(())
+                        } else {
+                            self.check_nameable(self.infcx.universe_of_ct(vid).unwrap())
+                        }
+                    }
+                    ty::ConstKind::Placeholder(p) => self.check_nameable(p.universe),
+                    _ => {
+                        if c.has_non_region_infer() || c.has_placeholders() {
+                            c.super_visit_with(self)
+                        } else {
+                            ControlFlow::Continue(())
+                        }
+                    }
                 }
             }
         }
 
-        let mut visitor = ContainsTerm { infcx: self.infcx, term: goal.predicate.term };
-
-        term_is_infer
-            && goal.predicate.alias.visit_with(&mut visitor).is_continue()
+        let mut visitor = ContainsTermOrNotNameable {
+            infcx: self.infcx,
+            universe_of_term,
+            term: goal.predicate.term,
+        };
+        goal.predicate.alias.visit_with(&mut visitor).is_continue()
             && goal.param_env.visit_with(&mut visitor).is_continue()
     }
 
@@ -718,6 +725,26 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
             })
     }
 
+    /// This sohuld only be used when we're either instantiating a previously
+    /// unconstrained "return value" or when we're sure that all aliases in
+    /// the types are rigid.
+    #[instrument(level = "debug", skip(self, param_env), ret)]
+    pub(super) fn eq_structurally_relating_aliases<T: ToTrace<'tcx>>(
+        &mut self,
+        param_env: ty::ParamEnv<'tcx>,
+        lhs: T,
+        rhs: T,
+    ) -> Result<(), NoSolution> {
+        let cause = ObligationCause::dummy();
+        let InferOk { value: (), obligations } = self
+            .infcx
+            .at(&cause, param_env)
+            .trace(lhs, rhs)
+            .eq_structurally_relating_aliases(lhs, rhs)?;
+        assert!(obligations.is_empty());
+        Ok(())
+    }
+
     #[instrument(level = "debug", skip(self, param_env), ret)]
     pub(super) fn sub<T: ToTrace<'tcx>>(
         &mut self,
diff --git a/compiler/rustc_trait_selection/src/solve/eval_ctxt/select.rs b/compiler/rustc_trait_selection/src/solve/eval_ctxt/select.rs
index 7196a5af259..3262d64cb7d 100644
--- a/compiler/rustc_trait_selection/src/solve/eval_ctxt/select.rs
+++ b/compiler/rustc_trait_selection/src/solve/eval_ctxt/select.rs
@@ -58,44 +58,26 @@ impl<'tcx> InferCtxt<'tcx> {
                 }
 
                 let candidate = candidates.pop().unwrap();
-                let (certainty, nested_goals) = ecx
-                    .instantiate_and_apply_query_response(
-                        trait_goal.param_env,
-                        orig_values,
-                        candidate.result,
-                    )
-                    .map_err(|_| SelectionError::Unimplemented)?;
-
-                Ok(Some((candidate, certainty, nested_goals)))
+                let certainty = ecx.instantiate_and_apply_query_response(
+                    trait_goal.param_env,
+                    orig_values,
+                    candidate.result,
+                );
+
+                Ok(Some((candidate, certainty)))
             });
 
-            let (candidate, certainty, nested_goals) = match result {
-                Ok(Some((candidate, certainty, nested_goals))) => {
-                    (candidate, certainty, nested_goals)
-                }
+            let (candidate, certainty) = match result {
+                Ok(Some(result)) => result,
                 Ok(None) => return Ok(None),
                 Err(e) => return Err(e),
             };
 
-            let nested_obligations: Vec<_> = nested_goals
-                .into_iter()
-                .map(|goal| {
-                    Obligation::new(
-                        self.tcx,
-                        ObligationCause::dummy(),
-                        goal.param_env,
-                        goal.predicate,
-                    )
-                })
-                .collect();
-
             let goal = self.resolve_vars_if_possible(trait_goal);
             match (certainty, candidate.source) {
                 // Rematching the implementation will instantiate the same nested goals that
                 // would have caused the ambiguity, so we can still make progress here regardless.
-                (_, CandidateSource::Impl(def_id)) => {
-                    rematch_impl(self, goal, def_id, nested_obligations)
-                }
+                (_, CandidateSource::Impl(def_id)) => rematch_impl(self, goal, def_id),
 
                 // If an unsize goal is ambiguous, then we can manually rematch it to make
                 // selection progress for coercion during HIR typeck. If it is *not* ambiguous,
@@ -108,20 +90,20 @@ impl<'tcx> InferCtxt<'tcx> {
                 | (Certainty::Yes, CandidateSource::BuiltinImpl(src @ BuiltinImplSource::Misc))
                     if self.tcx.lang_items().unsize_trait() == Some(goal.predicate.def_id()) =>
                 {
-                    rematch_unsize(self, goal, nested_obligations, src, certainty)
+                    rematch_unsize(self, goal, src, certainty)
                 }
 
                 // Technically some builtin impls have nested obligations, but if
                 // `Certainty::Yes`, then they should've all been verified and don't
                 // need re-checking.
                 (Certainty::Yes, CandidateSource::BuiltinImpl(src)) => {
-                    Ok(Some(ImplSource::Builtin(src, nested_obligations)))
+                    Ok(Some(ImplSource::Builtin(src, vec![])))
                 }
 
                 // It's fine not to do anything to rematch these, since there are no
                 // nested obligations.
                 (Certainty::Yes, CandidateSource::ParamEnv(_) | CandidateSource::AliasBound) => {
-                    Ok(Some(ImplSource::Param(nested_obligations)))
+                    Ok(Some(ImplSource::Param(vec![])))
                 }
 
                 (Certainty::Maybe(_), _) => Ok(None),
@@ -192,19 +174,16 @@ fn rematch_impl<'tcx>(
     infcx: &InferCtxt<'tcx>,
     goal: Goal<'tcx, ty::TraitPredicate<'tcx>>,
     impl_def_id: DefId,
-    mut nested: Vec<PredicateObligation<'tcx>>,
 ) -> SelectionResult<'tcx, Selection<'tcx>> {
     let args = infcx.fresh_args_for_item(DUMMY_SP, impl_def_id);
     let impl_trait_ref =
         infcx.tcx.impl_trait_ref(impl_def_id).unwrap().instantiate(infcx.tcx, args);
 
-    nested.extend(
-        infcx
-            .at(&ObligationCause::dummy(), goal.param_env)
-            .eq(DefineOpaqueTypes::No, goal.predicate.trait_ref, impl_trait_ref)
-            .map_err(|_| SelectionError::Unimplemented)?
-            .into_obligations(),
-    );
+    let mut nested = infcx
+        .at(&ObligationCause::dummy(), goal.param_env)
+        .eq(DefineOpaqueTypes::No, goal.predicate.trait_ref, impl_trait_ref)
+        .map_err(|_| SelectionError::Unimplemented)?
+        .into_obligations();
 
     nested.extend(
         infcx.tcx.predicates_of(impl_def_id).instantiate(infcx.tcx, args).into_iter().map(
@@ -221,11 +200,11 @@ fn rematch_impl<'tcx>(
 fn rematch_unsize<'tcx>(
     infcx: &InferCtxt<'tcx>,
     goal: Goal<'tcx, ty::TraitPredicate<'tcx>>,
-    mut nested: Vec<PredicateObligation<'tcx>>,
     source: BuiltinImplSource,
     certainty: Certainty,
 ) -> SelectionResult<'tcx, Selection<'tcx>> {
     let tcx = infcx.tcx;
+    let mut nested = vec![];
     let a_ty = structurally_normalize(goal.predicate.self_ty(), infcx, goal.param_env, &mut nested);
     let b_ty = structurally_normalize(
         goal.predicate.trait_ref.args.type_at(1),
diff --git a/compiler/rustc_trait_selection/src/solve/fulfill.rs b/compiler/rustc_trait_selection/src/solve/fulfill.rs
index 97f715b6386..c1b07765e50 100644
--- a/compiler/rustc_trait_selection/src/solve/fulfill.rs
+++ b/compiler/rustc_trait_selection/src/solve/fulfill.rs
@@ -2,7 +2,6 @@ use std::mem;
 
 use rustc_infer::infer::InferCtxt;
 use rustc_infer::traits::solve::MaybeCause;
-use rustc_infer::traits::Obligation;
 use rustc_infer::traits::{
     query::NoSolution, FulfillmentError, FulfillmentErrorCode, MismatchedProjectionTypes,
     PredicateObligation, SelectionError, TraitEngine,
@@ -11,7 +10,7 @@ use rustc_middle::ty;
 use rustc_middle::ty::error::{ExpectedFound, TypeError};
 
 use super::eval_ctxt::GenerateProofTree;
-use super::{Certainty, Goal, InferCtxtEvalExt};
+use super::{Certainty, InferCtxtEvalExt};
 
 /// A trait engine using the new trait solver.
 ///
@@ -48,11 +47,11 @@ impl<'tcx> FulfillmentCtxt<'tcx> {
         &self,
         infcx: &InferCtxt<'tcx>,
         obligation: &PredicateObligation<'tcx>,
-        result: &Result<(bool, Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution>,
+        result: &Result<(bool, Certainty), NoSolution>,
     ) {
         if let Some(inspector) = infcx.obligation_inspector.get() {
             let result = match result {
-                Ok((_, c, _)) => Ok(*c),
+                Ok((_, c)) => Ok(*c),
                 Err(NoSolution) => Err(NoSolution),
             };
             (inspector)(infcx, &obligation, result);
@@ -80,13 +79,13 @@ impl<'tcx> TraitEngine<'tcx> for FulfillmentCtxt<'tcx> {
                         .evaluate_root_goal(obligation.clone().into(), GenerateProofTree::IfEnabled)
                         .0
                     {
-                        Ok((_, Certainty::Maybe(MaybeCause::Ambiguity), _)) => {
+                        Ok((_, Certainty::Maybe(MaybeCause::Ambiguity))) => {
                             FulfillmentErrorCode::Ambiguity { overflow: false }
                         }
-                        Ok((_, Certainty::Maybe(MaybeCause::Overflow), _)) => {
+                        Ok((_, Certainty::Maybe(MaybeCause::Overflow))) => {
                             FulfillmentErrorCode::Ambiguity { overflow: true }
                         }
-                        Ok((_, Certainty::Yes, _)) => {
+                        Ok((_, Certainty::Yes)) => {
                             bug!("did not expect successful goal when collecting ambiguity errors")
                         }
                         Err(_) => {
@@ -120,7 +119,7 @@ impl<'tcx> TraitEngine<'tcx> for FulfillmentCtxt<'tcx> {
                 let goal = obligation.clone().into();
                 let result = infcx.evaluate_root_goal(goal, GenerateProofTree::IfEnabled).0;
                 self.inspect_evaluated_obligation(infcx, &obligation, &result);
-                let (changed, certainty, nested_goals) = match result {
+                let (changed, certainty) = match result {
                     Ok(result) => result,
                     Err(NoSolution) => {
                         errors.push(FulfillmentError {
@@ -178,16 +177,6 @@ impl<'tcx> TraitEngine<'tcx> for FulfillmentCtxt<'tcx> {
                         continue;
                     }
                 };
-                // Push any nested goals that we get from unifying our canonical response
-                // with our obligation onto the fulfillment context.
-                self.obligations.extend(nested_goals.into_iter().map(|goal| {
-                    Obligation::new(
-                        infcx.tcx,
-                        obligation.cause.clone(),
-                        goal.param_env,
-                        goal.predicate,
-                    )
-                }));
                 has_changed |= changed;
                 match certainty {
                     Certainty::Yes => {}
diff --git a/compiler/rustc_trait_selection/src/solve/inspect/analyse.rs b/compiler/rustc_trait_selection/src/solve/inspect/analyse.rs
index c5d4ce33d86..52b900af853 100644
--- a/compiler/rustc_trait_selection/src/solve/inspect/analyse.rs
+++ b/compiler/rustc_trait_selection/src/solve/inspect/analyse.rs
@@ -63,21 +63,12 @@ impl<'a, 'tcx> InspectCandidate<'a, 'tcx> {
             infcx.probe(|_| {
                 let mut instantiated_goals = vec![];
                 for goal in &self.nested_goals {
-                    let goal = match ProofTreeBuilder::instantiate_canonical_state(
+                    let goal = ProofTreeBuilder::instantiate_canonical_state(
                         infcx,
                         self.goal.goal.param_env,
                         self.goal.orig_values,
                         *goal,
-                    ) {
-                        Ok((_goals, goal)) => goal,
-                        Err(NoSolution) => {
-                            warn!(
-                                "unexpected failure when instantiating {:?}: {:?}",
-                                goal, self.nested_goals
-                            );
-                            return ControlFlow::Continue(());
-                        }
-                    };
+                    );
                     instantiated_goals.push(goal);
                 }
 
diff --git a/compiler/rustc_trait_selection/src/solve/inspect/build.rs b/compiler/rustc_trait_selection/src/solve/inspect/build.rs
index b587a93b24c..f7b310a7abe 100644
--- a/compiler/rustc_trait_selection/src/solve/inspect/build.rs
+++ b/compiler/rustc_trait_selection/src/solve/inspect/build.rs
@@ -87,7 +87,6 @@ struct WipGoalEvaluation<'tcx> {
     pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
     pub kind: WipGoalEvaluationKind<'tcx>,
     pub evaluation: Option<WipCanonicalGoalEvaluation<'tcx>>,
-    pub returned_goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
 }
 
 impl<'tcx> WipGoalEvaluation<'tcx> {
@@ -103,7 +102,6 @@ impl<'tcx> WipGoalEvaluation<'tcx> {
                 }
             },
             evaluation: self.evaluation.unwrap().finalize(),
-            returned_goals: self.returned_goals,
         }
     }
 }
@@ -312,7 +310,6 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
                 }
             },
             evaluation: None,
-            returned_goals: vec![],
         })
     }
 
@@ -369,17 +366,6 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
         }
     }
 
-    pub fn returned_goals(&mut self, goals: &[Goal<'tcx, ty::Predicate<'tcx>>]) {
-        if let Some(this) = self.as_mut() {
-            match this {
-                DebugSolver::GoalEvaluation(evaluation) => {
-                    assert!(evaluation.returned_goals.is_empty());
-                    evaluation.returned_goals.extend(goals);
-                }
-                _ => unreachable!(),
-            }
-        }
-    }
     pub fn goal_evaluation(&mut self, goal_evaluation: ProofTreeBuilder<'tcx>) {
         if let Some(this) = self.as_mut() {
             match (this, *goal_evaluation.state.unwrap()) {
diff --git a/compiler/rustc_trait_selection/src/solve/mod.rs b/compiler/rustc_trait_selection/src/solve/mod.rs
index 8b163d47d34..51094b781c0 100644
--- a/compiler/rustc_trait_selection/src/solve/mod.rs
+++ b/compiler/rustc_trait_selection/src/solve/mod.rs
@@ -267,6 +267,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
     /// This function is necessary in nearly all cases before matching on a type.
     /// Not doing so is likely to be incomplete and therefore unsound during
     /// coherence.
+    #[instrument(level = "debug", skip(self, param_env), ret)]
     fn structurally_normalize_ty(
         &mut self,
         param_env: ty::ParamEnv<'tcx>,
diff --git a/compiler/rustc_trait_selection/src/solve/normalizes_to/mod.rs b/compiler/rustc_trait_selection/src/solve/normalizes_to/mod.rs
index 5f625831156..aa8cc3667cd 100644
--- a/compiler/rustc_trait_selection/src/solve/normalizes_to/mod.rs
+++ b/compiler/rustc_trait_selection/src/solve/normalizes_to/mod.rs
@@ -68,6 +68,34 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
             kind => bug!("unknown DefKind {} in projection goal: {goal:#?}", kind.descr(def_id)),
         }
     }
+
+    /// When normalizing an associated item, constrain the result to `term`.
+    ///
+    /// While `NormalizesTo` goals have the normalized-to term as an argument,
+    /// this argument is always fully unconstrained for associated items.
+    /// It is therefore appropriate to instead think of these `NormalizesTo` goals
+    /// as function returning a term after normalizing.
+    ///
+    /// When equating an inference variable and an alias, we tend to emit `alias-relate`
+    /// goals and only actually instantiate the inference variable with an alias if the
+    /// alias is rigid. However, this means that constraining the expected term of
+    /// such goals ends up fully structurally normalizing the resulting type instead of
+    /// only by one step. To avoid this we instead use structural equality here, resulting
+    /// in each `NormalizesTo` only projects by a single step.
+    ///
+    /// Not doing so, currently causes issues because trying to normalize an opaque type
+    /// during alias-relate doesn't actually constrain the opaque if the concrete type
+    /// is an inference variable. This means that `NormalizesTo` for associated types
+    /// normalizing to an opaque type always resulted in ambiguity, breaking tests e.g.
+    /// tests/ui/type-alias-impl-trait/issue-78450.rs.
+    pub fn instantiate_normalizes_to_term(
+        &mut self,
+        goal: Goal<'tcx, NormalizesTo<'tcx>>,
+        term: ty::Term<'tcx>,
+    ) {
+        self.eq_structurally_relating_aliases(goal.param_env, goal.predicate.term, term)
+            .expect("expected goal term to be fully unconstrained");
+    }
 }
 
 impl<'tcx> assembly::GoalKind<'tcx> for NormalizesTo<'tcx> {
@@ -104,8 +132,8 @@ impl<'tcx> assembly::GoalKind<'tcx> for NormalizesTo<'tcx> {
                         goal.predicate.alias,
                         assumption_projection_pred.projection_ty,
                     )?;
-                    ecx.eq(goal.param_env, goal.predicate.term, assumption_projection_pred.term)
-                        .expect("expected goal term to be fully unconstrained");
+
+                    ecx.instantiate_normalizes_to_term(goal, assumption_projection_pred.term);
 
                     // Add GAT where clauses from the trait's definition
                     ecx.add_goals(
@@ -192,8 +220,7 @@ impl<'tcx> assembly::GoalKind<'tcx> for NormalizesTo<'tcx> {
                         "cannot project to an associated function"
                     ),
                 };
-                ecx.eq(goal.param_env, goal.predicate.term, error_term)
-                    .expect("expected goal term to be fully unconstrained");
+                ecx.instantiate_normalizes_to_term(goal, error_term);
                 ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
             };
 
@@ -248,8 +275,7 @@ impl<'tcx> assembly::GoalKind<'tcx> for NormalizesTo<'tcx> {
                 ty::AssocKind::Fn => unreachable!("we should never project to a fn"),
             };
 
-            ecx.eq(goal.param_env, goal.predicate.term, term.instantiate(tcx, args))
-                .expect("expected goal term to be fully unconstrained");
+            ecx.instantiate_normalizes_to_term(goal, term.instantiate(tcx, args));
             ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
         })
     }
@@ -456,7 +482,7 @@ impl<'tcx> assembly::GoalKind<'tcx> for NormalizesTo<'tcx> {
             borrow_region.expect_region(),
         );
 
-        ecx.eq(goal.param_env, goal.predicate.term.ty().unwrap(), upvars_ty)?;
+        ecx.instantiate_normalizes_to_term(goal, upvars_ty.into());
         ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
     }
 
@@ -543,8 +569,7 @@ impl<'tcx> assembly::GoalKind<'tcx> for NormalizesTo<'tcx> {
                 ),
             };
 
-            ecx.eq(goal.param_env, goal.predicate.term, metadata_ty.into())
-                .expect("expected goal term to be fully unconstrained");
+            ecx.instantiate_normalizes_to_term(goal, metadata_ty.into());
             ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
         })
     }
@@ -627,20 +652,22 @@ impl<'tcx> assembly::GoalKind<'tcx> for NormalizesTo<'tcx> {
         }
 
         ecx.probe_misc_candidate("builtin AsyncIterator kind").enter(|ecx| {
+            let expected_ty = ecx.next_ty_infer();
             // Take `AsyncIterator<Item = I>` and turn it into the corresponding
             // coroutine yield ty `Poll<Option<I>>`.
-            let expected_ty = Ty::new_adt(
+            let wrapped_expected_ty = Ty::new_adt(
                 tcx,
                 tcx.adt_def(tcx.require_lang_item(LangItem::Poll, None)),
                 tcx.mk_args(&[Ty::new_adt(
                     tcx,
                     tcx.adt_def(tcx.require_lang_item(LangItem::Option, None)),
-                    tcx.mk_args(&[goal.predicate.term.into()]),
+                    tcx.mk_args(&[expected_ty.into()]),
                 )
                 .into()]),
             );
             let yield_ty = args.as_coroutine().yield_ty();
-            ecx.eq(goal.param_env, expected_ty, yield_ty)?;
+            ecx.eq(goal.param_env, wrapped_expected_ty, yield_ty)?;
+            ecx.instantiate_normalizes_to_term(goal, expected_ty.into());
             ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
         })
     }
@@ -742,8 +769,7 @@ impl<'tcx> assembly::GoalKind<'tcx> for NormalizesTo<'tcx> {
         };
 
         ecx.probe_misc_candidate("builtin discriminant kind").enter(|ecx| {
-            ecx.eq(goal.param_env, goal.predicate.term, discriminant_ty.into())
-                .expect("expected goal term to be fully unconstrained");
+            ecx.instantiate_normalizes_to_term(goal, discriminant_ty.into());
             ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
         })
     }
diff --git a/tests/ui/coherence/occurs-check/associated-type.next.stderr b/tests/ui/coherence/occurs-check/associated-type.next.stderr
index 6119e6149a7..50b83b90b0b 100644
--- a/tests/ui/coherence/occurs-check/associated-type.next.stderr
+++ b/tests/ui/coherence/occurs-check/associated-type.next.stderr
@@ -1,11 +1,7 @@
 WARN rustc_infer::infer::relate::generalize may incompletely handle alias type: AliasTy { args: [*const ?1t, ReBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrNamed(DefId(0:27 ~ associated_type[f554]::{impl#3}::'a#1), 'a) })], def_id: DefId(0:5 ~ associated_type[f554]::ToUnit::Unit) }
-WARN rustc_infer::infer::relate::generalize may incompletely handle alias type: AliasTy { args: [*const ?1t, RePlaceholder(!1_BoundRegion { var: 0, kind: BrNamed(DefId(0:27 ~ associated_type[f554]::{impl#3}::'a#1), 'a) })], def_id: DefId(0:5 ~ associated_type[f554]::ToUnit::Unit) }
 WARN rustc_infer::infer::relate::generalize may incompletely handle alias type: AliasTy { args: [*const ?1t, ReBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrNamed(DefId(0:27 ~ associated_type[f554]::{impl#3}::'a#1), 'a) })], def_id: DefId(0:5 ~ associated_type[f554]::ToUnit::Unit) }
-WARN rustc_infer::infer::relate::generalize may incompletely handle alias type: AliasTy { args: [*const ?1t, RePlaceholder(!1_BoundRegion { var: 0, kind: BrNamed(DefId(0:27 ~ associated_type[f554]::{impl#3}::'a#1), 'a) })], def_id: DefId(0:5 ~ associated_type[f554]::ToUnit::Unit) }
 WARN rustc_infer::infer::relate::generalize may incompletely handle alias type: AliasTy { args: [*const ?1t, ReBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrNamed(DefId(0:27 ~ associated_type[f554]::{impl#3}::'a#1), 'a) })], def_id: DefId(0:5 ~ associated_type[f554]::ToUnit::Unit) }
-WARN rustc_infer::infer::relate::generalize may incompletely handle alias type: AliasTy { args: [*const ?1t, RePlaceholder(!1_BoundRegion { var: 0, kind: BrNamed(DefId(0:27 ~ associated_type[f554]::{impl#3}::'a#1), 'a) })], def_id: DefId(0:5 ~ associated_type[f554]::ToUnit::Unit) }
 WARN rustc_infer::infer::relate::generalize may incompletely handle alias type: AliasTy { args: [*const ?1t, ReBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrNamed(DefId(0:27 ~ associated_type[f554]::{impl#3}::'a#1), 'a) })], def_id: DefId(0:5 ~ associated_type[f554]::ToUnit::Unit) }
-WARN rustc_infer::infer::relate::generalize may incompletely handle alias type: AliasTy { args: [*const ?1t, RePlaceholder(!1_BoundRegion { var: 0, kind: BrNamed(DefId(0:27 ~ associated_type[f554]::{impl#3}::'a#1), 'a) })], def_id: DefId(0:5 ~ associated_type[f554]::ToUnit::Unit) }
 error[E0119]: conflicting implementations of trait `Overlap<for<'a> fn(&'a (), ())>` for type `for<'a> fn(&'a (), ())`
   --> $DIR/associated-type.rs:31:1
    |
diff --git a/tests/ui/coherence/occurs-check/opaques.next.stderr b/tests/ui/coherence/occurs-check/opaques.next.stderr
index 4ad8257d2c1..a5182eb5d9c 100644
--- a/tests/ui/coherence/occurs-check/opaques.next.stderr
+++ b/tests/ui/coherence/occurs-check/opaques.next.stderr
@@ -1,17 +1,17 @@
-error[E0119]: conflicting implementations of trait `Trait<Alias<_>>` for type `Alias<_>`
+error[E0119]: conflicting implementations of trait `Trait<_>`
   --> $DIR/opaques.rs:30:1
    |
 LL | impl<T> Trait<T> for T {
    | ---------------------- first implementation here
 ...
 LL | impl<T> Trait<T> for defining_scope::Alias<T> {
-   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ conflicting implementation for `Alias<_>`
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ conflicting implementation
 
 error[E0282]: type annotations needed
   --> $DIR/opaques.rs:13:20
    |
 LL |     pub fn cast<T>(x: Container<Alias<T>, T>) -> Container<T, T> {
-   |                    ^ cannot infer type for struct `Container<Alias<T>, T>`
+   |                    ^ cannot infer type for struct `Container<T, T>`
 
 error: aborting due to 2 previous errors
 
diff --git a/tests/ui/impl-trait/auto-trait-coherence.next.stderr b/tests/ui/impl-trait/auto-trait-coherence.next.stderr
index 3f979d1a50b..cd91bfcb48d 100644
--- a/tests/ui/impl-trait/auto-trait-coherence.next.stderr
+++ b/tests/ui/impl-trait/auto-trait-coherence.next.stderr
@@ -1,11 +1,11 @@
-error[E0119]: conflicting implementations of trait `AnotherTrait` for type `D<OpaqueType>`
+error[E0119]: conflicting implementations of trait `AnotherTrait` for type `D<_>`
   --> $DIR/auto-trait-coherence.rs:24:1
    |
 LL | impl<T: Send> AnotherTrait for T {}
    | -------------------------------- first implementation here
 ...
 LL | impl AnotherTrait for D<OpaqueType> {
-   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ conflicting implementation for `D<OpaqueType>`
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ conflicting implementation for `D<_>`
 
 error: aborting due to 1 previous error
 
diff --git a/tests/ui/impl-trait/auto-trait-coherence.rs b/tests/ui/impl-trait/auto-trait-coherence.rs
index 0f089c5adbd..e3036fd0fe2 100644
--- a/tests/ui/impl-trait/auto-trait-coherence.rs
+++ b/tests/ui/impl-trait/auto-trait-coherence.rs
@@ -22,7 +22,8 @@ impl<T: Send> AnotherTrait for T {}
 // (We treat opaque types as "foreign types" that could grow more impls
 // in the future.)
 impl AnotherTrait for D<OpaqueType> {
-    //~^ ERROR conflicting implementations of trait `AnotherTrait` for type `D<OpaqueType>`
+    //[old]~^ ERROR conflicting implementations of trait `AnotherTrait` for type `D<OpaqueType>`
+    //[next]~^^ ERROR conflicting implementations of trait `AnotherTrait` for type `D<_>`
 }
 
 fn main() {}
diff --git a/tests/ui/impl-trait/two_tait_defining_each_other2.current.stderr b/tests/ui/impl-trait/two_tait_defining_each_other2.current.stderr
index 33866451c6b..c5c9ae33f4d 100644
--- a/tests/ui/impl-trait/two_tait_defining_each_other2.current.stderr
+++ b/tests/ui/impl-trait/two_tait_defining_each_other2.current.stderr
@@ -7,7 +7,7 @@ LL | type A = impl Foo;
    = note: `A` must be used in combination with a concrete type within the same module
 
 error: opaque type's hidden type cannot be another opaque type from the same scope
-  --> $DIR/two_tait_defining_each_other2.rs:11:5
+  --> $DIR/two_tait_defining_each_other2.rs:12:5
    |
 LL |     x // B's hidden type is A (opaquely)
    |     ^ one of the two opaque types used here has to be outside its defining scope
diff --git a/tests/ui/impl-trait/two_tait_defining_each_other2.next.stderr b/tests/ui/impl-trait/two_tait_defining_each_other2.next.stderr
index 69328e20583..7e2b05618c4 100644
--- a/tests/ui/impl-trait/two_tait_defining_each_other2.next.stderr
+++ b/tests/ui/impl-trait/two_tait_defining_each_other2.next.stderr
@@ -1,8 +1,8 @@
-error[E0284]: type annotations needed: cannot satisfy `A == B`
-  --> $DIR/two_tait_defining_each_other2.rs:11:5
+error[E0284]: type annotations needed: cannot satisfy `_ == A`
+  --> $DIR/two_tait_defining_each_other2.rs:10:8
    |
-LL |     x // B's hidden type is A (opaquely)
-   |     ^ cannot satisfy `A == B`
+LL | fn muh(x: A) -> B {
+   |        ^ cannot satisfy `_ == A`
 
 error: aborting due to 1 previous error
 
diff --git a/tests/ui/impl-trait/two_tait_defining_each_other2.rs b/tests/ui/impl-trait/two_tait_defining_each_other2.rs
index 229a7411951..faa1fed22d3 100644
--- a/tests/ui/impl-trait/two_tait_defining_each_other2.rs
+++ b/tests/ui/impl-trait/two_tait_defining_each_other2.rs
@@ -8,9 +8,9 @@ type B = impl Foo;
 trait Foo {}
 
 fn muh(x: A) -> B {
+    //[next]~^ ERROR type annotations needed: cannot satisfy `_ == A`
     x // B's hidden type is A (opaquely)
     //[current]~^ ERROR opaque type's hidden type cannot be another opaque type
-    //[next]~^^ ERROR type annotations needed: cannot satisfy `A == B`
 }
 
 struct Bar;
diff --git a/tests/ui/traits/next-solver/assembly/candidates-equal-modulo-norm-1.rs b/tests/ui/traits/next-solver/assembly/candidates-equal-modulo-norm-1.rs
new file mode 100644
index 00000000000..3ac1639cfba
--- /dev/null
+++ b/tests/ui/traits/next-solver/assembly/candidates-equal-modulo-norm-1.rs
@@ -0,0 +1,26 @@
+//@ compile-flags: -Znext-solver
+//@ check-pass
+
+// Regression test for trait-system-refactor-initiative#84.
+//
+// We try to infer `T::Rigid: Into<?0>` and have 2 candidates from where-clauses:
+//
+// - `Into<String>`
+// - `Into<<T::Rigid as Elaborate>::Assoc>`
+//
+// This causes ambiguity unless we normalize the alias in the second candidate
+// to detect that they actually result in the same constraints.
+trait Trait {
+    type Rigid: Elaborate<Assoc = String> + Into<String> + Default;
+}
+
+trait Elaborate: Into<Self::Assoc> {
+    type Assoc;
+}
+
+fn test<T: Trait>() {
+    let rigid: T::Rigid = Default::default();
+    drop(rigid.into());
+}
+
+fn main() {}
diff --git a/tests/ui/traits/next-solver/assembly/candidates-equal-modulo-norm-2.rs b/tests/ui/traits/next-solver/assembly/candidates-equal-modulo-norm-2.rs
new file mode 100644
index 00000000000..a1b736184f1
--- /dev/null
+++ b/tests/ui/traits/next-solver/assembly/candidates-equal-modulo-norm-2.rs
@@ -0,0 +1,26 @@
+//@ compile-flags: -Znext-solver
+//@ check-pass
+
+// Regression test for trait-system-refactor-initiative#86. This previously
+// failed with ambiguity due to multiple candidates with different
+// normalization.
+
+trait Bar {
+    type Item;
+    type Assoc: AsRef<[Self::Item]>;
+}
+
+struct Foo<T: Bar> {
+    t: <T as Bar>::Assoc,
+}
+
+impl<T: Bar<Item = u32>> Foo<T>
+where
+    <T as Bar>::Assoc: AsRef<[u32]>,
+{
+    fn hello(&self) {
+        println!("{}", self.t.as_ref().len());
+    }
+}
+
+fn main() {}
diff --git a/tests/ui/traits/next-solver/coherence/trait_ref_is_knowable-norm-overflow.rs b/tests/ui/traits/next-solver/coherence/trait_ref_is_knowable-norm-overflow.rs
index 66409f171e6..3238f028362 100644
--- a/tests/ui/traits/next-solver/coherence/trait_ref_is_knowable-norm-overflow.rs
+++ b/tests/ui/traits/next-solver/coherence/trait_ref_is_knowable-norm-overflow.rs
@@ -16,6 +16,6 @@ trait Trait {}
 impl<T: Copy> Trait for T {}
 struct LocalTy;
 impl Trait for <LocalTy as Overflow>::Assoc {}
-//~^ ERROR conflicting implementations of trait `Trait` for type `<LocalTy as Overflow>::Assoc`
+//~^ ERROR conflicting implementations of trait `Trait`
 
 fn main() {}
diff --git a/tests/ui/traits/next-solver/coherence/trait_ref_is_knowable-norm-overflow.stderr b/tests/ui/traits/next-solver/coherence/trait_ref_is_knowable-norm-overflow.stderr
index 583945723d5..fc145b81196 100644
--- a/tests/ui/traits/next-solver/coherence/trait_ref_is_knowable-norm-overflow.stderr
+++ b/tests/ui/traits/next-solver/coherence/trait_ref_is_knowable-norm-overflow.stderr
@@ -1,11 +1,11 @@
-error[E0119]: conflicting implementations of trait `Trait` for type `<LocalTy as Overflow>::Assoc`
+error[E0119]: conflicting implementations of trait `Trait`
   --> $DIR/trait_ref_is_knowable-norm-overflow.rs:18:1
    |
 LL | impl<T: Copy> Trait for T {}
    | ------------------------- first implementation here
 LL | struct LocalTy;
 LL | impl Trait for <LocalTy as Overflow>::Assoc {}
-   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ conflicting implementation for `<LocalTy as Overflow>::Assoc`
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ conflicting implementation
 
 error[E0275]: overflow evaluating the requirement `<T as Overflow>::Assoc: Sized`
   --> $DIR/trait_ref_is_knowable-norm-overflow.rs:10:18
diff --git a/tests/ui/traits/next-solver/coherence/trait_ref_is_knowable-normalization-3.rs b/tests/ui/traits/next-solver/coherence/trait_ref_is_knowable-normalization-3.rs
index 98fd98ac282..70d8d74d5ea 100644
--- a/tests/ui/traits/next-solver/coherence/trait_ref_is_knowable-normalization-3.rs
+++ b/tests/ui/traits/next-solver/coherence/trait_ref_is_knowable-normalization-3.rs
@@ -9,7 +9,7 @@ impl<T> Id for T {
 }
 
 
-// Coherence should be able to reason that `(): PartialEq<<T as Id>::Assoc>>`
+// Coherence should be able to reason that `(): PartialEq<<LocalTy as Id>::Assoc>>`
 // does not hold.
 //
 // See https://github.com/rust-lang/trait-system-refactor-initiative/issues/51
diff --git a/tests/ui/traits/next-solver/generalize/generalize-proj-new-universe-index-2.rs b/tests/ui/traits/next-solver/generalize/generalize-proj-new-universe-index-2.rs
index 4de5eda3a79..91793e59f1a 100644
--- a/tests/ui/traits/next-solver/generalize/generalize-proj-new-universe-index-2.rs
+++ b/tests/ui/traits/next-solver/generalize/generalize-proj-new-universe-index-2.rs
@@ -1,8 +1,8 @@
 //@ compile-flags: -Znext-solver
-//@ known-bug: trait-system-refactor-initiative#60
+//@ check-pass
 
 // Generalizing a projection containing an inference variable
-// which cannot be named by the `root_vid` can result in ambiguity.
+// which cannot be named by the `root_vid` previously resulted in ambiguity.
 //
 // Because we do not decrement the universe index when exiting a forall,
 // this can cause unexpected failures.
diff --git a/tests/ui/traits/next-solver/generalize/generalize-proj-new-universe-index-2.stderr b/tests/ui/traits/next-solver/generalize/generalize-proj-new-universe-index-2.stderr
deleted file mode 100644
index 4548ab1e297..00000000000
--- a/tests/ui/traits/next-solver/generalize/generalize-proj-new-universe-index-2.stderr
+++ /dev/null
@@ -1,19 +0,0 @@
-error[E0284]: type annotations needed
-  --> $DIR/generalize-proj-new-universe-index-2.rs:74:5
-   |
-LL |     bound::<<Rigid as IdHigherRankedBound>::Assoc, <Wrapper<Leaf> as Id>::Assoc, _>()
-   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ cannot infer type of the type parameter `V` declared on the function `bound`
-   |
-   = note: cannot satisfy `<<Rigid as IdHigherRankedBound>::Assoc as WithAssoc<<Wrapper<Leaf> as Id>::Assoc>>::Assoc == _`
-note: required by a bound in `bound`
-  --> $DIR/generalize-proj-new-universe-index-2.rs:69:21
-   |
-LL | fn bound<T: ?Sized, U: ?Sized, V: ?Sized>()
-   |    ----- required by a bound in this function
-LL | where
-LL |     T: WithAssoc<U, Assoc = V>,
-   |                     ^^^^^^^^^ required by this bound in `bound`
-
-error: aborting due to 1 previous error
-
-For more information about this error, try `rustc --explain E0284`.
diff --git a/tests/ui/traits/next-solver/generalize/instantiate-canonical-occurs-check-failure.rs b/tests/ui/traits/next-solver/generalize/instantiate-canonical-occurs-check-failure.rs
new file mode 100644
index 00000000000..37d91fe2c7d
--- /dev/null
+++ b/tests/ui/traits/next-solver/generalize/instantiate-canonical-occurs-check-failure.rs
@@ -0,0 +1,29 @@
+//@ compile-flags: -Znext-solver
+//@ check-pass
+
+// With #119106 generalization now results in `AliasRelate` if the generalized
+// alias contains an inference variable which is not nameable.
+//
+// We previously proved alias-relate after canonicalization, which does not keep track
+// of universe indices, so all inference vars were nameable inside of `AliasRelate`.
+//
+// If we now have a rigid projection containing an unnameable inference variable,
+// we should emit an alias-relate obligation, which constrains the type of `x` to
+// an alias. This caused us to emit yet another equivalent alias-relate obligation
+// when trying to instantiate the query result, resulting in overflow.
+trait Trait<'a> {
+    type Assoc: Default;
+}
+
+fn takes_alias<'a, T: Trait<'a>>(_: <T as Trait<'a>>::Assoc) {}
+
+fn foo<T: for<'a> Trait<'a>>() {
+    let x = Default::default();
+
+    let _incr_universe: for<'a, 'b> fn(&'a (), &'b ()) =
+        (|&(), &()| ()) as for<'a> fn(&'a (), &'a ());
+
+    takes_alias::<T>(x);
+}
+
+fn main() {}
diff --git a/tests/ui/traits/next-solver/generalize/occurs-check-nested-alias.next.stderr b/tests/ui/traits/next-solver/generalize/occurs-check-nested-alias.next.stderr
deleted file mode 100644
index cde925db184..00000000000
--- a/tests/ui/traits/next-solver/generalize/occurs-check-nested-alias.next.stderr
+++ /dev/null
@@ -1,9 +0,0 @@
-error[E0284]: type annotations needed: cannot satisfy `_ == <<T as Id<_>>::Id as Unnormalizable>::Assoc`
-  --> $DIR/occurs-check-nested-alias.rs:36:9
-   |
-LL |     x = y;
-   |         ^ cannot satisfy `_ == <<T as Id<_>>::Id as Unnormalizable>::Assoc`
-
-error: aborting due to 1 previous error
-
-For more information about this error, try `rustc --explain E0284`.
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 78fbe441527..536e7e97c40 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
@@ -1,10 +1,8 @@
 //@ revisions: old next
-//@[old] check-pass
-
-// Currently always fails to generalize the outer alias, even if it
-// is treated as rigid by `alias-relate`.
 //@[next] compile-flags: -Znext-solver
-//@[next] known-bug: trait-system-refactor-initiative#8
+//@ check-pass
+
+// case 3 of https://github.com/rust-lang/trait-system-refactor-initiative/issues/8.
 #![crate_type = "lib"]
 #![allow(unused)]
 trait Unnormalizable {
@@ -14,8 +12,8 @@ trait Unnormalizable {
 trait Id<T> {
     type Id;
 }
-impl<T, U> Id<T> for U {
-    type Id = U;
+impl<T, U> Id<U> for T {
+    type Id = T;
 }
 
 struct Inv<T>(*mut T);
@@ -24,15 +22,23 @@ fn unconstrained<T>() -> T {
     todo!()
 }
 
-fn create<T, U: Unnormalizable>(
-    x: &U,
-) -> (Inv<T>, Inv<<<U as Id<T>>::Id as Unnormalizable>::Assoc>) {
+fn create<T: Unnormalizable, U>(
+    x: &T,
+) -> (Inv<U>, Inv<<<T as Id<U>>::Id as Unnormalizable>::Assoc>) {
     todo!()
 }
 
 fn foo<T: Unnormalizable>() {
-    let q = unconstrained();
-    let (mut x, y) = create::<_, _>(&q);
-    x = y;
-    drop::<T>(q);
+    let t = unconstrained();
+    let (mut u, assoc) = create::<_, _>(&t);
+    u = assoc;
+    // Instantiating `?u` with `<<?t as Id<?u>>::Id as Unnormalizable>::Assoc` would
+    // 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/next-solver/issue-118950-root-region.stderr b/tests/ui/traits/next-solver/issue-118950-root-region.stderr
index e33320ed9e6..931c46c6887 100644
--- a/tests/ui/traits/next-solver/issue-118950-root-region.stderr
+++ b/tests/ui/traits/next-solver/issue-118950-root-region.stderr
@@ -14,13 +14,9 @@ LL | #![feature(lazy_type_alias)]
    = note: `#[warn(incomplete_features)]` on by default
 
 WARN rustc_infer::infer::relate::generalize may incompletely handle alias type: AliasTy { args: [ReBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrNamed(DefId(0:15 ~ issue_118950_root_region[d54f]::{impl#1}::'a), 'a) }), ?1t], def_id: DefId(0:8 ~ issue_118950_root_region[d54f]::Assoc) }
-WARN rustc_infer::infer::relate::generalize may incompletely handle alias type: AliasTy { args: [RePlaceholder(!1_BoundRegion { var: 0, kind: BrNamed(DefId(0:15 ~ issue_118950_root_region[d54f]::{impl#1}::'a), 'a) }), ?1t], def_id: DefId(0:8 ~ issue_118950_root_region[d54f]::Assoc) }
 WARN rustc_infer::infer::relate::generalize may incompletely handle alias type: AliasTy { args: [ReBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrNamed(DefId(0:15 ~ issue_118950_root_region[d54f]::{impl#1}::'a), 'a) }), ?1t], def_id: DefId(0:8 ~ issue_118950_root_region[d54f]::Assoc) }
-WARN rustc_infer::infer::relate::generalize may incompletely handle alias type: AliasTy { args: [RePlaceholder(!1_BoundRegion { var: 0, kind: BrNamed(DefId(0:15 ~ issue_118950_root_region[d54f]::{impl#1}::'a), 'a) }), ?1t], def_id: DefId(0:8 ~ issue_118950_root_region[d54f]::Assoc) }
 WARN rustc_infer::infer::relate::generalize may incompletely handle alias type: AliasTy { args: [ReBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrNamed(DefId(0:15 ~ issue_118950_root_region[d54f]::{impl#1}::'a), 'a) }), ?1t], def_id: DefId(0:8 ~ issue_118950_root_region[d54f]::Assoc) }
-WARN rustc_infer::infer::relate::generalize may incompletely handle alias type: AliasTy { args: [RePlaceholder(!1_BoundRegion { var: 0, kind: BrNamed(DefId(0:15 ~ issue_118950_root_region[d54f]::{impl#1}::'a), 'a) }), ?1t], def_id: DefId(0:8 ~ issue_118950_root_region[d54f]::Assoc) }
 WARN rustc_infer::infer::relate::generalize may incompletely handle alias type: AliasTy { args: [ReBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrNamed(DefId(0:15 ~ issue_118950_root_region[d54f]::{impl#1}::'a), 'a) }), ?1t], def_id: DefId(0:8 ~ issue_118950_root_region[d54f]::Assoc) }
-WARN rustc_infer::infer::relate::generalize may incompletely handle alias type: AliasTy { args: [RePlaceholder(!1_BoundRegion { var: 0, kind: BrNamed(DefId(0:15 ~ issue_118950_root_region[d54f]::{impl#1}::'a), 'a) }), ?1t], def_id: DefId(0:8 ~ issue_118950_root_region[d54f]::Assoc) }
 error[E0119]: conflicting implementations of trait `Overlap<fn(_)>` for type `fn(_)`
   --> $DIR/issue-118950-root-region.rs:19:1
    |