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:

- commenting "Axiom MayRet" in the "Foo" module type.
- or, admitting the proof of "Lemma zarb" of "Bar" module.

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 !

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

it works if you `unfold mayRet`

before`apply eq_refl`

, or if you use `refine (eq_refl _)`

I guess it's some issue with apply's unification

:heart: Great, thanks a lot. Gaëtan: your `refine`

solution perfectly solves the corresponding issue in my bigger development !

Something I found very weird is that when you print all the low-level contents of the proof terms found by the `apply`

or 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) ?

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

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

If you did, it sounds at least very unfortunate

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`

).

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