Stream: Coq users

Topic: Universe instance i+1

view this post on Zulip Cyril Cohen (Nov 20 2022 at 21:04):

I wonder if it is possible to make the following code run through with universe polymorphism:

Set Universe Polymorphism.
Unset Universe Minimization ToSet.
Set Printing Universes.
Definition f@{i j} (A : Type@{i}) (B : Type@{j}) := A.
Fail Definition g@{i} (A : Type@{i}) := f A (Type@{i}).

Right now it fails with error message

Error: Universe test.5 (Toplevel input, characters 342-343) is unbound.

Apparently it cannot instanciate j to i+1, and I cannot help manually:

Definition g@{i} (A : Type@{i}) := f@{i i+1} A (Type@{i}).

is even a syntax error.
Of course the following works:

Definition g@{i j} (A : Type@{i}) := f@{i j} A (Type@{i}).

but is not what I want since g now depends on two universe variables...

view this post on Zulip Gaƫtan Gilbert (Nov 20 2022 at 21:08):

it is a dream of @Matthieu Sozeau
but needs the universe checking graph to be generalized, which is especially difficult to do while preserving performance
see also

view this post on Zulip Meven Lennon-Bertrand (Nov 21 2022 at 10:42):

This is also how things are currently done in MetaCoq (which helps a lot with formalization, because we do not have to care about algebraic universes being only allowed at certain places, meaning in practice that some valid types containing algebraic universes are not valid terms). So the theory would be safe with such a change, the main issue is efficiency.

Last updated: Jan 28 2023 at 06:30 UTC