Implement a well-typed Gen for generating typed programs #1698
Description
See the design in #1697
The idea is that we could generate random programs that should have a known set of types. Then when we emit them as text, we can test the compiler against them. The motivation is to find corner cases in the compiler's type-inference or normalization/optimization rules. We could generate random programs and assert that the values generated by the optimized and unoptimized programs are the same. Also, we could assert that the time it takes to evaluate the optimized ones tends to be lower (or the minimum of N tries is lower).
The goal is to increase our confidence in the soundness of the type-checker.
Of course. We should also consider the opposite: definitely ill-typed programs for which the type-checker should definitely reject.