move universes from environment into the inference table

[nikomatsakis]

This PR does a pretty big refactoring to how we handle universes, initially suggested by @arielb1. Along the way, it fixes a few random bugs and refactored a few other things.

Perhaps the main goal of this branch is to do a more thorough form of canonicalization when creating queries. In particular, we currently canonicalize by taking all free, existentially quantified variables and "renumbering" them in order of their appearance, basically. But we could do even better if we canonicalized the universally quantified things to.

Consider this example. Here is an initial query:

forall<U> { exists<V> { U: Foo<V> } }

when we push this goal, we will wind up with something like

!1: Foo<?V>
// where ?V is in the universe 1

then when we canonicalize this query we get something like:

!1: Foo<?0>
// where ?0 is in the universe 1

Now consider this query, which is the same but for a (unused) forall:

forall<T> { forall<U> { exists<V> { U: Foo<V> } } }

when we push this goal, we will wind up with something like

!2: Foo<?V>
// where ?V is in the universe 2

If we canonicalize that, we get a distinct result:

!2: Foo<?0>
// where ?0 is in the universe 2

But really they are the same query.

In this branch, we have a notion of "universal canonicalization" that takes an existentially canonical thing (like what we have above) and renumbers the universally quantified names in order of left-to-right appearance. So in that case both queries wind up canonicalized to:

!1: Foo<?0>
// where ?0 is in the universe 1

We then keep a "universe map" that goes from the canonicalized universe (say, U1 here) back to the original universe (U2, in our second example).

In the final commit, this change to introduce canonical universes lets us go one step further. We can remove the universe field from the environment altogether and instead just track the 'max universe' in the inference table. Basically, every time we create a new universe, we just increment this (almost) global counter. And whenever we would cross between inference tables, that's precisely the points where we are performing universal canonicalization anyway.

I also did a few other refactorings along the way. In fact, I just remembered one I overlooked. (I also encountered a kind of serious problem with how we do normalization, but I'll describe that in a separate issue.)

cc @aturon @scalexm

[nikomatsakis]

I suppose I will merge this.