Within a language like the Calculus of Coinductive Constructions like Morte appears to implement it's not such a strange idea to have normalization.
So, no infinite loops means no Halting Problem means no completeness.
The upside is a larger set of easy-to-perform optimizations, much greater mathematical elegance. The downside is that you cannot directly write an interpreter for a complete language. Though you could write one which halts every N steps and requires user input to continue. In practice, that isn't the worst idea for a repl anyway.