rustc_next_trait_solver/solve/eval_ctxt/
mod.rs

Help
1use std::ops::ControlFlow;
2
3use derive_where::derive_where;
4#[cfg(feature = "nightly")]
5use rustc_macros::{HashStable_NoContext, TyDecodable, TyEncodable};
6use rustc_type_ir::data_structures::{HashMap, HashSet, ensure_sufficient_stack};
7use rustc_type_ir::fast_reject::DeepRejectCtxt;
8use rustc_type_ir::fold::{TypeFoldable, TypeFolder, TypeSuperFoldable};
9use rustc_type_ir::inherent::*;
10use rustc_type_ir::relate::Relate;
11use rustc_type_ir::relate::solver_relating::RelateExt;
12use rustc_type_ir::visit::{TypeSuperVisitable, TypeVisitable, TypeVisitableExt, TypeVisitor};
13use rustc_type_ir::{self as ty, CanonicalVarValues, InferCtxtLike, Interner, TypingMode};
14use rustc_type_ir_macros::{Lift_Generic, TypeFoldable_Generic, TypeVisitable_Generic};
15use tracing::{instrument, trace};
16
17use crate::coherence;
18use crate::delegate::SolverDelegate;
19use crate::solve::inspect::{self, ProofTreeBuilder};
20use crate::solve::search_graph::SearchGraph;
21use crate::solve::{
22    CanonicalInput, Certainty, FIXPOINT_STEP_LIMIT, Goal, GoalEvaluationKind, GoalSource,
23    HasChanged, NestedNormalizationGoals, NoSolution, PredefinedOpaquesData, QueryResult,
24};
25
26pub(super) mod canonical;
27mod probe;
28
29pub struct EvalCtxt<'a, D, I = <D as SolverDelegate>::Interner>
30where
31    D: SolverDelegate<Interner = I>,
32    I: Interner,
33{
34    /// The inference context that backs (mostly) inference and placeholder terms
35    /// instantiated while solving goals.
36    ///
37    /// NOTE: The `InferCtxt` that backs the `EvalCtxt` is intentionally private,
38    /// because the `InferCtxt` is much more general than `EvalCtxt`. Methods such
39    /// as  `take_registered_region_obligations` can mess up query responses,
40    /// using `At::normalize` is totally wrong, calling `evaluate_root_goal` can
41    /// cause coinductive unsoundness, etc.
42    ///
43    /// Methods that are generally of use for trait solving are *intentionally*
44    /// re-declared through the `EvalCtxt` below, often with cleaner signatures
45    /// since we don't care about things like `ObligationCause`s and `Span`s here.
46    /// If some `InferCtxt` method is missing, please first think defensively about
47    /// the method's compatibility with this solver, or if an existing one does
48    /// the job already.
49    delegate: &'a D,
50
51    /// The variable info for the `var_values`, only used to make an ambiguous response
52    /// with no constraints.
53    variables: I::CanonicalVars,
54    /// Whether we're currently computing a `NormalizesTo` goal. Unlike other goals,
55    /// `NormalizesTo` goals act like functions with the expected term always being
56    /// fully unconstrained. This would weaken inference however, as the nested goals
57    /// never get the inference constraints from the actual normalized-to type. Because
58    /// of this we return any ambiguous nested goals from `NormalizesTo` to the caller
59    /// when then adds these to its own context. The caller is always an `AliasRelate`
60    /// goal so this never leaks out of the solver.
61    is_normalizes_to_goal: bool,
62    pub(super) var_values: CanonicalVarValues<I>,
63
64    predefined_opaques_in_body: I::PredefinedOpaques,
65
66    /// The highest universe index nameable by the caller.
67    ///
68    /// When we enter a new binder inside of the query we create new universes
69    /// which the caller cannot name. We have to be careful with variables from
70    /// these new universes when creating the query response.
71    ///
72    /// Both because these new universes can prevent us from reaching a fixpoint
73    /// if we have a coinductive cycle and because that's the only way we can return
74    /// new placeholders to the caller.
75    pub(super) max_input_universe: ty::UniverseIndex,
76
77    pub(super) search_graph: &'a mut SearchGraph<D>,
78
79    nested_goals: NestedGoals<I>,
80
81    pub(super) origin_span: I::Span,
82
83    // Has this `EvalCtxt` errored out with `NoSolution` in `try_evaluate_added_goals`?
84    //
85    // If so, then it can no longer be used to make a canonical query response,
86    // since subsequent calls to `try_evaluate_added_goals` have possibly dropped
87    // ambiguous goals. Instead, a probe needs to be introduced somewhere in the
88    // evaluation code.
89    tainted: Result<(), NoSolution>,
90
91    pub(super) inspect: ProofTreeBuilder<D>,
92}
93
94#[derive_where(Clone, Debug, Default; I: Interner)]
95#[derive(TypeVisitable_Generic, TypeFoldable_Generic, Lift_Generic)]
96#[cfg_attr(feature = "nightly", derive(TyDecodable, TyEncodable, HashStable_NoContext))]
97struct NestedGoals<I: Interner> {
98    /// These normalizes-to goals are treated specially during the evaluation
99    /// loop. In each iteration we take the RHS of the projection, replace it with
100    /// a fresh inference variable, and only after evaluating that goal do we
101    /// equate the fresh inference variable with the actual RHS of the predicate.
102    ///
103    /// This is both to improve caching, and to avoid using the RHS of the
104    /// projection predicate to influence the normalizes-to candidate we select.
105    ///
106    /// Forgetting to replace the RHS with a fresh inference variable when we evaluate
107    /// this goal results in an ICE..
108    pub normalizes_to_goals: Vec<Goal<I, ty::NormalizesTo<I>>>,
109    /// The rest of the goals which have not yet processed or remain ambiguous.
110    pub goals: Vec<(GoalSource, Goal<I, I::Predicate>)>,
111}
112
113impl<I: Interner> NestedGoals<I> {
114    fn new() -> Self {
115        Self { normalizes_to_goals: Vec::new(), goals: Vec::new() }
116    }
117
118    fn is_empty(&self) -> bool {
119        self.normalizes_to_goals.is_empty() && self.goals.is_empty()
120    }
121}
122
123#[derive(PartialEq, Eq, Debug, Hash, Clone, Copy)]
124#[cfg_attr(feature = "nightly", derive(HashStable_NoContext))]
125pub enum GenerateProofTree {
126    Yes,
127    No,
128}
129
130pub trait SolverDelegateEvalExt: SolverDelegate {
131    /// Evaluates a goal from **outside** of the trait solver.
132    ///
133    /// Using this while inside of the solver is wrong as it uses a new
134    /// search graph which would break cycle detection.
135    fn evaluate_root_goal(
136        &self,
137        goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
138        generate_proof_tree: GenerateProofTree,
139        span: <Self::Interner as Interner>::Span,
140    ) -> (
141        Result<(HasChanged, Certainty), NoSolution>,
142        Option<inspect::GoalEvaluation<Self::Interner>>,
143    );
144
145    /// Check whether evaluating `goal` with a depth of `root_depth` may
146    /// succeed. This only returns `false` if the goal is guaranteed to
147    /// not hold. In case evaluation overflows and fails with ambiguity this
148    /// returns `true`.
149    ///
150    /// This is only intended to be used as a performance optimization
151    /// in coherence checking.
152    fn root_goal_may_hold_with_depth(
153        &self,
154        root_depth: usize,
155        goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
156    ) -> bool;
157
158    // FIXME: This is only exposed because we need to use it in `analyse.rs`
159    // which is not yet uplifted. Once that's done, we should remove this.
160    fn evaluate_root_goal_raw(
161        &self,
162        goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
163        generate_proof_tree: GenerateProofTree,
164    ) -> (
165        Result<(NestedNormalizationGoals<Self::Interner>, HasChanged, Certainty), NoSolution>,
166        Option<inspect::GoalEvaluation<Self::Interner>>,
167    );
168}
169
170impl<D, I> SolverDelegateEvalExt for D
171where
172    D: SolverDelegate<Interner = I>,
173    I: Interner,
174{
175    #[instrument(level = "debug", skip(self))]
176    fn evaluate_root_goal(
177        &self,
178        goal: Goal<I, I::Predicate>,
179        generate_proof_tree: GenerateProofTree,
180        span: I::Span,
181    ) -> (Result<(HasChanged, Certainty), NoSolution>, Option<inspect::GoalEvaluation<I>>) {
182        EvalCtxt::enter_root(self, self.cx().recursion_limit(), generate_proof_tree, span, |ecx| {
183            ecx.evaluate_goal(GoalEvaluationKind::Root, GoalSource::Misc, goal)
184        })
185    }
186
187    fn root_goal_may_hold_with_depth(
188        &self,
189        root_depth: usize,
190        goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
191    ) -> bool {
192        self.probe(|| {
193            EvalCtxt::enter_root(self, root_depth, GenerateProofTree::No, I::Span::dummy(), |ecx| {
194                ecx.evaluate_goal(GoalEvaluationKind::Root, GoalSource::Misc, goal)
195            })
196            .0
197        })
198        .is_ok()
199    }
200
201    #[instrument(level = "debug", skip(self))]
202    fn evaluate_root_goal_raw(
203        &self,
204        goal: Goal<I, I::Predicate>,
205        generate_proof_tree: GenerateProofTree,
206    ) -> (
207        Result<(NestedNormalizationGoals<I>, HasChanged, Certainty), NoSolution>,
208        Option<inspect::GoalEvaluation<I>>,
209    ) {
210        EvalCtxt::enter_root(
211            self,
212            self.cx().recursion_limit(),
213            generate_proof_tree,
214            I::Span::dummy(),
215            |ecx| ecx.evaluate_goal_raw(GoalEvaluationKind::Root, GoalSource::Misc, goal),
216        )
217    }
218}
219
220impl<'a, D, I> EvalCtxt<'a, D>
221where
222    D: SolverDelegate<Interner = I>,
223    I: Interner,
224{
225    pub(super) fn typing_mode(&self) -> TypingMode<I> {
226        self.delegate.typing_mode()
227    }
228
229    pub(super) fn set_is_normalizes_to_goal(&mut self) {
230        self.is_normalizes_to_goal = true;
231    }
232
233    /// Creates a root evaluation context and search graph. This should only be
234    /// used from outside of any evaluation, and other methods should be preferred
235    /// over using this manually (such as [`SolverDelegateEvalExt::evaluate_root_goal`]).
236    pub(super) fn enter_root<R>(
237        delegate: &D,
238        root_depth: usize,
239        generate_proof_tree: GenerateProofTree,
240        origin_span: I::Span,
241        f: impl FnOnce(&mut EvalCtxt<'_, D>) -> R,
242    ) -> (R, Option<inspect::GoalEvaluation<I>>) {
243        let mut search_graph = SearchGraph::new(root_depth);
244
245        let mut ecx = EvalCtxt {
246            delegate,
247            search_graph: &mut search_graph,
248            nested_goals: NestedGoals::new(),
249            inspect: ProofTreeBuilder::new_maybe_root(generate_proof_tree),
250
251            // Only relevant when canonicalizing the response,
252            // which we don't do within this evaluation context.
253            predefined_opaques_in_body: delegate
254                .cx()
255                .mk_predefined_opaques_in_body(PredefinedOpaquesData::default()),
256            max_input_universe: ty::UniverseIndex::ROOT,
257            variables: Default::default(),
258            var_values: CanonicalVarValues::dummy(),
259            is_normalizes_to_goal: false,
260            origin_span,
261            tainted: Ok(()),
262        };
263        let result = f(&mut ecx);
264
265        let proof_tree = ecx.inspect.finalize();
266        assert!(
267            ecx.nested_goals.is_empty(),
268            "root `EvalCtxt` should not have any goals added to it"
269        );
270
271        assert!(search_graph.is_empty());
272        (result, proof_tree)
273    }
274
275    /// Creates a nested evaluation context that shares the same search graph as the
276    /// one passed in. This is suitable for evaluation, granted that the search graph
277    /// has had the nested goal recorded on its stack ([`SearchGraph::with_new_goal`]),
278    /// but it's preferable to use other methods that call this one rather than this
279    /// method directly.
280    ///
281    /// This function takes care of setting up the inference context, setting the anchor,
282    /// and registering opaques from the canonicalized input.
283    fn enter_canonical<R>(
284        cx: I,
285        search_graph: &'a mut SearchGraph<D>,
286        canonical_input: CanonicalInput<I>,
287        canonical_goal_evaluation: &mut ProofTreeBuilder<D>,
288        f: impl FnOnce(&mut EvalCtxt<'_, D>, Goal<I, I::Predicate>) -> R,
289    ) -> R {
290        let (ref delegate, input, var_values) =
291            SolverDelegate::build_with_canonical(cx, &canonical_input);
292
293        let mut ecx = EvalCtxt {
294            delegate,
295            variables: canonical_input.canonical.variables,
296            var_values,
297            is_normalizes_to_goal: false,
298            predefined_opaques_in_body: input.predefined_opaques_in_body,
299            max_input_universe: canonical_input.canonical.max_universe,
300            search_graph,
301            nested_goals: NestedGoals::new(),
302            origin_span: I::Span::dummy(),
303            tainted: Ok(()),
304            inspect: canonical_goal_evaluation.new_goal_evaluation_step(var_values),
305        };
306
307        for &(key, ty) in &input.predefined_opaques_in_body.opaque_types {
308            ecx.delegate.inject_new_hidden_type_unchecked(key, ty, ecx.origin_span);
309        }
310
311        if !ecx.nested_goals.is_empty() {
312            panic!("prepopulating opaque types shouldn't add goals: {:?}", ecx.nested_goals);
313        }
314
315        let result = f(&mut ecx, input.goal);
316        ecx.inspect.probe_final_state(ecx.delegate, ecx.max_input_universe);
317        canonical_goal_evaluation.goal_evaluation_step(ecx.inspect);
318
319        // When creating a query response we clone the opaque type constraints
320        // instead of taking them. This would cause an ICE here, since we have
321        // assertions against dropping an `InferCtxt` without taking opaques.
322        // FIXME: Once we remove support for the old impl we can remove this.
323        // FIXME: Could we make `build_with_canonical` into `enter_with_canonical` and call this at the end?
324        delegate.reset_opaque_types();
325
326        result
327    }
328
329    /// The entry point of the solver.
330    ///
331    /// This function deals with (coinductive) cycles, overflow, and caching
332    /// and then calls [`EvalCtxt::compute_goal`] which contains the actual
333    /// logic of the solver.
334    ///
335    /// Instead of calling this function directly, use either [EvalCtxt::evaluate_goal]
336    /// if you're inside of the solver or [SolverDelegateEvalExt::evaluate_root_goal] if you're
337    /// outside of it.
338    #[instrument(level = "debug", skip(cx, search_graph, goal_evaluation), ret)]
339    fn evaluate_canonical_goal(
340        cx: I,
341        search_graph: &'a mut SearchGraph<D>,
342        canonical_input: CanonicalInput<I>,
343        goal_evaluation: &mut ProofTreeBuilder<D>,
344    ) -> QueryResult<I> {
345        let mut canonical_goal_evaluation =
346            goal_evaluation.new_canonical_goal_evaluation(canonical_input);
347
348        // Deal with overflow, caching, and coinduction.
349        //
350        // The actual solver logic happens in `ecx.compute_goal`.
351        let result = ensure_sufficient_stack(|| {
352            search_graph.with_new_goal(
353                cx,
354                canonical_input,
355                &mut canonical_goal_evaluation,
356                |search_graph, canonical_goal_evaluation| {
357                    EvalCtxt::enter_canonical(
358                        cx,
359                        search_graph,
360                        canonical_input,
361                        canonical_goal_evaluation,
362                        |ecx, goal| {
363                            let result = ecx.compute_goal(goal);
364                            ecx.inspect.query_result(result);
365                            result
366                        },
367                    )
368                },
369            )
370        });
371
372        canonical_goal_evaluation.query_result(result);
373        goal_evaluation.canonical_goal_evaluation(canonical_goal_evaluation);
374        result
375    }
376
377    /// Recursively evaluates `goal`, returning whether any inference vars have
378    /// been constrained and the certainty of the result.
379    fn evaluate_goal(
380        &mut self,
381        goal_evaluation_kind: GoalEvaluationKind,
382        source: GoalSource,
383        goal: Goal<I, I::Predicate>,
384    ) -> Result<(HasChanged, Certainty), NoSolution> {
385        let (normalization_nested_goals, has_changed, certainty) =
386            self.evaluate_goal_raw(goal_evaluation_kind, source, goal)?;
387        assert!(normalization_nested_goals.is_empty());
388        Ok((has_changed, certainty))
389    }
390
391    /// Recursively evaluates `goal`, returning the nested goals in case
392    /// the nested goal is a `NormalizesTo` goal.
393    ///
394    /// As all other goal kinds do not return any nested goals and
395    /// `NormalizesTo` is only used by `AliasRelate`, all other callsites
396    /// should use [`EvalCtxt::evaluate_goal`] which discards that empty
397    /// storage.
398    // FIXME(-Znext-solver=coinduction): `_source` is currently unused but will
399    // be necessary once we implement the new coinduction approach.
400    pub(super) fn evaluate_goal_raw(
401        &mut self,
402        goal_evaluation_kind: GoalEvaluationKind,
403        _source: GoalSource,
404        goal: Goal<I, I::Predicate>,
405    ) -> Result<(NestedNormalizationGoals<I>, HasChanged, Certainty), NoSolution> {
406        let (orig_values, canonical_goal) = self.canonicalize_goal(goal);
407        let mut goal_evaluation =
408            self.inspect.new_goal_evaluation(goal, &orig_values, goal_evaluation_kind);
409        let canonical_response = EvalCtxt::evaluate_canonical_goal(
410            self.cx(),
411            self.search_graph,
412            canonical_goal,
413            &mut goal_evaluation,
414        );
415        let response = match canonical_response {
416            Err(e) => {
417                self.inspect.goal_evaluation(goal_evaluation);
418                return Err(e);
419            }
420            Ok(response) => response,
421        };
422
423        let has_changed = if !response.value.var_values.is_identity_modulo_regions()
424            || !response.value.external_constraints.opaque_types.is_empty()
425        {
426            HasChanged::Yes
427        } else {
428            HasChanged::No
429        };
430
431        let (normalization_nested_goals, certainty) =
432            self.instantiate_and_apply_query_response(goal.param_env, orig_values, response);
433        self.inspect.goal_evaluation(goal_evaluation);
434
435        // FIXME: We previously had an assert here that checked that recomputing
436        // a goal after applying its constraints did not change its response.
437        //
438        // This assert was removed as it did not hold for goals constraining
439        // an inference variable to a recursive alias, e.g. in
440        // tests/ui/traits/next-solver/overflow/recursive-self-normalization.rs.
441        //
442        // Once we have decided on how to handle trait-system-refactor-initiative#75,
443        // we should re-add an assert here.
444
445        Ok((normalization_nested_goals, has_changed, certainty))
446    }
447
448    fn compute_goal(&mut self, goal: Goal<I, I::Predicate>) -> QueryResult<I> {
449        let Goal { param_env, predicate } = goal;
450        let kind = predicate.kind();
451        if let Some(kind) = kind.no_bound_vars() {
452            match kind {
453                ty::PredicateKind::Clause(ty::ClauseKind::Trait(predicate)) => {
454                    self.compute_trait_goal(Goal { param_env, predicate }).map(|(r, _via)| r)
455                }
456                ty::PredicateKind::Clause(ty::ClauseKind::HostEffect(predicate)) => {
457                    self.compute_host_effect_goal(Goal { param_env, predicate })
458                }
459                ty::PredicateKind::Clause(ty::ClauseKind::Projection(predicate)) => {
460                    self.compute_projection_goal(Goal { param_env, predicate })
461                }
462                ty::PredicateKind::Clause(ty::ClauseKind::TypeOutlives(predicate)) => {
463                    self.compute_type_outlives_goal(Goal { param_env, predicate })
464                }
465                ty::PredicateKind::Clause(ty::ClauseKind::RegionOutlives(predicate)) => {
466                    self.compute_region_outlives_goal(Goal { param_env, predicate })
467                }
468                ty::PredicateKind::Clause(ty::ClauseKind::ConstArgHasType(ct, ty)) => {
469                    self.compute_const_arg_has_type_goal(Goal { param_env, predicate: (ct, ty) })
470                }
471                ty::PredicateKind::Subtype(predicate) => {
472                    self.compute_subtype_goal(Goal { param_env, predicate })
473                }
474                ty::PredicateKind::Coerce(predicate) => {
475                    self.compute_coerce_goal(Goal { param_env, predicate })
476                }
477                ty::PredicateKind::DynCompatible(trait_def_id) => {
478                    self.compute_dyn_compatible_goal(trait_def_id)
479                }
480                ty::PredicateKind::Clause(ty::ClauseKind::WellFormed(arg)) => {
481                    self.compute_well_formed_goal(Goal { param_env, predicate: arg })
482                }
483                ty::PredicateKind::Clause(ty::ClauseKind::ConstEvaluatable(ct)) => {
484                    self.compute_const_evaluatable_goal(Goal { param_env, predicate: ct })
485                }
486                ty::PredicateKind::ConstEquate(_, _) => {
487                    panic!("ConstEquate should not be emitted when `-Znext-solver` is active")
488                }
489                ty::PredicateKind::NormalizesTo(predicate) => {
490                    self.compute_normalizes_to_goal(Goal { param_env, predicate })
491                }
492                ty::PredicateKind::AliasRelate(lhs, rhs, direction) => self
493                    .compute_alias_relate_goal(Goal {
494                        param_env,
495                        predicate: (lhs, rhs, direction),
496                    }),
497                ty::PredicateKind::Ambiguous => {
498                    self.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS)
499                }
500            }
501        } else {
502            self.enter_forall(kind, |ecx, kind| {
503                let goal = goal.with(ecx.cx(), ty::Binder::dummy(kind));
504                ecx.add_goal(GoalSource::InstantiateHigherRanked, goal);
505                ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
506            })
507        }
508    }
509
510    // Recursively evaluates all the goals added to this `EvalCtxt` to completion, returning
511    // the certainty of all the goals.
512    #[instrument(level = "trace", skip(self))]
513    pub(super) fn try_evaluate_added_goals(&mut self) -> Result<Certainty, NoSolution> {
514        let mut response = Ok(Certainty::overflow(false));
515        for _ in 0..FIXPOINT_STEP_LIMIT {
516            // FIXME: This match is a bit ugly, it might be nice to change the inspect
517            // stuff to use a closure instead. which should hopefully simplify this a bit.
518            match self.evaluate_added_goals_step() {
519                Ok(Some(cert)) => {
520                    response = Ok(cert);
521                    break;
522                }
523                Ok(None) => {}
524                Err(NoSolution) => {
525                    response = Err(NoSolution);
526                    break;
527                }
528            }
529        }
530
531        if response.is_err() {
532            self.tainted = Err(NoSolution);
533        }
534
535        response
536    }
537
538    /// Iterate over all added goals: returning `Ok(Some(_))` in case we can stop rerunning.
539    ///
540    /// Goals for the next step get directly added to the nested goals of the `EvalCtxt`.
541    fn evaluate_added_goals_step(&mut self) -> Result<Option<Certainty>, NoSolution> {
542        let cx = self.cx();
543        let mut goals = core::mem::take(&mut self.nested_goals);
544
545        // If this loop did not result in any progress, what's our final certainty.
546        let mut unchanged_certainty = Some(Certainty::Yes);
547        for goal in goals.normalizes_to_goals {
548            // Replace the goal with an unconstrained infer var, so the
549            // RHS does not affect projection candidate assembly.
550            let unconstrained_rhs = self.next_term_infer_of_kind(goal.predicate.term);
551            let unconstrained_goal = goal.with(
552                cx,
553                ty::NormalizesTo { alias: goal.predicate.alias, term: unconstrained_rhs },
554            );
555
556            let (NestedNormalizationGoals(nested_goals), _, certainty) = self.evaluate_goal_raw(
557                GoalEvaluationKind::Nested,
558                GoalSource::Misc,
559                unconstrained_goal,
560            )?;
561            // Add the nested goals from normalization to our own nested goals.
562            trace!(?nested_goals);
563            goals.goals.extend(nested_goals);
564
565            // Finally, equate the goal's RHS with the unconstrained var.
566            //
567            // SUBTLE:
568            // We structurally relate aliases here. This is necessary
569            // as we otherwise emit a nested `AliasRelate` goal in case the
570            // returned term is a rigid alias, resulting in overflow.
571            //
572            // It is correct as both `goal.predicate.term` and `unconstrained_rhs`
573            // start out as an unconstrained inference variable so any aliases get
574            // fully normalized when instantiating it.
575            //
576            // FIXME: Strictly speaking this may be incomplete if the normalized-to
577            // type contains an ambiguous alias referencing bound regions. We should
578            // consider changing this to only use "shallow structural equality".
579            self.eq_structurally_relating_aliases(
580                goal.param_env,
581                goal.predicate.term,
582                unconstrained_rhs,
583            )?;
584
585            // We only look at the `projection_ty` part here rather than
586            // looking at the "has changed" return from evaluate_goal,
587            // because we expect the `unconstrained_rhs` part of the predicate
588            // to have changed -- that means we actually normalized successfully!
589            let with_resolved_vars = self.resolve_vars_if_possible(goal);
590            if goal.predicate.alias != with_resolved_vars.predicate.alias {
591                unchanged_certainty = None;
592            }
593
594            match certainty {
595                Certainty::Yes => {}
596                Certainty::Maybe(_) => {
597                    self.nested_goals.normalizes_to_goals.push(with_resolved_vars);
598                    unchanged_certainty = unchanged_certainty.map(|c| c.unify_with(certainty));
599                }
600            }
601        }
602
603        for (source, goal) in goals.goals {
604            let (has_changed, certainty) =
605                self.evaluate_goal(GoalEvaluationKind::Nested, source, goal)?;
606            if has_changed == HasChanged::Yes {
607                unchanged_certainty = None;
608            }
609
610            match certainty {
611                Certainty::Yes => {}
612                Certainty::Maybe(_) => {
613                    self.nested_goals.goals.push((source, goal));
614                    unchanged_certainty = unchanged_certainty.map(|c| c.unify_with(certainty));
615                }
616            }
617        }
618
619        Ok(unchanged_certainty)
620    }
621
622    /// Record impl args in the proof tree for later access by `InspectCandidate`.
623    pub(crate) fn record_impl_args(&mut self, impl_args: I::GenericArgs) {
624        self.inspect.record_impl_args(self.delegate, self.max_input_universe, impl_args)
625    }
626
627    pub(super) fn cx(&self) -> I {
628        self.delegate.cx()
629    }
630
631    #[instrument(level = "trace", skip(self))]
632    pub(super) fn add_normalizes_to_goal(&mut self, mut goal: Goal<I, ty::NormalizesTo<I>>) {
633        goal.predicate =
634            goal.predicate.fold_with(&mut ReplaceAliasWithInfer::new(self, goal.param_env));
635        self.inspect.add_normalizes_to_goal(self.delegate, self.max_input_universe, goal);
636        self.nested_goals.normalizes_to_goals.push(goal);
637    }
638
639    #[instrument(level = "debug", skip(self))]
640    pub(super) fn add_goal(&mut self, source: GoalSource, mut goal: Goal<I, I::Predicate>) {
641        goal.predicate =
642            goal.predicate.fold_with(&mut ReplaceAliasWithInfer::new(self, goal.param_env));
643        self.inspect.add_goal(self.delegate, self.max_input_universe, source, goal);
644        self.nested_goals.goals.push((source, goal));
645    }
646
647    #[instrument(level = "trace", skip(self, goals))]
648    pub(super) fn add_goals(
649        &mut self,
650        source: GoalSource,
651        goals: impl IntoIterator<Item = Goal<I, I::Predicate>>,
652    ) {
653        for goal in goals {
654            self.add_goal(source, goal);
655        }
656    }
657
658    pub(super) fn next_region_var(&mut self) -> I::Region {
659        let region = self.delegate.next_region_infer();
660        self.inspect.add_var_value(region);
661        region
662    }
663
664    pub(super) fn next_ty_infer(&mut self) -> I::Ty {
665        let ty = self.delegate.next_ty_infer();
666        self.inspect.add_var_value(ty);
667        ty
668    }
669
670    pub(super) fn next_const_infer(&mut self) -> I::Const {
671        let ct = self.delegate.next_const_infer();
672        self.inspect.add_var_value(ct);
673        ct
674    }
675
676    /// Returns a ty infer or a const infer depending on whether `kind` is a `Ty` or `Const`.
677    /// If `kind` is an integer inference variable this will still return a ty infer var.
678    pub(super) fn next_term_infer_of_kind(&mut self, kind: I::Term) -> I::Term {
679        match kind.kind() {
680            ty::TermKind::Ty(_) => self.next_ty_infer().into(),
681            ty::TermKind::Const(_) => self.next_const_infer().into(),
682        }
683    }
684
685    /// Is the projection predicate is of the form `exists<T> <Ty as Trait>::Assoc = T`.
686    ///
687    /// This is the case if the `term` does not occur in any other part of the predicate
688    /// and is able to name all other placeholder and inference variables.
689    #[instrument(level = "trace", skip(self), ret)]
690    pub(super) fn term_is_fully_unconstrained(&self, goal: Goal<I, ty::NormalizesTo<I>>) -> bool {
691        let universe_of_term = match goal.predicate.term.kind() {
692            ty::TermKind::Ty(ty) => {
693                if let ty::Infer(ty::TyVar(vid)) = ty.kind() {
694                    self.delegate.universe_of_ty(vid).unwrap()
695                } else {
696                    return false;
697                }
698            }
699            ty::TermKind::Const(ct) => {
700                if let ty::ConstKind::Infer(ty::InferConst::Var(vid)) = ct.kind() {
701                    self.delegate.universe_of_ct(vid).unwrap()
702                } else {
703                    return false;
704                }
705            }
706        };
707
708        struct ContainsTermOrNotNameable<'a, D: SolverDelegate<Interner = I>, I: Interner> {
709            term: I::Term,
710            universe_of_term: ty::UniverseIndex,
711            delegate: &'a D,
712            cache: HashSet<I::Ty>,
713        }
714
715        impl<D: SolverDelegate<Interner = I>, I: Interner> ContainsTermOrNotNameable<'_, D, I> {
716            fn check_nameable(&self, universe: ty::UniverseIndex) -> ControlFlow<()> {
717                if self.universe_of_term.can_name(universe) {
718                    ControlFlow::Continue(())
719                } else {
720                    ControlFlow::Break(())
721                }
722            }
723        }
724
725        impl<D: SolverDelegate<Interner = I>, I: Interner> TypeVisitor<I>
726            for ContainsTermOrNotNameable<'_, D, I>
727        {
728            type Result = ControlFlow<()>;
729            fn visit_ty(&mut self, t: I::Ty) -> Self::Result {
730                if self.cache.contains(&t) {
731                    return ControlFlow::Continue(());
732                }
733
734                match t.kind() {
735                    ty::Infer(ty::TyVar(vid)) => {
736                        if let ty::TermKind::Ty(term) = self.term.kind() {
737                            if let ty::Infer(ty::TyVar(term_vid)) = term.kind() {
738                                if self.delegate.root_ty_var(vid)
739                                    == self.delegate.root_ty_var(term_vid)
740                                {
741                                    return ControlFlow::Break(());
742                                }
743                            }
744                        }
745
746                        self.check_nameable(self.delegate.universe_of_ty(vid).unwrap())?;
747                    }
748                    ty::Placeholder(p) => self.check_nameable(p.universe())?,
749                    _ => {
750                        if t.has_non_region_infer() || t.has_placeholders() {
751                            t.super_visit_with(self)?
752                        }
753                    }
754                }
755
756                assert!(self.cache.insert(t));
757                ControlFlow::Continue(())
758            }
759
760            fn visit_const(&mut self, c: I::Const) -> Self::Result {
761                match c.kind() {
762                    ty::ConstKind::Infer(ty::InferConst::Var(vid)) => {
763                        if let ty::TermKind::Const(term) = self.term.kind() {
764                            if let ty::ConstKind::Infer(ty::InferConst::Var(term_vid)) = term.kind()
765                            {
766                                if self.delegate.root_const_var(vid)
767                                    == self.delegate.root_const_var(term_vid)
768                                {
769                                    return ControlFlow::Break(());
770                                }
771                            }
772                        }
773
774                        self.check_nameable(self.delegate.universe_of_ct(vid).unwrap())
775                    }
776                    ty::ConstKind::Placeholder(p) => self.check_nameable(p.universe()),
777                    _ => {
778                        if c.has_non_region_infer() || c.has_placeholders() {
779                            c.super_visit_with(self)
780                        } else {
781                            ControlFlow::Continue(())
782                        }
783                    }
784                }
785            }
786        }
787
788        let mut visitor = ContainsTermOrNotNameable {
789            delegate: self.delegate,
790            universe_of_term,
791            term: goal.predicate.term,
792            cache: Default::default(),
793        };
794        goal.predicate.alias.visit_with(&mut visitor).is_continue()
795            && goal.param_env.visit_with(&mut visitor).is_continue()
796    }
797
798    #[instrument(level = "trace", skip(self, param_env), ret)]
799    pub(super) fn eq<T: Relate<I>>(
800        &mut self,
801        param_env: I::ParamEnv,
802        lhs: T,
803        rhs: T,
804    ) -> Result<(), NoSolution> {
805        self.relate(param_env, lhs, ty::Variance::Invariant, rhs)
806    }
807
808    /// This should be used when relating a rigid alias with another type.
809    ///
810    /// Normally we emit a nested `AliasRelate` when equating an inference
811    /// variable and an alias. This causes us to instead constrain the inference
812    /// variable to the alias without emitting a nested alias relate goals.
813    #[instrument(level = "trace", skip(self, param_env), ret)]
814    pub(super) fn relate_rigid_alias_non_alias(
815        &mut self,
816        param_env: I::ParamEnv,
817        alias: ty::AliasTerm<I>,
818        variance: ty::Variance,
819        term: I::Term,
820    ) -> Result<(), NoSolution> {
821        // NOTE: this check is purely an optimization, the structural eq would
822        // always fail if the term is not an inference variable.
823        if term.is_infer() {
824            let cx = self.cx();
825            // We need to relate `alias` to `term` treating only the outermost
826            // constructor as rigid, relating any contained generic arguments as
827            // normal. We do this by first structurally equating the `term`
828            // with the alias constructor instantiated with unconstrained infer vars,
829            // and then relate this with the whole `alias`.
830            //
831            // Alternatively we could modify `Equate` for this case by adding another
832            // variant to `StructurallyRelateAliases`.
833            let identity_args = self.fresh_args_for_item(alias.def_id);
834            let rigid_ctor = ty::AliasTerm::new_from_args(cx, alias.def_id, identity_args);
835            let ctor_term = rigid_ctor.to_term(cx);
836            let obligations = self.delegate.eq_structurally_relating_aliases(
837                param_env,
838                term,
839                ctor_term,
840                self.origin_span,
841            )?;
842            debug_assert!(obligations.is_empty());
843            self.relate(param_env, alias, variance, rigid_ctor)
844        } else {
845            Err(NoSolution)
846        }
847    }
848
849    /// This sohuld only be used when we're either instantiating a previously
850    /// unconstrained "return value" or when we're sure that all aliases in
851    /// the types are rigid.
852    #[instrument(level = "trace", skip(self, param_env), ret)]
853    pub(super) fn eq_structurally_relating_aliases<T: Relate<I>>(
854        &mut self,
855        param_env: I::ParamEnv,
856        lhs: T,
857        rhs: T,
858    ) -> Result<(), NoSolution> {
859        let result = self.delegate.eq_structurally_relating_aliases(
860            param_env,
861            lhs,
862            rhs,
863            self.origin_span,
864        )?;
865        assert_eq!(result, vec![]);
866        Ok(())
867    }
868
869    #[instrument(level = "trace", skip(self, param_env), ret)]
870    pub(super) fn sub<T: Relate<I>>(
871        &mut self,
872        param_env: I::ParamEnv,
873        sub: T,
874        sup: T,
875    ) -> Result<(), NoSolution> {
876        self.relate(param_env, sub, ty::Variance::Covariant, sup)
877    }
878
879    #[instrument(level = "trace", skip(self, param_env), ret)]
880    pub(super) fn relate<T: Relate<I>>(
881        &mut self,
882        param_env: I::ParamEnv,
883        lhs: T,
884        variance: ty::Variance,
885        rhs: T,
886    ) -> Result<(), NoSolution> {
887        let goals = self.delegate.relate(param_env, lhs, variance, rhs, self.origin_span)?;
888        self.add_goals(GoalSource::Misc, goals);
889        Ok(())
890    }
891
892    /// Equates two values returning the nested goals without adding them
893    /// to the nested goals of the `EvalCtxt`.
894    ///
895    /// If possible, try using `eq` instead which automatically handles nested
896    /// goals correctly.
897    #[instrument(level = "trace", skip(self, param_env), ret)]
898    pub(super) fn eq_and_get_goals<T: Relate<I>>(
899        &self,
900        param_env: I::ParamEnv,
901        lhs: T,
902        rhs: T,
903    ) -> Result<Vec<Goal<I, I::Predicate>>, NoSolution> {
904        Ok(self.delegate.relate(param_env, lhs, ty::Variance::Invariant, rhs, self.origin_span)?)
905    }
906
907    pub(super) fn instantiate_binder_with_infer<T: TypeFoldable<I> + Copy>(
908        &self,
909        value: ty::Binder<I, T>,
910    ) -> T {
911        self.delegate.instantiate_binder_with_infer(value)
912    }
913
914    /// `enter_forall`, but takes `&mut self` and passes it back through the
915    /// callback since it can't be aliased during the call.
916    pub(super) fn enter_forall<T: TypeFoldable<I> + Copy, U>(
917        &mut self,
918        value: ty::Binder<I, T>,
919        f: impl FnOnce(&mut Self, T) -> U,
920    ) -> U {
921        self.delegate.enter_forall(value, |value| f(self, value))
922    }
923
924    pub(super) fn resolve_vars_if_possible<T>(&self, value: T) -> T
925    where
926        T: TypeFoldable<I>,
927    {
928        self.delegate.resolve_vars_if_possible(value)
929    }
930
931    pub(super) fn fresh_args_for_item(&mut self, def_id: I::DefId) -> I::GenericArgs {
932        let args = self.delegate.fresh_args_for_item(def_id);
933        for arg in args.iter() {
934            self.inspect.add_var_value(arg);
935        }
936        args
937    }
938
939    pub(super) fn register_ty_outlives(&self, ty: I::Ty, lt: I::Region) {
940        self.delegate.register_ty_outlives(ty, lt, self.origin_span);
941    }
942
943    pub(super) fn register_region_outlives(&self, a: I::Region, b: I::Region) {
944        // `b : a` ==> `a <= b`
945        self.delegate.sub_regions(b, a, self.origin_span);
946    }
947
948    /// Computes the list of goals required for `arg` to be well-formed
949    pub(super) fn well_formed_goals(
950        &self,
951        param_env: I::ParamEnv,
952        arg: I::GenericArg,
953    ) -> Option<Vec<Goal<I, I::Predicate>>> {
954        self.delegate.well_formed_goals(param_env, arg)
955    }
956
957    pub(super) fn trait_ref_is_knowable(
958        &mut self,
959        param_env: I::ParamEnv,
960        trait_ref: ty::TraitRef<I>,
961    ) -> Result<bool, NoSolution> {
962        let delegate = self.delegate;
963        let lazily_normalize_ty = |ty| self.structurally_normalize_ty(param_env, ty);
964        coherence::trait_ref_is_knowable(&**delegate, trait_ref, lazily_normalize_ty)
965            .map(|is_knowable| is_knowable.is_ok())
966    }
967
968    pub(super) fn fetch_eligible_assoc_item(
969        &self,
970        goal_trait_ref: ty::TraitRef<I>,
971        trait_assoc_def_id: I::DefId,
972        impl_def_id: I::DefId,
973    ) -> Result<Option<I::DefId>, I::ErrorGuaranteed> {
974        self.delegate.fetch_eligible_assoc_item(goal_trait_ref, trait_assoc_def_id, impl_def_id)
975    }
976
977    pub(super) fn insert_hidden_type(
978        &mut self,
979        opaque_type_key: ty::OpaqueTypeKey<I>,
980        param_env: I::ParamEnv,
981        hidden_ty: I::Ty,
982    ) -> Result<(), NoSolution> {
983        let mut goals = Vec::new();
984        self.delegate.insert_hidden_type(opaque_type_key, param_env, hidden_ty, &mut goals)?;
985        self.add_goals(GoalSource::Misc, goals);
986        Ok(())
987    }
988
989    pub(super) fn add_item_bounds_for_hidden_type(
990        &mut self,
991        opaque_def_id: I::DefId,
992        opaque_args: I::GenericArgs,
993        param_env: I::ParamEnv,
994        hidden_ty: I::Ty,
995    ) {
996        let mut goals = Vec::new();
997        self.delegate.add_item_bounds_for_hidden_type(
998            opaque_def_id,
999            opaque_args,
1000            param_env,
1001            hidden_ty,
1002            &mut goals,
1003        );
1004        self.add_goals(GoalSource::AliasWellFormed, goals);
1005    }
1006
1007    // Do something for each opaque/hidden pair defined with `def_id` in the
1008    // current inference context.
1009    pub(super) fn probe_existing_opaque_ty(
1010        &mut self,
1011        key: ty::OpaqueTypeKey<I>,
1012    ) -> Option<(ty::OpaqueTypeKey<I>, I::Ty)> {
1013        let mut matching =
1014            self.delegate.clone_opaque_types_for_query_response().into_iter().filter(
1015                |(candidate_key, _)| {
1016                    candidate_key.def_id == key.def_id
1017                        && DeepRejectCtxt::relate_rigid_rigid(self.cx())
1018                            .args_may_unify(candidate_key.args, key.args)
1019                },
1020            );
1021        let first = matching.next();
1022        let second = matching.next();
1023        assert_eq!(second, None);
1024        first
1025    }
1026
1027    // Try to evaluate a const, or return `None` if the const is too generic.
1028    // This doesn't mean the const isn't evaluatable, though, and should be treated
1029    // as an ambiguity rather than no-solution.
1030    pub(super) fn evaluate_const(
1031        &self,
1032        param_env: I::ParamEnv,
1033        uv: ty::UnevaluatedConst<I>,
1034    ) -> Option<I::Const> {
1035        self.delegate.evaluate_const(param_env, uv)
1036    }
1037
1038    pub(super) fn is_transmutable(
1039        &mut self,
1040        param_env: I::ParamEnv,
1041        dst: I::Ty,
1042        src: I::Ty,
1043        assume: I::Const,
1044    ) -> Result<Certainty, NoSolution> {
1045        self.delegate.is_transmutable(param_env, dst, src, assume)
1046    }
1047}
1048
1049/// Eagerly replace aliases with inference variables, emitting `AliasRelate`
1050/// goals, used when adding goals to the `EvalCtxt`. We compute the
1051/// `AliasRelate` goals before evaluating the actual goal to get all the
1052/// constraints we can.
1053///
1054/// This is a performance optimization to more eagerly detect cycles during trait
1055/// solving. See tests/ui/traits/next-solver/cycles/cycle-modulo-ambig-aliases.rs.
1056struct ReplaceAliasWithInfer<'me, 'a, D, I>
1057where
1058    D: SolverDelegate<Interner = I>,
1059    I: Interner,
1060{
1061    ecx: &'me mut EvalCtxt<'a, D>,
1062    param_env: I::ParamEnv,
1063    cache: HashMap<I::Ty, I::Ty>,
1064}
1065
1066impl<'me, 'a, D, I> ReplaceAliasWithInfer<'me, 'a, D, I>
1067where
1068    D: SolverDelegate<Interner = I>,
1069    I: Interner,
1070{
1071    fn new(ecx: &'me mut EvalCtxt<'a, D>, param_env: I::ParamEnv) -> Self {
1072        ReplaceAliasWithInfer { ecx, param_env, cache: Default::default() }
1073    }
1074}
1075
1076impl<D, I> TypeFolder<I> for ReplaceAliasWithInfer<'_, '_, D, I>
1077where
1078    D: SolverDelegate<Interner = I>,
1079    I: Interner,
1080{
1081    fn cx(&self) -> I {
1082        self.ecx.cx()
1083    }
1084
1085    fn fold_ty(&mut self, ty: I::Ty) -> I::Ty {
1086        match ty.kind() {
1087            ty::Alias(..) if !ty.has_escaping_bound_vars() => {
1088                let infer_ty = self.ecx.next_ty_infer();
1089                let normalizes_to = ty::PredicateKind::AliasRelate(
1090                    ty.into(),
1091                    infer_ty.into(),
1092                    ty::AliasRelationDirection::Equate,
1093                );
1094                self.ecx.add_goal(
1095                    GoalSource::Misc,
1096                    Goal::new(self.cx(), self.param_env, normalizes_to),
1097                );
1098                infer_ty
1099            }
1100            _ => {
1101                if !ty.has_aliases() {
1102                    ty
1103                } else if let Some(&entry) = self.cache.get(&ty) {
1104                    return entry;
1105                } else {
1106                    let res = ty.super_fold_with(self);
1107                    assert!(self.cache.insert(ty, res).is_none());
1108                    res
1109                }
1110            }
1111        }
1112    }
1113
1114    fn fold_const(&mut self, ct: I::Const) -> I::Const {
1115        match ct.kind() {
1116            ty::ConstKind::Unevaluated(..) if !ct.has_escaping_bound_vars() => {
1117                let infer_ct = self.ecx.next_const_infer();
1118                let normalizes_to = ty::PredicateKind::AliasRelate(
1119                    ct.into(),
1120                    infer_ct.into(),
1121                    ty::AliasRelationDirection::Equate,
1122                );
1123                self.ecx.add_goal(
1124                    GoalSource::Misc,
1125                    Goal::new(self.cx(), self.param_env, normalizes_to),
1126                );
1127                infer_ct
1128            }
1129            _ => ct.super_fold_with(self),
1130        }
1131    }
1132
1133    fn fold_predicate(&mut self, predicate: I::Predicate) -> I::Predicate {
1134        if predicate.allow_normalization() { predicate.super_fold_with(self) } else { predicate }
1135    }
1136}
rustc_next_trait_solver/solve/eval_ctxt/mod.rs

rustc_next_trait_solver/solve/eval_ctxt/
mod.rs
