[Agda] function parameters similar to data parameters

[Andreas Abel]

On 19.11.2012 10:21, Dominique Devriese wrote:
> 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.

I stumbled over this problem several times myself.  It is a tricky one 
to fix, I have fixed the lhs aspect of it.  See issue 655.


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/