Conservative Approximation of Kleene-Mycroft Iteration for Polymorphic Recursion?
You should have a look at the following paper -- and the previous work by Gori and Levi:

On Polymorphic Recursion, Type Systems, and Abstract Interpretation
Marco Comini, Ferruccio Damiani, Samuel Vrech, 2008   


  The problem of typing polymorphic recursion (i.e., recursive function
  definitions rec {x = e} where different occurrences of x in e are used
  with different types) has been investigated both by people working on
  type systems and by people working on abstract interpretation.
  Recently, Gori and Levi have developed an abstract interpreter that is
  able to type all the ML typable recursive definitions and interesting
  examples of polymorphic recursion. The problem of finding a type
  system corresponding to their abstract interpreter was open.
  
  In this paper we present a type system corresponding to the Gori-Levi
  abstract interpreter. Interestingly enough, the type system is derived
  from the system of simple types (which is the let-free fragment of the
  ML type system) by adapting a general technique for extending
  a decidable type system enjoying principal typings by adding
  a decidable rule for typing recursive definitions. The key role played
  in our investigation by the notion of principal typing suggests that
  this notion might be useful in other investigations about the
  relations between type systems and type inference algorithms
  synthesized by abstract interpretation.