[bjz_]

I've been trying to learn enough about this problem to be of use in implementing this (playing around with my own language implementations). It seems like a real challenge might be around ensuring that your programs have extraneous 'type stuff' removed in the compiled program. Part of this could be helped with a nice way of doing proof irrelevance (eg. something like Quantitative Type Theory) and another could be multistage programming (eg. something like MetaML or MetaOCaml). The latter would make it much easier to do a more general form of Rust's monomorphisation of type parameters. You'd then may also want some sort of uniqueness typing and borrowing, but I have no idea where to get started on that! And you also don't want to drown in a mountain of annotations!