The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Samuel,

I think I have shown how to fix this kind of issue in my post. I don't see 
how your case is different. I would suggest to try the following:

- put the inductive type definitions from module functor Imp into a module 
type functor IMP
- define module Imp as "Module Imp (P : ImpParameters) := Empty <+ IMP P."
- give everything which needs Imp a parameter of type IMP and instantiate it 
with Imp
- possibly define combined module types and modules to avoid long parameter 
lists

The trick is that now the inductive definition is in the module type rather 
than in the module instance and the type is the same for all instances, so 
the inductive types are the same. At the end of the code I posted, you can 
actually prove the following:

Theorem Eq1: FD.bar = FDX.bar.
Proof.
  reflexivity.
Qed.

Theorem Eq2: FD.Bar = FDX.Bar.
Proof.
  reflexivity.
Qed.

although Coq still thinks FD.bar and FDX.bar are separate definitions as 
Locate bar or Locate Bar shows.

This might seem like a bizarre hack, but I think it is quite logical to do it 
this way. My view is that whatever is needed by other modules must be defined 
in a module type. Modules are there to define concrete implementations of 
abstract definitions in a module type. Other modules should only use module 
types and not concrete modules. When you cannot abstract away from what is in 
a module, it is part of the interface and doesn't belong in a module but in a 
module type.

If you have an inductive definition and where you use this type you can 
replace it with an abstract type (say a generic map data structure), the 
inductive belongs in a module and the module type just provides an abstract 
type. If you need the details of the inductive in modules using it, the 
inductive belongs into a module type.

Of cause if a module A just uses another module B to implement its 
functionality in such a way that nothing of B is visible at the interface 
(signature) of A, A can just use a module B. This typically applies to 
modules just defining a bunch of lemmas, tactics or notations but also to 
modules defining helper data structures like maps or sets, which are 
abstracted away at the external interface of module A. But anything about 
other modules which is somehow visible in the signature of A, must be defined 
in a module type, and not in a module.

In my experience the module system works quite well, if it is used in this 
way.
 
I hope those who came up with the module system agree with this view.

Best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928