My 1988 POPL paper with Bob Harper makes a gross error regarding the complexity of ML type inference. In summarizing the "known" results about ML typing, we said that type inference was linear time. We now know that it is not even polynomial. Sorry about the error. John