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...

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

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