The Coq mailing list

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

Le Thu, 16 Aug 2012 17:56:26 +0200 (CEST),
<kik314 AT gmail.com>
 a écrit :

> Hi,
> 
> I'm trying to avoid "Error: Universe inconsistency."
> I noticed using functor modules, instead of copy and pasting,
> may solve the error.
> 
> ---
> Module Type DummyType.
> End DummyType.
> 
> Module MyMod (D : DummyType).
> Definition id (t : Type) (x : t) := x.
> Inductive exp : Type -> Type :=
> | Const : forall T, T -> exp T.
> End MyMod.
> 
> Module D1 : DummyType.
> End D1.
> 
> Module D2 : DummyType.
> End D2.
> 
> Module M1 := MyMod D1.
> Module M2 := MyMod D2.
> ---
> 
> I got two copies of "id" and "exp" and surely they are not
> convertible. But,
> 
> ---
> Check (M1.id _ M2.id).
> Check (M1.Const (M2.Const O)).
> ---
> 
> cause "Error: Universe inconsistency." because two copies share its
> universe variables.
> Why application of functor module does not make fresh universe
> variables?

That has nothing to do with functors.

If you instantiate universe manually, you have:

Module Type DummyType.
End DummyType.

Definition TypeX := Type.
Definition TypeY := Type.
Definition TypeZ := Type.

Module MyMod (D : DummyType).
Definition id (t : TypeX) (x : t) : t := x.
Inductive exp : TypeY -> TypeZ :=
| Const : forall (T:TypeY), T -> exp T.
End MyMod.
(* Now we have TypeY < TypeZ *)

Module D1 : DummyType.
End D1.

Module D2 : DummyType.
End D2.

Module M1 := MyMod D1.
Module M2 := MyMod D2.

Now,

M1.id _ M2.id
must be expanded as
M1.id (forall (T : TypeX), T -> T) M2.id
as (forall (T : TypeX), T -> T) is the type of M2.id
but for same reasons, the first argument of M1.id needs to be of type
TypeX.

So you have to check the constraint '(forall (T:TypeX), T -> T) :
TypeX' which does not hold.

I guess you previously tried 'M1.id _ M1.id' which also failed (for
exactly the same reasons) and then tried to trick Coq, with a second
module, hoping to break some self-depndendency.

Your second problem was pretty much about the same thing.

In fact to break things, you should need to make modules dependant of a
universe, like (which is impossible in Coq):

Module MyMod <TypeX TypeY TypeZ : Universe>.
Definition id (t : TypeX) (x : t) : t := x.
Inductive exp : TypeY -> TypeZ :=
| Const : forall (T:TypeY), T -> exp T.
End MyMod.

Definition Type1 := Type.
Definition Type2 := Type.
Module M1 := MyMod<Type1, Type, Type>.
Module M2 := MyMod<Type2, Type, Type>.

So that you colud write "M1.id _ M2.id", thus adding the constraint
Type2<Type1.