Polymorphic recursion

In computer science, polymorphic recursion (also referred to as MilnerMycroft typability or the MilnerMycroft calculus) refers to a recursive parametrically polymorphic function where the type parameter changes with each recursive invocation made, instead of staying constant. Type inference for polymorphic recursion is equivalent to semi-unification and therefore undecidable and requires the use of a semi-algorithm or programmer-supplied type annotations.