haskell - 安全使用来自 GADT 存在的 unsafeCoerce？

Question

说我有

{-# 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

如果我只使用 derefFrom使用适当构造的参数，这段代码会按预期工作吗？看起来是这样，但我不知道可能有什么问题。

通过适当构造的论点，我的意思是:

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

(我将通过将 mkRef 的使用封装在一个 monad 中以确保 Ref 使用相应的列表正确生成，从而使这更安全。)

Answer 1

是的;只要你能确定unsafeCoerce只会被调用来强制一个实际上是目标类型的值，那么它是安全的。