Is the 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 

If I use only derefFrom with properly constructed arguments, will this code work properly? It seems like that, but I don't know what could be.

Accordingly constructed arguments I mean:

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

(I will make it safer by encapsulating the use of mkRef in the monad to ensure that Ref correctly generated with the appropriate list.)

Answer 1

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

Answer 2

I would not do this with the extensibility of GADT. This is not using unsafeCoerce , which the docs explicitly talk about. I would go with what they say and use Any from GHC.Prim as an intermediate type. Any is special in GHC in several ways - one of them is that guaranteed guaranteed values ​​of each type can safely navigate through it using unsafeCoerce .

But still need to consider. The monadic wrapper is not as simple as you think. Let's say you wrote this as simple as possible:

 {-# 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 is ... Function types, if you use them correctly. But there are many ways to use it incorrectly. Here is a simple example of its failure, but a more attractive example might have the wrong type enforcement.

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

Fortunately, we do not need to solve this problem from scratch - we can learn from history. ST could have similar problems with STRef leak values ​​between contexts. The solution is well known at this point: make sure that Ref cannot exit runEnv using a generic type variable.

This code will look something 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 sa = Ref Int newtype Env sa = Env (State (M.IntMap Any, Int) a) deriving (Functor, Applicative, Monad) runEnv :: (forall s. Env sa) -> a runEnv (Env s) = evalState s (M.empty, 0) mkRef :: a -> Env s (Ref sa) 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 sa -> Env sa readRef (Ref c) = Env $ do (m, _) <- get return . unsafeCoerce $ m M.! c writeRef :: Ref sa -> 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 did was override ST badly. This approach assumes that your own use of unsafeCoerce is correct, will not quickly collect links in the case of lengthy calculations with short-lived links, and has worse performance than ST . Therefore, although it is safe, it is not a great solution for anything.

So, this whole gigantic answer asked the question whether this is an XY problem. What are you trying to decide, what do you think is a good decision?