Agda hello-world 中运行的未解析元数据

Question

我试图编译hello-world example with Agda 2.6.1.3 and Agda stdlib 1.5。下面是代码：

module hello-world where

open import IO

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

使用Agda(agda --compile hello-world.agda)编译时，报如下错误：

Unsolved metas at the following locations:
  $HOME/hello-world.agda:5,8-11

报告的位置（5,8-11）对应令牌run。

我没有在 Agda 和 Agda-stdlib Issues 中找到任何相关信息，也没有在 SO 或其他网站上找到任何相关信息。是文档过时了，还是我有什么错误？

注：

在 $HOME/.agda/libraries 我有：

$HOME/agda-stdlib/standard-library.agda-lib

Answer 1

这是 https://github.com/agda/agda/issues/4250#issuecomment-771806949 评论中描述的问题。当前的解决方法是向 run 添加隐式参数，如下所示：

module hello-world where

open import IO
open import Level

main = run {0ℓ} (putStrLn "Hello, World!")

此问题将在即将发布的 Agda 2.6.2 版本和下一版本的标准库中修复。

Agda hello-world 中 运行 的未解析元数据