Polymorphism and Inductive datatypes
This has come up on the Coq mailing list several times, but I never saw a conclusive answer. Coq isn't as general as it could be; the rules in (Coquand, 1990) and (Giménez, 1998) (and his PhD thesis) are more general and do not require strict positivity. Positivity enough is not enough, however, when you go outside Set; this example came up in several discussions:

Inductive Big : Type := B : ((B -&gt; Prop) -&gt; Prop) -&gt; Big.


With plain data structures such as yours, the inductive type would not cause problems other than making the implementation more complex.

There is a general way to define types such as this defined as the fixpoint of a polynomial:
$$F = \epsilon + \delta\, (F \times F) + \omicron\, \mathrm{id} + F \circ F$$

Instead of attempting to define the function $\mathrm{exptree} : a \mapsto \mathrm{exptree}(a)$, define the family of types $\mathrm{exptree}, \mathrm{exptree} \circ \mathrm{exptree}, \mathrm{exptree} \circ \mathrm{exptree} \circ \mathrm{exptree}, \ldots$. This means adding an integer parameter to the type that encodes the number of self-compositions ($\mathrm{exptree}^0(a) = a$, $\mathrm{exptree}^1(a) = \mathrm{exptree}(a)$, $\mathrm{exptree}^2(a) = \mathrm{exptree}(\mathrm{exptree}(a))$, etc), and a supplementary injection constructor to turn $a$ into $\mathrm{exptree}^0(a) = a$.

Inductive et : nat -&gt; Type -&gt; Type :=
  | alpha : forall a, a -&gt; et 0 a                      (*injection*)
  | omicron : forall n a, et n a -&gt; et (S n) a         (**)
  | epsilon : forall (S n) a, et (S n) a
  | delta : forall n a, et (S n) a -&gt; et (S n) a -&gt; et (S n) a
  | iota : forall n a, et (S (S n)) a -&gt; et (S n) a
.


You can proceed to define values and work on them. Coq will often be able to infer the exponent. Set Implicit Arguments would make these definitions prettier.

Definition exptree := et 1.
Definition et1 : exptree nat :=
  delta _ _ (omicron _ _ (alpha _ 42)) (epsilon _ _).
Definition et2 : exptree nat := iota _ _ (omicron _ _ et1).


You may prefer to decrease the argument by 1, so that exptree is et 0. This removes a lot of S n in the definition, which may make some proofs easier, but it requires splitting the initial case from the recurrence case in every constructor that takes an $a$ in an argument (instead of adding a single injection constructor for $a$). In this example, there's only a single constructor to split, so this should be a good choice.

Inductive et : nat -&gt; Type -&gt; Type :=
  | omicron_0 : forall a, a -&gt; et 0 a
  | omicron_S : forall n a, et n a -&gt; et (S n) a
  | epsilon : forall n a, et n a
  | delta : forall n a, et n a -&gt; et n a -&gt; et n a
  | iota : forall n a, et (S n) a -&gt; et n a
.
Definition exptree := et 0.
Definition et1 : exptree nat :=
  delta _ _ (omicron_0 _ 42) (epsilon _ _).
Definition et2 : exptree nat :=
  (iota _ _ (omicron_S _ _ et1)).


I think this is the same principle proposed in a more general form by Ralph Mattes.

References

Thierry Coquand and 
Christine Paulin. Inductively defined types. In Proceedings of COLOG'88, LNCS 417, 1990. [Springer] [Google]

Eduardo Giménez. Structural Recursive Definitions in Type Theory. In ICALP'98: Proceedings of the 25th International Colloquium on Automata, Languages and Programming. Springer-Verlag, 1998. [PDF]