Can all typechecking occurrences of `coerce` safely be replaced with `unsafeCoerce`?

Question

I believe the following is as safe as Set.mapMonotonic coerce. i.e. the worst that can happen is I will break the Set invariants if a or b have different Ord instances:

coerceSet :: Coercible a b=> Set.Set a -> Set.Set b
coerceSet = unsafeCoerce

Is that correct?

EDIT: relevant feature issue for Set: https://github.com/haskell/containers/issues/308

Answer 1

This should be safe.

A valid coerce @a @b can always be replaced with a valid unsafeCoerce @a @b. Why? Because, at the Core level, they are the same function, coerce (which just returns its input, like id). The thing is that coerce takes, as argument, a proof that the two things being coerced have the same representation. With normal coerce, this proof is an actual proof, but with unsafeCoerce, this proof is just a token that says "trust me". This proof is passed as a type argument, and so, by type erasure, has no effect on the behavior of the program. Thus unsafeCoerce and coerce are equivalent whenever both are possible.

Now, this isn't the end of the story for Set, because coerce doesn't work on Set. Why? Let's peek at its definition.

data Set a = Bin !Size !a !(Set a) !(Set a) | Tip

From this definition, we see that a does not appear inside any type equalities etc. This means that we have congruence of representational equality at Set: if a ~#R b (if a has the same representation as b—~#R is unboxed Coercible), then Set a ~#R Set b. So, from the definition of Set alone, coerce should work on Set, and thus your unsafeCoerce should be safe. The containers library has to use a specific

type role Set nominal

to hide this fact from the world, artificially disabling coerce. You can never disable unsafeCoerce, though, and, reiterating, unsafeCoerce (in this context) is safe.

(Do be careful that the unsafeCoerce and the coerce have the same type! See @dfeuer's answer for an example of a situation where "overzealous" type inference bends everything out of shape. )

Answer 2

Yes, this should be safe in typical realistic circumstances. However, it is possible to come up with contrived examples where it's not. Here's one that uses defaulting. I imagine it might be possible to use overlapping instances or other wacky features to do something similar, but I don't know.

{-# language GADTs, TypeOperators, ExistentialQuantification #-}

import Data.Coerce
import Unsafe.Coerce
import Data.Type.Equality

data Buh a = Buh (a :~: Rational) a

data Bah = forall a. Bah (a :~: Rational) a

instance Show Bah where
  show (Bah Refl x) = show x

goo :: Rational -> Bah
goo x = case coerce p of
          Buh pf m ->
            let _q = truncate m
            in Bah pf 12
  where
    p = Buh Refl x

If you call goo, everything will be fine. If you replace coerce with unsafeCoerce, calling goo will segfault or do something else bad.