> Sadly I didn’t manage to make as much use of this type-level programming as I had hoped I would at the beginning: Idris allows you to gradually refine your ty

> Sadly I didn’t manage to make as much use of this type-level programming as I had hoped I would at the beginning: Idris allows you to gradually refine your types, and I’ve often succumbed to just moving on to the next feature as my interest for the game itself grew. This sounds quite promising. Large amounts of mandatory type level programming makes constructing useful programs hard. That it is opt-in is a good thing, and agrees with my own experiences with Idris, which are on a much smaller scale than the OP's.