<div dir="ltr"><div>That program delivered the error in context, but I discovered it does not deliver the error after re-starting Agda. Nor can I create a program that does. It appears to be a heisenbug. That won't be enough to track it down. Sorry. -- P</div><div><br></div><div><div><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div><div dir="ltr"><br></div><div>Too brief? Here's why: <a href="http://www.emailcharter.org/" target="_blank">http://www.emailcharter.org/</a></div></div></div></div></div></div><br></div></div><br><div class="gmail_quote"><div dir="ltr">On Thu, 20 Sep 2018 at 21:13, Philip Wadler <<a href="mailto:wadler@inf.ed.ac.uk">wadler@inf.ed.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div dir="ltr"><div>Attached program gives the message:</div><div><br></div><div>An internal error has occurred. Please report this as a bug.<br>Location of the error: src/full/Agda/TypeChecking/Serialise/Instances/Common.hs:178</div><div><br></div><div>Cheers, -- P<br></div><div><br></div><div><div dir="ltr" class="m_4374092152579954206gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div><div dir="ltr"><br></div><div>Too brief? Here's why: <a href="http://www.emailcharter.org/" target="_blank">http://www.emailcharter.org/</a></div></div></div></div></div></div></div></div>
</blockquote></div>