1
+ //! Data structure used to inspect trait solver behavior.
2
+ //!
3
+ //! During trait solving we optionally build "proof trees", the root of
4
+ //! which is a [GoalEvaluation] with [GoalEvaluationKind::Root]. These
5
+ //! trees are used to improve the debug experience and are also used by
6
+ //! the compiler itself to provide necessary context for error messages.
7
+ //!
8
+ //! Because each nested goal in the solver gets [canonicalized] separately
9
+ //! and we discard inference progress via "probes", we cannot mechanically
10
+ //! use proof trees without somehow "lifting up" data local to the current
11
+ //! `InferCtxt`. Any data used mechanically is therefore canonicalized and
12
+ //! stored as [CanonicalState]. As printing canonicalized data worsens the
13
+ //! debugging dumps, we do not simply canonicalize everything.
14
+ //!
15
+ //! This means proof trees contain inference variables and placeholders
16
+ //! local to a different `InferCtxt` which must not be used with the
17
+ //! current one.
18
+ //!
19
+ //! [canonicalized]: https://rustc-dev-guide.rust-lang.org/solve/canonicalization.html
20
+
1
21
use super :: {
2
22
CandidateSource , Canonical , CanonicalInput , Certainty , Goal , IsNormalizesToHack , NoSolution ,
3
23
QueryInput , QueryResult ,
@@ -8,6 +28,12 @@ use std::fmt::{Debug, Write};
8
28
9
29
mod format;
10
30
31
+ /// Some `data` together with information about how they relate to the input
32
+ /// of the canonical query.
33
+ ///
34
+ /// This is only ever used as [CanonicalState]. Any type information in proof
35
+ /// trees used mechanically has to be canonicalized as we otherwise leak
36
+ /// inference variables from a nested `InferCtxt`.
11
37
#[ derive( Debug , Clone , Copy , Eq , PartialEq , TypeFoldable , TypeVisitable ) ]
12
38
pub struct State < ' tcx , T > {
13
39
pub var_values : CanonicalVarValues < ' tcx > ,
@@ -22,6 +48,11 @@ pub enum CacheHit {
22
48
Global ,
23
49
}
24
50
51
+ /// When evaluating the root goals we also store the
52
+ /// original values for the `CanonicalVarValues` of the
53
+ /// canonicalized goal to map any [CanonicalState]
54
+ /// from the `InferCtxt` local to the solver query to
55
+ /// the `InferCtxt` of the caller.
25
56
#[ derive( Eq , PartialEq ) ]
26
57
pub enum GoalEvaluationKind < ' tcx > {
27
58
Root { orig_values : Vec < ty:: GenericArg < ' tcx > > } ,
@@ -33,6 +64,7 @@ pub struct GoalEvaluation<'tcx> {
33
64
pub uncanonicalized_goal : Goal < ' tcx , ty:: Predicate < ' tcx > > ,
34
65
pub kind : GoalEvaluationKind < ' tcx > ,
35
66
pub evaluation : CanonicalGoalEvaluation < ' tcx > ,
67
+ /// The nested goals from instantiating the query response.
36
68
pub returned_goals : Vec < Goal < ' tcx , ty:: Predicate < ' tcx > > > ,
37
69
}
38
70
@@ -74,6 +106,7 @@ pub struct GoalEvaluationStep<'tcx> {
74
106
/// of a goal.
75
107
#[ derive( Eq , PartialEq ) ]
76
108
pub struct Probe < ' tcx > {
109
+ /// What happened inside of this probe in chronological order.
77
110
pub steps : Vec < ProbeStep < ' tcx > > ,
78
111
pub kind : ProbeKind < ' tcx > ,
79
112
}
@@ -86,11 +119,20 @@ impl Debug for Probe<'_> {
86
119
87
120
#[ derive( Eq , PartialEq ) ]
88
121
pub enum ProbeStep < ' tcx > {
122
+ /// We added a goal to the `EvalCtxt` which will get proven
123
+ /// the next time `EvalCtxt::try_evaluate_added_goals` is called.
89
124
AddGoal ( CanonicalState < ' tcx , Goal < ' tcx , ty:: Predicate < ' tcx > > > ) ,
125
+ /// The inside of a `EvalCtxt::try_evaluate_added_goals` call.
90
126
EvaluateGoals ( AddedGoalsEvaluation < ' tcx > ) ,
127
+ /// A call to `probe` while proving the current goal. This is
128
+ /// used whenever there are multiple candidates to prove the
129
+ /// current goalby .
91
130
NestedProbe ( Probe < ' tcx > ) ,
92
131
}
93
132
133
+ /// What kind of probe we're in. In case the probe represents a candidate, or
134
+ /// the final result - via [ProbeKind::Root] - we also store the result for
135
+ /// the candidate.
94
136
#[ derive( Debug , PartialEq , Eq , Clone , Copy ) ]
95
137
pub enum ProbeKind < ' tcx > {
96
138
/// The root inference context while proving a goal.
0 commit comments