diff --git a/src/librustc/middle/traits/doc.rs b/src/librustc/middle/traits/doc.rs index c435697d85ca1..80697cb3a41db 100644 --- a/src/librustc/middle/traits/doc.rs +++ b/src/librustc/middle/traits/doc.rs @@ -272,6 +272,123 @@ nested obligation `int : Bar` to find out that `U=uint`. It would be good to only do *just as much* nested resolution as necessary. Currently, though, we just do a full resolution. +# Higher-ranked trait bounds + +One of the more subtle concepts at work are *higher-ranked trait +bounds*. An example of such a bound is `for<'a> MyTrait<&'a int>`. +Let's walk through how selection on higher-ranked trait references +works. + +## Basic matching and skolemization leaks + +Let's walk through the test `compile-fail/hrtb-just-for-static.rs` to see +how it works. The test starts with the trait `Foo`: + +```rust +trait Foo { + fn foo(&self, x: X) { } +} +``` + +Let's say we have a function `want_hrtb` that wants a type which +implements `Foo<&'a int>` for any `'a`: + +```rust +fn want_hrtb() where T : for<'a> Foo<&'a int> { ... } +``` + +Now we have a struct `AnyInt` that implements `Foo<&'a int>` for any +`'a`: + +```rust +struct AnyInt; +impl<'a> Foo<&'a int> for AnyInt { } +``` + +And the question is, does `AnyInt : for<'a> Foo<&'a int>`? We want the +answer to be yes. The algorithm for figuring it out is closely related +to the subtyping for higher-ranked types (which is described in +`middle::infer::higher_ranked::doc`, but also in a [paper by SPJ] that +I recommend you read). + +1. Skolemize the obligation. +2. Match the impl against the skolemized obligation. +3. Check for skolemization leaks. + +[paper by SPJ]: http://research.microsoft.com/en-us/um/people/simonpj/papers/higher-rank/ + +So let's work through our example. The first thing we would do is to +skolemize the obligation, yielding `AnyInt : Foo<&'0 int>` (here `'0` +represents skolemized region #0). Note that now have no quantifiers; +in terms of the compiler type, this changes from a `ty::PolyTraitRef` +to a `TraitRef`. We would then create the `TraitRef` from the impl, +using fresh variables for it's bound regions (and thus getting +`Foo<&'$a int>`, where `'$a` is the inference variable for `'a`). Next +we relate the two trait refs, yielding a graph with the constraint +that `'0 == '$a`. Finally, we check for skolemization "leaks" -- a +leak is basically any attempt to relate a skolemized region to another +skolemized region, or to any region that pre-existed the impl match. +The leak check is done by searching from the skolemized region to find +the set of regions that it is related to in any way. This is called +the "taint" set. To pass the check, that set must consist *solely* of +itself and region variables from the impl. If the taint set includes +any other region, then the match is a failure. In this case, the taint +set for `'0` is `{'0, '$a}`, and hence the check will succeed. + +Let's consider a failure case. Imagine we also have a struct + +```rust +struct StaticInt; +impl Foo<&'static int> for StaticInt; +``` + +We want the obligation `StaticInt : for<'a> Foo<&'a int>` to be +considered unsatisfied. The check begins just as before. `'a` is +skolemized to `'0` and the impl trait reference is instantiated to +`Foo<&'static int>`. When we relate those two, we get a constraint +like `'static == '0`. This means that the taint set for `'0` is `{'0, +'static}`, which fails the leak check. + +## Higher-ranked trait obligations + +Once the basic matching is done, we get to another interesting topic: +how to deal with impl obligations. I'll work through a simple example +here. Imagine we have the traits `Foo` and `Bar` and an associated impl: + +``` +trait Foo { + fn foo(&self, x: X) { } +} + +trait Bar { + fn bar(&self, x: X) { } +} + +impl Foo for F + where F : Bar +{ +} +``` + +Now let's say we have a obligation `for<'a> Foo<&'a int>` and we match +this impl. What obligation is generated as a result? We want to get +`for<'a> Bar<&'a int>`, but how does that happen? + +After the matching, we are in a position where we have a skolemized +substitution like `X => &'0 int`. If we apply this substitution to the +impl obligations, we get `F : Bar<&'0 int>`. Obviously this is not +directly usable because the skolemized region `'0` cannot leak out of +our computation. + +What we do is to create an inverse mapping from the taint set of `'0` +back to the original bound region (`'a`, here) that `'0` resulted +from. (This is done in `higher_ranked::plug_leaks`). We know that the +leak check passed, so this taint set consists solely of the skolemized +region itself plus various intermediate region variables. We then walk +the trait-reference and convert every region in that taint set back to +a late-bound region, so in this case we'd wind up with `for<'a> F : +Bar<&'a int>`. + # Caching and subtle considerations therewith In general we attempt to cache the results of trait selection. This @@ -400,6 +517,4 @@ there is no other type the user could enter. However, it is not future; we wouldn't have to guess types, in particular, we could be led by the impls. - - */ diff --git a/src/test/compile-fail/hrtb-conflate-regions.rs b/src/test/compile-fail/hrtb-conflate-regions.rs index 670e871084751..5eb8fd6931258 100644 --- a/src/test/compile-fail/hrtb-conflate-regions.rs +++ b/src/test/compile-fail/hrtb-conflate-regions.rs @@ -8,8 +8,8 @@ // option. This file may not be copied, modified, or distributed // except according to those terms. -// Test what an impl with only one bound region `'a` cannot be used to -// satisfy a constraint whre there are two bound regions. +// Test that an impl with only one bound region `'a` cannot be used to +// satisfy a constraint where there are two bound regions. trait Foo { fn foo(&self, x: X) { } diff --git a/src/test/compile-fail/hrtb-just-for-static.rs b/src/test/compile-fail/hrtb-just-for-static.rs index b21bae5653e22..36a45400eec1a 100644 --- a/src/test/compile-fail/hrtb-just-for-static.rs +++ b/src/test/compile-fail/hrtb-just-for-static.rs @@ -27,7 +27,7 @@ fn give_any() { want_hrtb::() } -// StaticInt only implements Foo<&'a int> for 'a, so it is an error. +// StaticInt only implements Foo<&'static int>, so it is an error. struct StaticInt; impl Foo<&'static int> for StaticInt { } fn give_static() { diff --git a/src/test/compile-fail/hrtb-type-outlives.rs b/src/test/compile-fail/hrtb-type-outlives.rs index 9a326aadc6a1c..9fe8f9ab46ddc 100644 --- a/src/test/compile-fail/hrtb-type-outlives.rs +++ b/src/test/compile-fail/hrtb-type-outlives.rs @@ -8,7 +8,7 @@ // option. This file may not be copied, modified, or distributed // except according to those terms. -// Test what happens when a HR obligation is applie to an impl with +// Test what happens when a HR obligation is applied to an impl with // "outlives" bounds. Currently we're pretty conservative here; this // will probably improve in time.