From e0a3f75523c6a6820520c647df014810e7519a9a Mon Sep 17 00:00:00 2001 From: lcnr Date: Mon, 13 Feb 2023 13:56:59 +0100 Subject: [PATCH 1/7] write canonicalization chapter first half --- src/solve/canonicalization.md | 76 ++++++++++++++++++++++++++++++++--- 1 file changed, 70 insertions(+), 6 deletions(-) diff --git a/src/solve/canonicalization.md b/src/solve/canonicalization.md index e34b13bec..596da5b42 100644 --- a/src/solve/canonicalization.md +++ b/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 necessary +for global caching of goals which include inference variables. - -As of 10 January 2023, canonicalization is not yet fully implemented -in the new solver. +The idea is that given the goals `u32: Trait` and `u32: Trait`, 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 u32: Trait` once +and reuse the result. -[chalk]: https://rust-lang.github.io/chalk/book/canonical_queries/canonicalization.html#canonicalization \ No newline at end of file +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` as an example and assume that this only holds +for `u32: Trait>` 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 u32: Trait`. + +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`. 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` and figure out that this holds, but we've constrained +`?0` to `Vec`. 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 Vec`. + +### 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`. + +It now equates the original value of `T` (`?x`) with the value for `T` in the +response (`Vec`), which correctly constrains `?x` to `Vec`. + +## `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 \ No newline at end of file From b85a45250d9d9efc4710fbb6b45d2dc6a345ae7f Mon Sep 17 00:00:00 2001 From: lcnr Date: Mon, 13 Feb 2023 13:58:29 +0100 Subject: [PATCH 2/7] w --- src/solve/canonicalization.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solve/canonicalization.md b/src/solve/canonicalization.md index 596da5b42..878067324 100644 --- a/src/solve/canonicalization.md +++ b/src/solve/canonicalization.md @@ -1,6 +1,6 @@ # Canonicalization -Canonicalization is the process of *isolating* a value from its context and necessary +Canonicalization is the process of *isolating* a value from its context and is necessary for global caching of goals which include inference variables. The idea is that given the goals `u32: Trait` and `u32: Trait`, where `?x` and `?y` From 47e03df6f5d42eb736b422189d9c693f8de738e3 Mon Sep 17 00:00:00 2001 From: lcnr Date: Mon, 13 Feb 2023 15:57:04 +0100 Subject: [PATCH 3/7] review --- src/solve/canonicalization.md | 21 ++++++++++----------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/src/solve/canonicalization.md b/src/solve/canonicalization.md index 878067324..4775efa53 100644 --- a/src/solve/canonicalization.md +++ b/src/solve/canonicalization.md @@ -30,8 +30,8 @@ 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. +To actually try to prove the canonical goal we start by instantiating the bound variables with +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`. We also remember which value we've used to instantiate the bound @@ -42,13 +42,12 @@ We now compute the goal `u32: Trait` and figure out that this holds, but we' ### 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. +We have to return to the caller has to know whether the goal holds and the inference constraints +from inside of the query. -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 Vec`. +To return the inference results to the caller 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 Vec`. ### Instantiating the query response @@ -65,9 +64,9 @@ Computing a trait goal may not only constrain inference variables, it can also a 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`. +This is done by not only returning the mapping from bound variables to the instantiated values +from the query but also extracting additional `ExternalConstraints` from the `InferCtxt` context +while building the response. ## How exactly does canonicalization work From 3eca414183228efa7564299639ea49ff802fb99e Mon Sep 17 00:00:00 2001 From: lcnr Date: Tue, 14 Feb 2023 16:20:47 +0100 Subject: [PATCH 4/7] very good section --- src/solve/canonicalization.md | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/solve/canonicalization.md b/src/solve/canonicalization.md index 4775efa53..235531fd4 100644 --- a/src/solve/canonicalization.md +++ b/src/solve/canonicalization.md @@ -70,4 +70,15 @@ while building the response. ## How exactly does canonicalization work -TODO \ No newline at end of file +TODO: link to code once the PR lands and elaborate + +- types and consts: infer to existentially bound var, placeholder to universally bound var, + considering universes +- generic parameters in the input get treated as placeholders in the root universe +- all regions in the input get all mapped to existentially bound vars and we "uniquify" them. + `T: Trait<'a, 'a>` gets canonicalized to `exists<'0, '1> T: Trait<'0, '1>`. We do not care + about their universes and simply put all regions into the highest universe of the input. +- once we collected all canonical vars we compress their universes, see comment in `finalize`. +- in the output everything in a universe of the caller gets put into the root universe and only + gets its correct universe when we unify the var values with the orig values of the caller +- we do not uniquify regions in the response and don't canonicalize `'static` \ No newline at end of file From 4d2e7e1bff7b60734f75c886af8fa19b079c0524 Mon Sep 17 00:00:00 2001 From: lcnr Date: Tue, 14 Feb 2023 16:21:54 +0100 Subject: [PATCH 5/7] whatever --- src/solve/canonicalization.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solve/canonicalization.md b/src/solve/canonicalization.md index 235531fd4..b248fd906 100644 --- a/src/solve/canonicalization.md +++ b/src/solve/canonicalization.md @@ -76,7 +76,7 @@ TODO: link to code once the PR lands and elaborate considering universes - generic parameters in the input get treated as placeholders in the root universe - all regions in the input get all mapped to existentially bound vars and we "uniquify" them. - `T: Trait<'a, 'a>` gets canonicalized to `exists<'0, '1> T: Trait<'0, '1>`. We do not care + `&'a (): Trait<'a>` gets canonicalized to `exists<'0, '1> &'0 (): Trait<'1>`. We do not care about their universes and simply put all regions into the highest universe of the input. - once we collected all canonical vars we compress their universes, see comment in `finalize`. - in the output everything in a universe of the caller gets put into the root universe and only From 6cb94c75bc1aa663cdf1a4beb6c5b1226892ab58 Mon Sep 17 00:00:00 2001 From: lcnr Date: Mon, 20 Feb 2023 15:28:14 +0100 Subject: [PATCH 6/7] review --- src/solve/canonicalization.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solve/canonicalization.md b/src/solve/canonicalization.md index b248fd906..36ad7630c 100644 --- a/src/solve/canonicalization.md +++ b/src/solve/canonicalization.md @@ -42,7 +42,7 @@ We now compute the goal `u32: Trait` and figure out that this holds, but we' ### Canonicalizing the query response -We have to return to the caller has to know whether the goal holds and the inference constraints +We have to return to the caller both whether the goal holds, and the inference constraints from inside of the query. To return the inference results to the caller we canonicalize the mapping from bound variables From cf8f9c3bc229c68cae704eb7a350ea242720d1fe Mon Sep 17 00:00:00 2001 From: lcnr Date: Mon, 20 Feb 2023 15:38:39 +0100 Subject: [PATCH 7/7] ok --- src/solve/canonicalization.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/solve/canonicalization.md b/src/solve/canonicalization.md index 36ad7630c..a14be5216 100644 --- a/src/solve/canonicalization.md +++ b/src/solve/canonicalization.md @@ -13,8 +13,8 @@ how canonicalization works. ## A walkthrough of canonical queries -We're going to use the goal `u32: Trait` as an example and assume that this only holds -for `u32: Trait>` where `?z` is unconstrained. +To make this a bit easier, let's use the trait goal `u32: Trait` as an example with the +assumption that the only relevant impl is `impl Trait> for u32`. ### Canonicalizing the input