<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body>
    <p>I got the same bug, with 2.6.1.</p>
    <p>But restarting agda, I fix it.</p>
    <p>Perhaps I did not install Agda in an orthodox way !<br>
    </p>
    <p>Cheers,</p>
    <p>Pierre<br>
    </p>
    <div class="moz-cite-prefix">Le 25/02/2019 à 12:45, Guillaume Allais
      a écrit :<br>
    </div>
    <blockquote type="cite"
      cite="mid:67b89280-6216-1b59-0b75-e541c830d44d@ens-lyon.org">
      <pre class="moz-quote-pre" wrap="">Hi Phil,

This particularly annoying bug has been fixed in 2.5.4.2:
<a class="moz-txt-link-freetext" href="https://github.com/agda/agda/issues/3199">https://github.com/agda/agda/issues/3199</a>

Cheers,
--
gallais

On 25/02/2019 00:31, Philip Wadler wrote:
</pre>
      <blockquote type="cite">
        <pre class="moz-quote-pre" wrap="">I am getting a strange bug.

An internal error has occurred. Please report this as a bug.
</pre>
        <blockquote type="cite">
          <pre class="moz-quote-pre" wrap="">Location of the error:
src/full/Agda/TypeChecking/Serialise/Instances/Common.hs:178
</pre>
        </blockquote>
        <pre class="moz-quote-pre" wrap="">

Relevant source files attached. The error occurs in CoercionsS.lagda.

What is the best way to report this, please?   -- P


.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. <a class="moz-txt-link-freetext" href="http://homepages.inf.ed.ac.uk/wadler/">http://homepages.inf.ed.ac.uk/wadler/</a>


The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.


_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>

</pre>
      </blockquote>
      <pre class="moz-quote-pre" wrap="">
</pre>
      <br>
      <fieldset class="mimeAttachmentHeader"></fieldset>
      <pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
    </blockquote>
    <pre class="moz-signature" cols="72">-- 
Cordialement,

---------------------------
Pierre Lescanne (Professeur émérite)
LIP / ENS de Lyon
46 allée d'Italie
69364 LYON Cedex 07, France
tél: +33 6 85 70 94 31
<a class="moz-txt-link-freetext" href="http://perso.ens-lyon.fr/pierre.lescanne/">http://perso.ens-lyon.fr/pierre.lescanne/</a>
---------------------------</pre>
  </body>
</html>