强制转换和角色——不能用 GHCi 的类型签名编译

Question

在 GHCi 中输入以下内容

>:set -XAllowAmbiguousTypes
>import Data.Coerce
>fcm f = coerce . foldMap (coerce . f)
>:t fcm
fcm
  :: (Foldable t, Monoid a1, Coercible a1 c, Coercible a2 a1) =>
     (a3 -> a2) -> t a3 -> c

好的，这就是我所期望的。将其复制粘贴到文件中。

{-# LANGUAGE AllowAmbiguousTypes #-}

import Data.Coerce

fcm :: (Foldable t, Monoid a1, Coercible a1 c, Coercible a2 a1) 
    => (a3 -> a2) -> t a3 -> c
fcm f = coerce . foldMap (coerce . f)

现在如果你将它加载到 GHCi 中，你会得到一个错误 -

Weird.hs:7:9: error:
    • Couldn't match representation of type ‘a0’ with that of ‘c’
    arising from a use of ‘coerce’
      ‘c’ is a rigid type variable bound by
    the type signature for:
      fcm :: forall (t :: * -> *) a1 c a2 a3.
             (Foldable t, Monoid a1, Coercible a1 c, Coercible a2 a1) =>
             (a3 -> a2) -> t a3 -> c
    at Weird.hs:(5,1)-(6,30)
    • In the first argument of ‘(.)’, namely ‘coerce’
      In the expression: coerce . foldMap (coerce . f)
      In an equation for ‘fcm’: fcm f = coerce . foldMap (coerce . f)
    • Relevant bindings include
    fcm :: (a3 -> a2) -> t a3 -> c (bound at Weird.hs:7:1)

嗯？ a0 哪里来的？如果删除类型签名，代码将再次正常编译。看起来我们现在有一个函数，我们无法向编译器解释其类型，GHCi 也无法告诉我们该类型是什么（它只能给我们错误）。 GHC 似乎在谈论不面向用户的内部类型变量（在本例中 a0）。

这与 Coercible 周围的黑魔法有关吗？来自 GHC.Types:

Note [Kind-changing of (~) and Coercible]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

(~) and Coercible are tricky to define. To the user, they must appear as
constraints, but we cannot define them as such in Haskell. But we also cannot
just define them only in GHC.Prim (like (->)), because we need a real module
for them, e.g. to compile the constructor's info table.

Furthermore the type of MkCoercible cannot be written in Haskell
(no syntax for ~#R).

So we define them as regular data types in GHC.Types, and do magic in TysWiredIn,
inside GHC, to change the kind and type.

我理解正确吗？或者是否可以为函数编写类型签名并成功编译代码？对于它的价值，我感兴趣的是能够写的东西稍微简单一些 -

fcm :: (Monoid m, Coercible m b, Coercible b m, Foldable f) => (a -> b) -> f a -> b
fcm f = coerce . foldMap (coerce . f)

sumBy = fcm @Sum

Answer 1

这是一个更简单的例子：

> :set -XAllowAmbiguousTypes
> import Data.Coerce
> f = coerce . coerce
> :t f
f :: (Coercible a1 c, Coercible a2 a1) => a2 -> c

到目前为止，还不错。一切看起来都很合理。但是，如果下面的代码会编译失败：

f :: (Coercible a1 c, Coercible a2 a1) => a2 -> c
f = coerce . coerce

• Couldn't match representation of type ‘a0’ with that of ‘c’
    arising from a use of ‘coerce’
  ‘c’ is a rigid type variable bound by
    the type signature for:
      f :: forall a1 c a2. (Coercible a1 c, Coercible a2 a1) => a2 -> c

为什么会这样？ a0从哪里来？

简单地说，在coerce . coerce中GHC必须选择一个中间类型，即第一次强制转换的结果。这原则上可以是任何东西，所以 GHC 为它生成了一个新的类型变量：上面，为此选择了 a0。

然后对代码进行类型检查，并将需要约束 Coercible a0 c, Coercible a2 a0。签名提供的是不同的。在这里，GHC 不会尝试 "match" 它们并选择 a0 = a1。事实上，在某些类型 class 上下文中，这可能是错误的选择。

例如：（人为的例子）

foo :: Read a => String -> ...
foo s = let
   x = read s && True
   in ...

使用 Read a 约束来解析 read s 是错误的。事实上，为此我们需要使用全局实例 Read Bool，并忽略约束。也许稍后在代码中还有另一个 read s 调用，我们确实需要约束，但在这里我们不能提交它。

要修复你的代码，你需要明确你的强制转换，告诉 GHC 你真的想使用你的约束。例如，以下类型检查 (ScopedTypeVariables on).

f :: forall a1 a2 c . (Coercible a1 c, Coercible a2 a1) => a2 -> c
f = coerce . (coerce :: a2 -> a1)

现在我们告诉GHC中间类型确实是我们的a1.

您可以通过添加类似的类型注释来修复您的代码。

强制转换和角色——不能用 GHCi 的类型签名编译

Coercion and roles - cannot compile with GHCi's type signature

haskell

ghc