The Coq mailing list

[<kik314 AT gmail.com>]

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?