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: instance (a ~~ c, b ~~ d, Ord a ~~ Ord c) => Map a b ~~ Map c d where ~~ is kind-polymorphic "equality up to newtypes". If Map was, say, indexed (nonparametric) in the first argument, that would be: instance b ~~ d => Map a b ~~ Map a d etc. Krzysztof Gogolewski