about summary refs log tree commit diff
path: root/compiler/rustc_next_trait_solver/src
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/rustc_next_trait_solver/src')
-rw-r--r--compiler/rustc_next_trait_solver/src/lib.rs3
-rw-r--r--compiler/rustc_next_trait_solver/src/relate.rs15
-rw-r--r--compiler/rustc_next_trait_solver/src/relate/combine.rs34
-rw-r--r--compiler/rustc_next_trait_solver/src/solve/assembly/mod.rs20
-rw-r--r--compiler/rustc_next_trait_solver/src/solve/eval_ctxt/canonical.rs2
-rw-r--r--compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs124
-rw-r--r--compiler/rustc_next_trait_solver/src/solve/mod.rs11
-rw-r--r--compiler/rustc_next_trait_solver/src/solve/normalizes_to/mod.rs65
-rw-r--r--compiler/rustc_next_trait_solver/src/solve/normalizes_to/opaque_types.rs34
-rw-r--r--compiler/rustc_next_trait_solver/src/solve/search_graph.rs3
-rw-r--r--compiler/rustc_next_trait_solver/src/solve/trait_goals.rs11
11 files changed, 188 insertions, 134 deletions
diff --git a/compiler/rustc_next_trait_solver/src/lib.rs b/compiler/rustc_next_trait_solver/src/lib.rs
index ca140500e2c..d67ae2550d9 100644
--- a/compiler/rustc_next_trait_solver/src/lib.rs
+++ b/compiler/rustc_next_trait_solver/src/lib.rs
@@ -5,13 +5,12 @@
 //! So if you got to this crate from the old solver, it's totally normal.
 
 // tidy-alphabetical-start
-#![cfg_attr(not(bootstrap), allow(rustc::usage_of_type_ir_inherent))]
+#![allow(rustc::usage_of_type_ir_inherent)]
 #![warn(unreachable_pub)]
 // tidy-alphabetical-end
 
 pub mod canonicalizer;
 pub mod coherence;
 pub mod delegate;
-pub mod relate;
 pub mod resolve;
 pub mod solve;
diff --git a/compiler/rustc_next_trait_solver/src/relate.rs b/compiler/rustc_next_trait_solver/src/relate.rs
deleted file mode 100644
index db819961bbd..00000000000
--- a/compiler/rustc_next_trait_solver/src/relate.rs
+++ /dev/null
@@ -1,15 +0,0 @@
-pub use rustc_type_ir::relate::*;
-
-pub mod combine;
-
-/// Whether aliases should be related structurally or not. Used
-/// to adjust the behavior of generalization and combine.
-///
-/// This should always be `No` unless in a few special-cases when
-/// instantiating canonical responses and in the new solver. Each
-/// such case should have a comment explaining why it is used.
-#[derive(Debug, Copy, Clone)]
-pub enum StructurallyRelateAliases {
-    Yes,
-    No,
-}
diff --git a/compiler/rustc_next_trait_solver/src/relate/combine.rs b/compiler/rustc_next_trait_solver/src/relate/combine.rs
deleted file mode 100644
index 96968327d8e..00000000000
--- a/compiler/rustc_next_trait_solver/src/relate/combine.rs
+++ /dev/null
@@ -1,34 +0,0 @@
-pub use rustc_type_ir::relate::*;
-use rustc_type_ir::solve::Goal;
-use rustc_type_ir::{InferCtxtLike, Interner, Upcast};
-
-use super::StructurallyRelateAliases;
-
-pub trait PredicateEmittingRelation<Infcx, I = <Infcx as InferCtxtLike>::Interner>:
-    TypeRelation<I>
-where
-    Infcx: InferCtxtLike<Interner = I>,
-    I: Interner,
-{
-    fn span(&self) -> I::Span;
-
-    fn param_env(&self) -> I::ParamEnv;
-
-    /// Whether aliases should be related structurally. This is pretty much
-    /// always `No` unless you're equating in some specific locations of the
-    /// new solver. See the comments in these use-cases for more details.
-    fn structurally_relate_aliases(&self) -> StructurallyRelateAliases;
-
-    /// Register obligations that must hold in order for this relation to hold
-    fn register_goals(&mut self, obligations: impl IntoIterator<Item = Goal<I, I::Predicate>>);
-
-    /// Register predicates that must hold in order for this relation to hold.
-    /// This uses the default `param_env` of the obligation.
-    fn register_predicates(
-        &mut self,
-        obligations: impl IntoIterator<Item: Upcast<I, I::Predicate>>,
-    );
-
-    /// Register `AliasRelate` obligation(s) that both types must be related to each other.
-    fn register_alias_relate_predicate(&mut self, a: I::Ty, b: I::Ty);
-}
diff --git a/compiler/rustc_next_trait_solver/src/solve/assembly/mod.rs b/compiler/rustc_next_trait_solver/src/solve/assembly/mod.rs
index cebeef76bfc..c9c0d6391fc 100644
--- a/compiler/rustc_next_trait_solver/src/solve/assembly/mod.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/assembly/mod.rs
@@ -6,6 +6,7 @@ use derive_where::derive_where;
 use rustc_type_ir::fold::TypeFoldable;
 use rustc_type_ir::inherent::*;
 use rustc_type_ir::lang_items::TraitSolverLangItem;
+use rustc_type_ir::solve::inspect;
 use rustc_type_ir::visit::TypeVisitableExt as _;
 use rustc_type_ir::{self as ty, Interner, Upcast as _, elaborate};
 use tracing::{debug, instrument};
@@ -288,6 +289,25 @@ where
         let Ok(normalized_self_ty) =
             self.structurally_normalize_ty(goal.param_env, goal.predicate.self_ty())
         else {
+            // FIXME: We register a fake candidate when normalization fails so that
+            // we can point at the reason for *why*. I'm tempted to say that this
+            // is the wrong way to do this, though.
+            let result =
+                self.probe(|&result| inspect::ProbeKind::RigidAlias { result }).enter(|this| {
+                    let normalized_ty = this.next_ty_infer();
+                    let alias_relate_goal = Goal::new(
+                        this.cx(),
+                        goal.param_env,
+                        ty::PredicateKind::AliasRelate(
+                            goal.predicate.self_ty().into(),
+                            normalized_ty.into(),
+                            ty::AliasRelationDirection::Equate,
+                        ),
+                    );
+                    this.add_goal(GoalSource::AliasWellFormed, alias_relate_goal);
+                    this.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS)
+                });
+            assert_eq!(result, Err(NoSolution));
             return vec![];
         };
 
diff --git a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/canonical.rs b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/canonical.rs
index 252a9ed1a2e..fdefec33eeb 100644
--- a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/canonical.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/canonical.rs
@@ -14,6 +14,7 @@ use std::iter;
 use rustc_index::IndexVec;
 use rustc_type_ir::fold::TypeFoldable;
 use rustc_type_ir::inherent::*;
+use rustc_type_ir::relate::solver_relating::RelateExt;
 use rustc_type_ir::{self as ty, Canonical, CanonicalVarValues, InferCtxtLike, Interner};
 use tracing::{instrument, trace};
 
@@ -443,7 +444,6 @@ where
     for &arg in &state.value.var_values.var_values.as_slice()
         [orig_values.len()..state.value.var_values.len()]
     {
-        // FIXME: This is so ugly.
         let unconstrained = delegate.fresh_var_for_kind_with_span(arg, span);
         orig_values.push(unconstrained);
     }
diff --git a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs
index ffa800348f2..0f8b796d602 100644
--- a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs
@@ -4,9 +4,11 @@ use derive_where::derive_where;
 #[cfg(feature = "nightly")]
 use rustc_macros::{HashStable_NoContext, TyDecodable, TyEncodable};
 use rustc_type_ir::data_structures::{HashMap, HashSet, ensure_sufficient_stack};
+use rustc_type_ir::fast_reject::DeepRejectCtxt;
 use rustc_type_ir::fold::{TypeFoldable, TypeFolder, TypeSuperFoldable};
 use rustc_type_ir::inherent::*;
 use rustc_type_ir::relate::Relate;
+use rustc_type_ir::relate::solver_relating::RelateExt;
 use rustc_type_ir::visit::{TypeSuperVisitable, TypeVisitable, TypeVisitableExt, TypeVisitor};
 use rustc_type_ir::{self as ty, CanonicalVarValues, InferCtxtLike, Interner};
 use rustc_type_ir_macros::{Lift_Generic, TypeFoldable_Generic, TypeVisitable_Generic};
@@ -17,8 +19,8 @@ use crate::delegate::SolverDelegate;
 use crate::solve::inspect::{self, ProofTreeBuilder};
 use crate::solve::search_graph::SearchGraph;
 use crate::solve::{
-    CanonicalInput, CanonicalResponse, Certainty, FIXPOINT_STEP_LIMIT, Goal, GoalEvaluationKind,
-    GoalSource, NestedNormalizationGoals, NoSolution, PredefinedOpaquesData, QueryResult,
+    CanonicalInput, Certainty, FIXPOINT_STEP_LIMIT, Goal, GoalEvaluationKind, GoalSource,
+    HasChanged, NestedNormalizationGoals, NoSolution, PredefinedOpaquesData, QueryResult,
     SolverMode,
 };
 
@@ -91,7 +93,6 @@ where
 #[derive_where(Clone, Debug, Default; I: Interner)]
 #[derive(TypeVisitable_Generic, TypeFoldable_Generic, Lift_Generic)]
 #[cfg_attr(feature = "nightly", derive(TyDecodable, TyEncodable, HashStable_NoContext))]
-// FIXME: This can be made crate-private once `EvalCtxt` also lives in this crate.
 struct NestedGoals<I: Interner> {
     /// These normalizes-to goals are treated specially during the evaluation
     /// loop. In each iteration we take the RHS of the projection, replace it with
@@ -126,11 +127,31 @@ pub enum GenerateProofTree {
 }
 
 pub trait SolverDelegateEvalExt: SolverDelegate {
+    /// Evaluates a goal from **outside** of the trait solver.
+    ///
+    /// Using this while inside of the solver is wrong as it uses a new
+    /// search graph which would break cycle detection.
     fn evaluate_root_goal(
         &self,
         goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
         generate_proof_tree: GenerateProofTree,
-    ) -> (Result<(bool, Certainty), NoSolution>, Option<inspect::GoalEvaluation<Self::Interner>>);
+    ) -> (
+        Result<(HasChanged, Certainty), NoSolution>,
+        Option<inspect::GoalEvaluation<Self::Interner>>,
+    );
+
+    /// Check whether evaluating `goal` with a depth of `root_depth` may
+    /// succeed. This only returns `false` if the goal is guaranteed to
+    /// not hold. In case evaluation overflows and fails with ambiguity this
+    /// returns `true`.
+    ///
+    /// This is only intended to be used as a performance optimization
+    /// in coherence checking.
+    fn root_goal_may_hold_with_depth(
+        &self,
+        root_depth: usize,
+        goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
+    ) -> bool;
 
     // FIXME: This is only exposed because we need to use it in `analyse.rs`
     // which is not yet uplifted. Once that's done, we should remove this.
@@ -139,7 +160,7 @@ pub trait SolverDelegateEvalExt: SolverDelegate {
         goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
         generate_proof_tree: GenerateProofTree,
     ) -> (
-        Result<(NestedNormalizationGoals<Self::Interner>, bool, Certainty), NoSolution>,
+        Result<(NestedNormalizationGoals<Self::Interner>, HasChanged, Certainty), NoSolution>,
         Option<inspect::GoalEvaluation<Self::Interner>>,
     );
 }
@@ -149,31 +170,41 @@ where
     D: SolverDelegate<Interner = I>,
     I: Interner,
 {
-    /// Evaluates a goal from **outside** of the trait solver.
-    ///
-    /// Using this while inside of the solver is wrong as it uses a new
-    /// search graph which would break cycle detection.
     #[instrument(level = "debug", skip(self))]
     fn evaluate_root_goal(
         &self,
         goal: Goal<I, I::Predicate>,
         generate_proof_tree: GenerateProofTree,
-    ) -> (Result<(bool, Certainty), NoSolution>, Option<inspect::GoalEvaluation<I>>) {
-        EvalCtxt::enter_root(self, generate_proof_tree, |ecx| {
+    ) -> (Result<(HasChanged, Certainty), NoSolution>, Option<inspect::GoalEvaluation<I>>) {
+        EvalCtxt::enter_root(self, self.cx().recursion_limit(), generate_proof_tree, |ecx| {
             ecx.evaluate_goal(GoalEvaluationKind::Root, GoalSource::Misc, goal)
         })
     }
 
+    fn root_goal_may_hold_with_depth(
+        &self,
+        root_depth: usize,
+        goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
+    ) -> bool {
+        self.probe(|| {
+            EvalCtxt::enter_root(self, root_depth, GenerateProofTree::No, |ecx| {
+                ecx.evaluate_goal(GoalEvaluationKind::Root, GoalSource::Misc, goal)
+            })
+            .0
+        })
+        .is_ok()
+    }
+
     #[instrument(level = "debug", skip(self))]
     fn evaluate_root_goal_raw(
         &self,
         goal: Goal<I, I::Predicate>,
         generate_proof_tree: GenerateProofTree,
     ) -> (
-        Result<(NestedNormalizationGoals<I>, bool, Certainty), NoSolution>,
+        Result<(NestedNormalizationGoals<I>, HasChanged, Certainty), NoSolution>,
         Option<inspect::GoalEvaluation<I>>,
     ) {
-        EvalCtxt::enter_root(self, generate_proof_tree, |ecx| {
+        EvalCtxt::enter_root(self, self.cx().recursion_limit(), generate_proof_tree, |ecx| {
             ecx.evaluate_goal_raw(GoalEvaluationKind::Root, GoalSource::Misc, goal)
         })
     }
@@ -197,10 +228,11 @@ where
     /// over using this manually (such as [`SolverDelegateEvalExt::evaluate_root_goal`]).
     pub(super) fn enter_root<R>(
         delegate: &D,
+        root_depth: usize,
         generate_proof_tree: GenerateProofTree,
         f: impl FnOnce(&mut EvalCtxt<'_, D>) -> R,
     ) -> (R, Option<inspect::GoalEvaluation<I>>) {
-        let mut search_graph = SearchGraph::new(delegate.solver_mode());
+        let mut search_graph = SearchGraph::new(delegate.solver_mode(), root_depth);
 
         let mut ecx = EvalCtxt {
             delegate,
@@ -339,7 +371,7 @@ where
         goal_evaluation_kind: GoalEvaluationKind,
         source: GoalSource,
         goal: Goal<I, I::Predicate>,
-    ) -> Result<(bool, Certainty), NoSolution> {
+    ) -> Result<(HasChanged, Certainty), NoSolution> {
         let (normalization_nested_goals, has_changed, certainty) =
             self.evaluate_goal_raw(goal_evaluation_kind, source, goal)?;
         assert!(normalization_nested_goals.is_empty());
@@ -360,7 +392,7 @@ where
         goal_evaluation_kind: GoalEvaluationKind,
         _source: GoalSource,
         goal: Goal<I, I::Predicate>,
-    ) -> Result<(NestedNormalizationGoals<I>, bool, Certainty), NoSolution> {
+    ) -> Result<(NestedNormalizationGoals<I>, HasChanged, Certainty), NoSolution> {
         let (orig_values, canonical_goal) = self.canonicalize_goal(goal);
         let mut goal_evaluation =
             self.inspect.new_goal_evaluation(goal, &orig_values, goal_evaluation_kind);
@@ -378,12 +410,18 @@ where
             Ok(response) => response,
         };
 
-        let has_changed = !response.value.var_values.is_identity_modulo_regions()
-            || !response.value.external_constraints.opaque_types.is_empty();
+        let has_changed = if !response.value.var_values.is_identity_modulo_regions()
+            || !response.value.external_constraints.opaque_types.is_empty()
+        {
+            HasChanged::Yes
+        } else {
+            HasChanged::No
+        };
 
         let (normalization_nested_goals, certainty) =
             self.instantiate_and_apply_query_response(goal.param_env, orig_values, response);
         self.inspect.goal_evaluation(goal_evaluation);
+
         // FIXME: We previously had an assert here that checked that recomputing
         // a goal after applying its constraints did not change its response.
         //
@@ -552,7 +590,7 @@ where
         for (source, goal) in goals.goals {
             let (has_changed, certainty) =
                 self.evaluate_goal(GoalEvaluationKind::Nested, source, goal)?;
-            if has_changed {
+            if has_changed == HasChanged::Yes {
                 unchanged_certainty = None;
             }
 
@@ -835,7 +873,7 @@ where
         lhs: T,
         rhs: T,
     ) -> Result<Vec<Goal<I, I::Predicate>>, NoSolution> {
-        self.delegate.relate(param_env, lhs, ty::Variance::Invariant, rhs)
+        Ok(self.delegate.relate(param_env, lhs, ty::Variance::Invariant, rhs)?)
     }
 
     pub(super) fn instantiate_binder_with_infer<T: TypeFoldable<I> + Copy>(
@@ -945,45 +983,27 @@ where
             hidden_ty,
             &mut goals,
         );
-        self.add_goals(GoalSource::Misc, goals);
+        self.add_goals(GoalSource::AliasWellFormed, goals);
     }
 
     // Do something for each opaque/hidden pair defined with `def_id` in the
     // current inference context.
-    pub(super) fn unify_existing_opaque_tys(
+    pub(super) fn probe_existing_opaque_ty(
         &mut self,
-        param_env: I::ParamEnv,
         key: ty::OpaqueTypeKey<I>,
-        ty: I::Ty,
-    ) -> Vec<CanonicalResponse<I>> {
-        // FIXME: Super inefficient to be cloning this...
-        let opaques = self.delegate.clone_opaque_types_for_query_response();
-
-        let mut values = vec![];
-        for (candidate_key, candidate_ty) in opaques {
-            if candidate_key.def_id != key.def_id {
-                continue;
-            }
-            values.extend(
-                self.probe(|result| inspect::ProbeKind::OpaqueTypeStorageLookup {
-                    result: *result,
-                })
-                .enter(|ecx| {
-                    for (a, b) in std::iter::zip(candidate_key.args.iter(), key.args.iter()) {
-                        ecx.eq(param_env, a, b)?;
-                    }
-                    ecx.eq(param_env, candidate_ty, ty)?;
-                    ecx.add_item_bounds_for_hidden_type(
-                        candidate_key.def_id.into(),
-                        candidate_key.args,
-                        param_env,
-                        candidate_ty,
-                    );
-                    ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
-                }),
+    ) -> Option<(ty::OpaqueTypeKey<I>, I::Ty)> {
+        let mut matching =
+            self.delegate.clone_opaque_types_for_query_response().into_iter().filter(
+                |(candidate_key, _)| {
+                    candidate_key.def_id == key.def_id
+                        && DeepRejectCtxt::relate_rigid_rigid(self.cx())
+                            .args_may_unify(candidate_key.args, key.args)
+                },
             );
-        }
-        values
+        let first = matching.next();
+        let second = matching.next();
+        assert_eq!(second, None);
+        first
     }
 
     // Try to evaluate a const, or return `None` if the const is too generic.
diff --git a/compiler/rustc_next_trait_solver/src/solve/mod.rs b/compiler/rustc_next_trait_solver/src/solve/mod.rs
index 309ab7f28d1..8fe39bb4ee1 100644
--- a/compiler/rustc_next_trait_solver/src/solve/mod.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/mod.rs
@@ -10,9 +10,6 @@
 //!
 //! For a high-level overview of how this solver works, check out the relevant
 //! section of the rustc-dev-guide.
-//!
-//! FIXME(@lcnr): Write that section. If you read this before then ask me
-//! about it on zulip.
 
 mod alias_relate;
 mod assembly;
@@ -48,6 +45,14 @@ enum GoalEvaluationKind {
     Nested,
 }
 
+/// Whether evaluating this goal ended up changing the
+/// inference state.
+#[derive(PartialEq, Eq, Debug, Hash, Clone, Copy)]
+pub enum HasChanged {
+    Yes,
+    No,
+}
+
 // FIXME(trait-system-refactor-initiative#117): we don't detect whether a response
 // ended up pulling down any universes.
 fn has_no_inference_or_external_constraints<I: Interner>(
diff --git a/compiler/rustc_next_trait_solver/src/solve/normalizes_to/mod.rs b/compiler/rustc_next_trait_solver/src/solve/normalizes_to/mod.rs
index fc9c634942b..4d8b193ee49 100644
--- a/compiler/rustc_next_trait_solver/src/solve/normalizes_to/mod.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/normalizes_to/mod.rs
@@ -15,7 +15,7 @@ use crate::solve::assembly::{self, Candidate};
 use crate::solve::inspect::ProbeKind;
 use crate::solve::{
     BuiltinImplSource, CandidateSource, Certainty, EvalCtxt, Goal, GoalSource, MaybeCause,
-    NoSolution, QueryResult,
+    NoSolution, QueryResult, Reveal,
 };
 
 impl<D, I> EvalCtxt<'_, D>
@@ -37,10 +37,61 @@ where
         match normalize_result {
             Ok(res) => Ok(res),
             Err(NoSolution) => {
-                let Goal { param_env, predicate: NormalizesTo { alias, term } } = goal;
-                self.relate_rigid_alias_non_alias(param_env, alias, ty::Invariant, term)?;
-                self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
+                self.probe(|&result| ProbeKind::RigidAlias { result }).enter(|this| {
+                    let Goal { param_env, predicate: NormalizesTo { alias, term } } = goal;
+                    this.add_rigid_constraints(param_env, alias)?;
+                    this.relate_rigid_alias_non_alias(param_env, alias, ty::Invariant, term)?;
+                    this.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
+                })
+            }
+        }
+    }
+
+    /// Register any obligations that are used to validate that an alias should be
+    /// treated as rigid.
+    ///
+    /// An alias may be considered rigid if it fails normalization, but we also don't
+    /// want to consider aliases that are not well-formed to be rigid simply because
+    /// they fail normalization.
+    ///
+    /// For example, some `<T as Trait>::Assoc` where `T: Trait` does not hold, or an
+    /// opaque type whose hidden type doesn't actually satisfy the opaque item bounds.
+    fn add_rigid_constraints(
+        &mut self,
+        param_env: I::ParamEnv,
+        rigid_alias: ty::AliasTerm<I>,
+    ) -> Result<(), NoSolution> {
+        let cx = self.cx();
+        match rigid_alias.kind(cx) {
+            // Projections are rigid only if their trait ref holds,
+            // and the GAT where-clauses hold.
+            ty::AliasTermKind::ProjectionTy | ty::AliasTermKind::ProjectionConst => {
+                let trait_ref = rigid_alias.trait_ref(cx);
+                self.add_goal(GoalSource::AliasWellFormed, Goal::new(cx, param_env, trait_ref));
+                Ok(())
+            }
+            ty::AliasTermKind::OpaqueTy => {
+                match param_env.reveal() {
+                    // In user-facing mode, paques are only rigid if we may not define it.
+                    Reveal::UserFacing => {
+                        if rigid_alias
+                            .def_id
+                            .as_local()
+                            .is_some_and(|def_id| self.can_define_opaque_ty(def_id))
+                        {
+                            Err(NoSolution)
+                        } else {
+                            Ok(())
+                        }
+                    }
+                    // Opaques are never rigid in reveal-all mode.
+                    Reveal::All => Err(NoSolution),
+                }
             }
+            // FIXME(generic_const_exprs): we would need to support generic consts here
+            ty::AliasTermKind::UnevaluatedConst => Err(NoSolution),
+            // Inherent and weak types are never rigid. This type must not be well-formed.
+            ty::AliasTermKind::WeakTy | ty::AliasTermKind::InherentTy => Err(NoSolution),
         }
     }
 
@@ -124,6 +175,7 @@ where
                     ecx.instantiate_normalizes_to_term(goal, assumption_projection_pred.term);
 
                     // Add GAT where clauses from the trait's definition
+                    // FIXME: We don't need these, since these are the type's own WF obligations.
                     ecx.add_goals(
                         GoalSource::Misc,
                         cx.own_predicates_of(goal.predicate.def_id())
@@ -179,7 +231,8 @@ where
                 .map(|pred| goal.with(cx, pred));
             ecx.add_goals(GoalSource::ImplWhereBound, where_clause_bounds);
 
-            // Add GAT where clauses from the trait's definition
+            // Add GAT where clauses from the trait's definition.
+            // FIXME: We don't need these, since these are the type's own WF obligations.
             ecx.add_goals(
                 GoalSource::Misc,
                 cx.own_predicates_of(goal.predicate.def_id())
@@ -899,7 +952,7 @@ where
                 for ty in types.iter() {
                     // We can't find the intersection if the types used are generic.
                     //
-                    // FIXME(effects) do we want to look at where clauses to get some
+                    // FIXME(effects): do we want to look at where clauses to get some
                     // clue for the case where generic types are being used?
                     let Some(kind) = ty::EffectKind::try_from_ty(cx, ty) else {
                         return Err(NoSolution);
diff --git a/compiler/rustc_next_trait_solver/src/solve/normalizes_to/opaque_types.rs b/compiler/rustc_next_trait_solver/src/solve/normalizes_to/opaque_types.rs
index 6a0703c5313..f8d51f304f3 100644
--- a/compiler/rustc_next_trait_solver/src/solve/normalizes_to/opaque_types.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/normalizes_to/opaque_types.rs
@@ -7,7 +7,9 @@ use rustc_type_ir::inherent::*;
 use rustc_type_ir::{self as ty, Interner};
 
 use crate::delegate::SolverDelegate;
-use crate::solve::{Certainty, EvalCtxt, Goal, NoSolution, QueryResult, Reveal, SolverMode};
+use crate::solve::{
+    Certainty, EvalCtxt, Goal, NoSolution, QueryResult, Reveal, SolverMode, inspect,
+};
 
 impl<D, I> EvalCtxt<'_, D>
 where
@@ -52,14 +54,28 @@ where
                 //
                 // If that fails, we insert `expected` as a new hidden type instead of
                 // eagerly emitting an error.
-                let matches =
-                    self.unify_existing_opaque_tys(goal.param_env, opaque_type_key, expected);
-                if !matches.is_empty() {
-                    if let Some(response) = self.try_merge_responses(&matches) {
-                        return Ok(response);
-                    } else {
-                        return self.flounder(&matches);
-                    }
+                let existing = self.probe_existing_opaque_ty(opaque_type_key);
+                if let Some((candidate_key, candidate_ty)) = existing {
+                    return self
+                        .probe(|result| inspect::ProbeKind::OpaqueTypeStorageLookup {
+                            result: *result,
+                        })
+                        .enter(|ecx| {
+                            for (a, b) in std::iter::zip(
+                                candidate_key.args.iter(),
+                                opaque_type_key.args.iter(),
+                            ) {
+                                ecx.eq(goal.param_env, a, b)?;
+                            }
+                            ecx.eq(goal.param_env, candidate_ty, expected)?;
+                            ecx.add_item_bounds_for_hidden_type(
+                                candidate_key.def_id.into(),
+                                candidate_key.args,
+                                goal.param_env,
+                                candidate_ty,
+                            );
+                            ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
+                        });
                 }
 
                 // Otherwise, define a new opaque type
diff --git a/compiler/rustc_next_trait_solver/src/solve/search_graph.rs b/compiler/rustc_next_trait_solver/src/solve/search_graph.rs
index e47cc03f5ad..0e3f179b0c8 100644
--- a/compiler/rustc_next_trait_solver/src/solve/search_graph.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/search_graph.rs
@@ -40,9 +40,6 @@ where
     }
 
     const DIVIDE_AVAILABLE_DEPTH_ON_OVERFLOW: usize = 4;
-    fn recursion_limit(cx: I) -> usize {
-        cx.recursion_limit()
-    }
 
     fn initial_provisional_result(
         cx: I,
diff --git a/compiler/rustc_next_trait_solver/src/solve/trait_goals.rs b/compiler/rustc_next_trait_solver/src/solve/trait_goals.rs
index 2074bdec485..5828b2ecf34 100644
--- a/compiler/rustc_next_trait_solver/src/solve/trait_goals.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/trait_goals.rs
@@ -108,7 +108,6 @@ where
         ecx: &mut EvalCtxt<'_, D>,
         _guar: I::ErrorGuaranteed,
     ) -> Result<Candidate<I>, NoSolution> {
-        // FIXME: don't need to enter a probe here.
         ecx.probe_builtin_trait_candidate(BuiltinImplSource::Misc)
             .enter(|ecx| ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes))
     }
@@ -463,7 +462,6 @@ where
         // Async coroutine unconditionally implement `Future`
         // Technically, we need to check that the future output type is Sized,
         // but that's already proven by the coroutine being WF.
-        // FIXME: use `consider_implied`
         ecx.probe_builtin_trait_candidate(BuiltinImplSource::Misc)
             .enter(|ecx| ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes))
     }
@@ -489,7 +487,6 @@ where
         // Gen coroutines unconditionally implement `Iterator`
         // Technically, we need to check that the iterator output type is Sized,
         // but that's already proven by the coroutines being WF.
-        // FIXME: use `consider_implied`
         ecx.probe_builtin_trait_candidate(BuiltinImplSource::Misc)
             .enter(|ecx| ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes))
     }
@@ -512,8 +509,7 @@ where
             return Err(NoSolution);
         }
 
-        // Gen coroutines unconditionally implement `FusedIterator`
-        // FIXME: use `consider_implied`
+        // Gen coroutines unconditionally implement `FusedIterator`.
         ecx.probe_builtin_trait_candidate(BuiltinImplSource::Misc)
             .enter(|ecx| ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes))
     }
@@ -539,7 +535,6 @@ where
         // Gen coroutines unconditionally implement `Iterator`
         // Technically, we need to check that the iterator output type is Sized,
         // but that's already proven by the coroutines being WF.
-        // FIXME: use `consider_implied`
         ecx.probe_builtin_trait_candidate(BuiltinImplSource::Misc)
             .enter(|ecx| ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes))
     }
@@ -610,7 +605,7 @@ where
             return Err(NoSolution);
         }
 
-        // FIXME(-Znext-solver): Implement this when we get const working in the new solver
+        // FIXME(effects): Implement this when we get const working in the new solver
 
         // `Destruct` is automatically implemented for every type in
         // non-const environments.
@@ -631,8 +626,6 @@ where
             return Err(NoSolution);
         }
 
-        // FIXME: This actually should destructure the `Result` we get from transmutability and
-        // register candidates. We probably need to register >1 since we may have an OR of ANDs.
         ecx.probe_builtin_trait_candidate(BuiltinImplSource::Misc).enter(|ecx| {
             let certainty = ecx.is_transmutable(
                 goal.param_env,