# 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 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?