如何在GHC.TypeLits中使用比较

Question

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

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

我的理解是,现在每个n类型Foo n都只填充一个值(根据值的值,可以是SmallFoo或BigFoo n).

但是,如果我现在想构建一个具体的实例,如下所示:

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

TypeLists的求解器现在不在GHC中,根据状态页面,它有可能在10月的GHC 7.8或其他东西.

也许最好现在使用其他包.