Title: Type Reconstruction in the Presence of Polymorphic Recursion and Recursive Types 
Author: Said Jahama, Boston University 
Date: December 1993


Abstract:

We establish the equivalence of type reconstruction with polymorphic recursion
and recursive types is equivalent to regular semi-unification which proves
the undecidability of the corresponding type reconstruction problem. We also
establish the equivalence of type reconstruction with polymorphic recursion
and positive recursive types to a special case of regular semi-unification
which we call positive regular semi-unification. The decidability of positive
regular semi-unification is an open problem.