Turing complete means that any computation can be done within the system. However, there are many Turing complete systems that still can't do a particular thing because they lack the relevant input/output ports. For instance, Conway's Life is well known to be Turing complete, but you can't make it run Doom, because there's no way to input values into it from a controller of any type, and there's no hook-up for the Life simulation to output to a conventional display. (The latter might be theoretically addressable, but the former is not. Life is intrinsically defined with its whole universe specified at the beginning. If you create something that can take in "input" you've created a new variant of Life. Which would not be a crime or anything and may be interesting in its own right, you just wouldn't be working with Life anymore.) You could statically convert some fixed series of inputs into some particular Life initial state, and somehow give it a specification for how to "output" Doom internally, and then run that, but that's not really "running Doom".
The fact that you can embed any arbitrary Turing complete operation into the type checking operation does not mean you have the correct input and output operations to apply a Turing-complete dependent type system onto a Python program.
Now, I'm not saying it can't be done, because I'm not taking a close enough look to be sure, and underestimating motivated type hackers is not a smart idea. But my gut says the odds that you're missing at least one critical source of information or output action you'd need to make this work approaches one. Especially in Python, of all languages. Python's "primitives" are incredibly complex and full of capability and trying to constrain them via dependent types is not entirely dissimilar to trying to make a "safe" subset of Python, which has proved to be effectively impossible even with a great deal more access to the internals of Python over the decades than a type system checking would have.
Kinda-sorta, but possibly not in a useful way. The fact that the type system can express numbers doesn't mean that those numbers are the same numbers used in the host language.
Church-encoded numerals are a common trick. This basically means the number 3 is encoded as Suc<Suc<Suc<Zero>>>.
I.e. if the hinting system is turing complete, it surely can express the concept as a program?