> Every program has a TS compiler that will compile it, but no compiler can work on all programs.

How would you correctly compile a program that has an actual infinite loop in the type system. Some equivalent of while (1) {}

The equivalent of "while (true) {}" depends on how you want to reduce your Turing program to the type system.

For example, you could translate "the Turning program yields 1" as "the types are valid", and anything else (0 or nontermination) as "the types are not valid".

So "while (true) {}" would correspond to invalid types. And a sufficiently smart interpreter/runtime could conclude that "while (true) {}" does not yield 1, just as a sufficiently smart complier could conclude the type constraints are not met.

But no interpreter (and no compiler) would be able to reach a correct conclusion in all cases.

I see. I got confused by the fact that for me a program that never ends is still valid, but I understand how this makes no sense for a type system.

A program like that isn't a valid typescript program, so failing to compile it is less of a bug. The point is that there are correctly-typed typescript programs that the compile won't compile.

How can you, specifically you the human, typecheck the program if it has an infinite loop in the types? If you can typecheck it, then I can write a compiler to typecheck it, repeat until my compiler can typecheck every correctly-typed program a human can write, at which point the problem becomes moot.

For every specific typescript compiler, there is a correct typescript program that that complier fails to compile. The ones for particular humans will generally not be the same as the ones for particular compilers.