Почему GHC противоречит сам себе при использовании ограничения Coercible?

Почему GHC делает вывод об унификации из принуждения связанных данных и почему он противоречит своей собственной сигнатуре проверенного типа, чтобы сделать это?

Эта проблема

{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeFamilies #-}

module Lib
    ( 
    ) where

import Data.Coerce

class Foo a where
  data Bar a

data Baz a = Baz
  { foo :: a
  , bar :: Bar a
  }

type BarSame a b = (Coercible (Bar a) (Bar b), Coercible (Bar b) (Bar a))

withBaz :: forall a b. BarSame a b => (a -> b) -> Baz a -> Baz b
withBaz f Baz{..} = Baz
  { foo = f foo
  , bar = coerce bar
  }

Это все хорошо - GHC с радостью скомпилирует этот код и уверен, что withBaz имеет заявленную подпись.

А теперь попробуем им воспользоваться!

instance (Foo a) => Foo (Maybe a) where
  data Bar (Maybe a) = MabyeBar (Bar a)

toMaybeBaz :: Baz a -> Baz (Maybe a)
toMaybeBaz = withBaz Just

Это дает ошибку, но очень странную:

withBaz Just
^^^^^^^^^^^^
cannot construct the infinite type: a ~ Maybe a

Действительно, если я войду в GHCi и попрошу дать мне тип withBaz:

ghc>:t withBaz
withBaz :: (b -> b) -> Baz b -> Baz b

Это не моя подпись.

Принуждение

Я подозреваю, что GHC обрабатывает аргументы типа withBaz, как будто они должны объединяться, потому что он выводит Coercible a b из Coercible (Bar a) (Bar b). Но поскольку это семейство данных, они даже не должны быть Coercible - уж точно не унифицируемыми.

Обновлять!

Следующее изменение исправляет компиляцию:

instance (Foo a) => Foo (Maybe a) where
  newtype Bar (Maybe a) = MabyeBar (Bar a)

То есть объявить семейство данных как newtype вместо data. Это похоже на то, как GHC рассматривает Coercible в языке в целом, в том смысле, что

data Id a = Id a

не вызовет генерацию экземпляра Coercible, хотя он определенно должен быть принудительным к a. С указанным выше объявлением это приведет к ошибке:

wrapId :: a -> Id a
wrapId = coerce

Но с объявлением newtype:

newtype Id a = Id a

тогда экземпляр Coercible существует, и wrapId компилируется.


coercion haskell ghc type-families
person Isaac van Bakel    schedule 24.12.2020    source источник
comment
Очень странно. Я хочу сказать, что это явно ошибка в проверке типов.   -  person leftaroundabout    schedule 24.12.2020
comment
Во-первых, вы можете упростить свой примерный код, просто указав, что функция test :: forall a b. (Coercible (Bar a) (Bar b)) => Bar a -> Bar b с реализацией test = coerce заканчивается типом test :: Bar b -> Bar b в GHCi. Тем не менее, можете ли вы привести пример использования withBaz для любого конкретного типа? Например, для toMaybeBaz, какой тип вы имеете в виду, который может быть приведен к MabyeBar (Bar a)?   -  person DDub    schedule 24.12.2020
comment
какой тип вы имеете в виду, который может быть приведен к MabyeBar (Bar a)? - Bar a, который Bar (Maybe a) - это оболочка. У них явно есть одно и то же представление в памяти, поэтому они должны быть принудительными.   -  person Isaac van Bakel    schedule 24.12.2020
comment
Я добавил обновление, так как комментарий @DDub побудил меня оглянуться назад на некоторый старый код, который действительно использовал coerce таким образом, и я обнаружил, что в нем есть объявление newtype для связанных данных семья, а не data.   -  person Isaac van Bakel    schedule 24.12.2020

Ответы (1)


arrow_upward
3
arrow_downward

Я считаю, что удаленный комментарий @dfeuer об отсутствии поддержки ролей для семейств типов / данных дает ответ.

Для параметризованного типа верхнего уровня, определенного data:

data Foo a = ...

приводимость типов Foo a и Foo b зависит от роли параметра a. В частности, если роль as номинальная, то Foo a и Foo b являются принудительными тогда и только тогда, когда a и b относятся к одному и тому же типу.

Итак, в программе:

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RoleAnnotations #-}

import Data.Coerce

type role Foo nominal
data Foo a = Foo

foo :: (Coercible (Foo a) (Foo b)) => a -> b
foo = undefined

из-за nominal роли параметра a в Foo a тип foo фактически упрощен до b -> b:

λ> :t foo
foo :: b -> b

Если аннотация роли изменяется с nominal на representational, тип упрощается до Coercible a b => a -> b, а если роль изменяется на phantom (значение по умолчанию для этого конкретного объявления Foo, поскольку a не отображается справа), тип упрощен до a -> b. Все это ожидаемо и соответствует определению каждой из этих ролей.

Обратите внимание, что если вы заменили объявление Foo на:

data Foo a = Foo a

тогда роль phantom больше не будет разрешена, но предполагаемые типы для foo для двух других ролей будут точно такими же, как раньше.

Однако есть важное различие, если вы переключитесь с data на newtype. С участием:

newtype Foo a = Foo a

вы обнаружите, что даже с type role Foo nominal предполагаемый тип для foo будет Coercible b a => a -> b вместо b -> b. Это связано с тем, что алгоритм типобезопасного приведения обрабатывает newtypes иначе, чем эквивалентные data типы, как вы отметили в своем вопросе - они всегда немедленно приводятся к принудительному развертыванию всякий раз, когда конструктор находится в области видимости, независимо от роли параметра типа.

Итак, с учетом всего сказанного, ваш опыт работы со связанными семействами данных согласуется с ролью параметра типа семейства, установленного на nominal. Хотя я не смог найти это задокументировано в руководстве GHC, похоже, что это поведение соответствует задумке, и есть открытый тикет, подтверждающий, что всем семействам данных / типов присвоена nominal роль всех параметров, и предлагается ослабить это ограничение, а у @dfeuer фактически есть подробное предложение от октября прошлого года.

person K. A. Buhr    schedule 24.12.2020
comment
У SPJ может быть билет. У меня есть предложение. Я довольно легкомысленно удалил комментарий. Чт, ответ основан на ... Ой. - person dfeuer; 24.12.2020
comment
newtypes ... всегда немедленно приводятся к принудительному исполнению через развертывание ... независимо от роли параметра типа - это интересный выбор дизайна. Вы знаете, откуда это? Мне кажется, что если вы явно напишете type role MyNewType nominal, то, что GHC проигнорирует вашу спецификацию, кажется совершенно безумным. - person Isaac van Bakel; 26.12.2020
comment
Возможно, вам будет полезно прочитать статью < / а>. По сути, роли управляют приведением типов между типами с одним и тем же конструктором типов и разными параметризациями: например, MyNewType FirstType может быть приведено к MyNewType SecondType. Напротив, принуждение от newtype к его обернутому значению (например, при заданном newtype MyNewType a = MyNewType a, принуждение от MyNewType a к a) регулируется наличием конструктора в области видимости (с объяснением, что это просто альтернатива с нулевой стоимостью для case x of MyNewtype y -> y). - person K. A. Buhr; 26.12.2020
comment
Если вы хотите, чтобы роли имели значение с newtypes, сделайте так, чтобы конструктор был вне области видимости, например, скрыв его в модуле. - person K. A. Buhr; 26.12.2020