We propose yet another approach to type inference with first-class implicit polymorphism, based on the interleaving of an Algorithm M-style constraint-generating elaboration of terms and a solver for the generated constraints. The novelty of our approach is that during type inference types may include explicit syntactic representations of unknown polymorphic types. Solving unification constraints with unknown polymorphic types also computes type arguments for the elaborated terms. The resulting system is uniform, simple, and compares favorably with other approaches to first-class implicit polymorphism.

https://mathstodon.xyz/@GarrettM/