Cyril Cohen (Nov 20 2022 at 21:04): 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...
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 https://github.com/coq/coq/pull/16022
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: Sep 23 2023 at 14:01 UTC