23

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

Jonathan Leffler
  • 730,956
  • 141
  • 904
  • 1,278
jberryman
  • 16,334
  • 5
  • 42
  • 83
  • 4
    Fantastic question. I look forward to seeing a comprehensive answer; the GHC documentation itself is incredibly vague about what you're actually allowed to use `unsafeCoerce` for. It's got a couple rules of thumb, but isn't clear (to me at least) exactly whether those rules apply here or not! I hope we get a GHC internals expert to write in some real detail what is and isn't kosher. – Daniel Wagner Sep 16 '19 at 20:50
  • 3
    @DanielWagner my experience with haskell libraries is the more unsafe something is the more cagey people get with their docs, unfortunately. – jberryman Sep 16 '19 at 21:03
  • @jberryman, the more unsafe something is the less likely the people writing/documenting it understand just how unsafe it is, and the more likely it is to get more unsafe when something else in the compiler or a library changes. Safety rules for `unsafeDupablePerformIO` are pretty straightforward, but I doubt anyone could confidently give you reliable ones for almost any uses of `unsafeInlinePerformIO`. – dfeuer Sep 18 '19 at 03:11

2 Answers2

12

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

HTNW
  • 27,182
  • 1
  • 32
  • 60
  • 2
    Arguably, the library is a bit self-contradictory here, since it allows us to break the invariant using `mapMonotonic`, but disables `coerce` because it can break the invariant. This might be the pragmatic way to do it, though, since one can hardly miss the requirement of `mapMonotonic` and break it, while it would be easier to break it using `coerce` on a larger type which involves a set somewhere inside. Still, the library could provide a way to enable safe coercions "on demand" on sets, e.g. using a `Dict`, letting the user guarantee that the types have the same ordering. – chi Sep 17 '19 at 06:59
  • @chi I'm interested in your `Dict` idea but don't have much experience working with constraint kinds and so on. It would be neat if we could somehow get a `coerce` on sets that was _safer_ than `mapMonotonic` – jberryman Sep 17 '19 at 14:33
  • 1
    @chi, `mapMonotonic` would be in a different, "unsafe", module if I'd been maintainer when it was added. But yes, being explicit is good. The only way to expose the optional coercion you want, with today's GHC, is to build it using `unsafeCoerce`. I'm thinking about a proposal to change that by removing the backwards reasoning from `Coercible` (it doesn't seem useful enough to justify these problems). – dfeuer Sep 17 '19 at 19:55
  • @chi, please see https://github.com/ghc-proposals/ghc-proposals/pull/276 – dfeuer Sep 17 '19 at 22:37
  • Oh, the other option would of course be to make `Set` a newtype around an underlying internal `Set` type with a `representational` parameter role, but that would be a major implementation pain. – dfeuer Sep 17 '19 at 22:41
6

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.

dfeuer
  • 48,079
  • 5
  • 63
  • 167
  • I don't think this is particularly fair. You've turned `coerce @(Buh Rational) @(Buh Rational)` into `unsafeCoerce @(Buh Rational) @(Buh Double)`, by abusing the rules of type inference. This is not a problem with the `coerce`->`unsafeCoerce` substitution itself, since you haven't "really" substituted `unsafeCoerce` for `coerce` at all. I do agree this is rather alarming, though. – HTNW Sep 17 '19 at 02:58
  • 1
    @HTNW, for sure. My point is that a blind syntactic substitution of one for the other may not be safe. – dfeuer Sep 17 '19 at 02:59