Having built a type checker with Z3 in the past, the simple answer to “does type checking happen to have the same complexity as SMT?” is no. That’s because the

Having built a type checker with Z3 in the past, the simple answer to “does type checking happen to have the same complexity as SMT?” is no. That’s because the “T” in SMT, “theories” can be pretty much anything - they’re essentially plugins. A more nuanced answer is that many problems are reducible to SAT, meaning that the answer can technically be yes, but a type checker that simply prints the message “UNSAT” upon failure isn’t very useful!