The up-to-date full record of the discussion about this question
in the Types Forum is available as a plain-text file.
I would like to find out if there has been any work done on type inference algorithms using a finite set of most general unifiers rather than a single mgu. While I'm sure that I've never seen or heard of any, and that the problem itself seems difficult at best, I would just like to make sure. Thank you.