Matching on type level Nat in GHC 7.6

Question

My question is probably easiest to explain in the form of an example:

type family   Take (n :: Nat) (xs :: [k]) :: [k]
type instance Take 0     xs        = '[]
type instance Take (n+1) (x ': xs) = x ': Take n xs

The second instance here is rejected, though, because (+), being a type family itself, can’t be used in the arguments. But there doesn’t seem to be any Succ or anything that is usually used for matching Nats.

So, can this be expressed; and if so, how?

Update. I notice that the isZero and isEven functions in GHC.TypeLits are under the heading “Destructing type-nats”. Are they meant to be used at the type level somehow? I would suspect not… but mostly because I can’t see how to. :)

Answer 1

I think this is a known problem in the current implementation of TypeNats. But it is being worked on, have a look at: https://plus.google.com/117760254622432568621/posts/iMYU2SMViay