There is nothing preventing the Rust language definition to add a constraint to type checking saying "recursion depth <= 128" or something like that (e.g. depth

There is nothing preventing the Rust language definition to add a constraint to type checking saying "recursion depth <= 128" or something like that (e.g. depth <= N where N is an implementation-defined constant). In fact, since rustc is "the spec" today, that's kind of how it is ""specified"". Any implementation that does not conform to that would be... non-conforming... or using your own point-of-view, they would be implementing some programming language, but that language wouldn't be "Rust". Then the question is not if Rust programs type-check in finite time, but rather, whether they type check in <= N steps. And e.g. the current implementation answers that question very quickly by just trying.