Localizing Type Errors for Syntactic Sugar by Lifting

Syntactic sugar enhances the usability of a core language by providing intuitive syntax in a surface language; however, its interaction with the core-language type checker often results in error messages that are unclear to surface programmers. Existing techniques, such as type lifting, can automatically infer typing rules for syntactic sugar, but they do not consider localizing type errors directly in the surface syntax. This paper studies the problem of localizing and reporting type errors for syntactic sugar, addressing two key challenges: precisely localizing errors and ensuring that they are fixable. Inspired by the recently proposed marked lambda calculus (MLC), we develop ℓ MLC as our core language which tracks error provenance and locations via type annotations. Building on this, we propose the Ste llar framework, which automatically lifts the core language’s typing rules to the surface language while enabling error localization in the surface syntax. Ste llar also ensures that the reported errors are fixable by incorporating extra premises into the lifted typing rules. We implement Ste llar and evaluate it across various surface languages with different type structures, demonstrating that our approach precisely localizes errors and avoids unhelpful references to core-language constructs. Our evaluation suggests that Ste llar can help surface programmers address type errors more effectively, enhancing the practicality of syntactic sugar in language engineering.