具有RankNTypes的newtype

Question

如果我想声明一个newtype类型的类型被约束为具有类型类的实例,我似乎可以这样做:

{-# LANGUAGE RankNTypes #-}

newtype ShowBox = ShowBox (forall a. Show a => a)

GHC编译就好了,但是当我尝试并实际使用ShowBox时

ShowBox "hello"

我收到编译器错误

<interactive>:1:18:
    Could not deduce (a ~ [Char])
    from the context (Show a)
      bound by a type expected by the context: Show a => a
      at <interactive>:1:10-24
      `a' is a rigid type variable bound by
          a type expected by the context: Show a => a at <interactive>:1:10
    In the first argument of `ShowBox', namely `"hello"'
    In the expression: ShowBox "hello"
    In an equation for `a': a = ShowBox "hello"

有没有办法让这项工作？

Answer 1

你向编译器承诺,你放入的值ShowBox将具有该类型forall a. Show a => a.这种类型只有一个可能的值,而且它是_|_.我想你可能想要一个存在类型,看起来很相似,但意味着一些非常不同的东西.

{-# LANGUAGE ExistentialQuantification #-}

data ShowBox = forall a. Show a => ShowBox a

这必须用data,而不是newtype.在这种情况下,构造函数上的模式匹配是将Show实例放入范围的原因.由于newtypes没有运行时表示,因此它们无法存储存在量化所暗示的多态见证.

Answer 2

好吧,你的Show构造函数有这种类型:

Show :: (forall a. Show a => a) -> ShowBox

你试图将这个函数应用于[Char]不是类型的类型forall a. Show a => a,因为它a是一个"Skolem变量",只能在非常严格的规则下与其他类型统一(其他人能够比我更好地解释).

你确定以下不是你想要的(modulo datavs. newtype)吗？为什么要forall在构造函数内部进行范围调整？

-- Show :: Show a => a -> ShowBox
data ShowBox = forall a. Show a => Show a