The Coq mailing list

[kik <kik314 AT gmail.com>]

Thanks!

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

Yes.  This solves the problem.
But explicit universe is not the way of Coq.

Is it correct there are no way to copy definitions without explicit
copy and pasting to avoid universe inconsistency?
I think adding command which copies modules (or some code region) with
new universe variables makes it more easy to define some higher order
construct.
I also think this method is far from elegance.

2012/8/17 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.