rustc_trait_selection/solve/inspect/
analyse.rs

1//! An infrastructure to mechanically analyse proof trees.
2//!
3//! It is unavoidable that this representation is somewhat
4//! lossy as it should hide quite a few semantically relevant things,
5//! e.g. canonicalization and the order of nested goals.
6//!
7//! @lcnr: However, a lot of the weirdness here is not strictly necessary
8//! and could be improved in the future. This is mostly good enough for
9//! coherence right now and was annoying to implement, so I am leaving it
10//! as is until we start using it for something else.
11
12use std::assert_matches::assert_matches;
13
14use rustc_infer::infer::InferCtxt;
15use rustc_infer::traits::Obligation;
16use rustc_macros::extension;
17use rustc_middle::traits::ObligationCause;
18use rustc_middle::traits::solve::{Certainty, Goal, GoalSource, NoSolution, QueryResult};
19use rustc_middle::ty::{TyCtxt, VisitorResult, try_visit};
20use rustc_middle::{bug, ty};
21use rustc_next_trait_solver::resolve::eager_resolve_vars;
22use rustc_next_trait_solver::solve::inspect::{self, instantiate_canonical_state};
23use rustc_next_trait_solver::solve::{MaybeCause, SolverDelegateEvalExt as _};
24use rustc_span::Span;
25use tracing::instrument;
26
27use crate::solve::delegate::SolverDelegate;
28use crate::traits::ObligationCtxt;
29
30pub struct InspectConfig {
31    pub max_depth: usize,
32}
33
34pub struct InspectGoal<'a, 'tcx> {
35    infcx: &'a SolverDelegate<'tcx>,
36    depth: usize,
37    orig_values: Vec<ty::GenericArg<'tcx>>,
38    goal: Goal<'tcx, ty::Predicate<'tcx>>,
39    result: Result<Certainty, NoSolution>,
40    evaluation_kind: inspect::GoalEvaluationKind<TyCtxt<'tcx>>,
41    normalizes_to_term_hack: Option<NormalizesToTermHack<'tcx>>,
42    source: GoalSource,
43}
44
45/// The expected term of a `NormalizesTo` goal gets replaced
46/// with an unconstrained inference variable when computing
47/// `NormalizesTo` goals and we return the nested goals to the
48/// caller, who also equates the actual term with the expected.
49///
50/// This is an implementation detail of the trait solver and
51/// not something we want to leak to users. We therefore
52/// treat `NormalizesTo` goals as if they apply the expected
53/// type at the end of each candidate.
54#[derive(Copy, Clone)]
55struct NormalizesToTermHack<'tcx> {
56    term: ty::Term<'tcx>,
57    unconstrained_term: ty::Term<'tcx>,
58}
59
60impl<'tcx> NormalizesToTermHack<'tcx> {
61    /// Relate the `term` with the new `unconstrained_term` created
62    /// when computing the proof tree for this `NormalizesTo` goals.
63    /// This handles nested obligations.
64    fn constrain_and(
65        &self,
66        infcx: &InferCtxt<'tcx>,
67        span: Span,
68        param_env: ty::ParamEnv<'tcx>,
69        f: impl FnOnce(&ObligationCtxt<'_, 'tcx>),
70    ) -> Result<Certainty, NoSolution> {
71        let ocx = ObligationCtxt::new(infcx);
72        ocx.eq(
73            &ObligationCause::dummy_with_span(span),
74            param_env,
75            self.term,
76            self.unconstrained_term,
77        )?;
78        f(&ocx);
79        let errors = ocx.select_all_or_error();
80        if errors.is_empty() {
81            Ok(Certainty::Yes)
82        } else if errors.iter().all(|e| !e.is_true_error()) {
83            Ok(Certainty::AMBIGUOUS)
84        } else {
85            Err(NoSolution)
86        }
87    }
88}
89
90pub struct InspectCandidate<'a, 'tcx> {
91    goal: &'a InspectGoal<'a, 'tcx>,
92    kind: inspect::ProbeKind<TyCtxt<'tcx>>,
93    steps: Vec<&'a inspect::ProbeStep<TyCtxt<'tcx>>>,
94    final_state: inspect::CanonicalState<TyCtxt<'tcx>, ()>,
95    result: QueryResult<'tcx>,
96    shallow_certainty: Certainty,
97}
98
99impl<'a, 'tcx> InspectCandidate<'a, 'tcx> {
100    pub fn kind(&self) -> inspect::ProbeKind<TyCtxt<'tcx>> {
101        self.kind
102    }
103
104    pub fn result(&self) -> Result<Certainty, NoSolution> {
105        self.result.map(|c| c.value.certainty)
106    }
107
108    pub fn goal(&self) -> &'a InspectGoal<'a, 'tcx> {
109        self.goal
110    }
111
112    /// Certainty passed into `evaluate_added_goals_and_make_canonical_response`.
113    ///
114    /// If this certainty is `Yes`, then we must be confident that the candidate
115    /// must hold iff it's nested goals hold. This is not true if the certainty is
116    /// `Maybe(..)`, which suggests we forced ambiguity instead.
117    ///
118    /// This is *not* the certainty of the candidate's full nested evaluation, which
119    /// can be accessed with [`Self::result`] instead.
120    pub fn shallow_certainty(&self) -> Certainty {
121        self.shallow_certainty
122    }
123
124    /// Visit all nested goals of this candidate without rolling
125    /// back their inference constraints. This function modifies
126    /// the state of the `infcx`.
127    pub fn visit_nested_no_probe<V: ProofTreeVisitor<'tcx>>(&self, visitor: &mut V) -> V::Result {
128        for goal in self.instantiate_nested_goals(visitor.span()) {
129            try_visit!(goal.visit_with(visitor));
130        }
131
132        V::Result::output()
133    }
134
135    /// Instantiate the nested goals for the candidate without rolling back their
136    /// inference constraints. This function modifies the state of the `infcx`.
137    ///
138    /// See [`Self::instantiate_impl_args`] if you need the impl args too.
139    #[instrument(
140        level = "debug",
141        skip_all,
142        fields(goal = ?self.goal.goal, steps = ?self.steps)
143    )]
144    pub fn instantiate_nested_goals(&self, span: Span) -> Vec<InspectGoal<'a, 'tcx>> {
145        let infcx = self.goal.infcx;
146        let param_env = self.goal.goal.param_env;
147        let mut orig_values = self.goal.orig_values.to_vec();
148
149        let mut instantiated_goals = vec![];
150        for step in &self.steps {
151            match **step {
152                inspect::ProbeStep::AddGoal(source, goal) => instantiated_goals.push((
153                    source,
154                    instantiate_canonical_state(infcx, span, param_env, &mut orig_values, goal),
155                )),
156                inspect::ProbeStep::RecordImplArgs { .. } => {}
157                inspect::ProbeStep::MakeCanonicalResponse { .. }
158                | inspect::ProbeStep::NestedProbe(_) => unreachable!(),
159            }
160        }
161
162        let () =
163            instantiate_canonical_state(infcx, span, param_env, &mut orig_values, self.final_state);
164
165        if let Some(term_hack) = &self.goal.normalizes_to_term_hack {
166            // FIXME: We ignore the expected term of `NormalizesTo` goals
167            // when computing the result of its candidates. This is
168            // scuffed.
169            let _ = term_hack.constrain_and(infcx, span, param_env, |_| {});
170        }
171
172        instantiated_goals
173            .into_iter()
174            .map(|(source, goal)| self.instantiate_proof_tree_for_nested_goal(source, goal, span))
175            .collect()
176    }
177
178    /// Instantiate the args of an impl if this candidate came from a
179    /// `CandidateSource::Impl`. This function modifies the state of the
180    /// `infcx`.
181    #[instrument(
182        level = "debug",
183        skip_all,
184        fields(goal = ?self.goal.goal, steps = ?self.steps)
185    )]
186    pub fn instantiate_impl_args(&self, span: Span) -> ty::GenericArgsRef<'tcx> {
187        let infcx = self.goal.infcx;
188        let param_env = self.goal.goal.param_env;
189        let mut orig_values = self.goal.orig_values.to_vec();
190
191        for step in &self.steps {
192            match **step {
193                inspect::ProbeStep::RecordImplArgs { impl_args } => {
194                    let impl_args = instantiate_canonical_state(
195                        infcx,
196                        span,
197                        param_env,
198                        &mut orig_values,
199                        impl_args,
200                    );
201
202                    let () = instantiate_canonical_state(
203                        infcx,
204                        span,
205                        param_env,
206                        &mut orig_values,
207                        self.final_state,
208                    );
209
210                    // No reason we couldn't support this, but we don't need to for select.
211                    assert!(
212                        self.goal.normalizes_to_term_hack.is_none(),
213                        "cannot use `instantiate_impl_args` with a `NormalizesTo` goal"
214                    );
215
216                    return eager_resolve_vars(infcx, impl_args);
217                }
218                inspect::ProbeStep::AddGoal(..) => {}
219                inspect::ProbeStep::MakeCanonicalResponse { .. }
220                | inspect::ProbeStep::NestedProbe(_) => unreachable!(),
221            }
222        }
223
224        bug!("expected impl args probe step for `instantiate_impl_args`");
225    }
226
227    pub fn instantiate_proof_tree_for_nested_goal(
228        &self,
229        source: GoalSource,
230        goal: Goal<'tcx, ty::Predicate<'tcx>>,
231        span: Span,
232    ) -> InspectGoal<'a, 'tcx> {
233        let infcx = self.goal.infcx;
234        match goal.predicate.kind().no_bound_vars() {
235            Some(ty::PredicateKind::NormalizesTo(ty::NormalizesTo { alias, term })) => {
236                let unconstrained_term = infcx.next_term_var_of_kind(term, span);
237                let goal =
238                    goal.with(infcx.tcx, ty::NormalizesTo { alias, term: unconstrained_term });
239                // We have to use a `probe` here as evaluating a `NormalizesTo` can constrain the
240                // expected term. This means that candidates which only fail due to nested goals
241                // and which normalize to a different term then the final result could ICE: when
242                // building their proof tree, the expected term was unconstrained, but when
243                // instantiating the candidate it is already constrained to the result of another
244                // candidate.
245                let normalizes_to_term_hack = NormalizesToTermHack { term, unconstrained_term };
246                let (proof_tree, nested_goals_result) = infcx.probe(|_| {
247                    // Here, if we have any nested goals, then we make sure to apply them
248                    // considering the constrained RHS, and pass the resulting certainty to
249                    // `InspectGoal::new` so that the goal has the right result (and maintains
250                    // the impression that we don't do this normalizes-to infer hack at all).
251                    let (nested, proof_tree) = infcx.evaluate_root_goal_for_proof_tree(goal, span);
252                    let nested_goals_result = nested.and_then(|(nested, _)| {
253                        normalizes_to_term_hack.constrain_and(
254                            infcx,
255                            span,
256                            proof_tree.uncanonicalized_goal.param_env,
257                            |ocx| {
258                                ocx.register_obligations(nested.0.into_iter().map(|(_, goal)| {
259                                    Obligation::new(
260                                        infcx.tcx,
261                                        ObligationCause::dummy_with_span(span),
262                                        goal.param_env,
263                                        goal.predicate,
264                                    )
265                                }));
266                            },
267                        )
268                    });
269                    (proof_tree, nested_goals_result)
270                });
271                InspectGoal::new(
272                    infcx,
273                    self.goal.depth + 1,
274                    proof_tree,
275                    Some((normalizes_to_term_hack, nested_goals_result)),
276                    source,
277                )
278            }
279            _ => {
280                // We're using a probe here as evaluating a goal could constrain
281                // inference variables by choosing one candidate. If we then recurse
282                // into another candidate who ends up with different inference
283                // constraints, we get an ICE if we already applied the constraints
284                // from the chosen candidate.
285                let proof_tree =
286                    infcx.probe(|_| infcx.evaluate_root_goal_for_proof_tree(goal, span).1);
287                InspectGoal::new(infcx, self.goal.depth + 1, proof_tree, None, source)
288            }
289        }
290    }
291
292    /// Visit all nested goals of this candidate, rolling back
293    /// all inference constraints.
294    pub fn visit_nested_in_probe<V: ProofTreeVisitor<'tcx>>(&self, visitor: &mut V) -> V::Result {
295        self.goal.infcx.probe(|_| self.visit_nested_no_probe(visitor))
296    }
297}
298
299impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
300    pub fn infcx(&self) -> &'a InferCtxt<'tcx> {
301        self.infcx
302    }
303
304    pub fn goal(&self) -> Goal<'tcx, ty::Predicate<'tcx>> {
305        self.goal
306    }
307
308    pub fn result(&self) -> Result<Certainty, NoSolution> {
309        self.result
310    }
311
312    pub fn source(&self) -> GoalSource {
313        self.source
314    }
315
316    pub fn depth(&self) -> usize {
317        self.depth
318    }
319
320    fn candidates_recur(
321        &'a self,
322        candidates: &mut Vec<InspectCandidate<'a, 'tcx>>,
323        steps: &mut Vec<&'a inspect::ProbeStep<TyCtxt<'tcx>>>,
324        probe: &'a inspect::Probe<TyCtxt<'tcx>>,
325    ) {
326        let mut shallow_certainty = None;
327        for step in &probe.steps {
328            match *step {
329                inspect::ProbeStep::AddGoal(..) | inspect::ProbeStep::RecordImplArgs { .. } => {
330                    steps.push(step)
331                }
332                inspect::ProbeStep::MakeCanonicalResponse { shallow_certainty: c } => {
333                    assert_matches!(
334                        shallow_certainty.replace(c),
335                        None | Some(Certainty::Maybe(MaybeCause::Ambiguity))
336                    );
337                }
338                inspect::ProbeStep::NestedProbe(ref probe) => {
339                    match probe.kind {
340                        // These never assemble candidates for the goal we're trying to solve.
341                        inspect::ProbeKind::ProjectionCompatibility
342                        | inspect::ProbeKind::ShadowedEnvProbing => continue,
343
344                        inspect::ProbeKind::NormalizedSelfTyAssembly
345                        | inspect::ProbeKind::UnsizeAssembly
346                        | inspect::ProbeKind::Root { .. }
347                        | inspect::ProbeKind::TraitCandidate { .. }
348                        | inspect::ProbeKind::OpaqueTypeStorageLookup { .. }
349                        | inspect::ProbeKind::RigidAlias { .. } => {
350                            // Nested probes have to prove goals added in their parent
351                            // but do not leak them, so we truncate the added goals
352                            // afterwards.
353                            let num_steps = steps.len();
354                            self.candidates_recur(candidates, steps, probe);
355                            steps.truncate(num_steps);
356                        }
357                    }
358                }
359            }
360        }
361
362        match probe.kind {
363            inspect::ProbeKind::ProjectionCompatibility
364            | inspect::ProbeKind::ShadowedEnvProbing => {
365                bug!()
366            }
367
368            inspect::ProbeKind::NormalizedSelfTyAssembly | inspect::ProbeKind::UnsizeAssembly => {}
369
370            // We add a candidate even for the root evaluation if there
371            // is only one way to prove a given goal, e.g. for `WellFormed`.
372            inspect::ProbeKind::Root { result }
373            | inspect::ProbeKind::TraitCandidate { source: _, result }
374            | inspect::ProbeKind::OpaqueTypeStorageLookup { result }
375            | inspect::ProbeKind::RigidAlias { result } => {
376                // We only add a candidate if `shallow_certainty` was set, which means
377                // that we ended up calling `evaluate_added_goals_and_make_canonical_response`.
378                if let Some(shallow_certainty) = shallow_certainty {
379                    candidates.push(InspectCandidate {
380                        goal: self,
381                        kind: probe.kind,
382                        steps: steps.clone(),
383                        final_state: probe.final_state,
384                        shallow_certainty,
385                        result,
386                    });
387                }
388            }
389        }
390    }
391
392    pub fn candidates(&'a self) -> Vec<InspectCandidate<'a, 'tcx>> {
393        let mut candidates = vec![];
394        let last_eval_step = match &self.evaluation_kind {
395            // An annoying edge case in case the recursion limit is 0.
396            inspect::GoalEvaluationKind::Overflow => return vec![],
397            inspect::GoalEvaluationKind::Evaluation { final_revision } => final_revision,
398        };
399
400        let mut nested_goals = vec![];
401        self.candidates_recur(&mut candidates, &mut nested_goals, &last_eval_step);
402
403        candidates
404    }
405
406    /// Returns the single candidate applicable for the current goal, if it exists.
407    ///
408    /// Returns `None` if there are either no or multiple applicable candidates.
409    pub fn unique_applicable_candidate(&'a self) -> Option<InspectCandidate<'a, 'tcx>> {
410        // FIXME(-Znext-solver): This does not handle impl candidates
411        // hidden by env candidates.
412        let mut candidates = self.candidates();
413        candidates.retain(|c| c.result().is_ok());
414        candidates.pop().filter(|_| candidates.is_empty())
415    }
416
417    fn new(
418        infcx: &'a InferCtxt<'tcx>,
419        depth: usize,
420        root: inspect::GoalEvaluation<TyCtxt<'tcx>>,
421        term_hack_and_nested_certainty: Option<(
422            NormalizesToTermHack<'tcx>,
423            Result<Certainty, NoSolution>,
424        )>,
425        source: GoalSource,
426    ) -> Self {
427        let infcx = <&SolverDelegate<'tcx>>::from(infcx);
428
429        let inspect::GoalEvaluation { uncanonicalized_goal, orig_values, kind, result } = root;
430        // If there's a normalizes-to goal, AND the evaluation result with the result of
431        // constraining the normalizes-to RHS and computing the nested goals.
432        let result = result.and_then(|ok| {
433            let nested_goals_certainty =
434                term_hack_and_nested_certainty.map_or(Ok(Certainty::Yes), |(_, c)| c)?;
435            Ok(ok.value.certainty.and(nested_goals_certainty))
436        });
437
438        InspectGoal {
439            infcx,
440            depth,
441            orig_values,
442            goal: eager_resolve_vars(infcx, uncanonicalized_goal),
443            result,
444            evaluation_kind: kind,
445            normalizes_to_term_hack: term_hack_and_nested_certainty.map(|(n, _)| n),
446            source,
447        }
448    }
449
450    pub(crate) fn visit_with<V: ProofTreeVisitor<'tcx>>(&self, visitor: &mut V) -> V::Result {
451        if self.depth < visitor.config().max_depth {
452            try_visit!(visitor.visit_goal(self));
453        }
454
455        V::Result::output()
456    }
457}
458
459/// The public API to interact with proof trees.
460pub trait ProofTreeVisitor<'tcx> {
461    type Result: VisitorResult = ();
462
463    fn span(&self) -> Span;
464
465    fn config(&self) -> InspectConfig {
466        InspectConfig { max_depth: 10 }
467    }
468
469    fn visit_goal(&mut self, goal: &InspectGoal<'_, 'tcx>) -> Self::Result;
470}
471
472#[extension(pub trait ProofTreeInferCtxtExt<'tcx>)]
473impl<'tcx> InferCtxt<'tcx> {
474    fn visit_proof_tree<V: ProofTreeVisitor<'tcx>>(
475        &self,
476        goal: Goal<'tcx, ty::Predicate<'tcx>>,
477        visitor: &mut V,
478    ) -> V::Result {
479        self.visit_proof_tree_at_depth(goal, 0, visitor)
480    }
481
482    fn visit_proof_tree_at_depth<V: ProofTreeVisitor<'tcx>>(
483        &self,
484        goal: Goal<'tcx, ty::Predicate<'tcx>>,
485        depth: usize,
486        visitor: &mut V,
487    ) -> V::Result {
488        let (_, proof_tree) = <&SolverDelegate<'tcx>>::from(self)
489            .evaluate_root_goal_for_proof_tree(goal, visitor.span());
490        visitor.visit_goal(&InspectGoal::new(self, depth, proof_tree, None, GoalSource::Misc))
491    }
492}
rustc_trait_selection/solve/inspect/analyse.rs

rustc_trait_selection/solve/inspect/
analyse.rs
