The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

The simplest example of universe inconsistency which I was able to produce 
(without the use of Set or inductive definitions) is:

Variable var1: forall T:Type, forall t:T, Type.
Variable var2: var1 (forall T: Type, forall t:T, Type) var1.

The effect which your example shows is unavoidable. A context in Coq 
corresponds to (as far as I understand) a pair (U, Gamma) where U is a 
"universe scheme" and Gamma is a context in a type system defined by U. A 
universe scheme is the (finite) set whose elements define the different 
universes required to make sense of the given Coq-context together with two 
distinguished elements (Prop, Set) and two binary relations u_1<=u_2 
corresponding to"every member of u_1 is a member of u_2" and  u_1<<u_2 
corresponding to "u_1 is a member of u_2". There is a bunch of conditions 
which this structure has to satisfy in order to be acceptable ("acyclicity") 
and not to generate "universe inconsistency".

In your situation you add up "baseA" and "baseB" which already have a common 
intersection "base". When you do this the universe schemes are combined and 
the combination is not acyclic anymore.  

Vladimir.


PS What is {| ... |} ?? I think the meaning is clear but where is it 
described in the manual?

On Jan 19, 2010, at 8:32 AM, AUGER wrote:

> Hi all,
> I found a coq feature which doesn't seem natural:
> 
> Create 3 files:
> 
> -------------------------------------------
> (*base.v*)
> Record A :=
> { S: Type;
>  Eq: S -> S -> Prop
> }.
> 
> Record B :=
> { S': Type;
>  Eq': S' -> S' -> Prop
> }.
> -------------------------------------------
> (*baseA.v*)
> Require base.
> 
> Definition As :=
> {| base.S' := base.A;
>   base.Eq' := fun a b => a = b
> |}.
> -------------------------------------------
> (*baseB.v*)
> Require base.
> 
> Definition Bs :=
> {| base.S := base.B;
>   base.Eq := fun a b => a = b
> |}.
> -------------------------------------------
> (*baseC.v*)
> Require baseA.
> Require baseB.
> -------------------------------------------
> compile all:
> 
> 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...
> 
> -- 
> Cédric AUGER
> 
> Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay