Auto missing support for Copatterns

[GoogleCodeExporter]

git clone git@github.com:andreasabel/cubical.git -b 0.0.0.1

Load cubical/src/Control/Auto-Bug-in-Goal-2.agda

Fix the module name (should be Control.Auto-Bug-in-Goal-2).
Go to the second goal (?1).
Press C-c C-a.

An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/Auto/Convert.hs:585

Original issue reported on code.google.com by andreas....@gmail.com on 13 Nov 2013 at 10:03

[GoogleCodeExporter]

This gives a proper error now.  TODO: make Agsy work with copatterns.

Original comment by andreas....@gmail.com on 22 Nov 2013 at 9:46

• Changed title: Auto missing support for Copatterns
• Added labels: Type-Enhancement
• Removed labels: Type-Defect

[GoogleCodeExporter]

I talked to Fredrik today and he thinks it is not worth spending time on the 
current Auto since he has a new one.  He will do this after his thesis 
submission (sometime in Feb maybe)?

So, no milestone for 2.3.4.

Original comment by andreas....@gmail.com on 29 Nov 2013 at 3:38

• Removed labels: Milestone-2.3.4

[GoogleCodeExporter]

Original comment by andreas....@gmail.com on 29 Nov 2013 at 3:39

[isovector]

Without knowing anything about the internals, this feels like a rather arbitrary limitation. What would be necessary to get copatterns supported here?

[andreasabel]

What would be necessary to get copatterns supported here?

Understand and extend the Agda.Auto.* implementation. No one has been willing to do that; Auto is bit-rotting. If you look at the code, you might understand why.
@UlfNorell has a student working on a new term synthesizer.