Unresolved metas in for run in Agda hello-world

1
votes

I tried to compile the hello-world example with Agda 2.6.1.3 and Agda stdlib 1.5. Below is the code:

module hello-world where

open import IO

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

When compiling with Agda (agda --compile hello-world.agda), the following error is reported:

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

The reported position (5,8-11) corresponds to token run.

I did not find any related information in both Agda and Agda-stdlib Issues, nor on SO or other websites. Is the documentation out-dated, or did I make any mistakes?

Note:

  • The Agda compiler is installed with stack install Agda with resolver lts-17.5.
  • I also tried manually compiling from GitHub sources (branch release-2.6.1.3).
  • In $HOME/.agda/libraries I have: 
    $HOME/agda-stdlib/standard-library.agda-lib
  • In $HOME/.agda/defaults I have: 
    standard-library
1
agdaagda-stdlib

1 Answers

4
votes

This is the problem described in the comment at https://github.com/agda/agda/issues/4250#issuecomment-771806949. The current workaround is to add an implicit argument to run as follows:

module hello-world where

open import IO
open import Level

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

This issue will be fixed in the upcoming release of Agda 2.6.2 and the next version of the standard library.