I highly recommend the book. Typing in examples and getting experience collaborating with the compiler on edits is worthwhile. Even if you never use Idris(2) again after reading it, the demos on creating state machine DSLs with contextual invariants will leave a lasting impression.
[1] https://idris2.readthedocs.io/en/latest/typedd/typedd.html
[2] https://github.com/idris-lang/Idris2/tree/master/tests/typed...