I've not used Idris too much, so I can't say for sure. My guess is that the answer is that it could do everything I want type-system-wise, but there are things

I've not used Idris too much, so I can't say for sure. My guess is that the answer is that it could do everything I want type-system-wise, but there are things I want outside of the type sytem that I don't think it could do. For example, I want the compiler to automatically rewrite my code to be much more efficient and numerically stable (see the HerbiePlugin to the GHC compiler which goes this https://github.com/mikeizbicki/HerbiePlugin https://github.com/mikeizbicki/HerbiePlugin). My understanding is that the Idris compiler gets much less engineering work done on it (outside of the type system), and so getting efficient running code will be too difficult.