No, you're mixing up concepts (consistency vs. soundness).
If a type system has non-normalizing types (or non-normalizing terms which appear in types), then it is inconsistent as a logic, which means that via Curry-Howard you can prove anything (ex falso quodlibet). Regarding incompleteness, any sufficiently expressive logic is incomplete per Gödel's first incompleteness theorem.
A type system which is inconsistent as a logic can still be sound as a type system. Soundness is the property that you described in your second paragraph (not letting "invalid" programs through). A simple example is System U. It's sound as a type system, but inconsistent as a logic. That means it works for programming, but not for proving.
The only thing this means is that type checking a Rust program might never terminate.
Nothing more, nothing less.
It might take 10 seconds, it might take 10 days, it might take till the universe freezes.
In practice, the compiler - like pretty much every single compiler with a Turing complete type system - has a recursion limit, that rejects programs that accidentally take too long to type check, but users can increase this limit by adding a source annotation (that's suggested by the compiler).
This is completely orthogonal to whether the programs are valid or not.
If your program is invalid, the compiler will never accept it, no matter how much compute time you throw at it.
Type checking always terminates for valid Rust programs (by definition), so if you throw enough compute at any valid Rust program, the compiler will eventually accept it.
I don't see how this is the case. The type system being Turing complete just makes it undecidable, ie. it's not guaranteed to finish type checking. In a way you could call that "preventing some type valid program", though I wouldn't consider an infinite loop of types valid.
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.
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.
(I think the person you replied to is exaggerating the significance of this, though: it's obviously not a big deal in practice.)
I'm specifically not talking about something like Typescript which is widely known to be unsound, but a type system that was believed to be "safe" before someone figured it is Turing complete.
This reminds me of that: http://litherum.blogspot.com/2019/03/addition-font.html
You can craft font files that perform arbitrary calculations… if you give the font shaping engine a (practically) unlimited stack, where it usually limits recursion to 6 levels. If you do so, you can make a font that does math (or whatever you want) as part of computing ligatures.
But in practice, you hardly ever hit those kinds of limits unless you're trying to do something silly on purpose. Sure you cannot port Doom to font substitution lookup tables, despite them being Turing complete. But that doesn't make your font shaping engine useless, or even broken.
edit: by which I mean, the theoretically defined type system, not the actual program implementing it.
Aren't such programs not very interesting by definition?
And why would you call them "valid" programs?
How is Turing-completeness related to soundness? I am behind on CS theory, but what little I know about category-theory tells me this isn’t the case.