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.