[Agda] Bug report

[Philip Wadler]

Attached program gives the message:

An internal error has occurred. Please report this as a bug.
Location of the error:
src/full/Agda/TypeChecking/Serialise/Instances/Common.hs:178

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/

Too brief? Here's why: http://www.emailcharter.org/

[Philip Wadler]

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

. \ 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/

Too brief? Here's why: http://www.emailcharter.org/

Post by Philip Wadler
An internal error has occurred. Please report this as a bug.
src/full/Agda/TypeChecking/Serialise/Instances/Common.hs:178
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/
Too brief? Here's why: http://www.emailcharter.org/

[Guillaume Allais]

Hi Phil,

We are about to release 2.5.4.2 and it should contain a fix for it!
If you're in a hurry, you can install the dev version after commit:
https://github.com/agda/agda/commit/6349949acc7dfaeac5fe814e2b60c30edfae43c2

issue on the tracker: https://github.com/agda/agda/issues/3199
2.5.4.2 to be released: https://github.com/agda/agda/issues/3228

Cheers,
--
gallais

Post by Philip Wadler
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
. \ 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/
Too brief? Here's why: http://www.emailcharter.org/

Post by Philip Wadler
An internal error has occurred. Please report this as a bug.
src/full/Agda/TypeChecking/Serialise/Instances/Common.hs:178
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/
Too brief? Here's why: http://www.emailcharter.org/

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda