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