I use Agda for prototyping all the time, but the things I'm prototyping are typically type-astronautics, etc. It's easier to build something in a sane type theory like Agda's and then figure out how to shoehorn it into Haskell than the other way around.
Agda is not so good at prototyping many other things. I just use it when I need it. I often end up using it as kind of a kludgy logical framework for my research in Linguistics and Type Theory, since I haven't yet figured out how to use Twelf.
Agda deals with IO and mutation in the same way that Haskell does (the IO monad and the State monad); with special directives, these can be compiled down to plain Haskell code. But Agda's support for extracting Haskell implementations is pretty wacky and not really mature enough for use (for instance, I have many times had it spit out unbuildable code which I needed to preprocess to get it to work). Idris is a somewhat similar language which is compiled and very easy to run, however.
Agda has more support for abstraction & modularity than Haskell by virtue of having a more advanced module system (it has both structures and structures parameterized by values & types, but lacks clean ML-style system of signatures, structures and functors). However, if you are not careful, you will often leak definitional equalities in very dependently-typed code, leading to fragile module boundaries. There are a number of ways to get around this, though; it's still an open question how to achieve modularity in the large in an intensional type theory. Homotopy Type Theory clarifies the situation somewhat. Of course, if you're just writing Haskell in Agda, then you have strictly more modularity here; it's just the interaction with dependent types that can prove tricky.
Agda does not support "Type Class Prolog" in the way that Haskell does; it has a limited support for implicit resolution which suffices for overloading, but not so well for doing Haskell-style type class stuff. Eventually, you may find that Modules Matter Most(!), and end up missing Haskell-style type classes much less.
Most of the things I want to do end up meaning that I need a logical framework in which to build a type theory. I use Agda for that, but this is not its strength (try building a non-trivial term language with binding, for instance).
I never realized it could be much easier than Agda, but I've been playing with Twelf now for a little bit and am getting a feel for how LF and HOAS work together.
I find Idris has a more computational flair while Agda is often "done after typechecking". Idris doesn't enforce termination as strictly as Agda. Idris' interactive modes are less friendly and powerful—Agda's emacs mode is best in breed.
Idris has typeclasses and Agda something akin to first-class modules (as stated above). That's a fairly big difference.
Idris handles laziness and strictness (or, relatedly, data/codata) a little differently than Agda, but it's not a huge concern until you get technical.
Idris is also just younger than Agda and subsequently works a little wonkily. Again I find this exposed through the interactive mode which sometimes provides rather strange information. Although honestly that happens in both Agda and Idris.
Idris has nice syntax for embedded DSLs which is demonstrated in its Effects library which would be possible to replicate in Agda but not as nice looking.
One big difference is that Agda uses universe polymorphism and Idris uses cumulative universes. This shows up in a lot of parameterization of Set in Agda.
If you find Idris easy to understand than Agda will be absolutely no harder. Go take a look at the Agda standard library to get a taste: https://github.com/agda/agda-stdlib
Agda is not so good at prototyping many other things. I just use it when I need it. I often end up using it as kind of a kludgy logical framework for my research in Linguistics and Type Theory, since I haven't yet figured out how to use Twelf.
Agda deals with IO and mutation in the same way that Haskell does (the IO monad and the State monad); with special directives, these can be compiled down to plain Haskell code. But Agda's support for extracting Haskell implementations is pretty wacky and not really mature enough for use (for instance, I have many times had it spit out unbuildable code which I needed to preprocess to get it to work). Idris is a somewhat similar language which is compiled and very easy to run, however.
Agda has more support for abstraction & modularity than Haskell by virtue of having a more advanced module system (it has both structures and structures parameterized by values & types, but lacks clean ML-style system of signatures, structures and functors). However, if you are not careful, you will often leak definitional equalities in very dependently-typed code, leading to fragile module boundaries. There are a number of ways to get around this, though; it's still an open question how to achieve modularity in the large in an intensional type theory. Homotopy Type Theory clarifies the situation somewhat. Of course, if you're just writing Haskell in Agda, then you have strictly more modularity here; it's just the interaction with dependent types that can prove tricky.
Agda does not support "Type Class Prolog" in the way that Haskell does; it has a limited support for implicit resolution which suffices for overloading, but not so well for doing Haskell-style type class stuff. Eventually, you may find that Modules Matter Most(!), and end up missing Haskell-style type classes much less.