You can play around with idiom brackets now using the Strathclyde Haskell Enhancement (SHE)[1]. It's pretty easy to configure and will give you a good feel for how the feature behaves in practice. I haven't used Idris, and the syntax looks a bit different[2], but I suspect they're pretty similar in capability. If not, I'd love to see how they differ in detail.
Personally, I'm definitely in favor of idiom brackets or similar syntax abstractly. That said, I tried using SHE's idiom brackets in some of my own existing code and was a bit underwhelmed. They're certainly an improvement for simpler cases, especially ones using operators, but fall apart quickly for more complex expressions. Now, I might have been using them incorrectly, but I found it awkward to express code that used both normal *and* Applicative application at the same time... which proved to be about half of all my code using Applicative operators. Common cases like `f <$> g x <*> h y` are a bit tricky, and they completely hose the $ operator.
Now, I didn't spend much time or effort trying to make idiom brackets work, so I'm certainly not saying that they're unworkable. A good start for the proposal would be to examine more complex cases and idioms present in real code and how idiom brackets would—or wouldn't—improve them. Idris likely has some more interesting examples to start from, but there are probably enough differences in both the language and common idioms to make specific Haskell examples necessary. Adding idiom brackets to some of your own code, or code from some open source projects, would be a good way to both find relevant examples and refine the whole proposal.