I can define the following inductive type:
Inductive T : Type -> Type :=
| c1 : forall (A : Type), A -> T A
| c2 : T unit.
But then the command Check (c1 (T nat))
fails with the message: The term T nat
has type Type@{max(Set, Top.3+1)}
while it is expected to have type Type@{Top.3}
(universe inconsistency).
How can I tweak the above inductive definition so that c1 (T nat)
does not cause a universe inconsistency, and without setting universe polymorphism on?
The following works, but I would prefer a solution without adding equality:
Inductive T (A : Type) : Type :=
| c1 : A -> T A
| c2' : A = unit -> T A.
Definition c2 : T unit := c2' unit eq_refl.
Check (c1 (T nat)).
(*
c1 (T nat)
: T nat -> T (T nat)
*)
Let me first answer the question of why we get the universe inconsistency in the first place.
Universe inconsistencies are the errors that Coq reports to avoid proofs of False
via Russell's paradox, which results from considering the set of all sets which do not contain themselves.
There's a variant which is more convenient to formalize in type theory called Hurken's Paradox; see Coq.Logic.Hurkens
for more details. There is a specialization of Hurken's paradox which proves that no type can retract to a smaller type. That is, given
U := Type@{u}
A : U
down : U -> A
up : A -> U
up_down : forall (X:U), up (down X) = X
we can prove False
.
This is almost exactly the setup of your Inductive
type. Annotating your type with universes, you start with
Inductive T : Type@{i} -> Type@{j} :=
| c1 : forall (A : Type@{i}), A -> T A
| c2 : T unit.
Note that we can invert this inductive; we may write
Definition c1' (A : Type@{i}) (v : T A) : A
:= match v with
| c1 A x => x
| c2 => tt
end.
Lemma c1'_c1 (A : Type@{i}) : forall v, c1' A (c1 A v) = v.
Proof. reflexivity. Qed.
Suppose, for a moment, that c1 (T nat)
typechecked. Since T nat : Type@{j}
, this would require j <= i
. If it gave us that j < i
, then we would be set. We could write c1 Type@{j}
. And this is exactly the setup for the variant of Hurken's that I mentioned above! We could define
u = j
U := Type@{j}
A := T Type@{j}
down : U -> A := c1 Type@{j}
up : A -> U := c1' Type@{j}
up_down := c1'_c1 Type@{j}
and hence prove False
.
Coq needs to implement a rule for avoiding this paradox. As described here, the rule is that for each (non-parameter) argument to a constructor of an inductive, if the type of the argument has a sort in universe u
, then the universe of the inductive is constrained to be >= u
. In this case, this is stricter than Coq needs to be. As mentioned by SkySkimmer here, Coq could recognize arguments which appear directly in locations which are indices of the inductive, and disregard those in the same way that it disregards parameters.
So, to finally answer your question, I believe the following are your only options:
Set Universe Polymorphism
so that in T (T nat)
, your two T
s take different universe arguments. (Equivalently, you can write Polymorphic Inductive
.):
to before it.)-type-in-type
to entirely disable universe checking.False
in the process. (Possibly involving module subtyping, see, e.g., this recent bug in modules with universes.))