## Stream: Coq users

### Topic: Monomorphic Universe problem

#### Stéphane Desarzens (Aug 18 2023 at 11:45):

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.

Lemma bar (U : Type) : foo (Ensemble U) U.

Lemma WF_implies_MEP
(T : Type) (R : T -> T -> Prop) :
well_founded R -> forall S:Ensemble T, True.

Theorem foo_wf :
well_founded foo.

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)".
``````

#### Paolo Giarrusso (Aug 18 2023 at 17:56):

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

#### Gaëtan Gilbert (Aug 18 2023 at 18:00):

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

#### Stéphane Desarzens (Aug 19 2023 at 06:31):

@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