> Industry typing metalanguages are not expressive enough to deal with even fairly basic real-world programs and force you to write bad code to work around the type checker's stupidity.

I honestly don't see that. Could you provide some examples?