[mathetic]

So I use QuickCheck often and I'm a true believer, but the point this post is making is absolutely justified. Tying the test generation to the type is often requires some creative ways of writing `Arbitrary` instances (the specification of how test cases should be generated).

However, I don't think what the author is suggesting in its place better. The advantage of tying the test case generation to the type is that it's compositional. Lots of sub Arbitrary instances come together to generate the test case and in the long term I find this to be more maintainable. Whereas the author's approach discourages compositionally.

The real problem is that the types in vanilla Haskell are too loose, so there lots of inhabitants of a type that we are not interested in. The author mentions in passing, dependent-types might be a solution and that is exactly right. What is needed is to make the irrelevant terms illegal altogether. This is pretty achievable and is already somewhat used. For example, the program synthesis (proof search) mechanism of Idris 2[0] uses linear[1] dependent types[2] to heavily constrain which terms are possible candidates for a given type. The specificity of the type reduces the search space, hence increases the effectiveness of the proof search.

[0] https://github.com/edwinb/Idris2

[1] https://en.wikipedia.org/wiki/Substructural_type_system#Line...

[2] https://en.wikipedia.org/wiki/Dependent_type