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.
Idris' dependent types are more powerful, though @edwinb would probably be the one to explain the differences in detail (he gave a talk awhile back on Scala vs. Idris).
no. in idris you can declare a functions that takes integers less than five, and if you write code that can eve theoretically allow that function to get called with 5 or greater you get a compiler error. things like that
