haskell - 为什么 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 - 当然不能统一。
更新!
以下更改修复了编译:

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编译。

Answer 1

我相信@dfeuer 关于缺乏对类型/数据系列的“角色”支持的评论提供了答案。
对于顶级，data -定义的参数化类型:

data Foo a = ...

类型的强制力 Foo a和 Foo b取决于参数 a的作用.特别是，如果 a s 角色是名义上的，那么 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 .这是因为类型安全强制的算法处理 newtype s 不同于“等效” data类型，正如您在问题中所指出的那样——无论类型参数的作用如何，只要构造函数在范围内，它们总是可以通过展开立即强制执行。
因此，尽管如此，您对关联数据系列的体验与将系列的类型参数设置为 nominal 的角色是一致的。 .虽然我在 GHC 手册中找不到它，但这似乎是设计的行为，并且有 an open ticket确认所有数据/类型系列都分配了所有参数 nominal角色并提议放宽此限制，而@dfeuer 实际上有一个 detailed proposal从去年十月开始。