Harden type simplification and subsumption checking

[LPTK]

There is a lot we can do to make sure that type simplification does the right thing. (Currently, the result of type simplification is only used to pretty-print type inference results, and there are some known bugs, such as this.)

For example, we should probably add a "full" testing mode that makes sure the simplified type is always equivalent to the raw inferred one. We could also experiment with using simplified types in following test blocks, which might actually improve the overall type inference running time (to verify). This could be done in tests run separately, making sure the new inferred types are the same (or at least, equivalent).

After we have this, the implementation of type simplification will become significantly hardened.