Sure, and there exists a dependent type system in Rust's trait system. It is wildly impractical to actually use, interacts poorly with the actual language, and a great example of why Turing Completeness of a type system means very little in practice.
That's almost certainly a bug. At any rate, a proper language with dependent types does not have a Turing-complete type checker and that's what makes it magical. You get incredible power without having to worry about non-termination in your type checker.
It's not a bug, it's due to the trait (aka typeclass) system.
Apparently Haskell has some restrictions that make typeclasses decidable (if -XUndecidableInstances is not set), but Rust has no such mechanism other than numeric iteration limits.
Guaranteed termination of a sound dependent type system is only useful as a mathematical property, not a practical one (yes, I know the mathematical consequences have practical benefit but I mean directly it doesn’t say anything about what a typical user thinks of as “termination”). You could still trivially write an algorithm at the type level which is Turing-complete in a practical sense.
For example, write a type that implements a Turing machine parameterized by a program and a natural number N of evaluation steps to take. Apply that type to Graham’s number or some suitably large natural number. You now have a type that is, for all practical purposes, Turing-complete, even though it is theoretically guaranteed to terminate.
For example, write a type that implements a Turing machine parameterized by a program and a natural number N of evaluation steps to take. Apply that type to Graham’s number or some suitably large natural number.
To do that you’d first need to be able to fit Graham’s number into your source code which unfortunately is never going to happen.
Idris has a termination checker which in practice rejects non-primitive recursion. If you can’t prove to the type checker that your recursive function deferments toward a base case at every step then your program won’t type check. So there’s no back-door method to get Graham’s number or other silliness like the Ackerman function into your types.
https://sdleffler.github.io/RustTypeSystemTuringComplete/