Yes the literature says how to do this. It's not hard. Any program that could be written in something weaker like System F will have the same erasure.

> inherently involve a kind of compile-time evaluation.

compile-time evaluation doesn't pose a phase-separation problem. Indeed, nothing to the right of a `:` will ever need to be evaluated on runtime.