一句话：提出基于算法M约束生成与求解、以显式未知多态类型表示实现一等隐式多态类型推断的新算法。
本文研究一等隐式多态（first-class implicit polymorphism）的类型推断问题。作者提出一种新算法，将 Algorithm M 风格的、生成约束的项 elaboration 与针对这些约束的求解器交错进行。其核心新颖点是在类型推断期间，用显式的语法表示来刻画未知多态类型；当对含未知多态类型的合一约束求解时，也会同时为所 elaboration 的项计算类型实参。该系统具有统一、简单的特点，并可扩展以支持领域特定约束。摘要还称其相较已有的一等隐式多态方案具有优势，但未给出具体实验或形式化细节。
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 types include explicit syntactic representations of unknown polymorphic types during type inference. Solving unification constraints with unknown polymorphic types also computes type arguments for the elaborated terms. The resulting system is uniform, simple, extends to support domain-specific constraints, and compares favorably with other approaches to first-class implicit polymorphism.
@article{Morris26,
title = {Another Type Inference Algorithm for First-Class Implicit Polymorphism},
author = {J. Garrett Morris},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {ICFP},
year = {2026},
doi = {10.1145/3828702}
}