[Agda] Datatype parameters and indices

[Andreas Abel]

[This is a candidate for a FAQ.]

That P passes but N not is an artefact of data type declarations.

Parameters are actually *absent* from constructors, so pack is really

   pack : ?A -> P ?A

for ?A to be instantiated according to the context where pack occurs. 
The syntax

   pack {A = Nat} zero

is valid, but the instantiation of parameter of A to Nat should only 
regarded as a hint to the type checker, and not an actual setting of an 
argument of pack.

In contrast, packn actually expects a first argument of type Set, which 
is too big for type N : ... -> Set, so Agda complains.

Hope that helps,

Andreas

On 25.01.13 12:05 AM, Jan Malakhovski wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/