Question: typing with set of most general unifiers

I would like to thank to all those who replied to my request for help
on the subject of type inference with sets of most general unifiers.
The most common reference was to Mitchell Wand's paper.

  author =       "Mitchell Wand",
  title =        "Type Inference for Record Concatenation 
                  and Multiple Inheritance",
  booktitle =    "Fourth Annual Symposium on 
                  Logic In Computer Science",
  pages =        "92--97",
  year =         1989

Another interesting reference was to a paper by Nipkow and Snelting.

Order-sorted unification is infinitary in general, but finitary under
a condition of regularity.

    Author = "Tobias Nipkow and Gregor Snelting",
    Key = "NipSne91",
    Title = "Type Classes and Overloading Resolution via Order-Sorted Unification.",
    Booktitle = "Functional Programming Languages and Computer Architecture",
    Year = 1991,

Also suggested was a paper in POPL about 4 years ago on Algebraic
Reconstruction for Types and Effects.

Thanks again to all those who replied.

Simon Courtenage
King's College London.