[Haskell-cafe] Splitting HList

[Gautier DI FOLCO]

Hello,

I want to know if it is possible to split a HList?
I want to have a function like this:
splitV :: HList (s ++ s') -> (HList s, HList s')
splitV = _

So I have begun by something which I thought simple:
type family   HSplit (ts :: [k]) (xs :: [k]) :: ([k], [k])
type instance HSplit ts xs = ([xs], SndHSplit ts xs)

type family   SndHSplit (ts :: [k]) (xs :: [k]) :: [k]
type instance SndHSplit ts '[] = ts
type instance SndHSplit (t ': ts) (x ': xs) = SndHSplit ts xs

But I get the following error:
H.hs:133:50:
    The second argument of ‘SndHSplit’ should have kind ‘[k0]’,
      but ‘xs’ has kind ‘*’
    In the type ‘([xs], SndHSplit ts xs)’
    In the type instance declaration for ‘HSplit’

I don't understand why because xs and the first element of the tuple have
the same kind ([k]).

Thanks by advance for your help/explanations.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140613/0b71dc7b/attachment.html>