[Agda] Bug in simplification?

[Philip Wadler]

Why does the attached not work? Is there a workaround, or a repair on the
horizon? Note particularly the "1" in the error message, which appears
spurious. Cheers, -- P

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180317/a05824b7/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: DecidableBroken.agda
Type: application/octet-stream
Size: 1123 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180317/a05824b7/attachment.obj>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180317/a05824b7/attachment.ksh>