4
$\begingroup$

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?

$\endgroup$

1 Answer 1

4
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.