[Agda] Codata oddity

[Conor McBride]

Hi Andreas

On 6 Jun 2008, at 19:33, Andreas Abel wrote:

> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA1
>
> Nils Anders Danielsson wrote:
>>
>>   p : ω ≡ cons ω
>
> I think that
>
>     p = refl
>
> should type check, since it leads to checking definitional equality of
>
>     w == cons w

Well, quite.

So there's currently a mismatch between the
fact that case computes in a supply-driven
manner (if it can unfold, it will), but
definitional comparison with a coconstructor
does not cause a corresponding unfolding.
One can fix this either by making the former
lazier or the latter more energetic. They
certainly need to be compatible. I suspect
both are possible with a suitable setup, and
hence that the latter is preferable as you
suggest.

The questions, I suppose, are

(1) Is the proposed unfolding strategy
   ok, or at least fixable? Does my

   fred ~ cons fred
   jim ~ cons fred

   example pass the productivity check?
   If so, how do we ensure that fred == jim ?

   Can we always figure out how far to
   unroll to get an intensional match?

(2) Even if it is ok, is it enough to
   solve the general problem, not just this
   instance of it? Suppose we have

     out P1 = P1
     ...
     out Pn = Pn

   for some big complex covering of patterns.
   We can define

     proof x : out x = x

   by splitting x to that covering and giving
   refl in all cases. Now take a tight loop

     y ~ c y .. y

     proof y : out y = y

   proof y will compute to refl by unfolding
   y as much as necessary; out y will compute
   the same amount; the definitional equality
   will unfold y accordingly, so refl checks.
   Good! But I still don't understand it.

By the way, we shouldn't get distracted by
the use of the identity type to expose
difficulties with the definitional equality.
I expect this problem bites just as well
if you want

   \ p -> p : P w -> P (cons w)

What fun!

All the best

Conor