是否可以用`unsafeCoerce`来安全地替换所有`coerce'类型检查？

Question

我相信以下内容与一样安全Set.mapMonotonic coerce。即可能发生的最坏情况是，Set如果a或b具有不同的Ord实例，我将打破不变式：

coerceSet :: Coercible a b=> Set.Set a -> Set.Set b
coerceSet = unsafeCoerce

那是对的吗？

编辑：有关以下功能的问题Set：https：//github.com/haskell/containers/issues/308

Answer 1

这应该是安全的。

有效值coerce @a @b始终可以用有效值代替unsafeCoerce @a @b。为什么？因为在Core级别上，它们是相同的函数coerce（仅返回其输入，如id）。事实是，coerce被强迫的两个事物具有相同的表示形式作为证据。对于normal coerce，此证明是实际证明，但是对于unsafeCoerce，此证明只是一个表示“信任我”的令牌。该证明是作为类型参数传递的，因此，通过类型擦除，对程序的行为没有影响。因此unsafeCoerce，coerce只要两者都可能，则和是等效的。

现在，这还不是故事的结局Set，因为coerce它不起作用Set。为什么？让我们来看看它的定义。

data Set a = Bin !Size !a !(Set a) !(Set a) | Tip

从这个定义中，我们看到a不会在任何类型等式之内出现。这意味着我们在以下位置具有表示形式相等Set：if a ~#R b（if a与b- 相同的表示形式~#R被拆箱Coercible），然后Set a ~#R Set b。因此，从Set单独的定义出发，coerce 应该对起作用Set，因此您unsafeCoerce 应该是安全的。该containers库必须使用特定的

type role Set nominal

将这个事实隐藏在世界之外，人为地致残coerce。unsafeCoerce但是，您永远都不能禁用它，并且重申unsafeCoerce一下，（在这种情况下）是安全的。

（请注意the unsafeCoerce和the coerce具有相同的类型！请参见@dfeuer的答案，以获取“过分”类型推断使所有内容变形的情况的示例。）

Answer 2

是的，这在典型的现实情况下应该是安全的。但是，有可能提出一些虚构的示例。这是使用默认设置的一种。我想也许可以使用重叠的实例或其他古怪的功能来做类似的事情，但我不知道。

{-# language GADTs, TypeOperators, ExistentialQuantification #-}

import Data.Coerce
import Unsafe.Coerce
import Data.Type.Equality

data Buh a = Buh (a :~: Rational) a

data Bah = forall a. Bah (a :~: Rational) a

instance Show Bah where
  show (Bah Refl x) = show x

goo :: Rational -> Bah
goo x = case coerce p of
          Buh pf m ->
            let _q = truncate m
            in Bah pf 12
  where
    p = Buh Refl x

如果您致电goo，一切都会好起来的。如果替换coerce为unsafeCoerce，则调用goo将导致段错误或其他不良后果。