[Agda] Are the parameters implicit arguments to the constructors?

[Andrés Sicard-Ramírez]

Hi,

I have the idea that the parameters are implicit arguments to the
constructors. For example, the following code is type checked  (From
Agda2/examples/AIM6/HelloAgda/Datatypes.agda)

data List (A : Set) : Set where
  []   : List A
  _::_ : A -> List A -> List A

nil : (A : Set) -> List A
nil A = [] {A}


but in

foo : {A : Set} -> List A -> Bool
foo ([] {A}) = {! !}
foo (_::_ {A} x xs) = {! !}

the first equation generates the error

"The constructor [] expects 0 arguments, but has been given 1
when checking that the pattern [] {A} has type List A"

and the second equation generates the error

"Found an implicit argument where an explicit argument was expected
when checking that the pattern _::_ {A} x xs has type List A"


Is it the expected behavior?


Best,

-- 
Andrés