一句话：提出一等约束类型系统 FCCT，证明可类型性精确刻画 call-by-name 终止，并给出可终止的近似类型推断。
本文将约束类型提升为一等公民，提出在 System F 上支持多态子类型和类型中约束抽象的系统 FCCT：类型 c ⇒ τ 的值可在消解约束 c 后当作 τ 使用。通过精化到 System F，作者证明所有良类型项在 call-by-name 求值下终止，且所有 CBN 终止项均良类型，从而 FCCT 可类型性精确刻画 CBN 终止。作者还给出无近似的主类型推断半算法 FCCT_I，展示其可间接模拟项归约，揭示有界多态类型推断的困难；并扩展该算法以跟踪抽象调用上下文、通过共享多态实例化进行近似，在保持可靠性下保证终止。最后建立约束类型与交集类型系统的联系。
We study a first-class treatment of constrained types, which were previously confined mostly to ML-style polymorphism. We define System FCCT, an extension of System F with polymorphic subtyping and constraint abstraction in types. A value of type c ⇒ τ can be used at type τ in any context where the subtyping constraint c can be discharged. We show that FCCT exhibits interesting properties. First, all well-typed FCCT terms terminate under call-by-name evaluation (CBN), which can be shown by elaboration into System F. Second, all CBN-terminating terms are well-typed in FCCT. Together, these two properties mean that typability in System FCCT characterizes call-by-name termination. Third, FCCT admits a principal type inference semi-algorithm, called FCCT I , which makes no approximations and can thus be seen as an idealized “ground truth” of type inference. We show that FCCT I indirectly simulates term reduction, shedding some light on the difficulty of bounded polymorphic type inference. Finally, we extend FCCT I to track abstracted call contexts and perform approximation by sharing polymorphic instantiations, ensuring termination on all input terms while preserving soundness. In addition to making the connection between polymorphic subtype constraint solving and term reduction, this paper also establishes a connection between constrained types and existing intersection type systems, which are known to characterize various normalization properties.
@article{LamFP26,
title = {First-Class Constrained Types: Elaboration, Type Inference, Approximation, and a Characterization of Termination},
author = {Chun Kit Lam and Florent Ferrari and Lionel Parreaux},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {ICFP},
year = {2026},
doi = {10.1145/3828701}
}