Agda’s auto proof search is hardwired into the compiler. That makes it fast,
but limits the amount of customization you can do. One alternative approach
would be to implement a similar proof search procedure using Agda’s
reflection mechanism. With the recent beefed up version of reflection using
the TC monad,
you no longer need to implement your own unification procedure.
Carlos
Tome’s been working on reimplementing these ideas (check out his code
https://github.com/carlostome/AutoInAgda ). He’s been working on several
versions that try to use information from the context, print debugging info,
etc. Hope this helps!