为什么不存在量化和datakinds一起工作？

Question

{-# LANGUAGE DataKinds, ExistentialQuantification, KindSignatures #-} 
import Data.Proxy 

data Type t= forall (a :: t). Type (Proxy a) 

给出了错误

Type variable ‘t’ used in a kind 
In the kind ‘t’ 
In the definition of data constructor ‘Type’ 
In the data declaration for ‘Type’ 

但是t是一类变量，而不是一个类型变量。这是怎么回事？

Answer 1

类型构造器的参数的数据类型，不种。所以data Type t = ...意味着t是一个类型变量。

在GHC 8.0 TypeInType扩展删除类型和种类之间的区别，让你启用（和GHC会建议使分机，如果你不这样做），你的程序被接受。

Answer 2

到GHC 8之前，因为没有获准一种绑定，随时随地。在这里，我们必须使用类型代理。在这种情况下，我们可以这样做：

import Data.Proxy 

data Type (kp :: KProxy k) = forall (a :: k). Type (Proxy a) 

随着GHC 8，你确实可以写你的原始版本：

{-# language TypeInType #-} 

data Type t = forall (a :: t). Type (Proxy a)