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

说我有

{-# 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 使用相应的列表正确生成，从而使其更安全。)

最佳答案

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

关于haskell - 安全使用来自 GADT 存在的 unsafeCoerce？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/21612213/