Merge pull request #219 from tmandry/reorg-traits

Traits chapter cleanup

src/SUMMARY.md

@@ -39,11 +39,11 @@
       - [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)
-    - [Lowering rules](./traits/lowering-rules.md)
-      - [The lowering module in rustc](./traits/lowering-module.md)
-    - [Well-formedness checking](./traits/wf.md)
     - [The SLG solver](./traits/slg.md)
     - [An Overview of Chalk](./traits/chalk-overview.md)
     - [Bibliography](./traits/bibliography.md)

src/traits/associated-types.md

@@ -5,7 +5,7 @@ associated types. The full system consists of several moving parts,
 which we will introduce one by one:
 
 - Projection and the `Normalize` predicate
-- Skolemization
+- Placeholder associated type projections
 - The `ProjectionEq` predicate
 - Integration with unification
 
@@ -14,11 +14,11 @@ which we will introduce one by one:
 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.)
+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
 
@@ -41,10 +41,11 @@ 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`.
+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
@@ -60,9 +61,8 @@ forall<T> {
 
 where in this case, the one `Implemented` condition is always true.
 
-(An aside: since we do not permit quantification over traits, this is
-really more like a family of program clauses, one for each associated
-type.)
+> 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.
@@ -76,17 +76,18 @@ normalized. For example, consider this function:
 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.
+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
@@ -106,9 +107,10 @@ placeholder associated types (see the `TypeName` enum declared in
 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;
-- **placeholder** associated types can be used when we don't.
+- 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:
@@ -151,16 +153,16 @@ 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
+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 (un-placeholder!) associated type
+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)
+> 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/index.md

@@ -1,17 +1,26 @@
 # 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].) 🚧
+> 🚧 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
 
-Trait solving is based around a few key ideas:
+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.
@@ -19,30 +28,36 @@ Trait solving is based around a few key ideas:
     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.
-- [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 thet type checker.
   
-Note: this is not a complete list of topics. See the sidebar for more.
+> 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:
-* The [chalk][chalk] repository is where we experiment with new ideas and
-  designs for the trait system. It basically consists of a unit testing framework
-  for the correctness and feasibility of the logical rules defining the new-style
-  trait system. It also provides the [`chalk_engine`][chalk_engine] crate, which
-  defines the new-style trait solver used both in the unit testing framework and
-  in 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**. 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-nursery/chalk
 [chalk_engine]: https://github.com/rust-lang-nursery/chalk/tree/master/chalk-engine

src/traits/regions.md

@@ -1,3 +1,9 @@
 # Region constraints
 
-*to be written*
+*To be written.*
+
+Chalk does not have the concept of region constraints, and as of this
+writing, work on rustc was not far enough to worry about them.
+
+In the meantime, you can read about region constraints in the
+[type inference](../type-inference.html#region-constraints) section.