Universe-polymorphic module types and modules · Coq users

I have the following code, where I have a module type foo of heterogeneous relations with arbitrary domain and codomain, and an instance myfoo giving, for each type A, the equality relation on A. However, End myfoo. gives the universe polymorphic error written below. How can I fix this? Ideally, the universes of A and B would be quantified over just like A and B themselves, and just happen to be instantiated to the same thing in myfoo. However, I'm also okay with giving A and B the same universe (polymorphically), as long as not all instances have to agree on some globally fixed universe.

Set Universe Polymorphism.

Module Type foo.
  Parameter A B : Type.
  Parameter T : A -> B -> Prop.
End foo.

Module myfoo <: foo.
  Parameter A : Type.
  Definition B := A.
  Definition T := eq (A:=A).
End myfoo.

(* Error: Signature components for label A do not match:
 * incompatible polymorphic binders: got @{u} but expected
 * @[u u0}.
 *)

Gaëtan Gilbert (Aug 10 2022 at 14:42):

James Wood (Aug 10 2022 at 14:52):

Error: Signature components for label T do not match:
incompatible polymorphic binders: got @{u |= u <= eq.u0} but expected
@{u u0}.

Gaëtan Gilbert (Aug 10 2022 at 15:04):

the module type foo expects to have T for A at any universe and B at any universe
myfoo only provides T for A and B at the same universe, and it must be small enough to be an argument of eq (which is template polymorphic and here template poly is basically the same as monomorphic)

Set Universe Polymorphism.

Inductive eq {A} a : A -> Prop := eq_refl : eq a a.

Module Type foo.
  Parameter A : Type. Parameter B : Type.
  Parameter T@{u} : A@{u} -> B@{u} -> Prop.
End foo.

Module myfoo <: foo.
  Parameter A : Type.
  Definition B := A.
  Definition T := eq (A:=A).
End myfoo.

I dont know if it will be all that useful though
in general univ poly in module types poses quite strong requirements

James Wood (Aug 10 2022 at 15:09):

I'll give something like this a go, thanks. Also, I've noticed that there's an even smaller example, which might cause me pain later:

Set Universe Polymorphism.

Module Type bar.
  Parameter A : Type.
End bar.

Module mybar <: bar.
  Definition A := nat.
End mybar.

James Wood (Aug 10 2022 at 15:13):

This bit I don't quite understand. T, as I've defined it, only works for the specific A and B defined in myfoo. But somehow it's got to be more universe-polymorphic than it is type-polymorphic.

Gaëtan Gilbert (Aug 10 2022 at 15:15):

Parameter T : A -> B -> Prop. means Parameter T@{u v} : A@{u} -> B@{v} -> Prop.
you can Set Printing Universes then Print T (before End foo) to see what gets generated

James Wood (Aug 10 2022 at 15:27):

There's no way to associate the universe parameters with the module (type), then? I think my simpler example shows that the default way universe parameters associate to definitions just doesn't work for module types and modules.

Gaëtan Gilbert (Aug 10 2022 at 15:29):

Paolo Giarrusso (Aug 10 2022 at 19:31):

Paolo Giarrusso (Aug 10 2022 at 19:32):

(@James Wood I've been warned against partially applied template-polymorphic types, but eta-expansion usually fixes that)

Gaëtan Gilbert (Aug 10 2022 at 20:01):

actually I misremembered, eq isn't template
template wouldn't have helped because template only helps to inhabit a smaller universe, the default constraints are always there AFAICT
for instance

(* monomorphic may escape constraints through the global env, so if we
   want to be really sure of what's happening we use polymorphism *)
Set Universe Polymorphism.
Definition bla@{u v|u < v} : Type@{v}.
Proof.
  exact_no_check (option ltac:(exact_no_check Type@{u})).
Defined.

fails at Defined saying This term has type "Type@{foo.1+1}" which should be coercible to "Type@{option.u0}".
this may be a bug TBH

Stream: Coq users

Topic: Universe-polymorphic module types and modules

James Wood (Aug 10 2022 at 13:38):