change NormalizesTo to fully structurally normalize

[lcnr]

notes in https://hackmd.io/wZ016dE4QKGIhrOnHLlThQ

need to also update the dev-guide once this PR lands. in short, the setup is now as follows:

normalizes-to internally implements one step normalization, applying that normalization to the goal.predicate.term causes the projected term to get recursively normalized. With this normalizes-to normalizes until the projected term is rigid, meaning that we normalize as many steps necessary, but at least 1.

To handle rigid aliases, we add another candidate only if the 1 to inf step normalization failed. With this normalizes-to is now full structural normalization. We can now change AliasRelate to simply emit normalizes-to goals for the rhs and lhs.

This avoids the concerns from rust-lang/trait-system-refactor-initiative#103 and generally feels cleaner

[rustbot]

r? @compiler-errors

rustbot has assigned @compiler-errors.
They will have a look at your PR within the next two weeks and either review your PR or reassign to another reviewer.

Use r? to explicitly pick a reviewer

[rustbot]

Some changes occurred to the core trait solver

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

[lcnr]

TODO: this currently negatively affects perf because the structural norm is now nested alias-relate -> normalizes-to -> alias-relate. Intend to change instantiate_normalizes_to_term to use normalizes_to directly instead

[BoxyUwU]

r? @BoxyUwU
would like to review this myself

[lcnr]

TODO: this currently negatively affects perf because the structural norm is now nested alias-relate -> normalizes-to -> alias-relate. Intend to change instantiate_normalizes_to_term to use normalizes_to directly instead

Actually doesn't really negatively affect perf compared to the previous impl 🤔 trying the separate approach ends up causing worse perf by propagating more nested goals upwards, causing us to spend a lot more time in try_evaluated_added_goals

[BoxyUwU]

@bors r+ rollup=never

[bors]

📌 Commit 92b280c has been approved by BoxyUwU

It is now in the queue for this repository.

[BoxyUwU]

i mean @bors rollup=always (new solver)