[Agda] Datatype parameters and indices

[Jan Malakhovski]

Hello everyone,

A question that doesn't leave me for a while (like a year or so).

If I remember right, a dozen of versions ago the following code did type check.

~~~~
data P (A : Set) : Set where
  pack : A → P A

data N : Set → Set where
  packn : {A : Set} → A → N A
~~~~

Now it complains:

~~~~
The type of the constructor does not fit in the sort of the
datatype, since Set₁ is not less or equal than Set
when checking the constructor packn in the declaration of N
~~~~

I can't help but wonder about a justification for this.
It is said that parameters transform into constructors' implicit arguments, but the code above makes me think that, strictly speaking, it isn't the case.

Best regards,
  Jan