[Agda] Strict positivity and indices

[Dan Doel]

Greetings,

There's a recent thread on coq-club about a certain inductive definition here:

  https://sympa-roc.inria.fr/wws/arc/coq-club/2012-05/msg00032.html

The Agda equivalent is:

    data Val : Set where
      nat : ℕ -> Val
      vec : (l : List Val) -> 0 < length l -> Val

Coq rejects this as not being strictly positive. Agda doesn't complain.

If I understand the proposed explanation, it's that the second
argument has type 0 < length {Val} l, and the arguments to < are
indices, not parameters (and indices are not strictly positive
positions). So my question is: is Coq right, or is Agda?

-- Dan