Lazy normalization notes

Why do constants need lazy normalization?

See this Zulip conversation

Basic plan

One possible approach for lazy normalization in rustc is as follows. One key observation here is that we can do lazy normalization for constants and for associated types independently. I'm going to lay out how things should work with constants, as they are mildly simpler – but associated types could follow along a similar path. (The major difference is that we must accommodate subtyping.)

• In the ty::infer code that does "subtyping", "type equality", and so forth:
  • When we encounter a (Unevaluated, _) or (_, Unevaluated) case, we generate an obligation instead of processing it immediately.
  • Otherwise, we invoke the super_relate_consts code that does structural matching.
  • This obligation is for a ConstEquate(C, C) – meaning that we have to prove the two constants equal
• In the fulfillment code, a ConstEquate(C1, C2) obligation can be handled as follows:
  • If C1 or C2 includes inference variables, then we do nothing (leaving the obligation unfulfilled)
  • Otherwise, we eval each constant:
    • if we get back "too generic", then we will never be able to normalize it further; that's ok
    • if we get back a result, great
  • We then invoke the super_relate_consts method on the (now normalized) sides
• super_relate_consts is the same as today; it does structural matching on its two arguments

Obstacles

The current handling of regions is something of an obstacle, as the leak_check prevents us from creating obligations.

I am investigating removing it in the lazy-norm-anon-const-push-2 branch, but that re-opens some mildly tricky questions about the role the 'empty region plays. In particular, as noted in this commit, a few notable tests start to
pass because of "empty" interactions that are not obviously desirable:

• hrtb-exists-forall-trait-contravariant.rs
• hrtb-exists-forall-trait-covariant.rs
• issue-46989.rs

In addition, the following changes didn't seem obviously desired:

• old-lub-glb-object.rs got an additional error
• issue-57639.rs regresses, for the reasons covered in the issue

Finally there are some anticipated regressions:

• coherence-subtyping.rs gets an additional error

At heart is the question of whether this ought to be satisfiable:

• exists<'a> { forall<'b> { 'b: 'a } }

The current region solver assumes ReEmpty is less than all other things, which is the root of our problem here. I am exploring making ReEmpty be indexed by a universe to get rid of this behavior. (Update: it looks like this is working.)