The up-to-date full record of the discussion about this question
in the Types Forum is available as a plain-text file.
Question:
Consider a typed lambda-calculus with records. Suppose that the record types are ordered by a subtyping relation, and suppose that there is a subsumption rule. The question of type inference is to decide if a given unannotated program is typable. Which papers are published about type inference problems of this form?
Please send replies to me. If there is sufficient interest, I will send a summary to the types list.