[Ace17]

Of course not. In my understanding, the article was about static type checking, though.

[dllthomas]

It is! That's what is so cool about it! Idris lets you write an append that will work for any X and Y chosen at runtime, but will check that the result must have length X + Y at compile time.