Title: Universally Quantified Type Inference
Abstract: Haskell’s type system is based on the Hindley–Milner type system, which supports only rank-1 types. As functional languages have evolved, higher-rank types have been recognized as being useful for expressing more general abstract functions. Peyton Jones et al. introduced a type inference algorithm for universally quantified types in Haskell. However, full type inference for higher-ranked types is undecidable and consequently often requires explicit type annotations to facilitate type inference. In this work, we propose a simplified algorithm for inferring these types. Our approach is demonstrated using a minimal programming language syntax and provides a modular method for inferring higher-ranked types. The inference process is organized into two distinct steps: generating type equations and then solving them. By separating the collection of equations from their resolution, this work gives a more modular inference algorithm, which is slightly more general than the bidirectional system introduced by Peyton Jones.
