From a10a29a33fcf8efd1c3ba0cb6bb70615cdeac405 Mon Sep 17 00:00:00 2001 From: lcnr Date: Thu, 21 Mar 2024 17:07:59 +0100 Subject: [PATCH] explore significant changes with the new solver --- src/solve/significant-changes.md | 109 +++++++++++++++++++++++++++++++ 1 file changed, 109 insertions(+) create mode 100644 src/solve/significant-changes.md diff --git a/src/solve/significant-changes.md b/src/solve/significant-changes.md new file mode 100644 index 00000000..a42606ca --- /dev/null +++ b/src/solve/significant-changes.md @@ -0,0 +1,109 @@ +## Significant changes and quirks + +While some of the items below are already mentioned separately, this page tracks the +main changes from the old trait system implementation. This also mentions some ways +in which the solver significantly diverges from an idealized implementation. This +document simplifies and ignores edge cases. It is recommended to add an implicit +"mostly" to each statement. + +### Canonicalization + +The new solver uses [canonicalization] when evaluating nested goals. In case there +are possibly multiple candidates, each candidate is eagerly canonicalized. We then +attempt to merge their canonical responses. This differs from the old implementation +which does not use canonicalization inside of the trait system. + +This has a some major impacts on the design of both solvers. Without using +canonicalization to stash the constraints of candidates, candidate selection has +to discard the constraints of each candidate, only applying the constraints by +reevaluating the candidate after it has been selected: [source][evaluate_stack]. +Without canonicalization it is also not possible to cache the inference constraints +from evaluating a goal. This causes the old implementation to have two systems: +*evaluate* and *fulfill*. *Evaluation* is cached, does not apply inference constraints +and is used when selecting candidates. *Fulfillment* applies inference and region +constraints is not cached and applies inference constraints. + +By using canonicalization, the new implementation is able to merge *evaluation* and +*fulfillment*, avoiding complexity and subtle differences in behavior. It greatly +simplifies caching and prevents accidentally relying on untracked information. +It allows us to avoid reevaluating candidates after selection and enables us to merge +the responses of multiple candidates. However, canonicalizing goals during evaluation +forces the new implementation to use a fixpoint algorithm when encountering cycles +during trait solving: [source][cycle-fixpoint]. + +[canoncalization]: ./canonicalization.md +[evaluate_stack]: https://github.com/rust-lang/rust/blob/47dd709bedda8127e8daec33327e0a9d0cdae845/compiler/rustc_trait_selection/src/traits/select/mod.rs#L1232-L1237 +[cycle-fixpoint]: https://github.com/rust-lang/rust/blob/df8ac8f1d74cffb96a93ae702d16e224f5b9ee8c/compiler/rustc_trait_selection/src/solve/search_graph.rs#L382-L387 + +### Deferred alias equality + +The new implementation emits `AliasRelate` goals when relating aliases while the +old implementation structurally relates the aliases instead. This enables the +new solver to stall equality until it is able to normalize the related aliases. + +The behavior of the old solver is incomplete and relies on eager normalization +which replaces ambiguous aliases with inference variables. As this is not +not possible for aliases containing bound variables, the old implementation does +nto handle aliases inside of binders correctly, e.g. [#102048]. See the chapter on +[normalization] for more details. + +[#102048]: https://github.com/rust-lang/rust/issues/102048 + +### Eagerly evaluating nested goals + +The new implementation eagerly handles nested goals instead of returning +them to the caller. The old implementation does both. In evaluation nested +goals [are eagerly handled][eval-nested], while fulfillment simply +[returns them for later processing][fulfill-nested]. + +As the new implementation has to be able to eagerly handle nested goals for +candidate selection, always doing so reduces complexity. It may also enable +us to merge more candidates in the future. + +[eval-nested]: https://github.com/rust-lang/rust/blob/master/compiler/rustc_trait_selection/src/traits/select/mod.rs#L1271-L1277 +[fulfill-nested]: https://github.com/rust-lang/rust/blob/df8ac8f1d74cffb96a93ae702d16e224f5b9ee8c/compiler/rustc_trait_selection/src/traits/fulfill.rs#L708-L712 + +### Nested goals are evaluated until reaching a fixpoint + +The new implementation always evaluates goals in a loop until reachin a fixpoint. +The old implementation only does so in *fulfillment*, but not in *evaluation*. +Always doing so strengthens inference and is reduces the order dependence of +the trait solver. See [trait-system-refactor-initiative#102]. + +[trait-system-refactor-initiative#102]: https://github.com/rust-lang/trait-system-refactor-initiative/issues/102 + +### Proof trees and providing diagnostics information + +The new implementation does not track diagnostics information directly, +instead providing [proof trees][trees] which are used to lazily compute the +relevant information. This is not yet fully fleshed out and somewhat hacky. +The goal is to avoid tracking this information in the happy path to improve +performance and to avoid accidentally relying on diagnostics data for behavior. + +[trees]: ./proof-trees.md + +## Major quirks of the new implementation + +### Hiding impls if there are any env candidates + +If there is at least one `ParamEnv` or `AliasBound` candidate to prove +some `Trait` goal, we discard all impl candidates for both `Trait` and +`Projection` goals: [source][discard-from-env]. This prevents users from +using an impl which is entirely covered by a `where`-bound, matching the +behavior of the old implementation and avoiding some weird errors, +e.g. [trait-system-refactor-initiative#76]. + +[discard-from-env]: https://github.com/rust-lang/rust/blob/03994e498df79aa1f97f7bbcfd52d57c8e865049/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L785-L789 +[trait-system-refactor-initiative#76]: https://github.com/rust-lang/trait-system-refactor-initiative/issues/76 + +### `NormalizesTo` goals are a function + +See the [normalizaton] chapter. We replace the expected term with an unconstrained +inference variable before computing `NormalizesTo` goals to prevent it from affecting +normalization. This means that `NormalizesTo` goals are handled somewhat differently +from all other goal kinds and need some additional solver support. Most notably, +their ambiguous nested goals are returned to the caller which then evaluates them. +See [#122687] for more details. + +[#122687]: https://github.com/rust-lang/rust/pull/122687 +[normalization]: ./normalization.md \ No newline at end of file