agdaagda-stdlib

Unresolved metas in for run in Agda hello-world


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:


Solution

  • 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.