[Agda] Agda's copatterns incompatible with initial algebras

[Andrea Vezzosi]

Right, unfortunately the rule in question is what's allowing "tail :
Stream ∞ -> Stream ∞" and "suc : ℕ ∞ → ℕ ∞" to typecheck at the
moment, so we need to find an alternative.

By the way, it would be interesting to figure out if there are similar
problems arising when we use the sizes for coinduction instead.

On Thu, Jun 19, 2014 at 11:48 AM, Dmitriy Traytel <traytel at in.tum.de> wrote:
> So I was just one day late.  Good to know that this issue worked on.
>
> Thanks for the pointer, Andrea. Next time I'll check the bug tracker first.
>
> Cheers,
> Dmitriy
>
> Am 19.06.2014 10:57, schrieb 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
>>>
>