Document new algorithm at a high-level.

4 files changed, 121 insertions, 6 deletions

diff --git a/src/librustc/middle/traits/doc.rs b/src/librustc/middle/traits/doc.rs
index c435697d85c..80697cb3a41 100644
--- a/src/librustc/middle/traits/doc.rs
+++ b/src/librustc/middle/traits/doc.rs
@@ -272,6 +272,123 @@ nested obligation `int : Bar<U>` 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<X> {
+    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<T>() 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<X> {
+    fn foo(&self, x: X) { }
+}
+
+trait Bar<X> {
+    fn bar(&self, x: X) { }
+}
+
+impl<X,F> Foo<X> for F
+    where F : Bar<X>
+{
+}
+```
+
+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 670e8710847..5eb8fd69312 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<X> {
     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 b21bae5653e..36a45400eec 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::<AnyInt>()
 }
 
-// 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 9a326aadc6a..9fe8f9ab46d 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.