[Haskell-cafe] Associative Commutative Unification

[Edsko de Vries]

On Tue, Jul 08, 2008 at 08:24:45AM -0400, John D. Ramsdell wrote:
> The Haskell typechecker contains a nice example of a unifier for
> freely generated terms.  My focus is on equational unification, but
> thanks anyway.

Are you aware of "Term Rewriting and all That"? It describes how to do
associative commutative unification; whether it satisfies your
'obviously correct' criterion I don't know. 

Edsko