[Agda] Implicit argument with type function

[Sean Leather]

Hi,

Suppose we have the trivial code below.

\begin{code}
module Test where
open import Data.Unit using (Unit; unit)

Unit' : Set
Unit' = Unit -- type synonym: This could also be a more complicated
function.

-- The Universe
data U : Set where
  u : U

el : U -> Set
el u = Unit' -- using type synonym

f : {u : U} -> el u -> Unit
f {u} unit = unit

val : Unit
val = f unit -- ERROR! 'f' and 'unit' are highlighted yellow in Emacs
\end{code}

(Note that this has been heavily simplified in order to highlight the
problem.)

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 ]

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".

Ideally, I would not want to do either of these. First, Imagine that in #1,
we have a more complicated type function. It is not necessarily trivial to
replace the type function with a datatype. In the code I started with, this
is the case. Second, I would like to make the implicit argument '{u}' not
required in 'f'. This was a primary goal in writing the code the way I did.
So, the solution in #2 is perhaps the lesser of two evils, but it is still
not desirable.

Is this an inherent limitation in Agda? Or is there another (better) way to
do what I'm trying to do?

Thanks,
Sean
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080620/2aaa4c55/attachment.html