Comment by danilafe

Its parameterized modules, extremely elegant yet flexible mixfix notation mechanism, the various niceties around pattern matching (though this one might be a bit of Stockholm syndrome; Agda doesn't nicely allow pattern matching anywhere except at function clauses), the fact that records, GADTS, and modules all feel like aspects of the same thing, and the fact that typeclasses are 'just' records that are automatically filled in. The typeclass and module features IMO already give it some edge over Haskell. I don't know if it's friendlier, but it is more ergonomic.