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...

BTW, TypeScript documents where it's unsound and why consciously made those choices: https://www.typescriptlang.org/docs/handbook/type-compatibil...

This also probably means that you really need to start writing tests for your types :)

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

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.