diff --git a/compiler/rustc_borrowck/src/type_check/relate_tys.rs b/compiler/rustc_borrowck/src/type_check/relate_tys.rs
index ee0bd13109bb6..a60175d98965e 100644
--- a/compiler/rustc_borrowck/src/type_check/relate_tys.rs
+++ b/compiler/rustc_borrowck/src/type_check/relate_tys.rs
@@ -143,22 +143,6 @@ impl<'tcx> TypeRelatingDelegate<'tcx> for NllTypeRelatingDelegate<'_, '_, 'tcx>
         reg
     }
 
-    #[instrument(skip(self), level = "debug")]
-    fn generalize_existential(&mut self, universe: ty::UniverseIndex) -> ty::Region<'tcx> {
-        let reg = self.type_checker.infcx.next_nll_region_var_in_universe(
-            NllRegionVariableOrigin::Existential { from_forall: false },
-            universe,
-        );
-
-        if cfg!(debug_assertions) {
-            let mut var_to_origin = self.type_checker.infcx.reg_var_to_origin.borrow_mut();
-            let prev = var_to_origin.insert(reg.as_var(), RegionCtxt::Existential(None));
-            assert_eq!(prev, None);
-        }
-
-        reg
-    }
-
     fn push_outlives(
         &mut self,
         sup: ty::Region<'tcx>,
diff --git a/compiler/rustc_infer/src/infer/canonical/query_response.rs b/compiler/rustc_infer/src/infer/canonical/query_response.rs
index 56a45586c9d2e..4539ebf8754c7 100644
--- a/compiler/rustc_infer/src/infer/canonical/query_response.rs
+++ b/compiler/rustc_infer/src/infer/canonical/query_response.rs
@@ -731,13 +731,6 @@ impl<'tcx> TypeRelatingDelegate<'tcx> for QueryTypeRelatingDelegate<'_, 'tcx> {
         ty::Region::new_placeholder(self.infcx.tcx, placeholder)
     }
 
-    fn generalize_existential(&mut self, universe: ty::UniverseIndex) -> ty::Region<'tcx> {
-        self.infcx.next_nll_region_var_in_universe(
-            NllRegionVariableOrigin::Existential { from_forall: false },
-            universe,
-        )
-    }
-
     fn push_outlives(
         &mut self,
         sup: ty::Region<'tcx>,
diff --git a/compiler/rustc_infer/src/infer/relate/combine.rs b/compiler/rustc_infer/src/infer/relate/combine.rs
index 7edfbf02a6829..454de4f978519 100644
--- a/compiler/rustc_infer/src/infer/relate/combine.rs
+++ b/compiler/rustc_infer/src/infer/relate/combine.rs
@@ -23,19 +23,18 @@
 //! this should be correctly updated.
 
 use super::equate::Equate;
-use super::generalize::{self, CombineDelegate, Generalization};
 use super::glb::Glb;
 use super::lub::Lub;
 use super::sub::Sub;
 use crate::infer::{DefineOpaqueTypes, InferCtxt, TypeTrace};
 use crate::traits::{Obligation, PredicateObligations};
 use rustc_middle::infer::canonical::OriginalQueryValues;
-use rustc_middle::infer::unify_key::{ConstVariableValue, EffectVarValue};
+use rustc_middle::infer::unify_key::EffectVarValue;
 use rustc_middle::ty::error::{ExpectedFound, TypeError};
 use rustc_middle::ty::relate::{RelateResult, TypeRelation};
 use rustc_middle::ty::{self, InferConst, ToPredicate, Ty, TyCtxt, TypeVisitableExt};
-use rustc_middle::ty::{AliasRelationDirection, TyVar};
 use rustc_middle::ty::{IntType, UintType};
+use rustc_span::Span;
 
 #[derive(Clone)]
 pub struct CombineFields<'infcx, 'tcx> {
@@ -221,11 +220,11 @@ impl<'tcx> InferCtxt<'tcx> {
             }
 
             (ty::ConstKind::Infer(InferConst::Var(vid)), _) => {
-                return self.unify_const_variable(vid, b);
+                return self.instantiate_const_var(vid, b);
             }
 
             (_, ty::ConstKind::Infer(InferConst::Var(vid))) => {
-                return self.unify_const_variable(vid, a);
+                return self.instantiate_const_var(vid, a);
             }
 
             (ty::ConstKind::Infer(InferConst::EffectVar(vid)), _) => {
@@ -259,69 +258,6 @@ impl<'tcx> InferCtxt<'tcx> {
         ty::relate::structurally_relate_consts(relation, a, b)
     }
 
-    /// Unifies the const variable `target_vid` with the given constant.
-    ///
-    /// This also tests if the given const `ct` contains an inference variable which was previously
-    /// unioned with `target_vid`. If this is the case, inferring `target_vid` to `ct`
-    /// would result in an infinite type as we continuously replace an inference variable
-    /// in `ct` with `ct` itself.
-    ///
-    /// This is especially important as unevaluated consts use their parents generics.
-    /// They therefore often contain unused args, making these errors far more likely.
-    ///
-    /// A good example of this is the following:
-    ///
-    /// ```compile_fail,E0308
-    /// #![feature(generic_const_exprs)]
-    ///
-    /// fn bind<const N: usize>(value: [u8; N]) -> [u8; 3 + 4] {
-    ///     todo!()
-    /// }
-    ///
-    /// fn main() {
-    ///     let mut arr = Default::default();
-    ///     arr = bind(arr);
-    /// }
-    /// ```
-    ///
-    /// Here `3 + 4` ends up as `ConstKind::Unevaluated` which uses the generics
-    /// of `fn bind` (meaning that its args contain `N`).
-    ///
-    /// `bind(arr)` now infers that the type of `arr` must be `[u8; N]`.
-    /// The assignment `arr = bind(arr)` now tries to equate `N` with `3 + 4`.
-    ///
-    /// As `3 + 4` contains `N` in its args, this must not succeed.
-    ///
-    /// See `tests/ui/const-generics/occurs-check/` for more examples where this is relevant.
-    #[instrument(level = "debug", skip(self))]
-    fn unify_const_variable(
-        &self,
-        target_vid: ty::ConstVid,
-        ct: ty::Const<'tcx>,
-    ) -> RelateResult<'tcx, ty::Const<'tcx>> {
-        let span = match self.inner.borrow_mut().const_unification_table().probe_value(target_vid) {
-            ConstVariableValue::Known { value } => {
-                bug!("instantiating a known const var: {target_vid:?} {value} {ct}")
-            }
-            ConstVariableValue::Unknown { origin, universe: _ } => origin.span,
-        };
-        // FIXME(generic_const_exprs): Occurs check failures for unevaluated
-        // constants and generic expressions are not yet handled correctly.
-        let Generalization { value_may_be_infer: value, needs_wf: _ } = generalize::generalize(
-            self,
-            &mut CombineDelegate { infcx: self, span },
-            ct,
-            target_vid,
-            ty::Variance::Invariant,
-        )?;
-
-        self.inner
-            .borrow_mut()
-            .const_unification_table()
-            .union_value(target_vid, ConstVariableValue::Known { value });
-        Ok(value)
-    }
-
     fn unify_integral_variable(
         &self,
         vid_is_expected: bool,
@@ -383,131 +319,6 @@ impl<'infcx, 'tcx> CombineFields<'infcx, 'tcx> {
         Glb::new(self, a_is_expected)
     }
 
-    /// Here, `dir` is either `EqTo`, `SubtypeOf`, or `SupertypeOf`.
-    /// The idea is that we should ensure that the type `a_ty` is equal
-    /// to, a subtype of, or a supertype of (respectively) the type
-    /// to which `b_vid` is bound.
-    ///
-    /// Since `b_vid` has not yet been instantiated with a type, we
-    /// will first instantiate `b_vid` with a *generalized* version
-    /// of `a_ty`. Generalization introduces other inference
-    /// variables wherever subtyping could occur.
-    #[instrument(skip(self), level = "debug")]
-    pub fn instantiate(
-        &mut self,
-        a_ty: Ty<'tcx>,
-        ambient_variance: ty::Variance,
-        b_vid: ty::TyVid,
-        a_is_expected: bool,
-    ) -> RelateResult<'tcx, ()> {
-        // Get the actual variable that b_vid has been inferred to
-        debug_assert!(self.infcx.inner.borrow_mut().type_variables().probe(b_vid).is_unknown());
-
-        // Generalize type of `a_ty` appropriately depending on the
-        // direction. As an example, assume:
-        //
-        // - `a_ty == &'x ?1`, where `'x` is some free region and `?1` is an
-        //   inference variable,
-        // - and `dir` == `SubtypeOf`.
-        //
-        // Then the generalized form `b_ty` would be `&'?2 ?3`, where
-        // `'?2` and `?3` are fresh region/type inference
-        // variables. (Down below, we will relate `a_ty <: b_ty`,
-        // adding constraints like `'x: '?2` and `?1 <: ?3`.)
-        let Generalization { value_may_be_infer: b_ty, needs_wf } = generalize::generalize(
-            self.infcx,
-            &mut CombineDelegate { infcx: self.infcx, span: self.trace.span() },
-            a_ty,
-            b_vid,
-            ambient_variance,
-        )?;
-
-        // Constrain `b_vid` to the generalized type `b_ty`.
-        if let &ty::Infer(TyVar(b_ty_vid)) = b_ty.kind() {
-            self.infcx.inner.borrow_mut().type_variables().equate(b_vid, b_ty_vid);
-        } else {
-            self.infcx.inner.borrow_mut().type_variables().instantiate(b_vid, b_ty);
-        }
-
-        if needs_wf {
-            self.obligations.push(Obligation::new(
-                self.tcx(),
-                self.trace.cause.clone(),
-                self.param_env,
-                ty::Binder::dummy(ty::PredicateKind::Clause(ty::ClauseKind::WellFormed(
-                    b_ty.into(),
-                ))),
-            ));
-        }
-
-        // Finally, relate `b_ty` to `a_ty`, as described in previous comment.
-        //
-        // FIXME(#16847): This code is non-ideal because all these subtype
-        // relations wind up attributed to the same spans. We need
-        // to associate causes/spans with each of the relations in
-        // the stack to get this right.
-        if b_ty.is_ty_var() {
-            // This happens for cases like `<?0 as Trait>::Assoc == ?0`.
-            // We can't instantiate `?0` here as that would result in a
-            // cyclic type. We instead delay the unification in case
-            // the alias can be normalized to something which does not
-            // mention `?0`.
-            if self.infcx.next_trait_solver() {
-                let (lhs, rhs, direction) = match ambient_variance {
-                    ty::Variance::Invariant => {
-                        (a_ty.into(), b_ty.into(), AliasRelationDirection::Equate)
-                    }
-                    ty::Variance::Covariant => {
-                        (a_ty.into(), b_ty.into(), AliasRelationDirection::Subtype)
-                    }
-                    ty::Variance::Contravariant => {
-                        (b_ty.into(), a_ty.into(), AliasRelationDirection::Subtype)
-                    }
-                    ty::Variance::Bivariant => unreachable!("bivariant generalization"),
-                };
-                self.obligations.push(Obligation::new(
-                    self.tcx(),
-                    self.trace.cause.clone(),
-                    self.param_env,
-                    ty::PredicateKind::AliasRelate(lhs, rhs, direction),
-                ));
-            } else {
-                match a_ty.kind() {
-                    &ty::Alias(ty::Projection, data) => {
-                        // FIXME: This does not handle subtyping correctly, we could
-                        // instead create a new inference variable for `a_ty`, emitting
-                        // `Projection(a_ty, a_infer)` and `a_infer <: b_ty`.
-                        self.obligations.push(Obligation::new(
-                            self.tcx(),
-                            self.trace.cause.clone(),
-                            self.param_env,
-                            ty::ProjectionPredicate { projection_ty: data, term: b_ty.into() },
-                        ))
-                    }
-                    // The old solver only accepts projection predicates for associated types.
-                    ty::Alias(ty::Inherent | ty::Weak | ty::Opaque, _) => {
-                        return Err(TypeError::CyclicTy(a_ty));
-                    }
-                    _ => bug!("generalizated `{a_ty:?} to infer, not an alias"),
-                }
-            }
-        } else {
-            match ambient_variance {
-                ty::Variance::Invariant => self.equate(a_is_expected).relate(a_ty, b_ty),
-                ty::Variance::Covariant => self.sub(a_is_expected).relate(a_ty, b_ty),
-                ty::Variance::Contravariant => self.sub(a_is_expected).relate_with_variance(
-                    ty::Contravariant,
-                    ty::VarianceDiagInfo::default(),
-                    a_ty,
-                    b_ty,
-                ),
-                ty::Variance::Bivariant => unreachable!("bivariant generalization"),
-            }?;
-        }
-
-        Ok(())
-    }
-
     pub fn register_obligations(&mut self, obligations: PredicateObligations<'tcx>) {
         self.obligations.extend(obligations);
     }
@@ -520,6 +331,8 @@ impl<'infcx, 'tcx> CombineFields<'infcx, 'tcx> {
 }
 
 pub trait ObligationEmittingRelation<'tcx>: TypeRelation<'tcx> {
+    fn span(&self) -> Span;
+
     fn param_env(&self) -> ty::ParamEnv<'tcx>;
 
     /// Register obligations that must hold in order for this relation to hold
diff --git a/compiler/rustc_infer/src/infer/relate/equate.rs b/compiler/rustc_infer/src/infer/relate/equate.rs
index cb62f258373f9..0087add4c725e 100644
--- a/compiler/rustc_infer/src/infer/relate/equate.rs
+++ b/compiler/rustc_infer/src/infer/relate/equate.rs
@@ -8,6 +8,7 @@ use rustc_middle::ty::TyVar;
 use rustc_middle::ty::{self, Ty, TyCtxt, TypeVisitableExt};
 
 use rustc_hir::def_id::DefId;
+use rustc_span::Span;
 
 /// Ensures `a` is made equal to `b`. Returns `a` on success.
 pub struct Equate<'combine, 'infcx, 'tcx> {
@@ -81,12 +82,12 @@ impl<'tcx> TypeRelation<'tcx> for Equate<'_, '_, 'tcx> {
                 infcx.inner.borrow_mut().type_variables().equate(a_id, b_id);
             }
 
-            (&ty::Infer(TyVar(a_id)), _) => {
-                self.fields.instantiate(b, ty::Invariant, a_id, self.a_is_expected)?;
+            (&ty::Infer(TyVar(a_vid)), _) => {
+                infcx.instantiate_ty_var(self, self.a_is_expected, a_vid, ty::Invariant, b)?;
             }
 
-            (_, &ty::Infer(TyVar(b_id))) => {
-                self.fields.instantiate(a, ty::Invariant, b_id, self.a_is_expected)?;
+            (_, &ty::Infer(TyVar(b_vid))) => {
+                infcx.instantiate_ty_var(self, !self.a_is_expected, b_vid, ty::Invariant, a)?;
             }
 
             (
@@ -170,6 +171,10 @@ impl<'tcx> TypeRelation<'tcx> for Equate<'_, '_, 'tcx> {
 }
 
 impl<'tcx> ObligationEmittingRelation<'tcx> for Equate<'_, '_, 'tcx> {
+    fn span(&self) -> Span {
+        self.fields.trace.span()
+    }
+
     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 bc16d613ccbcd..c0cb02916fe8f 100644
--- a/compiler/rustc_infer/src/infer/relate/generalize.rs
+++ b/compiler/rustc_infer/src/infer/relate/generalize.rs
@@ -1,5 +1,7 @@
 use std::mem;
 
+use crate::infer::type_variable::{TypeVariableOrigin, TypeVariableOriginKind, TypeVariableValue};
+use crate::infer::{InferCtxt, ObligationEmittingRelation, RegionVariableOrigin};
 use rustc_data_structures::sso::SsoHashMap;
 use rustc_data_structures::stack::ensure_sufficient_stack;
 use rustc_hir::def_id::DefId;
@@ -7,98 +9,225 @@ use rustc_middle::infer::unify_key::ConstVariableValue;
 use rustc_middle::ty::error::TypeError;
 use rustc_middle::ty::relate::{self, Relate, RelateResult, TypeRelation};
 use rustc_middle::ty::visit::MaxUniverse;
-use rustc_middle::ty::{self, InferConst, Term, Ty, TyCtxt, TypeVisitable, TypeVisitableExt};
+use rustc_middle::ty::{self, Ty, TyCtxt};
+use rustc_middle::ty::{AliasRelationDirection, InferConst, Term, TypeVisitable, TypeVisitableExt};
 use rustc_span::Span;
 
-use crate::infer::nll_relate::TypeRelatingDelegate;
-use crate::infer::type_variable::{TypeVariableOrigin, TypeVariableOriginKind, TypeVariableValue};
-use crate::infer::{InferCtxt, RegionVariableOrigin};
-
-/// Attempts to generalize `term` for the type variable `for_vid`.
-/// This checks for cycles -- that is, whether the type `term`
-/// references `for_vid`.
-pub fn generalize<'tcx, D: GeneralizerDelegate<'tcx>, T: Into<Term<'tcx>> + Relate<'tcx>>(
-    infcx: &InferCtxt<'tcx>,
-    delegate: &mut D,
-    term: T,
-    for_vid: impl Into<ty::TermVid>,
-    ambient_variance: ty::Variance,
-) -> RelateResult<'tcx, Generalization<T>> {
-    let (for_universe, root_vid) = match for_vid.into() {
-        ty::TermVid::Ty(ty_vid) => (
-            infcx.probe_ty_var(ty_vid).unwrap_err(),
-            ty::TermVid::Ty(infcx.inner.borrow_mut().type_variables().sub_root_var(ty_vid)),
-        ),
-        ty::TermVid::Const(ct_vid) => (
-            infcx.probe_const_var(ct_vid).unwrap_err(),
-            ty::TermVid::Const(infcx.inner.borrow_mut().const_unification_table().find(ct_vid).vid),
-        ),
-    };
-
-    let mut generalizer = Generalizer {
-        infcx,
-        delegate,
-        ambient_variance,
-        root_vid,
-        for_universe,
-        root_term: term.into(),
-        in_alias: false,
-        needs_wf: false,
-        cache: Default::default(),
-    };
-
-    assert!(!term.has_escaping_bound_vars());
-    let value_may_be_infer = generalizer.relate(term, term)?;
-    let needs_wf = generalizer.needs_wf;
-    Ok(Generalization { value_may_be_infer, needs_wf })
-}
-
-/// Abstracts the handling of region vars between HIR and MIR/NLL typechecking
-/// in the generalizer code.
-pub trait GeneralizerDelegate<'tcx> {
-    fn forbid_inference_vars() -> bool;
-
-    fn span(&self) -> Span;
+impl<'tcx> InferCtxt<'tcx> {
+    /// The idea is that we should ensure that the type variable `target_vid`
+    /// is equal to, a subtype of, or a supertype of `source_ty`.
+    ///
+    /// For this, we will instantiate `target_vid` with a *generalized* version
+    /// of `source_ty`. Generalization introduces other inference variables wherever
+    /// subtyping could occur. This also does the occurs checks, detecting whether
+    /// instantiating `target_vid` would result in a cyclic type. We eagerly error
+    /// in this case.
+    #[instrument(skip(self, relation, target_is_expected), level = "debug")]
+    pub(super) fn instantiate_ty_var<R: ObligationEmittingRelation<'tcx>>(
+        &self,
+        relation: &mut R,
+        target_is_expected: bool,
+        target_vid: ty::TyVid,
+        ambient_variance: ty::Variance,
+        source_ty: Ty<'tcx>,
+    ) -> RelateResult<'tcx, ()> {
+        debug_assert!(self.inner.borrow_mut().type_variables().probe(target_vid).is_unknown());
+
+        // Generalize `source_ty` depending on the current variance. As an example, assume
+        // `?target <: &'x ?1`, where `'x` is some free region and `?1` is an inference
+        // variable.
+        //
+        // Then the `generalized_ty` would be `&'?2 ?3`, where `'?2` and `?3` are fresh
+        // 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, ambient_variance, source_ty)?;
+
+        // Constrain `b_vid` to the generalized type `generalized_ty`.
+        if let &ty::Infer(ty::TyVar(generalized_vid)) = generalized_ty.kind() {
+            self.inner.borrow_mut().type_variables().equate(target_vid, generalized_vid);
+        } else {
+            self.inner.borrow_mut().type_variables().instantiate(target_vid, generalized_ty);
+        }
 
-    fn generalize_region(&mut self, universe: ty::UniverseIndex) -> ty::Region<'tcx>;
-}
+        // See the comment on `Generalization::has_unconstrained_ty_var`.
+        if has_unconstrained_ty_var {
+            relation.register_predicates([ty::ClauseKind::WellFormed(generalized_ty.into())]);
+        }
 
-pub struct CombineDelegate<'cx, 'tcx> {
-    pub infcx: &'cx InferCtxt<'tcx>,
-    pub span: Span,
-}
+        // Finally, relate `generalized_ty` to `source_ty`, as described in previous comment.
+        //
+        // FIXME(#16847): This code is non-ideal because all these subtype
+        // relations wind up attributed to the same spans. We need
+        // to associate causes/spans with each of the relations in
+        // the stack to get this right.
+        if generalized_ty.is_ty_var() {
+            // This happens for cases like `<?0 as Trait>::Assoc == ?0`.
+            // We can't instantiate `?0` here as that would result in a
+            // cyclic type. We instead delay the unification in case
+            // the alias can be normalized to something which does not
+            // mention `?0`.
+            if self.next_trait_solver() {
+                let (lhs, rhs, direction) = match ambient_variance {
+                    ty::Variance::Invariant => {
+                        (generalized_ty.into(), source_ty.into(), AliasRelationDirection::Equate)
+                    }
+                    ty::Variance::Covariant => {
+                        (generalized_ty.into(), source_ty.into(), AliasRelationDirection::Subtype)
+                    }
+                    ty::Variance::Contravariant => {
+                        (source_ty.into(), generalized_ty.into(), AliasRelationDirection::Subtype)
+                    }
+                    ty::Variance::Bivariant => unreachable!("bivariant generalization"),
+                };
 
-impl<'tcx> GeneralizerDelegate<'tcx> for CombineDelegate<'_, 'tcx> {
-    fn forbid_inference_vars() -> bool {
-        false
-    }
+                relation.register_predicates([ty::PredicateKind::AliasRelate(lhs, rhs, direction)]);
+            } else {
+                match source_ty.kind() {
+                    &ty::Alias(ty::Projection, data) => {
+                        // FIXME: This does not handle subtyping correctly, we could
+                        // instead create a new inference variable `?normalized_source`, emitting
+                        // `Projection(normalized_source, ?ty_normalized)` and `?normalized_source <: generalized_ty`.
+                        relation.register_predicates([ty::ProjectionPredicate {
+                            projection_ty: data,
+                            term: generalized_ty.into(),
+                        }]);
+                    }
+                    // The old solver only accepts projection predicates for associated types.
+                    ty::Alias(ty::Inherent | ty::Weak | ty::Opaque, _) => {
+                        return Err(TypeError::CyclicTy(source_ty));
+                    }
+                    _ => bug!("generalized `{source_ty:?} to infer, not an alias"),
+                }
+            }
+        } else {
+            // HACK: make sure that we `a_is_expected` continues to be
+            // correct when relating the generalized type with the source.
+            if target_is_expected == relation.a_is_expected() {
+                relation.relate_with_variance(
+                    ambient_variance,
+                    ty::VarianceDiagInfo::default(),
+                    generalized_ty,
+                    source_ty,
+                )?;
+            } else {
+                relation.relate_with_variance(
+                    ambient_variance.xform(ty::Contravariant),
+                    ty::VarianceDiagInfo::default(),
+                    source_ty,
+                    generalized_ty,
+                )?;
+            }
+        }
 
-    fn span(&self) -> Span {
-        self.span
+        Ok(())
     }
 
-    fn generalize_region(&mut self, universe: ty::UniverseIndex) -> ty::Region<'tcx> {
-        // FIXME: This is non-ideal because we don't give a
-        // very descriptive origin for this region variable.
-        self.infcx
-            .next_region_var_in_universe(RegionVariableOrigin::MiscVariable(self.span), universe)
-    }
-}
+    /// Instantiates the const variable `target_vid` with the given constant.
+    ///
+    /// This also tests if the given const `ct` contains an inference variable which was previously
+    /// unioned with `target_vid`. If this is the case, inferring `target_vid` to `ct`
+    /// would result in an infinite type as we continuously replace an inference variable
+    /// in `ct` with `ct` itself.
+    ///
+    /// This is especially important as unevaluated consts use their parents generics.
+    /// They therefore often contain unused args, making these errors far more likely.
+    ///
+    /// A good example of this is the following:
+    ///
+    /// ```compile_fail,E0308
+    /// #![feature(generic_const_exprs)]
+    ///
+    /// fn bind<const N: usize>(value: [u8; N]) -> [u8; 3 + 4] {
+    ///     todo!()
+    /// }
+    ///
+    /// fn main() {
+    ///     let mut arr = Default::default();
+    ///     arr = bind(arr);
+    /// }
+    /// ```
+    ///
+    /// Here `3 + 4` ends up as `ConstKind::Unevaluated` which uses the generics
+    /// of `fn bind` (meaning that its args contain `N`).
+    ///
+    /// `bind(arr)` now infers that the type of `arr` must be `[u8; N]`.
+    /// The assignment `arr = bind(arr)` now tries to equate `N` with `3 + 4`.
+    ///
+    /// As `3 + 4` contains `N` in its args, this must not succeed.
+    ///
+    /// See `tests/ui/const-generics/occurs-check/` for more examples where this is relevant.
+    #[instrument(level = "debug", skip(self))]
+    pub(super) fn instantiate_const_var(
+        &self,
+        target_vid: ty::ConstVid,
+        source_ct: ty::Const<'tcx>,
+    ) -> RelateResult<'tcx, ty::Const<'tcx>> {
+        let span = match self.inner.borrow_mut().const_unification_table().probe_value(target_vid) {
+            ConstVariableValue::Known { value } => {
+                bug!("instantiating a known const var: {target_vid:?} {value} {source_ct}")
+            }
+            ConstVariableValue::Unknown { origin, universe: _ } => origin.span,
+        };
+        // 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(span, target_vid, ty::Variance::Invariant, source_ct)?;
+
+        debug_assert!(!generalized_ct.is_ct_infer());
+        if has_unconstrained_ty_var {
+            span_bug!(span, "unconstrained ty var when generalizing `{source_ct:?}`");
+        }
 
-impl<'tcx, T> GeneralizerDelegate<'tcx> for T
-where
-    T: TypeRelatingDelegate<'tcx>,
-{
-    fn forbid_inference_vars() -> bool {
-        <Self as TypeRelatingDelegate<'tcx>>::forbid_inference_vars()
-    }
+        self.inner
+            .borrow_mut()
+            .const_unification_table()
+            .union_value(target_vid, ConstVariableValue::Known { value: generalized_ct });
 
-    fn span(&self) -> Span {
-        <Self as TypeRelatingDelegate<'tcx>>::span(&self)
+        // FIXME(generic_const_exprs): We have to make sure we actually equate
+        // `generalized_ct` and `source_ct` here.
+        Ok(generalized_ct)
     }
 
-    fn generalize_region(&mut self, universe: ty::UniverseIndex) -> ty::Region<'tcx> {
-        <Self as TypeRelatingDelegate<'tcx>>::generalize_existential(self, universe)
+    /// Attempts to generalize `source_term` for the type variable `target_vid`.
+    /// This checks for cycles -- that is, whether `source_term` references `target_vid`.
+    fn generalize<T: Into<Term<'tcx>> + Relate<'tcx>>(
+        &self,
+        span: Span,
+        target_vid: impl Into<ty::TermVid>,
+        ambient_variance: ty::Variance,
+        source_term: T,
+    ) -> RelateResult<'tcx, Generalization<T>> {
+        assert!(!source_term.has_escaping_bound_vars());
+        let (for_universe, root_vid) = match target_vid.into() {
+            ty::TermVid::Ty(ty_vid) => (
+                self.probe_ty_var(ty_vid).unwrap_err(),
+                ty::TermVid::Ty(self.inner.borrow_mut().type_variables().sub_root_var(ty_vid)),
+            ),
+            ty::TermVid::Const(ct_vid) => (
+                self.probe_const_var(ct_vid).unwrap_err(),
+                ty::TermVid::Const(
+                    self.inner.borrow_mut().const_unification_table().find(ct_vid).vid,
+                ),
+            ),
+        };
+
+        let mut generalizer = Generalizer {
+            infcx: self,
+            span,
+            root_vid,
+            for_universe,
+            ambient_variance,
+            root_term: source_term.into(),
+            in_alias: false,
+            has_unconstrained_ty_var: false,
+            cache: Default::default(),
+        };
+
+        let value_may_be_infer = generalizer.relate(source_term, source_term)?;
+        let has_unconstrained_ty_var = generalizer.has_unconstrained_ty_var;
+        Ok(Generalization { value_may_be_infer, has_unconstrained_ty_var })
     }
 }
 
@@ -115,18 +244,10 @@ where
 /// establishes `'0: 'x` as a constraint.
 ///
 /// [blog post]: https://is.gd/0hKvIr
-struct Generalizer<'me, 'tcx, D> {
+struct Generalizer<'me, 'tcx> {
     infcx: &'me InferCtxt<'tcx>,
 
-    /// This is used to abstract the behaviors of the three previous
-    /// generalizer-like implementations (`Generalizer`, `TypeGeneralizer`,
-    /// and `ConstInferUnifier`). See [`GeneralizerDelegate`] for more
-    /// information.
-    delegate: &'me mut D,
-
-    /// After we generalize this type, we are going to relate it to
-    /// some other type. What will be the variance at this point?
-    ambient_variance: ty::Variance,
+    span: Span,
 
     /// The vid of the type variable that is in the process of being
     /// instantiated. If we find this within the value we are folding,
@@ -138,6 +259,10 @@ struct Generalizer<'me, 'tcx, D> {
     /// we reject the relation.
     for_universe: ty::UniverseIndex,
 
+    /// After we generalize this type, we are going to relate it to
+    /// some other type. What will be the variance at this point?
+    ambient_variance: ty::Variance,
+
     /// The root term (const or type) we're generalizing. Used for cycle errors.
     root_term: Term<'tcx>,
 
@@ -150,11 +275,11 @@ struct Generalizer<'me, 'tcx, D> {
     /// hold by either normalizing the outer or the inner associated type.
     in_alias: bool,
 
-    /// See the field `needs_wf` in `Generalization`.
-    needs_wf: bool,
+    /// See the field `has_unconstrained_ty_var` in `Generalization`.
+    has_unconstrained_ty_var: bool,
 }
 
-impl<'tcx, D> Generalizer<'_, 'tcx, D> {
+impl<'tcx> Generalizer<'_, 'tcx> {
     /// Create an error that corresponds to the term kind in `root_term`
     fn cyclic_term_error(&self) -> TypeError<'tcx> {
         match self.root_term.unpack() {
@@ -164,10 +289,7 @@ impl<'tcx, D> Generalizer<'_, 'tcx, D> {
     }
 }
 
-impl<'tcx, D> TypeRelation<'tcx> for Generalizer<'_, 'tcx, D>
-where
-    D: GeneralizerDelegate<'tcx>,
-{
+impl<'tcx> TypeRelation<'tcx> for Generalizer<'_, 'tcx> {
     fn tcx(&self) -> TyCtxt<'tcx> {
         self.infcx.tcx
     }
@@ -236,12 +358,6 @@ where
         // subtyping. This is basically our "occurs check", preventing
         // us from creating infinitely sized types.
         let g = match *t.kind() {
-            ty::Infer(ty::TyVar(_)) | ty::Infer(ty::IntVar(_)) | ty::Infer(ty::FloatVar(_))
-                if D::forbid_inference_vars() =>
-            {
-                bug!("unexpected inference variable encountered in NLL generalization: {t}");
-            }
-
             ty::Infer(ty::FreshTy(_) | ty::FreshIntTy(_) | ty::FreshFloatTy(_)) => {
                 bug!("unexpected infer type: {t}")
             }
@@ -272,11 +388,10 @@ where
                                     }
                                 }
 
-                                // Bivariant: make a fresh var, but we
-                                // may need a WF predicate. See
-                                // comment on `needs_wf` field for
-                                // more info.
-                                ty::Bivariant => self.needs_wf = true,
+                                // Bivariant: make a fresh var, but remember that
+                                // it is unconstrained. See the comment in
+                                // `Generalization`.
+                                ty::Bivariant => self.has_unconstrained_ty_var = true,
 
                                 // Co/contravariant: this will be
                                 // sufficiently constrained later on.
@@ -345,7 +460,7 @@ where
                             Ok(self.infcx.next_ty_var_in_universe(
                                 TypeVariableOrigin {
                                     kind: TypeVariableOriginKind::MiscVariable,
-                                    span: self.delegate.span(),
+                                    span: self.span,
                                 },
                                 self.for_universe,
                             ))
@@ -403,7 +518,10 @@ where
             }
         }
 
-        Ok(self.delegate.generalize_region(self.for_universe))
+        Ok(self.infcx.next_region_var_in_universe(
+            RegionVariableOrigin::MiscVariable(self.span),
+            self.for_universe,
+        ))
     }
 
     #[instrument(level = "debug", skip(self, c2), ret)]
@@ -415,9 +533,6 @@ where
         assert_eq!(c, c2); // we are misusing TypeRelation here; both LHS and RHS ought to be ==
 
         match c.kind() {
-            ty::ConstKind::Infer(InferConst::Var(_)) if D::forbid_inference_vars() => {
-                bug!("unexpected inference variable encountered in NLL generalization: {:?}", c);
-            }
             ty::ConstKind::Infer(InferConst::Var(vid)) => {
                 // If root const vids are equal, then `root_vid` and
                 // `vid` are related and we'd be inferring an infinitely
@@ -452,6 +567,9 @@ where
                 }
             }
             ty::ConstKind::Infer(InferConst::EffectVar(_)) => Ok(c),
+            // FIXME: Unevaluated constants are also not rigid, so the current
+            // approach of always relating them structurally is incomplete.
+            //
             // FIXME: remove this branch once `structurally_relate_consts` is fully
             // structural.
             ty::ConstKind::Unevaluated(ty::UnevaluatedConst { def, args }) => {
@@ -511,30 +629,27 @@ pub struct Generalization<T> {
     /// recursion.
     pub value_may_be_infer: T,
 
-    /// If true, then the generalized type may not be well-formed,
-    /// even if the source type is well-formed, so we should add an
-    /// additional check to enforce that it is. This arises in
-    /// particular around 'bivariant' type parameters that are only
-    /// constrained by a where-clause. As an example, imagine a type:
+    /// In general, we do not check whether all types which occur during
+    /// type checking are well-formed. We only check wf of user-provided types
+    /// and when actually using a type, e.g. for method calls.
+    ///
+    /// This means that when subtyping, we may end up with unconstrained
+    /// inference variables if a generalized type has bivariant parameters.
+    /// A parameter may only be bivariant if it is constrained by a projection
+    /// bound in a where-clause. As an example, imagine a type:
     ///
     ///     struct Foo<A, B> where A: Iterator<Item = B> {
     ///         data: A
     ///     }
     ///
-    /// here, `A` will be covariant, but `B` is
-    /// unconstrained. However, whatever it is, for `Foo` to be WF, it
-    /// must be equal to `A::Item`. If we have an input `Foo<?A, ?B>`,
-    /// then after generalization we will wind up with a type like
-    /// `Foo<?C, ?D>`. When we enforce that `Foo<?A, ?B> <: Foo<?C,
-    /// ?D>` (or `>:`), we will wind up with the requirement that `?A
-    /// <: ?C`, but no particular relationship between `?B` and `?D`
-    /// (after all, we do not know the variance of the normalized form
-    /// of `A::Item` with respect to `A`). If we do nothing else, this
-    /// may mean that `?D` goes unconstrained (as in #41677). So, in
-    /// this scenario where we create a new type variable in a
-    /// bivariant context, we set the `needs_wf` flag to true. This
-    /// will force the calling code to check that `WF(Foo<?C, ?D>)`
-    /// holds, which in turn implies that `?C::Item == ?D`. So once
-    /// `?C` is constrained, that should suffice to restrict `?D`.
-    pub needs_wf: bool,
+    /// here, `A` will be covariant, but `B` is unconstrained.
+    ///
+    /// However, whatever it is, for `Foo` to be WF, it must be equal to `A::Item`.
+    /// If we have an input `Foo<?A, ?B>`, then after generalization we will wind
+    /// up with a type like `Foo<?C, ?D>`. When we enforce `Foo<?A, ?B> <: Foo<?C, ?D>`,
+    /// we will wind up with the requirement that `?A <: ?C`, but no particular
+    /// relationship between `?B` and `?D` (after all, these types may be completely
+    /// different). If we do nothing else, this may mean that `?D` goes unconstrained
+    /// (as in #41677). To avoid this we emit a `WellFormed` obligation in these cases.
+    pub has_unconstrained_ty_var: bool,
 }
diff --git a/compiler/rustc_infer/src/infer/relate/glb.rs b/compiler/rustc_infer/src/infer/relate/glb.rs
index aa89124301e8c..6cf5135459967 100644
--- a/compiler/rustc_infer/src/infer/relate/glb.rs
+++ b/compiler/rustc_infer/src/infer/relate/glb.rs
@@ -2,6 +2,7 @@
 
 use rustc_middle::ty::relate::{Relate, RelateResult, TypeRelation};
 use rustc_middle::ty::{self, Ty, TyCtxt, TypeVisitableExt};
+use rustc_span::Span;
 
 use super::combine::{CombineFields, ObligationEmittingRelation};
 use super::lattice::{self, LatticeDir};
@@ -134,6 +135,10 @@ impl<'combine, 'infcx, 'tcx> LatticeDir<'infcx, 'tcx> for Glb<'combine, 'infcx,
 }
 
 impl<'tcx> ObligationEmittingRelation<'tcx> for Glb<'_, '_, 'tcx> {
+    fn span(&self) -> Span {
+        self.fields.trace.span()
+    }
+
     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 87d777530c866..5b4f80fd73a02 100644
--- a/compiler/rustc_infer/src/infer/relate/lub.rs
+++ b/compiler/rustc_infer/src/infer/relate/lub.rs
@@ -7,6 +7,7 @@ use crate::traits::{ObligationCause, PredicateObligations};
 
 use rustc_middle::ty::relate::{Relate, RelateResult, TypeRelation};
 use rustc_middle::ty::{self, Ty, TyCtxt, TypeVisitableExt};
+use rustc_span::Span;
 
 /// "Least upper bound" (common supertype)
 pub struct Lub<'combine, 'infcx, 'tcx> {
@@ -134,6 +135,10 @@ impl<'combine, 'infcx, 'tcx> LatticeDir<'infcx, 'tcx> for Lub<'combine, 'infcx,
 }
 
 impl<'tcx> ObligationEmittingRelation<'tcx> for Lub<'_, '_, 'tcx> {
+    fn span(&self) -> Span {
+        self.fields.trace.span()
+    }
+
     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 f688c2b74a6d2..26270c77f1ae4 100644
--- a/compiler/rustc_infer/src/infer/relate/mod.rs
+++ b/compiler/rustc_infer/src/infer/relate/mod.rs
@@ -3,7 +3,7 @@
 
 pub(super) mod combine;
 mod equate;
-pub(super) mod generalize;
+mod generalize;
 mod glb;
 mod higher_ranked;
 mod lattice;
diff --git a/compiler/rustc_infer/src/infer/relate/nll.rs b/compiler/rustc_infer/src/infer/relate/nll.rs
index 5e2d2af9b8587..4ba4bd38e9fe4 100644
--- a/compiler/rustc_infer/src/infer/relate/nll.rs
+++ b/compiler/rustc_infer/src/infer/relate/nll.rs
@@ -25,13 +25,11 @@ use rustc_data_structures::fx::FxHashMap;
 use rustc_middle::traits::ObligationCause;
 use rustc_middle::ty::fold::FnMutDelegate;
 use rustc_middle::ty::relate::{Relate, RelateResult, TypeRelation};
-use rustc_middle::ty::visit::TypeVisitableExt;
+use rustc_middle::ty::TypeVisitableExt;
 use rustc_middle::ty::{self, InferConst, Ty, TyCtxt};
 use rustc_span::{Span, Symbol};
-use std::fmt::Debug;
 
 use super::combine::ObligationEmittingRelation;
-use super::generalize::{self, Generalization};
 use crate::infer::InferCtxt;
 use crate::infer::{TypeVariableOrigin, TypeVariableOriginKind};
 use crate::traits::{Obligation, PredicateObligations};
@@ -99,15 +97,6 @@ pub trait TypeRelatingDelegate<'tcx> {
     /// placeholder region.
     fn next_placeholder_region(&mut self, placeholder: ty::PlaceholderRegion) -> ty::Region<'tcx>;
 
-    /// Creates a new existential region in the given universe. This
-    /// is used when handling subtyping and type variables -- if we
-    /// have that `?X <: Foo<'a>`, for example, we would instantiate
-    /// `?X` with a type like `Foo<'?0>` where `'?0` is a fresh
-    /// existential variable created by this function. We would then
-    /// relate `Foo<'?0>` with `Foo<'a>` (and probably add an outlives
-    /// relation stating that `'?0: 'a`).
-    fn generalize_existential(&mut self, universe: ty::UniverseIndex) -> ty::Region<'tcx>;
-
     /// Enables some optimizations if we do not expect inference variables
     /// in the RHS of the relation.
     fn forbid_inference_vars() -> bool;
@@ -153,112 +142,44 @@ where
         self.delegate.push_outlives(sup, sub, info);
     }
 
-    /// Relate a type inference variable with a value type. This works
-    /// by creating a "generalization" G of the value where all the
-    /// lifetimes are replaced with fresh inference values. This
-    /// generalization G becomes the value of the inference variable,
-    /// and is then related in turn to the value. So e.g. if you had
-    /// `vid = ?0` and `value = &'a u32`, we might first instantiate
-    /// `?0` to a type like `&'0 u32` where `'0` is a fresh variable,
-    /// and then relate `&'0 u32` with `&'a u32` (resulting in
-    /// relations between `'0` and `'a`).
-    ///
-    /// The variable `pair` can be either a `(vid, ty)` or `(ty, vid)`
-    /// -- in other words, it is always an (unresolved) inference
-    /// variable `vid` and a type `ty` that are being related, but the
-    /// vid may appear either as the "a" type or the "b" type,
-    /// depending on where it appears in the tuple. The trait
-    /// `VidValuePair` lets us work with the vid/type while preserving
-    /// the "sidedness" when necessary -- the sidedness is relevant in
-    /// particular for the variance and set of in-scope things.
-    fn relate_ty_var<PAIR: VidValuePair<'tcx>>(
-        &mut self,
-        pair: PAIR,
-    ) -> RelateResult<'tcx, Ty<'tcx>> {
-        debug!("relate_ty_var({:?})", pair);
-
-        let vid = pair.vid();
-        let value_ty = pair.value_ty();
-
-        // FIXME(invariance) -- this logic assumes invariance, but that is wrong.
-        // This only presently applies to chalk integration, as NLL
-        // doesn't permit type variables to appear on both sides (and
-        // doesn't use lazy norm).
-        match *value_ty.kind() {
-            ty::Infer(ty::TyVar(value_vid)) => {
-                // Two type variables: just equate them.
-                self.infcx.inner.borrow_mut().type_variables().equate(vid, value_vid);
-                return Ok(value_ty);
-            }
-
-            _ => (),
-        }
-
-        let generalized_ty = self.generalize(value_ty, vid)?;
-        debug!("relate_ty_var: generalized_ty = {:?}", generalized_ty);
-
-        if D::forbid_inference_vars() {
-            // In NLL, we don't have type inference variables
-            // floating around, so we can do this rather imprecise
-            // variant of the occurs-check.
-            assert!(!generalized_ty.has_non_region_infer());
-        }
-
-        self.infcx.inner.borrow_mut().type_variables().instantiate(vid, generalized_ty);
-
-        // Relate the generalized kind to the original one.
-        let result = pair.relate_generalized_ty(self, generalized_ty);
-
-        debug!("relate_ty_var: complete, result = {:?}", result);
-        result
-    }
-
-    fn generalize(&mut self, ty: Ty<'tcx>, for_vid: ty::TyVid) -> RelateResult<'tcx, Ty<'tcx>> {
-        let Generalization { value_may_be_infer: ty, needs_wf: _ } = generalize::generalize(
-            self.infcx,
-            &mut self.delegate,
-            ty,
-            for_vid,
-            self.ambient_variance,
-        )?;
-
-        if ty.is_ty_var() {
-            span_bug!(self.delegate.span(), "occurs check failure in MIR typeck");
-        }
-        Ok(ty)
-    }
-
-    fn relate_opaques(&mut self, a: Ty<'tcx>, b: Ty<'tcx>) -> RelateResult<'tcx, Ty<'tcx>> {
+    fn relate_opaques(&mut self, a: Ty<'tcx>, b: Ty<'tcx>) -> RelateResult<'tcx, ()> {
+        let infcx = self.infcx;
+        debug_assert!(!infcx.next_trait_solver());
         let (a, b) = if self.a_is_expected() { (a, b) } else { (b, a) };
-        let mut generalize = |ty, ty_is_expected| {
-            let var = self.infcx.next_ty_var_id_in_universe(
+        // `handle_opaque_type` cannot handle subtyping, so to support subtyping
+        // we instead eagerly generalize here. This is a bit of a mess but will go
+        // away once we're using the new solver.
+        let mut enable_subtyping = |ty, ty_is_expected| {
+            let ty_vid = infcx.next_ty_var_id_in_universe(
                 TypeVariableOrigin {
                     kind: TypeVariableOriginKind::MiscVariable,
                     span: self.delegate.span(),
                 },
                 ty::UniverseIndex::ROOT,
             );
-            if ty_is_expected {
-                self.relate_ty_var((ty, var))
+
+            let variance = if ty_is_expected {
+                self.ambient_variance
             } else {
-                self.relate_ty_var((var, ty))
-            }
+                self.ambient_variance.xform(ty::Contravariant)
+            };
+
+            self.infcx.instantiate_ty_var(self, ty_is_expected, ty_vid, variance, ty)?;
+            Ok(infcx.resolve_vars_if_possible(Ty::new_infer(infcx.tcx, ty::TyVar(ty_vid))))
         };
+
         let (a, b) = match (a.kind(), b.kind()) {
-            (&ty::Alias(ty::Opaque, ..), _) => (a, generalize(b, false)?),
-            (_, &ty::Alias(ty::Opaque, ..)) => (generalize(a, true)?, b),
+            (&ty::Alias(ty::Opaque, ..), _) => (a, enable_subtyping(b, false)?),
+            (_, &ty::Alias(ty::Opaque, ..)) => (enable_subtyping(a, true)?, b),
             _ => unreachable!(
                 "expected at least one opaque type in `relate_opaques`, got {a} and {b}."
             ),
         };
         let cause = ObligationCause::dummy_with_span(self.delegate.span());
-        let obligations = self
-            .infcx
-            .handle_opaque_type(a, b, true, &cause, self.delegate.param_env())?
-            .obligations;
+        let obligations =
+            infcx.handle_opaque_type(a, b, true, &cause, self.delegate.param_env())?.obligations;
         self.delegate.register_obligations(obligations);
-        trace!(a = ?a.kind(), b = ?b.kind(), "opaque type instantiated");
-        Ok(a)
+        Ok(())
     }
 
     fn enter_forall<T, U>(
@@ -356,76 +277,6 @@ where
     }
 }
 
-/// When we instantiate an inference variable with a value in
-/// `relate_ty_var`, we always have the pair of a `TyVid` and a `Ty`,
-/// but the ordering may vary (depending on whether the inference
-/// variable was found on the `a` or `b` sides). Therefore, this trait
-/// allows us to factor out common code, while preserving the order
-/// when needed.
-trait VidValuePair<'tcx>: Debug {
-    /// Extract the inference variable (which could be either the
-    /// first or second part of the tuple).
-    fn vid(&self) -> ty::TyVid;
-
-    /// Extract the value it is being related to (which will be the
-    /// opposite part of the tuple from the vid).
-    fn value_ty(&self) -> Ty<'tcx>;
-
-    /// Given a generalized type G that should replace the vid, relate
-    /// G to the value, putting G on whichever side the vid would have
-    /// appeared.
-    fn relate_generalized_ty<D>(
-        &self,
-        relate: &mut TypeRelating<'_, 'tcx, D>,
-        generalized_ty: Ty<'tcx>,
-    ) -> RelateResult<'tcx, Ty<'tcx>>
-    where
-        D: TypeRelatingDelegate<'tcx>;
-}
-
-impl<'tcx> VidValuePair<'tcx> for (ty::TyVid, Ty<'tcx>) {
-    fn vid(&self) -> ty::TyVid {
-        self.0
-    }
-
-    fn value_ty(&self) -> Ty<'tcx> {
-        self.1
-    }
-
-    fn relate_generalized_ty<D>(
-        &self,
-        relate: &mut TypeRelating<'_, 'tcx, D>,
-        generalized_ty: Ty<'tcx>,
-    ) -> RelateResult<'tcx, Ty<'tcx>>
-    where
-        D: TypeRelatingDelegate<'tcx>,
-    {
-        relate.relate(generalized_ty, self.value_ty())
-    }
-}
-
-// In this case, the "vid" is the "b" type.
-impl<'tcx> VidValuePair<'tcx> for (Ty<'tcx>, ty::TyVid) {
-    fn vid(&self) -> ty::TyVid {
-        self.1
-    }
-
-    fn value_ty(&self) -> Ty<'tcx> {
-        self.0
-    }
-
-    fn relate_generalized_ty<D>(
-        &self,
-        relate: &mut TypeRelating<'_, 'tcx, D>,
-        generalized_ty: Ty<'tcx>,
-    ) -> RelateResult<'tcx, Ty<'tcx>>
-    where
-        D: TypeRelatingDelegate<'tcx>,
-    {
-        relate.relate(self.value_ty(), generalized_ty)
-    }
-}
-
 impl<'tcx, D> TypeRelation<'tcx> for TypeRelating<'_, 'tcx, D>
 where
     D: TypeRelatingDelegate<'tcx>,
@@ -472,6 +323,8 @@ where
 
         if !D::forbid_inference_vars() {
             b = self.infcx.shallow_resolve(b);
+        } else {
+            assert!(!b.has_non_region_infer(), "unexpected inference var {:?}", b);
         }
 
         if a == b {
@@ -479,22 +332,30 @@ where
         }
 
         match (a.kind(), b.kind()) {
-            (_, &ty::Infer(ty::TyVar(vid))) => {
-                if D::forbid_inference_vars() {
-                    // Forbid inference variables in the RHS.
-                    bug!("unexpected inference var {:?}", b)
-                } else {
-                    self.relate_ty_var((a, vid))
+            (&ty::Infer(ty::TyVar(a_vid)), &ty::Infer(ty::TyVar(b_vid))) => {
+                match self.ambient_variance {
+                    ty::Invariant => infcx.inner.borrow_mut().type_variables().equate(a_vid, b_vid),
+                    _ => unimplemented!(),
                 }
             }
 
-            (&ty::Infer(ty::TyVar(vid)), _) => self.relate_ty_var((vid, b)),
+            (&ty::Infer(ty::TyVar(a_vid)), _) => {
+                infcx.instantiate_ty_var(self, true, a_vid, self.ambient_variance, b)?
+            }
+
+            (_, &ty::Infer(ty::TyVar(b_vid))) => infcx.instantiate_ty_var(
+                self,
+                false,
+                b_vid,
+                self.ambient_variance.xform(ty::Contravariant),
+                a,
+            )?,
 
             (
                 &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 || infcx.next_trait_solver() => {
-                infcx.super_combine_tys(self, a, b).or_else(|err| {
+                infcx.super_combine_tys(self, a, b).map(|_| ()).or_else(|err| {
                     // This behavior is only there for the old solver, the new solver
                     // shouldn't ever fail. Instead, it unconditionally emits an
                     // alias-relate goal.
@@ -504,22 +365,24 @@ where
                         "failure to relate an opaque to itself should result in an error later on",
                     );
                     if a_def_id.is_local() { self.relate_opaques(a, b) } else { Err(err) }
-                })
+                })?;
             }
             (&ty::Alias(ty::Opaque, ty::AliasTy { def_id, .. }), _)
             | (_, &ty::Alias(ty::Opaque, ty::AliasTy { def_id, .. }))
                 if def_id.is_local() && !self.infcx.next_trait_solver() =>
             {
-                self.relate_opaques(a, b)
+                self.relate_opaques(a, b)?;
             }
 
             _ => {
                 debug!(?a, ?b, ?self.ambient_variance);
 
                 // Will also handle unification of `IntVar` and `FloatVar`.
-                self.infcx.super_combine_tys(self, a, b)
+                self.infcx.super_combine_tys(self, a, b)?;
             }
         }
+
+        Ok(a)
     }
 
     #[instrument(skip(self), level = "trace")]
@@ -669,6 +532,10 @@ impl<'tcx, D> ObligationEmittingRelation<'tcx> for TypeRelating<'_, 'tcx, D>
 where
     D: TypeRelatingDelegate<'tcx>,
 {
+    fn span(&self) -> Span {
+        self.delegate.span()
+    }
+
     fn param_env(&self) -> ty::ParamEnv<'tcx> {
         self.delegate.param_env()
     }
diff --git a/compiler/rustc_infer/src/infer/relate/sub.rs b/compiler/rustc_infer/src/infer/relate/sub.rs
index 36876acd7c0d4..5bd3a238a67e8 100644
--- a/compiler/rustc_infer/src/infer/relate/sub.rs
+++ b/compiler/rustc_infer/src/infer/relate/sub.rs
@@ -6,6 +6,7 @@ use rustc_middle::ty::relate::{Cause, Relate, RelateResult, TypeRelation};
 use rustc_middle::ty::visit::TypeVisitableExt;
 use rustc_middle::ty::TyVar;
 use rustc_middle::ty::{self, Ty, TyCtxt};
+use rustc_span::Span;
 use std::mem;
 
 /// Ensures `a` is made a subtype of `b`. Returns `a` on success.
@@ -103,12 +104,12 @@ impl<'tcx> TypeRelation<'tcx> for Sub<'_, '_, 'tcx> {
 
                 Ok(a)
             }
-            (&ty::Infer(TyVar(a_id)), _) => {
-                self.fields.instantiate(b, ty::Contravariant, a_id, !self.a_is_expected)?;
+            (&ty::Infer(TyVar(a_vid)), _) => {
+                infcx.instantiate_ty_var(self, self.a_is_expected, a_vid, ty::Covariant, b)?;
                 Ok(a)
             }
-            (_, &ty::Infer(TyVar(b_id))) => {
-                self.fields.instantiate(a, ty::Covariant, b_id, self.a_is_expected)?;
+            (_, &ty::Infer(TyVar(b_vid))) => {
+                infcx.instantiate_ty_var(self, !self.a_is_expected, b_vid, ty::Contravariant, a)?;
                 Ok(a)
             }
 
@@ -199,6 +200,10 @@ impl<'tcx> TypeRelation<'tcx> for Sub<'_, '_, 'tcx> {
 }
 
 impl<'tcx> ObligationEmittingRelation<'tcx> for Sub<'_, '_, 'tcx> {
+    fn span(&self) -> Span {
+        self.fields.trace.span()
+    }
+
     fn param_env(&self) -> ty::ParamEnv<'tcx> {
         self.fields.param_env
     }
diff --git a/tests/ui/coherence/occurs-check/associated-type.next.stderr b/tests/ui/coherence/occurs-check/associated-type.next.stderr
index 65be4a9c884fa..e405f389f5e4b 100644
--- a/tests/ui/coherence/occurs-check/associated-type.next.stderr
+++ b/tests/ui/coherence/occurs-check/associated-type.next.stderr
@@ -1,11 +1,11 @@
 WARN rustc_infer::infer::relate::generalize may incompletely handle alias type: Alias(Projection, 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: Alias(Projection, AliasTy { args: [*const ?1t, RePlaceholder(!2_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: Alias(Projection, 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: Alias(Projection, 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: Alias(Projection, AliasTy { args: [*const ?1t, RePlaceholder(!2_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: Alias(Projection, 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: Alias(Projection, 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: Alias(Projection, AliasTy { args: [*const ?1t, RePlaceholder(!2_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: Alias(Projection, 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: Alias(Projection, 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: Alias(Projection, AliasTy { args: [*const ?1t, RePlaceholder(!2_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: Alias(Projection, 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/associated-type.old.stderr b/tests/ui/coherence/occurs-check/associated-type.old.stderr
index 8e852ec796ede..4a67a777f1051 100644
--- a/tests/ui/coherence/occurs-check/associated-type.old.stderr
+++ b/tests/ui/coherence/occurs-check/associated-type.old.stderr
@@ -1,11 +1,11 @@
 WARN rustc_infer::infer::relate::generalize may incompletely handle alias type: Alias(Projection, 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: Alias(Projection, AliasTy { args: [*const ?1t, RePlaceholder(!3_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: Alias(Projection, AliasTy { args: [*const ?1t, RePlaceholder(!2_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: Alias(Projection, 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: Alias(Projection, AliasTy { args: [*const ?1t, RePlaceholder(!3_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: Alias(Projection, AliasTy { args: [*const ?1t, RePlaceholder(!2_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: Alias(Projection, 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: Alias(Projection, AliasTy { args: [*const ?1t, RePlaceholder(!3_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: Alias(Projection, AliasTy { args: [*const ?1t, RePlaceholder(!2_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: Alias(Projection, 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: Alias(Projection, AliasTy { args: [*const ?1t, RePlaceholder(!3_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: Alias(Projection, AliasTy { args: [*const ?1t, RePlaceholder(!2_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/impl-trait/rpit/early_bound.rs b/tests/ui/impl-trait/rpit/early_bound.rs
index 03bd64d4d76d0..6dda687929c4d 100644
--- a/tests/ui/impl-trait/rpit/early_bound.rs
+++ b/tests/ui/impl-trait/rpit/early_bound.rs
@@ -5,7 +5,6 @@ fn test<'a: 'a>(n: bool) -> impl Sized + 'a {
     let true = n else { loop {} };
     let _ = || {
         let _ = identity::<&'a ()>(test(false));
-        //~^ ERROR hidden type for `impl Sized + 'a` captures lifetime that does not appear in bounds
     };
     loop {}
 }
diff --git a/tests/ui/impl-trait/rpit/early_bound.stderr b/tests/ui/impl-trait/rpit/early_bound.stderr
index 815368f250e35..780dea4e284ee 100644
--- a/tests/ui/impl-trait/rpit/early_bound.stderr
+++ b/tests/ui/impl-trait/rpit/early_bound.stderr
@@ -1,14 +1,3 @@
-error[E0700]: hidden type for `impl Sized + 'a` captures lifetime that does not appear in bounds
-  --> $DIR/early_bound.rs:7:17
-   |
-LL | fn test<'a: 'a>(n: bool) -> impl Sized + 'a {
-   |         --                  --------------- opaque type defined here
-   |         |
-   |         hidden type `&'a ()` captures the lifetime `'a` as defined here
-...
-LL |         let _ = identity::<&'a ()>(test(false));
-   |                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
 error: concrete type differs from previous defining opaque type use
   --> $DIR/early_bound.rs:3:29
    |
@@ -21,6 +10,5 @@ note: previous use here
 LL |         let _ = identity::<&'a ()>(test(false));
    |                                    ^^^^^^^^^^^
 
-error: aborting due to 2 previous errors
+error: aborting due to 1 previous error
 
-For more information about this error, try `rustc --explain E0700`.
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
index aaadf604a80ac..cde925db18484 100644
--- 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
@@ -1,8 +1,8 @@
-error[E0284]: type annotations needed: cannot satisfy `<<T as Id<_>>::Id as Unnormalizable>::Assoc == _`
+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 == _`
+   |         ^ cannot satisfy `_ == <<T as Id<_>>::Id as Unnormalizable>::Assoc`
 
 error: aborting due to 1 previous error