haskell - 是否可以为强制写一个别名？

Question

假设出于这个问题的目的，我想创建 coerce 的别名。 .我从显而易见的开始

import Data.Coerce

q = coerce

有点令人惊讶的是，这会产生一个错误:

coerce.hs:3:5: error:
    • Couldn't match representation of type ‘a0’ with that of ‘b0’
        arising from a use of ‘coerce’
    • In the expression: coerce
      In an equation for ‘q’: q = coerce
    • Relevant bindings include q :: a0 -> b0 (bound at coerce.hs:4:1)
  |
4 | q = coerce
  |     ^^^^^^

这个错误非常不透明，所以我拍了 coerce的类型签名1转至 q :

{-# Language RankNTypes #-}
{-# Language KindSignatures #-}
{-# Language PolyKinds #-}
import Data.Coerce
import GHC.Exts

q :: forall (k :: RuntimeRep) (a :: TYPE k) (b :: TYPE k). Coercible a b => a -> b
q = coerce

但这会导致错误:

coerce.hs:8:5: error:
    Cannot use function with levity-polymorphic arguments:
      coerce :: a -> b
    Levity-polymorphic arguments: a :: TYPE k
  |
8 | q = coerce
  |     ^^^^^^

这个错误不是很有帮助。它告诉我，轻浮多态性存在问题，仅此而已。
我真正好奇的是，当我制作 q底部:

{-# Language RankNTypes #-}
{-# Language KindSignatures #-}
{-# Language PolyKinds #-}
import Data.Coerce
import GHC.Exts

q :: forall (k :: RuntimeRep) (a :: TYPE k) (b :: TYPE k). Coercible a b => a -> b
q = q

错误消失，代码编译正常。
我不确定这样的别名是否可能，或者别名的问题是什么。 q 是否可以使用这样的别名？维护 coerce 的类型?编译器在我的代码中遇到什么问题？

1:正如评论所指出的，这种类型签名仅在 base-4.13 或 ghc 8.8 之后才具有轻量多态性。出于这个问题的目的，我们需要 levity 多态性。

Answer 1

@dfeuer 的回答涵盖了一种解决方法，但我认为 issue #17670解释了为什么会这样。因为coerce是一个primop，它必须是完全饱和的，所以任何使用都是隐式的eta-expanded。当你写:

q = coerce

你真的在写:

q = \x -> coerce x

您收到的初始错误消息实际上是单态限制的结果。如果你写:

q x = coerce x

或添加 NoMonomorphismRestriction扩展，程序被接受。不幸的是，结果 q不是轻浮多态的。它是用提升类型实例化的。
如果尝试通过添加适当的多态类型签名来强制问题:

q :: forall (k :: RuntimeRep) (a :: TYPE k) (b :: TYPE k). Coercible a b => a -> b
q = coerce

然后 GHC 的前沿版本(例如，上个月从源代码构建的“8.11”)给出了详细的错误消息:

BadCoerce.hs:11:5: error:
    Cannot use function with levity-polymorphic arguments:
      coerce :: a -> b
    (Note that levity-polymorphic primops such as 'coerce' and unboxed tuples
    are eta-expanded internally because they must occur fully saturated.
    Use -fprint-typechecker-elaboration to display the full expression.)
    Levity-polymorphic arguments: a :: TYPE k

最终，您遇到了禁止任何变量(在本例中为 eta-expand coerce 引入的隐式变量)被允许为轻率多态的禁令。原因 q = q有效的是没有 eta 扩展，因此不涉及变量。试试 q x = q x它将失败，并显示“此处不允许使用 levity-polymorphic 类型”错误消息。