Stream: Coq users

Topic: Universe-polymorphic module types and modules


view this post on Zulip James Wood (Aug 10 2022 at 13:38):

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}.
 *)

view this post on Zulip Gaëtan Gilbert (Aug 10 2022 at 14:42):

don't declare them together, ie do Parameter A : Type. Parameter B : Type.

view this post on Zulip James Wood (Aug 10 2022 at 14:52):

Thanks, that makes a difference, but I get the error message:

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

That seems more surprising, if anything. :upside_down:

view this post on Zulip 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)

you can do

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

view this post on Zulip 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.

view this post on Zulip James Wood (Aug 10 2022 at 15:13):

Gaëtan Gilbert said:

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

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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Aug 10 2022 at 15:29):

there is no module level univ polymorphism

view this post on Zulip Paolo Giarrusso (Aug 10 2022 at 19:31):

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.

Would it work to declare a "maximal" universe for those to fit in?

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)

Why? If it's because of the eta-contraction, that's fixable by eta-expansion

view this post on Zulip 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)

view this post on Zulip 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


Last updated: Mar 29 2024 at 15:02 UTC