It it always safe to use unsafeCoerce for valid equalities?

Question

I have a witness type for type-level lists,

data List xs where
    Nil :: List '[]
    Cons :: proxy x -> List xs -> List (x ': xs)

as well as the following utilities.

-- Type level append
type family xs ++ ys where
    '[] ++ ys = ys
    (x ': xs) ++ ys = x ': (xs ++ ys)

-- Value level append
append :: List xs -> List ys -> List (xs ++ ys)
append Nil ys = ys
append (Cons x xs) ys = Cons x (append xs ys)

-- Proof of associativity of (++)
assoc :: List xs -> proxy ys -> proxy' zs -> ((xs ++ ys) ++ zs) :~: (xs ++ (ys ++ zs))
assoc Nil _ _ = Refl
assoc (Cons _ xs) ys zs = case assoc xs ys zs of Refl -> Refl

Now, I have two different but equivalent definitions of a type-level reverse function,

-- The first version, O(n)
type Reverse xs = Rev '[] xs
type family Rev acc xs where
    Rev acc '[] = acc
    Rev acc (x ': xs) = Rev (x ': acc) xs

-- The second version, O(n²)
type family Reverse' xs where
    Reverse' '[] = '[]
    Reverse' (x ': xs) = Reverse' xs ++ '[x]

The first is more efficient, but the second is easier to use when proving things to the compiler, so it would be nice to have a proof of equivalence. In order to do this, I need a proof of Rev acc xs :~: Reverse' xs ++ acc. This is what I came up with:

revAppend :: List acc -> List xs -> Rev acc xs :~: Reverse' xs ++ acc
revAppend _ Nil = Refl
revAppend acc (Cons x xs) =
    case (revAppend (Cons x acc) xs, assoc (reverse' xs) (Cons x Nil) acc) of
        (Refl, Refl) -> Refl

reverse' :: List xs -> List (Reverse' xs)
reverse' Nil = Nil
reverse' (Cons x xs) = append (reverse' xs) (Cons x Nil)

Unfortunately, revAppend is O(n³), which completely defeats the purpose of this exercise. However, we can bypass all this and get O(1) by using unsafeCoerce:

revAppend :: Rev acc xs :~: Reverse' xs ++ acc
revAppend = unsafeCoerce Refl

Is this safe? What about the general case? For example, if I have two type families F :: k -> * and G :: k -> *, and I know that they are equivalent, is it safe to define the following?

equal :: F a :~: G a
equal = unsafeCoerce Refl

Answer 1

It would be very nice if GHC used a termination checker on expressions e::T where T has only one constructor with no arguments K (e.g. :~:, ()). When the check succeeds, GHC could rewrite e as K skipping the computation completely. You would have to rule out FFI, unsafePerformIO, trace, ... but it seems feasible. If this were implemented, it would solve the posted question very nicely, allowing one to actually write proofs having zero runtime cost.

Failing this, you can use unsafeCoerce in the meanwhile, as you propose. If you are really, really sure that two type are the same you can use it safely. The typical example is implementing Data.Typeable. Of course, a misuse of unsafeCoerce on different types would lead to unpredictable effects, hopefully a crash.

You could even write your own "safer" variant of unsafeCoerce:

unsafeButNotSoMuchCoerce :: (a :~: b) -> a -> b
#ifdef CHECK_TYPEEQ
unsafeButNotSoMuchCoerce Refl = id
#else
unsafeButNotSoMuchCoerce _ = unsafeCoerce
#endif

If CHECK_TYPEEQ is defined it leads to slower code. If undefined, it skips it and coerces at zero cost. In the latter case it is still unsafe because you can pass bottom as the first arg and the program will not loop but will instead perform the wrong coercion. In this way you can test your program with the safe but slow mode, and then turn to the unsafe mode and pray your "proofs" were always terminating.