Polymorphism and Inductive datatypes

I'm curious. I've been working on this datatype in OCaml:

type 'a exptree =
  | Epsilon
  | Delta of 'a exptree * 'a exptree
  | Omicron of 'a
  | Iota of 'a exptree exptree

Which can be manipulated using explicitly typed recursive functions (a feature that has been added quite recently). Example:

let rec map : 'a 'b. ('a -> 'b) -> 'a exptree -> 'b exptree =
  fun f ->
    begin function
    | Epsilon -> Epsilon
    | Delta (t1, t2) -> Delta (map f t1, map f t2)
    | Omicron t -> Omicron (f t)
    | Iota tt -> Iota (map (map f) tt)
    end

But I've never been able to define it in Coq:

Inductive exptree a :=
  | epsilon : exptree a
  | delta : exptree a -> exptree a -> exptree a
  | omicron : a -> exptree a
  | iota : exptree (exptree a) -> exptree a
.

Coq is whining. It doesn't like the last constructor, and says something I don't completely understand or agree with:

Error: Non strictly positive occurrence of "exptree" in "exptree (exptree a) -> exptree a".

What I can understand is that inductive types using a negation inside their definition like type 'a term = Constructor ('a term -> …) are rejected, because they would lead to ugly non well-founded beasts like (untyped) λ-terms.
However this particular exptree datatype seems innocuous enough: looking at its OCaml definition, its argument 'a is never used in negative positions.

It seems that Coq is overcautious here.
So is there really a problem with this particular inductive datatype?
Or could Coq be slightly more permissive here?

Also, what about other proof assistants, are they able to cope with such an inductive definition (in a natural way)?

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 -> Prop) -> Prop) -> 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 -> Type -> Type :=
  | alpha : forall a, a -> et 0 a                      (*injection*)
  | omicron : forall n a, et n a -> et (S n) a         (**)
  | epsilon : forall (S n) a, et (S n) a
  | delta : forall n a, et (S n) a -> et (S n) a -> et (S n) a
  | iota : forall n a, et (S (S n)) a -> 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 -> Type -> Type :=
  | omicron_0 : forall a, a -> et 0 a
  | omicron_S : forall n a, et n a -> et (S n) a
  | epsilon : forall n a, et n a
  | delta : forall n a, et n a -> et n a -> et n a
  | iota : forall n a, et (S n) a -> 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]

StackExchange Computer Science Q#851, answer score: 9