[Agda] FOREIGN GHC pragma triggers parse error

Shin-Cheng Mu scm at iis.sinica.edu.tw
Mon Mar 6 15:27:58 CET 2017


Hi,

I just installed a fresh copy of Agda using cabal,
and the latest standard library. When I tried to 
load files with Agda, I get parse errors at 
FOREIGN GHC pragmas. For example, trying Data.Empty:

  agda <path to>/src/Data/Empty.agda 

<path to>/src/Data/Empty.agda:13,5-5
<path to>/src/Data/Empty.agda:13,5: Parse error
FOREIGN<ERROR>
 GHC data AgdaEmpty #-}
{-# CO...

Why would this happen?

Agda Version 2.5.2
Standard Library Version 0.13
GHC Version 8.0.1

and if these matters...

Happy Version 1.19.5
Alex version 3.2.1

Thank you!

sincerely,
Shin-Cheng Mu


More information about the Agda mailing list