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?