Agda 错误：使用 --guardedness 标志从不支持的模块导入模块 IO

Question

我这个例子取自 Agda 文档

module hello-world-prog where

open import IO

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

但是当我运行 Ctrl+c、Ctrl+x、Ctrl+c 并输入 GHC 时，出现以下错误：

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

错误消息非常不言自明：

IO

模块有

--guardedness

标志，但你的模块没有，Agda认为这是一个错误。

您可以通过添加来进行类型检查

{-# OPTIONS --guardedness #-}

到文件顶部。

如果您好奇为什么现在默认情况下关闭防护，您可以在this问题中找到详细信息。