Were this true it would be terrible, because Turing-completeness necessarily includes non-termination. This would mean that a compiler would crash, or get stuck in an infinite loop.
It is true and it is terrible. Woe to be a programmer. The Church-Turing Theorem implies it is almost impossible for any languages exhibiting recursion to not be (Church-)Turing Complete. It is easy to forget how deeply, darkly, and deceptively simple the Lambda Calculus is. It is easy to forget that anywhere you may splice in something that even gently resembles the Lambda Calculus you may draw out the frightening runes of the many eldritch combinators many of which are indeed subject to accidental infinite recursion and The Halting Problem. (Including the infamous Y combinator.)
I have seen the Typescript "computing this type lead to what appeared to be infinite recursion and I gave up" errors. The compiler is well built, it mostly does not truly crash in an exceptional case like that, but it does have to use hard, practical heuristics to avoid getting stuck in infinite loops (including harsh stack depths and calculation timeouts for type checking).
https://3fx.ch/typing-is-hard.html is a neat summary, and yes the situation is worse than most programmers would guess:
Most industry languages, including "boring" reliable ones like C++, Java or Rust have _undecidable_ type systems;( and quite a few are unsound as well.)
This doesn't mean type systems are useless! But as GP said there are tradeoffs, and suspiciously many language designers gave up "clean" properties like guaranteed-terminating compiler, or you know actually guaranteeing run-time safety...
yes, all turing complete type systems make it possible to define type structures that would cause infinite loops, but typically they are able to detect this and refuse to compile
“Oh, right.” He blusters a non-termination argument at nobody in particular. “That’s why we usually think in subsets of Haskell where types don’t have bottom values.”
Yes, this is why unsafe exists. It tells the typing system to take a hike and let the natural Turing completeness of types happen. Trying to explain to people who don't understand higher order functions that types are the first rung of an infinite ladder of meta languages is like trying to explain the colour blue to nematodes.
