[Agda] Agda type inference oddity on functions

[Nils Anders Danielsson]

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 → …

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

--
/NAD