The Coq mailing list

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

I am observing some strange interactions between modules and morphisms.

First of all, testing whether a relation is "registered" appears to be
a syntactic check that does account for covertability or sharing
constraints indicated by modules, which is a bit of a hassle.

More strange is the following situation.  I have the code:

...
(* Module ASD := Foo (AS).  (* Line 1 *) *)
...
setoid_replace (union X X) with X using relation AS.Equal.  (* Line 2 *)
...

This "setoid_replace" on Line 2 works perfectly when Line 1 is not
executed.  However, by uncommenting Line 1 and changing *nothing* else
in the file, I get the following error message at Line 2:

Error: refiner was given an argument "ASD.MP.FM.EqualSetoid_morphism" of type
"let ASetoidClass :=
   SymmetricReflexive variance (Seq_sym t Equal ASD.MP.FM.Equal_ST)
     (Seq_refl t Equal ASD.MP.FM.Equal_ST) in
 Morphism_Theory (cons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class"
instead of
"Morphism_Theory
   (cons (FM.EqualSetoid Covariant) (singl (FM.EqualSetoid Covariant)))
   (iff_relation tt)"

I suspect this has to do with the fact that a some relations and some
of their morphisms (in my particular case, the ones in FSetFacts),
which were already registered, are being re-registered by this functor
instantiation, and this is causing problems.  But does this mean that
functors declaring morphisms should only ever be instantiated once?
Or is there a way around this?

-Aaron