Reification of Universes!

[gmalecha]

No description provided.

[gmalecha]

It probably isn't too bad to determine the universe levels, but there doesn't seem to be any convenient way to denote them.

[gmalecha]

I can just use the type as the universe level (though this could induce universe problems if you try to quote something with syntax inside of it).

This means that you can't see if two universes are the same, but this information does not readily exist in the kernel anyways.

[gmalecha]

demo of this in f250e6d

[gmalecha]

Going to solve this in master using a reification map.

[mattam82]

One could reify using a map from level list (level being a positive with a boolean for +1 potentially) to Type. (That last type will be higher than any other). In the universe polymorphic case the term under the universe context refers to the universe context variables (internally, using de Bruijn indices, but you probably don't see it if you get the body of e.g. id@{i} := fun (A : Type@{Var 0}) (a : A) => a then the body you get is "fun (A: Type@{i}) (a : A) => A".

[gmalecha]

One issue that we might run into is that you can never write a Gallina term that is universe polymorphic because the top-level always instantiates it with fresh variables. When we quote, we will either need to figure this out, or not really quote universe polymorphism.

Potentially the annoying bit with universes is that constraints might dictate that two universes are equal, but they will appear syntactically different. Perhaps this isn't a problem though because it appears the same way in Coq.

[aa755]

Because one cannot analyze a Type in Gallina, writing program transformations with an intent of unquoting can be problematic if we define Ast.universe:=Type. Can we instead define Ast.universe:=string? To support universe polymorphism, quoting of definitions will perhaps need to be updated to also reify the context of universes (as list of names?). Analogous changes would be needed in the unquoting function: the user will have to specify the local universe context as a list of names. For universe names not in the context, the unquoting function would create fresh rigid universe levels?

Also, is there a way to implement unquoting (e.g. Make Definition) such that the user doesn't have to specify the universe constraints needed for a definition to typecheck and let Coq figure them out?