A very large percentage of compilers for statically typed languages include algorithms with worst-case exponential time. For instance, the celebrated Hindley M

A very large percentage of compilers for statically typed languages include algorithms with worst-case exponential time. For instance, the celebrated Hindley Milner type inference algorithm, which is "almost linear" in practice, has worst-case exponential time (the reason it rarely comes up is that programs rarely have deeply-left-nested let bindings). Anyway, type checkers that employ constraint solving can be a lot easier to reason about and extend than alternatives (and give way better error messages, which is probably the second-most-important thing a type checker does).