Clarifications and edits to hrtb chapter

src/trait-caching.md

@@ -51,4 +51,3 @@ and draw finer-grained distinctions, but that led to a serious of
 annoying and weird bugs like #22019 and #18290. This simple rule seems
 to be pretty clearly safe and also still retains a very high hit rate
 (~95% when compiling rustc).
-

src/trait-hrtb.md

@@ -1,14 +1,13 @@
 # Higher-ranked trait bounds
 
-One of the more subtle concepts at work are *higher-ranked trait
+One of the more subtle concepts in trait resolution is *higher-ranked trait
 bounds*. An example of such a bound is `for<'a> MyTrait<&'a isize>`.
 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`:
+Suppose we have a trait `Foo`:
 
 ```rust
 trait Foo<X> {
@@ -33,25 +32,34 @@ impl<'a> Foo<&'a isize> for AnyInt { }
 
 And the question is, does `AnyInt : for<'a> Foo<&'a isize>`? 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).
+to the subtyping for higher-ranked types (which is described in [here][hrsubtype]
+and also in a [paper by SPJ]. If you wish to understand higher-ranked
+subtyping, we recommend you read the paper). There are a few parts:
 
-1. Skolemize the obligation.
+**TODO**: We should define _skolemize_.
+
+1. _Skolemize_ the obligation.
 2. Match the impl against the skolemized obligation.
-3. Check for skolemization leaks.
+3. Check for _skolemization leaks_.
 
+[hrsubtype]: https://github.com/rust-lang/rust/tree/master/src/librustc/infer/higher_ranked/README.md
 [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
+So let's work through our example.
+
+1. The first thing we would do is to
 skolemize the obligation, yielding `AnyInt : Foo<&'0 isize>` (here `'0`
-represents skolemized region #0). Note that now have no quantifiers;
+represents skolemized region #0). Note that we 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 isize>`, where `'$a` is the inference variable for `'a`). Next
+`Foo<&'$a isize>`, where `'$a` is the inference variable for `'a`).
+
+2. Next
 we relate the two trait refs, yielding a graph with the constraint
-that `'0 == '$a`. Finally, we check for skolemization "leaks" – a
+that `'0 == '$a`.
+
+3. 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
@@ -75,6 +83,8 @@ skolemized to `'0` and the impl trait reference is instantiated to
 like `'static == '0`. This means that the taint set for `'0` is `{'0,
 'static}`, which fails the leak check.
 
+**TODO**: This is because `'static` is not a region variable but is in the taint set, right?
+
 ## Higher-ranked trait obligations
 
 Once the basic matching is done, we get to another interesting topic:
@@ -96,9 +106,9 @@ impl<X,F> Foo<X> for F
 }
 ```
 
-Now let's say we have a obligation `for<'a> Foo<&'a isize>` and we match
+Now let's say we have a obligation `Baz: for<'a> Foo<&'a isize>` and we match
 this impl. What obligation is generated as a result? We want to get
-`for<'a> Bar<&'a isize>`, but how does that happen?
+`Baz: for<'a> Bar<&'a isize>`, but how does that happen?
 
 After the matching, we are in a position where we have a skolemized
 substitution like `X => &'0 isize`. If we apply this substitution to the
@@ -112,5 +122,4 @@ 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 isize>`.
+a late-bound region, so in this case we'd wind up with `Baz: for<'a> Bar<&'a isize>`.