Type error debugging in Hazel

This report seeks to improve the debugging of type errors in Hazel, a gradually typed functional language supporting incomplete programs, by explaining static type errors more completely and by combining the benefits of static and dynamic type errors. Three methods are developed. Type slicing highlights the code that determines an expression’s synthesised or analysed type, explaining not just where a static error occurred but why; it generalises beyond errors, applying to all expressions. Cast slicing propagates type slices through evaluation, attaching to each runtime cast a slice of the source code that gave rise to it, recovering the source context of dynamic type errors. A type error witness search procedure, built on indeterminate evaluation, automatically finds inputs witnessing a dynamic counterpart to a static error, linking the two classes of errors. All three methods are given mathematical foundations over a core bidirectionally and gradually typed calculus of functions, holes, and casts; the implementation in the Hazel programming environment extends considerably beyond this formalised fragment, covering nearly the full language. The methods are evaluated on a corpus of ill-typed Hazel programs, with the best search strategy failing to find existing dynamic witnesses for only 2% of the corpus.