Stream: wg-traits

Topic: TyData::Placeholder


Florian Diebold (Feb 14 2020 at 19:26, on Zulip):

in the vein of aligning RA's Ty more with Chalk, I'm wondering about placeholders. We used to represent placeholders (for type parameters) in RA as simple indices, but after some refactoring recently, we now just use the (globally) unique ID of the type parameter, which simplifies a few things. Chalk has this representation of universe index + index. I actually don't quite understand what universes are, so

  1. what are universes? do they correspond to scopes introducing type parameters? why are they needed?
  2. why does Chalk need to know about them? It seems they are maybe only relevant in case of lifetime placeholders?
nikomatsakis (Feb 14 2020 at 19:32, on Zulip):

This is something we have to address with rustc, too

nikomatsakis (Feb 14 2020 at 19:33, on Zulip):

So, universes are used when dealing with types like for<'a> fn(&'a u32) or when solving goals like forall<T> { if (T: Debug) { Vec<T>: Debug } } (which rust can't currently express, but which arise with GATs)

nikomatsakis (Feb 14 2020 at 19:33, on Zulip):

in those cases, we need to 'instantiate' the type parameter T with something, and we use a placeholder for that; the universe helps us track what is in scope

nikomatsakis (Feb 14 2020 at 19:33, on Zulip):

there are a few write-ups about it, we should move them to the chalk book

nikomatsakis (Feb 14 2020 at 19:34, on Zulip):

in rustc, we have both: we use placeholders like chalk for the "transient lifetimes we create when dealing with higher-ranke things" and we use parameters w/ a def-id for the cases where you can readily enumerate "here are the parametrs in scope" (e.g., when you are checking the body of a function)

nikomatsakis (Feb 14 2020 at 19:35, on Zulip):

they are really both the same sort of placeholder, but we treat them slightly differently, and I also think there is some reason we might want that in chalk -- in particular, some of the thoughts I've had about how to handle region solving in a more principled way involve distinguishing between the lifetimes in scope on the fn being checked, and the ifetimes that you instantiate as you deal with higher-ranked types like fn

Florian Diebold (Feb 14 2020 at 19:36, on Zulip):

nikomatsakis said:

there are a few write-ups about it, we should move them to the chalk book

yeah, actually there's a link in the doc for UniverseIndex which seems to be outdated

nikomatsakis (Feb 14 2020 at 19:51, on Zulip):

@Florian Diebold I think the best write-up is this one

Florian Diebold (Feb 14 2020 at 19:57, on Zulip):

ah yeah, I think I actually read that one before. It seems it only talks about lifetimes, so the vague recollections I had of that didn't seem applicable for types :sweat_smile:

nikomatsakis (Feb 14 2020 at 20:00, on Zulip):

yeah, the concepts are all applicable

nikomatsakis (Feb 14 2020 at 20:00, on Zulip):

but that may not be obvious :)

nikomatsakis (Feb 14 2020 at 20:00, on Zulip):

if you have to solve something like exists<T> { forall<U> { T = U } } (which should not be provable...) you would get errors because of universes

Last update: Feb 25 2020 at 03:50UTC