[Agda] Implicit argument with type function

[Wouter Swierstra]

Hi Sean,

> If I load this in Emacs, I get the following errors (without further  
> explanation):
>
> _13 : U  [ at /Users/leather/Research/generics/paper/Agda/Test.lagda: 
> 19,7-8 ]
> _14 : (el _13)  [ at /Users/leather/Research/generics/paper/Agda/ 
> Test.lagda:19,9-13 ]

This basically means that there is an implicit argument of type U  
(called _13) and one of type (el _13) that Agda could not fill in for  
you. The relevant code should turn yellow in the Emacs buffer.

> While the error message could be improved, I have traced the problem  
> to my use of an implicit argument along with a type synonym. There  
> are (at least?) two ways to fix this error:
>
> (1) Change Unit' to Unit in the 'el' such that we have "el u =  
> Unit". This changes it from the type synonym to the actual datatype.
> (2) Add the implicit argument to the call of 'f' in 'val' such that  
> we have "val = f {u} unit".

Yes - these are the two ways to solve this problem. Agda will  
automatically instantiate such implicit arguments if your "el"  
function has right-hand sides that are all headed by a different type  
constructor. It will not unfold type synonyms (like in your example)  
or any other functions. This is a limitation of the current treatment  
of implicit arguments. It's still a bit unclear what the best design  
choice is - so any ideas are very welcome.

Hope this helps,

   Wouter