How to use the comparison in GHC.TypeLits
I ran into problems playing with GHC.TypeLits. Consider the following GADT:
data Foo :: Nat -> * where
SmallFoo :: (n <= 2) => Foo n
BigFoo :: (3 <= n) => Foo n
My understanding was, that now for every n , the type Foo n is populated by exactly one value (which is either a SmallFoo or a BigFoo depending on the value of n ).
But if I now want to construct a concrete instance as follows:
myFoo :: Foo 4
myFoo = BigFoo
Then GHC (7.6.2) spits out the following error message:
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
This seems odd - I expected there to be a predefined instance for such type level nat comparisons. How can I express these kinds of constraints in my data constructor using type level naturals?
Solver for TypeLists is not in GHC right now, according to status page there are some chances that it will be in GHC 7.8 in october or something.
Maybe it's better to use other packages for now.
This compiles on the current head of the type-nats branch, which should (hopefully) be merged for 7.8.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
module X where
import GHC.TypeLits
data Foo :: Nat -> * where
SmallFoo :: (n <= 2) => Foo n
BigFoo :: (3 <= n) => Foo n
myFoo :: Foo 4
myFoo = BigFoo
Where if myFoo is changed to be of type Foo 1 it fails to compile, presumably because the x <= y class constraint is expanded to the (x <=? y) ~ 'True equality constraint:
$ /Source/ghc/inplace/bin/ghc-stage1 /tmp/blah.hs
[1 of 1] Compiling X ( /tmp/blah.hs, /tmp/blah.o )
/tmp/blah.hs:16:13:
Couldn't match type ‛3 <=? 1’ with ‛'True’
In the expression: BigFoo
In an equation for ‛myFoo’: myFoo = BigFoo
上一篇: Haskell无法统一类型实例方程
下一篇: 如何使用GHC.TypeLits中的比较