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