Polymorphic type slicing

This dissertation formalises and mechanises type slicing – a technique that incrementally explains program types by highlighting minimal program fragments. Using this, a programmer can select any sub-term of a program and incrementally explore complex types and concisely explain type errors. Crucially, this includes highlighting context surrounding the term, differing from typical type error highlighting, which simply states that a term has the wrong type, but not what about the surrounding context explains why it has this type. This is formalised in a bidirectional, gradually typed core calculus with explicit System F style polymorphism, products, and sum types. A novel context classification judgement formalises the notion of splitting type information into that derived from a selected sub-term and that coming from the surrounding context, and can be applied to arbitrary bidirectional type systems. Further, the theory extends formally to ill-typed programs with error marks, building upon the marked lambda calculus of Zhao et al. Essentially the whole construction is mechanised in Agda.