It means that the type system can prove certain properties for you. For example, in languages with dependent type systems like Agda, you can construct a sorted list type that the compiler will prove it sorted at all times, otherwise it won’t compile. Or a complex tree type that is always balanced. Or a set of only even numbers, and again it won’t compile otherwise…

(Sadly, if you go that far, it isn’t generally Turing complete anymore. Though in some cases that’s a good thing.)