Quite interesting, I had not thought of pattern-exhaustiveness checking like that.<p>Isn't compiling several languages, including Rust, actually undecidable though? Seems like if your type system or metaprogramming systems are Turing complete, this has to be the case.<p>So that's worse than NP-hard already (though calling it NP-hard is still technically correct).