Would it be generally desirable in the following example for Coq to generate `U <= X`

instead of `U = X`

? It seems counter-intuitive to me to pick the less general solution when it involves the same number of universes.

```
Monomorphic Universe X.
Set Printing Universes.
Axiom H : forall A:Type@{X}, Prop.
Definition t@{U} : forall A : Type@{U}, Prop := H.
Print t. (* [...] {t.U} |= X = t.U *)
```

I know that picking the more general solution involves eta-expanding `H`

but this apparently already happens when the algorithm decides there is no other solution—as can be seen by adding `|U<X+`

to `t`

's universe declarations. So I wonder: why shouldn't we always eta-expand and get more general universe constraints? This example is very reduced but I have real code that breaks because of exactly this behavior. If this can't be changed in general do people think it would make sense to have a flag or something like that to enable it locally?

Just to be sure, this relaxation would only apply to monomorphic `X`

, no ? (for polymorphic `X`

, it seems to me that you shouldn't hit problems due to this equality constraint down the line and would prefer to minimize the number of distinct universe levels for simpler reasoning about universe levels)

Only in this reduced example would polymorphic `X`

help. In my actual code, `X`

appears in multiple places in the signature of `t`

and making it polymorphic only delays the conflict to the point where `t`

is used (maybe in conjunction with other functions that deal with instances of `X`

in such a way that their choice of `X`

and `t`

's choice of `X`

must coincide).

Last updated: Dec 07 2023 at 09:01 UTC