[Agda] Status of copatterns

[Francesco Mazzoli]

Hi list,

After attending a talk by Andreas Abel on copatterns I have been trying them out
today and in my opinion they improve considerably the usability of coinduction.
I always felt the ‘manual’ coinduction that Agda currently provides is pretty
clunky while copatterns feel much more ‘right’.

However, there are a couple of problems in the current implementation which make
copatterns not that usable:

* Holes don’t work properly, see
  <https://code.google.com/p/agda/issues/detail?id=742>
* ‘where’ is unimplemented

Now, some problems are to be expected in such an early stage, however a comment
by Andreas on the mentioned bug caught my eye:

   Probably can be fixed, but how much should I invest into this throw-away
   code?

Does this mean that the current implementation is going to be replaced by a
better one, or does it mean that the future of copatterns is uncertain?  In the
latter case, what are the roadblocks that make copatterns problematic?

Thanks,
Francesco