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

我在使用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比较。如何使用类型级别的自然表达在数据构造函数中表达这些约束？

最佳答案

根据status page的说法，TypeLists的求解器现在不在GHC中，根据十月份的情况，它很有可能会出现在GHC 7.8中。

也许现在最好使用other packages。