I tried using Idris to write this one. Some quick thoughts:
I didn’t use dependent types at all — my solution would have been nearly identical in Haskell.
The error messages from Idris were mostly unhelpful.
I often hit an error saying it couldn’t find an typeclass implementation for a variable I didn’t declare anywhere.
I needed more manual type annotations than I thought necessary — for example, {m = _ Error IO}.
The syntax for named implementations is not well-documented and it took a few tries to write it in a way that was accepted by the compiler and did the right thing.
There is no equivalent to Hoogle, and in particular I needed to search the Idris github repo to find the Maximum instance for Semigroup, which doesn’t even appear in the rendered documentation.
The rendered documentation would be more helpful if it linked to the source code, like Haddock does.
I’m not sure my code is idiomatic Idris, if there is such a thing.
I don’t think I’ll use Idris for further tasks because its UX relies too heavily on the users knowing how the parser and compiler works.