Safe use of unsafeCoerce from GADT existential?

Question

Say I have

{-# LANGUAGE GADTs #-}

import Unsafe.Coerce 
 
data Any where
    Any :: a -> Any

type Index = Int

newtype Ref a = Ref Index

mkRef :: a -> Index -> (Any, Ref a)
mkRef x idx = (Any x, Ref idx)

(any0, ref0) = mkRef "hello" 0
(any1, ref1) = mkRef 'x' 1
(any2, ref2) = mkRef (666 :: Int) 2

anys :: [Any]
anys = [any0, any1, any2]

derefFrom :: Ref a -> [Any] -> a
(Ref idx) `derefFrom` pool = case pool !! idx of
    Any x -> unsafeCoerce x

Provided I only use derefFrom with appropriately constructed arguments, will this code work as expected? It appears so, but I don't know what gotchas there may be.

By appropriately constructed arguments, I mean:

ref0 `derefFrom` anys
ref1 `derefFrom` anys
ref2 `derefFrom` anys

(I will make this safer by encapsulating use of mkRef in a monad to ensure Refs are generated properly with a corresponding list.)

Answer 1

I wouldn't do it with a GADT existential. That's not a use of unsafeCoerce that the docs explicitly say is valid. I'd go with what they say, and use Any from GHC.Prim as the intermediate type. Any is special in GHC in several ways - one of them is that values of every type are guaranteed to be able to round-trip through it safely with unsafeCoerce.

But there's still more to consider. The monadic wrapper isn't as simple as you think. Let's say you wrote it the simplest way possible, something like this:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}

import qualified Data.IntMap.Strict as M

import Control.Applicative

import Control.Monad.State.Strict

import GHC.Prim (Any)
import Unsafe.Coerce


newtype Ref a = Ref Int

newtype Env a = Env (State (M.IntMap Any, Int) a)
    deriving (Functor, Applicative, Monad)


runEnv :: Env a -> a
runEnv (Env s) = evalState s (M.empty, 0)


mkRef :: a -> Env (Ref a)
mkRef x = Env $ do
    (m, c) <- get
    let m' = M.insert c (unsafeCoerce x) m
        c' = c + 1
    put (m', c')
    return $ Ref c


readRef :: Ref a -> Env a
readRef (Ref c) = Env $ do
    (m, _) <- get
    return . unsafeCoerce $ m M.! c


writeRef :: Ref a -> a -> Env ()
writeRef (Ref c) x = Env $ do
    (m, c') <- get
    let m' = M.insert c (unsafeCoerce x) m
    put (m', c')


-- a stupid example of an exceedingly imperative fib function
fib :: Int -> Env Int
fib x = do
    res <- mkRef 1
    let loop i = when (i <= x) $ do
            r <- readRef res
            writeRef res $ r * i
            loop (i + 1)
    loop 2
    readRef res


main :: IO ()
main = print $ runEnv (fib 5)

This... Sort of functions, if you use it exactly correctly. But there are lots of ways to use it incorrectly. Here's a simple example of it crashing, but a more involved example could have an incorrect type coercion.

main :: IO ()
main = do
    let x = runEnv $ mkRef "Hello"
        y = runEnv $ readRef x
    print y

Fortunately, we don't need to solve this problem from scratch - we can learn from the lessons of history. ST could have had similar problems with STRef values leaking between contexts. The solution is well-known at this point: make sure that Refs can't escape from runEnv by use of a universally-quantified type variable.

That code would look more like this:

{-# LANGUAGE RankNTypes, GeneralizedNewtypeDeriving #-}

import qualified Data.IntMap.Strict as M

import Control.Applicative

import Control.Monad.State.Strict

import GHC.Prim (Any)
import Unsafe.Coerce


newtype Ref s a = Ref Int

newtype Env s a = Env (State (M.IntMap Any, Int) a)
    deriving (Functor, Applicative, Monad)


runEnv :: (forall s. Env s a) -> a
runEnv (Env s) = evalState s (M.empty, 0)


mkRef :: a -> Env s (Ref s a)
mkRef x = Env $ do
    (m, c) <- get
    let m' = M.insert c (unsafeCoerce x) m
        c' = c + 1
    put (m', c')
    return $ Ref c


readRef :: Ref s a -> Env s a
readRef (Ref c) = Env $ do
    (m, _) <- get
    return . unsafeCoerce $ m M.! c


writeRef :: Ref s a -> a -> Env s ()
writeRef (Ref c) x = Env $ do
    (m, c') <- get
    let m' = M.insert c (unsafeCoerce x) m
    put (m', c')


-- a stupid example of an exceedingly imperative fib function
fib :: Int -> Env s Int
fib x = do
    res <- mkRef 1
    let loop i = when (i <= x) $ do
            r <- readRef res
            writeRef res $ r * i
            loop (i + 1)
    loop 2
    readRef res


main :: IO ()
main = print $ runEnv (fib 5)

Of course, at this point, all I've done is reimplement ST badly. This approach involves proving your own use of unsafeCoerce is correct, won't collect references promptly in the case of long-running computations with short-lived references, and has worse performance than ST. So while it's safe, it's not a great solution to anything.

So, this whole giant answer has been asking if this is an XY problem sort of thing. What are you trying to solve that you think this is a good solution for?

Answer 2

Yes; so long as you can be sure that unsafeCoerce will only be called to coerce a value that is actually of the target type, then it is safe.