Напечатайте роли и сбивающее с толку поведение `coerce`

У меня есть тип, Id aи я пытаюсь предотвратить случайное принуждение, например, Id Doubleк Id Int.

Если я правильно понимаю роли типов, следующее не должно компилироваться.

{-# LANGUAGE RoleAnnotations #-}
import Data.Coerce (coerce)

type role Id nominal
newtype Id a = Id String

badKey :: Id Int
badKey = coerce (Id "I point to a Double" :: Id Double)

К сожалению, это делает:

Prelude> :load Id.hs
[1 of 1] Compiling Main             ( Id.hs, interpreted )
Ok, one module loaded.
*Main> :type badKey
badKey :: Id Int

Что мне не хватает в типовых ролях?

Coercibleимеет три возможных «типа» экземпляров (которые автоматически генерируются компилятором, а не определяются пользователем). Только один из них на самом деле зависит от ролей .

• Каждый тип принужден к себе.
• Вы можете привести «под» конструктор типа при условии, что затронутые переменные типа - representationalили phantom. Например, вы можете привести Map Char Intв Map Char (Data.Monoid.Sum Int)потому что у Mapнас есть type role Map nominal representational.
• Вы всегда можете привести новый тип к базовому типу и наоборот, если конструктор нового типа находится в области видимости. Это игнорирует все роли! Смысл в том, что, учитывая, что конструктор доступен, вы всегда можете свернуть и развернуть вручную, так что роль в любом случае не дает вам никакой безопасности.

В вашем примере применяется третье правило. Если бы новый тип был определен в другом модуле, а конструктор не был импортирован, приведение не удалось бы (чтобы заставить его работать снова, вам нужно было бы переключить роль на phantom).

Несколько удивительное специальное поведение для новых типов объясняется в этом выпуске GHC.