Modernizing SMT-Based Type Error Localization
Max Kopinsky, Brigitte Pientka, Xujie Si
TL;DR
This work addresses the difficulty of locating root causes for type errors in ill-typed programs by extending and modernizing the MinErrLoc framework. It introduces Tyro, a two-stage system that uses a human-readable intermediate representation and a novel polymorphic-type constraint encoding to translate typing constraints into an SMT-based MaxSMT problem, enabling off-the-shelf solvers to identify minimal error sources. The approach demonstrates strong localization accuracy on expert-labeled and large-scale student-program data, while maintaining modularity and trust through the IR-based design and flexible encodings. The results suggest practical impact for IDE-integrated diagnostics and scalable evaluation of error localization methods, with potential applicability to other languages and SMT-based tooling.
Abstract
Traditional implementations of strongly-typed functional programming languages often miss the root cause of type errors. As a consequence, type error messages are often misleading and confusing - particularly for students learning such a language. We describe Tyro, a type error localization tool which determines the optimal source of an error for ill-typed programs following fundamental ideas by Pavlinovic et al. : we first translate typing constraints into SMT (Satisfiability Modulo Theories) using an intermediate representation which is more readable than the actual SMT encoding; during this phase we apply a new encoding for polymorphic types. Second, we translate our intermediate representation into an actual SMT encoding and take advantage of recent advancements in off-the-shelf SMT solvers to effectively find optimal error sources for ill-typed programs. Our design maintains the separation of heuristic and search also present in prior and similar work. In addition, our architecture design increases modularity, re-usability, and trust in the overall architecture using an intermediate representation to facilitate the safe generation of the SMT encoding. We believe this design principle will apply to many other tools that leverage SMT solvers. Our experimental evaluation reinforces that the SMT approach finds accurate error sources using both expert-labeled programs and an automated method for larger-scale analysis. Compared to prior work, Tyro lays the basis for large-scale evaluation of error localization techniques, which can be integrated into programming environments and enable us to understand the impact of precise error messages for students in practice.