The Coq mailing list

["Aaron Bohannon" <bohannon AT cis.upenn.edu>]

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