'类型'混淆了类型索引GADT中的forall

Question

我在GHC 8.0.1中遇到了奇怪的情况,它使用了类型索引(？)GADT,其中类型vs类型签名中引入foralls会产生不同的类型检查行为.

请考虑以下数据类型:

{-# LANGUAGE TypeInType, GADTs, ExplicitForAll #-}
-- Same thing happens when we replace ExplicitForAll with ScopedTypeVariables

import Data.Kind

data F (k :: * -> *) where

data G :: F k -> * where
  G :: G x

这种数据类型编译得很好.但是,如果我们要x在构造函数中指定类型,则会G出现类型错误.

data H :: F k -> * where
  H :: forall k' (x :: F k'). H x

错误消息是

• Kind variable ‘k’ is implicitly bound in datatype
  ‘H’, but does not appear as the kind of any
  of its type variables. Perhaps you meant
  to bind it (with TypeInType) explicitly somewhere?
• In the data declaration for ‘H’

如果我们添加forall到类签名(有或没有forall在构造函数中),则没有错误.

data I :: forall k. F k -> * where
  I :: I x

data J :: forall k. F k -> * where
  J :: forall k' (x :: F k'). J x

这是怎么回事？

Answer 1

这里的作者TypeInType。KA Buhr 就在上面；这只是一个错误。它固定在 HEAD 中。

对于过于好奇的人：此错误消息旨在消除诸如

data J = forall (a :: k). MkJ (Proxy a)

在哪里

data Proxy (a :: k) = Proxy

可以从 导入Data.Proxy。当用 Haskell98 风格的语法声明数据类型时，任何存在量化的变量都必须使用forall. 但k从未明确纳入范围；它只是用于 的那种a。所以这意味着k应该被普遍量化（换句话说，它应该是 的一个不可见参数J，就像 的k参数一样Proxy）...但是当我们编写 时J，没有办法确定k应该是什么，所以它总是模糊的。（相反，我们可以通过查看 的种类来发现k参数 to的选择。）Proxya

J8.0.1 和 HEAD 中不允许使用此定义。