Stream: Coq users

Topic: Universe and Modules for dummies


view this post on Zulip Sylvain Boulmé (Jul 30 2023 at 17:20):

Hello,

I cannot understand what happens with the attached file (both in coq 8.17.1 and coq 8.16.1):
UnivBug.v

Basically, it fails with the following message.
File "./UnivBug.v", line 39, characters 6-13:
Error:
The term "A.t nat" has type "Type@{A.t.u0}" while it is expected to have type
"?A" (unable to find a well-typed instantiation for
"?A": cannot ensure that "Type@{UnivBug.12+1}" is a subtype of
"Type@{eq.u0}").

Changing the line "Module A <: Foo := Bar." into "Module A := Bar." makes the failure disappear.

Printing Universes gives very similar outputs in both cases except that
A.t.u0 = eq.u0 for the failing case
whereas A.t.u0 <= eq.u0 for the non-failing one.

What really puzzles me is that there are two other alternative ways to make the failure disappear:

Thus, from the previously described experiments, the constraint "eq.u0 <= A.t.u0" of the failing case appears
with the conjunction of three constraints:

- Module A <: Foo
- Type of "Foo.MayRet".
- Something in the proof of "Bar.zarb".

But, I do not understand why. Of course, I would like to have a patch enabling these 3 constraints.
Any help would be really appreciated. Thanks !

view this post on Zulip Kenji Maillard (Jul 31 2023 at 11:46):

Hello, I don't fully understand where the constraint A.t.u0 = eq.u0 is comming from, my naive guess would be that the application of the hypothesis H in the lemma zarb uses cumulativity on the domain of the function which is restricted to equality of universe levels.
Making zarb polymorphic seem to help with this issue:

Module Bar.

   Definition t (A:Type) := A.

   Definition mayRet {A:Type} (a b:A): Prop := a=b.


   Polymorphic Lemma zarb: forall (A : Type) (k: t A) x, (forall r, mayRet k r -> r=x tt) -> k = x tt.
   (* Admitted. *)
   Proof.
     intros A k x H; eapply (H k); apply eq_refl.
   Qed.

End Bar.

view this post on Zulip Gaëtan Gilbert (Jul 31 2023 at 12:40):

it works if you unfold mayRet beforeapply eq_refl, or if you use refine (eq_refl _)
I guess it's some issue with apply's unification

view this post on Zulip Sylvain Boulmé (Jul 31 2023 at 13:29):

:heart: Great, thanks a lot. Gaëtan: your refine solution perfectly solves the corresponding issue in my bigger development !

view this post on Zulip Sylvain Boulmé (Jul 31 2023 at 13:36):

Something I found very weird is that when you print all the low-level contents of the proof terms found by the applyor the refine version: these proof terms seem identical. Would this means that the unnecessary universe constraint comes from the apply tactic itself and not from the typechecking of the generated term ? Do you believe that this unexpected behavior should be reported as an issue (or even a bug) ?

view this post on Zulip Paolo Giarrusso (Jul 31 2023 at 13:50):

Did you enable Set Printing Universes? Set Printing All doesn't print all

view this post on Zulip Paolo Giarrusso (Jul 31 2023 at 13:50):

In some IDEs it's "all low-level" vs "all basic low-level"

view this post on Zulip Paolo Giarrusso (Jul 31 2023 at 13:51):

If you did, it sounds at least very unfortunate

view this post on Zulip Sylvain Boulmé (Aug 01 2023 at 18:07):

Yes, I have printed the proof terms with both Set Printing Universes and Set Printing All, exactly like in the UnivBug.v file given above. And, again, this is very strange that the failure disappears when commenting the declaration of "Foo.MayRet". I cannot undestand how this interact with apply (since apply is run in the Bar module which is not constraint by Foo).

view this post on Zulip Gaëtan Gilbert (Aug 01 2023 at 18:37):

universes are global, so Module A <: Foo := Bar. globally adds the universe constraints needed to make Bar fit Foo


Last updated: Jun 23 2024 at 05:02 UTC