为什么 GHC 在使用 Coercible 约束时会自相矛盾？

Question

为什么 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- 当然不是统一的。

更新！

以下更改修复了编译：

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

即 - 将数据系列声明为 a newtype，而不是 a data。这似乎与 GHCCoercible在一般语言中的处理一致，因为

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

会不会导致Coercible被生成的实例-即使它绝对应该强制转换到a。使用上面的声明，这将出错：

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

但是有一个newtype声明：

data Id a = Id a

然后Coercible实例存在并wrapId编译。

Answer 1

我相信 @dfeuer 已删除的有关类型/数据系列缺乏“角色”支持的评论提供了答案。

\n

对于顶级data定义的参数化类型：

\n

data Foo a = ...\n

\n

类型的可强制执行性Foo a取决于Foo b参数的作用a。特别是，如果as 角色是名义上的，则Foo a和Foo b是可强制的当且仅当a和b是完全相同的类型。

\n

所以，在程序中：

\n

{-# LANGUAGE FlexibleContexts #-}\n{-# LANGUAGE RoleAnnotations #-}\n\nimport Data.Coerce\n\ntype role Foo nominal\ndata Foo a = Foo\n\nfoo :: (Coercible (Foo a) (Foo b)) => a -> b\nfoo = undefined\n

\n

由于中nominal参数的作用， 的类型实际上被简化为：aFoo afoob -> b

\n

\xce\xbb> :t foo\nfoo :: b -> b\n

\n

如果角色注释从 更改为nominal，则representational类型会简化为Coercible a b => a -> b，如果角色更改为phantom（此特定声明的默认值Foo，因为a没有出现在右侧），则类型会简化为a -> b。这一切都符合预期，并且对应于每个角色的定义。

\n

请注意，如果您将 的 声明替换Foo为：

\n

data Foo a = Foo a\n

\n

那么该phantom角色将不再被允许，但foo在其他两个角色下的推断类型将与以前完全相同。

\n

data然而，如果从 a 切换到 a ，就会有一个重要的区别newtype。和：

\n

newtype Foo a = Foo a\n

\n

您会发现，即使使用type role Foo nominal， 的推断类型foo也将Coercible b a => a -> b代替b -> b。这是因为类型安全强制转换的算法处理newtypes 的方式与“等效”data类型不同，正如您在问题中指出的那样——只要构造函数在作用域内，它们总是可以通过展开立即强制转换，无论角色如何的类型参数。

\n

因此，尽管如此，您对关联数据族的体验与将族类型参数设置为 的角色是一致的nominal。虽然我在 GHC 手册中找不到它的记录，但这似乎是设计的行为，并且有一个开放的票证承认所有数据/类型系列都具有指定角色的所有参数nominal，并建议放宽此限制，并且@dfeuer 实际上在去年 10 月就有了一份详细的提案。

\n