expand reorder topic list slightly

src/SUMMARY.md

@@ -22,8 +22,8 @@
     - [Caching subtleties](./trait-caching.md)
     - [Specialization](./trait-specialization.md)
 - [Trait solving (new-style)](./traits.md)    
-    - [Canonicalization](./traits-canonicalization.md)
     - [Lowering to logic](./traits-lowering-to-logic.md)
+    - [Canonical queries](./traits-canonicalization.md)
     - [Goals and clauses](./traits-goals-and-clauses.md)
     - [Lowering rules](./traits-lowering-rules.md)
     - [Equality and associated types](./traits-associated-types.md)

src/traits-canonicalization.md

@@ -24,8 +24,9 @@ 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
+the same answer. That answer will be expressed in terms of the
-involved.
+canonical variables (`?0`, `?1`), which we can then map back to the
+original variables (`?T`, `?U`).
 
 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.

src/traits.md

@@ -13,11 +13,21 @@ instructions for getting involved in the
 
 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.
+  - The [goals and clauses](./traits-goals-and-clauses.html) chapter
+    describes the precise lowering rules we use.
+- [Canonical queries](./traits-canonicalization.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](./traits-associated-types.html), which is the
+  technique we use to accommodate associated types when figuring out
+  whether types are equal.
+- [Region constraints](./traits-regions.md), 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.
   
-*more to come*
+Note: this is not a complete list of topics. See the sidebar for more.