The Coq mailing list

[Peter LeFanu Lumsdaine <p.l.lumsdaine AT gmail.com>]

I’m rather confused about what should happen when parameters occur
non-uniformly in constructors in inductive definitions.  The manual
says (version 8.3pl1, section 4.5, p111):

> Since COQ version 8.1, there is no restriction about parameters in the 
> types of
> arguments of constructors. The following definition is valid:

----8<---
Inductive list’ (A:Set) : Set :=
 | nil’ : list’ A
 | cons’ : A -> list’ (A->A) -> list’ A.
----8<---

When I run this definition through Coq, it does accept it, but seems
to deal with it just by treating A as an index rather than a
parameter.  That is, the resulting recursor has type

----8<---
list'_rect
     : forall P : forall A : Set, list' A -> Type,
       (forall A : Set, P A (nil' A)) ->
       (forall (A : Set) (a : A) (l : list' (A -> A)),
        P (A -> A) l -> P A (cons' A a l)) ->
       forall (A : Set) (l : list' A), P A l
----8<---

which is what I’d expect with A an index — it is not itself
universally quantified over all A:Set, but instead requires that the
predicate into which we eliminate is so quantified.  (And it’s the
same as what you get if you rewrite the definition with A as an index,
[Inductive list' : Set -> Set := …].)

In the manual’s own words on the difference between parameters and indices:

> The information which says that for any A, (List A) is an inductively 
> defined Set
> has been lost.

Am I misunderstanding something about the difference between
parameters and indices, or what is going on here?

The behaviour of Coq here makes more sense to me than what is
advertised in the manual: I can’t see how you really could let
parameters occur unrestrictedly in constructors like that, and can’t
see what other recursor there could be.  But again, I may be
misunderstanding how the distinction between parameters and indices
extends to the non-uniform case.

I would also be interested in any pointers to the literature on
non-uniform parameters — I haven’t been able to find any.

–p.