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.
Normalization in the new solver exclusively happens via Projection1 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 Projection1 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)1. ?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.
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.
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.