爲什麼不存在量化和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)