タイプインデックス付きGADTで混乱している「種類」

Question

GHC 8.0.1では、kind-indexed（？）GADTを使用して奇妙な状況に遭遇しましたが、タイプvs kindシグネチャで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 

このデータ型はうまくコンパイルします。ただし、Gのコンストラクタでxの種類を指定する場合は、型エラーが発生します。我々は（とまたはコンストラクタでforallせず）種類のシグネチャにforallを追加した場合

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’ 

あります。

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 Proxy (a :: k) = Proxy 

はData.Proxyからインポートすることができる

data J = forall (a :: k). MkJ (Proxy a) 

ような定義を排除することを意味する：過度に好奇心が強いため

。 Haskell98形式の構文でデータ型を宣言するときは、現存する量的な変数はすべて明示的にforallのスコープに入れなければなりません。しかしkは明示的にスコープに入れられません。それはちょうどaの種類で使用されています。だから、kは普遍的な定量化されなければなりません（換言すれば、kのパラメータがProxyのような、不可視のパラメータJ）... Jと書くと、kは何かを決定する方法がありませんしたがって、常に曖昧になります。 （これとは対照的に、我々はaの種類を見て、Proxyにkパラメータの選択肢を発見することができます。）

Jためのこの定義は、8.0.1にし、HEADに許可されていません。