What's the difference between Dependent Haskell and Idris

There is a big effort mainly from Richard Eisenberg and others to create a dependent typed Haskell. I have seen Haskell and now I am trying to learn Idris. I have seen that many things that Haskell tries to implement with dependent types,type families etc are implemented in Idris, with a way more easy for a beginner to use and understand. What will be the benefit for the Haskell community if this effort succeeds? What Haskell can do better than Idris in that domain? This is not a question about Haskell vs Idris, but I want to understand the theory behind the differences. For example Haskell uses System F. Idris uses Quantitative Type Theory.