> You can recover a sort of phase distinction Yes the literature says how to do this. It's not hard. Any program that could be written in something weaker like

> You can recover a sort of phase distinction 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.