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

Posted 2023-02-18

【中文标题】为啥 GHC 在使用 Coercible 约束时会自相矛盾？

【英文标题】：Why is GHC contradicting itself when using a Coercible constraint?为什么 GHC 在使用 Coercible 约束时会自相矛盾？

【发布时间】：2021-04-02 21:53:26

【问题描述】：

为什么 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 (Bar a) (Bar b) 推断 Coercible a 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 编译。

【问题讨论】：

很奇怪。我很想说这显然是类型检查器中的一个错误。

首先，您可以通过指出函数test :: forall a b. (Coercible (Bar a) (Bar b)) => Bar a -> Bar b 与实现test = coerce 以GHCi 中的test :: Bar b -> Bar b 类型结束来简化示例代码。也就是说，您能否提供一个在任何实际具体类型中使用 withBaz 的示例？例如，对于toMaybeBaz，您认为可以强制转换为MabyeBar (Bar a) 的类型是什么？

"你心目中的哪种类型可以强制转换为MabyeBar (Bar a)？" - Bar a，Bar (Maybe a) 是一个包装器。它们在内存中显然具有相同的表示，因此它们应该是可强制的。

我添加了一个更新，因为@DDub 的评论启发我回顾了一些旧代码确实以这种方式使用coerce，我发现它具有关联数据系列的newtype 声明，而不是data 声明。

【参考方案1】：

我相信 @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

因为Foo a中参数a的nominal角色，所以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 手册中找不到它的记录，但这似乎是设计的行为，并且有 an open ticket 承认所有数据/类型系列的所有参数都分配了 nominal 角色并建议放宽此限制，并且 @ dfeuer 实际上有一个从去年 10 月开始的detailed proposal。

【讨论】：

SPJ 可能有票。我有a proposal。我相当不假思索地删除了评论周四的答案是基于... Oooops。

"newtypes ... 总是通过展开立即强制...不管类型参数的作用" - 这是一个有趣的设计选择。你知道它来自哪里吗？我觉得，如果你明确写 type role MyNewType nominal，GHC 会忽略你的规范似乎绝对是疯子。

阅读the paper 可能会有所帮助。基本上，角色控制具有相同类型构造函数和不同参数化的类型之间的强制：例如，可以将MyNewType FirstType 强制转换为MyNewType SecondType。相反，从newtype 到其包装值的强制转换（例如，给定newtype MyNewType a = MyNewType a，将MyNewType a 强制转换为a）是通过使构造函数在范围内来控制的（理由是它只是一个零成本的替代方案到case x of MyNewtype y -> y)。

如果您希望角色与newtypes 相关，请安排使构造函数超出范围，例如将其隐藏在模块中。