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://do

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 http://docs.idris-lang.org/en/latest/reference/erasure.html