|
| 1 | +# Higher-ranked trait bounds |
| 2 | + |
| 3 | +One of the more subtle concepts in trait resolution is *higher-ranked trait |
| 4 | +bounds*. An example of such a bound is `for<'a> MyTrait<&'a isize>`. |
| 5 | +Let's walk through how selection on higher-ranked trait references |
| 6 | +works. |
| 7 | + |
| 8 | +## Basic matching and skolemization leaks |
| 9 | + |
| 10 | +Suppose we have a trait `Foo`: |
| 11 | + |
| 12 | +```rust |
| 13 | +trait Foo<X> { |
| 14 | + fn foo(&self, x: X) { } |
| 15 | +} |
| 16 | +``` |
| 17 | + |
| 18 | +Let's say we have a function `want_hrtb` that wants a type which |
| 19 | +implements `Foo<&'a isize>` for any `'a`: |
| 20 | + |
| 21 | +```rust |
| 22 | +fn want_hrtb<T>() where T : for<'a> Foo<&'a isize> { ... } |
| 23 | +``` |
| 24 | + |
| 25 | +Now we have a struct `AnyInt` that implements `Foo<&'a isize>` for any |
| 26 | +`'a`: |
| 27 | + |
| 28 | +```rust |
| 29 | +struct AnyInt; |
| 30 | +impl<'a> Foo<&'a isize> for AnyInt { } |
| 31 | +``` |
| 32 | + |
| 33 | +And the question is, does `AnyInt : for<'a> Foo<&'a isize>`? We want the |
| 34 | +answer to be yes. The algorithm for figuring it out is closely related |
| 35 | +to the subtyping for higher-ranked types (which is described in [here][hrsubtype] |
| 36 | +and also in a [paper by SPJ]. If you wish to understand higher-ranked |
| 37 | +subtyping, we recommend you read the paper). There are a few parts: |
| 38 | + |
| 39 | +**TODO**: We should define _skolemize_. |
| 40 | + |
| 41 | +1. _Skolemize_ the obligation. |
| 42 | +2. Match the impl against the skolemized obligation. |
| 43 | +3. Check for _skolemization leaks_. |
| 44 | + |
| 45 | +[hrsubtype]: https://github.com/rust-lang/rust/tree/master/src/librustc/infer/higher_ranked/README.md |
| 46 | +[paper by SPJ]: http://research.microsoft.com/en-us/um/people/simonpj/papers/higher-rank/ |
| 47 | + |
| 48 | +So let's work through our example. |
| 49 | + |
| 50 | +1. The first thing we would do is to |
| 51 | +skolemize the obligation, yielding `AnyInt : Foo<&'0 isize>` (here `'0` |
| 52 | +represents skolemized region #0). Note that we now have no quantifiers; |
| 53 | +in terms of the compiler type, this changes from a `ty::PolyTraitRef` |
| 54 | +to a `TraitRef`. We would then create the `TraitRef` from the impl, |
| 55 | +using fresh variables for it's bound regions (and thus getting |
| 56 | +`Foo<&'$a isize>`, where `'$a` is the inference variable for `'a`). |
| 57 | + |
| 58 | +2. Next |
| 59 | +we relate the two trait refs, yielding a graph with the constraint |
| 60 | +that `'0 == '$a`. |
| 61 | + |
| 62 | +3. Finally, we check for skolemization "leaks" – a |
| 63 | +leak is basically any attempt to relate a skolemized region to another |
| 64 | +skolemized region, or to any region that pre-existed the impl match. |
| 65 | +The leak check is done by searching from the skolemized region to find |
| 66 | +the set of regions that it is related to in any way. This is called |
| 67 | +the "taint" set. To pass the check, that set must consist *solely* of |
| 68 | +itself and region variables from the impl. If the taint set includes |
| 69 | +any other region, then the match is a failure. In this case, the taint |
| 70 | +set for `'0` is `{'0, '$a}`, and hence the check will succeed. |
| 71 | + |
| 72 | +Let's consider a failure case. Imagine we also have a struct |
| 73 | + |
| 74 | +```rust |
| 75 | +struct StaticInt; |
| 76 | +impl Foo<&'static isize> for StaticInt; |
| 77 | +``` |
| 78 | + |
| 79 | +We want the obligation `StaticInt : for<'a> Foo<&'a isize>` to be |
| 80 | +considered unsatisfied. The check begins just as before. `'a` is |
| 81 | +skolemized to `'0` and the impl trait reference is instantiated to |
| 82 | +`Foo<&'static isize>`. When we relate those two, we get a constraint |
| 83 | +like `'static == '0`. This means that the taint set for `'0` is `{'0, |
| 84 | +'static}`, which fails the leak check. |
| 85 | + |
| 86 | +**TODO**: This is because `'static` is not a region variable but is in the taint set, right? |
| 87 | + |
| 88 | +## Higher-ranked trait obligations |
| 89 | + |
| 90 | +Once the basic matching is done, we get to another interesting topic: |
| 91 | +how to deal with impl obligations. I'll work through a simple example |
| 92 | +here. Imagine we have the traits `Foo` and `Bar` and an associated impl: |
| 93 | + |
| 94 | +```rust |
| 95 | +trait Foo<X> { |
| 96 | + fn foo(&self, x: X) { } |
| 97 | +} |
| 98 | + |
| 99 | +trait Bar<X> { |
| 100 | + fn bar(&self, x: X) { } |
| 101 | +} |
| 102 | + |
| 103 | +impl<X,F> Foo<X> for F |
| 104 | + where F : Bar<X> |
| 105 | +{ |
| 106 | +} |
| 107 | +``` |
| 108 | + |
| 109 | +Now let's say we have a obligation `Baz: for<'a> Foo<&'a isize>` and we match |
| 110 | +this impl. What obligation is generated as a result? We want to get |
| 111 | +`Baz: for<'a> Bar<&'a isize>`, but how does that happen? |
| 112 | + |
| 113 | +After the matching, we are in a position where we have a skolemized |
| 114 | +substitution like `X => &'0 isize`. If we apply this substitution to the |
| 115 | +impl obligations, we get `F : Bar<&'0 isize>`. Obviously this is not |
| 116 | +directly usable because the skolemized region `'0` cannot leak out of |
| 117 | +our computation. |
| 118 | + |
| 119 | +What we do is to create an inverse mapping from the taint set of `'0` |
| 120 | +back to the original bound region (`'a`, here) that `'0` resulted |
| 121 | +from. (This is done in `higher_ranked::plug_leaks`). We know that the |
| 122 | +leak check passed, so this taint set consists solely of the skolemized |
| 123 | +region itself plus various intermediate region variables. We then walk |
| 124 | +the trait-reference and convert every region in that taint set back to |
| 125 | +a late-bound region, so in this case we'd wind up with `Baz: for<'a> Bar<&'a isize>`. |
0 commit comments