[Agda] Codata oddity

[Andreas Abel]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Nils Anders Danielsson wrote:
> The current implementation of codata seems to be a bit problematic.
> The following program was suggested by Nicolas Oury:
> 
>   data _≡_ {a : Set} (x : a) : a -> Set where
>     refl : x ≡ x
> 
>   codata Stream : Set where
>     cons : Stream -> Stream
>
>   ω : Stream
>   ω ~ cons ω
> 
>   p : ω ≡ cons ω

I think that

    p = refl

should type check, since it leads to checking definitional equality of

    w == cons w

Well, then you chose to allow unrolling of the lhs, so we get

    cons w == cons w

and finally

    w == w

which holds by a reflexivity check.

Where do I get into problems then?

Cheers,
Andreas

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

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFISYMIPMHaDxpUpLMRAsLgAJ9G0wjeaEBCwxGfTke4R6y3wTCbkACg78Zw
/6WWmgL3/nf4GRcN5ptPSFQ=
=WXl2
-----END PGP SIGNATURE-----