Getting into the Flow: Towards Better Type Error Messages for Constraint-Based Type Inference
Ishan Bhanuka, Lionel Parreaux, David Binder, Jonathan Immanuel Brachthäuser
Abstract
Creating good type error messages for constraint-based type inference systems is difficult. Typical type error messages reflect implementation details of the underlying constraint-solving algorithms rather than the specific factors leading to type mismatches.
We propose using subtyping constraints that capture data flow to classify and explain type errors. Our algorithm explains type errors as faulty data flows, which programmers are already used to reasoning about, and illustrates these data flows as sequences of relevant program locations. We show that our ideas and algorithm are not limited to languages with subtyping, as they can be readily integrated with Hindley-Milner type inference. In addition to these core contributions, we present the results of a user study to evaluate the quality of our messages compared to other implementations. While the quantitative evaluation does not show that flow-based messages improve the localization or understanding of the causes of type errors, the qualitative evaluation suggests a real need and demand for flow-based messages. 1 CCS Concepts: • Software and its engineering → General programming languages; • Theory of computation → Program analysis; Type theory; • Human-centered computing → Human computer interaction (HCI).
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Cited by top-tier papers8
- Total Type Error Localization and Recovery with HolesEric Zhao, Raef Maroof, Anand Dukkipati, Andrew Blinn et al.POPL 2024 · 15 citations
- When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class PolymorphismLionel Parreaux, Aleksander Boruch-Gruszecki, Andong Fan, Chun Yin ChauPOPL 2024 · 13 citations
- Code Style Sheets: CSS for CodeSam Cohen, Ravi ChughOOPSLA 2025 · 5 citations
- A Lightweight Type-and-Effect System for Invalidation Safety: Tracking Permanent and Temporary Invalidation with Constraint-Based Subtype InferenceCunyuan Gao, Lionel ParreauxOOPSLA 2025 · 4 citations
- Usability Barriers for Liquid TypesCatarina Gamboa, Abigail Reese, Alcides Fonseca, Jonathan AldrichPLDI 2025 · 4 citations
Builds on2
- MLstruct: principal type inference in a Boolean algebra of structural typesLionel Parreaux, Chun Yin ChauOOPSLA 2022 · 31 citations
- When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class PolymorphismLionel Parreaux, Aleksander Boruch-Gruszecki, Andong Fan, Chun Yin ChauPOPL 2024 · 13 citations
Related papers
- Refinement Type RefutationsRobin Webbers, Klaus von Gleissenthall, Ranjit JhalaOOPSLA 2024 · 3 citations
- The Simple Essence of Overloading: Making Ad-Hoc Polymorphism More Algebraic with Flow-Based Variational Type-CheckingJirí Benes, Jonathan Immanuel BrachthäuserOOPSLA 2025
- Local Contextual Type InferenceXu Xue, Chen Cui, Shengyi Jiang, Bruno C. d. S. OliveiraPOPL 2026
- Data flow refinement type inferenceZvonimir Pavlinovic, Yusen Su, Thomas WiesPOPL 2021 · 15 citations
- Localizing Type Errors for Syntactic Sugar by LiftingZhichao Guan, Tailai Yu, Di Wang, Zhenjiang HuOOPSLA 2026
