[Agda] Agda's copatterns incompatible with initial algebras

[Andrea Vezzosi]

Hi Dmitriy,

Indeed there is a bug here [1] about sizes, you shouldn't be able to define

shd wit = inn wit

because inn requires the result size to increase.

Cheers,
Andrea

[1] https://code.google.com/p/agda/issues/detail?id=1201

On Wed, Jun 18, 2014 at 9:07 PM, Dmitriy Traytel <traytel at in.tum.de> wrote:
> Dear Agda developers,
>
> today, I was able to prove false in Agda using copatterns and sized types
> only (attached). Is my assumption, that those two extensions are supposed to
> work together properly, correct?
>
> Especially, the definition of "wit" that refers to itself in order to
> produce its own head looks fishy. I would have expected that something would
> prevent me from doing this.
>
> This is my first proof in Agda, so please apologize if the example is not as
> simplified as possible. The proof (and this email's title) is based on the
> examples that exhibit the incompatibility of sized types and the "musical
> coinduction" from [1] (of course replacing the "musical coinduction" by
> copatterns).
>
> Or am I doing something completely wrong?
>
> Cheers,
> Dmitriy
>
> [1] https://lists.chalmers.se/pipermail/agda/2011/003337.html
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>