Standard type systems are Turing equivalent. This includes the type systems of functional languages like ML and Haskell. In fact, there's a neat correspondence [0] between algebraic data types and propositional logic (examples in Haskell):

  union types (data T = mkTA A | mkTB B) <-> logical disjunction (A ∨ B)

        product types (data T = mkT A B) <-> logical conjunction (A ∧ B)

        function types (type T = A -> B) <-> logical implication (A → B)

                      the unit type (()) <-> true (⊤)

                              bottom (⊥) <-> false (⊥)

(And, if you were wondering, that's where the symbol for "bottom" comes from!)

Inference on richer type systems, e.g., systems that support dependent types (types built up from expressions about the values they represent) is in general undecidable, which is why some dependently typed languages (e.g., Coq) have type systems that are not Turing equivalent—the language designers have consciously pared down parts of the type system in order to guarantee that type-checking terminates.

0. This is the Curry-Howard correspondence: http://en.wikipedia.org/wiki/Curry–Howard_correspondence#Cor...