The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

What is the reason to forbid such an inductive:

Inductive foo A : Type :=
| Nfoo : A → bar nat → foo A
| Afoo : A → foo A

with bar B : Type :=
| Nbar : B → bar bool → bar B
| Bbar : B → foo B → bar B
.

I know there are 3 kinds of arguments to an inductive:

* indices, the most versatile, always work but often a pain in the neck
  to deal with
* "true" parameters, that is the whole structure depends on them, and
  they cannot be modified along the calls
* "false" parameters, which somewhere between indices and true
  parameters, they can vary along the calls but are forced for the type
  of closed constructors

To illustrate this:

✂✂✂✂✂✂✂
Inductive eq (A:Type) (a:A) : A → Prop := eq_refl : eq a a.

(A:Type) and (a:A) are "true" parameters, but the A in the A→Prop is an
indice.
✂✂✂✂✂✂✂
Inductive Acc (A : Type) (R : A → A → Prop) (x : A) : Prop :=
    Acc_intro : (forall y : A, R y x → Acc R y) → Acc R x

A and R are "true" parameters.
x is a "false" parameter (and worse than that, "R y x" generally
forbids to have x=y ^^).
✂✂✂✂✂✂✂

In my foo/bar example, A and B cannot be "true" parameters, so they can
be either "false" or indices. Setting them as indices work of course,
but are not convenient, and Coq does not want to use them as
parameters, since signature of bar and signature of foo differs.
In fact, I understand this restriction for "true" parameters, but I
think that it should be relaxed for "false" parameters. At least, I
have no example in mind where it would be inconsistant to allow it.