Revert "Auto merge of #92007 - oli-obk:lazy_tait2, r=nikomatsakis"

This reverts commit e7cc3bddbe0d0e374d05e7003e662bba1742dbae, reversing
changes made to 734368a200904ef9c21db86c595dc04263c87be0.

16 files changed, 283 insertions, 602 deletions

diff --git a/compiler/rustc_infer/src/infer/at.rs b/compiler/rustc_infer/src/infer/at.rs
index 6515f948dd3..c26ea4c9669 100644
--- a/compiler/rustc_infer/src/infer/at.rs
+++ b/compiler/rustc_infer/src/infer/at.rs
@@ -34,12 +34,6 @@ pub struct At<'a, 'tcx> {
     pub infcx: &'a InferCtxt<'a, 'tcx>,
     pub cause: &'a ObligationCause<'tcx>,
     pub param_env: ty::ParamEnv<'tcx>,
-    /// Whether we should define opaque types
-    /// or just treat them opaquely.
-    /// Currently only used to prevent predicate
-    /// matching from matching anything against opaque
-    /// types.
-    pub define_opaque_types: bool,
 }
 
 pub struct Trace<'a, 'tcx> {
@@ -55,7 +49,7 @@ impl<'a, 'tcx> InferCtxt<'a, 'tcx> {
         cause: &'a ObligationCause<'tcx>,
         param_env: ty::ParamEnv<'tcx>,
     ) -> At<'a, 'tcx> {
-        At { infcx: self, cause, param_env, define_opaque_types: true }
+        At { infcx: self, cause, param_env }
     }
 }
 
@@ -70,10 +64,6 @@ pub trait ToTrace<'tcx>: Relate<'tcx> + Copy {
 }
 
 impl<'a, 'tcx> At<'a, 'tcx> {
-    pub fn define_opaque_types(self, define_opaque_types: bool) -> Self {
-        Self { define_opaque_types, ..self }
-    }
-
     /// Hacky routine for equating two impl headers in coherence.
     pub fn eq_impl_headers(
         self,
@@ -204,7 +194,7 @@ impl<'a, 'tcx> Trace<'a, 'tcx> {
     {
         let Trace { at, trace, a_is_expected } = self;
         at.infcx.commit_if_ok(|_| {
-            let mut fields = at.infcx.combine_fields(trace, at.param_env, at.define_opaque_types);
+            let mut fields = at.infcx.combine_fields(trace, at.param_env);
             fields
                 .sub(a_is_expected)
                 .relate(a, b)
@@ -221,7 +211,7 @@ impl<'a, 'tcx> Trace<'a, 'tcx> {
     {
         let Trace { at, trace, a_is_expected } = self;
         at.infcx.commit_if_ok(|_| {
-            let mut fields = at.infcx.combine_fields(trace, at.param_env, at.define_opaque_types);
+            let mut fields = at.infcx.combine_fields(trace, at.param_env);
             fields
                 .equate(a_is_expected)
                 .relate(a, b)
@@ -236,7 +226,7 @@ impl<'a, 'tcx> Trace<'a, 'tcx> {
     {
         let Trace { at, trace, a_is_expected } = self;
         at.infcx.commit_if_ok(|_| {
-            let mut fields = at.infcx.combine_fields(trace, at.param_env, at.define_opaque_types);
+            let mut fields = at.infcx.combine_fields(trace, at.param_env);
             fields
                 .lub(a_is_expected)
                 .relate(a, b)
@@ -251,7 +241,7 @@ impl<'a, 'tcx> Trace<'a, 'tcx> {
     {
         let Trace { at, trace, a_is_expected } = self;
         at.infcx.commit_if_ok(|_| {
-            let mut fields = at.infcx.combine_fields(trace, at.param_env, at.define_opaque_types);
+            let mut fields = at.infcx.combine_fields(trace, at.param_env);
             fields
                 .glb(a_is_expected)
                 .relate(a, b)
diff --git a/compiler/rustc_infer/src/infer/canonical/query_response.rs b/compiler/rustc_infer/src/infer/canonical/query_response.rs
index 7d86f8a763c..5b4a9d9dfad 100644
--- a/compiler/rustc_infer/src/infer/canonical/query_response.rs
+++ b/compiler/rustc_infer/src/infer/canonical/query_response.rs
@@ -26,7 +26,6 @@ use rustc_middle::ty::fold::TypeFoldable;
 use rustc_middle::ty::relate::TypeRelation;
 use rustc_middle::ty::subst::{GenericArg, GenericArgKind};
 use rustc_middle::ty::{self, BoundVar, Const, ToPredicate, Ty, TyCtxt};
-use rustc_span::Span;
 use std::fmt::Debug;
 use std::iter;
 
@@ -90,7 +89,6 @@ impl<'cx, 'tcx> InferCtxt<'cx, 'tcx> {
             var_values: inference_vars,
             region_constraints: QueryRegionConstraints::default(),
             certainty: Certainty::Proven, // Ambiguities are OK!
-            opaque_types: vec![],
             value: answer,
         })
     }
@@ -135,27 +133,14 @@ impl<'cx, 'tcx> InferCtxt<'cx, 'tcx> {
         let certainty =
             if ambig_errors.is_empty() { Certainty::Proven } else { Certainty::Ambiguous };
 
-        let opaque_types = self.take_opaque_types_for_query_response();
-
         Ok(QueryResponse {
             var_values: inference_vars,
             region_constraints,
             certainty,
             value: answer,
-            opaque_types,
         })
     }
 
-    fn take_opaque_types_for_query_response(&self) -> Vec<(Ty<'tcx>, Ty<'tcx>)> {
-        self.inner
-            .borrow_mut()
-            .opaque_type_storage
-            .take_opaque_types()
-            .into_iter()
-            .map(|(k, v)| (self.tcx.mk_opaque(k.def_id, k.substs), v.hidden_type.ty))
-            .collect()
-    }
-
     /// Given the (canonicalized) result to a canonical query,
     /// instantiates the result so it can be used, plugging in the
     /// values from the canonical query. (Note that the result may
@@ -238,12 +223,13 @@ impl<'cx, 'tcx> InferCtxt<'cx, 'tcx> {
     where
         R: Debug + TypeFoldable<'tcx>,
     {
-        let InferOk { value: result_subst, mut obligations } = self
-            .query_response_substitution_guess(cause, param_env, original_values, query_response)?;
+        let result_subst =
+            self.query_response_substitution_guess(cause, original_values, query_response);
 
         // Compute `QueryOutlivesConstraint` values that unify each of
         // the original values `v_o` that was canonicalized into a
         // variable...
+        let mut obligations = vec![];
 
         for (index, original_value) in original_values.var_values.iter().enumerate() {
             // ...with the value `v_r` of that variable from the query.
@@ -358,25 +344,20 @@ impl<'cx, 'tcx> InferCtxt<'cx, 'tcx> {
             original_values, query_response,
         );
 
-        let mut value = self.query_response_substitution_guess(
-            cause,
-            param_env,
-            original_values,
-            query_response,
-        )?;
+        let result_subst =
+            self.query_response_substitution_guess(cause, original_values, query_response);
 
-        value.obligations.extend(
-            self.unify_query_response_substitution_guess(
+        let obligations = self
+            .unify_query_response_substitution_guess(
                 cause,
                 param_env,
                 original_values,
-                &value.value,
+                &result_subst,
                 query_response,
             )?
-            .into_obligations(),
-        );
+            .into_obligations();
 
-        Ok(value)
+        Ok(InferOk { value: result_subst, obligations })
     }
 
     /// Given the original values and the (canonicalized) result from
@@ -391,10 +372,9 @@ impl<'cx, 'tcx> InferCtxt<'cx, 'tcx> {
     fn query_response_substitution_guess<R>(
         &self,
         cause: &ObligationCause<'tcx>,
-        param_env: ty::ParamEnv<'tcx>,
         original_values: &OriginalQueryValues<'tcx>,
         query_response: &Canonical<'tcx, QueryResponse<'tcx, R>>,
-    ) -> InferResult<'tcx, CanonicalVarValues<'tcx>>
+    ) -> CanonicalVarValues<'tcx>
     where
         R: Debug + TypeFoldable<'tcx>,
     {
@@ -494,16 +474,7 @@ impl<'cx, 'tcx> InferCtxt<'cx, 'tcx> {
                 .collect(),
         };
 
-        let mut obligations = vec![];
-
-        // Carry all newly resolved opaque types to the caller's scope
-        for &(a, b) in &query_response.value.opaque_types {
-            let a = substitute_value(self.tcx, &result_subst, a);
-            let b = substitute_value(self.tcx, &result_subst, b);
-            obligations.extend(self.handle_opaque_type(a, b, cause, param_env)?.obligations);
-        }
-
-        Ok(InferOk { value: result_subst, obligations })
+        result_subst
     }
 
     /// Given a "guess" at the values for the canonical variables in
@@ -660,10 +631,6 @@ struct QueryTypeRelatingDelegate<'a, 'tcx> {
 }
 
 impl<'tcx> TypeRelatingDelegate<'tcx> for QueryTypeRelatingDelegate<'_, 'tcx> {
-    fn span(&self) -> Span {
-        self.cause.span
-    }
-
     fn param_env(&self) -> ty::ParamEnv<'tcx> {
         self.param_env
     }
@@ -719,14 +686,4 @@ impl<'tcx> TypeRelatingDelegate<'tcx> for QueryTypeRelatingDelegate<'_, 'tcx> {
     fn forbid_inference_vars() -> bool {
         true
     }
-
-    fn register_opaque_type(&mut self, a: Ty<'tcx>, b: Ty<'tcx>, a_is_expected: bool) {
-        self.obligations.push(self.infcx.opaque_ty_obligation(
-            a,
-            b,
-            a_is_expected,
-            self.param_env,
-            self.cause.clone(),
-        ));
-    }
 }
diff --git a/compiler/rustc_infer/src/infer/combine.rs b/compiler/rustc_infer/src/infer/combine.rs
index 5668b6c10b0..a77fd8fae8d 100644
--- a/compiler/rustc_infer/src/infer/combine.rs
+++ b/compiler/rustc_infer/src/infer/combine.rs
@@ -51,12 +51,6 @@ pub struct CombineFields<'infcx, 'tcx> {
     pub cause: Option<ty::relate::Cause>,
     pub param_env: ty::ParamEnv<'tcx>,
     pub obligations: PredicateObligations<'tcx>,
-    /// Whether we should define opaque types
-    /// or just treat them opaquely.
-    /// Currently only used to prevent predicate
-    /// matching from matching anything against opaque
-    /// types.
-    pub define_opaque_types: bool,
 }
 
 #[derive(Copy, Clone, Debug)]
@@ -328,7 +322,6 @@ impl<'infcx, 'tcx> CombineFields<'infcx, 'tcx> {
     /// 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>,
@@ -341,6 +334,8 @@ impl<'infcx, 'tcx> CombineFields<'infcx, '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());
 
+        debug!("instantiate(a_ty={:?} dir={:?} b_vid={:?})", a_ty, dir, b_vid);
+
         // Generalize type of `a_ty` appropriately depending on the
         // direction.  As an example, assume:
         //
@@ -353,7 +348,10 @@ impl<'infcx, 'tcx> CombineFields<'infcx, 'tcx> {
         // variables. (Down below, we will relate `a_ty <: b_ty`,
         // adding constraints like `'x: '?2` and `?1 <: ?3`.)
         let Generalization { ty: b_ty, needs_wf } = self.generalize(a_ty, b_vid, dir)?;
-        debug!(?b_ty);
+        debug!(
+            "instantiate(a_ty={:?}, dir={:?}, b_vid={:?}, generalized b_ty={:?})",
+            a_ty, dir, b_vid, b_ty
+        );
         self.infcx.inner.borrow_mut().type_variables().instantiate(b_vid, b_ty);
 
         if needs_wf {
@@ -394,13 +392,13 @@ impl<'infcx, 'tcx> CombineFields<'infcx, 'tcx> {
     /// Preconditions:
     ///
     /// - `for_vid` is a "root vid"
-    #[instrument(skip(self), level = "trace")]
     fn generalize(
         &self,
         ty: Ty<'tcx>,
         for_vid: ty::TyVid,
         dir: RelationDir,
     ) -> RelateResult<'tcx, Generalization<'tcx>> {
+        debug!("generalize(ty={:?}, for_vid={:?}, dir={:?}", ty, for_vid, dir);
         // Determine the ambient variance within which `ty` appears.
         // The surrounding equation is:
         //
@@ -414,7 +412,7 @@ impl<'infcx, 'tcx> CombineFields<'infcx, 'tcx> {
             RelationDir::SupertypeOf => ty::Contravariant,
         };
 
-        trace!(?ambient_variance);
+        debug!("generalize: ambient_variance = {:?}", ambient_variance);
 
         let for_universe = match self.infcx.inner.borrow_mut().type_variables().probe(for_vid) {
             v @ TypeVariableValue::Known { .. } => {
@@ -423,8 +421,8 @@ impl<'infcx, 'tcx> CombineFields<'infcx, 'tcx> {
             TypeVariableValue::Unknown { universe } => universe,
         };
 
-        trace!(?for_universe);
-        trace!(?self.trace);
+        debug!("generalize: for_universe = {:?}", for_universe);
+        debug!("generalize: trace = {:?}", self.trace);
 
         let mut generalize = Generalizer {
             infcx: self.infcx,
@@ -441,12 +439,12 @@ impl<'infcx, 'tcx> CombineFields<'infcx, 'tcx> {
         let ty = match generalize.relate(ty, ty) {
             Ok(ty) => ty,
             Err(e) => {
-                debug!(?e, "failure");
+                debug!("generalize: failure {:?}", e);
                 return Err(e);
             }
         };
         let needs_wf = generalize.needs_wf;
-        trace!(?ty, ?needs_wf, "success");
+        debug!("generalize: success {{ {:?}, {:?} }}", ty, needs_wf);
         Ok(Generalization { ty, needs_wf })
     }
 
diff --git a/compiler/rustc_infer/src/infer/equate.rs b/compiler/rustc_infer/src/infer/equate.rs
index 9f6c6d31845..90c0ff9226f 100644
--- a/compiler/rustc_infer/src/infer/equate.rs
+++ b/compiler/rustc_infer/src/infer/equate.rs
@@ -66,19 +66,18 @@ impl<'tcx> TypeRelation<'tcx> for Equate<'_, '_, 'tcx> {
         self.relate(a, b)
     }
 
-    #[instrument(skip(self), level = "debug")]
     fn tys(&mut self, a: Ty<'tcx>, b: Ty<'tcx>) -> RelateResult<'tcx, Ty<'tcx>> {
+        debug!("{}.tys({:?}, {:?})", self.tag(), a, b);
         if a == b {
             return Ok(a);
         }
 
-        trace!(a = ?a.kind(), b = ?b.kind());
-
         let infcx = self.fields.infcx;
-
         let a = infcx.inner.borrow_mut().type_variables().replace_if_possible(a);
         let b = infcx.inner.borrow_mut().type_variables().replace_if_possible(b);
 
+        debug!("{}.tys: replacements ({:?}, {:?})", self.tag(), a, b);
+
         match (a.kind(), b.kind()) {
             (&ty::Infer(TyVar(a_id)), &ty::Infer(TyVar(b_id))) => {
                 infcx.inner.borrow_mut().type_variables().equate(a_id, b_id);
@@ -92,21 +91,6 @@ impl<'tcx> TypeRelation<'tcx> for Equate<'_, '_, 'tcx> {
                 self.fields.instantiate(a, RelationDir::EqTo, b_id, self.a_is_expected)?;
             }
 
-            (&ty::Opaque(a_def_id, _), &ty::Opaque(b_def_id, _)) if a_def_id == b_def_id => {
-                self.fields.infcx.super_combine_tys(self, a, b)?;
-            }
-            (&ty::Opaque(did, ..), _) | (_, &ty::Opaque(did, ..))
-                if self.fields.define_opaque_types && did.is_local() =>
-            {
-                self.fields.obligations.push(infcx.opaque_ty_obligation(
-                    a,
-                    b,
-                    self.a_is_expected(),
-                    self.param_env(),
-                    self.fields.trace.cause.clone(),
-                ));
-            }
-
             _ => {
                 self.fields.infcx.super_combine_tys(self, a, b)?;
             }
diff --git a/compiler/rustc_infer/src/infer/glb.rs b/compiler/rustc_infer/src/infer/glb.rs
index c4c4eab261e..862f5a5fbb8 100644
--- a/compiler/rustc_infer/src/infer/glb.rs
+++ b/compiler/rustc_infer/src/infer/glb.rs
@@ -4,7 +4,7 @@ use super::InferCtxt;
 use super::Subtype;
 
 use crate::infer::combine::ConstEquateRelation;
-use crate::traits::{ObligationCause, PredicateObligation};
+use crate::traits::ObligationCause;
 use rustc_middle::ty::relate::{Relate, RelateResult, TypeRelation};
 use rustc_middle::ty::{self, Ty, TyCtxt};
 
@@ -111,20 +111,12 @@ impl<'combine, 'infcx, 'tcx> LatticeDir<'infcx, 'tcx> for Glb<'combine, 'infcx,
         &self.fields.trace.cause
     }
 
-    fn add_obligations(&mut self, obligations: Vec<PredicateObligation<'tcx>>) {
-        self.fields.obligations.extend(obligations)
-    }
-
     fn relate_bound(&mut self, v: Ty<'tcx>, a: Ty<'tcx>, b: Ty<'tcx>) -> RelateResult<'tcx, ()> {
         let mut sub = self.fields.sub(self.a_is_expected);
         sub.relate(v, a)?;
         sub.relate(v, b)?;
         Ok(())
     }
-
-    fn define_opaque_types(&self) -> bool {
-        self.fields.define_opaque_types
-    }
 }
 
 impl<'tcx> ConstEquateRelation<'tcx> for Glb<'_, '_, 'tcx> {
diff --git a/compiler/rustc_infer/src/infer/lattice.rs b/compiler/rustc_infer/src/infer/lattice.rs
index 6bda44f0ef2..c47d4769637 100644
--- a/compiler/rustc_infer/src/infer/lattice.rs
+++ b/compiler/rustc_infer/src/infer/lattice.rs
@@ -22,7 +22,7 @@
 use super::type_variable::{TypeVariableOrigin, TypeVariableOriginKind};
 use super::InferCtxt;
 
-use crate::traits::{ObligationCause, PredicateObligation};
+use crate::traits::ObligationCause;
 use rustc_middle::ty::relate::{RelateResult, TypeRelation};
 use rustc_middle::ty::TyVar;
 use rustc_middle::ty::{self, Ty};
@@ -32,10 +32,6 @@ pub trait LatticeDir<'f, 'tcx>: TypeRelation<'tcx> {
 
     fn cause(&self) -> &ObligationCause<'tcx>;
 
-    fn add_obligations(&mut self, obligations: Vec<PredicateObligation<'tcx>>);
-
-    fn define_opaque_types(&self) -> bool;
-
     // Relates the type `v` to `a` and `b` such that `v` represents
     // the LUB/GLB of `a` and `b` as appropriate.
     //
@@ -45,7 +41,6 @@ pub trait LatticeDir<'f, 'tcx>: TypeRelation<'tcx> {
     fn relate_bound(&mut self, v: Ty<'tcx>, a: Ty<'tcx>, b: Ty<'tcx>) -> RelateResult<'tcx, ()>;
 }
 
-#[instrument(skip(this), level = "debug")]
 pub fn super_lattice_tys<'a, 'tcx: 'a, L>(
     this: &mut L,
     a: Ty<'tcx>,
@@ -54,17 +49,15 @@ pub fn super_lattice_tys<'a, 'tcx: 'a, L>(
 where
     L: LatticeDir<'a, 'tcx>,
 {
-    debug!("{}", this.tag());
+    debug!("{}.lattice_tys({:?}, {:?})", this.tag(), a, b);
 
     if a == b {
         return Ok(a);
     }
 
     let infcx = this.infcx();
-
     let a = infcx.inner.borrow_mut().type_variables().replace_if_possible(a);
     let b = infcx.inner.borrow_mut().type_variables().replace_if_possible(b);
-
     match (a.kind(), b.kind()) {
         // If one side is known to be a variable and one is not,
         // create a variable (`v`) to represent the LUB. Make sure to
@@ -101,22 +94,6 @@ where
             Ok(v)
         }
 
-        (&ty::Opaque(a_def_id, _), &ty::Opaque(b_def_id, _)) if a_def_id == b_def_id => {
-            infcx.super_combine_tys(this, a, b)
-        }
-        (&ty::Opaque(did, ..), _) | (_, &ty::Opaque(did, ..))
-            if this.define_opaque_types() && did.is_local() =>
-        {
-            this.add_obligations(vec![infcx.opaque_ty_obligation(
-                a,
-                b,
-                this.a_is_expected(),
-                this.param_env(),
-                this.cause().clone(),
-            )]);
-            Ok(a)
-        }
-
         _ => infcx.super_combine_tys(this, a, b),
     }
 }
diff --git a/compiler/rustc_infer/src/infer/lub.rs b/compiler/rustc_infer/src/infer/lub.rs
index bbd8e001469..5191d1c1cc1 100644
--- a/compiler/rustc_infer/src/infer/lub.rs
+++ b/compiler/rustc_infer/src/infer/lub.rs
@@ -4,7 +4,7 @@ use super::InferCtxt;
 use super::Subtype;
 
 use crate::infer::combine::ConstEquateRelation;
-use crate::traits::{ObligationCause, PredicateObligation};
+use crate::traits::ObligationCause;
 use rustc_middle::ty::relate::{Relate, RelateResult, TypeRelation};
 use rustc_middle::ty::{self, Ty, TyCtxt};
 
@@ -117,18 +117,10 @@ impl<'combine, 'infcx, 'tcx> LatticeDir<'infcx, 'tcx> for Lub<'combine, 'infcx,
         &self.fields.trace.cause
     }
 
-    fn add_obligations(&mut self, obligations: Vec<PredicateObligation<'tcx>>) {
-        self.fields.obligations.extend(obligations)
-    }
-
     fn relate_bound(&mut self, v: Ty<'tcx>, a: Ty<'tcx>, b: Ty<'tcx>) -> RelateResult<'tcx, ()> {
         let mut sub = self.fields.sub(self.a_is_expected);
         sub.relate(a, v)?;
         sub.relate(b, v)?;
         Ok(())
     }
-
-    fn define_opaque_types(&self) -> bool {
-        self.fields.define_opaque_types
-    }
 }
diff --git a/compiler/rustc_infer/src/infer/mod.rs b/compiler/rustc_infer/src/infer/mod.rs
index 08320a0ff1d..c18d36d1f74 100644
--- a/compiler/rustc_infer/src/infer/mod.rs
+++ b/compiler/rustc_infer/src/infer/mod.rs
@@ -5,7 +5,7 @@ pub use self::RegionVariableOrigin::*;
 pub use self::SubregionOrigin::*;
 pub use self::ValuePairs::*;
 
-use self::opaque_types::OpaqueTypeStorage;
+use self::opaque_types::OpaqueTypeMap;
 pub(crate) use self::undo_log::{InferCtxtUndoLogs, Snapshot, UndoLog};
 
 use crate::traits::{self, ObligationCause, PredicateObligations, TraitEngine};
@@ -192,8 +192,18 @@ pub struct InferCtxtInner<'tcx> {
 
     undo_log: InferCtxtUndoLogs<'tcx>,
 
-    /// Caches for opaque type inference.
-    pub opaque_type_storage: OpaqueTypeStorage<'tcx>,
+    // Opaque types found in explicit return types and their
+    // associated fresh inference variable. Writeback resolves these
+    // variables to get the concrete type, which can be used to
+    // 'de-opaque' OpaqueTypeDecl outside of type inference.
+    pub opaque_types: OpaqueTypeMap<'tcx>,
+
+    /// A map from inference variables created from opaque
+    /// type instantiations (`ty::Infer`) to the actual opaque
+    /// type (`ty::Opaque`). Used during fallback to map unconstrained
+    /// opaque type inference variables to their corresponding
+    /// opaque type.
+    pub opaque_types_vars: FxHashMap<Ty<'tcx>, Ty<'tcx>>,
 }
 
 impl<'tcx> InferCtxtInner<'tcx> {
@@ -207,7 +217,8 @@ impl<'tcx> InferCtxtInner<'tcx> {
             float_unification_storage: ut::UnificationTableStorage::new(),
             region_constraint_storage: Some(RegionConstraintStorage::new()),
             region_obligations: vec![],
-            opaque_type_storage: Default::default(),
+            opaque_types: Default::default(),
+            opaque_types_vars: Default::default(),
         }
     }
 
@@ -227,11 +238,6 @@ impl<'tcx> InferCtxtInner<'tcx> {
     }
 
     #[inline]
-    pub fn opaque_types(&mut self) -> opaque_types::OpaqueTypeTable<'_, 'tcx> {
-        self.opaque_type_storage.with_log(&mut self.undo_log)
-    }
-
-    #[inline]
     fn int_unification_table(
         &mut self,
     ) -> ut::UnificationTable<
@@ -291,10 +297,6 @@ pub struct InferCtxt<'a, 'tcx> {
     /// to the outside until the end up in an `InferCtxt` for typeck or borrowck.
     pub defining_use_anchor: Option<LocalDefId>,
 
-    /// Used by WF-checking to not have to figure out hidden types itself, but
-    /// to just invoke type_of to get the already computed hidden type from typeck.
-    pub reveal_defining_opaque_types: bool,
-
     /// During type-checking/inference of a body, `in_progress_typeck_results`
     /// contains a reference to the typeck results being built up, which are
     /// used for reading closure kinds/signatures as they are inferred,
@@ -563,7 +565,6 @@ pub struct InferCtxtBuilder<'tcx> {
     tcx: TyCtxt<'tcx>,
     fresh_typeck_results: Option<RefCell<ty::TypeckResults<'tcx>>>,
     defining_use_anchor: Option<LocalDefId>,
-    reveal_defining_opaque_types: bool,
 }
 
 pub trait TyCtxtInferExt<'tcx> {
@@ -572,12 +573,7 @@ pub trait TyCtxtInferExt<'tcx> {
 
 impl<'tcx> TyCtxtInferExt<'tcx> for TyCtxt<'tcx> {
     fn infer_ctxt(self) -> InferCtxtBuilder<'tcx> {
-        InferCtxtBuilder {
-            tcx: self,
-            defining_use_anchor: None,
-            fresh_typeck_results: None,
-            reveal_defining_opaque_types: false,
-        }
+        InferCtxtBuilder { tcx: self, defining_use_anchor: None, fresh_typeck_results: None }
     }
 }
 
@@ -601,13 +597,6 @@ impl<'tcx> InferCtxtBuilder<'tcx> {
         self
     }
 
-    /// WF-checking doesn't need to recompute opaque types and can instead use
-    /// the type_of query to get them from typeck.
-    pub fn reveal_defining_opaque_types(mut self) -> Self {
-        self.reveal_defining_opaque_types = true;
-        self
-    }
-
     /// Given a canonical value `C` as a starting point, create an
     /// inference context that contains each of the bound values
     /// within instantiated as a fresh variable. The `f` closure is
@@ -632,17 +621,11 @@ impl<'tcx> InferCtxtBuilder<'tcx> {
     }
 
     pub fn enter<R>(&mut self, f: impl for<'a> FnOnce(InferCtxt<'a, 'tcx>) -> R) -> R {
-        let InferCtxtBuilder {
-            tcx,
-            defining_use_anchor,
-            reveal_defining_opaque_types,
-            ref fresh_typeck_results,
-        } = *self;
+        let InferCtxtBuilder { tcx, defining_use_anchor, ref fresh_typeck_results } = *self;
         let in_progress_typeck_results = fresh_typeck_results.as_ref();
         f(InferCtxt {
             tcx,
             defining_use_anchor,
-            reveal_defining_opaque_types,
             in_progress_typeck_results,
             inner: RefCell::new(InferCtxtInner::new()),
             lexical_region_resolutions: RefCell::new(None),
@@ -764,7 +747,6 @@ impl<'a, 'tcx> InferCtxt<'a, 'tcx> {
         &'a self,
         trace: TypeTrace<'tcx>,
         param_env: ty::ParamEnv<'tcx>,
-        define_opaque_types: bool,
     ) -> CombineFields<'a, 'tcx> {
         CombineFields {
             infcx: self,
@@ -772,7 +754,6 @@ impl<'a, 'tcx> InferCtxt<'a, 'tcx> {
             cause: None,
             param_env,
             obligations: PredicateObligations::new(),
-            define_opaque_types,
         }
     }
 
@@ -1088,20 +1069,12 @@ impl<'a, 'tcx> InferCtxt<'a, 'tcx> {
         self.tcx.mk_ty_var(self.next_ty_var_id(origin))
     }
 
-    pub fn next_ty_var_id_in_universe(
-        &self,
-        origin: TypeVariableOrigin,
-        universe: ty::UniverseIndex,
-    ) -> TyVid {
-        self.inner.borrow_mut().type_variables().new_var(universe, origin)
-    }
-
     pub fn next_ty_var_in_universe(
         &self,
         origin: TypeVariableOrigin,
         universe: ty::UniverseIndex,
     ) -> Ty<'tcx> {
-        let vid = self.next_ty_var_id_in_universe(origin, universe);
+        let vid = self.inner.borrow_mut().type_variables().new_var(universe, origin);
         self.tcx.mk_ty_var(vid)
     }
 
diff --git a/compiler/rustc_infer/src/infer/nll_relate/mod.rs b/compiler/rustc_infer/src/infer/nll_relate/mod.rs
index 3a288516664..0a210ed053c 100644
--- a/compiler/rustc_infer/src/infer/nll_relate/mod.rs
+++ b/compiler/rustc_infer/src/infer/nll_relate/mod.rs
@@ -24,13 +24,11 @@
 use crate::infer::combine::ConstEquateRelation;
 use crate::infer::InferCtxt;
 use crate::infer::{ConstVarValue, ConstVariableValue};
-use crate::infer::{TypeVariableOrigin, TypeVariableOriginKind};
 use rustc_data_structures::fx::FxHashMap;
 use rustc_middle::ty::error::TypeError;
 use rustc_middle::ty::fold::{TypeFoldable, TypeVisitor};
 use rustc_middle::ty::relate::{self, Relate, RelateResult, TypeRelation};
 use rustc_middle::ty::{self, InferConst, Ty, TyCtxt};
-use rustc_span::Span;
 use std::fmt::Debug;
 use std::ops::ControlFlow;
 
@@ -77,7 +75,6 @@ where
 
 pub trait TypeRelatingDelegate<'tcx> {
     fn param_env(&self) -> ty::ParamEnv<'tcx>;
-    fn span(&self) -> Span;
 
     /// Push a constraint `sup: sub` -- this constraint must be
     /// satisfied for the two types to be related. `sub` and `sup` may
@@ -90,8 +87,6 @@ pub trait TypeRelatingDelegate<'tcx> {
         info: ty::VarianceDiagInfo<'tcx>,
     );
 
-    fn register_opaque_type(&mut self, a: Ty<'tcx>, b: Ty<'tcx>, a_is_expected: bool);
-
     fn const_equate(&mut self, a: &'tcx ty::Const<'tcx>, b: &'tcx ty::Const<'tcx>);
 
     /// Creates a new universe index. Used when instantiating placeholders.
@@ -282,6 +277,7 @@ where
         projection_ty: ty::ProjectionTy<'tcx>,
         value_ty: Ty<'tcx>,
     ) -> Ty<'tcx> {
+        use crate::infer::type_variable::{TypeVariableOrigin, TypeVariableOriginKind};
         use rustc_span::DUMMY_SP;
 
         match *value_ty.kind() {
@@ -290,8 +286,6 @@ where
                     kind: TypeVariableOriginKind::MiscVariable,
                     span: DUMMY_SP,
                 });
-                // FIXME(lazy-normalization): This will always ICE, because the recursive
-                // call will end up in the _ arm below.
                 self.relate_projection_ty(projection_ty, var);
                 self.relate_projection_ty(other_projection_ty, var);
                 var
@@ -537,8 +531,6 @@ where
 
     #[instrument(skip(self), level = "debug")]
     fn tys(&mut self, a: Ty<'tcx>, mut b: Ty<'tcx>) -> RelateResult<'tcx, Ty<'tcx>> {
-        let infcx = self.infcx;
-
         let a = self.infcx.shallow_resolve(a);
 
         if !D::forbid_inference_vars() {
@@ -567,35 +559,6 @@ where
 
             (&ty::Infer(ty::TyVar(vid)), _) => self.relate_ty_var((vid, b)),
 
-            (&ty::Opaque(a_def_id, _), &ty::Opaque(b_def_id, _)) if a_def_id == b_def_id => {
-                self.infcx.super_combine_tys(self, a, b)
-            }
-            (&ty::Opaque(did, ..), _) | (_, &ty::Opaque(did, ..)) if did.is_local() => {
-                let (a, b) = if self.a_is_expected() { (a, b) } else { (b, a) };
-                let mut generalize = |ty, ty_is_expected| {
-                    let var = 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))
-                    } else {
-                        self.relate_ty_var((var, ty))
-                    }
-                };
-                let (a, b) = match (a.kind(), b.kind()) {
-                    (&ty::Opaque(..), _) => (a, generalize(b, false)?),
-                    (_, &ty::Opaque(..)) => (generalize(a, true)?, b),
-                    _ => unreachable!(),
-                };
-                self.delegate.register_opaque_type(a, b, true);
-                trace!(a = ?a.kind(), b = ?b.kind(), "opaque type instantiated");
-                Ok(a)
-            }
-
             (&ty::Projection(projection_ty), _)
                 if D::normalization() == NormalizationStrategy::Lazy =>
             {
diff --git a/compiler/rustc_infer/src/infer/opaque_types.rs b/compiler/rustc_infer/src/infer/opaque_types.rs
index 46420fbe0c3..e7dca94806c 100644
--- a/compiler/rustc_infer/src/infer/opaque_types.rs
+++ b/compiler/rustc_infer/src/infer/opaque_types.rs
@@ -1,11 +1,10 @@
+use crate::infer::type_variable::{TypeVariableOrigin, TypeVariableOriginKind};
 use crate::infer::{InferCtxt, InferOk};
-use crate::traits::{self, PredicateObligation};
-use hir::def_id::{DefId, LocalDefId};
-use hir::OpaqueTyOrigin;
+use crate::traits;
 use rustc_data_structures::sync::Lrc;
 use rustc_data_structures::vec_map::VecMap;
 use rustc_hir as hir;
-use rustc_middle::traits::ObligationCause;
+use rustc_hir::def_id::LocalDefId;
 use rustc_middle::ty::fold::BottomUpFolder;
 use rustc_middle::ty::subst::{GenericArgKind, Subst};
 use rustc_middle::ty::{self, OpaqueTypeKey, Ty, TyCtxt, TypeFoldable, TypeVisitor};
@@ -15,28 +14,14 @@ use std::ops::ControlFlow;
 
 pub type OpaqueTypeMap<'tcx> = VecMap<OpaqueTypeKey<'tcx>, OpaqueTypeDecl<'tcx>>;
 
-mod table;
-
-pub use table::{OpaqueTypeStorage, OpaqueTypeTable};
-
-use super::InferResult;
-
 /// Information about the opaque types whose values we
 /// are inferring in this function (these are the `impl Trait` that
 /// appear in the return type).
-#[derive(Clone, Debug)]
+#[derive(Copy, Clone, Debug)]
 pub struct OpaqueTypeDecl<'tcx> {
-    /// The hidden types that have been inferred for this opaque type.
-    /// There can be multiple, but they are all `lub`ed together at the end
-    /// to obtain the canonical hidden type.
-    pub hidden_type: OpaqueHiddenType<'tcx>,
-
-    /// The origin of the opaque type.
-    pub origin: hir::OpaqueTyOrigin,
-}
+    /// The opaque type (`ty::Opaque`) for this declaration.
+    pub opaque_type: Ty<'tcx>,
 
-#[derive(Copy, Clone, Debug, TypeFoldable)]
-pub struct OpaqueHiddenType<'tcx> {
     /// The span of this particular definition of the opaque type. So
     /// for example:
     ///
@@ -50,7 +35,7 @@ pub struct OpaqueHiddenType<'tcx> {
     /// In cases where the fn returns `(impl Trait, impl Trait)` or
     /// other such combinations, the result is currently
     /// over-approximated, but better than nothing.
-    pub span: Span,
+    pub definition_span: Span,
 
     /// The type variable that represents the value of the opaque type
     /// that we require. In other words, after we compile this function,
@@ -64,132 +49,54 @@ pub struct OpaqueHiddenType<'tcx> {
     /// those that are arguments to `Foo` in the constraint above. (In
     /// other words, `?C` should not include `'b`, even though it's a
     /// lifetime parameter on `foo`.)
-    pub ty: Ty<'tcx>,
+    pub concrete_ty: Ty<'tcx>,
+
+    /// The origin of the opaque type.
+    pub origin: hir::OpaqueTyOrigin,
 }
 
 impl<'a, 'tcx> InferCtxt<'a, 'tcx> {
-    pub fn handle_opaque_type(
+    /// Replaces all opaque types in `value` with fresh inference variables
+    /// and creates appropriate obligations. For example, given the input:
+    ///
+    ///     impl Iterator<Item = impl Debug>
+    ///
+    /// this method would create two type variables, `?0` and `?1`. It would
+    /// return the type `?0` but also the obligations:
+    ///
+    ///     ?0: Iterator<Item = ?1>
+    ///     ?1: Debug
+    ///
+    /// Moreover, it returns an `OpaqueTypeMap` that would map `?0` to
+    /// info about the `impl Iterator<..>` type and `?1` to info about
+    /// the `impl Debug` type.
+    ///
+    /// # Parameters
+    ///
+    /// - `parent_def_id` -- the `DefId` of the function in which the opaque type
+    ///   is defined
+    /// - `body_id` -- the body-id with which the resulting obligations should
+    ///   be associated
+    /// - `param_env` -- the in-scope parameter environment to be used for
+    ///   obligations
+    /// - `value` -- the value within which we are instantiating opaque types
+    /// - `value_span` -- the span where the value came from, used in error reporting
+    pub fn instantiate_opaque_types<T: TypeFoldable<'tcx>>(
         &self,
-        a: Ty<'tcx>,
-        b: Ty<'tcx>,
-        cause: &ObligationCause<'tcx>,
+        body_id: hir::HirId,
         param_env: ty::ParamEnv<'tcx>,
-    ) -> InferResult<'tcx, ()> {
-        if a.references_error() || b.references_error() {
-            return Ok(InferOk { value: (), obligations: vec![] });
-        }
-        if self.defining_use_anchor.is_some() {
-            let process = |a: Ty<'tcx>, b: Ty<'tcx>| match *a.kind() {
-                ty::Opaque(def_id, substs) => {
-                    if let ty::Opaque(did2, _) = *b.kind() {
-                        // We could accept this, but there are various ways to handle this situation, and we don't
-                        // want to make a decision on it right now. Likely this case is so super rare anyway, that
-                        // no one encounters it in practice.
-                        // It does occur however in `fn fut() -> impl Future<Output = i32> { async { 42 } }`,
-                        // where it is of no concern, so we only check for TAITs.
-                        if let Some(OpaqueTyOrigin::TyAlias) =
-                            self.opaque_type_origin(did2, cause.span)
-                        {
-                            self.tcx
-                                .sess
-                                .struct_span_err(
-                                    cause.span,
-                                    "opaque type's hidden type cannot be another opaque type from the same scope",
-                                )
-                                .span_label(cause.span, "one of the two opaque types used here has to be outside its defining scope")
-                                .span_note(
-                                    self.tcx.def_span(def_id),
-                                    "opaque type whose hidden type is being assigned",
-                                )
-                                .span_note(
-                                    self.tcx.def_span(did2),
-                                    "opaque type being used as hidden type",
-                                )
-                                .emit();
-                        }
-                    }
-                    Some(self.register_hidden_type(
-                        OpaqueTypeKey { def_id, substs },
-                        cause.clone(),
-                        param_env,
-                        b,
-                        // Check that this is `impl Trait` type is
-                        // declared by `parent_def_id` -- i.e., one whose
-                        // value we are inferring.  At present, this is
-                        // always true during the first phase of
-                        // type-check, but not always true later on during
-                        // NLL. Once we support named opaque types more fully,
-                        // this same scenario will be able to arise during all phases.
-                        //
-                        // Here is an example using type alias `impl Trait`
-                        // that indicates the distinction we are checking for:
-                        //
-                        // ```rust
-                        // mod a {
-                        //   pub type Foo = impl Iterator;
-                        //   pub fn make_foo() -> Foo { .. }
-                        // }
-                        //
-                        // mod b {
-                        //   fn foo() -> a::Foo { a::make_foo() }
-                        // }
-                        // ```
-                        //
-                        // Here, the return type of `foo` references an
-                        // `Opaque` indeed, but not one whose value is
-                        // presently being inferred. You can get into a
-                        // similar situation with closure return types
-                        // today:
-                        //
-                        // ```rust
-                        // fn foo() -> impl Iterator { .. }
-                        // fn bar() {
-                        //     let x = || foo(); // returns the Opaque assoc with `foo`
-                        // }
-                        // ```
-                        self.opaque_type_origin(def_id, cause.span)?,
-                    ))
-                }
-                _ => None,
-            };
-            if let Some(res) = process(a, b) {
-                res
-            } else if let Some(res) = process(b, a) {
-                res
-            } else {
-                // Rerun equality check, but this time error out due to
-                // different types.
-                match self.at(cause, param_env).define_opaque_types(false).eq(a, b) {
-                    Ok(_) => span_bug!(
-                        cause.span,
-                        "opaque types are never equal to anything but themselves: {:#?}",
-                        (a, b)
-                    ),
-                    Err(e) => Err(e),
-                }
-            }
-        } else {
-            let (opaque_type, hidden_ty) = match (a.kind(), b.kind()) {
-                (ty::Opaque(..), _) => (a, b),
-                (_, ty::Opaque(..)) => (b, a),
-                types => span_bug!(
-                    cause.span,
-                    "opaque type obligations only work for opaque types: {:#?}",
-                    types
-                ),
-            };
-            let key = opaque_type.expect_opaque_type();
-            let origin = self.opaque_ty_origin_unchecked(key.def_id, cause.span);
-            let prev = self.inner.borrow_mut().opaque_types().register(
-                key,
-                OpaqueHiddenType { ty: hidden_ty, span: cause.span },
-                origin,
-            );
-            match prev {
-                Some(prev) => self.at(cause, param_env).eq(prev, hidden_ty),
-                None => Ok(InferOk { value: (), obligations: vec![] }),
-            }
-        }
+        value: T,
+        value_span: Span,
+    ) -> InferOk<'tcx, T> {
+        debug!(
+            "instantiate_opaque_types(value={:?}, body_id={:?}, \
+             param_env={:?}, value_span={:?})",
+            value, body_id, param_env, value_span,
+        );
+        let mut instantiator =
+            Instantiator { infcx: self, body_id, param_env, value_span, obligations: vec![] };
+        let value = instantiator.instantiate_opaque_types_in_map(value);
+        InferOk { value, obligations: instantiator.obligations }
     }
 
     /// Given the map `opaque_types` containing the opaque
@@ -324,23 +231,51 @@ impl<'a, 'tcx> InferCtxt<'a, 'tcx> {
     /// but this is not necessary, because the opaque type we
     /// create will be allowed to reference `T`. So we only generate a
     /// constraint that `'0: 'a`.
+    ///
+    /// # The `free_region_relations` parameter
+    ///
+    /// The `free_region_relations` argument is used to find the
+    /// "minimum" of the regions supplied to a given opaque type.
+    /// It must be a relation that can answer whether `'a <= 'b`,
+    /// where `'a` and `'b` are regions that appear in the "substs"
+    /// for the opaque type references (the `<'a>` in `Foo1<'a>`).
+    ///
+    /// Note that we do not impose the constraints based on the
+    /// generic regions from the `Foo1` definition (e.g., `'x`). This
+    /// is because the constraints we are imposing here is basically
+    /// the concern of the one generating the constraining type C1,
+    /// which is the current function. It also means that we can
+    /// take "implied bounds" into account in some cases:
+    ///
+    /// ```text
+    /// trait SomeTrait<'a, 'b> { }
+    /// fn foo<'a, 'b>(_: &'a &'b u32) -> impl SomeTrait<'a, 'b> { .. }
+    /// ```
+    ///
+    /// Here, the fact that `'b: 'a` is known only because of the
+    /// implied bounds from the `&'a &'b u32` parameter, and is not
+    /// "inherent" to the opaque type definition.
+    ///
+    /// # Parameters
+    ///
+    /// - `opaque_types` -- the map produced by `instantiate_opaque_types`
+    /// - `free_region_relations` -- something that can be used to relate
+    ///   the free regions (`'a`) that appear in the impl trait.
     #[instrument(level = "debug", skip(self))]
-    pub fn register_member_constraints(
+    pub fn constrain_opaque_type(
         &self,
-        param_env: ty::ParamEnv<'tcx>,
         opaque_type_key: OpaqueTypeKey<'tcx>,
-        concrete_ty: Ty<'tcx>,
-        span: Span,
+        opaque_defn: &OpaqueTypeDecl<'tcx>,
     ) {
         let def_id = opaque_type_key.def_id;
 
         let tcx = self.tcx;
 
-        let concrete_ty = self.resolve_vars_if_possible(concrete_ty);
+        let concrete_ty = self.resolve_vars_if_possible(opaque_defn.concrete_ty);
 
         debug!(?concrete_ty);
 
-        let first_own_region = match self.opaque_ty_origin_unchecked(def_id, span) {
+        let first_own_region = match opaque_defn.origin {
             hir::OpaqueTyOrigin::FnReturn(..) | hir::OpaqueTyOrigin::AsyncFn(..) => {
                 // We lower
                 //
@@ -384,7 +319,7 @@ impl<'a, 'tcx> InferCtxt<'a, 'tcx> {
             op: |r| {
                 self.member_constraint(
                     opaque_type_key.def_id,
-                    span,
+                    opaque_defn.definition_span,
                     concrete_ty,
                     r,
                     &choice_regions,
@@ -393,34 +328,15 @@ impl<'a, 'tcx> InferCtxt<'a, 'tcx> {
         });
     }
 
-    pub fn opaque_ty_obligation(
-        &self,
-        a: Ty<'tcx>,
-        b: Ty<'tcx>,
-        a_is_expected: bool,
-        param_env: ty::ParamEnv<'tcx>,
-        cause: ObligationCause<'tcx>,
-    ) -> PredicateObligation<'tcx> {
-        let (a, b) = if a_is_expected { (a, b) } else { (b, a) };
-        PredicateObligation::new(
-            cause,
-            param_env,
-            self.tcx.mk_predicate(ty::Binder::dummy(ty::PredicateKind::OpaqueType(a, b))),
-        )
-    }
-
-    #[instrument(skip(self), level = "trace")]
-    pub fn opaque_type_origin(&self, opaque_def_id: DefId, span: Span) -> Option<OpaqueTyOrigin> {
-        let def_id = opaque_def_id.as_local()?;
-        let opaque_hir_id = self.tcx.hir().local_def_id_to_hir_id(def_id);
+    fn opaque_type_origin(&self, def_id: LocalDefId) -> Option<hir::OpaqueTyOrigin> {
+        let tcx = self.tcx;
+        let opaque_hir_id = tcx.hir().local_def_id_to_hir_id(def_id);
         let parent_def_id = self.defining_use_anchor?;
-        let item_kind = &self.tcx.hir().expect_item(def_id).kind;
-
+        let item_kind = &tcx.hir().expect_item(def_id).kind;
         let hir::ItemKind::OpaqueTy(hir::OpaqueTy { origin, ..  }) = item_kind else {
             span_bug!(
-                span,
-                "weird opaque type: {:#?}, {:#?}",
-                opaque_def_id,
+                tcx.def_span(def_id),
+                "weird opaque type: {:#?}",
                 item_kind
             )
         };
@@ -431,29 +347,11 @@ impl<'a, 'tcx> InferCtxt<'a, 'tcx> {
             hir::OpaqueTyOrigin::FnReturn(parent) => parent == parent_def_id,
             // Named `type Foo = impl Bar;`
             hir::OpaqueTyOrigin::TyAlias => {
-                may_define_opaque_type(self.tcx, parent_def_id, opaque_hir_id)
+                may_define_opaque_type(tcx, parent_def_id, opaque_hir_id)
             }
         };
-        trace!(?origin);
         in_definition_scope.then_some(*origin)
     }
-
-    #[instrument(skip(self), level = "trace")]
-    fn opaque_ty_origin_unchecked(&self, opaque_def_id: DefId, span: Span) -> OpaqueTyOrigin {
-        let def_id = opaque_def_id.as_local().unwrap();
-        let origin = match self.tcx.hir().expect_item(def_id).kind {
-            hir::ItemKind::OpaqueTy(hir::OpaqueTy { origin, .. }) => origin,
-            ref itemkind => {
-                span_bug!(span, "weird opaque type: {:?}, {:#?}", opaque_def_id, itemkind)
-            }
-        };
-        trace!(?origin);
-        origin
-    }
-
-    pub fn opaque_types(&self) -> OpaqueTypeMap<'tcx> {
-        self.inner.borrow().opaque_type_storage.opaque_types()
-    }
 }
 
 // Visitor that requires that (almost) all regions in the type visited outlive
@@ -528,93 +426,180 @@ where
     }
 }
 
-pub enum UseKind {
-    DefiningUse,
-    OpaqueUse,
+struct Instantiator<'a, 'tcx> {
+    infcx: &'a InferCtxt<'a, 'tcx>,
+    body_id: hir::HirId,
+    param_env: ty::ParamEnv<'tcx>,
+    value_span: Span,
+    obligations: Vec<traits::PredicateObligation<'tcx>>,
 }
 
-impl UseKind {
-    pub fn is_defining(self) -> bool {
-        match self {
-            UseKind::DefiningUse => true,
-            UseKind::OpaqueUse => false,
-        }
+impl<'a, 'tcx> Instantiator<'a, 'tcx> {
+    fn instantiate_opaque_types_in_map<T: TypeFoldable<'tcx>>(&mut self, value: T) -> T {
+        let tcx = self.infcx.tcx;
+        value.fold_with(&mut BottomUpFolder {
+            tcx,
+            ty_op: |ty| {
+                if ty.references_error() {
+                    return tcx.ty_error();
+                } else if let ty::Opaque(def_id, substs) = ty.kind() {
+                    // Check that this is `impl Trait` type is
+                    // declared by `parent_def_id` -- i.e., one whose
+                    // value we are inferring.  At present, this is
+                    // always true during the first phase of
+                    // type-check, but not always true later on during
+                    // NLL. Once we support named opaque types more fully,
+                    // this same scenario will be able to arise during all phases.
+                    //
+                    // Here is an example using type alias `impl Trait`
+                    // that indicates the distinction we are checking for:
+                    //
+                    // ```rust
+                    // mod a {
+                    //   pub type Foo = impl Iterator;
+                    //   pub fn make_foo() -> Foo { .. }
+                    // }
+                    //
+                    // mod b {
+                    //   fn foo() -> a::Foo { a::make_foo() }
+                    // }
+                    // ```
+                    //
+                    // Here, the return type of `foo` references an
+                    // `Opaque` indeed, but not one whose value is
+                    // presently being inferred. You can get into a
+                    // similar situation with closure return types
+                    // today:
+                    //
+                    // ```rust
+                    // fn foo() -> impl Iterator { .. }
+                    // fn bar() {
+                    //     let x = || foo(); // returns the Opaque assoc with `foo`
+                    // }
+                    // ```
+                    if let Some(def_id) = def_id.as_local() {
+                        if let Some(origin) = self.infcx.opaque_type_origin(def_id) {
+                            let opaque_type_key =
+                                OpaqueTypeKey { def_id: def_id.to_def_id(), substs };
+                            return self.fold_opaque_ty(ty, opaque_type_key, origin);
+                        }
+
+                        debug!(
+                            "instantiate_opaque_types_in_map: \
+                             encountered opaque outside its definition scope \
+                             def_id={:?}",
+                            def_id,
+                        );
+                    }
+                }
+
+                ty
+            },
+            lt_op: |lt| lt,
+            ct_op: |ct| ct,
+        })
     }
-}
 
-impl<'a, 'tcx> InferCtxt<'a, 'tcx> {
     #[instrument(skip(self), level = "debug")]
-    fn register_hidden_type(
-        &self,
+    fn fold_opaque_ty(
+        &mut self,
+        ty: Ty<'tcx>,
         opaque_type_key: OpaqueTypeKey<'tcx>,
-        cause: ObligationCause<'tcx>,
-        param_env: ty::ParamEnv<'tcx>,
-        hidden_ty: Ty<'tcx>,
         origin: hir::OpaqueTyOrigin,
-    ) -> InferResult<'tcx, ()> {
-        let tcx = self.tcx;
+    ) -> Ty<'tcx> {
+        let infcx = self.infcx;
+        let tcx = infcx.tcx;
         let OpaqueTypeKey { def_id, substs } = opaque_type_key;
 
+        // Use the same type variable if the exact same opaque type appears more
+        // than once in the return type (e.g., if it's passed to a type alias).
+        if let Some(opaque_defn) = infcx.inner.borrow().opaque_types.get(&opaque_type_key) {
+            debug!("re-using cached concrete type {:?}", opaque_defn.concrete_ty.kind());
+            return opaque_defn.concrete_ty;
+        }
+
+        let ty_var = infcx.next_ty_var(TypeVariableOrigin {
+            kind: TypeVariableOriginKind::TypeInference,
+            span: self.value_span,
+        });
+
         // Ideally, we'd get the span where *this specific `ty` came
         // from*, but right now we just use the span from the overall
         // value being folded. In simple cases like `-> impl Foo`,
         // these are the same span, but not in cases like `-> (impl
         // Foo, impl Bar)`.
-        let span = cause.span;
+        let definition_span = self.value_span;
 
-        let mut obligations = vec![];
-        let prev = self.inner.borrow_mut().opaque_types().register(
-            OpaqueTypeKey { def_id, substs },
-            OpaqueHiddenType { ty: hidden_ty, span },
-            origin,
-        );
-        if let Some(prev) = prev {
-            obligations = self.at(&cause, param_env).eq(prev, hidden_ty)?.obligations;
+        {
+            let mut infcx = self.infcx.inner.borrow_mut();
+            infcx.opaque_types.insert(
+                OpaqueTypeKey { def_id, substs },
+                OpaqueTypeDecl { opaque_type: ty, definition_span, concrete_ty: ty_var, origin },
+            );
+            infcx.opaque_types_vars.insert(ty_var, ty);
         }
 
+        debug!("generated new type inference var {:?}", ty_var.kind());
+
         let item_bounds = tcx.explicit_item_bounds(def_id);
 
+        self.obligations.reserve(item_bounds.len());
         for (predicate, _) in item_bounds {
             debug!(?predicate);
             let predicate = predicate.subst(tcx, substs);
+            debug!(?predicate);
 
             let predicate = predicate.fold_with(&mut BottomUpFolder {
                 tcx,
                 ty_op: |ty| match *ty.kind() {
-                    // We can't normalize associated types from `rustc_infer`,
-                    // but we can eagerly register inference variables for them.
-                    ty::Projection(projection_ty) if !projection_ty.has_escaping_bound_vars() => {
-                        self.infer_projection(
-                            param_env,
-                            projection_ty,
-                            cause.clone(),
-                            0,
-                            &mut obligations,
-                        )
-                    }
                     // Replace all other mentions of the same opaque type with the hidden type,
                     // as the bounds must hold on the hidden type after all.
                     ty::Opaque(def_id2, substs2) if def_id == def_id2 && substs == substs2 => {
-                        hidden_ty
+                        ty_var
+                    }
+                    // Instantiate nested instances of `impl Trait`.
+                    ty::Opaque(..) => self.instantiate_opaque_types_in_map(ty),
+                    _ => ty,
+                },
+                lt_op: |lt| lt,
+                ct_op: |ct| ct,
+            });
+
+            // We can't normalize associated types from `rustc_infer`, but we can eagerly register inference variables for them.
+            let predicate = predicate.fold_with(&mut BottomUpFolder {
+                tcx,
+                ty_op: |ty| match ty.kind() {
+                    ty::Projection(projection_ty) if !projection_ty.has_escaping_bound_vars() => {
+                        infcx.infer_projection(
+                            self.param_env,
+                            *projection_ty,
+                            traits::ObligationCause::misc(self.value_span, self.body_id),
+                            0,
+                            &mut self.obligations,
+                        )
                     }
                     _ => ty,
                 },
                 lt_op: |lt| lt,
                 ct_op: |ct| ct,
             });
+            debug!(?predicate);
 
             if let ty::PredicateKind::Projection(projection) = predicate.kind().skip_binder() {
                 if projection.term.references_error() {
-                    // No point on adding these obligations since there's a type error involved.
-                    return Ok(InferOk { value: (), obligations: vec![] });
+                    return tcx.ty_error();
                 }
-                trace!("{:#?}", projection.term);
             }
+
+            let cause =
+                traits::ObligationCause::new(self.value_span, self.body_id, traits::OpaqueType);
+
             // Require that the predicate holds for the concrete type.
             debug!(?predicate);
-            obligations.push(traits::Obligation::new(cause.clone(), param_env, predicate));
+            self.obligations.push(traits::Obligation::new(cause, self.param_env, predicate));
         }
-        Ok(InferOk { value: (), obligations })
+
+        ty_var
     }
 }
 
diff --git a/compiler/rustc_infer/src/infer/opaque_types/table.rs b/compiler/rustc_infer/src/infer/opaque_types/table.rs
deleted file mode 100644
index 9b8f225ce36..00000000000
--- a/compiler/rustc_infer/src/infer/opaque_types/table.rs
+++ /dev/null
@@ -1,88 +0,0 @@
-use rustc_data_structures::undo_log::UndoLogs;
-use rustc_hir::OpaqueTyOrigin;
-use rustc_middle::ty::{self, OpaqueTypeKey, Ty};
-use rustc_span::DUMMY_SP;
-
-use crate::infer::{InferCtxtUndoLogs, UndoLog};
-
-use super::{OpaqueHiddenType, OpaqueTypeDecl, OpaqueTypeMap};
-
-#[derive(Default, Debug)]
-pub struct OpaqueTypeStorage<'tcx> {
-    // Opaque types found in explicit return types and their
-    // associated fresh inference variable. Writeback resolves these
-    // variables to get the concrete type, which can be used to
-    // 'de-opaque' OpaqueTypeDecl, after typeck is done with all functions.
-    pub opaque_types: OpaqueTypeMap<'tcx>,
-}
-
-impl<'tcx> OpaqueTypeStorage<'tcx> {
-    #[instrument(level = "debug")]
-    pub(crate) fn remove(&mut self, key: OpaqueTypeKey<'tcx>, idx: Option<OpaqueHiddenType<'tcx>>) {
-        if let Some(idx) = idx {
-            self.opaque_types.get_mut(&key).unwrap().hidden_type = idx;
-        } else {
-            match self.opaque_types.remove(&key) {
-                None => bug!("reverted opaque type inference that was never registered: {:?}", key),
-                Some(_) => {}
-            }
-        }
-    }
-
-    pub fn get_decl(&self, key: &OpaqueTypeKey<'tcx>) -> Option<&OpaqueTypeDecl<'tcx>> {
-        self.opaque_types.get(key)
-    }
-
-    pub fn opaque_types(&self) -> OpaqueTypeMap<'tcx> {
-        self.opaque_types.clone()
-    }
-
-    #[instrument(level = "debug")]
-    pub fn take_opaque_types(&mut self) -> OpaqueTypeMap<'tcx> {
-        std::mem::take(&mut self.opaque_types)
-    }
-
-    #[inline]
-    pub(crate) fn with_log<'a>(
-        &'a mut self,
-        undo_log: &'a mut InferCtxtUndoLogs<'tcx>,
-    ) -> OpaqueTypeTable<'a, 'tcx> {
-        OpaqueTypeTable { storage: self, undo_log }
-    }
-}
-
-impl<'tcx> Drop for OpaqueTypeStorage<'tcx> {
-    fn drop(&mut self) {
-        if !self.opaque_types.is_empty() {
-            ty::tls::with(|tcx| {
-                tcx.sess.delay_span_bug(DUMMY_SP, &format!("{:?}", self.opaque_types))
-            });
-        }
-    }
-}
-
-pub struct OpaqueTypeTable<'a, 'tcx> {
-    storage: &'a mut OpaqueTypeStorage<'tcx>,
-
-    undo_log: &'a mut InferCtxtUndoLogs<'tcx>,
-}
-
-impl<'a, 'tcx> OpaqueTypeTable<'a, 'tcx> {
-    #[instrument(skip(self), level = "debug")]
-    pub fn register(
-        &mut self,
-        key: OpaqueTypeKey<'tcx>,
-        hidden_type: OpaqueHiddenType<'tcx>,
-        origin: OpaqueTyOrigin,
-    ) -> Option<Ty<'tcx>> {
-        if let Some(decl) = self.storage.opaque_types.get_mut(&key) {
-            let prev = std::mem::replace(&mut decl.hidden_type, hidden_type);
-            self.undo_log.push(UndoLog::OpaqueTypes(key, Some(prev)));
-            return Some(prev.ty);
-        }
-        let decl = OpaqueTypeDecl { hidden_type, origin };
-        self.storage.opaque_types.insert(key, decl);
-        self.undo_log.push(UndoLog::OpaqueTypes(key, None));
-        None
-    }
-}
diff --git a/compiler/rustc_infer/src/infer/outlives/mod.rs b/compiler/rustc_infer/src/infer/outlives/mod.rs
index b60ffc1878b..03d6c45a653 100644
--- a/compiler/rustc_infer/src/infer/outlives/mod.rs
+++ b/compiler/rustc_infer/src/infer/outlives/mod.rs
@@ -28,7 +28,6 @@ pub fn explicit_outlives_bounds<'tcx>(
             | ty::PredicateKind::TypeOutlives(..)
             | ty::PredicateKind::ConstEvaluatable(..)
             | ty::PredicateKind::ConstEquate(..)
-            | ty::PredicateKind::OpaqueType(..)
             | ty::PredicateKind::TypeWellFormedFromEnv(..) => None,
             ty::PredicateKind::RegionOutlives(ty::OutlivesPredicate(r_a, r_b)) => {
                 Some(OutlivesBound::RegionSubRegion(r_b, r_a))
diff --git a/compiler/rustc_infer/src/infer/outlives/obligations.rs b/compiler/rustc_infer/src/infer/outlives/obligations.rs
index d554d7d935c..a5276afc5bf 100644
--- a/compiler/rustc_infer/src/infer/outlives/obligations.rs
+++ b/compiler/rustc_infer/src/infer/outlives/obligations.rs
@@ -153,7 +153,6 @@ impl<'cx, 'tcx> InferCtxt<'cx, 'tcx> {
     /// This function may have to perform normalizations, and hence it
     /// returns an `InferOk` with subobligations that must be
     /// processed.
-    #[instrument(level = "debug", skip(self, region_bound_pairs_map))]
     pub fn process_registered_region_obligations(
         &self,
         region_bound_pairs_map: &FxHashMap<hir::HirId, RegionBoundPairs<'tcx>>,
@@ -165,6 +164,8 @@ impl<'cx, 'tcx> InferCtxt<'cx, 'tcx> {
             "cannot process registered region obligations in a snapshot"
         );
 
+        debug!(?param_env, "process_registered_region_obligations()");
+
         let my_region_obligations = self.take_registered_region_obligations();
 
         for (body_id, RegionObligation { sup_type, sub_region, origin }) in my_region_obligations {
diff --git a/compiler/rustc_infer/src/infer/sub.rs b/compiler/rustc_infer/src/infer/sub.rs
index e0a8219beed..ccac0efd6c9 100644
--- a/compiler/rustc_infer/src/infer/sub.rs
+++ b/compiler/rustc_infer/src/infer/sub.rs
@@ -2,7 +2,6 @@ use super::combine::{CombineFields, RelationDir};
 use super::SubregionOrigin;
 
 use crate::infer::combine::ConstEquateRelation;
-use crate::infer::{TypeVariableOrigin, TypeVariableOriginKind};
 use crate::traits::Obligation;
 use rustc_middle::ty::fold::TypeFoldable;
 use rustc_middle::ty::relate::{Cause, Relate, RelateResult, TypeRelation};
@@ -75,8 +74,9 @@ impl<'tcx> TypeRelation<'tcx> for Sub<'_, '_, 'tcx> {
         }
     }
 
-    #[instrument(skip(self), level = "debug")]
     fn tys(&mut self, a: Ty<'tcx>, b: Ty<'tcx>) -> RelateResult<'tcx, Ty<'tcx>> {
+        debug!("{}.tys({:?}, {:?})", self.tag(), a, b);
+
         if a == b {
             return Ok(a);
         }
@@ -84,7 +84,6 @@ impl<'tcx> TypeRelation<'tcx> for Sub<'_, '_, 'tcx> {
         let infcx = self.fields.infcx;
         let a = infcx.inner.borrow_mut().type_variables().replace_if_possible(a);
         let b = infcx.inner.borrow_mut().type_variables().replace_if_possible(b);
-
         match (a.kind(), b.kind()) {
             (&ty::Infer(TyVar(_)), &ty::Infer(TyVar(_))) => {
                 // Shouldn't have any LBR here, so we can safely put
@@ -122,40 +121,6 @@ impl<'tcx> TypeRelation<'tcx> for Sub<'_, '_, 'tcx> {
                 Ok(self.tcx().ty_error())
             }
 
-            (&ty::Opaque(a_def_id, _), &ty::Opaque(b_def_id, _)) if a_def_id == b_def_id => {
-                self.fields.infcx.super_combine_tys(self, a, b)?;
-                Ok(a)
-            }
-            (&ty::Opaque(did, ..), _) | (_, &ty::Opaque(did, ..))
-                if self.fields.define_opaque_types && did.is_local() =>
-            {
-                let mut generalize = |ty, ty_is_expected| {
-                    let var = infcx.next_ty_var_id_in_universe(
-                        TypeVariableOrigin {
-                            kind: TypeVariableOriginKind::MiscVariable,
-                            span: self.fields.trace.cause.span,
-                        },
-                        ty::UniverseIndex::ROOT,
-                    );
-                    self.fields.instantiate(ty, RelationDir::SubtypeOf, var, ty_is_expected)?;
-                    Ok(infcx.tcx.mk_ty_var(var))
-                };
-                let (a, b) = if self.a_is_expected { (a, b) } else { (b, a) };
-                let (a, b) = match (a.kind(), b.kind()) {
-                    (&ty::Opaque(..), _) => (a, generalize(b, true)?),
-                    (_, &ty::Opaque(..)) => (generalize(a, false)?, b),
-                    _ => unreachable!(),
-                };
-                self.fields.obligations.push(infcx.opaque_ty_obligation(
-                    a,
-                    b,
-                    true,
-                    self.param_env(),
-                    self.fields.trace.cause.clone(),
-                ));
-                Ok(a)
-            }
-
             _ => {
                 self.fields.infcx.super_combine_tys(self, a, b)?;
                 Ok(a)
diff --git a/compiler/rustc_infer/src/infer/undo_log.rs b/compiler/rustc_infer/src/infer/undo_log.rs
index 02b15baf8fb..89db8f464b4 100644
--- a/compiler/rustc_infer/src/infer/undo_log.rs
+++ b/compiler/rustc_infer/src/infer/undo_log.rs
@@ -4,15 +4,13 @@ use rustc_data_structures::snapshot_vec as sv;
 use rustc_data_structures::undo_log::{Rollback, UndoLogs};
 use rustc_data_structures::unify as ut;
 use rustc_middle::infer::unify_key::RegionVidKey;
-use rustc_middle::ty::{self, OpaqueTypeKey};
+use rustc_middle::ty;
 
 use crate::{
     infer::{region_constraints, type_variable, InferCtxtInner},
     traits,
 };
 
-use super::opaque_types::OpaqueHiddenType;
-
 pub struct Snapshot<'tcx> {
     pub(crate) undo_len: usize,
     _marker: PhantomData<&'tcx ()>,
@@ -20,7 +18,6 @@ pub struct Snapshot<'tcx> {
 
 /// Records the "undo" data for a single operation that affects some form of inference variable.
 pub(crate) enum UndoLog<'tcx> {
-    OpaqueTypes(OpaqueTypeKey<'tcx>, Option<OpaqueHiddenType<'tcx>>),
     TypeVariables(type_variable::UndoLog<'tcx>),
     ConstUnificationTable(sv::UndoLog<ut::Delegate<ty::ConstVid<'tcx>>>),
     IntUnificationTable(sv::UndoLog<ut::Delegate<ty::IntVid>>),
@@ -67,7 +64,6 @@ impl_from! {
 impl<'tcx> Rollback<UndoLog<'tcx>> for InferCtxtInner<'tcx> {
     fn reverse(&mut self, undo: UndoLog<'tcx>) {
         match undo {
-            UndoLog::OpaqueTypes(key, idx) => self.opaque_type_storage.remove(key, idx),
             UndoLog::TypeVariables(undo) => self.type_variable_storage.reverse(undo),
             UndoLog::ConstUnificationTable(undo) => self.const_unification_storage.reverse(undo),
             UndoLog::IntUnificationTable(undo) => self.int_unification_storage.reverse(undo),
diff --git a/compiler/rustc_infer/src/traits/util.rs b/compiler/rustc_infer/src/traits/util.rs
index 6600d5e4d02..674c75fdee5 100644
--- a/compiler/rustc_infer/src/traits/util.rs
+++ b/compiler/rustc_infer/src/traits/util.rs
@@ -167,9 +167,6 @@ impl<'tcx> Elaborator<'tcx> {
                 // Currently, we do not elaborate WF predicates,
                 // although we easily could.
             }
-            ty::PredicateKind::OpaqueType(..) => {
-                todo!("{:#?}", obligation)
-            }
             ty::PredicateKind::ObjectSafe(..) => {
                 // Currently, we do not elaborate object-safe
                 // predicates.