GHC存在量化的单身人士
我正在使用GHC 7.10和singletons软件包。 在这个库中有一个名为SomeSing的GADT，它允许你对单例进行存在量化。 它的定义如下所示：
data SomeSing (kproxy :: KProxy k) where
SomeSing :: Sing (a :: k) -> SomeSing ('KProxy :: KProxy k)
它效果很好。 我们可以用这个来包装一个单例，这样只有类型是已知的，而不是类型。
我想创建一个变体，一个类似的包装器，它可以让我包装一个单例，并将类型函数的结果应用于它：
data SomeSingWith (kproxy :: KProxy k) (f :: TyFun k n -> *) where
SomeSingWith :: Sing (a :: k) -> Apply g a -> SomeSingWith ('KProxy :: KProxy k) g
但是，我得到这个错误：
Data constructor ‘SomeSingWith’ cannot be GADT-like in its *kind* arguments
SomeSingWith :: forall (k :: BOX) (g :: TyFun k * -> *) (a :: k).
Sing a -> Apply g a -> SomeSingWith 'KProxy g
In the definition of data constructor ‘SomeSingWith’
In the data declaration for ‘SomeSingWith’
这是什么意思？ 它可以修复，还是我在GHC中做的不可能？
我想到了。 TyFun的第二个参数需要被激发*而不是被允许成为任意类型。 这是有道理的。 但是，与该错误相关的错误消息并不有用。
data SomeSingWith (kproxy :: KProxy k) (f :: TyFun k * -> *) where
SomeSingWith :: Sing (a :: k) -> Apply g a -> SomeSingWith ('KProxy :: KProxy k) g