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.
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.