Precise explanation of success typing errors

Abstract

Nowadays, many dynamic languages come with (some sort of) type inference in order to detect type errors statically. Often, in order not to unnecessarily reject programs which are allowed under a dynamic type discipline, their type inference algorithms are based on non-standard (i.e., not unification based) type inference algorithms. Instead, they employ aggressive forwards and backwards propagation of subtype constraints. Although such analyses are effective in locating actual programming errors, the errors they report are often extremely difficult for programmers to follow and convince themselves of their validity. We have observed this phenomenon in the context of Erlang: for a number of years now its implementation comes with a static analysis tool called Dialyzer which, among other software discrepancies, detects definite type errors (i.e., code points that will result in a runtime error if executed) by inferring success typings. In this work, we extend the analysis that infers success typings, with infrastructure that maintains additional information that can be used to provide precise (i.e., minimal) explanations about the cause of a discrepancy reported by Dialyzer using program slicing. We have implemented the techniques we describe in a publicly available development branch of Dialyzer