[Agda] Datatype parameters and indices

Jan Malakhovski oxij at oxij.org
Fri Jan 25 00:05:39 CET 2013

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,

More information about the Agda mailing list