On: Things that Idris improves things over Haskell

[dynamic]

Checking the head of an empty list is a simple example. (Although see https://wiki.haskell.org/Non-empty_list for an approach to avoiding these runtime errors in Haskell).

Here's a more advanced example: https://news.ycombinator.com/item?id=14569605.