Polymorphic Coverage Types

Test input generators are an important part of property-based testing (PBT) frameworks, and a key expectation is that they be capable of producing all acceptable elements that satisfy both the function's input type and the generator-provided constraints. However, it is not readily apparent how to validate whether a particular generator's output satisfies this coverage requirement. In practice, developers typically rely on manual inspection and post-mortem analysis of test runs to determine whether a generator provides sufficient coverage; these approaches are error-prone and difficult to scale as generators grow more complex. To address this problem, we present a new refinement-type-based verification procedure for validating the coverage provided by input test generators, based on a novel interpretation of types that embeds "must-style" underapproximate reasoning principles as a fundamental part of the type system. In our formulation, the types associated with expressions capture the set of values guaranteed to be produced by the expression, rather than the usual interpretation in which types represent the set of values an expression may produce. We formalize the notion of coverage types in a rich core language supporting higher-order functions and inductive datatypes. To better support real-world test generators, we extend this type system with type and qualifier polymorphism, enabling static verification of coverage guarantees for test input generators constructed using the monadic combinators found in most PBT frameworks. Finally, we have implemented a coverage type checker for OCaml programs based on this core calculus and present a detailed evaluation of its utility using a corpus of benchmarks drawn from both the PBT literature and open-source projects.