Можно ли безопасно заменить все случаи проверки типов 'coerce' на unsafeCoerce?

Ответ 1

Это должно быть безопасно.

Действительный coerce @a @b всегда можно заменить действительным unsafeCoerce @a @b. Почему? Потому что на уровне ядра это одна и та же функция, coerce (которая просто возвращает свой ввод, как id). Дело в том, что coerce принимает в качестве аргумента доказательство того, что две принуждаемые вещи имеют одинаковое представление. При обычном coerce это доказательство является фактическим доказательством, но с unsafeCoerce это доказательство является просто токеном, который говорит: "Поверь мне". Это доказательство передается в качестве аргумента типа, и поэтому при стирании типа не влияет на поведение программы. Таким образом, unsafeCoerce и coerce эквивалентны, когда оба возможны.

Теперь это не конец истории для Set, потому что coerce не работает на Set. Почему? Давайте посмотрим на его определение.

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

Из этого определения мы видим, что a не появляется внутри каких-либо равенств типов и т.д. Это означает, что мы имеем конгруэнтное равенство представлений в Set: если a ~#R b (если a имеет то же представление, что и b - ~#R распаковывается Coercible), затем Set a ~#R Set b. Таким образом, из определения только Set, coerce должен работать на Set, и, таким образом, ваш unsafeCoerce должен быть в безопасности. Библиотека containers должна использовать определенный

type role Set nominal

чтобы скрыть этот факт от мира, искусственно отключая coerce. Вы никогда не сможете отключить unsafeCoerce, и, повторяя, unsafeCoerce (в этом контексте) безопасен.

(Будьте осторожны, чтобы unsafeCoerce и coerce имели одинаковый тип! См. ответ @dfeuer для примера ситуации, когда "чрезмерно усердный" вывод типа изгибает все из формы.)

Ответ 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 приведет к сбою или сделает что-то еще плохое.