[Agda] Implicit arguments inference

[Ulf Norell]

On Mon, Sep 26, 2016 at 6:38 AM, Valery Isaev <valery.isaev at gmail.com>
wrote:

> Oh, sorry. It seems that this code works well indeed. The problem occurs
> in the code I give below. The reason is that I import both Data.List and
> Data.Vec. But since xs has type List ℕ, it should be obvious which
> constructor to use.
>

Constructor disambiguation doesn't work that way I'm afraid. In order to
make use of argument types we'd have to essentially try type checking all
possibilities, and I'm a bit worried about exponential behaviour.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160926/f6d0474f/attachment.html