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.
Dart has a pretty sophisticated type system — generics, generic methods, function types, subtyping, etc. — but isn't Turing-complete as far as I know.
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.