diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 94e619f42..4870e0cbf 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -124,6 +124,7 @@ - [Canonicalization](./solve/canonicalization.md) - [Coinduction](./solve/coinduction.md) - [Proof trees](./solve/proof-trees.md) + - [Normalization](./solve/normalization.md) - [Type checking](./type-checking.md) - [Method Lookup](./method-lookup.md) - [Variance](./variance.md) diff --git a/src/solve/normalization.md b/src/solve/normalization.md new file mode 100644 index 000000000..653c976a4 --- /dev/null +++ b/src/solve/normalization.md @@ -0,0 +1,80 @@ +# Normalization in the new solver + +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(::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 `::Assoc`, we first create +a fresh inference variable `?normalized` and then prove +`Projection(::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]. + +## Outside of the trait solver + +The core type system - relating types and trait solving - will not need deep +normalization with the new solver. There are still some areas which depend on it. +For these areas there is the function `At::deeply_normalize`. Without additional +trait solver support deep normalization does not always work in case of ambiguity. +Luckily deep normalization is currently only necessary in places where there is no ambiguity. +`At::deeply_normalize` immediately fails if there's ambiguity. + +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. + +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 +`FnCtxt::structurally_resolve_type` which always emits a hard error if the self type ends +up as an inference variable. There are some existing places which have a fallback for +inference variables instead. These places use `try_structurally_resolve_type` instead. + +## Why deep normalization with ambiguity is hard + +Fully correct deep normalization is very challenging, especially with the new solver +given that we do not want to deeply normalize inside of the solver. Mostly deeply normalizing +but sometimes failing to do so is bound to cause very hard to minimize and understand bugs. +If possible, avoiding any reliance on deep normalization entirely therefore feels preferable. + +If the solver itself does not deeply normalize, any inference constraints returned by the +solver would require normalization. Handling this correctly is ugly. This also means that +we change goals we provide to the trait solver by "normalizing away" some projections. + +The way we (mostly) guarantee deep normalization with the old solver is by eagerly replacing +the projection with an inference variable and emitting a nested `Projection` goal. This works +as `Projection` goals in the old solver deeply normalize. Unless we add another `PredicateKind` +for deep normalization to the new solver we cannot emulate this behavior. This does not work +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. \ No newline at end of file