There is no total order on type systems. ATS is quite advanced yes, and as of late, I would put Scala in the same group of languages with highly complex and powerful type systems.

But I have a hunch that the type system of Haskell allows for more expression than the comparable ATS type system. Even though ATS has variants of dependent types and also linear (perhaps affine?) types.

Very next sentence:

The only systems which can beat it are theorem provers like Coq, and they are not general purpose programming languages (Morriset and the YNot team might disagree though!).

ATS is dependently typed and therefore falls under theorem provers.

ATS is meant to be a general purpose programming language. The fact that you have a theorem proving subsystem is to aid in the programming/verification. Idris is another dependently typed prog. lang. that is intended for general purpose programming.

Idris was not on my radar in 2010 :)