Dependent types are expressive enough to describe data with complex internal invariant, from sorted lists and fully-connected graphs to well-formed sequences of API requests and semantically correct programs. It means that once we’ve modelled complex requiements in a dependently-typed data structure, we can safely feed it to a system with such requirements. For example, once we’ve modelled a semantically correct program, we can give it to the compiler as an input, in order to load the typechecker and code generator.

Once we are able to generate such dependently-typed values, we can do property-based testing of such systems with complex requirements on their inputs. Property-based testing is a well-established approach which allows to discover bugs almost impossible to find manually, and being correctly applied allows to significantly reduce costs of high-quality testing.

The challenge is both to effectively generate dependently-typed values and to automate creation of these generators, especially with nice guarantees, say on completeness and distribution. In this work we present an approach to do this as long as an experience on applying it to some real-world applications.