fix ucanonicalization bugs

[basil-cow]

some small bugs

[shepmaster]

Is "ucanonicalization" a typo or a fancy compiler term?

[bjorn3]

I think @Areredify means universe canonicalization.

[basil-cow]

@shepmaster bjorn3 is right, ucanonicalization stands for universe canonicalization: basically, after goal canonicalization (that replaces bound inference variables with their values) we do universe canonicalization that remaps universes to their "canonical" representation, so that if the same subgoal is encountered with slightly different universes, we can use cached result instead of recomputing it. Consider

goal {
   forall<T1> {
      forall<T2> {
          Implemented(S<T2>: Trait)
      }
   }
}


goal {
   forall<T1> {
      Implemented(S<T1>: Trait)
   }
}

These goals are almost the same, except when pursuing the Implemented subgoal, the first will look like Implemented(S<!2_0>: Trait) and second will look like Implemented(S<!1_0>: Trait). We, of course, want to reuse the first goal when proving the second goal because they are almost the same. After ucanonicalizing they will both look like Implemented(S<!1_0>: Trait) (or Implemented(S<!0_0>: Trait), don't remember which one is it), which allows for caching.

[jackh726]

Do you have an example of a regression test(s)?

[basil-cow]

Uhh, sure

[basil-cow]

Hmm, I am no longer sure that this is a bug

[basil-cow]

closing in favor of #512