My understanding of the promise of Idris is that anything you _want_ to put into the type definitions for your application, you _can_ put into the type definitions.
Imagine C++ template programming with C++ syntax, sane error messages, and ability to use any C++ code.