The Coq mailing list

[Petter Urkedal <paurkedal AT gmail.com>]

My previous mail "FMap* with Set" was a bit too terse (including the
title), so I attach the whole derivation, which gives

Error: The term "Labelling.t nat" has type
 "Type (* max(Coq.Structures.OrderedType.5, Set) *)"
 while it is expected to have type "Set".

Now, I see what is happening here is that OrderedType.t has been
assigned an indeterminate universe.  Further, it cannot be forced to
Set, because some other module might constrain in to be a higher
universe, which would cause problems in a diamond import.  The reason
I attempted to coerce it to Set in the first place was due to the
misconception (I now believe) that specifications need to be in Set to
be extracted.

I can see the point of using Type in a parameter positions of general
purpose modules, and this seems to be the general design of the
standard library.  So, is the idea that one should just switch to Type
whenever these are mixed into ones own data structures, even if they
could have been in Set from a logical point of view?  I don't see a
problem with it if extraction works, it seems a bit radical to lift
whole developments to an unspecific universe.

Attachment: Label.v
Description: Binary data