haskell - 如何在 GHC.TypeLits 中使用比较

Question

我在玩 GHC.TypeLits 时遇到了问题.考虑以下 GADT:

data Foo :: Nat -> * where
  SmallFoo :: (n <= 2)  => Foo n
  BigFoo   :: (3 <= n)  => Foo n

我的理解是，现在对于每个 n , 类型 Foo n仅由一个值填充(取决于 n 的值，它是 SmallFoo 或 BigFoo )。

但是如果我现在想构造一个具体的实例如下:

myFoo :: Foo 4
myFoo = BigFoo

然后 GHC (7.6.2) 吐出以下错误信息:

No instance for (3 <= 4) arising from a use of `BigFoo'
Possible fix: add an instance declaration for (3 <= 4)
In the expression: BigFoo
In an equation for `myFoo': myFoo = BigFoo

这看起来很奇怪——我希望有一个预定义的实例用于这种类型级别的 nat 比较。如何使用类型级别的自然属性在我的数据构造函数中表达这些类型的约束？

Answer 1

根据 status page，TypeLists 的求解器现在不在 GHC 中。很有可能它会在 10 月的 GHC 7.8 或其他版本中出现。

也许使用 other packages 会更好目前。