Coq - unify types from module functors with same parameters?

user_5947247 0
Viewed 165

How can I get Coq to recognise that two types, which are each imported from a module which is created from a module functor using the same argument, but appear in different modules, are actually the same type?

Minimal example

Module Type S.
End S.

Module F (s : S).
Inductive foo : Type := a.
End F.

Module G (s : S).
Include F s.
End G.

Module H (s : S).
Include F.
End H.

Module I (s : S).

Module G := G s.
Module H := H s.

(* This is a type error - but the foos are the same! *)
Axiom bar : forall g : G.foo, forall h : H.foo, g = h.

End I.

In the above Coq file, I want to declare an axiom that requires that the type foo in G s be the same as the type foo in H s. Clearly, this is actually the case. But can I get Coq to recognise it?

coq module
1 Answers

This is not possible. There is no structural equivalence between inductive types. By using Include twice, you are creating two different types. They happen to have the same name, but this is just a coincidence.

More generally, inductive types are badly supported by the module system. Any time you try something a bit fancy, Coq will complain that "The kernel does not recognize yet that a parameter can be instantiated by an inductive type."

As a rule of thumb, I suggest to always define inductive types outside module functors. I suppose that your type foo would depend on some property of module s, so you have to make it a bit more generic:

Module Type S.
Axiom t : Type.
End S.

Inductive foo (t : Type) : Type := a : t -> foo t.

Module F (s : S).
Definition foo := foo s.t.
End F.
user_134991210
Related