haskell - 对类型索引 GADT 中的 forall 感到“有点”困惑

Question

我在 GHC 8.0.1 中遇到了一个带有种类索引 (?) GADT 的奇怪情况，其中在类型与种类签名中引入 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的作者这里。 K. A. 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 的种类来发现 Proxy 参数的选择 a。)
J 的这个定义在 8.0.1 和 HEAD 中是不允许的。