The Coq mailing list

["Andrew McCreight" <continuation AT gmail.com>]

I had this exact same problem.  I think my solution was to define a signature for sets + (some subset of) FSetFacts and use that as a functor argument instead of the raw set.  It is a little ugly, especially given that you can't really unpack a module inside of another module, so there is always an extra level of indirection (unless you import the outer module, which is not something you usually want to do, because you'll usually have more than one kind of set sitting around).

-Andrew

On Thu, Jun 5, 2008 at 2:21 PM, Aaron Bohannon <bohannon AT cis.upenn.edu> wrote:

I've noticed a bad interaction between setoids and the module system.
If a setoid is defined in a functor (let's call it F), then apparently
that functor must only be instantiated exactly once (otherwise, you
will see a long warning and rewriting in the setoid will stop
working).  This doesn't sound like a huge problem (why would you
instantiate a functor twice?), until you try to write another functor
G (in its own file) with proofs that require rewriting in the setoid
defined in F.  In order for the file containing G to compile, G must
instantiate F internally.  Thus, one must be sure to never instantiate
F outside of G.  OK, now that's already a software engineering
nightmare, but worse, imagine two functors G1 and G2 that both require
access to rewriting in the setoid defined in F.  Now you're completely
stuck.

I'm not sure if I can call this a bug, because there is no simple,
obvious solution.  The only thing that comes to mind would be to allow
abstraction over setoid and morphism declarations by including them in
module types.  Is anybody working on this issue?  Does anybody know of
good work-arounds?  For a specific example of such a functor F, see
the FSetFacts file from the standard library.

 - Aaron

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
         http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club