Why is this considered newsworthy? How many practical type systems do you know that are not Turing-complete, yet powerful enough as development aids? (Hindley-Milner doesn't count. HM might have decidable type checking, but actual programming languages don't just use HM. In particular, OCaml and GHC Haskell do not have decidable type checking.) Heck, maybe computer scientists ought to do more research into non-Turing-complete development tools.
OCaml's _type_ system is not turing complete (unless you have a new striking example to provide, but this would be considered a critical soundness bug).
There are two undecidable bit in OCaml's typechecker:
1) Checking module types, due to the possibility of naming and manipulating type signatures, in particular in functors. It's extremely hard to hit by accident, since computing in signatures is quite unidiomatic (and unwieldy).
2) Exhaustiveness of pattern matching for GADTs. You can hit that one (although, not "by accident") fairly easily, so the exploration is bounded and always terminate.
As for Haskell, the base system for typeclasses is not turing complete, you need a specific combination of extensions which are known to be dangerous together.
Finally, to answer the first question ... Most dependently typed languages (Coq, Agda) are not turing complete. People who do research in type systems are usually rather careful about the whole thing.
To me, the issue is not the type system being TC, which may or may not be desirable depending on applications.
What is a bit unsettling is that somebody noticed that it was in fact TC: this property should be clear from the type system design and not something to be discovered afterwards.
