I've been curious about Idris, but apparently there was recently an amazing talk from an (the?) Idris creator talking about rewriting it from scratch with a major emphasis on relying on linear logic. He demonstrated how it does a lot of proving work for you automatically, which caused a lot of wows and applause. Anyway, I'm not sure how valuable it will be for me to learn the current version of Idris given that.