Remove details about chalk and point to Chalk Book instead.

2020-04-19 22:48:45 +08:00 · 2020-04-19 22:48:45 +08:00 · 7d843fcd4f
parent 1b0f87c8dc
commit 7d843fcd4f
15 changed files with 48 additions and 3183 deletions
--- a/src/SUMMARY.md
+++ b/src/SUMMARY.md
@ -72,24 +72,13 @@
        - [`TypeFolder` and `TypeFoldable`](./ty-fold.md)
        - [Generic arguments](./generic_arguments.md)
    - [Type inference](./type-inference.md)
-    - [Trait solving (old-style)](./traits/resolution.md)
+    - [Trait solving](./traits/resolution.md)
        - [Higher-ranked trait bounds](./traits/hrtb.md)
        - [Caching subtleties](./traits/caching.md)
        - [Specialization](./traits/specialization.md)
-    - [Trait solving (new-style)](./traits/index.md)
+        - [Chalk-based trait solving](./traits/chalk.md)
-        - [Lowering to logic](./traits/lowering-to-logic.md)
+        - [Region constraints](./traits/regions.md)
-            - [Goals and clauses](./traits/goals-and-clauses.md)
+        - [Chalk-oriented lowering module in rustc](./traits/lowering-module.md)
            - [Equality and associated types](./traits/associated-types.md)
            - [Implied bounds](./traits/implied-bounds.md)
            - [Region constraints](./traits/regions.md)
            - [The lowering module in rustc](./traits/lowering-module.md)
            - [Lowering rules](./traits/lowering-rules.md)
            - [Well-formedness checking](./traits/wf.md)
        - [Canonical queries](./traits/canonical-queries.md)
            - [Canonicalization](./traits/canonicalization.md)
        - [The SLG solver](./traits/slg.md)
        - [An Overview of Chalk](./traits/chalk-overview.md)
        - [Bibliography](./traits/bibliography.md)
    - [Type checking](./type-checking.md)
        - [Method Lookup](./method-lookup.md)
        - [Variance](./variance.md)
--- a/src/traits/associated-types.md
+++ b/src/traits/associated-types.md
@ -1,168 +0,0 @@
 # Equality and associated types
 This section covers how the trait system handles equality between
 associated types. The full system consists of several moving parts,
 which we will introduce one by one:
 - Projection and the `Normalize` predicate
 - Placeholder associated type projections
 - The `ProjectionEq` predicate
 - Integration with unification
 ## Associated type projection and normalization
 When a trait defines an associated type (e.g.,
 [the `Item` type in the `IntoIterator` trait][intoiter-item]), that
 type can be referenced by the user using an **associated type
 projection** like `<Option<u32> as IntoIterator>::Item`.
 > Often, people will use the shorthand syntax `T::Item`. Presently, that
 > syntax is expanded during ["type collection"](../type-checking.html) into the
 > explicit form, though that is something we may want to change in the future.
 [intoiter-item]: https://doc.rust-lang.org/nightly/core/iter/trait.IntoIterator.html#associatedtype.Item
 <a name="normalize"></a>
 In some cases, associated type projections can be **normalized** –
 that is, simplified – based on the types given in an impl. So, to
 continue with our example, the impl of `IntoIterator` for `Option<T>`
 declares (among other things) that `Item = T`:
 ```rust,ignore
 impl<T> IntoIterator for Option<T> {
  type Item = T;
  ...
 }
 ```
 This means we can normalize the projection `<Option<u32> as
 IntoIterator>::Item` to just `u32`.
 In this case, the projection was a "monomorphic" one – that is, it
 did not have any type parameters.  Monomorphic projections are special
 because they can **always** be fully normalized.
 Often, we can normalize other associated type projections as well. For
 example, `<Option<?T> as IntoIterator>::Item`, where `?T` is an inference
 variable, can be normalized to just `?T`.
 In our logic, normalization is defined by a predicate
 `Normalize`. The `Normalize` clauses arise only from
 impls. For example, the `impl` of `IntoIterator` for `Option<T>` that
 we saw above would be lowered to a program clause like so:
 ```text
 forall<T> {
    Normalize(<Option<T> as IntoIterator>::Item -> T) :-
        Implemented(Option<T>: IntoIterator)
 }
 ```
 where in this case, the one `Implemented` condition is always true.
 > Since we do not permit quantification over traits, this is really more like
 > a family of program clauses, one for each associated type.
 We could apply that rule to normalize either of the examples that
 we've seen so far.
 ## Placeholder associated types
 Sometimes however we want to work with associated types that cannot be
 normalized. For example, consider this function:
 ```rust,ignore
 fn foo<T: IntoIterator>(...) { ... }
 ```
 In this context, how would we normalize the type `T::Item`?
 Without knowing what `T` is, we can't really do so. To represent this case,
 we introduce a type called a **placeholder associated type projection**. This
 is written like so: `(IntoIterator::Item)<T>`.
 You may note that it looks a lot like a regular type (e.g., `Option<T>`),
 except that the "name" of the type is `(IntoIterator::Item)`. This is not an
 accident: placeholder associated type projections work just like ordinary
 types like `Vec<T>` when it comes to unification. That is, they are only
 considered equal if (a) they are both references to the same associated type,
 like `IntoIterator::Item` and (b) their type arguments are equal.
 Placeholder associated types are never written directly by the user.
 They are used internally by the trait system only, as we will see
 shortly.
 In rustc, they correspond to the `TyKind::UnnormalizedProjectionTy` enum
 variant, declared in [`librustc_middle/ty/sty.rs`][sty]. In chalk, we use an
 `ApplicationTy` with a name living in a special namespace dedicated to
 placeholder associated types (see the `TypeName` enum declared in
 [`chalk-ir/src/lib.rs`][chalk_type_name]).
 [sty]: https://github.com/rust-lang/rust/blob/master/src/librustc_middle/ty/sty.rs
 [chalk_type_name]: https://github.com/rust-lang-nursery/chalk/blob/master/chalk-ir/src/lib.rs
 ## Projection equality
 So far we have seen two ways to answer the question of "When can we
 consider an associated type projection equal to another type?":
 - the `Normalize` predicate could be used to transform projections when we
  knew which impl applied;
 - **placeholder** associated types can be used when we don't. This is also
  known as **lazy normalization**.
 We now introduce the `ProjectionEq` predicate to bring those two cases
 together. The `ProjectionEq` predicate looks like so:
 ```text
 ProjectionEq(<T as IntoIterator>::Item = U)
 ```
 and we will see that it can be proven *either* via normalization or
 via the placeholder type. As part of lowering an associated type declaration from
 some trait, we create two program clauses for `ProjectionEq`:
 ```text
 forall<T, U> {
    ProjectionEq(<T as IntoIterator>::Item = U) :-
        Normalize(<T as IntoIterator>::Item -> U)
 }
 forall<T> {
    ProjectionEq(<T as IntoIterator>::Item = (IntoIterator::Item)<T>)
 }
 ```
 These are the only two `ProjectionEq` program clauses we ever make for
 any given associated item.
 ## Integration with unification
 Now we are ready to discuss how associated type equality integrates
 with unification. As described in the
 [type inference](../type-inference.html) section, unification is
 basically a procedure with a signature like this:
 ```text
 Unify(A, B) = Result<(Subgoals, RegionConstraints), NoSolution>
 ```
 In other words, we try to unify two things A and B. That procedure
 might just fail, in which case we get back `Err(NoSolution)`. This
 would happen, for example, if we tried to unify `u32` and `i32`.
 The key point is that, on success, unification can also give back to
 us a set of subgoals that still remain to be proven. (It can also give
 back region constraints, but those are not relevant here).
 Whenever unification encounters a non-placeholder associated type
 projection P being equated with some other type T, it always succeeds,
 but it produces a subgoal `ProjectionEq(P = T)` that is propagated
 back up. Thus it falls to the ordinary workings of the trait system
 to process that constraint.
 > If we unify two projections P1 and P2, then unification produces a
 > variable X and asks us to prove that `ProjectionEq(P1 = X)` and
 > `ProjectionEq(P2 = X)`. (That used to be needed in an older system to
 > prevent cycles; I rather doubt it still is. -nmatsakis)
--- a/src/traits/bibliography.md
+++ b/src/traits/bibliography.md
@ -1,27 +0,0 @@
 # Bibliography
 If you'd like to read more background material, here are some
 recommended texts and papers:
 [Programming with Higher-order Logic][phl], by Dale Miller and Gopalan
 Nadathur, covers the key concepts of Lambda prolog. Although it's a
 slim little volume, it's the kind of book where you learn something
 new every time you open it.
 [phl]: https://www.amazon.com/Programming-Higher-Order-Logic-Dale-Miller/dp/052187940X
 <a name="pphhf"></a>
 ["A proof procedure for the logic of Hereditary Harrop formulas"][pphhf],
 by Gopalan Nadathur. This paper covers the basics of universes,
 environments, and Lambda Prolog-style proof search. Quite readable.
 [pphhf]: https://dl.acm.org/citation.cfm?id=868380
 <a name="slg"></a> 
 ["A new formulation of tabled resolution with delay"][nftrd], by
 Theresa Swift. This paper gives a kind of abstract treatment of the
 SLG formulation that is the basis for our on-demand solver.
 [nftrd]: https://dl.acm.org/citation.cfm?id=651202
--- a/src/traits/canonical-queries.md
+++ b/src/traits/canonical-queries.md
@ -1,252 +0,0 @@
 # Canonical queries
 The "start" of the trait system is the **canonical query** (these are
 both queries in the more general sense of the word – something you
 would like to know the answer to – and in the
 [rustc-specific sense](../query.html)).  The idea is that the type
 checker or other parts of the system, may in the course of doing their
 thing want to know whether some trait is implemented for some type
 (e.g., is `u32: Debug` true?). Or they may want to
 [normalize some associated type](./associated-types.html).
 This section covers queries at a fairly high level of abstraction. The
 subsections look a bit more closely at how these ideas are implemented
 in rustc.
 ## The traditional, interactive Prolog query
 In a traditional Prolog system, when you start a query, the solver
 will run off and start supplying you with every possible answer it can
 find. So given something like this:
 ```text
 ?- Vec<i32>: AsRef<?U>
 ```
 The solver might answer:
 ```text
 Vec<i32>: AsRef<[i32]>
    continue? (y/n)
 ```
 This `continue` bit is interesting. The idea in Prolog is that the
 solver is finding **all possible** instantiations of your query that
 are true. In this case, if we instantiate `?U = [i32]`, then the query
 is true (note that a traditional Prolog interface does not, directly,
 tell us a value for `?U`, but we can infer one by unifying the
 response with our original query – Rust's solver gives back a
 substitution instead). If we were to hit `y`, the solver might then
 give us another possible answer:
 ```text
 Vec<i32>: AsRef<Vec<i32>>
    continue? (y/n)
 ```
 This answer derives from the fact that there is a reflexive impl
 (`impl<T> AsRef<T> for T`) for `AsRef`. If were to hit `y` again,
 then we might get back a negative response:
 ```text
 no
 ```
 Naturally, in some cases, there may be no possible answers, and hence
 the solver will just give me back `no` right away:
 ```text
 ?- Box<i32>: Copy
    no
 ```
 In some cases, there might be an infinite number of responses. So for
 example if I gave this query, and I kept hitting `y`, then the solver
 would never stop giving me back answers:
 ```text
 ?- Vec<?U>: Clone
    Vec<i32>: Clone
        continue? (y/n)
    Vec<Box<i32>>: Clone
        continue? (y/n)
    Vec<Box<Box<i32>>>: Clone
        continue? (y/n)
    Vec<Box<Box<Box<i32>>>>: Clone
        continue? (y/n)
 ```
 As you can imagine, the solver will gleefully keep adding another
 layer of `Box` until we ask it to stop, or it runs out of memory.
 Another interesting thing is that queries might still have variables
 in them. For example:
 ```text
 ?- Rc<?T>: Clone
 ```
 might produce the answer:
 ```text
 Rc<?T>: Clone
    continue? (y/n)
 ```
 After all, `Rc<?T>` is true **no matter what type `?T` is**.
 <a name="query-response"></a>
 ## A trait query in rustc
 The trait queries in rustc work somewhat differently. Instead of
 trying to enumerate **all possible** answers for you, they are looking
 for an **unambiguous** answer. In particular, when they tell you the
 value for a type variable, that means that this is the **only possible
 instantiation** that you could use, given the current set of impls and
 where-clauses, that would be provable. (Internally within the solver,
 though, they can potentially enumerate all possible answers. See
 [the description of the SLG solver](./slg.html) for details.)
 The response to a trait query in rustc is typically a
 `Result<QueryResult<T>, NoSolution>` (where the `T` will vary a bit
 depending on the query itself). The `Err(NoSolution)` case indicates
 that the query was false and had no answers (e.g., `Box<i32>: Copy`).
 Otherwise, the `QueryResult` gives back information about the possible answer(s)
 we did find. It consists of four parts:
 - **Certainty:** tells you how sure we are of this answer. It can have two
  values:
  - `Proven` means that the result is known to be true.
    - This might be the result for trying to prove `Vec<i32>: Clone`,
      say, or `Rc<?T>: Clone`.
  - `Ambiguous` means that there were things we could not yet prove to
    be either true *or* false, typically because more type information
    was needed. (We'll see an example shortly.)
    - This might be the result for trying to prove `Vec<?T>: Clone`.
 - **Var values:** Values for each of the unbound inference variables
  (like `?T`) that appeared in your original query. (Remember that in Prolog,
  we had to infer these.)
  - As we'll see in the example below, we can get back var values even
    for `Ambiguous` cases.
 - **Region constraints:** these are relations that must hold between
  the lifetimes that you supplied as inputs. We'll ignore these here,
  but see the
  [section on handling regions in traits](./regions.html) for
  more details.
 - **Value:** The query result also comes with a value of type `T`. For
  some specialized queries – like normalizing associated types –
  this is used to carry back an extra result, but it's often just
  `()`.
 ### Examples
 Let's work through an example query to see what all the parts mean.
 Consider [the `Borrow` trait][borrow]. This trait has a number of
 impls; among them, there are these two (for clarity, I've written the
 `Sized` bounds explicitly):
 [borrow]: https://doc.rust-lang.org/std/borrow/trait.Borrow.html
 ```rust,ignore
 impl<T> Borrow<T> for T where T: ?Sized
 impl<T> Borrow<[T]> for Vec<T> where T: Sized
 ```
 **Example 1.** Imagine we are type-checking this (rather artificial)
 bit of code:
 ```rust,ignore
 fn foo<A, B>(a: A, vec_b: Option<B>) where A: Borrow<B> { }
 fn main() {
    let mut t: Vec<_> = vec![]; // Type: Vec<?T>
    let mut u: Option<_> = None; // Type: Option<?U>
    foo(t, u); // Example 1: requires `Vec<?T>: Borrow<?U>`
    ...
 }
 ```
 As the comments indicate, we first create two variables `t` and `u`;
 `t` is an empty vector and `u` is a `None` option. Both of these
 variables have unbound inference variables in their type: `?T`
 represents the elements in the vector `t` and `?U` represents the
 value stored in the option `u`.  Next, we invoke `foo`; comparing the
 signature of `foo` to its arguments, we wind up with `A = Vec<?T>` and
 `B = ?U`. Therefore, the where clause on `foo` requires that `Vec<?T>:
 Borrow<?U>`. This is thus our first example trait query.
 There are many possible solutions to the query `Vec<?T>: Borrow<?U>`;
 for example:
 - `?U = Vec<?T>`,
 - `?U = [?T]`,
 - `?T = u32, ?U = [u32]`
 - and so forth.
 Therefore, the result we get back would be as follows (I'm going to
 ignore region constraints and the "value"):
 - Certainty: `Ambiguous` – we're not sure yet if this holds
 - Var values: `[?T = ?T, ?U = ?U]` – we learned nothing about the values of
  the variables
 In short, the query result says that it is too soon to say much about
 whether this trait is proven. During type-checking, this is not an
 immediate error: instead, the type checker would hold on to this
 requirement (`Vec<?T>: Borrow<?U>`) and wait. As we'll see in the next
 example, it may happen that `?T` and `?U` wind up constrained from
 other sources, in which case we can try the trait query again.
 **Example 2.** We can now extend our previous example a bit,
 and assign a value to `u`:
 ```rust,ignore
 fn foo<A, B>(a: A, vec_b: Option<B>) where A: Borrow<B> { }
 fn main() {
    // What we saw before:
    let mut t: Vec<_> = vec![]; // Type: Vec<?T>
    let mut u: Option<_> = None; // Type: Option<?U>
    foo(t, u); // `Vec<?T>: Borrow<?U>` => ambiguous
    // New stuff:
    u = Some(vec![]); // ?U = Vec<?V>
 }
 ```
 As a result of this assignment, the type of `u` is forced to be
 `Option<Vec<?V>>`, where `?V` represents the element type of the
 vector. This in turn implies that `?U` is [unified] to `Vec<?V>`.
 [unified]: ../type-checking.html
 Let's suppose that the type checker decides to revisit the
 "as-yet-unproven" trait obligation we saw before, `Vec<?T>:
 Borrow<?U>`. `?U` is no longer an unbound inference variable; it now
 has a value, `Vec<?V>`. So, if we "refresh" the query with that value, we get:
 ```text
 Vec<?T>: Borrow<Vec<?V>>
 ```
 This time, there is only one impl that applies, the reflexive impl:
 ```text
 impl<T> Borrow<T> for T where T: ?Sized
 ```
 Therefore, the trait checker will answer:
 - Certainty: `Proven`
 - Var values: `[?T = ?T, ?V = ?T]`
 Here, it is saying that we have indeed proven that the obligation
 holds, and we also know that `?T` and `?V` are the same type (but we
 don't know what that type is yet!).
 (In fact, as the function ends here, the type checker would give an
 error at this point, since the element types of `t` and `u` are still
 not yet known, even though they are known to be the same.)
--- a/src/traits/canonicalization.md
+++ b/src/traits/canonicalization.md
@ -1,256 +0,0 @@
 # Canonicalization
 Canonicalization is the process of **isolating** an inference value
 from its context. It is a key part of implementing
 [canonical queries][cq], and you may wish to read the parent chapter
 to get more context.
 Canonicalization is really based on a very simple concept: every
 [inference variable](../type-inference.html#vars) is always in one of
 two states: either it is **unbound**, in which case we don't know yet
 what type it is, or it is **bound**, in which case we do. So to
 isolate some data-structure T that contains types/regions from its
 environment, we just walk down and find the unbound variables that
 appear in T; those variables get replaced with "canonical variables",
 starting from zero and numbered in a fixed order (left to right, for
 the most part, but really it doesn't matter as long as it is
 consistent).
 [cq]: ./canonical-queries.html
 So, for example, if we have the type `X = (?T, ?U)`, where `?T` and
 `?U` are distinct, unbound inference variables, then the canonical
 form of `X` would be `(?0, ?1)`, where `?0` and `?1` represent these
 **canonical placeholders**. Note that the type `Y = (?U, ?T)` also
 canonicalizes to `(?0, ?1)`. But the type `Z = (?T, ?T)` would
 canonicalize to `(?0, ?0)` (as would `(?U, ?U)`). In other words, the
 exact identity of the inference variables is not important – unless
 they are repeated.
 We use this to improve caching as well as to detect cycles and other
 things during trait resolution. Roughly speaking, the idea is that if
 two trait queries have the same canonical form, then they will get
 the same answer. That answer will be expressed in terms of the
 canonical variables (`?0`, `?1`), which we can then map back to the
 original variables (`?T`, `?U`).
 ## Canonicalizing the query
 To see how it works, imagine that we are asking to solve the following
 trait query: `?A: Foo<'static, ?B>`, where `?A` and `?B` are unbound.
 This query contains two unbound variables, but it also contains the
 lifetime `'static`. The trait system generally ignores all lifetimes
 and treats them equally, so when canonicalizing, we will *also*
 replace any [free lifetime](../appendix/background.html#free-vs-bound) with a
 canonical variable (Note that `'static` is actually a _free_ lifetime 
 variable here. We are not considering it in the typing context of the whole 
 program but only in the context of this trait reference. Mathematically, we
 are not quantifying over the whole program, but only this obligation).
 Therefore, we get the following result:
 ```text
 ?0: Foo<'?1, ?2>
 ```
 Sometimes we write this differently, like so:
 ```text
 for<T,L,T> { ?0: Foo<'?1, ?2> }
 ```
 This `for<>` gives some information about each of the canonical
 variables within.  In this case, each `T` indicates a type variable,
 so `?0` and `?2` are types; the `L` indicates a lifetime variable, so
 `?1` is a lifetime. The `canonicalize` method *also* gives back a
 `CanonicalVarValues` array OV with the "original values" for each
 canonicalized variable:
 ```text
 [?A, 'static, ?B]
 ```
 We'll need this vector OV later, when we process the query response.
 ## Executing the query
 Once we've constructed the canonical query, we can try to solve it.
 To do so, we will wind up creating a fresh inference context and
 **instantiating** the canonical query in that context. The idea is that
 we create a substitution S from the canonical form containing a fresh
 inference variable (of suitable kind) for each canonical variable.
 So, for our example query:
 ```text
 for<T,L,T> { ?0: Foo<'?1, ?2> }
 ```
 the substitution S might be:
 ```text
 S = [?A, '?B, ?C]
 ```
 We can then replace the bound canonical variables (`?0`, etc) with
 these inference variables, yielding the following fully instantiated
 query:
 ```text
 ?A: Foo<'?B, ?C>
 ```
 Remember that substitution S though! We're going to need it later.
 OK, now that we have a fresh inference context and an instantiated
 query, we can go ahead and try to solve it. The trait solver itself is
 explained in more detail in [another section](./slg.html), but
 suffice to say that it will compute a [certainty value][cqqr] (`Proven` or
 `Ambiguous`) and have side-effects on the inference variables we've
 created. For example, if there were only one impl of `Foo`, like so:
 [cqqr]: ./canonical-queries.html#query-response
 ```rust,ignore
 impl<'a, X> Foo<'a, X> for Vec<X>
 where X: 'a
 { ... }
 ```
 then we might wind up with a certainty value of `Proven`, as well as
 creating fresh inference variables `'?D` and `?E` (to represent the
 parameters on the impl) and unifying as follows:
 - `'?B = '?D`
 - `?A = Vec<?E>`
 - `?C = ?E`
 We would also accumulate the region constraint `?E: '?D`, due to the
 where clause.
 In order to create our final query result, we have to "lift" these
 values out of the query's inference context and into something that
 can be reapplied in our original inference context. We do that by
 **re-applying canonicalization**, but to the **query result**.
 ## Canonicalizing the query result
 As discussed in [the parent section][cqqr], most trait queries wind up
 with a result that brings together a "certainty value" `certainty`, a
 result substitution `var_values`, and some region constraints. To
 create this, we wind up re-using the substitution S that we created
 when first instantiating our query. To refresh your memory, we had a query
 ```text
 for<T,L,T> { ?0: Foo<'?1, ?2> }
 ```
 for which we made a substutition S:
 ```text
 S = [?A, '?B, ?C]
 ```
 We then did some work which unified some of those variables with other things.
 If we "refresh" S with the latest results, we get:
 ```text
 S = [Vec<?E>, '?D, ?E]
 ```
 These are precisely the new values for the three input variables from
 our original query. Note though that they include some new variables
 (like `?E`). We can make those go away by canonicalizing again! We don't
 just canonicalize S, though, we canonicalize the whole query response QR:
 ```text
 QR = {
    certainty: Proven,             // or whatever
    var_values: [Vec<?E>, '?D, ?E] // this is S
    region_constraints: [?E: '?D], // from the impl
    value: (),                     // for our purposes, just (), but
                                   // in some cases this might have
                                   // a type or other info
 }
 ```
 The result would be as follows:
 ```text
 Canonical(QR) = for<T, L> {
    certainty: Proven,
    var_values: [Vec<?0>, '?1, ?0]
    region_constraints: [?0: '?1],
    value: (),
 }
 ```
 (One subtle point: when we canonicalize the query **result**, we do not
 use any special treatment for free lifetimes. Note that both
 references to `'?D`, for example, were converted into the same
 canonical variable (`?1`). This is in contrast to the original query,
 where we canonicalized every free lifetime into a fresh canonical
 variable.)
 Now, this result must be reapplied in each context where needed.
 ## Processing the canonicalized query result
 In the previous section we produced a canonical query result. We now have
 to apply that result in our original context. If you recall, way back in the
 beginning, we were trying to prove this query:
 ```text
 ?A: Foo<'static, ?B>
 ```
 We canonicalized that into this:
 ```text
 for<T,L,T> { ?0: Foo<'?1, ?2> }
 ```
 and now we got back a canonical response:
 ```text
 for<T, L> {
    certainty: Proven,
    var_values: [Vec<?0>, '?1, ?0]
    region_constraints: [?0: '?1],
    value: (),
 }
 ```
 We now want to apply that response to our context. Conceptually, how
 we do that is to (a) instantiate each of the canonical variables in
 the result with a fresh inference variable, (b) unify the values in
 the result with the original values, and then (c) record the region
 constraints for later. Doing step (a) would yield a result of
 ```text
 {
      certainty: Proven,
      var_values: [Vec<?C>, '?D, ?C]
                       ^^   ^^^ fresh inference variables
      region_constraints: [?C: '?D],
      value: (),
 }
 ```
 Step (b) would then unify:
 ```text
 ?A with Vec<?C>
 'static with '?D
 ?B with ?C
 ```
 And finally the region constraint of `?C: 'static` would be recorded
 for later verification.
 (What we *actually* do is a mildly optimized variant of that: Rather
 than eagerly instantiating all of the canonical values in the result
 with variables, we instead walk the vector of values, looking for
 cases where the value is just a canonical variable. In our example,
 `values[2]` is `?C`, so that means we can deduce that `?C := ?B` and
 `'?D := 'static`. This gives us a partial set of values. Anything for
 which we do not find a value, we create an inference variable.)
--- a/src/traits/chalk-overview.md
+++ b/src/traits/chalk-overview.md
@ -1,256 +0,0 @@
 # An Overview of Chalk
 > Chalk is under heavy development, so if any of these links are broken or if
 > any of the information is inconsistent with the code or outdated, please
 > [open an issue][rustc-issues] so we can fix it. If you are able to fix the
 > issue yourself, we would love your contribution!
 [Chalk][chalk] recasts Rust's trait system explicitly in terms of logic
 programming by "lowering" Rust code into a kind of logic program we can then
 execute queries against (see [*Lowering to Logic*][lowering-to-logic] and
 [*Lowering Rules*][lowering-rules]). Its goal is to be an executable, highly
 readable specification of the Rust trait system.
 There are many expected benefits from this work. It will consolidate our
 existing, somewhat ad-hoc implementation into something far more principled and
 expressive, which should behave better in corner cases, and be much easier to
 extend.
 ## Chalk Structure
 Chalk has two main "products". The first of these is the
 [`chalk_engine`][chalk_engine] crate, which defines the core [SLG
 solver][slg]. This is the part rustc uses.
 The rest of chalk can be considered an elaborate testing harness. Chalk is
 capable of parsing Rust-like "programs", lowering them to logic, and
 performing queries on them.
 Here's a sample session in the chalk repl, chalki. After feeding it our
 program, we perform some queries on it.
 ```rust,ignore
 ?- program
 Enter a program; press Ctrl-D when finished
 | struct Foo { }
 | struct Bar { }
 | struct Vec<T> { }
 | trait Clone { }
 | impl<T> Clone for Vec<T> where T: Clone { }
 | impl Clone for Foo { }
 ?- Vec<Foo>: Clone
 Unique; substitution [], lifetime constraints []
 ?- Vec<Bar>: Clone
 No possible solution.
 ?- exists<T> { Vec<T>: Clone }
 Ambiguous; no inference guidance
 ```
 You can see more examples of programs and queries in the [unit
 tests][chalk-test-example].
 Next we'll go through each stage required to produce the output above.
 ### Parsing ([chalk_parse])
 Chalk is designed to be incorporated with the Rust compiler, so the syntax and
 concepts it deals with heavily borrow from Rust. It is convenient for the sake
 of testing to be able to run chalk on its own, so chalk includes a parser for a
 Rust-like syntax. This syntax is orthogonal to the Rust AST and grammar. It is
 not intended to look exactly like it or support the exact same syntax.
 The parser takes that syntax and produces an [Abstract Syntax Tree (AST)][ast].
 You can find the [complete definition of the AST][chalk-ast] in the source code.
 The syntax contains things from Rust that we know and love, for example: traits,
 impls, and struct definitions. Parsing is often the first "phase" of
 transformation that a program goes through in order to become a format that
 chalk can understand.
 ### Rust Intermediate Representation ([chalk_rust_ir])
 After getting the AST we convert it to a more convenient intermediate
 representation called [`chalk_rust_ir`][chalk_rust_ir]. This is sort of
 analogous to the [HIR] in Rust. The process of converting to IR is called
 *lowering*.
 The [`chalk::program::Program`][chalk-program] struct contains some "rust things"
 but indexed and accessible in a different way. For example, if you have a
 type like `Foo<Bar>`, we would represent `Foo` as a string in the AST but in
 `chalk::program::Program`, we use numeric indices (`ItemId`).
 The [IR source code][ir-code] contains the complete definition.
 ### Chalk Intermediate Representation ([chalk_ir])
 Once we have Rust IR it is time to convert it to "program clauses". A
 [`ProgramClause`] is essentially one of the following:
 * A [clause] of the form `consequence :- conditions` where `:-` is read as
  "if" and `conditions = cond1 && cond2 && ...`
 * A universally quantified clause of the form
  `forall<T> { consequence :- conditions }`
  * `forall<T> { ... }` is used to represent [universal quantification]. See the
    section on [Lowering to logic][lowering-forall] for more information.
  * A key thing to note about `forall` is that we don't allow you to "quantify"
    over traits, only types and regions (lifetimes). That is, you can't make a
    rule like `forall<Trait> { u32: Trait }` which would say "`u32` implements
    all traits". You can however say `forall<T> { T: Trait }` meaning "`Trait`
    is implemented by all types".
  * `forall<T> { ... }` is represented in the code using the [`Binders<T>`
    struct][binders-struct].
 *See also: [Goals and Clauses][goals-and-clauses]*
 This is where we encode the rules of the trait system into logic. For
 example, if we have the following Rust:
 ```rust,ignore
 impl<T: Clone> Clone for Vec<T> {}
 ```
 We generate the following program clause:
 ```rust,ignore
 forall<T> { (Vec<T>: Clone) :- (T: Clone) }
 ```
 This rule dictates that `Vec<T>: Clone` is only satisfied if `T: Clone` is also
 satisfied (i.e. "provable").
 Similar to [`chalk::program::Program`][chalk-program] which has "rust-like
 things", chalk_ir defines [`ProgramEnvironment`] which is "pure logic".
 The main field in that struct is `program_clauses`, which contains the
 [`ProgramClause`]s generated by the rules module.
 ### Rules ([chalk_solve])
 The `chalk_solve` crate ([source code][chalk_solve]) defines the logic rules we
 use for each item in the Rust IR. It works by iterating over every trait, impl,
 etc. and emitting the rules that come from each one.
 *See also: [Lowering Rules][lowering-rules]*
 #### Well-formedness checks
 As part of lowering to logic, we also do some "well formedness" checks. See
 the [`chalk_solve::wf` source code][solve-wf-src] for where those are done.
 *See also: [Well-formedness checking][wf-checking]*
 #### Coherence
 The method `CoherenceSolver::specialization_priorities` in the `coherence` module
 ([source code][coherence-src]) checks "coherence", which means that it
 ensures that two impls of the same trait for the same type cannot exist.
 ### Solver ([chalk_solve])
 Finally, when we've collected all the program clauses we care about, we want
 to perform queries on it. The component that finds the answer to these
 queries is called the *solver*.
 *See also: [The SLG Solver][slg]*
 ## Crates
 Chalk's functionality is broken up into the following crates:
 - [**chalk_engine**][chalk_engine]: Defines the core [SLG solver][slg].
 - [**chalk_rust_ir**][chalk_rust_ir], containing the "HIR-like" form of the AST
 - [**chalk_ir**][chalk_ir]: Defines chalk's internal representation of
  types, lifetimes, and goals.
 - [**chalk_solve**][chalk_solve]: Combines `chalk_ir` and `chalk_engine`,
  effectively, which implements logic rules converting `chalk_rust_ir` to
  `chalk_ir`
  - Defines the `coherence` module, which implements coherence rules
  - [`chalk_engine::context`][engine-context] provides the necessary hooks.
 - [**chalk_parse**][chalk_parse]: Defines the raw AST and a parser.
 - [**chalk**][doc-chalk]: Brings everything together. Defines the following
  modules:
  - `chalk::lowering`, which converts AST to `chalk_rust_ir`
  - Also includes [chalki][chalki], chalk's REPL.
 [Browse source code on GitHub](https://github.com/rust-lang/chalk)
 ## Testing
 chalk has a test framework for lowering programs to logic, checking the
 lowered logic, and performing queries on it. This is how we test the
 implementation of chalk itself, and the viability of the [lowering
 rules][lowering-rules].
 The main kind of tests in chalk are **goal tests**. They contain a program,
 which is expected to lower to logic successfully, and a set of queries
 (goals) along with the expected output. Here's an
 [example][chalk-test-example]. Since chalk's output can be quite long, goal
 tests support specifying only a prefix of the output.
 **Lowering tests** check the stages that occur before we can issue queries
 to the solver: the [lowering to chalk_rust_ir][chalk-test-lowering], and the
 [well-formedness checks][chalk-test-wf] that occur after that.
 ### Testing internals
 Goal tests use a [`test!` macro][test-macro] that takes chalk's Rust-like
 syntax and runs it through the full pipeline described above. The macro
 ultimately calls the [`solve_goal` function][solve_goal].
 Likewise, lowering tests use the [`lowering_success!` and
 `lowering_error!` macros][test-lowering-macros].
 ## More Resources
 * [Chalk Source Code](https://github.com/rust-lang/chalk)
 * [Chalk Glossary](https://github.com/rust-lang/chalk/blob/master/GLOSSARY.md)
 ### Blog Posts
 * [Lowering Rust traits to logic](http://smallcultfollowing.com/babysteps/blog/2017/01/26/lowering-rust-traits-to-logic/)
 * [Unification in Chalk, part 1](http://smallcultfollowing.com/babysteps/blog/2017/03/25/unification-in-chalk-part-1/)
 * [Unification in Chalk, part 2](http://smallcultfollowing.com/babysteps/blog/2017/04/23/unification-in-chalk-part-2/)
 * [Negative reasoning in Chalk](https://aturon.github.io/blog/2017/04/24/negative-chalk/)
 * [Query structure in chalk](http://smallcultfollowing.com/babysteps/blog/2017/05/25/query-structure-in-chalk/)
 * [Cyclic queries in chalk](http://smallcultfollowing.com/babysteps/blog/2017/09/12/tabling-handling-cyclic-queries-in-chalk/)
 * [An on-demand SLG solver for chalk](http://smallcultfollowing.com/babysteps/blog/2018/01/31/an-on-demand-slg-solver-for-chalk/)
 [goals-and-clauses]: ./goals-and-clauses.html
 [HIR]: ../hir.html
 [lowering-forall]: ./lowering-to-logic.html#type-checking-generic-functions-beyond-horn-clauses
 [lowering-rules]: ./lowering-rules.html
 [lowering-to-logic]: ./lowering-to-logic.html
 [slg]: ./slg.html
 [wf-checking]: ./wf.html
 [ast]: https://en.wikipedia.org/wiki/Abstract_syntax_tree
 [chalk]: https://github.com/rust-lang/chalk
 [rustc-issues]: https://github.com/rust-lang/rustc-dev-guide/issues
 [universal quantification]: https://en.wikipedia.org/wiki/Universal_quantification
 [`ProgramClause`]: https://rust-lang.github.io/chalk/chalk_ir/struct.ProgramClause.html
 [`ProgramEnvironment`]: https://rust-lang.github.io/chalk/chalk_integration/program_environment/struct.ProgramEnvironment.html
 [chalk_engine]: https://rust-lang.github.io/chalk/chalk_engine
 [chalk_ir]: https://rust-lang.github.io/chalk/chalk_ir/index.html
 [chalk_parse]: https://rust-lang.github.io/chalk/chalk_parse/index.html
 [chalk_solve]: https://rust-lang.github.io/chalk/chalk_solve/index.html
 [chalk_rust_ir]: https://rust-lang.github.io/chalk/chalk_rust_ir/index.html
 [doc-chalk]: https://rust-lang.github.io/chalk/chalk/index.html
 [engine-context]: https://rust-lang.github.io/chalk/chalk_engine/context/index.html
 [chalk-program]: https://rust-lang.github.io/chalk/chalk_integration/program/struct.Program.html
 [binders-struct]: https://rust-lang.github.io/chalk/chalk_ir/struct.Binders.html
 [chalk-ast]: https://rust-lang.github.io/chalk/chalk_parse/ast/index.html
 [chalk-test-example]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L115
 [chalk-test-lowering-example]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rust_ir/lowering/test.rs#L8-L31
 [chalk-test-lowering]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rust_ir/lowering/test.rs
 [chalk-test-wf]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules/wf/test.rs#L1
 [chalki]: https://github.com/rust-lang/chalk/blob/master/src/main.rs
 [clause]: https://github.com/rust-lang/chalk/blob/master/GLOSSARY.md#clause
 [coherence-src]: https://rust-lang.github.io/chalk/chalk_solve/coherence/index.html
 [ir-code]: https://rust-lang.github.io/chalk/chalk_rust_ir/
 [solve-wf-src]: https://rust-lang.github.io/chalk/chalk_solve/wf/index.html
 [solve_goal]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L85
 [test-lowering-macros]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test_util.rs#L21-L54
 [test-macro]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L33
--- a/src/traits/chalk.md
+++ b/src/traits/chalk.md
@ -0,0 +1,43 @@
 # Chalk-based trait solving (new-style)
 > 🚧 This chapter describes "new-style" trait solving. This is still in the
 > [process of being implemented][wg]; this chapter serves as a kind of
 > in-progress design document. If you would prefer to read about how the
 > current trait solver works, check out
 > [this other subchapter](./resolution.html). 🚧
 >
 > By the way, if you would like to help in hacking on the new solver, you will
 > find instructions for getting involved in the
 > [Traits Working Group tracking issue][wg]!
 [wg]: https://github.com/rust-lang/rust/issues/48416
 The new-style trait solver is based on the work done in [chalk][chalk]. Chalk
 recasts Rust's trait system explicitly in terms of logic programming. It does
 this by "lowering" Rust code into a kind of logic program we can then execute
 queries against.
 The key observation here is that the Rust trait system is basically a
 kind of logic, and it can be mapped onto standard logical inference
 rules. We can then look for solutions to those inference rules in a
 very similar fashion to how e.g. a [Prolog] solver works. It turns out
 that we can't *quite* use Prolog rules (also called Horn clauses) but
 rather need a somewhat more expressive variant.
 [Prolog]: https://en.wikipedia.org/wiki/Prolog
 You can read more about chalk itself in the
 [Chalk book](https://rust-lang.github.io/chalk/book/) section.
 ## Ongoing work
 The design of the new-style trait solving currently happens in two places:
 **chalk**. The [chalk][chalk] repository is where we experiment with new ideas
 and designs for the trait system.
 **rustc**. Once we are happy with the logical rules, we proceed to
 implementing them in rustc. This mainly happens in
 [`librustc_traits`][librustc_traits]. We map our struct, trait, and impl declarations into logical inference rules in the [lowering module in rustc](./lowering-module.md).
 [chalk]: https://github.com/rust-lang/chalk
 [librustc_traits]: https://github.com/rust-lang/rust/tree/master/src/librustc_traits
--- a/src/traits/goals-and-clauses.md
+++ b/src/traits/goals-and-clauses.md
@ -1,270 +0,0 @@
 # Goals and clauses
 In logic programming terms, a **goal** is something that you must
 prove and a **clause** is something that you know is true. As
 described in the [lowering to logic](./lowering-to-logic.html)
 chapter, Rust's trait solver is based on an extension of hereditary
 harrop (HH) clauses, which extend traditional Prolog Horn clauses with
 a few new superpowers.
 ## Goals and clauses meta structure
 In Rust's solver, **goals** and **clauses** have the following forms
 (note that the two definitions reference one another):
 ```text
 Goal = DomainGoal           // defined in the section below
        | Goal && Goal
        | Goal || Goal
        | exists<K> { Goal }   // existential quantification
        | forall<K> { Goal }   // universal quantification
        | if (Clause) { Goal } // implication
        | true                 // something that's trivially true
        | ambiguous            // something that's never provable
 Clause = DomainGoal
        | Clause :- Goal     // if can prove Goal, then Clause is true
        | Clause && Clause
        | forall<K> { Clause }
 K = <type>     // a "kind"
    | <lifetime>
 ```
 The proof procedure for these sorts of goals is actually quite
 straightforward.  Essentially, it's a form of depth-first search. The
 paper
 ["A Proof Procedure for the Logic of Hereditary Harrop Formulas"][pphhf]
 gives the details.
 In terms of code, these types are defined in
 [`librustc_middle/traits/mod.rs`][traits_mod] in rustc, and in
 [`chalk-ir/src/lib.rs`][chalk_ir] in chalk.
 [pphhf]: ./bibliography.html#pphhf
 [traits_mod]: https://github.com/rust-lang/rust/blob/master/src/librustc_middle/traits/mod.rs
 [chalk_ir]: https://github.com/rust-lang/chalk/blob/master/chalk-ir/src/lib.rs
 <a name="domain-goals"></a>
 ## Domain goals
 *Domain goals* are the atoms of the trait logic. As can be seen in the
 definitions given above, general goals basically consist in a combination of
 domain goals.
 Moreover, flattening a bit the definition of clauses given previously, one can
 see that clauses are always of the form:
 ```text
 forall<K1, ..., Kn> { DomainGoal :- Goal }
 ```
 hence domain goals are in fact clauses' LHS. That is, at the most granular level,
 domain goals are what the trait solver will end up trying to prove.
 <a name="trait-ref"></a>
 To define the set of domain goals in our system, we need to first
 introduce a few simple formulations. A **trait reference** consists of
 the name of a trait along with a suitable set of inputs P0..Pn:
 ```text
 TraitRef = P0: TraitName<P1..Pn>
 ```
 So, for example, `u32: Display` is a trait reference, as is `Vec<T>:
 IntoIterator`. Note that Rust surface syntax also permits some extra
 things, like associated type bindings (`Vec<T>: IntoIterator<Item =
 T>`), that are not part of a trait reference.
 <a name="projection"></a>
 A **projection** consists of an associated item reference along with
 its inputs P0..Pm:
 ```text
 Projection = <P0 as TraitName<P1..Pn>>::AssocItem<Pn+1..Pm>
 ```
 Given these, we can define a `DomainGoal` as follows:
 ```text
 DomainGoal = Holds(WhereClause)
            | FromEnv(TraitRef)
            | FromEnv(Type)
            | WellFormed(TraitRef)
            | WellFormed(Type)
            | Normalize(Projection -> Type)
 WhereClause = Implemented(TraitRef)
            | ProjectionEq(Projection = Type)
            | Outlives(Type: Region)
            | Outlives(Region: Region)
 ```
 `WhereClause` refers to a `where` clause that a Rust user would actually be able
 to write in a Rust program. This abstraction exists only as a convenience as we
 sometimes want to only deal with domain goals that are effectively writable in
 Rust.
 Let's break down each one of these, one-by-one.
 #### Implemented(TraitRef)
 e.g. `Implemented(i32: Copy)`
 True if the given trait is implemented for the given input types and lifetimes.
 #### ProjectionEq(Projection = Type)
 e.g. `ProjectionEq<T as Iterator>::Item = u8`
 The given associated type `Projection` is equal to `Type`; this can be proved
 with either normalization or using placeholder associated types. See
 [the section on associated types](./associated-types.html).
 #### Normalize(Projection -> Type)
 e.g. `ProjectionEq<T as Iterator>::Item -> u8`
 The given associated type `Projection` can be [normalized][n] to `Type`.
 As discussed in [the section on associated
 types](./associated-types.html), `Normalize` implies `ProjectionEq`,
 but not vice versa. In general, proving `Normalize(<T as Trait>::Item -> U)`
 also requires proving `Implemented(T: Trait)`.
 [n]: ./associated-types.html#normalize
 [at]: ./associated-types.html
 #### FromEnv(TraitRef)
 e.g. `FromEnv(Self: Add<i32>)`
 True if the inner `TraitRef` is *assumed* to be true,
 that is, if it can be derived from the in-scope where clauses.
 For example, given the following function:
 ```rust
 fn loud_clone<T: Clone>(stuff: &T) -> T {
    println!("cloning!");
    stuff.clone()
 }
 ```
 Inside the body of our function, we would have `FromEnv(T: Clone)`. In-scope
 where clauses nest, so a function body inside an impl body inherits the
 impl body's where clauses, too.
 This and the next rule are used to implement [implied bounds]. As we'll see
 in the section on lowering, `FromEnv(TraitRef)` implies `Implemented(TraitRef)`,
 but not vice versa. This distinction is crucial to implied bounds.
 #### FromEnv(Type)
 e.g. `FromEnv(HashSet<K>)`
 True if the inner `Type` is *assumed* to be well-formed, that is, if it is an
 input type of a function or an impl.
 For example, given the following code:
 ```rust,ignore
 struct HashSet<K> where K: Hash { ... }
 fn loud_insert<K>(set: &mut HashSet<K>, item: K) {
    println!("inserting!");
    set.insert(item);
 }
 ```
 `HashSet<K>` is an input type of the `loud_insert` function. Hence, we assume it
 to be well-formed, so we would have `FromEnv(HashSet<K>)` inside the body of our
 function. As we'll see in the section on lowering, `FromEnv(HashSet<K>)` implies
 `Implemented(K: Hash)` because the
 `HashSet` declaration was written with a `K: Hash` where clause. Hence, we don't
 need to repeat that bound on the `loud_insert` function: we rather automatically
 assume that it is true.
 #### WellFormed(Item)
 These goals imply that the given item is *well-formed*.
 We can talk about different types of items being well-formed:
 * *Types*, like `WellFormed(Vec<i32>)`, which is true in Rust, or
  `WellFormed(Vec<str>)`, which is not (because `str` is not `Sized`.)
 * *TraitRefs*, like `WellFormed(Vec<i32>: Clone)`.
 Well-formedness is important to [implied bounds]. In particular, the reason
 it is okay to assume `FromEnv(T: Clone)` in the `loud_clone` example is that we
 _also_ verify `WellFormed(T: Clone)` for each call site of `loud_clone`.
 Similarly, it is okay to assume `FromEnv(HashSet<K>)` in the `loud_insert`
 example because we will verify `WellFormed(HashSet<K>)` for each call site of
 `loud_insert`. 
 #### Outlives(Type: Region), Outlives(Region: Region)
 e.g. `Outlives(&'a str: 'b)`, `Outlives('a: 'static)`
 True if the given type or region on the left outlives the right-hand region.
 <a name="coinductive"></a>
 ## Coinductive goals
 Most goals in our system are "inductive". In an inductive goal,
 circular reasoning is disallowed. Consider this example clause:
 ```text
    Implemented(Foo: Bar) :-
        Implemented(Foo: Bar).
 ```
 Considered inductively, this clause is useless: if we are trying to
 prove `Implemented(Foo: Bar)`, we would then recursively have to prove
 `Implemented(Foo: Bar)`, and that cycle would continue ad infinitum
 (the trait solver will terminate here, it would just consider that
 `Implemented(Foo: Bar)` is not known to be true).
 However, some goals are *co-inductive*. Simply put, this means that
 cycles are OK. So, if `Bar` were a co-inductive trait, then the rule
 above would be perfectly valid, and it would indicate that
 `Implemented(Foo: Bar)` is true.
 *Auto traits* are one example in Rust where co-inductive goals are used.
 Consider the `Send` trait, and imagine that we have this struct:
 ```rust
 struct Foo {
    next: Option<Box<Foo>>
 }
 ```
 The default rules for auto traits say that `Foo` is `Send` if the
 types of its fields are `Send`. Therefore, we would have a rule like
 ```text
 Implemented(Foo: Send) :-
    Implemented(Option<Box<Foo>>: Send).
 ```
 As you can probably imagine, proving that `Option<Box<Foo>>: Send` is
 going to wind up circularly requiring us to prove that `Foo: Send`
 again. So this would be an example where we wind up in a cycle – but
 that's ok, we *do* consider `Foo: Send` to hold, even though it
 references itself.
 In general, co-inductive traits are used in Rust trait solving when we
 want to enumerate a fixed set of possibilities. In the case of auto
 traits, we are enumerating the set of reachable types from a given
 starting point (i.e., `Foo` can reach values of type
 `Option<Box<Foo>>`, which implies it can reach values of type
 `Box<Foo>`, and then of type `Foo`, and then the cycle is complete).
 In addition to auto traits, `WellFormed` predicates are co-inductive.
 These are used to achieve a similar "enumerate all the cases" pattern,
 as described in the section on [implied bounds].
 [implied bounds]: ./lowering-rules.html#implied-bounds
 ## Incomplete chapter
 Some topics yet to be written:
 - Elaborate on the proof procedure
 - SLG solving – introduce negative reasoning
--- a/src/traits/implied-bounds.md
+++ b/src/traits/implied-bounds.md
@ -1,502 +0,0 @@
 # Implied Bounds
 Implied bounds remove the need to repeat where clauses written on
 a type declaration or a trait declaration. For example, say we have the
 following type declaration:
 ```rust,ignore
 struct HashSet<K: Hash> {
    ...
 }
 ```
 then everywhere we use `HashSet<K>` as an "input" type, that is appearing in
 the receiver type of an `impl` or in the arguments of a function, we don't
 want to have to repeat the `where K: Hash` bound, as in:
 ```rust,ignore
 // I don't want to have to repeat `where K: Hash` here.
 impl<K> HashSet<K> {
    ...
 }
 // Same here.
 fn loud_insert<K>(set: &mut HashSet<K>, item: K) {
    println!("inserting!");
    set.insert(item);
 }
 ```
 Note that in the `loud_insert` example, `HashSet<K>` is not the type
 of the `set` argument of `loud_insert`, it only *appears* in the
 argument type `&mut HashSet<K>`: we care about every type appearing
 in the function's header (the header is the signature without the return type),
 not only types of the function's arguments.
 The rationale for applying implied bounds to input types is that, for example,
 in order to call the `loud_insert` function above, the programmer must have
 *produced* the type `HashSet<K>` already, hence the compiler already verified
 that `HashSet<K>` was well-formed, i.e. that `K` effectively implemented
 `Hash`, as in the following example:
 ```rust,ignore
 fn main() {
    // I am producing a value of type `HashSet<i32>`.
    // If `i32` was not `Hash`, the compiler would report an error here.
    let set: HashSet<i32> = HashSet::new();
    loud_insert(&mut set, 5);
 }
 ```
 Hence, we don't want to repeat where clauses for input types because that would
 sort of duplicate the work of the programmer, having to verify that their types
 are well-formed both when calling the function and when using them in the
 arguments of their function. The same reasoning applies when using an `impl`.
 Similarly, given the following trait declaration:
 ```rust,ignore
 trait Copy where Self: Clone { // desugared version of `Copy: Clone`
    ...
 }
 ```
 then everywhere we bound over `SomeType: Copy`, we would like to be able to
 use the fact that `SomeType: Clone` without having to write it explicitly,
 as in:
 ```rust,ignore
 fn loud_clone<T: Clone>(x: T) {
    println!("cloning!");
    x.clone();
 }
 fn fun_with_copy<T: Copy>(x: T) {
    println!("will clone a `Copy` type soon...");
    // I'm using `loud_clone<T: Clone>` with `T: Copy`, I know this
    // implies `T: Clone` so I don't want to have to write it explicitly.
    loud_clone(x);
 }
 ```
 The rationale for implied bounds for traits is that if a type implements
 `Copy`, that is, if there exists an `impl Copy` for that type, there *ought*
 to exist an `impl Clone` for that type, otherwise the compiler would have
 reported an error in the first place. So again, if we were forced to repeat the
 additional `where SomeType: Clone` everywhere whereas we already know that
 `SomeType: Copy` hold, we would kind of duplicate the verification work.
 Implied bounds are not yet completely enforced in rustc, at the moment it only
 works for outlive requirements, super trait bounds, and bounds on associated
 types. The full RFC can be found [here][RFC]. We'll give here a brief view
 of how implied bounds work and why we chose to implement it that way. The
 complete set of lowering rules can be found in the corresponding
 [chapter](./lowering-rules.md).
 [RFC]: https://github.com/rust-lang/rfcs/blob/master/text/2089-implied-bounds.md
 ## Implied bounds and lowering rules
 Now we need to express implied bounds in terms of logical rules. We will start
 with exposing a naive way to do it. Suppose that we have the following traits:
 ```rust,ignore
 trait Foo {
    ...
 }
 trait Bar where Self: Foo { } {
    ...
 }
 ```
 So we would like to say that if a type implements `Bar`, then necessarily
 it must also implement `Foo`. We might think that a clause like this would
 work:
 ```text
 forall<Type> {
    Implemented(Type: Foo) :- Implemented(Type: Bar).
 }
 ```
 Now suppose that we just write this impl:
 ```rust,ignore
 struct X;
 impl Bar for X { }
 ```
 Clearly this should not be allowed: indeed, we wrote a `Bar` impl for `X`, but
 the `Bar` trait requires that we also implement `Foo` for `X`, which we never
 did. In terms of what the compiler does, this would look like this:
 ```rust,ignore
 struct X;
 impl Bar for X {
    // We are in a `Bar` impl for the type `X`.
    // There is a `where Self: Foo` bound on the `Bar` trait declaration.
    // Hence I need to prove that `X` also implements `Foo` for that impl
    // to be legal.
 }
 ```
 So the compiler would try to prove `Implemented(X: Foo)`. Of course it will
 not find any `impl Foo for X` since we did not write any. However, it
 will see our implied bound clause:
 ```text
 forall<Type> {
    Implemented(Type: Foo) :- Implemented(Type: Bar).
 }
 ```
 so that it may be able to prove `Implemented(X: Foo)` if `Implemented(X: Bar)`
 holds. And it turns out that `Implemented(X: Bar)` does hold since we wrote
 a `Bar` impl for `X`! Hence the compiler will accept the `Bar` impl while it
 should not.
 ## Implied bounds coming from the environment
 So the naive approach does not work. What we need to do is to somehow decouple
 implied bounds from impls. Suppose we know that a type `SomeType<...>`
 implements `Bar` and we want to deduce that `SomeType<...>` must also implement
 `Foo`.
 There are two possibilities: first, we have enough information about
 `SomeType<...>` to see that there exists a `Bar` impl in the program which
 covers `SomeType<...>`, for example a plain `impl<...> Bar for SomeType<...>`.
 Then if the compiler has done its job correctly, there *must* exist a `Foo`
 impl which covers `SomeType<...>`, e.g. another plain
 `impl<...> Foo for SomeType<...>`. In that case then, we can just use this
 impl and we do not need implied bounds at all.
 Second possibility: we do not know enough about `SomeType<...>` in order to
 find a `Bar` impl which covers it, for example if `SomeType<...>` is just
 a type parameter in a function:
 ```rust,ignore
 fn foo<T: Bar>() {
    // We'd like to deduce `Implemented(T: Foo)`.
 }
 ```
 That is, the information that `T` implements `Bar` here comes from the
 *environment*. The environment is the set of things that we assume to be true
 when we type check some Rust declaration. In that case, what we assume is that
 `T: Bar`. Then at that point, we might authorize ourselves to have some kind
 of  "local" implied bound reasoning which would say
 `Implemented(T: Foo) :- Implemented(T: Bar)`. This reasoning would
 only be done within our `foo` function in order to avoid the earlier
 problem where we had a global clause.
 We can apply these local reasonings everywhere we can have an environment
 -- i.e. when we can write where clauses -- that is, inside impls,
 trait declarations, and type declarations.
 ## Computing implied bounds with `FromEnv`
 The previous subsection showed that it was only useful to compute implied
 bounds for facts coming from the environment.
 We talked about "local" rules, but there are multiple possible strategies to
 indeed implement the locality of implied bounds.
 In rustc, the current strategy is to *elaborate* bounds: that is, each time
 we have a fact in the environment, we recursively derive all the other things
 that are implied by this fact until we reach a fixed point. For example, if
 we have the following declarations:
 ```rust,ignore
 trait A { }
 trait B where Self: A { }
 trait C where Self: B { }
 fn foo<T: C>() {
    ...
 }
 ```
 then inside the `foo` function, we start with an environment containing only
 `Implemented(T: C)`. Then because of implied bounds for the `C` trait, we
 elaborate `Implemented(T: B)` and add it to our environment. Because of
 implied bounds for the `B` trait, we elaborate `Implemented(T: A)`and add it
 to our environment as well. We cannot elaborate anything else, so we conclude
 that our final environment consists of `Implemented(T: A + B + C)`.
 In the new-style trait system, we like to encode as many things as possible
 with logical rules. So rather than "elaborating", we have a set of *global*
 program clauses defined like so:
 ```text
 forall<T> { Implemented(T: A) :- FromEnv(T: A). }
 forall<T> { Implemented(T: B) :- FromEnv(T: B). }
 forall<T> { FromEnv(T: A) :- FromEnv(T: B). }
 forall<T> { Implemented(T: C) :- FromEnv(T: C). }
 forall<T> { FromEnv(T: C) :- FromEnv(T: C). }
 ```
 So these clauses are defined globally (that is, they are available from
 everywhere in the program) but they cannot be used because the hypothesis
 is always of the form `FromEnv(...)` which is a bit special. Indeed, as
 indicated by the name, `FromEnv(...)` facts can **only** come from the
 environment.
 How it works is that in the `foo` function, instead of having an environment
 containing `Implemented(T: C)`, we replace this environment with
 `FromEnv(T: C)`. From here and thanks to the above clauses, we see that we
 are able to reach any of `Implemented(T: A)`, `Implemented(T: B)` or
 `Implemented(T: C)`, which is what we wanted.
 ## Implied bounds and well-formedness checking
 Implied bounds are tightly related with well-formedness checking.
 Well-formedness checking is the process of checking that the impls the
 programmer wrote are legal, what we referred to earlier as "the compiler doing
 its job correctly".
 We already saw examples of illegal and legal impls:
 ```rust,ignore
 trait Foo { }
 trait Bar where Self: Foo { }
 struct X;
 struct Y;
 impl Bar for X {
    // This impl is not legal: the `Bar` trait requires that we also
    // implement `Foo`, and we didn't.
 }
 impl Foo for Y {
    // This impl is legal: there is nothing to check as there are no where
    // clauses on the `Foo` trait.
 }
 impl Bar for Y {
    // This impl is legal: we have a `Foo` impl for `Y`.
 }
 ```
 We must define what "legal" and "illegal" mean. For this, we introduce another
 predicate: `WellFormed(Type: Trait)`. We say that the trait reference
 `Type: Trait` is well-formed if `Type` meets the bounds written on the
 `Trait` declaration. For each impl we write, assuming that the where clauses
 declared on the impl hold, the compiler tries to prove that the corresponding
 trait reference is well-formed. The impl is legal if the compiler manages to do
 so.
 Coming to the definition of `WellFormed(Type: Trait)`, it would be tempting
 to define it as:
 ```rust,ignore
 trait Trait where WC1, WC2, ..., WCn {
    ...
 }
 ```
 ```text
 forall<Type> {
    WellFormed(Type: Trait) :- WC1 && WC2 && .. && WCn.
 }
 ```
 and indeed this was basically what was done in rustc until it was noticed that
 this mixed badly with implied bounds. The key thing is that implied bounds
 allows someone to derive all bounds implied by a fact in the environment, and
 this *transitively* as we've seen with the `A + B + C` traits example.
 However, the `WellFormed` predicate as defined above only checks that the
 *direct* superbounds hold. That is, if we come back to our `A + B + C`
 example:
 ```rust,ignore
 trait A { }
 // No where clauses, always well-formed.
 // forall<Type> { WellFormed(Type: A). }
 trait B where Self: A { }
 // We only check the direct superbound `Self: A`.
 // forall<Type> { WellFormed(Type: B) :- Implemented(Type: A). }
 trait C where Self: B { }
 // We only check the direct superbound `Self: B`. We do not check
 // the `Self: A` implied bound  coming from the `Self: B` superbound.
 // forall<Type> { WellFormed(Type: C) :- Implemented(Type: B). }
 ```
 There is an asymmetry between the recursive power of implied bounds and
 the shallow checking of `WellFormed`. It turns out that this asymmetry
 can be [exploited][bug]. Indeed, suppose that we define the following
 traits:
 ```rust,ignore
 trait Partial where Self: Copy { }
 // WellFormed(Self: Partial) :- Implemented(Self: Copy).
 trait Complete where Self: Partial { }
 // WellFormed(Self: Complete) :- Implemented(Self: Partial).
 impl<T> Partial for T where T: Complete { }
 impl<T> Complete for T { }
 ```
 For the `Partial` impl, what the compiler must prove is:
 ```text
 forall<T> {
    if (T: Complete) { // assume that the where clauses hold
        WellFormed(T: Partial) // show that the trait reference is well-formed
    }
 }
 ```
 Proving `WellFormed(T: Partial)` amounts to proving `Implemented(T: Copy)`.
 However, we have `Implemented(T: Complete)` in our environment: thanks to
 implied bounds, we can deduce `Implemented(T: Partial)`. Using implied bounds
 one level deeper, we can deduce `Implemented(T: Copy)`. Finally, the `Partial`
 impl is legal.
 For the `Complete` impl, what the compiler must prove is:
 ```text
 forall<T> {
    WellFormed(T: Complete) // show that the trait reference is well-formed
 }
 ```
 Proving `WellFormed(T: Complete)` amounts to proving `Implemented(T: Partial)`.
 We see that the `impl Partial for T` applies if we can prove
 `Implemented(T: Complete)`, and it turns out we can prove this fact since our
 `impl<T> Complete for T` is a blanket impl without any where clauses.
 So both impls are legal and the compiler accepts the program. Moreover, thanks
 to the `Complete` blanket impl, all types implement `Complete`. So we could
 now use this impl like so:
 ```rust,ignore
 fn eat<T>(x: T) { }
 fn copy_everything<T: Complete>(x: T) {
    eat(x);
    eat(x);
 }
 fn main() {
    let not_copiable = vec![1, 2, 3, 4];
    copy_everything(not_copiable);
 }
 ```
 In this program, we use the fact that `Vec<i32>` implements `Complete`, as any
 other type. Hence we can call `copy_everything` with an argument of type
 `Vec<i32>`. Inside the `copy_everything` function, we have the
 `Implemented(T: Complete)` bound in our environment. Thanks to implied bounds,
 we can deduce `Implemented(T: Partial)`. Using implied bounds again, we deduce
 `Implemented(T: Copy)` and we can indeed call the `eat` function which moves
 the argument twice since its argument is `Copy`. Problem: the `T` type was
 in fact `Vec<i32>` which is not copy at all, hence we will double-free the
 underlying vec storage so we have a memory unsoundness in safe Rust.
 Of course, disregarding the asymmetry between `WellFormed` and implied bounds,
 this bug was possible only because we had some kind of self-referencing impls.
 But self-referencing impls are very useful in practice and are not the real
 culprits in this affair.
 [bug]: https://github.com/rust-lang/rust/pull/43786
 ## Co-inductiveness of `WellFormed`
 So the solution is to fix this asymmetry between `WellFormed` and implied
 bounds. For that, we need for the `WellFormed` predicate to not only require
 that the direct superbounds hold, but also all the bounds transitively implied
 by the superbounds. What we can do is to have the following rules for the
 `WellFormed` predicate:
 ```rust,ignore
 trait A { }
 // WellFormed(Self: A) :- Implemented(Self: A).
 trait B where Self: A { }
 // WellFormed(Self: B) :- Implemented(Self: B) && WellFormed(Self: A).
 trait C where Self: B { }
 // WellFormed(Self: C) :- Implemented(Self: C) && WellFormed(Self: B).
 ```
 Notice that we are now also requiring `Implemented(Self: Trait)` for
 `WellFormed(Self: Trait)` to be true: this is to simplify the process of
 traversing all the implied bounds transitively. This does not change anything
 when checking whether impls are legal, because since we assume
 that the where clauses hold inside the impl, we know that the corresponding
 trait reference do hold. Thanks to this setup, you can see that we indeed
 require to prove the set of all bounds transitively implied by the where
 clauses.
 However there is still a catch. Suppose that we have the following trait
 definition:
 ```rust,ignore
 trait Foo where <Self as Foo>::Item: Foo {
    type Item;
 }
 ```
 so this definition is a bit more involved than the ones we've seen already
 because it defines an associated item. However, the well-formedness rule
 would not be more complicated:
 ```text
 WellFormed(Self: Foo) :-
    Implemented(Self: Foo) &&
    WellFormed(<Self as Foo>::Item: Foo).
 ```
 Now we would like to write the following impl:
 ```rust,ignore
 impl Foo for i32 {
    type Item = i32;
 }
 ```
 The `Foo` trait definition and the `impl Foo for i32` are perfectly valid
 Rust: we're kind of recursively using our `Foo` impl in order to show that
 the associated value indeed implements `Foo`, but that's ok. But if we
 translate this to our well-formedness setting, the compiler proof process
 inside the `Foo` impl is the following: it starts with proving that the
 well-formedness goal `WellFormed(i32: Foo)` is true. In order to do that,
 it must prove the following goals: `Implemented(i32: Foo)` and
 `WellFormed(<i32 as Foo>::Item: Foo)`. `Implemented(i32: Foo)` holds because
 there is our impl and there are no where clauses on it so it's always true.
 However, because of the associated type value we used,
 `WellFormed(<i32 as Foo>::Item: Foo)` simplifies to just
 `WellFormed(i32: Foo)`. So in order to prove its original goal
 `WellFormed(i32: Foo)`, the compiler needs to prove `WellFormed(i32: Foo)`:
 this clearly is a cycle and cycles are usually rejected by the trait solver,
 unless...  if the `WellFormed` predicate was made to be co-inductive.
 A co-inductive predicate, as discussed in the chapter on
 [goals and clauses](./goals-and-clauses.md#coinductive-goals), are predicates
 for which the
 trait solver accepts cycles. In our setting, this would be a valid thing to do:
 indeed, the `WellFormed` predicate just serves as a way of enumerating all
 the implied bounds. Hence, it's like a fixed point algorithm: it tries to grow
 the set of implied bounds until there is nothing more to add. Here, a cycle
 in the chain of `WellFormed` predicates just means that there is no more bounds
 to add in that direction, so we can just accept this cycle and focus on other
 directions. It's easy to prove that under these co-inductive semantics, we
 are effectively visiting all the transitive implied bounds, and only these.
 ## Implied bounds on types
 We mainly talked about implied bounds for traits because this was the most
 subtle regarding implementation. Implied bounds on types are simpler,
 especially because if we assume that a type is well-formed, we don't use that
 fact to deduce that other types are well-formed, we only use it to deduce
 that e.g. some trait bounds hold.
 For types, we just use rules like these ones:
 ```rust,ignore
 struct Type<...> where WC1, ..., WCn {
    ...
 }
 ```
 ```text
 forall<...> {
    WellFormed(Type<...>) :- WC1, ..., WCn.
 }
 forall<...> {
    FromEnv(WC1) :- FromEnv(Type<...>).
    ...
    FromEnv(WCn) :- FromEnv(Type<...>).
 }
 ```
 We can see that we have this asymmetry between well-formedness check,
 which only verifies that the direct superbounds hold, and implied bounds which
 gives access to all bounds transitively implied by the where clauses. In that
 case this is ok because as we said, we don't use `FromEnv(Type<...>)` to deduce
 other `FromEnv(OtherType<...>)` things, nor do we use `FromEnv(Type: Trait)` to
 deduce `FromEnv(OtherType<...>)` things. So in that sense type definitions are
 "less recursive" than traits, and we saw in a previous subsection that
 it was the combination of asymmetry and recursive trait / impls that led to
 unsoundness. As such, the `WellFormed(Type<...>)` predicate does not need
 to be co-inductive.
 This asymmetry optimization is useful because in a real Rust program, we have
 to check the well-formedness of types very often (e.g. for each type which
 appears in the body of a function).
--- a/src/traits/index.md
+++ b/src/traits/index.md
@ -1,64 +0,0 @@
 # Trait solving (new-style)
 > 🚧 This chapter describes "new-style" trait solving. This is still in the
 > [process of being implemented][wg]; this chapter serves as a kind of
 > in-progress design document. If you would prefer to read about how the
 > current trait solver works, check out
 > [this other chapter](./resolution.html). 🚧
 >
 > By the way, if you would like to help in hacking on the new solver, you will
 > find instructions for getting involved in the
 > [Traits Working Group tracking issue][wg]!
 [wg]: https://github.com/rust-lang/rust/issues/48416
 The new-style trait solver is based on the work done in [chalk][chalk]. Chalk
 recasts Rust's trait system explicitly in terms of logic programming. It does
 this by "lowering" Rust code into a kind of logic program we can then execute
 queries against.
 You can read more about chalk itself in the
 [Overview of Chalk](./chalk-overview.md) section.
 Trait solving in rustc is based around a few key ideas:
 - [Lowering to logic](./lowering-to-logic.html), which expresses
  Rust traits in terms of standard logical terms.
  - The [goals and clauses](./goals-and-clauses.html) chapter
    describes the precise form of rules we use, and
    [lowering rules](./lowering-rules.html) gives the complete set of
    lowering rules in a more reference-like form.
  - [Lazy normalization](./associated-types.html), which is the
    technique we use to accommodate associated types when figuring out
    whether types are equal.
  - [Region constraints](./regions.html), which are accumulated
    during trait solving but mostly ignored. This means that trait
    solving effectively ignores the precise regions involved, always –
    but we still remember the constraints on them so that those
    constraints can be checked by the type checker.
 - [Canonical queries](./canonical-queries.html), which allow us
  to solve trait problems (like "is `Foo` implemented for the type
  `Bar`?") once, and then apply that same result independently in many
  different inference contexts.
 > This is not a complete list of topics. See the sidebar for more.
 ## Ongoing work
 The design of the new-style trait solving currently happens in two places:
 **chalk**. The [chalk][chalk] repository is where we experiment with new ideas
 and designs for the trait system. It primarily consists of two parts:
 * a unit testing framework
  for the correctness and feasibility of the logical rules defining the
  new-style trait system.
 * the [`chalk_engine`][chalk_engine] crate, which
  defines the new-style trait solver used both in the unit testing framework
  and in rustc.
 **rustc**. Once we are happy with the logical rules, we proceed to
 implementing them in rustc. This mainly happens in
 [`librustc_traits`][librustc_traits].
 [chalk]: https://github.com/rust-lang/chalk
 [chalk_engine]: https://github.com/rust-lang/chalk/tree/master/chalk-engine
 [librustc_traits]: https://github.com/rust-lang/rust/tree/master/src/librustc_traits
--- a/src/traits/lowering-rules.md
+++ b/src/traits/lowering-rules.md
@ -1,416 +0,0 @@
 # Lowering rules
 This section gives the complete lowering rules for Rust traits into
 [program clauses][pc]. It is a kind of reference. These rules
 reference the [domain goals][dg] defined in an earlier section.
 [pc]: ./goals-and-clauses.html
 [dg]: ./goals-and-clauses.html#domain-goals
 ## Notation
 The nonterminal `Pi` is used to mean some generic *parameter*, either a
 named lifetime like `'a` or a type parameter like `A`.
 The nonterminal `Ai` is used to mean some generic *argument*, which
 might be a lifetime like `'a` or a type like `Vec<A>`.
 When defining the lowering rules, we will give goals and clauses in
 the [notation given in this section](./goals-and-clauses.html).
 We sometimes insert "macros" like `LowerWhereClause!` into these
 definitions; these macros reference other sections within this chapter.
 ## Rule names and cross-references
 Each of these lowering rules is given a name, documented with a
 comment like so:
    // Rule Foo-Bar-Baz
 The reference implementation of these rules is to be found in
 [`chalk/chalk-solve/src/clauses.rs`][chalk_rules]. They are also ported in
 rustc in the [`librustc_traits`][librustc_traits] crate.
 [chalk_rules]: https://github.com/rust-lang/chalk/blob/master/chalk-solve/src/clauses.rs
 [librustc_traits]: https://github.com/rust-lang/rust/tree/master/src/librustc_traits
 ## Lowering where clauses
 When used in a goal position, where clauses can be mapped directly to
 the `Holds` variant of [domain goals][dg], as follows:
 - `A0: Foo<A1..An>` maps to `Implemented(A0: Foo<A1..An>)`
 - `T: 'r` maps to `Outlives(T, 'r)`
 - `'a: 'b` maps to `Outlives('a, 'b)`
 - `A0: Foo<A1..An, Item = T>` is a bit special and expands to two distinct
  goals, namely `Implemented(A0: Foo<A1..An>)` and
  `ProjectionEq(<A0 as Foo<A1..An>>::Item = T)`
 In the rules below, we will use `WC` to indicate where clauses that
 appear in Rust syntax; we will then use the same `WC` to indicate
 where those where clauses appear as goals in the program clauses that
 we are producing. In that case, the mapping above is used to convert
 from the Rust syntax into goals.
 ### Transforming the lowered where clauses
 In addition, in the rules below, we sometimes do some transformations
 on the lowered where clauses, as defined here:
 - `FromEnv(WC)` – this indicates that:
  - `Implemented(TraitRef)` becomes `FromEnv(TraitRef)`
  - other where-clauses are left intact
 - `WellFormed(WC)` – this indicates that:
  - `Implemented(TraitRef)` becomes `WellFormed(TraitRef)`
  - other where-clauses are left intact
 *TODO*: I suspect that we want to alter the outlives relations too,
 but Chalk isn't modeling those right now.
 ## Lowering traits
 Given a trait definition
 ```rust,ignore
 trait Trait<P1..Pn> // P0 == Self
 where WC
 {
    // trait items
 }
 ```
 we will produce a number of declarations. This section is focused on
 the program clauses for the trait header (i.e., the stuff outside the
 `{}`); the [section on trait items](#trait-items) covers the stuff
 inside the `{}`.
 ### Trait header
 From the trait itself we mostly make "meta" rules that setup the
 relationships between different kinds of domain goals.  The first such
 rule from the trait header creates the mapping between the `FromEnv`
 and `Implemented` predicates:
 ```text
 // Rule Implemented-From-Env
 forall<Self, P1..Pn> {
  Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn>)
 }
 ```
 <a name="implied-bounds"></a>
 #### Implied bounds
 The next few clauses have to do with implied bounds (see also
 [RFC 2089] and the [implied bounds][implied_bounds] chapter for a more in depth
 cover). For each trait, we produce two clauses:
 [RFC 2089]: https://rust-lang.github.io/rfcs/2089-implied-bounds.html
 [implied_bounds]: ./implied-bounds.md
 ```text
 // Rule Implied-Bound-From-Trait
 //
 // For each where clause WC:
 forall<Self, P1..Pn> {
  FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>)
 }
 ```
 This clause says that if we are assuming that the trait holds, then we can also
 assume that its where-clauses hold. It's perhaps useful to see an example:
 ```rust,ignore
 trait Eq: PartialEq { ... }
 ```
 In this case, the `PartialEq` supertrait is equivalent to a `where
 Self: PartialEq` where clause, in our simplified model. The program
 clause above therefore states that if we can prove `FromEnv(T: Eq)` –
 e.g., if we are in some function with `T: Eq` in its where clauses –
 then we also know that `FromEnv(T: PartialEq)`. Thus the set of things
 that follow from the environment are not only the **direct where
 clauses** but also things that follow from them.
 The next rule is related; it defines what it means for a trait reference
 to be **well-formed**:
 ```text
 // Rule WellFormed-TraitRef
 forall<Self, P1..Pn> {
  WellFormed(Self: Trait<P1..Pn>) :- Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)
 }
 ```
 This `WellFormed` rule states that `T: Trait` is well-formed if (a)
 `T: Trait` is implemented and (b) all the where-clauses declared on
 `Trait` are well-formed (and hence they are implemented). Remember
 that the `WellFormed` predicate is
 [coinductive](./goals-and-clauses.html#coinductive); in this
 case, it is serving as a kind of "carrier" that allows us to enumerate
 all the where clauses that are transitively implied by `T: Trait`.
 An example:
 ```rust,ignore
 trait Foo: A + Bar { }
 trait Bar: B + Foo { }
 trait A { }
 trait B { }
 ```
 Here, the transitive set of implications for `T: Foo` are `T: A`, `T: Bar`, and
 `T: B`.  And indeed if we were to try to prove `WellFormed(T: Foo)`, we would
 have to prove each one of those:
 - `WellFormed(T: Foo)`
  - `Implemented(T: Foo)`
  - `WellFormed(T: A)`
    - `Implemented(T: A)`
  - `WellFormed(T: Bar)`
    - `Implemented(T: Bar)`
    - `WellFormed(T: B)`
      - `Implemented(T: Bar)`
    - `WellFormed(T: Foo)` -- cycle, true coinductively
 This `WellFormed` predicate is only used when proving that impls are
 well-formed – basically, for each impl of some trait ref `TraitRef`,
 we must show that `WellFormed(TraitRef)`. This in turn justifies the
 implied bounds rules that allow us to extend the set of `FromEnv`
 items.
 ## Lowering type definitions
 We also want to have some rules which define when a type is well-formed.
 For example, given this type:
 ```rust,ignore
 struct Set<K> where K: Hash { ... }
 ```
 then `Set<i32>` is well-formed because `i32` implements `Hash`, but
 `Set<NotHash>` would not be well-formed. Basically, a type is well-formed
 if its parameters verify the where clauses written on the type definition.
 Hence, for every type definition:
 ```rust, ignore
 struct Type<P1..Pn> where WC { ... }
 ```
 we produce the following rule:
 ```text
 // Rule WellFormed-Type
 forall<P1..Pn> {
  WellFormed(Type<P1..Pn>) :- WC
 }
 ```
 Note that we use `struct` for defining a type, but this should be understood
 as a general type definition (it could be e.g. a generic `enum`).
 Conversely, we define rules which say that if we assume that a type is
 well-formed, we can also assume that its where clauses hold. That is,
 we produce the following family of rules:
 ```text
 // Rule Implied-Bound-From-Type
 //
 // For each where clause `WC`
 forall<P1..Pn> {
  FromEnv(WC) :- FromEnv(Type<P1..Pn>)
 }
 ```
 As for the implied bounds RFC, functions will *assume* that their arguments
 are well-formed. For example, suppose we have the following bit of code:
 ```rust,ignore
 trait Hash: Eq { }
 struct Set<K: Hash> { ... }
 fn foo<K>(collection: Set<K>, x: K, y: K) {
    // `x` and `y` can be equalized even if we did not explicitly write
    // `where K: Eq`
    if x == y {
        ...
    }
 }
 ```
 In the `foo` function, we assume that `Set<K>` is well-formed, i.e. we have
 `FromEnv(Set<K>)` in our environment. Because of the previous rule, we get
 `FromEnv(K: Hash)` without needing an explicit where clause. And because
 of the `Hash` trait definition, there also exists a rule which says:
 ```text
 forall<K> {
  FromEnv(K: Eq) :- FromEnv(K: Hash)
 }
 ```
 which means that we finally get `FromEnv(K: Eq)` and then can compare `x`
 and `y` without needing an explicit where clause.
 <a name="trait-items"></a>
 ## Lowering trait items
 ### Associated type declarations
 Given a trait that declares a (possibly generic) associated type:
 ```rust,ignore
 trait Trait<P1..Pn> // P0 == Self
 where WC
 {
    type AssocType<Pn+1..Pm>: Bounds where WC1;
 }
 ```
 We will produce a number of program clauses. The first two define
 the rules by which `ProjectionEq` can succeed; these two clauses are discussed
 in detail in the [section on associated types](./associated-types.html),
 but reproduced here for reference:
 ```text
 // Rule ProjectionEq-Normalize
 //
 // ProjectionEq can succeed by normalizing:
 forall<Self, P1..Pn, Pn+1..Pm, U> {
  ProjectionEq(<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> = U) :-
      Normalize(<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> -> U)
 }
 ```
 ```text
 // Rule ProjectionEq-Placeholder
 //
 // ProjectionEq can succeed through the placeholder associated type,
 // see "associated type" chapter for more:
 forall<Self, P1..Pn, Pn+1..Pm> {
  ProjectionEq(
    <Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> =
    (Trait::AssocType)<Self, P1..Pn, Pn+1..Pm>
  )
 }
 ```
 The next rule covers implied bounds for the projection. In particular,
 the `Bounds` declared on the associated type must have been proven to hold
 to show that the impl is well-formed, and hence we can rely on them
 elsewhere.
 ```text
 // Rule Implied-Bound-From-AssocTy
 //
 // For each `Bound` in `Bounds`:
 forall<Self, P1..Pn, Pn+1..Pm> {
    FromEnv(<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm>>: Bound) :-
      FromEnv(Self: Trait<P1..Pn>) && WC1
 }
 ```
 Next, we define the requirements for an instantiation of our associated
 type to be well-formed...
 ```text
 // Rule WellFormed-AssocTy
 forall<Self, P1..Pn, Pn+1..Pm> {
    WellFormed((Trait::AssocType)<Self, P1..Pn, Pn+1..Pm>) :-
      Implemented(Self: Trait<P1..Pn>) && WC1
 }
 ```
 ...along with the reverse implications, when we can assume that it is
 well-formed.
 ```text
 // Rule Implied-WC-From-AssocTy
 //
 // For each where clause WC1:
 forall<Self, P1..Pn, Pn+1..Pm> {
    FromEnv(WC1) :- FromEnv((Trait::AssocType)<Self, P1..Pn, Pn+1..Pm>)
 }
 ```
 ```text
 // Rule Implied-Trait-From-AssocTy
 forall<Self, P1..Pn, Pn+1..Pm> {
    FromEnv(Self: Trait<P1..Pn>) :-
      FromEnv((Trait::AssocType)<Self, P1..Pn, Pn+1..Pm>)
 }
 ```
 ### Lowering function and constant declarations
 Chalk didn't model functions and constants, but I would eventually like to
 treat them exactly like normalization. See [the section on function/constant
 values below](#constant-vals) for more details.
 ## Lowering impls
 Given an impl of a trait:
 ```rust,ignore
 impl<P0..Pn> Trait<A1..An> for A0
 where WC
 {
    // zero or more impl items
 }
 ```
 Let `TraitRef` be the trait reference `A0: Trait<A1..An>`. Then we
 will create the following rules:
 ```text
 // Rule Implemented-From-Impl
 forall<P0..Pn> {
  Implemented(TraitRef) :- WC
 }
 ```
 In addition, we will lower all of the *impl items*.
 ## Lowering impl items
 ### Associated type values
 Given an impl that contains:
 ```rust,ignore
 impl<P0..Pn> Trait<P1..Pn> for P0
 where WC_impl
 {
    type AssocType<Pn+1..Pm> = T;
 }
 ```
 and our where clause `WC1` on the trait associated type from above, we
 produce the following rule:
 ```text
 // Rule Normalize-From-Impl
 forall<P0..Pm> {
  forall<Pn+1..Pm> {
    Normalize(<P0 as Trait<P1..Pn>>::AssocType<Pn+1..Pm> -> T) :-
      Implemented(P0 as Trait) && WC1
  }
 }
 ```
 Note that `WC_impl` and `WC1` both encode where-clauses that the impl can
 rely on. (`WC_impl` is not used here, because it is implied by
 `Implemented(P0 as Trait)`.)
 <a name="constant-vals"></a>
 ### Function and constant values
 Chalk didn't model functions and constants, but I would eventually
 like to treat them exactly like normalization. This presumably
 involves adding a new kind of parameter (constant), and then having a
 `NormalizeValue` domain goal. This is *to be written* because the
 details are a bit up in the air.
--- a/src/traits/lowering-to-logic.md
+++ b/src/traits/lowering-to-logic.md
@ -1,185 +0,0 @@
 # Lowering to logic
 The key observation here is that the Rust trait system is basically a
 kind of logic, and it can be mapped onto standard logical inference
 rules. We can then look for solutions to those inference rules in a
 very similar fashion to how e.g. a [Prolog] solver works. It turns out
 that we can't *quite* use Prolog rules (also called Horn clauses) but
 rather need a somewhat more expressive variant.
 [Prolog]: https://en.wikipedia.org/wiki/Prolog
 ## Rust traits and logic
 One of the first observations is that the Rust trait system is
 basically a kind of logic. As such, we can map our struct, trait, and
 impl declarations into logical inference rules. For the most part,
 these are basically Horn clauses, though we'll see that to capture the
 full richness of Rust – and in particular to support generic
 programming – we have to go a bit further than standard Horn clauses.
 To see how this mapping works, let's start with an example. Imagine
 we declare a trait and a few impls, like so:
 ```rust
 trait Clone { }
 impl Clone for usize { }
 impl<T> Clone for Vec<T> where T: Clone { }
 ```
 We could map these declarations to some Horn clauses, written in a
 Prolog-like notation, as follows:
 ```text
 Clone(usize).
 Clone(Vec<?T>) :- Clone(?T).
 // The notation `A :- B` means "A is true if B is true".
 // Or, put another way, B implies A.
 ```
 In Prolog terms, we might say that `Clone(Foo)` – where `Foo` is some
 Rust type – is a *predicate* that represents the idea that the type
 `Foo` implements `Clone`. These rules are **program clauses**; they
 state the conditions under which that predicate can be proven (i.e.,
 considered true). So the first rule just says "Clone is implemented
 for `usize`". The next rule says "for any type `?T`, Clone is
 implemented for `Vec<?T>` if clone is implemented for `?T`". So
 e.g. if we wanted to prove that `Clone(Vec<Vec<usize>>)`, we would do
 so by applying the rules recursively:
 - `Clone(Vec<Vec<usize>>)` is provable if:
  - `Clone(Vec<usize>)` is provable if:
    - `Clone(usize)` is provable. (Which it is, so we're all good.)
 But now suppose we tried to prove that `Clone(Vec<Bar>)`. This would
 fail (after all, I didn't give an impl of `Clone` for `Bar`):
 - `Clone(Vec<Bar>)` is provable if:
  - `Clone(Bar)` is provable. (But it is not, as there are no applicable rules.)
 We can easily extend the example above to cover generic traits with
 more than one input type. So imagine the `Eq<T>` trait, which declares
 that `Self` is equatable with a value of type `T`:
 ```rust,ignore
 trait Eq<T> { ... }
 impl Eq<usize> for usize { }
 impl<T: Eq<U>> Eq<Vec<U>> for Vec<T> { }
 ```
 That could be mapped as follows:
 ```text
 Eq(usize, usize).
 Eq(Vec<?T>, Vec<?U>) :- Eq(?T, ?U).
 ```
 So far so good.
 ## Type-checking normal functions
 OK, now that we have defined some logical rules that are able to
 express when traits are implemented and to handle associated types,
 let's turn our focus a bit towards **type-checking**. Type-checking is
 interesting because it is what gives us the goals that we need to
 prove. That is, everything we've seen so far has been about how we
 derive the rules by which we can prove goals from the traits and impls
 in the program; but we are also interested in how to derive the goals
 that we need to prove, and those come from type-checking.
 Consider type-checking the function `foo()` here:
 ```rust,ignore
 fn foo() { bar::<usize>() }
 fn bar<U: Eq<U>>() { }
 ```
 This function is very simple, of course: all it does is to call
 `bar::<usize>()`. Now, looking at the definition of `bar()`, we can see
 that it has one where-clause `U: Eq<U>`. So, that means that `foo()` will
 have to prove that `usize: Eq<usize>` in order to show that it can call `bar()`
 with `usize` as the type argument.
 If we wanted, we could write a Prolog predicate that defines the
 conditions under which `bar()` can be called. We'll say that those
 conditions are called being "well-formed":
 ```text
 barWellFormed(?U) :- Eq(?U, ?U).
 ```
 Then we can say that `foo()` type-checks if the reference to
 `bar::<usize>` (that is, `bar()` applied to the type `usize`) is
 well-formed:
 ```text
 fooTypeChecks :- barWellFormed(usize).
 ```
 If we try to prove the goal `fooTypeChecks`, it will succeed:
 - `fooTypeChecks` is provable if:
  - `barWellFormed(usize)`, which is provable if:
    - `Eq(usize, usize)`, which is provable because of an impl.
 Ok, so far so good. Let's move on to type-checking a more complex function.
 ## Type-checking generic functions: beyond Horn clauses
 In the last section, we used standard Prolog horn-clauses (augmented with Rust's
 notion of type equality) to type-check some simple Rust functions. But that only
 works when we are type-checking non-generic functions. If we want to type-check
 a generic function, it turns out we need a stronger notion of goal than what Prolog
 can provide. To see what I'm talking about, let's revamp our previous
 example to make `foo` generic:
 ```rust,ignore
 fn foo<T: Eq<T>>() { bar::<T>() }
 fn bar<U: Eq<U>>() { }
 ```
 To type-check the body of `foo`, we need to be able to hold the type
 `T` "abstract".  That is, we need to check that the body of `foo` is
 type-safe *for all types `T`*, not just for some specific type. We might express
 this like so:
 ```text
 fooTypeChecks :-
  // for all types T...
  forall<T> {
    // ...if we assume that Eq(T, T) is provable...
    if (Eq(T, T)) {
      // ...then we can prove that `barWellFormed(T)` holds.
      barWellFormed(T)
    }
  }.
 ```
 This notation I'm using here is the notation I've been using in my
 prototype implementation; it's similar to standard mathematical
 notation but a bit Rustified. Anyway, the problem is that standard
 Horn clauses don't allow universal quantification (`forall`) or
 implication (`if`) in goals (though many Prolog engines do support
 them, as an extension). For this reason, we need to accept something
 called "first-order hereditary harrop" (FOHH) clauses – this long
 name basically means "standard Horn clauses with `forall` and `if` in
 the body". But it's nice to know the proper name, because there is a
 lot of work describing how to efficiently handle FOHH clauses; see for
 example Gopalan Nadathur's excellent
 ["A Proof Procedure for the Logic of Hereditary Harrop Formulas"][pphhf]
 in [the bibliography].
 [the bibliography]: ./bibliography.html
 [pphhf]: ./bibliography.html#pphhf
 It turns out that supporting FOHH is not really all that hard. And
 once we are able to do that, we can easily describe the type-checking
 rule for generic functions like `foo` in our logic.
 ## Source
 This page is a lightly adapted version of a
 [blog post by Nicholas Matsakis][lrtl].
 [lrtl]: http://smallcultfollowing.com/babysteps/blog/2017/01/26/lowering-rust-traits-to-logic/
--- a/src/traits/resolution.md
+++ b/src/traits/resolution.md
@ -6,7 +6,7 @@ some non-obvious things.
 **Note:** This chapter (and its subchapters) describe how the trait
 solver **currently** works. However, we are in the process of
 designing a new trait solver. If you'd prefer to read about *that*,
-see [*this* traits chapter](./index.html).
+see [*this* subchapter](./chalk.html).
 ## Major concepts
--- a/src/traits/slg.md
+++ b/src/traits/slg.md
@ -1,302 +0,0 @@
 # The On-Demand SLG solver
 Given a set of program clauses (provided by our [lowering rules][lowering])
 and a query, we need to return the result of the query and the value of any
 type variables we can determine. This is the job of the solver.
 For example, `exists<T> { Vec<T>: FromIterator<u32> }` has one solution, so
 its result is `Unique; substitution [?T := u32]`. A solution also comes with
 a set of region constraints, which we'll ignore in this introduction.
 [lowering]: ./lowering-rules.html
 ## Goals of the Solver
 ### On demand
 There are often many, or even infinitely many, solutions to a query. For
 example, say we want to prove that `exists<T> { Vec<T>: Debug }` for _some_
 type `?T`. Our solver should be capable of yielding one answer at a time, say
 `?T = u32`, then `?T = i32`, and so on, rather than iterating over every type
 in the type system. If we need more answers, we can request more until we are
 done. This is similar to how Prolog works.
 *See also: [The traditional, interactive Prolog query][pq]*
 [pq]: ./canonical-queries.html#the-traditional-interactive-prolog-query
 ### Breadth-first
 `Vec<?T>: Debug` is true if `?T: Debug`. This leads to a cycle: `[Vec<u32>,
 Vec<Vec<u32>>, Vec<Vec<Vec<u32>>>]`, and so on all implement `Debug`. Our
 solver ought to be breadth first and consider answers like `[Vec<u32>: Debug,
 Vec<i32>: Debug, ...]` before it recurses, or we may never find the answer
 we're looking for.
 ### Cachable
 To speed up compilation, we need to cache results, including partial results
 left over from past solver queries.
 ## Description of how it works
 The basis of the solver is the [`Forest`] type. A *forest* stores a
 collection of *tables* as well as a *stack*. Each *table* represents
 the stored results of a particular query that is being performed, as
 well as the various *strands*, which are basically suspended
 computations that may be used to find more answers. Tables are
 interdependent: solving one query may require solving others.
 [`Forest`]: https://rust-lang.github.io/chalk/chalk_engine/forest/struct.Forest.html
 ### Walkthrough
 Perhaps the easiest way to explain how the solver works is to walk
 through an example. Let's imagine that we have the following program:
 ```rust,ignore
 trait Debug { }
 struct u32 { }
 impl Debug for u32 { }
 struct Rc<T> { }
 impl<T: Debug> Debug for Rc<T> { }
 struct Vec<T> { }
 impl<T: Debug> Debug for Vec<T> { }
 ```
 Now imagine that we want to find answers for the query `exists<T> { Rc<T>:
 Debug }`. The first step would be to u-canonicalize this query; this is the
 act of giving canonical names to all the unbound inference variables based on
 the order of their left-most appearance, as well as canonicalizing the
 universes of any universally bound names (e.g., the `T` in `forall<T> { ...
 }`). In this case, there are no universally bound names, but the canonical
 form Q of the query might look something like:
 ```text
 Rc<?0>: Debug
 ```
 where `?0` is a variable in the root universe U0. We would then go and
 look for a table with this canonical query as the key: since the forest is
 empty, this lookup will fail, and we will create a new table T0,
 corresponding to the u-canonical goal Q.
 **Ignoring negative reasoning and regions.** To start, we'll ignore
 the possibility of negative goals like `not { Foo }`. We'll phase them
 in later, as they bring several complications.
 **Creating a table.** When we first create a table, we also initialize
 it with a set of *initial strands*. A "strand" is kind of like a
 "thread" for the solver: it contains a particular way to produce an
 answer. The initial set of strands for a goal like `Rc<?0>: Debug`
 (i.e., a "domain goal") is determined by looking for *clauses* in the
 environment. In Rust, these clauses derive from impls, but also from
 where-clauses that are in scope. In the case of our example, there
 would be three clauses, each coming from the program. Using a
 Prolog-like notation, these look like:
 ```text
 (u32: Debug).
 (Rc<T>: Debug) :- (T: Debug).
 (Vec<T>: Debug) :- (T: Debug).
 ```
 To create our initial strands, then, we will try to apply each of
 these clauses to our goal of `Rc<?0>: Debug`. The first and third
 clauses are inapplicable because `u32` and `Vec<?0>` cannot be unified
 with `Rc<?0>`. The second clause, however, will work.
 **What is a strand?** Let's talk a bit more about what a strand *is*. In the code, a strand
 is the combination of an inference table, an _X-clause_, and (possibly)
 a selected subgoal from that X-clause. But what is an X-clause
 ([`ExClause`], in the code)? An X-clause pulls together a few things:
 - The current state of the goal we are trying to prove;
 - A set of subgoals that have yet to be proven;
 - There are also a few things we're ignoring for now:
  - delayed literals, region constraints
 The general form of an X-clause is written much like a Prolog clause,
 but with somewhat different semantics. Since we're ignoring delayed
 literals and region constraints, an X-clause just looks like this:
 ```text
 G :- L
 ```
 where G is a goal and L is a set of subgoals that must be proven.
 (The L stands for *literal* -- when we address negative reasoning, a
 literal will be either a positive or negative subgoal.) The idea is
 that if we are able to prove L then the goal G can be considered true.
 In the case of our example, we would wind up creating one strand, with
 an X-clause like so:
 ```text
 (Rc<?T>: Debug) :- (?T: Debug)
 ```
 Here, the `?T` refers to one of the inference variables created in the
 inference table that accompanies the strand. (I'll use named variables
 to refer to inference variables, and numbered variables like `?0` to
 refer to variables in a canonicalized goal; in the code, however, they
 are both represented with an index.)
 For each strand, we also optionally store a *selected subgoal*. This
 is the subgoal after the turnstile (`:-`) that we are currently trying
 to prove in this strand. Initially, when a strand is first created,
 there is no selected subgoal.
 [`ExClause`]: https://rust-lang.github.io/chalk/chalk_engine/struct.ExClause.html
 **Activating a strand.** Now that we have created the table T0 and
 initialized it with strands, we have to actually try and produce an answer.
 We do this by invoking the [`ensure_root_answer`] operation on the table:
 specifically, we say `ensure_root_answer(T0, A0)`, meaning "ensure that there
 is a 0th answer A0 to query T0".
 Remember that tables store not only strands, but also a vector of cached
 answers. The first thing that [`ensure_root_answer`] does is to check whether
 answer A0 is in this vector. If so, we can just return immediately. In this
 case, the vector will be empty, and hence that does not apply (this becomes
 important for cyclic checks later on).
 When there is no cached answer, [`ensure_root_answer`] will try to produce one.
 It does this by selecting a strand from the set of active strands -- the
 strands are stored in a `VecDeque` and hence processed in a round-robin
 fashion. Right now, we have only one strand, storing the following X-clause
 with no selected subgoal:
 ```text
 (Rc<?T>: Debug) :- (?T: Debug)
 ```
 When we activate the strand, we see that we have no selected subgoal,
 and so we first pick one of the subgoals to process. Here, there is only
 one (`?T: Debug`), so that becomes the selected subgoal, changing
 the state of the strand to:
 ```text
 (Rc<?T>: Debug) :- selected(?T: Debug, A0)
 ```
 Here, we write `selected(L, An)` to indicate that (a) the literal `L`
 is the selected subgoal and (b) which answer `An` we are looking for. We
 start out looking for `A0`.
 [`ensure_root_answer`]:  https://rust-lang.github.io/chalk/chalk_engine/forest/struct.Forest.html#method.ensure_root_answer
 **Processing the selected subgoal.** Next, we have to try and find an
 answer to this selected goal. To do that, we will u-canonicalize it
 and try to find an associated table. In this case, the u-canonical
 form of the subgoal is `?0: Debug`: we don't have a table yet for
 that, so we can create a new one, T1. As before, we'll initialize T1
 with strands. In this case, there will be three strands, because all
 the program clauses are potentially applicable. Those three strands
 will be:
 - `(u32: Debug) :-`, derived from the program clause `(u32: Debug).`.
  - Note: This strand has no subgoals.
 - `(Vec<?U>: Debug) :- (?U: Debug)`, derived from the `Vec` impl.
 - `(Rc<?U>: Debug) :- (?U: Debug)`, derived from the `Rc` impl.
 We can thus summarize the state of the whole forest at this point as
 follows:
 ```text
 Table T0 [Rc<?0>: Debug]
  Strands:
    (Rc<?T>: Debug) :- selected(?T: Debug, A0)
 Table T1 [?0: Debug]
  Strands:
    (u32: Debug) :-
    (Vec<?U>: Debug) :- (?U: Debug)
    (Rc<?V>: Debug) :- (?V: Debug)
 ```
 **Delegation between tables.** Now that the active strand from T0 has
 created the table T1, it can try to extract an answer. It does this
 via that same `ensure_answer` operation we saw before. In this case,
 the strand would invoke `ensure_answer(T1, A0)`, since we will start
 with the first answer. This will cause T1 to activate its first
 strand, `u32: Debug :-`.
 This strand is somewhat special: it has no subgoals at all. This means
 that the goal is proven. We can therefore add `u32: Debug` to the set
 of *answers* for our table, calling it answer A0 (it is the first
 answer). The strand is then removed from the list of strands.
 The state of table T1 is therefore:
 ```text
 Table T1 [?0: Debug]
  Answers:
    A0 = [?0 = u32]
  Strand:
    (Vec<?U>: Debug) :- (?U: Debug)
    (Rc<?V>: Debug) :- (?V: Debug)
 ```
 Note that I am writing out the answer A0 as a substitution that can be
 applied to the table goal; actually, in the code, the goals for each
 X-clause are also represented as substitutions, but in this exposition
 I've chosen to write them as full goals, following [NFTD].
 [NFTD]: ./bibliography.html#slg
 Since we now have an answer, `ensure_answer(T1, A0)` will return `Ok`
 to the table T0, indicating that answer A0 is available. T0 now has
 the job of incorporating that result into its active strand. It does
 this in two ways. First, it creates a new strand that is looking for
 the next possible answer of T1. Next, it incorpoates the answer from
 A0 and removes the subgoal. The resulting state of table T0 is:
 ```text
 Table T0 [Rc<?0>: Debug]
  Strands:
    (Rc<?T>: Debug) :- selected(?T: Debug, A1)
    (Rc<u32>: Debug) :-
 ```
 We then immediately activate the strand that incorporated the answer
 (the `Rc<u32>: Debug` one). In this case, that strand has no further
 subgoals, so it becomes an answer to the table T0. This answer can
 then be returned up to our caller, and the whole forest goes quiescent
 at this point (remember, we only do enough work to generate *one*
 answer). The ending state of the forest at this point will be:
 ```text
 Table T0 [Rc<?0>: Debug]
  Answer:
    A0 = [?0 = u32]
  Strands:
    (Rc<?T>: Debug) :- selected(?T: Debug, A1)
 Table T1 [?0: Debug]
  Answers:
    A0 = [?0 = u32]
  Strand:
    (Vec<?U>: Debug) :- (?U: Debug)
    (Rc<?V>: Debug) :- (?V: Debug)
 ```
 Here you can see how the forest captures both the answers we have
 created thus far *and* the strands that will let us try to produce
 more answers later on.
 ## See also
 - [chalk_solve README][readme], which contains links to papers used and
  acronyms referenced in the code
 - This section is a lightly adapted version of the blog post [An on-demand
  SLG solver for chalk][slg-blog]
 - [Negative Reasoning in Chalk][negative-reasoning-blog] explains the need
  for negative reasoning, but not how the SLG solver does it
 [readme]: https://github.com/rust-lang/chalk/blob/239e4ae4e69b2785b5f99e0f2b41fc16b0b4e65e/chalk-engine/src/README.md
 [slg-blog]: http://smallcultfollowing.com/babysteps/blog/2018/01/31/an-on-demand-slg-solver-for-chalk/
 [negative-reasoning-blog]: https://aturon.github.io/blog/2017/04/24/negative-chalk/
--- a/src/traits/wf.md
+++ b/src/traits/wf.md
@ -1,469 +0,0 @@
 # Well-formedness checking
 WF checking has the job of checking that the various declarations in a Rust
 program are well-formed. This is the basis for implied bounds, and partly for
 that reason, this checking can be surprisingly subtle! For example, we
 have to be sure that each impl proves the WF conditions declared on
 the trait.
 For each declaration in a Rust program, we will generate a logical goal and try
 to prove it using the lowered rules we described in the
 [lowering rules](./lowering-rules.md) chapter. If we are able to prove it, we
 say that the construct is well-formed. If not, we report an error to the user.
 Well-formedness checking happens in the [`chalk/chalk-solve/src/wf.rs`][wf]
 module in chalk. After you have read this chapter, you may find useful to see
 an extended set of examples in the [`chalk/tests/test/wf_lowering.rs`][wf_test] submodule.
 The new-style WF checking has not been implemented in rustc yet.
 [wf]: https://github.com/rust-lang/chalk/blob/master/chalk-solve/src/wf.rs
 [wf_test]: https://github.com/rust-lang/chalk/blob/master/tests/test/wf_lowering.rs
 We give here a complete reference of the generated goals for each Rust
 declaration.
 In addition to the notations introduced in the chapter about
 lowering rules, we'll introduce another notation: when checking WF of a
 declaration, we'll often have to prove that all types that appear are
 well-formed, except type parameters that we always assume to be WF. Hence,
 we'll use the following notation: for a type `SomeType<...>`, we define
 `InputTypes(SomeType<...>)` to be the set of all non-parameter types appearing
 in `SomeType<...>`, including `SomeType<...>` itself.
 Examples:
 * `InputTypes((u32, f32)) = [u32, f32, (u32, f32)]`
 * `InputTypes(Box<T>) = [Box<T>]` (assuming that `T` is a type parameter)
 * `InputTypes(Box<Box<T>>) = [Box<T>, Box<Box<T>>]`
 We also extend the `InputTypes` notation to where clauses in the natural way.
 So, for example `InputTypes(A0: Trait<A1,...,An>)` is the union of
 `InputTypes(A0)`, `InputTypes(A1)`, ..., `InputTypes(An)`.
 # Type definitions
 Given a general type definition:
 ```rust,ignore
 struct Type<P...> where WC_type {
    field1: A1,
    ...
    fieldn: An,
 }
 ```
 we generate the following goal, which represents its well-formedness condition:
 ```text
 forall<P...> {
    if (FromEnv(WC_type)) {
        WellFormed(InputTypes(WC_type)) &&
            WellFormed(InputTypes(A1)) &&
            ...
            WellFormed(InputTypes(An))
    }
 }
 ```
 which in English states: assuming that the where clauses defined on the type
 hold, prove that every type appearing in the type definition is well-formed.
 Some examples:
 ```rust,ignore
 struct OnlyClone<T> where T: Clone {
    clonable: T,
 }
 // The only types appearing are type parameters: we have nothing to check,
 // the type definition is well-formed.
 ```
 ```rust,ignore
 struct Foo<T> where T: Clone {
    foo: OnlyClone<T>,
 }
 // The only non-parameter type which appears in this definition is
 // `OnlyClone<T>`. The generated goal is the following:
 // ```
 // forall<T> {
 //     if (FromEnv(T: Clone)) {
 //          WellFormed(OnlyClone<T>)
 //     }
 // }
 // ```
 // which is provable.
 ```
 ```rust,ignore
 struct Bar<T> where <T as Iterator>::Item: Debug {
    bar: i32,
 }
 // The only non-parameter types which appear in this definition are
 // `<T as Iterator>::Item` and `i32`. The generated goal is the following:
 // ```
 // forall<T> {
 //     if (FromEnv(<T as Iterator>::Item: Debug)) {
 //          WellFormed(<T as Iterator>::Item) &&
 //               WellFormed(i32)
 //     }
 // }
 // ```
 // which is not provable since `WellFormed(<T as Iterator>::Item)` requires
 // proving `Implemented(T: Iterator)`, and we are unable to prove that for an
 // unknown `T`.
 //
 // Hence, this type definition is considered illegal. An additional
 // `where T: Iterator` would make it legal.
 ```
 # Trait definitions
 Given a general trait definition:
 ```rust,ignore
 trait Trait<P1...> where WC_trait {
    type Assoc<P2...>: Bounds_assoc where WC_assoc;
 }
 ```
 we generate the following goal:
 ```text
 forall<P1...> {
    if (FromEnv(WC_trait)) {
        WellFormed(InputTypes(WC_trait)) &&
            forall<P2...> {
                if (FromEnv(WC_assoc)) {
                    WellFormed(InputTypes(Bounds_assoc)) &&
                        WellFormed(InputTypes(WC_assoc))
                }
            }
    }
 }
 ```
 There is not much to verify in a trait definition. We just want
 to prove that the types appearing in the trait definition are well-formed,
 under the assumption that the different where clauses hold.
 Some examples:
 ```rust,ignore
 trait Foo<T> where T: Iterator, <T as Iterator>::Item: Debug {
    ...
 }
 // The only non-parameter type which appears in this definition is
 // `<T as Iterator>::Item`. The generated goal is the following:
 // ```
 // forall<T> {
 //     if (FromEnv(T: Iterator), FromEnv(<T as Iterator>::Item: Debug)) {
 //         WellFormed(<T as Iterator>::Item)
 //     }
 // }
 // ```
 // which is provable thanks to the `FromEnv(T: Iterator)` assumption.
 ```
 ```rust,ignore
 trait Bar {
    type Assoc<T>: From<<T as Iterator>::Item>;
 }
 // The only non-parameter type which appears in this definition is
 // `<T as Iterator>::Item`. The generated goal is the following:
 // ```
 // forall<T> {
 //     WellFormed(<T as Iterator>::Item)
 // }
 // ```
 // which is not provable, hence the trait definition is considered illegal.
 ```
 ```rust,ignore
 trait Baz {
    type Assoc<T>: From<<T as Iterator>::Item> where T: Iterator;
 }
 // The generated goal is now:
 // ```
 // forall<T> {
 //     if (FromEnv(T: Iterator)) {
 //         WellFormed(<T as Iterator>::Item)
 //     }
 // }
 // ```
 // which is now provable.
 ```
 # Impls
 Now we give ourselves a general impl for the trait defined above:
 ```rust,ignore
 impl<P1...> Trait<A1...> for SomeType<A2...> where WC_impl {
    type Assoc<P2...> = SomeValue<A3...> where WC_assoc;
 }
 ```
 Note that here, `WC_assoc` are the same where clauses as those defined on the
 associated type definition in the trait declaration, *except* that type
 parameters from the trait are substituted with values provided by the impl
 (see example below). You cannot add new where clauses. You may omit to write
 the where clauses if you want to emphasize the fact that you are actually not
 relying on them.
 Some examples to illustrate that:
 ```rust,ignore
 trait Foo<T> {
    type Assoc where T: Clone;
 }
 struct OnlyClone<T: Clone> { ... }
 impl<U> Foo<Option<U>> for () {
    // We substitute type parameters from the trait by the ones provided
    // by the impl, that is instead of having a `T: Clone` where clause,
    // we have an `Option<U>: Clone` one.
    type Assoc = OnlyClone<Option<U>> where Option<U>: Clone;
 }
 impl<T> Foo<T> for i32 {
    // I'm not using the `T: Clone` where clause from the trait, so I can
    // omit it.
    type Assoc = u32;
 }
 impl<T> Foo<T> for f32 {
    type Assoc = OnlyClone<Option<T>> where Option<T>: Clone;
    //                                ^^^^^^^^^^^^^^^^^^^^^^
    //                                this where clause does not exist
    //                                on the original trait decl: illegal
 }
 ```
 > So in Rust, where clauses on associated types work *exactly* like where
 > clauses on trait methods: in an impl, we must substitute the parameters from
 > the traits with values provided by the impl, we may omit them if we don't
 > need them, but we cannot add new where clauses.
 Now let's see the generated goal for this general impl:
 ```text
 forall<P1...> {
    // Well-formedness of types appearing in the impl
    if (FromEnv(WC_impl), FromEnv(InputTypes(SomeType<A2...>: Trait<A1...>))) {
        WellFormed(InputTypes(WC_impl)) &&
            forall<P2...> {
                if (FromEnv(WC_assoc)) {
                        WellFormed(InputTypes(SomeValue<A3...>))
                }
            }
    }
    // Implied bounds checking
    if (FromEnv(WC_impl), FromEnv(InputTypes(SomeType<A2...>: Trait<A1...>))) {
        WellFormed(SomeType<A2...>: Trait<A1...>) &&
            forall<P2...> {
                if (FromEnv(WC_assoc)) {
                    WellFormed(SomeValue<A3...>: Bounds_assoc)
                }
            }
    }
 }
 ```
 Here is the most complex goal. As always, first, assuming that
 the various where clauses hold, we prove that every type appearing in the impl
 is well-formed, ***except*** types appearing in the impl header
 `SomeType<A2...>: Trait<A1...>`. Instead, we *assume* that those types are
 well-formed
 (hence the `if (FromEnv(InputTypes(SomeType<A2...>: Trait<A1...>)))`
 conditions). This is
 part of the implied bounds proposal, so that we can rely on the bounds
 written on the definition of e.g. the `SomeType<A2...>` type (and that we don't
 need to repeat those bounds).
 > Note that we don't need to check well-formedness of types appearing in
 > `WC_assoc` because we already did that in the trait decl (they are just
 > repeated with some substitutions of values which we already assume to be
 > well-formed)
 Next, still assuming that the where clauses on the impl `WC_impl` hold and that
 the input types of `SomeType<A2...>` are well-formed, we prove that
 `WellFormed(SomeType<A2...>: Trait<A1...>)` hold. That is, we want to prove
 that `SomeType<A2...>` verify all the where clauses that might transitively
 be required by the `Trait` definition (see
 [this subsection](./implied-bounds.md#co-inductiveness-of-wellformed)).
 Lastly, assuming in addition that the where clauses on the associated type
 `WC_assoc` hold,
 we prove that `WellFormed(SomeValue<A3...>: Bounds_assoc)` hold. Again, we are
 not only proving `Implemented(SomeValue<A3...>: Bounds_assoc)`, but also
 all the facts that might transitively come from `Bounds_assoc`. We must do this
 because we allow the use of implied bounds on associated types: if we have
 `FromEnv(SomeType: Trait)` in our environment, the lowering rules
 chapter indicates that we are able to deduce
 `FromEnv(<SomeType as Trait>::Assoc: Bounds_assoc)` without knowing what the
 precise value of `<SomeType as Trait>::Assoc` is.
 Some examples for the generated goal:
 ```rust,ignore
 // Trait Program Clauses
 // These are program clauses that come from the trait definitions below
 // and that the trait solver can use for its reasonings. I'm just restating
 // them here so that we have them in mind.
 trait Copy { }
 // This is a program clause that comes from the trait definition above
 // and that the trait solver can use for its reasonings. I'm just restating
 // it here (and also the few other ones coming just after) so that we have
 // them in mind.
 // `WellFormed(Self: Copy) :- Implemented(Self: Copy).`
 trait Partial where Self: Copy { }
 // ```
 // WellFormed(Self: Partial) :-
 //     Implemented(Self: Partial) &&
 //     WellFormed(Self: Copy).
 // ```
 trait Complete where Self: Partial { }
 // ```
 // WellFormed(Self: Complete) :-
 //     Implemented(Self: Complete) &&
 //     WellFormed(Self: Partial).
 // ```
 // Impl WF Goals
 impl<T> Partial for T where T: Complete { }
 // The generated goal is:
 // ```
 // forall<T> {
 //     if (FromEnv(T: Complete)) {
 //         WellFormed(T: Partial)
 //     }
 // }
 // ```
 // Then proving `WellFormed(T: Partial)` amounts to proving
 // `Implemented(T: Partial)` and `Implemented(T: Copy)`.
 // Both those facts can be deduced from the `FromEnv(T: Complete)` in our
 // environment: this impl is legal.
 impl<T> Complete for T { }
 // The generated goal is:
 // ```
 // forall<T> {
 //     WellFormed(T: Complete)
 // }
 // ```
 // Then proving `WellFormed(T: Complete)` amounts to proving
 // `Implemented(T: Complete)`, `Implemented(T: Partial)` and
 // `Implemented(T: Copy)`.
 //
 // `Implemented(T: Complete)` can be proved thanks to the
 // `impl<T> Complete for T` blanket impl.
 //
 // `Implemented(T: Partial)` can be proved thanks to the
 // `impl<T> Partial for T where T: Complete` impl and because we know
 // `T: Complete` holds.
 // However, `Implemented(T: Copy)` cannot be proved: the impl is illegal.
 // An additional `where T: Copy` bound would be sufficient to make that impl
 // legal.
 ```
 ```rust,ignore
 trait Bar { }
 impl<T> Bar for T where <T as Iterator>::Item: Bar { }
 // We have a non-parameter type appearing in the where clauses:
 // `<T as Iterator>::Item`. The generated goal is:
 // ```
 // forall<T> {
 //     if (FromEnv(<T as Iterator>::Item: Bar)) {
 //         WellFormed(T: Bar) &&
 //             WellFormed(<T as Iterator>::Item: Bar)
 //     }
 // }
 // ```
 // And `WellFormed(<T as Iterator>::Item: Bar)` is not provable: we'd need
 // an additional `where T: Iterator` for example.
 ```
 ```rust,ignore
 trait Foo { }
 trait Bar {
    type Item: Foo;
 }
 struct Stuff<T> { }
 impl<T> Bar for Stuff<T> where T: Foo {
    type Item = T;
 }
 // The generated goal is:
 // ```
 // forall<T> {
 //     if (FromEnv(T: Foo)) {
 //         WellFormed(T: Foo).
 //     }
 // }
 // ```
 // which is provable.
 ```
 ```rust,ignore
 trait Debug { ... }
 // `WellFormed(Self: Debug) :- Implemented(Self: Debug).`
 struct Box<T> { ... }
 impl<T> Debug for Box<T> where T: Debug { ... }
 trait PointerFamily {
    type Pointer<T>: Debug where T: Debug;
 }
 // `WellFormed(Self: PointerFamily) :- Implemented(Self: PointerFamily).`
 struct BoxFamily;
 impl PointerFamily for BoxFamily {
    type Pointer<T> = Box<T> where T: Debug;
 }
 // The generated goal is:
 // ```
 // forall<T> {
 //     WellFormed(BoxFamily: PointerFamily) &&
 //
 //     if (FromEnv(T: Debug)) {
 //         WellFormed(Box<T>: Debug) &&
 //             WellFormed(Box<T>)
 //     }
 // }
 // ```
 // `WellFormed(BoxFamily: PointerFamily)` amounts to proving
 // `Implemented(BoxFamily: PointerFamily)`, which is ok thanks to our impl.
 //
 // `WellFormed(Box<T>)` is always true (there are no where clauses on the
 // `Box` type definition).
 //
 // Moreover, we have an `impl<T: Debug> Debug for Box<T>`, hence
 // we can prove `WellFormed(Box<T>: Debug)` and the impl is indeed legal.
 ```
 ```rust,ignore
 trait Foo {
    type Assoc<T>;
 }
 struct OnlyClone<T: Clone> { ... }
 impl Foo for i32 {
    type Assoc<T> = OnlyClone<T>;
 }
 // The generated goal is:
 // ```
 // forall<T> {
 //     WellFormed(i32: Foo) &&
 //        WellFormed(OnlyClone<T>)
 // }
 // ```
 // however `WellFormed(OnlyClone<T>)` is not provable because it requires
 // `Implemented(T: Clone)`. It would be tempting to just add a `where T: Clone`
 // bound inside the `impl Foo for i32` block, however we saw that it was
 // illegal to add where clauses that didn't come from the trait definition.
 ```