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

rustc_trait_selection/solve/inspect/
analyse.rs
