Unification & Sharing aka Unify and Conquer


Does anybody know if there is a more recent account of the work by
Henry Baker described in his "Unify and Conquer" (Proc LFP 1990)
paper?  More specifically, he shows a relationship between Hindley
Milner typing and a sharing analysis via the unification.  If two
types are unified then there is possible sharing.  His analysis will
show the type of append to be:
  append :: List_1(a) x List_2(a) -> List_2(a)
indicating that the result might share with the second argument.

He does not prove the soundness of his analyis.  Has anybody else done
so, or has anybody else written about this relationship?