Отключить приведение типа Haskell

Проблема в том, что newtype можно принудить к своему представлению, пока конструктор находится в области видимости — действительно, это большая часть мотивации для Coercible. А ограничения Coercible подобны любым другим ограничениям класса типов, они автоматически ищутся и объединяются для вас, только в еще большей степени. Таким образом, coerce c3 обнаруживает, что у вас есть

instance Coercible (Container p) [Int]
instance Coercible [Int] (Container p')

для всех p и p', и с радостью создадим для вас составное принуждение с помощью

instance (Coercible a b, Coercible b c) => Coercible a c

Если вы не экспортируете конструктор Container — как вы, вероятно, все равно захотите сделать! — тогда уже не известно, что newtype равно его представлению (вы теряете первые два экземпляра выше), и вы получаете желаемую ошибку в других модулях:

ContainerClient.hs:13:6:
    Couldn't match type ‘4’ with ‘3’
    arising from trying to show that the representations of
      ‘Container 3’ and
      ‘Container 4’ are the same
    Relevant role signatures: type role Container nominal nominal
    In the expression: coerce c3
    In an equation for ‘c4’: c4 = coerce c3

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

В качестве примечания: вы, вероятно, не хотите использовать здесь метод доступа в стиле записи и экспортировать его; который позволяет пользователям использовать синтаксис обновления записи для изменения кода из-под вас, поэтому

c3 :: Container 3
c3 = mempty

c3' :: Container 3
c3' = c3{runContainer = []}

становится действительным. Вместо этого сделайте runContainer отдельной функцией.

Мы можем убедиться, что получаем композицию двух ограничений представления newtype, взглянув на ядро ​​(через -ddump-simpl): в модуле, который определяет Container (который я также назвал Container), вывод (если мы удалим список экспорта)

c4 :: Container 4
[GblId, Str=DmdType]
c4 =
  c3
  `cast` (Container.NTCo:Container[0] <GHC.TypeLits.Nat>_N <3>_N
          ; Sym (Container.NTCo:Container[0] <GHC.TypeLits.Nat>_N <4>_N)
          :: Container 3 ~R# Container 4)

Это немного трудно читать, но важно видеть Container.NTCo:Container[0]: NTCo является newtype приведением между newtype Container p и его типом представления. Sym переворачивает это, а ; составляет два ограничения.

Назовите окончательное ограничение γₓ; тогда весь вывод типизации

Sym :: (a ~ b) -> (b ~ a)
-- Sym is built-in

(;) :: (a ~ b) -> (b ~ c) -> (a ~ c)
-- (;) is built-in

γₙ :: k -> (p :: k) -> Container p ~ [Int]
γₙ k p = Container.NTCo:Container[0] <k>_N <p>_N

γ₃ :: Container 3 ~ [Int]
γ₃ = γₙ GHC.TypeLits.Nat 3

γ₄ :: Container 4 ~ [Int]
γ₄ = γₙ GHC.TypeLits.Nat 4

γ₄′ :: [Int] ~ Container 4
γ₄′ = Sym γ₄

γₓ :: Container 3 ~ Container 4
γₓ = γ₃ ; γ₄′

Вот исходные файлы, которые я использовал:

Контейнер.hs:

{-# LANGUAGE FlexibleContexts, UndecidableInstances, ScopedTypeVariables,
             RoleAnnotations, PolyKinds, DataKinds #-}

module Container (Container(), runContainer) where

import Data.Proxy
import Data.Reflection
import Data.Coerce

newtype Container p = Container { runContainer :: [Int] }
    deriving (Eq, Show)
type role Container nominal

instance Reifies p Integer => Monoid (Container p) where
  mempty = Container $ replicate (fromIntegral (reflect (Proxy :: Proxy p))) 0
  mappend (Container l) (Container r) = Container $ l ++ r

c3 :: Container 3
c3 = mempty

-- Works
c4 :: Container 4
c4 = coerce c3

ContainerClient.hs:

{-# LANGUAGE DataKinds #-}

module ContainerClient where

import Container
import Data.Coerce

c3 :: Container 3
c3 = mempty

-- Doesn't work :-)
c4 :: Container 4
c4 = coerce c3