A short answer is that the theory is just simpler. Non-dependent type theory spends a lot of effort separating values, types, kinds and valid operations over them. For example you need lots of extensions to make it possible to use a type both at the value, type, and kind level in Haskell. Each extension to the type system adds more complexity, and requires special code to implement its functionality (DataKinds, PolyKinds, TypeFamilies, etc). You also end up needing at least two or more different kinds of ASTs one that describes expressions, one for types, one for kinds, etc.

All of this falls away in dependent type theory you can represent the whole language with a class of pesudo-terms. For example the core expressions can be captured by the below grammar:

    term := x
         | f x
         | forall (x : Type), B x
         | lambda (x : A), e
         | Type

Type checking (not inference) is straight forward to implement for these theories and can be done in about a page or two of code. Of course "elaboration" or "type-inference" for these theories can be much more complex, but Haskell's isn't simple either. The most recent publication on the TI algorithm is roughly 80 pages.

Haskell's type system has accrued complexity over the years, whereas a small dependently typed language can be implemented very easily [1].

[1] https://www.andres-loeh.de/LambdaPi/

That's not a fair comparison, though. A fair comparison might be Haskell's type system compared to Idris, or a small dependent typed language against a small type inference language.

The question was, "how's that?". My answer was, it's possible for a small dependently typed language to be simpler than Haskell.

I'd already made the assertion that Idris was less complicated than Haskell.