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

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.