work on traits chapters

Author: nikomatsakis

Diff for: src/SUMMARY.md

@@ -17,10 +17,19 @@
 - [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 solving (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)
+    - [Well-formedness checking](./traits-wf.md)
+    - [Bibliography](./traits-bibliography.md)
 - [Type checking](./type-checking.md)
 - [The MIR (Mid-level IR)](./mir.md)
     - [MIR construction](./mir-construction.md)

Diff for: 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

Diff for: 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)
+

Diff for: 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/

Diff for: 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.)
+