new solver: write canonicalization chapter

src/solve/canonicalization.md

@@ -1,10 +1,74 @@
 # Canonicalization
 
-While the exact approach to canonicalization for this solver will differ slightly
-wrt to lifetimes, please visit [the relevant chalk chapter][chalk] for now.
+Canonicalization is the process of *isolating* a value from its context and is necessary
+for global caching of goals which include inference variables.
 
-<!-- date-check: jan 2023 -->
-As of 10 January 2023,  canonicalization is not yet fully implemented
-in the new solver.
+The idea is that given the goals `u32: Trait<?x>` and `u32: Trait<?y>`, where `?x` and `?y`
+are two different currently unconstrained inference variables, we should get the same result
+for both goals. We can therefore prove *the canonical query* `exists<T> u32: Trait<T>` once
+and reuse the result.
 
-[chalk]: https://rust-lang.github.io/chalk/book/canonical_queries/canonicalization.html#canonicalization
+Let's first go over the way canonical queries work and then dive into the specifics of
+how canonicalization works.
+
+## A walkthrough of canonical queries
+
+We're going to use the goal `u32: Trait<?x>` as an example and assume that this only holds
+for `u32: Trait<Vec<?z>>` where `?z` is unconstrained.
+
+### Canonicalizing the input
+
+We start by *canonicalizing* the goal, replacing inference variables with existential and
+placeholders with universal bound variables. This would result in the *canonical goal*
+`exists<T> u32: Trait<T>`.
+
+We remember the original values of all bound variables in the original context. Here this would
+map `T` back to `?x`. These original values are used later on when dealing with the query
+response.
+
+We now call the canonical query with the canonical goal.
+
+### Instantiating the canonical goal inside of the query
+
+To actually try to prove the canonical goal we start by instantiating existential variables with
+inference variables and universal variables without inference variables and placeholders again.
+
+This happens inside of the query in a completely separate `InferCtxt`. Inside of the query we
+now have a goal `u32: Trait<?0>`. We also remember which value we've used to instantiate the bound
+variables in the canonical goal, which maps `T` to `?0`.
+
+We now compute the goal `u32: Trait<?0>` and figure out that this holds, but we've constrained
+`?0` to `Vec<?1>`. We finally convert this result to something useful to the caller.
+
+### Canonicalizing the query response
+
+The caller has to know both the result of the query and any inference constraints from inside
+of the query. The result is already context independent, so we can return that as is, we do have
+to canonicalize the inference constraints though.
+
+For this we canonicalize the mapping from bound variables to the instantiated values in the query.
+This means that the query response is `Certainty::Yes` and a mapping from `T` to
+`exists<U> Vec<U>`.
+
+### Instantiating the query response
+
+The caller now has to apply the constraints returned by the query. For this they first
+instantiate the bound variables of the canonical response with inference variables and
+placeholders again, so the mapping in the response is now from `T` to `Vec<?z>`.
+
+It now equates the original value of `T` (`?x`) with the value for `T` in the
+response (`Vec<?z>`), which correctly constrains `?x` to `Vec<?z>`.
+
+## `ExternalConstraints`
+
+Computing a trait goal may not only constrain inference variables, it can also add region
+obligations, e.g. given a goal `(): AOutlivesB<'a, 'b>` we would like to return the fact that
+`'a: 'b` has to hold.
+
+This is done by not only returning the canonical `var_values` from the query but also extracting
+additional `ExternalConstraints` from the inference context while building the response. These
+constraints get canonicalized together with the `var_values`.
+
+## How exactly does canonicalization work
+
+TODO