Most, possibly all, of what you do in Idris can be encoded into Scala, but working with type-level functions become very cumbersome. The compiler doesn't understand that a type-level function is a function, so every time you apply a function to a type and need to know the result is the same as itself you have to summon evidence that this is so (which also sends compile times through the roof). Higher-kinded types get treated differently for equality unless you encode them as members of wrapper types. You end up having to write all your type-level stuff in a kind of continuation-passing style and defining intermediate types to represent each step of your algorithm.