haskellsetcoerce

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


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


Solution

  • 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. )