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:
stack install Agda
with resolver lts-17.5
.release-2.6.1.3
).$HOME/.agda/libraries
I have:
$HOME/agda-stdlib/standard-library.agda-lib
$HOME/.agda/defaults
I have:
standard-library
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.