In C++, if you were to write your own generic sort function template that takes a comparison predicate argument, then the compiler would be able to inline this predicate.
This is not the case in C: qsort is compiled once, and its comparison predicate argument is never inlined (Perhaps the compiler/linker state of the art improved lately, so please do correct me if my information is out-of-date)
This is a boon to generic programming in C++ (not just the sort function, of course): you can achieve the same performance, for which in C, you would have to abandon genericity (or use macros).
My question is: can Idris do what C++ does here? Can it inline functions that are used as arguments?
Idris does have support for partial evaluation of higher order function via an annotation mechanism. By marking the argument you expect to be passed at compile time [static], you can get the resulting program to be specialised.
Cf. the manual for more details.