一句话：提出 counter-factual typing 与 variational typing，系统定位类型错误、生成纠错信息并排序呈现最可能原因。
类型推断失败时，错误可能源于多个候选位置，且类型信息有限使生成有用纠错信息十分困难。现有方法常不完备、未区分潜在原因，或几乎不说明如何消除错误。本文提出 counter-factual typing：在 AST 叶节点全面发现错误原因，为每个原因计算消除类型错误的消息，并排序后迭代呈现最可能原因。最大技术挑战是高效生成所有消息，其成本看似随表达式规模指数增长；作者借助 variational typing 复用共享子计算，只需对 ill-typed 表达式类型化一次即可生成全部消息。在文献中收集的大量例子上评估，结果表明该方法优于此前方法且计算可行。
Abstract When type inference fails, it is often difficult to pinpoint the cause of the type error among many potential candidates. Generating informative messages to remove the type error is another difficult task due to the limited availability of type information. Over the last three decades many approaches have been developed to help debug type errors. However, most of these methods suffer from one or more of the following problems: (1) Being incomplete, they miss the real cause. (2) They cover many potential causes without distinguishing them. (3) They provide little or no information for how to remove the type error. Any one of this problems can turn the type-error debugging process into a tedious and ineffective endeavor. To address this issue, we have developed a method named counter-factual typing , which (1) finds a comprehensive set of error causes in AST leaves, (2) computes an informative message on how to get rid of the type error for each error cause, and (3) ranks all messages and iteratively presents the message for the most likely error cause. The biggest technical challenge is the efficient generation of all error messages, which seems to be exponential in the size of the expression. We address this challenge by employing the idea of variational typing that systematically reuses computations for shared parts and generates all messages by typing the whole ill-typed expression only once. We have evaluated our approach over a large set of examples collected from previous publications in the literature. The evaluation result shows that our approach outperforms previous approaches and is computationally feasible.