Safe use of unsafeCoerce from GADT existential?

haskell

Solution

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.

Problem

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 `Ref`s are generated properly with a corresponding list.)

Original source