document difference between solvers + new solver normalization

src/solve/canonicalization.md

@@ -78,7 +78,6 @@ TODO: link to code once the PR lands and elaborate
 - all regions in the input get all mapped to existentially bound vars and we "uniquify" them.
     `&'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
     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`

src/solve/normalization.md

@@ -3,32 +3,82 @@
 With the new solver we've made some fairly significant changes to normalization when compared
 to the existing implementation.
 
-We now differentiate between "shallow normalization" and "deep normalization".
-"Shallow normalization" normalizes a type until it is no-longer a potentially normalizeable alias;
-it does not recurse into the type. "deep normalization" replaces all normalizeable aliases in a
-type with its underlying type.
-
-The old trait solver currently always deeply normalizes via `Projection` obligations.
-This is the only way to normalize in the old solver. By replacing projections with a new
-inference variable and then emitting `Projection(<T as Trait>::Assoc, ?new_infer)` the old
-solver successfully deeply normalizes even in the case of ambiguity. This approach does not
-work for projections referencing bound variables.
-
-## Inside of the trait solver
-
-Normalization in the new solver exclusively happens via `Projection`[^0] goals.
-This only succeeds by first normalizing the alias by one level and then equating
-it with the expected type. This differs from [the behavior of projection clauses]
-which can also be proven by successfully equating the projection without normalizating.
-This means that `Projection`[^0] goals must only be used in places where we
-*have to normalize* to make progress. To normalize `<T as Trait>::Assoc`, we first create
-a fresh inference variable `?normalized` and then prove
-`Projection(<T as Trait>::Assoc, ?normalized)`[^0]. `?normalized` is then constrained to
-the underlying type. 
-
-Inside of the trait solver we never deeply normalize. we only apply shallow normalization
-in [`assemble_candidates_after_normalizing_self_ty`] and inside for [`AliasRelate`]
-goals for the [`normalizes-to` candidates].
+We now differentiate between "one-step normalization", "structural normalization" and
+"deep normalization".
+
+## One-step normalization
+
+One-step normalization is implemented via `NormalizesTo` goals. Unlike other goals
+in the trait solver, `NormalizesTo` always expects the term to be an unconstrained
+inference variable[^opaques]. Think of it as a function, taking an alias as input
+and returning its underlying value. If the alias is rigid, `NormalizesTo` fails and
+returns `NoSolution`. This is the case for `<T as Trait>::Assoc` if there's a `T: Trait`
+where-bound and for opaque types with `Reveal::UserFacing` unless they are in the
+defining scope. We must not treat any aliases as rigid in coherence.
+
+The underlying value may itself be an unnormalized alias, e.g.
+`NormalizesTo(<<() as Id>::This as Id>::This)` only returns `<() as Id>::This`,
+even though that alias can be further normalized to `()`. As the term is
+always an unconstrained inference variable, the expected term cannot influence
+normalization, see [trait-system-refactor-initiative#22] for more.
+
+Only ever computing `NormalizesTo` goals with an unconstrained inference variable
+requires special solver support. It is only used by `AliasRelate` goals and pending
+`NormalizesTo` goals are tracked separately from other goals: [source][try-eval-norm].
+As the expected term is always erased in `NormalizesTo`, we have to return its
+ambiguous nested goals to its caller as not doing so weakens inference. See
+[#122687] for more details.  
+
+[trait-system-refactor-initiative#22]: /~https://github.com/rust-lang/trait-system-refactor-initiative/issues/22
+[try-eval-norm]: /~https://github.com/rust-lang/rust/blob/2627e9f3012a97d3136b3e11bf6bd0853c38a534/compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs#L523-L537
+[#122687]: /~https://github.com/rust-lang/rust/pull/122687
+
+## `AliasRelate` and structural normalization
+
+We structurally normalize an alias by applying one-step normalization until
+we end up with a rigid alias, ambiguity, or overflow. This is done by repeatedly
+evaluating `NormalizesTo` goals inside of a snapshot: [source][structural_norm].
+
+`AliasRelate(lhs, rhs)` is implemented by first structurally normalizing both the
+`lhs` and the `rhs` and then relating the resulting rigid types (or inference
+variables). Importantly, if `lhs` or `rhs` ends up as an alias, this alias can
+now be treated as rigid and gets unified without emitting a nested `AliasRelate`
+goal: [source][structural-relate].
+
+This means that `AliasRelate` with an unconstrained `rhs` ends up functioning
+similar to `NormalizesTo`, acting as a function which fully normalizes `lhs`
+before assigning the resulting rigid type to an inference variable. This is used by
+`fn structurally_normalize_ty` both [inside] and [outside] of the trait solver.
+This has to be used whenever we match on the value of some type, both inside
+and outside of the trait solver.
+
+FIXME: structure, maybe we should have an "alias handling" chapter instead as
+talking about normalization without explaining that doesn't make too much
+sense.
+
+FIXME: it is likely that this will subtly change again by mostly moving structural
+normalization into `NormalizesTo`.
+
+[structural_norm]: /~https://github.com/rust-lang/rust/blob/2627e9f3012a97d3136b3e11bf6bd0853c38a534/compiler/rustc_trait_selection/src/solve/alias_relate.rs#L140-L175
+[structural-relate]: /~https://github.com/rust-lang/rust/blob/a0569fa8f91b5271e92d2f73fd252de7d3d05b9c/compiler/rustc_trait_selection/src/solve/alias_relate.rs#L88-L107
+[inside]: /~https://github.com/rust-lang/rust/blob/a0569fa8f91b5271e92d2f73fd252de7d3d05b9c/compiler/rustc_trait_selection/src/solve/mod.rs#L278-L299
+[outside]: /~https://github.com/rust-lang/rust/blob/a0569fa8f91b5271e92d2f73fd252de7d3d05b9c/compiler/rustc_trait_selection/src/traits/structural_normalize.rs#L17-L48
+
+## Deep normalization
+
+By walking over a type, and using `fn structurally_normalize_ty` for each encountered
+alias, it is possible to deeply normalize a type, normalizing all aliases as much as
+possible. However, this only works for aliases referencing bound variables if they are
+not ambiguous as we're unable to replace the alias with a corresponding inference
+variable without leaking universes.
+
+FIXME: we previously had to also be careful about instantiating the new inference
+variable with another normalizeable alias. Due to our recent changes to generalization,
+this should not be the case anymore. Equating an inference variable with an alias
+now always uses `AliasRelate` to fully normalize the alias before instantiating the
+inference variable: [source][generalize-no-alias]
+
+[generalize-no-alias]: /~https://github.com/rust-lang/rust/blob/a0569fa8f91b5271e92d2f73fd252de7d3d05b9c/compiler/rustc_infer/src/infer/relate/generalize.rs#L353-L358
 
 ## Outside of the trait solver
 
@@ -41,10 +91,8 @@ Luckily deep normalization is currently only necessary in places where there is
 
 If we only care about the outermost layer of types, we instead use
 `At::structurally_normalize` or `FnCtxt::(try_)structurally_resolve_type`.
-Unlike `At::deeply_normalize`, shallow normalization is also used in cases where we
-have to handle ambiguity. `At::structurally_normalize` normalizes until the self type
-is either rigid or an inference variable and we're stuck with ambiguity. This means
-that the self type may not be fully normalized after `At::structurally_normalize` was called.
+Unlike `At::deeply_normalize`, structural normalization is also used in cases where we
+have to handle ambiguity.
 
 Because this may result in behavior changes depending on how the trait solver handles
 ambiguity, it is safer to also require full normalization there. This happens in
@@ -70,11 +118,4 @@ for deep normalization to the new solver we cannot emulate this behavior. This d
 for projections with bound variables, sometimes leaving them unnormalized. An approach which
 also supports projections with bound variables will be even more involved. 
 
-
-[`assemble_candidates_after_normalizing_self_ty`]: /~https://github.com/rust-lang/rust/blob/1b6d4cdc4d923c148198ad4df230af48cdaca59e/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L330-L378
-[`AliasRelate`]: /~https://github.com/rust-lang/rust/blob/1b6d4cdc4d923c148198ad4df230af48cdaca59e/compiler/rustc_trait_selection/src/solve/alias_relate.rs#L16-L102
-[`normalizes-to` candidates]: /~https://github.com/rust-lang/rust/blob/1b6d4cdc4d923c148198ad4df230af48cdaca59e/compiler/rustc_trait_selection/src/solve/alias_relate.rs#L105-L151
-[the behavior of projection clauses]: /~https://github.com/rust-lang/trait-system-refactor-initiative/issues/1
-[normalize-via-infer]: /~https://github.com/rust-lang/rust/blob/1b6d4cdc4d923c148198ad4df230af48cdaca59e/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L350-L358
-
-[^0]: TODO: currently refactoring this to use `NormalizesTo` predicates instead.
+[^opaques]: opaque types are currently handled a bit differently. this may change in the future

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
+not 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 reaching 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