#5 funny error

[somebody]

type checking this code:

data Nat = zer | suc (m::Nat)

plus (m::Nat) (n::Nat)::Nat =
case m of
(zer )-> n
(suc m')-> suc (plus m' n)

gives the error:

Error in the definition of plus because:
More function arguments than the function type specifies: plus

in:

Agda with idata and implicit arguments / ver. 1.0.1

[ghc604; built Dec 8 2006 16:55:39]

This a rather strange. A similar error arises if

one::Nat = suc zero
three::Nat = suc one