Add Property Testing for the TinyLang.Field.TypeChecker

[jakzale]

• we could either reuse the generator in TinyLang.Field.Generators, or
• write a new generator using leancheck.

[effectfully]

leancheck and other enumerative libraries tend to generate values skewed towards "zero" (whatever "zero" is). The entire point of property-based testing is that you generate lots of diverse, interesting, invariants-fulfilling values that are distributed uniformly inside particular patterns (e.g. when generating an integer we want to generate values around some particular bounds uniformly and also between those bounds uniformly). When you combine several different generators of interesting (representative) values together, you get another interesting generator.

And when you get a test failure, shrinking allows to reduce the test sample in a way that is completely unrelated to how the sample was generated. Rich generators make it likely to reveal a bug if there's one, and good shrinking allows to boil the problem down to a minimal test case. Generation and shrinking are two separate concepts that shouldn't be "entangled".

This is particularly evident in our case. Naive enumeration results in boring terms being generated. Most of the time we want to generate typed terms, enumerating those doesn't sound particularly fun. We also want both a type-preserving and non-type-preserving shrinkers, because those two reveal different kinds of bugs (e.g. the latter better reveals scope bugs than the former, because you're allowed to prune more subterms than if you were to preserve well-typedness).

So we need flexibility rather than convenience of generating instances via deriveListable, because the latter is pretty useless in our case anyway.