Unexpected "GRIN ByteCode location names not in scope"

[phile314]

When compiling the Agda Standard library, I get the following UHC compilation error:

[124/238] Compiling Core                 Agda.Relation.Binary.Product.Pointwise (Agda/Relation/Binary/Product/Pointwise.bcr)
Compilation error:
Grin to ByteCode
(Internal) GRIN ByteCode location names not in scope:
  Agda.Relation.Binary.Product.Pointwise.x141_@UNQ_@195_@FFE_@nl.uu.agda.fresh-local-name

I have looked at the corresponding UHC Core file, and the code there looks fine to me.
Pointwise.tcr.txt
The core dump uses a slightly different pretty printer for the names, but searching for x141
should yield the interesting occurences.

If I compile using -O0, everything works fine and the produced binary executes successfully. Omitting the -O0 option, the above error happens. I don't have a minimal example, the code triggering this depends on 124 other Agda modules. I also don't have a Haskell file triggering this. I tested using UHC 1.1.9.3.

Related Agda issue: agda/agda#1879

[asr]

I could reproduce the error in the OP using UHC 1.1.9.4. Any ideas?

[atzedijkstra]

I have not yet looked into this (and have less time doing so coming weeks...). My usual way of finding out where it goes wrong is to build variant 99 (make 99/ehc;make 99/ehclib; install/bin/99/ehc --help # look for "dump") which allows dumping of intermediate core/grin transformation stages. Usually something goes wrong there. It is then a matter of finding out where Core/Grin is still correct and is transformed to something incorrect (as the front end code generation is not used in this issue). I suspect there will be a erroneous code float.

A

On 23 May 2016, at 10:45, Andrés Sicard-Ramírez notifications@github.com wrote:

I could reproduce the error in the OP using UHC 1.1.9.4. Any ideas?

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly or view it on GitHub

[atzedijkstra]

The given .tcr file is not parseable. In general the full dump language is richer than what the parser for .tcr files accepts. Could you provide a .bcr file, i.e. a binary dump?