I would second this. If you've never done pure functional programming before I would hesitate to recommend Idris as your first foray simply because of ergonomic

I would second this. If you've never done pure functional programming before I would hesitate to recommend Idris as your first foray simply because of ergonomic issues with the tooling. Regardless of whether you think Idris the language is suitable for a beginner, it's not a fun experience to deal with the landscape of abandoned libraries, editor integration issues, compiler bugs, etc. if you are already struggling to understand some of the basic principles behind the language. The only exception is if you use it purely as a companion to the Type-Driven Development book. As long as you don't stray too far from the book you generally won't run into any of these other issues and it's more plausible to think of it as a first foray into pure functional programming.