The idea is that Shen has a turing-complete type system, so it shouldn't even be possible to create a more powerful type system (given a specific definition of "powerful").
To expand on that idea a little bit: that's a valid definition of 'powerful', but there's another definition of 'powerful' which some people mean when they talk about type systems, and that's "To what degree does this type system prevent errors?" It seems from cursory research that Shen is powerful with respect to the definition, "To what degree can we encode computations in the type system at compile-time?" and Agda and Coq's type systems are powerful with respect to the definition, "How can we limit the class of programs by encoding constraints in the type system such that the resulting programs are provably correct?" Consequently, neither Agda nor Coq are Turing-complete even at the language level, much less the type level, but that accordingly gives them greater power to know information about their programs at compile time.
