Yes, they are consistent. Yes, there are useful systems.

See https://en.wikipedia.org/wiki/Agda_(programming_language) for a reasonably practical example:

> Agda is a total language, i.e., each program in it must terminate and all possible patterns must be matched.