Does anyone know if Idris improves on this aspect of Haskell?
However, GHC is a phenomenal compiler, and can outperform Idris for many things; this is natural, as it's seen a lot of interest in terms of producing performant code.
There are still some gotchas in Idris code. The biggest one that I can think of is indexing some type with data that doesn't manage to get erased (the usual type erasure algorithm is pretty aggressive, but it can't remove everything). Some of the most useful types for programming (as in, proving theorems about the code) are wonderfully inefficient (as an example, the inductive definition of natural number is an empty linked list - taking up plenty of space in pointers, and killing your cache whenever it's accessed - Idris knows about Nat, but not about other types). Operations on the data, which might look very efficient, can also end up operating on the indices, which might not be.
Here's the docs explaining the possible hiccup with erasure: http://docs.idris-lang.org/en/latest/reference/erasure.html
I am eager to point out, how lazy is to call lazy strict.
Idris on the other hand is still very much an experimental project more focused on practical applications of dependent type theory than things like performance. However, with enough work done on its compiler, its strictness and the abundance of type information might allow it to be eventually more performant. Though, the lack of type erasure might negatively impact performance as well depending on how types work at runtime...