[Agda] The sort of a datatype cannot depend on its indices

[Ulf Norell]

On Thu, Feb 4, 2010 at 10:03 PM, Chris Casinghino <
chris.casinghino at gmail.com> wrote:

> Hi all,
>
> I triggered the error in the subject line by trying to define a
> datatype whose Sort depended on one of its indices.  I'm curious about
> this restriction: is there a theoretic reason for it or was it just a
> matter of convenience in the implementation.
>

Both, I would say. I have no idea what the theory for such a datatype would
be, and it would mean more work when checking levels of datatypes.

At the moment to check the level of a datatype we check that all the
constructor
arguments have types that fit inside the target level of the datatype. With
your datatype this level might be different for each constructor and it
depends
on the values of the constructor arguments.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100205/d6ca7768/attachment.html