Just checked the code examples in a current Standard ML compiler, and they work without modification and behave as described. That's why you should choose Standard ML for your next project.

Great example though. When looking at Idris I had the impression there was a logical end point of having the type system so descriptive that, given the type of a function, there was only one possible implementation.