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
When compiling the Agda Standard library, I get the following UHC compilation error:
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