Which doesn't matter that much because there is a fairly small limit on how deep recursion can go which you can easily exceed without Turing-completeness, and the distinction between a program that will halt eventually but not within the limit you give it and one that will never halt doesn't matter for practical purposes.

The point isn't that there is an infinite loop of types that is rejected, the point is that there must be a finite loop of types that is rejected because it is indistinguishable from an infinite loop of types.

(I think the person you replied to is exaggerating the significance of this, though: it's obviously not a big deal in practice.)

It’s a consequence of Goedels incompleteness theorem. You cannot create a type system that stops if the program is type valid, and does not stop (or stops indicating invalid) if the program is type invalid. The practical consequences of this are (probably) minimal.

The proof is trivial. The valid proofs in Zfc are ennumerable. Let f be a proposition in zfc that is undecidable in zfc. Write a computer program c that checks for a proposition p whether proof number n is a proof of p for all n. Apply that computer program to p. A rust program that is valid iff c(p) either doesn’t stop type checking or is invalid.

Do you mean apply program c to proposition f? That is compute c(f)? Of course no one disputes that if one encoded this in Rust's type system, Rust will enter an infinite loop. That's the point of this article.

But none of this has to do with whether Rust's type system is sound or complete as a type system, only that as a logic it is undecidable.

Yes (changed the post)... my point is that the program is valid! Rusts type system can fail to stop on valid programs. I’m probably making a mess of all this though and should shut up before I confuse things more!

Also I obviously fucked up the trivial proof. What I want to write is a rust program that type checks iff an an undecidable true proposition is true! But c doesn’t do that

type systems often feel like a rudimentary typeless haskell or prolog layered as a templating system over the underlying code, particularly if the types are used in generating code for generic types in the underlying typed language.

for any reasonable program, you're not going to run into problems with the turing complete aspects of the type system. it's only when you start cleverly lifting logic into the type system to run in that typeless compile-time space that you'll feel punished by it.

if you want to check if a type adheres to some constraint and then choose between different things to do, and then do that recursively et cetera, sure, you'll blow the template expansion stack.

because you're not longer programming in the typed language, but in the typeless meta-language of its type system.