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

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.