diff --git a/src/traits/chalk-overview.md b/src/traits/chalk-overview.md
index 4abe0ac0..5e0f147c 100644
--- a/src/traits/chalk-overview.md
+++ b/src/traits/chalk-overview.md
@@ -55,7 +55,7 @@ Next we'll go through each stage required to produce the output above.
 
 [chalk-tests]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L115
 
-### Parsing
+### 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
@@ -71,11 +71,23 @@ 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.
 
-### Lowering
+### Rust Intermediate Representation ([rust_ir])
 
-After parsing, there is a "lowering" phase. This aims to convert traits/impls
-into "program clauses". A [`ProgramClause` (source code)][programclause] is
-essentially one of the following:
+After getting the AST we convert it to a more convenient intermediate
+representation called [`rust_ir`][rust_ir]. This is sort of analogous to the
+[HIR] in Rust. The process of converting to IR is called *lowering*.
+
+The [`rust_ir::Program`][rust_ir-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
+`rust_ir::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 && ...`
@@ -93,8 +105,8 @@ essentially one of the following:
 
 *See also: [Goals and Clauses][goals-and-clauses]*
 
-Lowering is the phase where we encode the rules of the trait system into logic.
-For example, if we have the following Rust:
+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> {}
@@ -109,54 +121,61 @@ 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 [`rust_ir::Program`][rust_ir-program] which has "rust-like
+things", chalk_ir defines [`ProgramEnvironment`] which which is "pure logic".
+The main field in that struct is `program_clauses`, which contains the
+[`ProgramClause`]s generated by the rules module.
+
+#### Rules
+
+The `rules` module ([source code][rules-src]) 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]*
+
+[`ProgramEnvironment`]: https://rust-lang-nursery.github.io/chalk/doc/chalk_ir/struct.ProgramEnvironment.html
+[`ProgramClause`]: https://rust-lang-nursery.github.io/chalk/doc/chalk_ir/enum.ProgramClause.html
+[rules-src]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules.rs
+
 #### Well-formedness checks
 
-As part of lowering from the AST to the internal IR, we also do some "well
-formedness" checks. See the [source code][well-formedness-checks] for where
-those are done. The call to `record_specialization_priorities` checks
-"coherence" which means that it ensures that two impls of the same trait for the
-same type cannot exist.
+As part of lowering to logic, we also do some "well formedness" checks. See
+the [`rules::wf` source code][rules-wf-src] for where those are done.
 
-### Intermediate Representation (IR)
+*See also: [Well-formedness checking][wf-checking]*
 
-The second intermediate representation in chalk is called, well, the "ir". :)
-The [IR source code][ir-code] contains the complete definition. The
-`ir::Program` struct contains some "rust things" but indexed and accessible in
-a different way. This is sort of analogous to the [HIR] in Rust.
+[rules-wf-src]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules/wf.rs
 
-For example, if you have a type like `Foo<Bar>`, we would represent `Foo` as a
-string in the AST but in `ir::Program`, we use numeric indices (`ItemId`).
+#### Coherence
 
-In addition to `ir::Program` which has "rust-like things", there is also
-`ir::ProgramEnvironment` which is "pure logic". The main field in that struct is
-`program_clauses` which contains the `ProgramClause`s that we generated
-previously.
+The function `record_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.
 
-### Rules
+[coherence-src]: https://github.com/rust-lang-nursery/chalk/blob/master/src/coherence.rs
 
-The `rules` module works by iterating over every trait, impl, etc. and emitting
-the rules that come from each one. See [Lowering Rules][lowering-rules] for the
-most up-to-date reference on that.
+### Solver ([chalk_solve])
 
-The `ir::ProgramEnvironment` is created [in this module][rules-environment].
+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*.
 
-### Solver
-
-See [The SLG Solver][slg].
+*See also: [The SLG Solver][slg]*
 
 ## Crates
 
 Chalk's functionality is broken up into the following crates:
 - [**chalk_engine**][doc-chalk-engine]: Defines the core [SLG solver][slg].
-- [**chalk_ir**][doc-chalk-ir]: Defines chalk's internal representation of
+- [**chalk_ir**][chalk_ir]: Defines chalk's internal representation of
   types, lifetimes, and goals.
 - [**chalk_solve**][doc-chalk-solve]: Combines `chalk_ir` and `chalk_engine`,
   effectively.
   - [`chalk_engine::context`][engine-context] provides the necessary hooks.
-- [**chalk_parse**][doc-chalk-parse]: Defines the raw AST and a parser.
+- [**chalk_parse**][chalk_parse]: Defines the raw AST and a parser.
 - [**chalk**][doc-chalk]: Brings everything together. Defines the following
   modules:
-  - [`rust_ir`][doc-chalk-rust-ir], containing the "HIR-like" form of the AST
+  - [`rust_ir`][rust_ir], containing the "HIR-like" form of the AST
     - `rust_ir::lowering`, which converts AST to `rust_ir`
   - `rules`, which implements logic rules converting `rust_ir` to `chalk_ir`
   - `coherence`, which implements coherence rules
@@ -167,11 +186,12 @@ Chalk's functionality is broken up into the following crates:
 [engine-context]: https://rust-lang-nursery.github.io/chalk/doc/chalk_engine/context/index.html
 
 [doc-chalk-engine]: https://rust-lang-nursery.github.io/chalk/doc/chalk_engine/index.html
-[doc-chalk-ir]: https://rust-lang-nursery.github.io/chalk/doc/chalk_ir/index.html
+[chalk_ir]: https://rust-lang-nursery.github.io/chalk/doc/chalk_ir/index.html
 [doc-chalk-solve]: https://rust-lang-nursery.github.io/chalk/doc/chalk_solve/index.html
-[doc-chalk-parse]: https://rust-lang-nursery.github.io/chalk/doc/chalk_parse/index.html
+[chalk_parse]: https://rust-lang-nursery.github.io/chalk/doc/chalk_parse/index.html
 [doc-chalk]: https://rust-lang-nursery.github.io/chalk/doc/chalk/index.html
-[doc-chalk-rust-ir]: https://rust-lang-nursery.github.io/chalk/doc/chalk/rules/index.html
+[rust_ir]: https://rust-lang-nursery.github.io/chalk/doc/chalk/rust_ir/index.html
+[rust_ir-program]: https://rust-lang-nursery.github.io/chalk/doc/chalk/rust_ir/struct.Program.html
 [doc-chalki]: https://rust-lang-nursery.github.io/chalk/doc/chalki/index.html
 
 ## Testing
@@ -201,15 +221,14 @@ is the function that is ultimately called.
 [chalk]: https://github.com/rust-lang-nursery/chalk
 [lowering-to-logic]: ./lowering-to-logic.html
 [lowering-rules]: ./lowering-rules.html
+[wf-checking]: ./wf.html
 [ast]: https://en.wikipedia.org/wiki/Abstract_syntax_tree
 [chalk-ast]: https://github.com/rust-lang-nursery/chalk/blob/master/chalk-parse/src/ast.rs
 [universal quantification]: https://en.wikipedia.org/wiki/Universal_quantification
 [lowering-forall]: ./lowering-to-logic.html#type-checking-generic-functions-beyond-horn-clauses
-[programclause]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/ir.rs#L721
 [clause]: https://github.com/rust-lang-nursery/chalk/blob/master/GLOSSARY.md#clause
 [goals-and-clauses]: ./goals-and-clauses.html
-[well-formedness-checks]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/ir/lowering.rs#L230-L232
-[ir-code]: https://github.com/rust-lang-nursery/chalk/tree/master/chalk-ir
+[ir-code]: https://github.com/rust-lang-nursery/chalk/blob/master/src/rust_ir.rs
 [HIR]: ../hir.html
 [binders-struct]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/ir.rs#L661
 [rules-environment]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/rules.rs#L9