An optimisation to pattern-match compilation is to reorder matches so that constant constructors come first, because the test for them is cheap. Combined with exhaustiveness checking, this can make some cases very fast. Such reordering could probably happen in exhLang.
@felixk42 is looking into this.
Add exh_reorder to the compiler
Updated backendProof, which required proving syntactic properties
(set_globals/esgc_free) - this was surprisingly difficult.
The implementation and proof of the reordering phase itself is due to
Felix Kam (with my help).