The Coq mailing list

[roconnor AT theorem.ca]

On Tue, 19 Jan 2010, AUGER wrote:

> Hi all,
> I found a coq feature which doesn't seem natural:
>
> coqc base.v; coqc baseA.v; coqc baseB.v
>
> and then try to compile baseC.v, it will fail
> (hopefully, since we morally defined the set of all sets),
> but when we are used to functionnal programing, we don't expect
> such an error, as something compiled can always be used...

Each module comes with a set of global universe constraints.  When you 
combine two modules their sets of universe constraints are unioned and my 
become inconsistent.

I don't find this very different than trying to compile together two 
Haskell modules that both define class instances over the same type. 
Again we have each module with some sort of global constraint.  When the 
global constraints merge there can be conflicts.  (Granted in GHC an 
error only occurs when you try to use the overlapping instances.)

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''