对'类型'的迷惑

我在GHC 8.0.1中遇到了一种奇怪的情况，它使用了kind-indexed（？）GADT，其中在类型签名和类签名中引入了多个类，产生了不同的类型检查行为。

考虑以下数据类型：

{-# 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

这种数据类型编译得很好。 然而，如果我们想在构造函数G指定x的种类，我们会得到一个类型错误。

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

这是怎么回事？

---

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一个看不见的参数，就像Proxy的k参数一样）...但是当我们写J ，没有办法确定k应该是什么，所以它总是含糊不清。 （相比之下，我们可以发现在选择k参数Proxy通过观察a的那种。）

J这个定义在8.0.1和HEAD中是不允许的。

链接地址: http://www.djcxy.com/p/33345.html

上一篇: 'Kind' of confused about forall in type

下一篇: Liberal coverage condition introduced in GHC 7.7 breaks code valid in GHC 7.6