handle universes in canonicalization

[nikomatsakis]

Now that #47861 has landed, there is a notion of universes for type variables. For now, in order to get #48411 landed, the canonicalization code is simply using UniverseIndex::ROOT for the universes of type variables it creates (those universes aren't really being used anyway presently).

However, what we ought to be doing is recording (during canonicalization) the universe of the variables that are being fed in. We can then canonicalize those universes (what chalk calls u_canonicalize) and then recreate them on the other side. And finally we map the universes back.

I'll try to leave more detailed notes later. I expect to either do this or mentor this as follow-up.

cc @sgrif

[sgrif]

Definitely interested in working through this

[nikomatsakis]

@sgrif and I had a brief conversation in gitter going into a bit more detail. I'll try to get to writing up a rustc-guide chapter here.

[nikomatsakis]

@sgrif ok so I was thinking about this last night after we talked. My PR to move skolemized things into the global tcx works, but as I said on gitter I'm now revisiting that question. Maybe you were onto something in #49598.

Perhaps we could set it up like so:

When you canonicalize, we replace skolemized regions with canonical variables, as in your PR.

We would also add information to CanonicalVarInfo indicating whether this was "universally" or "existentially" bound:

rust/src/librustc/infer/canonical.rs

Lines 85 to 87 in 4bf76d6

	pub struct CanonicalVarInfo {
	pub kind: CanonicalVarKind,
	}

Then when we instantiate each canonical variable, we would create "skolemized" variables for those things that were skolemized (in the appropriate universe):

rust/src/librustc/infer/canonical.rs

Lines 247 to 251 in 4bf76d6

	pub fn fresh_inference_var_for_canonical_var(
	&self,
	span: Span,
	cv_info: CanonicalVarInfo,
	) -> Kind<'tcx> {

I think we could start with "identity mapping" between universes, in which case we would still need to carry (in the Canonical value) the max universe of any skolemized things we encountered, so that when we create a fresh inference context, we can make it contain that many universes.

Once we add a real map, I think we could put the map into CanonicalVarValues, or maybe a new kind of struct that wraps it (CanonicalMapping):

rust/src/librustc/infer/canonical.rs

Lines 76 to 78 in 4bf76d6

	pub struct CanonicalVarValues<'tcx> {
	pub var_values: IndexVec<CanonicalVar, Kind<'tcx>>,
	}

then instantiate_query_result would take a CanonicalMapping instead of just a CanonicalVarValues:

rust/src/librustc/infer/canonical.rs

Line 288 in 4bf76d6

original_values: &CanonicalVarValues<'tcx>,

and use the info to do the mapping.

[sgrif]

Makes sense. Thanks for looking into it

[sgrif]

@nikomatsakis Sorry for the radio silence, I've been at a conference the last week. After poking at the solution you described, I think we need to take #49598 as an intermediate step. InferCtxt doesn't know anything about universes until #48407, but that is blocked on some solution to this in the short term. I can roll this change into that PR, but it's already huge and we're not even sure we want to land it until we can get a crater run.