| Then we can define | | safeCoerce :: (a ~~ b) => a -> b | safeCoerce = unsafeCoerce
Yes, that's right. When I said "we have the technology" I meant that we (will) have something similar to ~~. See our paper "Generative Type Abstraction and Type-level Computation" http://www.cis.upenn.edu/~sweirich/newtypes.pdf. No unsafeCoerce required.
The idea was to put safeCoerce into a library. The syntax extension would be light-weight because contexts, unlike expressions, still have plenty of room for extensions. The idea is is based on the assumption that to the compiler, 'unsafeCoerce' looks like an artificial safe coercion, so that after inlining safeCoerce, we get exactly the effect of a safe coercion during type checking and further compilation. Perhaps that assumption is wrong. I'll look at the paper. Regards, Bertram