Stream: Coq users

Topic: Monomorphic Universe problem

view this post on Zulip 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.
  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)".

view this post on Zulip 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 "

view this post on Zulip 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

view this post on Zulip 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