agdaagda-mode

Agda error: Importing module IO using the --guardedness flag from a module which does not

I have this example taken from the Agda documentation

module hello-world-prog where

open import IO

main : Main
main = run (putStrLn "Hello, World!")

But when I run Ctrl+c, Ctrl+x, Ctrl+c and enter GHC, I get the following error:

C:\Users\myname\Documents\Agda\hello-world-prog.agda:3,1-15
Importing module IO using the --guardedness flag from a module
which does not.
when scope checking the declaration
  open import IO
Solution

  • The error message is pretty self-explanatory: the IO module has the --guardedness flag, but your module doesn't and Agda consider this to be an error.

    You can make it type check by adding

    {-# OPTIONS --guardedness #-}

    to the top of the file.

    If you're curious why guardedness is now turned off by default, you can find details in this issue.