scuellar/MMap — pull request #1 by finrod (2014-06-17 19:46:32+00:00)
Title: Resolution for not being able to Include IsEq and HasEqDec

The (higher-order) Module Types IsEq and HasEqDec cannot be Included for a couple of reasons.
a) In the appropriate line we're in a Section, thus almost any Module-level command (save for Import) will fault. This is with good reason: Section Variables get abstracted at the end of section _at the Gallina term level_, not at the module language level (at which it doesn't make any sense). The module system is in many ways second-class citizen: this is one of them.
b) Obviously, one could close the Section before trying to Include the MTs. This is problematic, since both of these are higher-order (otherwise the Include might even work within the Section; haven't checked). What happens in this case (c.f. section 2.5.1 of the RefMan) is that the Module (Type) gets instantiated with the Module (Type) that we're currently building interactively. This would be well and good, were it not for the sort of the parameter t. In a map, this is a type constructor (Type -> Type), whereas Eq, the parameter of IsEq, requires it to have the sort Type (unsurprisingly, really, since it's using t as a proper type). Thus, we won't be able to include these.
c) Since this is the case, one might try to build another instance of Eq, and instantiate IsEq and HasEqDec explicitly with that module. That won't work, however — roughly speaking, since modules cannot be parametrised with types in this way (this is also why one can't define it inside the section).

Thus, the simplest thing is to just copy over the contents of IsEq and HasEqDec explicitly, sacrificing perhaps some stability under future development, but at least achieving something. One needs to pay a little attention to types while copying over, which the attached patch does.

Cheers,
— Filip