I ran into the a problem, with universe polymorphism is disabled. If I enable it at the start of the file, the problem disappears. Could someone help me figure out why? A minimized example is as follows:

```
Definition Ensemble (U : Type) := U -> Prop.
Definition foo (U V:Type) : Prop.
Admitted.
Lemma bar (U : Type) : foo (Ensemble U) U.
Admitted.
Lemma WF_implies_MEP
(T : Type) (R : T -> T -> Prop) :
well_founded R -> forall S:Ensemble T, True.
Admitted.
Theorem foo_wf :
well_founded foo.
Admitted.
Theorem problem (P : Type -> Prop) : True.
Proof.
unshelve eapply (WF_implies_MEP Type foo _ P).
apply foo_wf.
```

This fails with:

```
Error: In environment
P : Type -> Prop
Unable to unify "well_founded foo" with "well_founded (fun U V : Type => foo U V)".
```

Does the problem disappear if you switch to refine (foo_wf _ _ _) with the right number of undescores "

if you put `bar`

after `problem`

you get

```
The term "Ensemble U" has type "Type@{max(Set+1,Ensemble.u0)}" while it is expected to have type
"Type@{foo.u0}" (universe inconsistency: Cannot enforce Ensemble.u0 <= foo.u0 because foo.u0
< WF_implies_MEP.u0 <= Ensemble.u0).
```

IOW applying `foo`

to `Ensemble U`

implies some constraint and `problem`

produces an incompatible constraint

@Paolo Giarrusso , no, using refine doesn't help. But if `foo_wf`

is formulated as `Theorem foo_wf : well_founded (fun A B : Type => foo A B).`

it works.

Am I forced in this situation to enable universe polymorphism? Is there some documentation about the universe constraints, so I can understand better what constraints are generated? Or that I can deduce by myself why one sequence of commands works and the other does not? I know of `Print Universes.`

but that list is rather long.

Last updated: Jun 23 2024 at 04:03 UTC