Refinement Type Refutations

Refinement types combine SMT decidable constraints with a compositional, syntax-directed type system to provide a convenient way to statically and automatically check properties of programs. However, when type checking fails, programmers must use cryptic error messages that, at best, point out the code location where a subtyping constraint failed to determine the root cause of the failure. In this paper, we introduce refinement type refutations , a new approach to explaining why refinement type checking fails, which mirrors the compositional way in which refinement type checking is carried out. First, we show how to systematically transform standard bidirectional type checking rules to obtain refutations. Second, we extend the approach to account for global constraint-based refinement inference via the notion of a must-instantiation : a set of concrete inhabitants of the types of subterms that suffice to demonstrate why typing fails. Third, we implement our method in H ay S tack –an extension to L iquid H askell which automatically finds type-refutations when refinement type checking fails, and helps users understand refutations via an interactive user-interface. Finally, we present an empirical evaluation of H ay S tack using the regression benchmark-set of L iquid H askell , and the benchmark set of G2, a previous method that searches for (non-compositional) counterexample traces by symbolically executing Haskell source. We show that H ay S tack can find refutations for <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mrow> <mml:mn>99.7</mml:mn> <mml:mtext>%</mml:mtext> </mml:mrow> </mml:math> of benchmarks, including those with complex typing constructs ( e.g ., abstract and bounded refinements, and reflection), and does so, an order of magnitude faster than G2.