[Agda] Agda's copatterns incompatible with initial algebras

[Andreas Abel]

Actual, Dmitriy has found a different bug.  It is a bug in the untyped 
guardedness check.

   wit : Stream (Mu-Stream ∞)
   shd wit = inn wit
   stl wit = wit

Since (shd wit) is not a recursive position for streams, the recursive 
call to wit should be banned here.  Only (stl wit) is a recursive position.

   https://code.google.com/p/agda/issues/detail?id=1209

Thanks for spotting!

Andreas

On 19.06.2014 15:26, Andrea Vezzosi wrote:
> 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
>>>>
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


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

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

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