[Agda] Agda type inference oddity on functions

[Alan Jeffrey]

On 09/27/2010 01:50 PM, Nils Anders Danielsson wrote:
> On 2010-09-27 11:49, Alan Jeffrey wrote:
>> That is, the type inference engine doesn't infer that lambda-terms or
>> applied terms have function type, which seems odd to me.
>
> For some reason the type of an abstraction is more likely to be inferred
> if you write
>
>     λ (x : _) → …
>
> rather than
>
>     λ x → …

Oh wow, you're right!  As it happens, the roadblock I'm hitting is 
caused by the problem on function application rather than on lambda 
abstraction.

> I believe Ulf introduced this behaviour in preparation for something
> else which hasn't been implemented (yet?).

Hmm, that's rather annoying.  Any chance that Mystery Feature X could be 
persuaded to use a different syntax, so that lambda and application 
could be used just for regular old functions?

 > --
 > /NAD
 >

A.