[Agda] Implicit argument with type function

[Sean Leather]

Hi,

On Sat, Jun 21, 2008 at 10:21, Wouter Swierstra <wss at cs.nott.ac.uk> wrote:

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

Is it a problem of performance? For example, in order to determine whether
Agda can instantiate an implicit argument, it may possibly need to evaluate
a complex function.

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.

By the way, I encountered the isssue using standard library code. I could
easily work around it by writing my own datatype (instead of using a
provided type function), but then that defeats the purpose of having
reusable libraries. ;)

Sean
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080621/e96fc9c5/attachment.html