haskell - 为什么存在量化和数据种类不能一起工作？

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是Kind变量，不是类型变量。怎么回事？

Answer 1

在 GHC 8 之前，任何地方都不允许种类绑定(bind)。在这里，我们必须使用种类代理。在这种情况下我们可以这样做:

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)