I added a translation of this Kata over to Idris, adapting the structure of the code as close as possible (except moving (:<:) from a typeclass (interface in Idris) to a data type that covers all 3 instances similar to the Elem datatype in the Idris standard library.

Idris is a functional language like Haskell, but with a Dependent type system instead. It also, unlike Haskell, uses Strict instead of lazy evaluation.

https://www.codewars.com/kumite/63f93ea7cbfbb30047dcece3?sel=63f93ea7cbfbb30047dcece3

I'd appreciate any help or suggestions!

I've tried porting this as close as possible to Idris, only electing to switch from a typeclass for (:<:) to a proof-like data type instead. Annoyingly/Sadly, the In constructor of Expr generates a warning about it not strictly positive (even though, the way we use it here, that shouldn't pose a problem) that I couldn't find a way to disable, and led to needing me to plaster partial annotations on a lot of the other functions.

Any help improving it appreciated, especially since I mostly write with Idris 2 nowadays!