[15155]

In Idris, as far as I know, runtime type information is kept around by default and erased through usage-based optimization (and possibly annotation?)

http://docs.idris-lang.org/en/latest/reference/erasure.html