always emit `AliasRelate` goals when relating aliases

Add `StructurallyRelateAliases` to allow instantiating infer vars with rigid aliases.
Change `instantiate_query_response` to be infallible in the new solver. This requires canonicalization to not hide any information used by the query, so weaken
universe compression. It also modifies `term_is_fully_unconstrained` to allow
region inference variables in a higher universe.

21 files changed, 420 insertions, 275 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_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/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..7abe8eb1947 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;
             }
@@ -633,43 +615,46 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
         &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<'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(())
+                if let Some(vid) = t.ty_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 if self
+                        .universe_of_term
+                        .cannot_name(self.infcx.universe_of_ty(vid).unwrap())
+                    {
+                        ControlFlow::Break(())
+                    } else {
+                        ControlFlow::Continue(())
+                    }
                 } else if t.has_non_region_infer() {
                     t.super_visit_with(self)
                 } else {
@@ -678,12 +663,20 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
             }
 
             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(())
+                if let ty::ConstKind::Infer(ty::InferConst::Var(vid)) = c.kind() {
+                    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 if self
+                        .universe_of_term
+                        .cannot_name(self.infcx.universe_of_ct(vid).unwrap())
+                    {
+                        ControlFlow::Break(())
+                    } else {
+                        ControlFlow::Continue(())
+                    }
                 } else if c.has_non_region_infer() {
                     c.super_visit_with(self)
                 } else {
@@ -692,10 +685,12 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
             }
         }
 
-        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 +713,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/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)
         })
     }