You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
In rustc we allow an universal binder to bind more than one name, such as for<'a, 'b> fn(&'a u32, &'b u32) were both 'a and 'b have a DeBruijn index of 0. In chalk we also allow you to write that, but when moved into the environment 'a and 'b will have distinct universes (see fn instantiate_binders_universally and unify_forall_tys).
Currently chalk represents universal type in the environment directly by the universe index, so forall<T> { Goal(T) } becomes Goal(Ui) once the binder is into the environment. We might want to instead represent them with an index into a table in the environment, like we do for existential variables today, this would be one way to allow us to associate the universal type not only with a universe but with a particular name within that universe. Or maybe we could inline it by carrying two indexes Uij where j is the relative index of the name within the universe.
A motivation would be to u-canonicalize forall<T, U> { Goal(T, U) } and forall<T, U> { Goal(U, T) } into the same thing, as it should be easier to put the universals in a canonical order when you know they are at the universe.
Or at least that's how I understood it, ping @nikomatsakis
The text was updated successfully, but these errors were encountered:
leoyvens
changed the title
Allow a universal binder to bind many names
Allow a universe to bind many names
Jun 5, 2018
Uh oh!
There was an error while loading. Please reload this page.
In rustc we allow an universal binder to bind more than one name, such as
for<'a, 'b> fn(&'a u32, &'b u32)
were both'a
and'b
have a DeBruijn index of0
. In chalk we also allow you to write that, but when moved into the environment'a
and'b
will have distinct universes (seefn instantiate_binders_universally
andunify_forall_tys
).Currently chalk represents universal type in the environment directly by the universe index, so
forall<T> { Goal(T) }
becomesGoal(Ui)
once the binder is into the environment. We might want to instead represent them with an index into a table in the environment, like we do for existential variables today, this would be one way to allow us to associate the universal type not only with a universe but with a particular name within that universe. Or maybe we could inline it by carrying two indexesUij
wherej
is the relative index of the name within the universe.A motivation would be to u-canonicalize
forall<T, U> { Goal(T, U) }
andforall<T, U> { Goal(U, T) }
into the same thing, as it should be easier to put the universals in a canonical order when you know they are at the universe.Or at least that's how I understood it, ping @nikomatsakis
The text was updated successfully, but these errors were encountered: