GHC 存在量化单例答案

【问题标题】：GHC existentially quantified singletonGHC 存在量化单例
【发布时间】：2015-11-19 11:51:29
【问题描述】：

我正在使用 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 中做的事情是不可能的？

【问题讨论】：

GADT 是一种按类型索引的代数数据类型，但无论出于何种技术原因，您都不能拥有基于种类索引的 GADT。这就是错误的含义。

标签： haskell ghc

【解决方案1】：

我想通了。 TyFun 的第二个参数需要为 * 类型，而不是任意类型。这是有道理的。但是，与错误相关的错误消息没有帮助。

data SomeSingWith (kproxy :: KProxy k) (f :: TyFun k * -> *) where
  SomeSingWith :: Sing (a :: k) -> Apply g a -> SomeSingWith ('KProxy :: KProxy k) g

【讨论】：

请注意，您不需要将kproxy 作为SomeSingWith 的索引，因为k 在f 的种类中很明显。
这里的定义与问题中的定义相同。这是故意的吗？
@ReidBarton 对不起。我在写问题的过程中发现了解决方案，但我还是决定完成它。看起来我确实意外地在问题中发布了解决方案。我将其更改为非工作版本（这是一个字符的差异）。