|
| 1 | +# Canonical queries |
| 2 | + |
| 3 | +The "start" of the trait system is the **canonical query** (these are |
| 4 | +both queries in the more general sense of the word – something you |
| 5 | +would like to know the answer to – and in the |
| 6 | +[rustc-specific sense](../query.html)). The idea is that the type |
| 7 | +checker or other parts of the system, may in the course of doing their |
| 8 | +thing want to know whether some trait is implemented for some type |
| 9 | +(e.g., is `u32: Debug` true?). Or they may want to |
| 10 | +[normalize some associated type](./associated-types.html). |
| 11 | + |
| 12 | +This section covers queries at a fairly high level of abstraction. The |
| 13 | +subsections look a bit more closely at how these ideas are implemented |
| 14 | +in rustc. |
| 15 | + |
| 16 | +## The traditional, interactive Prolog query |
| 17 | + |
| 18 | +In a traditional Prolog system, when you start a query, the solver |
| 19 | +will run off and start supplying you with every possible answer it can |
| 20 | +find. So given something like this: |
| 21 | + |
| 22 | +```text |
| 23 | +?- Vec<i32>: AsRef<?U> |
| 24 | +``` |
| 25 | + |
| 26 | +The solver might answer: |
| 27 | + |
| 28 | +```text |
| 29 | +Vec<i32>: AsRef<[i32]> |
| 30 | + continue? (y/n) |
| 31 | +``` |
| 32 | + |
| 33 | +This `continue` bit is interesting. The idea in Prolog is that the |
| 34 | +solver is finding **all possible** instantiations of your query that |
| 35 | +are true. In this case, if we instantiate `?U = [i32]`, then the query |
| 36 | +is true (note that a traditional Prolog interface does not, directly, |
| 37 | +tell us a value for `?U`, but we can infer one by unifying the |
| 38 | +response with our original query – Rust's solver gives back a |
| 39 | +substitution instead). If we were to hit `y`, the solver might then |
| 40 | +give us another possible answer: |
| 41 | + |
| 42 | +```text |
| 43 | +Vec<i32>: AsRef<Vec<i32>> |
| 44 | + continue? (y/n) |
| 45 | +``` |
| 46 | + |
| 47 | +This answer derives from the fact that there is a reflexive impl |
| 48 | +(`impl<T> AsRef<T> for T`) for `AsRef`. If were to hit `y` again, |
| 49 | +then we might get back a negative response: |
| 50 | + |
| 51 | +```text |
| 52 | +no |
| 53 | +``` |
| 54 | + |
| 55 | +Naturally, in some cases, there may be no possible answers, and hence |
| 56 | +the solver will just give me back `no` right away: |
| 57 | + |
| 58 | +```text |
| 59 | +?- Box<i32>: Copy |
| 60 | + no |
| 61 | +``` |
| 62 | + |
| 63 | +In some cases, there might be an infinite number of responses. So for |
| 64 | +example if I gave this query, and I kept hitting `y`, then the solver |
| 65 | +would never stop giving me back answers: |
| 66 | + |
| 67 | +```text |
| 68 | +?- Vec<?U>: Clone |
| 69 | + Vec<i32>: Clone |
| 70 | + continue? (y/n) |
| 71 | + Vec<Box<i32>>: Clone |
| 72 | + continue? (y/n) |
| 73 | + Vec<Box<Box<i32>>>: Clone |
| 74 | + continue? (y/n) |
| 75 | + Vec<Box<Box<Box<i32>>>>: Clone |
| 76 | + continue? (y/n) |
| 77 | +``` |
| 78 | + |
| 79 | +As you can imagine, the solver will gleefully keep adding another |
| 80 | +layer of `Box` until we ask it to stop, or it runs out of memory. |
| 81 | + |
| 82 | +Another interesting thing is that queries might still have variables |
| 83 | +in them. For example: |
| 84 | + |
| 85 | +```text |
| 86 | +?- Rc<?T>: Clone |
| 87 | +``` |
| 88 | + |
| 89 | +might produce the answer: |
| 90 | + |
| 91 | +```text |
| 92 | +Rc<?T>: Clone |
| 93 | + continue? (y/n) |
| 94 | +``` |
| 95 | + |
| 96 | +After all, `Rc<?T>` is true **no matter what type `?T` is**. |
| 97 | + |
| 98 | +<a name="query-response"></a> |
| 99 | + |
| 100 | +## A trait query in rustc |
| 101 | + |
| 102 | +The trait queries in rustc work somewhat differently. Instead of |
| 103 | +trying to enumerate **all possible** answers for you, they are looking |
| 104 | +for an **unambiguous** answer. In particular, when they tell you the |
| 105 | +value for a type variable, that means that this is the **only possible |
| 106 | +instantiation** that you could use, given the current set of impls and |
| 107 | +where-clauses, that would be provable. (Internally within the solver, |
| 108 | +though, they can potentially enumerate all possible answers. See |
| 109 | +[the description of the SLG solver](./slg.html) for details.) |
| 110 | + |
| 111 | +The response to a trait query in rustc is typically a |
| 112 | +`Result<QueryResult<T>, NoSolution>` (where the `T` will vary a bit |
| 113 | +depending on the query itself). The `Err(NoSolution)` case indicates |
| 114 | +that the query was false and had no answers (e.g., `Box<i32>: Copy`). |
| 115 | +Otherwise, the `QueryResult` gives back information about the possible answer(s) |
| 116 | +we did find. It consists of four parts: |
| 117 | + |
| 118 | +- **Certainty:** tells you how sure we are of this answer. It can have two |
| 119 | + values: |
| 120 | + - `Proven` means that the result is known to be true. |
| 121 | + - This might be the result for trying to prove `Vec<i32>: Clone`, |
| 122 | + say, or `Rc<?T>: Clone`. |
| 123 | + - `Ambiguous` means that there were things we could not yet prove to |
| 124 | + be either true *or* false, typically because more type information |
| 125 | + was needed. (We'll see an example shortly.) |
| 126 | + - This might be the result for trying to prove `Vec<?T>: Clone`. |
| 127 | +- **Var values:** Values for each of the unbound inference variables |
| 128 | + (like `?T`) that appeared in your original query. (Remember that in Prolog, |
| 129 | + we had to infer these.) |
| 130 | + - As we'll see in the example below, we can get back var values even |
| 131 | + for `Ambiguous` cases. |
| 132 | +- **Region constraints:** these are relations that must hold between |
| 133 | + the lifetimes that you supplied as inputs. We'll ignore these here, |
| 134 | + but see the |
| 135 | + [section on handling regions in traits](./regions.html) for |
| 136 | + more details. |
| 137 | +- **Value:** The query result also comes with a value of type `T`. For |
| 138 | + some specialized queries – like normalizing associated types – |
| 139 | + this is used to carry back an extra result, but it's often just |
| 140 | + `()`. |
| 141 | + |
| 142 | +### Examples |
| 143 | + |
| 144 | +Let's work through an example query to see what all the parts mean. |
| 145 | +Consider [the `Borrow` trait][borrow]. This trait has a number of |
| 146 | +impls; among them, there are these two (for clarity, I've written the |
| 147 | +`Sized` bounds explicitly): |
| 148 | + |
| 149 | +[borrow]: https://doc.rust-lang.org/std/borrow/trait.Borrow.html |
| 150 | + |
| 151 | +```rust,ignore |
| 152 | +impl<T> Borrow<T> for T where T: ?Sized |
| 153 | +impl<T> Borrow<[T]> for Vec<T> where T: Sized |
| 154 | +``` |
| 155 | + |
| 156 | +**Example 1.** Imagine we are type-checking this (rather artificial) |
| 157 | +bit of code: |
| 158 | + |
| 159 | +```rust,ignore |
| 160 | +fn foo<A, B>(a: A, vec_b: Option<B>) where A: Borrow<B> { } |
| 161 | +
|
| 162 | +fn main() { |
| 163 | + let mut t: Vec<_> = vec![]; // Type: Vec<?T> |
| 164 | + let mut u: Option<_> = None; // Type: Option<?U> |
| 165 | + foo(t, u); // Example 1: requires `Vec<?T>: Borrow<?U>` |
| 166 | + ... |
| 167 | +} |
| 168 | +``` |
| 169 | + |
| 170 | +As the comments indicate, we first create two variables `t` and `u`; |
| 171 | +`t` is an empty vector and `u` is a `None` option. Both of these |
| 172 | +variables have unbound inference variables in their type: `?T` |
| 173 | +represents the elements in the vector `t` and `?U` represents the |
| 174 | +value stored in the option `u`. Next, we invoke `foo`; comparing the |
| 175 | +signature of `foo` to its arguments, we wind up with `A = Vec<?T>` and |
| 176 | +`B = ?U`. Therefore, the where clause on `foo` requires that `Vec<?T>: |
| 177 | +Borrow<?U>`. This is thus our first example trait query. |
| 178 | + |
| 179 | +There are many possible solutions to the query `Vec<?T>: Borrow<?U>`; |
| 180 | +for example: |
| 181 | + |
| 182 | +- `?U = Vec<?T>`, |
| 183 | +- `?U = [?T]`, |
| 184 | +- `?T = u32, ?U = [u32]` |
| 185 | +- and so forth. |
| 186 | + |
| 187 | +Therefore, the result we get back would be as follows (I'm going to |
| 188 | +ignore region constraints and the "value"): |
| 189 | + |
| 190 | +- Certainty: `Ambiguous` – we're not sure yet if this holds |
| 191 | +- Var values: `[?T = ?T, ?U = ?U]` – we learned nothing about the values of |
| 192 | + the variables |
| 193 | + |
| 194 | +In short, the query result says that it is too soon to say much about |
| 195 | +whether this trait is proven. During type-checking, this is not an |
| 196 | +immediate error: instead, the type checker would hold on to this |
| 197 | +requirement (`Vec<?T>: Borrow<?U>`) and wait. As we'll see in the next |
| 198 | +example, it may happen that `?T` and `?U` wind up constrained from |
| 199 | +other sources, in which case we can try the trait query again. |
| 200 | + |
| 201 | +**Example 2.** We can now extend our previous example a bit, |
| 202 | +and assign a value to `u`: |
| 203 | + |
| 204 | +```rust,ignore |
| 205 | +fn foo<A, B>(a: A, vec_b: Option<B>) where A: Borrow<B> { } |
| 206 | +
|
| 207 | +fn main() { |
| 208 | + // What we saw before: |
| 209 | + let mut t: Vec<_> = vec![]; // Type: Vec<?T> |
| 210 | + let mut u: Option<_> = None; // Type: Option<?U> |
| 211 | + foo(t, u); // `Vec<?T>: Borrow<?U>` => ambiguous |
| 212 | +
|
| 213 | + // New stuff: |
| 214 | + u = Some(vec![]); // ?U = Vec<?V> |
| 215 | +} |
| 216 | +``` |
| 217 | + |
| 218 | +As a result of this assignment, the type of `u` is forced to be |
| 219 | +`Option<Vec<?V>>`, where `?V` represents the element type of the |
| 220 | +vector. This in turn implies that `?U` is [unified] to `Vec<?V>`. |
| 221 | + |
| 222 | +[unified]: ../type-checking.html |
| 223 | + |
| 224 | +Let's suppose that the type checker decides to revisit the |
| 225 | +"as-yet-unproven" trait obligation we saw before, `Vec<?T>: |
| 226 | +Borrow<?U>`. `?U` is no longer an unbound inference variable; it now |
| 227 | +has a value, `Vec<?V>`. So, if we "refresh" the query with that value, we get: |
| 228 | + |
| 229 | +```text |
| 230 | +Vec<?T>: Borrow<Vec<?V>> |
| 231 | +``` |
| 232 | + |
| 233 | +This time, there is only one impl that applies, the reflexive impl: |
| 234 | + |
| 235 | +```text |
| 236 | +impl<T> Borrow<T> for T where T: ?Sized |
| 237 | +``` |
| 238 | + |
| 239 | +Therefore, the trait checker will answer: |
| 240 | + |
| 241 | +- Certainty: `Proven` |
| 242 | +- Var values: `[?T = ?T, ?V = ?T]` |
| 243 | + |
| 244 | +Here, it is saying that we have indeed proven that the obligation |
| 245 | +holds, and we also know that `?T` and `?V` are the same type (but we |
| 246 | +don't know what that type is yet!). |
| 247 | + |
| 248 | +(In fact, as the function ends here, the type checker would give an |
| 249 | +error at this point, since the element types of `t` and `u` are still |
| 250 | +not yet known, even though they are known to be the same.) |
| 251 | + |
| 252 | + |
0 commit comments