[Agda] Perplexed by compile behavior

[Chris Moline]

I've been trying to agda but I'm stumped by compiling a simple hello world
application.

In emacs the file loads without error but when I try to compile it with the
command line program I get this:


...
Compiling Learn in /home/cmo/src/agda/Learn/Learn.agdai to
/home/cmo/src/agda/Learn/MAlonzo/Code/Learn.hs

The type of main should be .IO.Primitive.IO A, for some A. The
given type is .IO.IO .Data.Unit.[~/src/agda/Learn] $



My hello world application looks like this:


module Learn where

open import Data.String
open import Data.Unit
open import IO

main : IO ⊤
main = putStrLn "hello"



The script that I'm using to compile the file is:

agda -c \
     -i "." \
     -i ~/.cabal/lib/Agda-2.3.2.1/ghc-7.6.3 \
     -i ~/src/agda/lib-0.7/src \
      $@

My ghc version is 7.6.3 and agda is version 2.3.2.1.

I'm really perplexed by the behavior of the agda programs. In the beginning
the same program I gave above would end with a parse error at eof. Then
that magically stopped. Then the compile would break without giving an
error message. It turned out that I gave main the type : String -> IO T but
still no error message? . Now finally I have the above error. I realize
that agda is in its early stages so it's no big deal, I just have no idea
why a simple program gives so much trouble.

Anyways I hope someone will give me advice as to what I'm doing wrong.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130823/b3b76a0f/attachment.html