[Agda] defining coinductive types

[Wojciech Jedynak]

Hello,

> Ok, I see.  Is it known that supporting non-strictly positive types would
> have bad consequences in Agda?  Not that I am suggesting it -- I am just
> curious about what might be possible.

Yes, it's possible to write a non-terminating expression using such a
type. For instance, take a look here:
<http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.BadInHaskell>

Best,
Wojtek