Relevant: "When we say that a language is expressive, we mean that it is easy to use. When we say that a type system is expressive, we mean that it is not." - Gilad Bracha
Very true, and awesome quote. It's worth noting though that once you're talking about dependently-typed type systems, it's accepted that you're going to be doing a lot of work with the type system. You're going to be using proof tactics to type your programs. It's almost the point at that point.