[Agda] New version of agda

[Anton Setzer]

Hi,

after experimenting a bit with the new syntax of Agda under windows
(which really installs amazingly easy, that's an excellent
windows installer),
I found that there seem to be some problems with it.


Consider the following inconsistent code:

-- Begin

C (!A:: Set) :: Set 
             = sig{ fst :: A}


c (!A:: Set)(a::A):: C A
                  = struct{ fst:: A = a}

a0 (!A :: Set)
   :: C A
   = c A

a (!A :: Set)
  :: A
  = (a0 A).fst

-- End

This code compiles, passes the termination checker,
but has an invisible open goal. 
The mistake in this code is that the hidden argument
of c should have been a::A instead of A :: Set
(this example was extracted from the 
big-examples.agda on the agda homepage, where
the signature of

prod (!A, !B::Set)(a::A)(b::B):: A*B =

was wrong).

However, the problem is not that the signature was
chosen correctly, but that Agda didn't notice it.

c (!A:: Set)(a::A):: C A
                  = struct{ fst:: A = a}

shouldn't type check, since the a in the body
of the function cannot be inferred from the 
non-hidden arguments. 

(By the way in line 260 of big-examples.agda
there occur currently three of these hidden 
goals - this indicates that this is a real 
source of mistakes).



Anton