Universe polymorphism and modules in Coq

Question

The following code (without universe polymorphism) is accepted by Coq (8.16.0) :

Module Type T.
Parameter F : Type -> Type.
End T.

Module M1 <: T.
Definition F (A : Type) : Type := A.
End M1.

Module M2 <: T.
Definition F (A : Type) : Type := A*A.
End M2.

But if I set universe polymorphism, M1 is rejected with the error message:

Signature components for field F do not match: incompatible polymorphic binders: got @{u u0 |= u <= u0} but expected @{u u0} (incompatible constraints).

I can have Coq accept M1 by adding a constraint in the Module Type:

Parameter F@{u v | u <= v} : Type@{u} -> Type@{v}.

But then M2 is rejected with the error message:

Signature components for field F do not match: incompatible polymorphic binders: got @{u u0 |= u <= prod.u0, u <= prod.u1, u <= u0} but expected @{u v |= u <= v} (incompatible constraints).

How can I have Coq accept both M1 and M2 when universe polymorphism is set?

Answer 1

If you go polymorphic, you should probably go all the way, and also use a polymorphic product type, like so:

Set Universe Polymorphism.

Record prod (A B : Type) : Type := { left : A ; right : B }.

Module Type T.
Parameter F@{u v | u <= v} : Type@{u} -> Type@{v}.
End T.

Module M1 <: T.
Definition F (A : Type) : Type := A.
End M1.

Module M2 <: T.
Definition F (A : Type) : Type := prod A A.
End M2.

This sadly means that you cannot use much of the (monomorphic) standard library, but I'm not sure that trying to build a polymorphic development using monomorphic primitives would work well anyway.