[TYPES] Complexity of row unification

[Henning Makholm]

I'm looking for a good reference for the time complexity of solving
equalities involving type rows, as used in type inference for record
operations. I can find plenty of papers that tell *how* to do record
unification, but none of them seem to discuss its complexity.

Rémy and Pottier say in their contribution to Pierce's new _Advanced
Topics in Types and Programming Languages_ that there is no known
complexity bound, but they are considering an advanced system where
type constructors distribute over records.

In the absence of such distribution it is straightforward to bound a
pedestrian implementation of the unification algorithm by
O(nm²*alpha(n)), where n is the size of the original equation set and
m is the number of different labels it mentions.  Unless I'm much
mistaken, just a tiny bit of ingenuity will get it down to
O(nm*alpha(n)), but neither of these bounds seem to be mentioned even
in passing at the places where I've tried looking for them.

Anyone? I'd rather avoid reinventing the wheel.

-- 
Henning Makholm          "Den nyttige hjemmedatamat er og forbliver en myte.
                    Generelt kan der ikke peges på databehandlingsopgaver af
                  en sådan størrelsesorden og af en karaktér, som berettiger
              forestillingerne om den nye hjemme- og husholdningsteknologi."