work on traits chapters

Author: nikomatsakis

src/SUMMARY.md

@@ -17,10 +17,18 @@
 - [The HIR (High-level IR)](./hir.md)
 - [The `ty` module: representing types](./ty.md)
 - [Type inference](./type-inference.md)
-- [Trait resolution](./trait-resolution.md)
+- [Trait bsolving (old-style)](./trait-resolution.md)
     - [Higher-ranked trait bounds](./trait-hrtb.md)
     - [Caching subtleties](./trait-caching.md)
-    - [Speciailization](./trait-specialization.md)
+    - [Specialization](./trait-specialization.md)
+- [Trait solving (new-style)](./traits.md)    
+    - [Canonicalization](./traits-canonicalization.md)
+    - [Lowering to logic](./traits-lowering-to-logic.md)
+    - [Goals and clauses](./traits-goals-and-clauses.md)
+    - [Lowering rules](./traits-lowering-rules.md)
+    - [Equality and associated types](./traits-associated-types.md)
+    - [Region constraints](./traits-regions.md)
+    - [Bibliography](./traits-bibliography.md)
 - [Type checking](./type-checking.md)
 - [The MIR (Mid-level IR)](./mir.md)
     - [MIR construction](./mir-construction.md)

src/trait-resolution.md

@@ -1,8 +1,13 @@
-# Trait resolution
+# Trait resolution (old-style)
 
 This chapter describes the general process of _trait resolution_ and points out
 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 [the traits chapter](./traits.html).
+
 ## Major concepts
 
 Trait resolution is the process of pairing up an impl with each

src/traits-associated-types.md

@@ -0,0 +1,143 @@
+# 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
+- Skolemization
+- 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,
+though, 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.)
+
+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
+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 -- but 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:
+
+    forall<T> {
+        Normalize(<Option<T> as IntoIterator>::Item -> T)
+    }    
+    
+(An aside: since we do not permit quantification over traits, this is
+really more like a family of predicates, one for each associated
+type.)
+
+We could apply that rule to normalize either of the examples that
+we've seen so far.
+
+## Skolemized associated types
+
+Sometimes however we want to work with associated types that cannot be
+normalized. For example, consider this function:
+
+```rust
+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 **skolemized 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: skolemized 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.
+
+Skolemized associated types are never written directly by the user.
+They are used internally by the trait system only, as we will see
+shortly.
+
+## 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 associated type
+  projections when we knew which impl was applicable;
+- **skolemized** associated types can be used when we don't.
+
+We now introduce the `ProjectionEq` predicate to bring those two cases
+together. The `ProjectionEq` predicate looks like so:
+
+    ProjectionEq(<T as IntoIterator>::Item = U)
+    
+and we will see that it can be proven *either* via normalization or
+skolemization. As part of lowering an associated type declaration from
+some trait, we create two program clauses for `ProjectionEq`:
+
+    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:
+
+    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 an (unskolemized!) 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)
+

src/traits-bibliography.md

@@ -0,0 +1,28 @@
+# 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 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 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
+[ts]: http://www3.cs.stonybrook.edu/~tswift/

src/traits-canonicalization.md

@@ -0,0 +1,93 @@
+# Canonicalization
+
+Canonicalization is the process of **isolating** an inference value
+from its context. It 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 thing T from its environment, we just walk down and find the
+unbound variables that appear in T; those variables get renumbered in
+a canonical order (left to right, for the most part, but really it
+doesn't matter as long as it is consistent).
+
+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 canonicalize form, then they will get
+the same answer -- modulo the precise identities of the variables
+involved.
+
+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](./background.html#free-vs-bound) with a
+canonical variable. Therefore, we get the following result: 
+
+    ?0: Foo<'?1, ?2>
+    
+Sometimes we write this differently, like so:    
+
+    for<T,L,T> { ?0: Foo<'?1, ?2> }
+    
+This `for<>` gives some information about each of the canonical
+variables within.  In this case, I am saying that `?0` is a type
+(`T`), `?1` is a lifetime (`L`), and `?2` is also a type (`T`). The
+`canonicalize` method *also* gives back a `CanonicalVarValues` array
+with the "original values" for each canonicalized variable:
+
+    [?A, 'static, ?B]
+
+Now we do the query and get back some result R. As part of that
+result, we'll have an array of values for the canonical inputs. For
+example, the canonical result might be:
+
+```
+for<2> {
+    values = [ Vec<?0>, '1, ?0 ]
+                   ^^   ^^  ^^ these are variables in the result!
+    ...
+}
+```
+
+Note that this result is itself canonical and may include some
+variables (in this case, `?0`).
+
+What we want to do conceptually is to (a) instantiate each of the
+canonical variables in the result with a fresh inference variable
+and then (b) unify the values in the result with the original values.
+Doing step (a) would yield a result of
+
+```
+{
+    values = [ Vec<?C>, '?X, ?C ]
+                   ^^   ^^^ fresh inference variables in `self`
+    ..
+}
+```
+
+Step (b) would then unify:
+
+```
+?A with Vec<?C>
+'static with '?X
+?B with ?C
+```
+
+(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 we means we can deduce that `?C := ?B and
+`'?X := 'static`. This gives us a partial set of values. Anything for
+which we do not find a value, we create an inference variable.)
+

src/traits-goals-and-clauses.md

@@ -0,0 +1,148 @@
+# 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](./traits-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):
+
+    Goal = DomainGoal
+         | Goal && Goal
+         | Goal || Goal
+         | exists<K> { Goal }   // existential quantification
+         | forall<K> { Goal }   // universal quantification 
+         | if (Clause) { Goal } // implication
+
+    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.
+
+[pphhf]: ./traits-bibliography.html#pphhf
+
+<a name="domain-goals">
+
+## Domain goals
+
+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 allow with a suitable set of inputs P0..Pn:
+
+    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 **projection** consists of a an associated item reference along with
+its inputs P0..Pm:
+
+    Projection = <P0 as TraitName<P1..Pn>>::AssocItem<Pn+1..Pm>
+
+Given that, we can define a `DomainGoal` as follows:
+
+    DomainGoal = Implemented(TraitRef)
+               | ProjectionEq(Projection = Type)
+               | Normalize(Projection -> Type)
+               | FromEnv(TraitRef)
+               | FromEnv(Projection = Type)
+               | WellFormed(Type)
+               | WellFormed(TraitRef)
+               | WellFormed(Projection = Type)
+               | Outlives(Type, Region)
+               | Outlives(Region, Region)
+
+- `Implemented(TraitRef)` -- true if the given trait is
+  implemented for the given input types and lifetimes
+- `FromEnv(TraitEnv)` -- true if the given trait is *assumed* to be implemented;
+  that is, if it can be derived from the in-scope where clauses
+  - as we'll see in the section on lowering, `FromEnv(X)` implies
+    `Implemented(X)` but not vice versa. This distinction is crucial
+    to [implied bounds].
+- `ProjectionEq(Projection = Type)` -- the given associated type `Projection` is equal
+  to `Type`; see [the section on associated types](./traits-associated-types.html)
+- `Normalize(Projection -> Type)` -- the given associated type `Projection` can be normalized
+  to `Type`
+  - as discussed in [the section on associated types](./traits-associated-types.html),
+    `Normalize` implies `ProjectionEq` but not vice versa
+- `WellFormed(..)` -- these goals imply that the given item is
+  *well-formed*
+  - well-formedness is important to [implied bounds].
+
+<a name=coinductive>
+
+## Coinductive goals
+
+Most goals in our system are "inductive". In an inductive goal,
+circular reasoning is disallowed. Consider this example clause:
+
+    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
+
+    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]: ./traits-lowering-rules.html#implied-bounds
+
+## Incomplete chapter
+
+Some topics yet to be written:
+
+- Elaborate on the proof procedure
+- SLG solving -- introduce negative reasoning

src/traits-lowering-rules.md

@@ -0,0 +1,267 @@
+# Lowering rules
+
+This section gives the complete lowering rules for Rust traits into
+[program clauses][pc]. These rules reference the [domain goals][dg] defined in
+an earlier section.
+
+[pc]: ./traits-goals-and-clauses.html
+[dg]: ./traits-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 paramter 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](./traits-goals-and-clauses.html).
+We sometimes insert "macros" like `LowerWhereClause!` into these
+definitions; these macros reference other sections within this chapter.
+
+## Lowering where clauses
+
+When used in a goal position, where clauses can be mapped directly
+[domain goals][dg], as follows:
+
+- `A0: Foo<A1..An>` maps to `Implemented(A0: Foo<A1..An>)`.
+- `A0: Foo<A1..An, Item = T>` maps to `ProjectionEq(<A0 as Foo<A1..An>>::Item = T)`
+- `T: 'r` maps to `Outlives(T, 'r)`
+- `'a: 'b` maps to `Outlives('a, 'b)`
+
+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)`
+  - `ProjectionEq(Projection = Ty)` becomes `FromEnv(Projection = Ty)`
+  - other where-clauses are left intact
+- `WellFormed(WC)` -- this indicates that:
+  - `Implemented(TraitRef)` becomes `WellFormed(TraitRef)`
+  - `ProjectionEq(Projection = Ty)` becomes `WellFormed(Projection = Ty)`
+  
+*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
+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 dush
+rule from the trait header creates the mapping between the `FromEnv`
+and `Implemented` predicates:
+
+    forall<Self, P1..Pn> {
+      Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn)
+    }
+
+<a name="implied-bounds">
+
+#### Implied bounds
+
+The next few clauses have to do with implied bounds (see also
+[RFC 2089]). For each trait, we produce two clauses:
+
+[RFC 2089]: https://rust-lang.github.io/rfcs/2089-implied-bounds.html
+
+    // 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 it's where-clauses hold. It's perhaps useful to see an example:
+
+```rust
+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**:
+
+    // For each where clause WC:
+    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](./traits-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
+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 that `WellFormed(TraitRef)`. This in turn justifies the
+implied bounds rules that allow us to extend the set of `FromEnv`
+items.
+
+<a name=trait-items>
+
+## Lowering trait items
+
+### Associated type declarations
+
+Given a trait that declares a (possibly generic) associated type:
+
+```rust
+trait Trait<P1..Pn> // P0 == Self
+where WC
+{
+    type AssocType<Pn+1..Pm>: Bounds where WC1;
+}
+```
+
+We will produce a number of program clases. The first two define
+the rules by which `ProjectionEq` can succeed; these two clauses are discussed
+in detail in the [section on associated types](./traits-associated-types.html).
+
+    // 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)
+    }
+
+    // ProjectionEq can succeed by skolemizing:
+    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>
+      ) :-
+        // But only if the trait is implemented, and the conditions from
+        // the associated type are met as well:
+        Implemented(Self: Trait<P1..Pn>),
+        WC1
+    }
+    
+The next rule covers implied bounds for the projection. In particular,
+the `Bounds` declared on the associated type must be proven to hold to
+show that the impl is well-formed, and hence we can rely on them from
+elsewhere.
+
+    // XXX how exactly should we set this up? Have to be careful;
+    // presumably this has to be a kind of `FromEnv` setup.
+
+### 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
+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:
+
+    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
+impl<P0..Pn> Trait<A1..An> for A0
+where WC
+{
+    type AssocType<Pn+1..Pm>: Bounds where WC1 = T;
+}
+```
+
+We produce the following rule:
+
+    forall<P0..Pm> {
+      forall<Pn+1..Pm> {
+        Normalize(<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm> -> T) :-
+          WC, WC1
+      }
+    }
+  
+Note that `WC` and `WC1` both encode where-clauses that the impl can
+rely on, whereas the bounds `Bounds` on the associated type are things
+that the impl must prove (see the well-formedness checking).
+
+<a name=constant-vals>
+
+### 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.
+
+

src/traits-lowering-to-logic.md

@@ -0,0 +1,182 @@
+# 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:
+
+```
+Clone(usize).
+Clone(Vec<?T>) :- Clone(?T).
+```
+
+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 is 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
+trait Eq<T> { ... }
+impl Eq<usize> for usize { }
+impl<T: Eq<U>> Eq<Vec<U>> for Vec<T> { }
+```
+
+That could be mapped as follows:
+
+```
+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 interesting in how derive the goals
+that we need to prove, and those come from type-checking.
+
+Consider type-checking the function `foo()` here:
+
+```rust
+fn foo() { bar::<usize>() }
+fn bar<U: Eq>() { }
+```
+
+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`. So, that means that `foo()` will
+have to prove that `usize: Eq` 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":
+
+```
+barWellFormed(?U) :- Eq(?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:
+
+```
+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)`, 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 Prolog
+can be provide. To see what I'm talking about, let's revamp our previous
+example to make `foo` generic:
+
+```rust
+fn foo<T: Eq>() { bar::<T>() }
+fn bar<U: Eq>() { }
+```
+
+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:
+
+```
+fooTypeChecks :-
+  // for all types T...
+  forall<T> {
+    // ...if we assume that Eq(T) is provable...
+    if (Eq(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]: ./traits-bibliography.html
+[pphhf]: ./traits-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/

src/traits-regions.md

@@ -0,0 +1,3 @@
+# Region constraints
+
+*to be written*

src/traits.md

@@ -0,0 +1,18 @@
+# Trait solving (new-style)
+
+🚧 This chapter describes "new-style" trait solving. This is still in
+the process of being implemented; 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 chapter](./trait-resolution.html).🚧
+
+Trait solving is based around a few key ideas:
+
+- [Canonicalization](./traits-canonicalization.html), which allows us to
+  extract types that contain inference variables in them from their
+  inference context, work with them, and then bring the results back
+  into the original context.
+- [Lowering to logic](./traits-lowering-to-logic.html), which expresses
+  Rust traits in terms of standard logical terms.
+
+*more to come*

src/type-inference.md

@@ -43,6 +43,8 @@ The `tcx.infer_ctxt` method actually returns a build, which means
 there are some kinds of configuration you can do before the `infcx` is
 created. See `InferCtxtBuilder` for more information.
 
+<a name=vars>
+
 ## Inference variables
 
 The main purpose of the inference context is to house a bunch of