The problem with “not writing code like that” is that eventually someone does.
At work we use a home-grown Haskell-like language with “row types” which can be split into disjoint sets of fields in order to represent joins and the like.
It works well in most cases, but it’s very easy to forget a type annotation and trigger unmanageable build-times. Often times, it is not obvious where something needs to be annotated. Sure, we can act as human time-outs, but the productivity loss can be substantial, especially for a newcomer to the language.
The solution to "eventually someone does" is "add a timeout, and when you hit that timeout give them an error so they can fix their code".
There's no practical difference between exponential and infinite time, you need to do this for bad exponential time cases anyways.
Many langauges type systems (Java, Typescript, C++, Rust, ...) really aren't guaranteed to terminate in the absence of a timeout either. They're (the type systems) turing complete, you can write infinite loops that the compiler can't know are infinite loops. This makes no practical difference relative to languages which "merely" have exponential time type systems, because with an exponential time type system you're alread accepting the risk that typechecking might not terminate before the heat death of the universe.
A timeout (or recursion/expansion depth limit) could be useful to give the human some specifics about what went wrong. But humans generally kill compilations that take much longer than usual. If it took 20 seconds before, and now it's run for 10 minutes and hasn't finished, I'm probably going to control-C it (or whatever), and then diff against the previous code to try to figure out what went wrong.
Yes, making it possible to reason locally about compiler performance can be pretty helpful. It’s one reason I like to have type declarations for public API’s. Also, hitting an implementation-defined limit (that you can raise) for unreasonable constructs might result in better errors than just continuing to run, but slowly.
A termination guarantee for type checking doesn’t really help.
At work we use a home-grown Haskell-like language with “row types” which can be split into disjoint sets of fields in order to represent joins and the like.
It works well in most cases, but it’s very easy to forget a type annotation and trigger unmanageable build-times. Often times, it is not obvious where something needs to be annotated. Sure, we can act as human time-outs, but the productivity loss can be substantial, especially for a newcomer to the language.