CODEWITHSUNDEEP
haskellghc
Ben
Ben

Reputation: 33

Heterogeneous reference equality in Haskell

In GHC, the equality instance for IORef and STRef are based on the following primitive operation:

sameMutVar# :: MutVar# s a -> MutVar# s a -> Int#

I would like to be able to compute a heterogeneous reference equality,

sameReference :: IORef a -> IORef b -> Bool

(or similarly for STRefs with potentially different types). Is it okay to just use unsafeCoerce for the purpose of checking the reference equality? Is there a reason that sameMutVar# is not given a heterogenous type signature?

EDIT: To add some context, I would like to have this hetereogenous pointer equality because I want to use the equality method to remove a particular IORef a from a list of IORefs whose types are existentially quantified over.

Upvotes: 3

Views: 292

Answers (1)

dfeuer
dfeuer

Reputation: 48581

It is perfectly safe to write

sameReference :: IORef a -> IORef b -> Bool
sameReference = unsafeCoerce ((==) :: IORef a -> IORef a -> Bool)

It would have been entirely reasonable for the primop to have been given type

sameMutVar# :: MutVar# s a -> MutVar# s b -> Int#

but the designers apparently felt that using that function on references of different types was more likely to be a mistake than otherwise.

What you can't do safely is conclude that sameReference (r1 :: IORef a) (r2 :: IORef b) = True implies that a and b are the same. Suppose you had

sameRefSameType :: IORef a -> IORef b -> Maybe (a :~: b)

Then you could easily write

oops :: Coercible a b => IORef a -> a :~: b
oops r = fromJust (sameRefSameType r (coerce r))

producing bogus evidence that any two coercible types are equal. You should be able to figure out how to use a GADT to get from there to mkUC :: IO (a -> b).

I believe that it would be safe to write

sameRefCoercibleTypes :: IORef a -> IORef b -> Maybe (Coercion a b)

Since Daniel Wagner mentioned stable names, I should mention that the situation for those is even worse in this context. I'll need to start with a bit of background. Suppose you write

f :: Either x Int -> Either x Bool
f (Left x) = Left x
f (Right _) = Right False

In the first case, it would be a shame to allocate a fresh Left constructor just to change the type. So GHC has a low-level optimization (after the core-to-core optimization pipeline) that tries to turn this into (essentially)

f p@(Left x) = unsafeCoerce p
f (Right _) = Right False

That means that you could have m :: Either x a and n :: Either x b where m and n refer to the same heap object despite a and b having completely unrelated types. If you create a stable name for m and a stable name for n, then those stable names will compare equal! If you posit even as much as

sameSNCoercibleTypes
  :: StableName a
  -> StableName b
  -> Maybe (Coercion a b)

then you can use m and n to "prove" Coercible (Either x a) (Either x b) from which you can convert any a into any b. It's a bit delicate, but since it's possible at all, assuming otherwise is rather unsafe.

Upvotes: 4

Related Questions