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

Question

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

Answer 1

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.