Sure, and I know about those. I wasn't claiming that this was only possible in Idris -- and I don't think their implementations are nearly as clean or straightforward as the one in Idris.

In Idris, the pattern used to implement this is available to anyone that knows the language. It feels a lot more natural than using a macro system or typeclasses -- it is just functions.