I've been using Agda for less than a week now, so I want to avoid making too many grand statements about it, but so far my impression is that the increase in power over, say, Haskell is large. It feels similar to the increase in power that one gets from moving from a language that doesn't support FP to a language that does. For example, I can try to program functionally in JavaScript, but it's not clear there's much benefit to it, and there may even be harm (try keeping a monad transformer stack straight without compiler support, and then discovering the inevitable bugs at run time). Moving to Haskell, it becomes clear how the generality baked into FP abstractions helps me use the type system to its fullest.
In Haskell, we like to talk about the benefits of equational reasoning, but I think it's rare that practitioners actually get out their pens and paper and write proofs [1]. Instead, the benefit is that enforcing the constraints that make equational reasoning possible makes informal reasoning easier. It's a sort of secondary benefit. Now when I move from Haskell to Agda I see how it unlocks the full power of equational reasoning, as now I can more directly write proofs in the language and have the compiler check them, and even assist me in writing them. This process makes extensive use of the ability to manipulate expressions algebraically and demonstrates what it really means to have a dialog with the compiler.
[1] There are exceptions to this of course. Library writers will sometimes take the time to prove properties of their abstractions, and they'll do this to great effect, but I don't think this is representative of day to day programming.