fill out the borrowck chapter a bit more

src/borrow_check/region_inference.md

@@ -24,7 +24,7 @@ The MIR-based region analysis consists of two major functions:
 - [`compute_regions`], invoked second: this is given as argument the
   results of move analysis. It has the job of computing values for all
   the inference variables that `replace_regions_in_mir` introduced.
-  - To do that, it first runs the [MIR type checker](#mirtypeck). This
+  - To do that, it first runs the [MIR type checker]. This
     is basically a normal type-checker but specialized to MIR, which
     is much simpler than full Rust, of course. Running the MIR type
     checker will however create **outlives constraints** between
@@ -44,29 +44,26 @@ The MIR-based region analysis consists of two major functions:
 [`RegionInferenceContext`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html
 [`solve`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#method.solve
 [NLL RFC]: http://rust-lang.github.io/rfcs/2094-nll.html
+[MIR type checker]: ./type_check.md
 
 ## Universal regions
 
-*to be written* – explain the `UniversalRegions` type
+The [`UnversalRegions`] type represents a collection of _unversal_ regions
+corresponding to some MIR `DefId`. It is constructed in
+[`replace_regions_in_mir`] when we replace all regions with fresh inference
+variables. [`UniversalRegions`] contains indices for all the free regions in
+the given MIR along with any relationships that are _known_ to hold between
+them (e.g. implied bounds, where clauses, etc.).
 
-## Region variables and constraints
+TODO: is there more to write here?
 
-*to be written* – describe the `RegionInferenceContext` and
-the role of `liveness_constraints` vs other `constraints`, plus
+[`UniversalRegions`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/universal_regions/struct.UniversalRegions.html
 
-## Closures
+## Region variables
 
-*to be written*
-
-<a name="mirtypeck"></a>
-
-## The MIR type-check
-
-## Representing the "values" of a region variable
-
-The value of a region can be thought of as a **set**; we call the
-domain of this set a `RegionElement`. In the code, the value for all
-regions is maintained in
+The value of a region can be thought of as a **set** of points in the MIR where
+the region is valid; we call the domain of this set a `RegionElement`. In the
+code, the value for all regions is maintained in
 [the `rustc_mir::borrow_check::nll::region_infer` module][ri]. For
 each region we maintain a set storing what elements are present in its
 value (to make this efficient, we give each kind of element an index,
@@ -90,11 +87,86 @@ The kinds of region elements are as follows:
   for details on placeholders, see the section
   [placeholders and universes](#placeholder).
 
+## Constraints
+
+Before we can infer the value of regions, we need to collect constraints on the
+regions. There are two primary types of constraints.
+
+1. Outlives constraints. These are constraints that one region outlives another
+   (e.g. `'a: 'b`). Outlives constraints are generated by the [MIR type
+   checker].
+2. Liveness constraints. Each region needs to be live at points where it can be
+   used. These constraints are collected by [`generate_constraints`].
+
+[`generate_constraints`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/constraint_generation/fn.generate_constraints.html
+
+## Inference Overview
+
+So how do we compute the contents of a region? This process is called _region
+inference_. The high-level idea is pretty simple, but there are some details we
+need to take care of.
+
+The [`RegionInferenceContext`] type contains all of the information needed to
+do inference, including the universal regions from `replace_regions_in_mir` and
+the constraints computed for each region. It is constructed just after we
+compute the liveness constraints.
+
+Here are some of the fields of the struct:
+
+- `constraints`: contains all the outlives constraints.
+- `liveness_constraints`: contains all the liveness constraints.
+- `universal_regions`: contains the `UniversalRegions` returned by
+  `replace_regions_in_mir`.
+- `universal_region_relations`: contains relations known to be true about
+  universal regions. For example, if we have a where clause that `'a: 'b`, that
+  relation is assumed to be true while borrow checking the implementation (it
+  is checked at the caller), so `universal_region_relations` would contain `'a:
+  'b`.
+- `type_tests`: contains some constraints on types that we must check after
+  inference (e.g. `T: 'a`).
+- `closure_bounds_mapping`: used for propagating region constraints from
+  closures back out to the creater of the closure.
+
+TODO: should we discuss any of the others fields? What about the SCCs?
+
+Ok, now that we have constructed a `RegionInferenceContext`, we can do
+inference.  This is done by calling the [`solve`] method on the context.
+
+We will start off the value of each region with the liveness constraints (the
+places we already know must be in the region). We will then use the outlives
+constraints to widen each region until all constraints are met. This is done in
+[`propagate_constraints`]. For each region, if `'a: 'b`, we add all elements of
+`'b` to `'a`.
+
+Then, we will check for errors. We first check that type tests are satisfied by
+calling [`check_type_tests`]. This checks constraints like `T: 'a`. Second, we
+check that universal regions are not "too big". This is done by calling
+[`check_universal_regions`]. This checks that for each region `'a` if `'a`
+contains the element `end('b)`, then we must already know that `'a: 'b` holds
+(e.g. from a where clause). If we don't already know this, that is an error...
+well, almost.
+
+[`propagate_constraints`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#method.propagate_constraints
+[`check_type_tests`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#method.check_type_tests
+[`check_universal_regions`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#method.check_universal_regions
+
+## Closures
+
+When we are checking the type tests and universal regions, we may come across a
+constraint that we can't prove yet if we are in a closure body! However, the
+necessary constraints may actually hold (we just don't know it yet). Thus, if
+we are inside a closure, we just collect all the constraints we can't prove yet
+and return them. Later, when we are borrow check the MIR node that created the
+closure, we can also check that these constraints hold. At that time, if we
+can't prove they hold, we report an error.
+
 ## Causal tracking
 
 *to be written* – describe how we can extend the values of a variable
  with causal tracking etc
 
+TODO: is this what I described above or something else?
+
 <a name="placeholder"></a>
 
 ## Placeholders and universes
@@ -541,3 +613,6 @@ Now constraint propagation is done, but when we check the outlives
 relationships, we find that `V2` includes this new element `placeholder(1)`,
 so we report an error.
 
+## Borrow Checker Errors
+
+TODO: we should discuss how to generate errors from the results of these analyses.