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 Stellar framework, which automatically lifts the core language's typing rules to the surface language while enabling error localization in the surface syntax. Stellar also ensures that the reported errors are fixable by incorporating extra premises into the lifted typing rules. We implement provenance 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 provenance can help surface programmers address type errors more effectively, enhancing the practicality of syntactic sugar in language engineering.