The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sat, 6 Oct 2012 10:19:39 +0200,
Petter Urkedal 
<paurkedal AT gmail.com>
 a écrit :

> 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.

The extraction does not make difference between Set and Type. After
all, OCaml, Haskell and Scheme do not care about universe
inconsistencies (which is mainly why we have Set and Type in Coq).
I would recommend to always use Type, and never Set. Or always use Set
and never Type (for very simple developpements which could allow it).
Mixing both is hardly ever a good idea. The only good points of using
Set vs Type is to make coq perform less computations to solve universe
constraints. But this part of the computation is often neglictable in
regards to the other computations.

Of course, it is okay to play with it and allows you to have a better
of the mechanics. But once you know how it works, chose between make
Coq do all computations (stick only to type) or make him do none (stick
with Set, and if needed define some universe: Definition U1 := Type.
Definition U2 := (Type : U1). and so on, which you will use instead of
Type)