That's true, but Haskell has come a long way since a direct comparison like that would make sense.
> I mean, this HN comments page alone has multiple threads where people don't think that the "x > y" proof example even works.
I think this is because people have some preconceived idea about what dependent typing is before they come to dependently typed languages. So, not only are they learning about dependent types, but they are also fighting their preconceived notions. That was certainly the case for me.
It's an interesting facet of the human condition; every time we learn a new tool, we have to be reminded that it's not magic.
Now, having become proficient, I have a better intuition for how to get my complex Idris programs to type check than my complex Haskell ones. Idris is actually simpler, it's not just about line counts.