[Agda] Implicit argument with type function

[Wouter Swierstra]

Hi Sean,

> Or is it a problem of semantics? For example, the type function may  
> reduce to a type constructor that already exists on the right-hand  
> side of "el."
>
> What are the variables (so to speak) in the design decision? It  
> seems like the scenario I encountered may arise frequently.

It's a question of finding a desirable level of automation. It's clear  
that you don't want to write all arguments out explicitly all the  
time; on the other hand, you'd like a clearly defined set of rules  
that determine when an argument can be left implicit.

The design is kind of related to that for Haskell's class system: if  
there's more than one implicit argument that fits, which one should  
you choose (cf. overlapping instances)? If your "el" function takes  
more than one argument, in which order should it try to find suitable  
arguments (cf. multiparameter type classes)?

At the moment, Agda errs on the side of caution - forcing you to  
explicitly pass implicit arguments sometimes. But there's definitely  
some room for improvement.

   Wouter