Flexible status of parameters in mutual inductive types

Relaxing the syntax of inductive types

Arguments of a block of mutual inductive types are of three kinds:

• parameters, global to all types of the block and given before the colon
• recursively non-uniform parameters, also global to all types of the block, and given after the global parameters, before the colon
• indices (called real arguments in the implementation), which are specific to each definition of the block, given after the colon

The first two classes are global in match with (i.e. they should be _ in the in clause of the match).

The last two classes are local in recursion schemes (i.e. the elimination predicate is dependent on both classes).

Except that an argument dependent on an index must be an index itself and that an argument dependent on a recursively non-uniform parameter must be a recursively non-uniform itself, it should be allowed to give the parameters in an arbitrary order and the status of the parameter inferred automatically.

The current structure has the form:

Inductive I (paramIJ:A1) (rec_non_uniform_paramIJ:A2) : forall (indexI:AI), Type := ...
with      J (paramIJ:A1) (rec_non_uniform_paramIJ:A2) : forall (indexJ:AJ), Type := ... .

But we could be more flexible, writing instead types like:

Inductive I (paramIJ:A1) (indexI:AI1) (rec_non_uniform_paramI:AI2) : Type := ...
with      J (indexJ:AJ1) (rec_non_uniform_parameterJ:AJ2) (paramIJ:A1) : Type := ... .

with an arbitrary order between the three kinds of parameters, and without requiring recursively non-uniform parameters to be the same (with same name and type) for each type of the block.

The change would require:

• to replace the registering by position into a registering by status: instead of 3 contexts in a row, it could be a single context annotated with a status; the context associated to one of the types of the block spans only over the constructors of the given type (no need to have the context being the same for all types of the block);
• to require _ in match only for the first two classes (actually, there is no reason to force a _, we could accept the return predicate to depend on the global parameter: referring to the global parameter via a variable or explicitly would not make a difference, up to conversion!);
• in elimination schemes, to have only parameters common to all types quantified globally; then, all other parameters are dependencies of the elimination predicates;
• in the syntax: to (eventually?) deprecate the syntax with indices on the right-hand side of the colon.

Note the handling of let-ins: a let-in dependent on an index should be index itself, and a let-in dependent on a recursively non-uniform parameter (and of no index) should be a recursively non-uniform parameter itself.

Note in passing that indices could now be referred using the name they have in the context of parameters:

Inductive I (n:nat) := C1 : I n | C2 : I 0.

will have the same semantics as the current:

Inductive I : nat -> Type := C1 n : I n | C2 : I 0.