Statically checking that progress is made does imply that the language is not Turing-complete if I understand it correctly, which is why Coq, the proof assistant language where all programs have to terminate, is not Turing-complete.