一句话：提出 FUSION 算法实现局部精化类型推断，用 SMT 验证多态数据类型与高阶函数，显著减少模板并加速。
针对多态数据类型和高阶函数程序，现有精化类型验证通常需要大量模板，且易产生虚假告警。本文提出 FUSION 局部精化类型推断算法：程序员只需为外部导出的顶层函数以及存在递归依赖（循环依赖）的位置编写签名，FUSION 即可在可判定精化逻辑内为所有中间项可预测地合成最精确的精化类型，并借助 SMT 完成程序检查。作者实现了 FUSION，并在约 12KLOC 的 LiquidHaskell 基准上评估。在已有安全基准上，所需模板约为原先一半，速度提升近 2 倍；在新定理证明基准上，速度提升 10–50 倍，且因合成最精确类型避免虚假告警，使验证成为可能。
We introduce the FUSION algorithm for local refinement type inference, yielding a new SMT-based method for verifying programs with polymorphic data types and higher-order functions. FUSION is concise as the programmer need only write signatures for (externally exported) top-level functions and places with cyclic (recursive) dependencies, after which FUSION can predictably synthesize the most precise refinement types for all intermediate terms (expressible in the decidable refinement logic), thereby checking the program without false alarms. We have implemented FUSION and evaluated it on the benchmarks from the LiquidHaskell suite totalling about 12KLOC. FUSION checks an existing safety benchmark suite using about half as many templates as previously required and nearly 2 × faster. In a new set of theorem proving benchmarks FUSION is both 10 — 50 × faster and, by synthesizing the most precise types, avoids false alarms to make verification possible.