|
| 1 | +// Copyright 2014 The Rust Project Developers. See the COPYRIGHT |
| 2 | +// file at the top-level directory of this distribution and at |
| 3 | +// http://rust-lang.org/COPYRIGHT. |
| 4 | +// |
| 5 | +// Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or |
| 6 | +// http://www.apache.org/licenses/LICENSE-2.0> or the MIT license |
| 7 | +// <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your |
| 8 | +// option. This file may not be copied, modified, or distributed |
| 9 | +// except according to those terms. |
| 10 | + |
| 11 | +/*! |
| 12 | +
|
| 13 | +# TRAIT RESOLUTION |
| 14 | +
|
| 15 | +This document describes the general process and points out some non-obvious |
| 16 | +things. |
| 17 | +
|
| 18 | +## Major concepts |
| 19 | +
|
| 20 | +Trait resolution is the process of pairing up an impl with each |
| 21 | +reference to a trait. So, for example, if there is a generic function like: |
| 22 | +
|
| 23 | + fn clone_slice<T:Clone>(x: &[T]) -> Vec<T> { ... } |
| 24 | +
|
| 25 | +and then a call to that function: |
| 26 | +
|
| 27 | + let v: Vec<int> = clone_slice([1, 2, 3].as_slice()) |
| 28 | +
|
| 29 | +it is the job of trait resolution to figure out (in which case) |
| 30 | +whether there exists an impl of `int : Clone` |
| 31 | +
|
| 32 | +Note that in some cases, like generic functions, we may not be able to |
| 33 | +find a specific impl, but we can figure out that the caller must |
| 34 | +provide an impl. To see what I mean, consider the body of `clone_slice`: |
| 35 | +
|
| 36 | + fn clone_slice<T:Clone>(x: &[T]) -> Vec<T> { |
| 37 | + let mut v = Vec::new(); |
| 38 | + for e in x.iter() { |
| 39 | + v.push((*e).clone()); // (*) |
| 40 | + } |
| 41 | + } |
| 42 | +
|
| 43 | +The line marked `(*)` is only legal if `T` (the type of `*e`) |
| 44 | +implements the `Clone` trait. Naturally, since we don't know what `T` |
| 45 | +is, we can't find the specific impl; but based on the bound `T:Clone`, |
| 46 | +we can say that there exists an impl which the caller must provide. |
| 47 | +
|
| 48 | +We use the term *obligation* to refer to a trait reference in need of |
| 49 | +an impl. |
| 50 | +
|
| 51 | +## Overview |
| 52 | +
|
| 53 | +Trait resolution consists of three major parts: |
| 54 | +
|
| 55 | +- SELECTION: Deciding how to resolve a specific obligation. For |
| 56 | + example, selection might decide that a specific obligation can be |
| 57 | + resolved by employing an impl which matches the self type, or by |
| 58 | + using a parameter bound. In the case of an impl, Selecting one |
| 59 | + obligation can create *nested obligations* because of where clauses |
| 60 | + on the impl itself. |
| 61 | +
|
| 62 | +- FULFILLMENT: The fulfillment code is what tracks that obligations |
| 63 | + are completely fulfilled. Basically it is a worklist of obligations |
| 64 | + to be selected: once selection is successful, the obligation is |
| 65 | + removed from the worklist and any nested obligations are enqueued. |
| 66 | +
|
| 67 | +- COHERENCE: The coherence checks are intended to ensure that there |
| 68 | + are never overlapping impls, where two impls could be used with |
| 69 | + equal precedence. |
| 70 | +
|
| 71 | +## Selection |
| 72 | +
|
| 73 | +Selection is the process of deciding whether an obligation can be |
| 74 | +resolved and, if so, how it is to be resolved (via impl, where clause, etc). |
| 75 | +The main interface is the `select()` function, which takes an obligation |
| 76 | +and returns a `SelectionResult`. There are three possible outcomes: |
| 77 | +
|
| 78 | +- `Ok(Some(selection))` -- yes, the obligation can be resolved, and |
| 79 | + `selection` indicates how. If the impl was resolved via an impl, |
| 80 | + then `selection` may also indicate nested obligations that are required |
| 81 | + by the impl. |
| 82 | +
|
| 83 | +- `Ok(None)` -- we are not yet sure whether the obligation can be |
| 84 | + resolved or not. This happens most commonly when the obligation |
| 85 | + contains unbound type variables. |
| 86 | +
|
| 87 | +- `Err(err)` -- the obligation definitely cannot be resolved due to a |
| 88 | + type error, or because there are no impls that could possibly apply, |
| 89 | + etc. |
| 90 | +
|
| 91 | +The basic algorithm for selection is broken into two big phases: |
| 92 | +candidate assembly and confirmation. |
| 93 | +
|
| 94 | +### Candidate assembly |
| 95 | +
|
| 96 | +Searches for impls/where-clauses/etc that might |
| 97 | +possibly be used to satisfy the obligation. Each of those is called |
| 98 | +a candidate. To avoid ambiguity, we want to find exactly one |
| 99 | +candidate that is definitively applicable. In some cases, we may not |
| 100 | +know whether an impl/where-clause applies or not -- this occurs when |
| 101 | +the obligation contains unbound inference variables. |
| 102 | +
|
| 103 | +One important point is that candidate assembly considers *only the |
| 104 | +input types* of the obligation when deciding whether an impl applies |
| 105 | +or not. Consider the following example: |
| 106 | +
|
| 107 | + trait Convert<T> { // T is output, Self is input |
| 108 | + fn convert(&self) -> T; |
| 109 | + } |
| 110 | +
|
| 111 | + impl Convert<uint> for int { ... } |
| 112 | +
|
| 113 | +Now assume we have an obligation `int : Convert<char>`. During |
| 114 | +candidate assembly, the impl above would be considered a definitively |
| 115 | +applicable candidate, because it has the same self type (`int`). The |
| 116 | +fact that the output type parameter `T` is `uint` on the impl and |
| 117 | +`char` in the obligation is not considered. |
| 118 | +
|
| 119 | +#### Skolemization |
| 120 | +
|
| 121 | +We (at least currently) wish to guarantee "crate concatenability" -- |
| 122 | +which basically means that you could take two crates, concatenate |
| 123 | +them textually, and the combined crate would continue to compile. The |
| 124 | +only real way that this relates to trait matching is with |
| 125 | +inference. We have to be careful not to influence unbound type |
| 126 | +variables during the selection process, basically. |
| 127 | +
|
| 128 | +Here is an example: |
| 129 | +
|
| 130 | + trait Foo { fn method() { ... }} |
| 131 | + impl Foo for int { ... } |
| 132 | +
|
| 133 | + fn something() { |
| 134 | + let mut x = None; // `x` has type `Option<?>` |
| 135 | + loop { |
| 136 | + match x { |
| 137 | + Some(ref y) => { // `y` has type ? |
| 138 | + y.method(); // (*) |
| 139 | + ... |
| 140 | + }}} |
| 141 | + } |
| 142 | +
|
| 143 | +The question is, can we resolve the call to `y.method()`? We don't yet |
| 144 | +know what type `y` has. However, there is only one impl in scope, and |
| 145 | +it is for `int`, so perhaps we could deduce that `y` *must* have type |
| 146 | +`int` (and hence the type of `x` is `Option<int>`)? This is actually |
| 147 | +sound reasoning: `int` is the only type in scope that could possibly |
| 148 | +make this program type check. However, this deduction is a bit |
| 149 | +"unstable", though, because if we concatenated with another crate that |
| 150 | +defined a newtype and implemented `Foo` for this newtype, then the |
| 151 | +inference would fail, because there would be two potential impls, not |
| 152 | +one. |
| 153 | +
|
| 154 | +It is unclear how important this property is. It might be nice to drop it. |
| 155 | +But for the time being we maintain it. |
| 156 | +
|
| 157 | +The way we do this is by *skolemizing* the obligation self type during |
| 158 | +the selection process -- skolemizing means, basically, replacing all |
| 159 | +unbound type variables with a new "skolemized" type. Each skolemized |
| 160 | +type is basically considered "as if" it were some fresh type that is |
| 161 | +distinct from all other types. The skolemization process also replaces |
| 162 | +lifetimes with `'static`, see the section on lifetimes below for an |
| 163 | +explanation. |
| 164 | +
|
| 165 | +In the example above, this means that when matching `y.method()` we |
| 166 | +would convert the type of `y` from a type variable `?` to a skolemized |
| 167 | +type `X`. Then, since `X` cannot unify with `int`, the match would |
| 168 | +fail. Special code exists to check that the match failed because a |
| 169 | +skolemized type could not be unified with another kind of type -- this is |
| 170 | +not considered a definitive failure, but rather an ambiguous result, |
| 171 | +since if the type variable were later to be unified with int, then this |
| 172 | +obligation could be resolved then. |
| 173 | +
|
| 174 | +*Note:* Currently, method matching does not use the trait resolution |
| 175 | +code, so if you in fact type in the example above, it may |
| 176 | +compile. Hopefully this will be fixed in later patches. |
| 177 | +
|
| 178 | +#### Matching |
| 179 | +
|
| 180 | +The subroutines that decide whether a particular impl/where-clause/etc |
| 181 | +applies to a particular obligation. At the moment, this amounts to |
| 182 | +unifying the self types, but in the future we may also recursively |
| 183 | +consider some of the nested obligations, in the case of an impl. |
| 184 | +
|
| 185 | +#### Lifetimes and selection |
| 186 | +
|
| 187 | +Because of how that lifetime inference works, it is not possible to |
| 188 | +give back immediate feedback as to whether a unification or subtype |
| 189 | +relationship between lifetimes holds or not. Therefore, lifetime |
| 190 | +matching is *not* considered during selection. This is achieved by |
| 191 | +having the skolemization process just replace *ALL* lifetimes with |
| 192 | +`'static`. Later, during confirmation, the non-skolemized self-type |
| 193 | +will be unified with the type from the impl (or whatever). This may |
| 194 | +yield lifetime constraints that will later be found to be in error (in |
| 195 | +contrast, the non-lifetime-constraints have already been checked |
| 196 | +during selection and can never cause an error, though naturally they |
| 197 | +may lead to other errors downstream). |
| 198 | +
|
| 199 | +#### Where clauses |
| 200 | +
|
| 201 | +Besides an impl, the other major way to resolve an obligation is via a |
| 202 | +where clause. The selection process is always given a *parameter |
| 203 | +environment* which contains a list of where clauses, which are |
| 204 | +basically obligations that can assume are satisfiable. We will iterate |
| 205 | +over that list and check whether our current obligation can be found |
| 206 | +in that list, and if so it is considered satisfied. More precisely, we |
| 207 | +want to check whether there is a where-clause obligation that is for |
| 208 | +the same trait (or some subtrait) and for which the self types match, |
| 209 | +using the definition of *matching* given above. |
| 210 | +
|
| 211 | +Consider this simple example: |
| 212 | +
|
| 213 | + trait A1 { ... } |
| 214 | + trait A2 : A1 { ... } |
| 215 | +
|
| 216 | + trait B { ... } |
| 217 | +
|
| 218 | + fn foo<X:A2+B> { ... } |
| 219 | +
|
| 220 | +Clearly we can use methods offered by `A1`, `A2`, or `B` within the |
| 221 | +body of `foo`. In each case, that will incur an obligation like `X : |
| 222 | +A1` or `X : A2`. The parameter environment will contain two |
| 223 | +where-clauses, `X : A2` and `X : B`. For each obligation, then, we |
| 224 | +search this list of where-clauses. To resolve an obligation `X:A1`, |
| 225 | +we would note that `X:A2` implies that `X:A1`. |
| 226 | +
|
| 227 | +### Confirmation |
| 228 | +
|
| 229 | +Confirmation unifies the output type parameters of the trait with the |
| 230 | +values found in the obligation, possibly yielding a type error. If we |
| 231 | +return to our example of the `Convert` trait from the previous |
| 232 | +section, confirmation is where an error would be reported, because the |
| 233 | +impl specified that `T` would be `uint`, but the obligation reported |
| 234 | +`char`. Hence the result of selection would be an error. |
| 235 | +
|
| 236 | +### Selection during translation |
| 237 | +
|
| 238 | +During type checking, we do not store the results of trait selection. |
| 239 | +We simply wish to verify that trait selection will succeed. Then |
| 240 | +later, at trans time, when we have all concrete types available, we |
| 241 | +can repeat the trait selection. In this case, we do not consider any |
| 242 | +where-clauses to be in scope. We know that therefore each resolution |
| 243 | +will resolve to a particular impl. |
| 244 | +
|
| 245 | +One interesting twist has to do with nested obligations. In general, in trans, |
| 246 | +we only need to do a "shallow" selection for an obligation. That is, we wish to |
| 247 | +identify which impl applies, but we do not (yet) need to decide how to select |
| 248 | +any nested obligations. Nonetheless, we *do* currently do a complete resolution, |
| 249 | +and that is because it can sometimes inform the results of type inference. That is, |
| 250 | +we do not have the full substitutions in terms of the type varibales of the impl available |
| 251 | +to us, so we must run trait selection to figure everything out. |
| 252 | +
|
| 253 | +Here is an example: |
| 254 | +
|
| 255 | + trait Foo { ... } |
| 256 | + impl<U,T:Bar<U>> Foo for Vec<T> { ... } |
| 257 | +
|
| 258 | + impl Bar<uint> for int { ... } |
| 259 | +
|
| 260 | +After one shallow round of selection for an obligation like `Vec<int> |
| 261 | +: Foo`, we would know which impl we want, and we would know that |
| 262 | +`T=int`, but we do not know the type of `U`. We must select the |
| 263 | +nested obligation `int : Bar<U>` to find out that `U=uint`. |
| 264 | +
|
| 265 | +It would be good to only do *just as much* nested resolution as |
| 266 | +necessary. Currently, though, we just do a full resolution. |
| 267 | +
|
| 268 | +*/ |
0 commit comments