[Agda] Using the latest versions

[Eelco Lempsink]

Hi,

I'm having some problems using the latest standard libraries and  
latest version of Agda.  I probably shouldn't have upgraded so  
enthusiastically, the cutting edge does hurt.

1. Parsing problems (it works when using interactive mode and I also  
upgrade the agda-executable).
> § agda -i ../agda-lib/  
> problem.agda                                       1
> Checking Data.Vec ( /Users/eelco/Archive/Studie/Afstuderen/agda-lib/ 
> Data/Vec.agda )
> /Users/eelco/Archive/Studie/Afstuderen/agda-lib/Data/Vec.agda:20,18-18
> /Users/eelco/Archive/Studie/Afstuderen/agda-lib/Data/Vec.agda:20,18:
> Parse error :<ERROR> a) (xs : Vec a n) → Vec a (su...

2. Type wierdness.  Using the following code...
> module problem where
>
> open import Data.Vec
> open import Data.Nat
>
> data Item : Set where
>   aap  : Item
>   noot : Item
>   mies : Item

2.1
> Map : ℕ -> Set
> Map n = Vec Item n

Gives the error (ℕ is red and underlined)
> Set !=< _6
> when checking that the expression ℕ has type _6

2.2
> Map : Set
> Map = Vec Item 42

Gives the error (Item is red and underlined)
> Set !=< Set
> when checking that the expression Item has type Set

2.3
> Map : Set
> Map = Vec ℕ 10

Gives the error (Vec ℕ 10 is red and underlined)
> Set !=< Set
> when checking that the expression Vec ℕ 42 has type Set

All 2.x the problems go away when using --type-in-type, but that's a  
workaround, not a solution.  Is this a bug, or is it just me?

-- 
Regards,

Eelco Lempsink

-------------- next part --------------
A non-text attachment was scrubbed...
Name: PGP.sig
Type: application/pgp-signature
Size: 194 bytes
Desc: This is a digitally signed message part
Url : https://lists.chalmers.se/mailman/private/agda/attachments/20090121/9ae2b919/PGP.bin