[Agda] Agsy vs Unifier

[Guido Martínez]

Hi all,

When doing transitivity reasoning on ≅, I used to use C-a to fill the
first and last holes (since they're determined by the outer type of
the equality), and every time I filled a justification, I could use
C-a to fill the next hole, as the type of the justification (and the
previous hole) perfectly determine the next.

In the attached file, you can see this working great on the proof of
comp-iso. One can delete any term and use C-a to fill it in, even when
only one bordering justification is set (except for first and last,
which always work). (My Agda version is 2.5.1).

On some other examples, such as the composition of functors on the
bottom of the file, this does not work anymore. Agsy is unable to fill
any hole at all, even when the justifications are all in place and
correct. What's more: writing "_" on every term hole works just fine,
and one can work by filling justifications one by one (looking at the
goal type to see the current term). Thus unification seems to beat
Agsy in this situation. (underscores are actually resolved by
unification, right?)

So a few questions arise:

- Why can't Agsy find these terms? They seem to be completely
determined by the context, and can apparently be found by unification.

- Shouldn't C-a try to unify too? I understand Agsy is a separate tool
from Agda so maybe it cannot do unification itself, but I guess Agda
could try to see if the hole is unifiable before calling Agsy. As a
user I certainly expect C-a to be at least as strong as unification.

- Somewhat related: A way of expanding a resolved underscore to an
actual term would be neat.

Hope I wasn't too confusing. I have more examples if required.
Thanks!
Guido
-------------- next part --------------
A non-text attachment was scrubbed...
Name: AgsyUnifier.agda
Type: application/octet-stream
Size: 3643 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20160927/a4fb8d16/AgsyUnifier.obj