Type systems allow programmers to communicate a partial specification of their program to the compiler using types, which can then be used to check that the implementation matches the specification. But can the types be used to aid programmers during development? In this experience report I describe the design and implementation of my lightweight and practical extension to the typed-holes of GHC that improves user experience by adding a list of valid hole fits and refinement hole fits to the error message of typed-holes. By leveraging the type checker, these fits are selected from identifiers in scope such that if the hole is substituted with a valid hole fit, the resulting expression is guaranteed to type check.

Matthías Páll Gissurarson is a PhD student in the Functional Programming division of Chalmers. His interests include functional programming, building tools, Magic: The Gathering and being an armchair philosopher. He’s currently working on the programming model for the Octopi project, a platform to program secure IoT applications.