[Agda] Extending Pattern Unification to Records

[Andreas Abel]

Brigitte and I have written a draft on higher-order unification using 
constraints.

   Higher-Order Dynamic Pattern Unification for
     Dependent Types and Records
   http://www2.tcs.ifi.lmu.de/~abel/unif-sigma.pdf

It contains some ideas that are relevant for Agda:

1. Detailed theoretical treatment of constraints that are outside of the 
pattern fragment and how they can be molded towards patterns by

   - pruning
   - eta-contraction
   - ignoring non-linear variable occurrences that do not appear on the 
right hand side

These techniques are in essence already implemented in Agda.

However, eta-contraction in Agda was found to be buggy; in the paper we 
argue that eta-contraction can be restricted to terms t_i in a l.h.s.

   X t1 ... tn = t   (X a meta-variable)

where eta-contraction is sound.

2. Full integration of record types by applying the (dependent version 
of the) isomorphisms

   A -> B * C = (A -> B) * (A -> C)
   A * B -> C = A -> B -> C

This allows to solve constraints like

   X (x , y) = t
   X (fst x) = t

Find more details in the paper.  Comments welcome!

Andreas