Agda编译报错：导入IO模块需--guardedness标志（官方示例问题）

错误原因 #

该报错源于IO模块依赖**guardedness（受限递归）**编译特性，但当前Agda模块未启用该标志，导致无法正常导入模块。

修复方案 #

在模块声明前添加启用--guardedness标志的指令，修改后的完整代码如下：

{-# OPTIONS --guardedness #-}
module hello-world-prog where

open import IO

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

兼容旧版本说明 #

若使用Agda 2.6.1及更早版本，可改用IO.Primitive模块（无需额外编译标志），代码示例：

module hello-world-prog where

open import IO.Primitive

main : Main
main = putStrLn "Hello, World!"

内容的提问来源于stack exchange，提问作者Werner Germán Busch