[Agda] function parameters similar to data parameters

[Peter Divianszky]

Hi,

Consider

---------------------------------------------------
ℕ-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)
---------------------------------------------------

Now this is possible:

---------------------------------------------------
module _ {P : ℕ → Set} (z : P zero) (s : ∀ m → P m → P (suc m)) where
   ℕ-elim : ∀ n → P n
   ℕ-elim zero = z
   ℕ-elim (suc n) = s _ (ℕ-elim n)
---------------------------------------------------

My question is, could we write

---------------------------------------------------
ℕ-elim {P : ℕ → Set} (z : P zero) (s : ∀ m → P m → P (suc m))
        : ∀ n → P n
ℕ-elim zero = z
ℕ-elim (suc n) = s _ (ℕ-elim n)
---------------------------------------------------

or maybe

---------------------------------------------------
ℕ-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)
---------------------------------------------------

One advantage would be that the first parameter of 's' could be easily 
hidden:

---------------------------------------------------
ℕ-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)
---------------------------------------------------

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),
while the following is ok:

---------------------------------------------------
module _ {P : ℕ → Set} (z : P zero) (s : ∀ {m} → P m → P (suc m)) where
   ℕ-elim : ∀ n → P n
   ℕ-elim zero = z
   ℕ-elim (suc n) = s (ℕ-elim n)
---------------------------------------------------


Cheers,
Peter