We propose another approach to type inference with first-class implicit polymorphism, based on the interleaving of an Algorithm $\mathcal M$-style constraint-generating elaboration of terms and a solver for the generated constraints. The novelty of our approach is that types in generated constraints include a explicit syntactic representation of instantiations 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/