Traditionally strongly typed languages has had a very obnoxious compiler that punishes every little developer mistake with marginally helpful error message. Thanks to Idris this has totally changed. Idris uses the power of the compiler to help you get it to compile by suggesting solutions(!), by letting you partially define the program, and by making the type information as visible to you as possible.
Did statically typed languages just become more powerful and easier?