Canonicalize root var when making response from new solver #108839

compiler-errors · 2023-03-07T04:49:44Z

During trait solving, if we equate two inference variables ?0 and ?1 but don't equate them with any rigid types, then InferCtxt::probe_ty_var will return Err for both of these. The canonicalizer code will then canonicalize the variables independently(!), and the response will not reflect the fact that these two variables have been made equal.

This hinders inference and I also don't think it's sound? I haven't thought too much about it past that, so let's talk about it.

r? @lcnr

compiler-errors · 2023-03-07T04:50:49Z

compiler/rustc_trait_selection/src/solve/mod.rs

@@ -238,6 +238,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
            && has_changed
            && !self.in_projection_eq_hack
            && !self.search_graph.in_cycle()
+            && false


Both of these UI tests I added in the PR fail here. That's because the inference guidance we applied from a Certainty::AMBIGUOUS response can make the goal pass the next time it's evaluated.

This seems like it's to be expected though, as long as we're returning canonical var values in ambiguous responses 🤔

shouldn't be, the issue again that the solver proves goals in sequence and doesn't reprove previous goals.

I guess disabling it for now is alright but I do want us to get to a point where we always internally keep reproving goals until we hit a fixpoint

compiler/rustc_trait_selection/src/solve/canonical/canonicalize.rs

lcnr · 2023-03-07T08:22:35Z

This hinders inference and I also don't think it's sound?

yeah, it's unsound. if you change the mirror example to not require ?0: Sized we drop the equality constraint. This example causes an ICE during mir typeck

trait Mirror {
    type Item: ?Sized;
}
impl<T: ?Sized> Mirror for *const T {
    type Item = T;
}

fn mirror<T>() -> T
where
    *const T: Mirror<Item = i32>,
{
    todo!()
}
fn mirror_reverse<T>(_: T)
where
    *const u32: Mirror<Item = T>,
{
}

fn main() {
    let x = mirror();
    mirror_reverse(x);
}

lcnr

yeah, this should affect the old canonicalization routine as well, but we don't use that with inference vars, at least not in soundness critical ways iirc. Ah well, would be good to fix if you want, r=me after adding this as a test regardless

rustbot · 2023-03-07T17:33:05Z

Some changes occurred to the core trait solver

cc @rust-lang/initiative-trait-system-refactor

compiler-errors · 2023-03-07T21:11:22Z

@bors r=lcnr

bors · 2023-03-07T21:11:24Z

📌 Commit 3bfcfd0 has been approved by lcnr

It is now in the queue for this repository.

…oot-var, r=lcnr Canonicalize root var when making response from new solver During trait solving, if we equate two inference variables `?0` and `?1` but don't equate them with any rigid types, then `InferCtxt::probe_ty_var` will return `Err` for both of these. The canonicalizer code will then canonicalize the variables independently(!), and the response will not reflect the fact that these two variables have been made equal. This hinders inference and I also don't think it's sound? I haven't thought too much about it past that, so let's talk about it. r? `@lcnr`

…iaskrgr Rollup of 8 pull requests Successful merges: - rust-lang#108754 (Retry `pred_known_to_hold_modulo_regions` with fulfillment if ambiguous) - rust-lang#108759 (1.41.1 supported 32-bit Apple targets) - rust-lang#108839 (Canonicalize root var when making response from new solver) - rust-lang#108856 (Remove DropAndReplace terminator) - rust-lang#108882 (Tweak E0740) - rust-lang#108898 (Set `LIBC_CHECK_CFG=1` when building Rust code in bootstrap) - rust-lang#108911 (Improve rustdoc-gui/tester.js code a bit) - rust-lang#108916 (Remove an unused return value in `rustc_hir_typeck`) Failed merges: r? `@ghost` `@rustbot` modify labels: rollup

…lcnr new solver: make all goal evaluation able to be automatically rerun It is generally wrong to call `evaluate_goal` multiple times or `evaluate_goal` and `evaluate_all` for the same `QueryResult` without correctly handling rerunning the goals when inference makes progress. Not doing so will result in the assertion in `evaluate_goal` firing because rerunning the goal will lead to a more accurate `QueryResult`. Currently there are lots of places that get this wrong and generally it is complex and error prone to handle correctly everywhere. This PR introduces a way to add goals to the `EvalCtxt` and then run all the added goals in a loop so that `evaluate_goal`/`evaluate_all` is not necessary to call manually. There are a few complications for making everything work "right": 1. the `normalizes-to` hack that replaces the rhs with an unconstrained infer var requires special casing in the new `try_evaluate_added_goals` function similar to how `evaluate_goal`'s assertion special cases that hack. 2. `assemble_candidates_after_normalizing_self_ty`'s normalization step needs to be reran for each candidate otherwise the found candidates will potentially get a more accurate `QueryResult` when rerunning the projection/trait goal which can effect the `QueryResult` of the projection/trait goal. This is implemented via `EvalCtxt::probe`'s closure's `EvalCtxt` inheriting the added goals of the `EvalCtxt` that `probe` is called on, allowing us to add goals in a probe, and then enter a nested probe for each candidate and evaluate added goals which include the normalization step's goals. I made `make_canonical_response` evaluate added goals so that it will be hard to mess up the impl of the solver by forgetting to evaluate added goals. Right now the only way to mess this up would be to call `response_no_constraints` (which from the name is obviously weird). The visibility of `evaluate_goal` means that it can be called from various `compute_x_goal` or candidate assembly functions, this is generally wrong and we should never call `evaluate_goal` manually, instead we should be calling `add_goal`/`add_goals`. This is solved by moving `evaluate_goal` `evaluate_canonical_goal` and `compute_goal` into `eval_ctxt`'s module and making them private so they cannot be called from elsewhere, forcing people to call `add_goal/s` and `evaluate_added_goals_and_make_canonical_resposne`/`try_evaluate_added_goals` --- Other changes: - removed the `&& false` that was introduced to the assertion in `evaluate_goal` in rust-lang#108839 - remove a `!self.did_overflow()` requirement in `search_graph.is_empty()` which causes goals that overflow to ICE - made `EvalCtxt::eq` take `&mut self` and add all the nested goals via `add_goals` instead of returning them as 99% of call sites just immediately called `EvalCtxt::add_goals` manually. r? `@lcnr`

…lcnr new solver: make all goal evaluation able to be automatically rerun It is generally wrong to call `evaluate_goal` multiple times or `evaluate_goal` and `evaluate_all` for the same `QueryResult` without correctly handling rerunning the goals when inference makes progress. Not doing so will result in the assertion in `evaluate_goal` firing because rerunning the goal will lead to a more accurate `QueryResult`. Currently there are lots of places that get this wrong and generally it is complex and error prone to handle correctly everywhere. This PR introduces a way to add goals to the `EvalCtxt` and then run all the added goals in a loop so that `evaluate_goal`/`evaluate_all` is not necessary to call manually. There are a few complications for making everything work "right": 1. the `normalizes-to` hack that replaces the rhs with an unconstrained infer var requires special casing in the new `try_evaluate_added_goals` function similar to how `evaluate_goal`'s assertion special cases that hack. 2. `assemble_candidates_after_normalizing_self_ty`'s normalization step needs to be reran for each candidate otherwise the found candidates will potentially get a more accurate `QueryResult` when rerunning the projection/trait goal which can effect the `QueryResult` of the projection/trait goal. This is implemented via `EvalCtxt::probe`'s closure's `EvalCtxt` inheriting the added goals of the `EvalCtxt` that `probe` is called on, allowing us to add goals in a probe, and then enter a nested probe for each candidate and evaluate added goals which include the normalization step's goals. I made `make_canonical_response` evaluate added goals so that it will be hard to mess up the impl of the solver by forgetting to evaluate added goals. Right now the only way to mess this up would be to call `response_no_constraints` (which from the name is obviously weird). The visibility of `evaluate_goal` means that it can be called from various `compute_x_goal` or candidate assembly functions, this is generally wrong and we should never call `evaluate_goal` manually, instead we should be calling `add_goal`/`add_goals`. This is solved by moving `evaluate_goal` `evaluate_canonical_goal` and `compute_goal` into `eval_ctxt`'s module and making them private so they cannot be called from elsewhere, forcing people to call `add_goal/s` and `evaluate_added_goals_and_make_canonical_resposne`/`try_evaluate_added_goals` --- Other changes: - removed the `&& false` that was introduced to the assertion in `evaluate_goal` in rust-lang#108839 - remove a `!self.did_overflow()` requirement in `search_graph.is_empty()` which causes goals that overflow to ICE - made `EvalCtxt::eq` take `&mut self` and add all the nested goals via `add_goals` instead of returning them as 99% of call sites just immediately called `EvalCtxt::add_goals` manually. r? ``@lcnr``

…lcnr new solver: make all goal evaluation able to be automatically rerun It is generally wrong to call `evaluate_goal` multiple times or `evaluate_goal` and `evaluate_all` for the same `QueryResult` without correctly handling rerunning the goals when inference makes progress. Not doing so will result in the assertion in `evaluate_goal` firing because rerunning the goal will lead to a more accurate `QueryResult`. Currently there are lots of places that get this wrong and generally it is complex and error prone to handle correctly everywhere. This PR introduces a way to add goals to the `EvalCtxt` and then run all the added goals in a loop so that `evaluate_goal`/`evaluate_all` is not necessary to call manually. There are a few complications for making everything work "right": 1. the `normalizes-to` hack that replaces the rhs with an unconstrained infer var requires special casing in the new `try_evaluate_added_goals` function similar to how `evaluate_goal`'s assertion special cases that hack. 2. `assemble_candidates_after_normalizing_self_ty`'s normalization step needs to be reran for each candidate otherwise the found candidates will potentially get a more accurate `QueryResult` when rerunning the projection/trait goal which can effect the `QueryResult` of the projection/trait goal. This is implemented via `EvalCtxt::probe`'s closure's `EvalCtxt` inheriting the added goals of the `EvalCtxt` that `probe` is called on, allowing us to add goals in a probe, and then enter a nested probe for each candidate and evaluate added goals which include the normalization step's goals. I made `make_canonical_response` evaluate added goals so that it will be hard to mess up the impl of the solver by forgetting to evaluate added goals. Right now the only way to mess this up would be to call `response_no_constraints` (which from the name is obviously weird). The visibility of `evaluate_goal` means that it can be called from various `compute_x_goal` or candidate assembly functions, this is generally wrong and we should never call `evaluate_goal` manually, instead we should be calling `add_goal`/`add_goals`. This is solved by moving `evaluate_goal` `evaluate_canonical_goal` and `compute_goal` into `eval_ctxt`'s module and making them private so they cannot be called from elsewhere, forcing people to call `add_goal/s` and `evaluate_added_goals_and_make_canonical_resposne`/`try_evaluate_added_goals` --- Other changes: - removed the `&& false` that was introduced to the assertion in `evaluate_goal` in rust-lang#108839 - remove a `!self.did_overflow()` requirement in `search_graph.is_empty()` which causes goals that overflow to ICE - made `EvalCtxt::eq` take `&mut self` and add all the nested goals via `add_goals` instead of returning them as 99% of call sites just immediately called `EvalCtxt::add_goals` manually. r? ```@lcnr```

…lcnr new solver: make all goal evaluation able to be automatically rerun It is generally wrong to call `evaluate_goal` multiple times or `evaluate_goal` and `evaluate_all` for the same `QueryResult` without correctly handling rerunning the goals when inference makes progress. Not doing so will result in the assertion in `evaluate_goal` firing because rerunning the goal will lead to a more accurate `QueryResult`. Currently there are lots of places that get this wrong and generally it is complex and error prone to handle correctly everywhere. This PR introduces a way to add goals to the `EvalCtxt` and then run all the added goals in a loop so that `evaluate_goal`/`evaluate_all` is not necessary to call manually. There are a few complications for making everything work "right": 1. the `normalizes-to` hack that replaces the rhs with an unconstrained infer var requires special casing in the new `try_evaluate_added_goals` function similar to how `evaluate_goal`'s assertion special cases that hack. 2. `assemble_candidates_after_normalizing_self_ty`'s normalization step needs to be reran for each candidate otherwise the found candidates will potentially get a more accurate `QueryResult` when rerunning the projection/trait goal which can effect the `QueryResult` of the projection/trait goal. This is implemented via `EvalCtxt::probe`'s closure's `EvalCtxt` inheriting the added goals of the `EvalCtxt` that `probe` is called on, allowing us to add goals in a probe, and then enter a nested probe for each candidate and evaluate added goals which include the normalization step's goals. I made `make_canonical_response` evaluate added goals so that it will be hard to mess up the impl of the solver by forgetting to evaluate added goals. Right now the only way to mess this up would be to call `response_no_constraints` (which from the name is obviously weird). The visibility of `evaluate_goal` means that it can be called from various `compute_x_goal` or candidate assembly functions, this is generally wrong and we should never call `evaluate_goal` manually, instead we should be calling `add_goal`/`add_goals`. This is solved by moving `evaluate_goal` `evaluate_canonical_goal` and `compute_goal` into `eval_ctxt`'s module and making them private so they cannot be called from elsewhere, forcing people to call `add_goal/s` and `evaluate_added_goals_and_make_canonical_resposne`/`try_evaluate_added_goals` --- Other changes: - removed the `&& false` that was introduced to the assertion in `evaluate_goal` in rust-lang#108839 - remove a `!self.did_overflow()` requirement in `search_graph.is_empty()` which causes goals that overflow to ICE - made `EvalCtxt::eq` take `&mut self` and add all the nested goals via `add_goals` instead of returning them as 99% of call sites just immediately called `EvalCtxt::add_goals` manually. r? ````@lcnr````

…lcnr new solver: make all goal evaluation able to be automatically rerun It is generally wrong to call `evaluate_goal` multiple times or `evaluate_goal` and `evaluate_all` for the same `QueryResult` without correctly handling rerunning the goals when inference makes progress. Not doing so will result in the assertion in `evaluate_goal` firing because rerunning the goal will lead to a more accurate `QueryResult`. Currently there are lots of places that get this wrong and generally it is complex and error prone to handle correctly everywhere. This PR introduces a way to add goals to the `EvalCtxt` and then run all the added goals in a loop so that `evaluate_goal`/`evaluate_all` is not necessary to call manually. There are a few complications for making everything work "right": 1. the `normalizes-to` hack that replaces the rhs with an unconstrained infer var requires special casing in the new `try_evaluate_added_goals` function similar to how `evaluate_goal`'s assertion special cases that hack. 2. `assemble_candidates_after_normalizing_self_ty`'s normalization step needs to be reran for each candidate otherwise the found candidates will potentially get a more accurate `QueryResult` when rerunning the projection/trait goal which can effect the `QueryResult` of the projection/trait goal. This is implemented via `EvalCtxt::probe`'s closure's `EvalCtxt` inheriting the added goals of the `EvalCtxt` that `probe` is called on, allowing us to add goals in a probe, and then enter a nested probe for each candidate and evaluate added goals which include the normalization step's goals. I made `make_canonical_response` evaluate added goals so that it will be hard to mess up the impl of the solver by forgetting to evaluate added goals. Right now the only way to mess this up would be to call `response_no_constraints` (which from the name is obviously weird). The visibility of `evaluate_goal` means that it can be called from various `compute_x_goal` or candidate assembly functions, this is generally wrong and we should never call `evaluate_goal` manually, instead we should be calling `add_goal`/`add_goals`. This is solved by moving `evaluate_goal` `evaluate_canonical_goal` and `compute_goal` into `eval_ctxt`'s module and making them private so they cannot be called from elsewhere, forcing people to call `add_goal/s` and `evaluate_added_goals_and_make_canonical_resposne`/`try_evaluate_added_goals` --- Other changes: - removed the `&& false` that was introduced to the assertion in `evaluate_goal` in rust-lang#108839 - remove a `!self.did_overflow()` requirement in `search_graph.is_empty()` which causes goals that overflow to ICE - made `EvalCtxt::eq` take `&mut self` and add all the nested goals via `add_goals` instead of returning them as 99% of call sites just immediately called `EvalCtxt::add_goals` manually. r? `````@lcnr`````

rustbot assigned lcnr Mar 7, 2023

compiler-errors commented Mar 7, 2023

View reviewed changes

lcnr reviewed Mar 7, 2023

View reviewed changes

compiler/rustc_trait_selection/src/solve/canonical/canonicalize.rs Outdated Show resolved Hide resolved

lcnr reviewed Mar 7, 2023

View reviewed changes

compiler-errors added 2 commits March 7, 2023 17:11

Canonicalize the ROOT VAR

8d13454

fix var equality issue with old canonicalizer

3bfcfd0

compiler-errors force-pushed the canonicalize-the-root-var branch from 2dc5b2d to 9bc37c3 Compare March 7, 2023 17:33

rustbot added T-compiler Relevant to the compiler team, which will review and decide on the PR/issue. WG-trait-system-refactor The Rustc Trait System Refactor Initiative labels Mar 7, 2023

compiler-errors force-pushed the canonicalize-the-root-var branch from 9bc37c3 to 3bfcfd0 Compare March 7, 2023 21:09

bors added the S-waiting-on-bors Status: Waiting on bors to run and complete tests. Bors will change the label on completion. label Mar 7, 2023

GuillaumeGomez mentioned this pull request Mar 8, 2023

Rollup of 10 pull requests #108904

Closed

matthiaskrgr mentioned this pull request Mar 8, 2023

Rollup of 8 pull requests #108920

Merged

bors merged commit 2428083 into rust-lang:master Mar 9, 2023

rustbot added this to the 1.70.0 milestone Mar 9, 2023

BoxyUwU mentioned this pull request Mar 9, 2023

new solver: make all goal evaluation able to be automatically rerun #108896

Merged

compiler-errors deleted the canonicalize-the-root-var branch August 11, 2023 19:56

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Canonicalize root var when making response from new solver #108839

Canonicalize root var when making response from new solver #108839

compiler-errors commented Mar 7, 2023

compiler-errors Mar 7, 2023 •

edited

Loading

lcnr Mar 7, 2023

lcnr commented Mar 7, 2023

lcnr left a comment •

edited

Loading

rustbot commented Mar 7, 2023

compiler-errors commented Mar 7, 2023

bors commented Mar 7, 2023

Canonicalize root var when making response from new solver #108839

Canonicalize root var when making response from new solver #108839

Conversation

compiler-errors commented Mar 7, 2023

compiler-errors Mar 7, 2023 • edited Loading

Choose a reason for hiding this comment

lcnr Mar 7, 2023

Choose a reason for hiding this comment

lcnr commented Mar 7, 2023

lcnr left a comment • edited Loading

Choose a reason for hiding this comment

rustbot commented Mar 7, 2023

compiler-errors commented Mar 7, 2023

bors commented Mar 7, 2023

compiler-errors Mar 7, 2023 •

edited

Loading

lcnr left a comment •

edited

Loading