Anything on top of the Calculus of Constructions is usually enough. So it's not a moving target, and there are multiple implementations.

if there is only one valid translation of the type constraints into executable code then what you have is a slow, expensive, and occasionally argumentative compiler

it merely remains to build a debugger for your Turing-complete type system, and the toolchain will be ready for production

A component, if I correctly understand the proponents of such type systems.

it certainly is a sister or niece of the "sufficiently advanced technology".

> Is this a brother or a cousin of the "sufficiently advanced compiler"? :-)

I believe the claim was that a sufficiently advanced compiler could do a lot of optimization and greatly improve performance. Maybe my claim here will turn out the same.