Conservative Approximation of Kleene-Mycroft Iteration for Polymorphic Recursion? To perform type inference in the presence of polymorphic recursion, one can use a Kleene-Mycroft iteration to compute the principal type of an expression. To type $\mathsf{fix}\ f\ldotp e$, we define $F(\sigma)$ as the principal type of $e$ under the assumption that $f : \sigma$. We can then define $\sigma_0 = \forall a \ldotp a$ and $\sigma_{i+1} = F(\sigma_i)$, until we reach a fixed-point $\sigma_k$. This $\sigma_k$ is then the principal type of $\mathsf{fix}\ f\ldotp e$.

There are two key issues with this:


Inference with polymorphic recursion is undecidable, so this iteration may not always reach a fixed-point.
The approximation at each stage of the iteration is not sound: if we quit after $j&lt;k$ iterations, not only will $\sigma_j$ not be the principal type of $\mathsf{fix}\ f\ldotp e$, but it will not be a type of $\mathsf{fix}\ f\ldotp e$ at all, since we made too strong of an assumption about the type of $f$ when checking $e$.


I'm wondering if there's a standard way to soundly approximate polymorphic recursion: that is, to iterate some number of times, and afterwards, obtain a type that is possibly less general than the principal type, but that is nevertheless a valid typing of $\mathsf{fix}\ f\ldotp e$.

For example, one can imagine the Hindley-Milner approximation, where we type $e$ under the assumption that $f$ has a monomorphic type, as being the 0-ary approximation. We may fail to find a typing for an expression that requires polymorphic recursion, but if we find a type, we know that it is a valid typing of the expression.

Does such an approximation exist?
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.