[Agda] Unification, the yellow stuff

[Andreas Abel]

Hi Agda crowd,

currently I am working on the Agda solver for metavariables (the 
higher-order unifier).  I have submitted some patches that let Agda make 
more use of free variable information to solve unification problems. 
However, I cannot see whether this is useful in practice.

To get some feedback, could you post me

- problems you have in practice with unification
   (weird behavior of the unifier, not solving things you expect it to 
solve, non-monotone behavior etc.)

- experience with performance of the unifier
   (does it work better now, is it slower/faster etc.)

Unification is the magic part of Agda.  I'd like to make it more 
stable/predictable (and more powerful if possible in a systematic way).

Grateful for you feedback,
Andreas