[Agda] function parameters similar to data parameters

[Dominique Devriese]

Peter, all,

2012/11/19 Peter Divianszky <divipp at gmail.com>:
> I conclude this because
>
> ---------------------------------------------------
> ℕ-elim : {P : ℕ → Set} (z : P zero) (s : ∀ {m} → P m → P (suc m))
>        → ∀ n → P n
> ℕ-elim z s zero = z
> ℕ-elim z s (suc n) = s (ℕ-elim z s n)
> ---------------------------------------------------
>
> is not allowed now ("Refuse to construct infinite term ..." error),

For clarity, the problem here is that the second s in the expression
"s (ℕ-elim z s n)" has its hidden argument instantiated. It is in fact
equivalent to "s {_}". This is correct behaviour with respect to how
hidden arguments are supposed to behave.  You can fix the error by
preventing the hidden argument from being instantiated by replacing
"s" by its eta-expansion "\ {m} -> s {m}".

I don't have an opinion about Peter's proposal, just wanted to point
out what the problem here is.

Dominique