Newtype wrappers

The idea can be extended to other situations where unsafeCoerce is
justified: empty types and phantom types. Given declarations

data Void
data Void'
data Const a b = Const a

we can create O(1) wrappers:

f :: F Void -> F Void'                   -- empty datatypes are exchangeable
g :: F (Const a Int) -> F (Const a Bool) -- phantom parameter is insignificant

assuming they do not mess with invariants of F.

From this perspective I prefer proposal 2 (a new constraint): new types of
coercions might be added by adding special cases in the constraint solver.
It is also a reuse of syntax: we can write

foo = newtypeCast :: [Int] -> [Age]

instead of adding a new form of declaration.

_____________________

As for safety, in some sense Map a b is parametric in a and b except
the Ord instance of a. We can coerce Map a b into Map c d if
we can coerce a into c, b into d and the Ord a instance matches
Ord c instance (for example, one is derived from the other).
This could be implemented via an instance like this: