<div dir="ltr">Hello,<br><br>I want to know if it is possible to split a HList?<br>I want to have a function like this:<br><div style="margin-left:40px">splitV :: HList (s ++ s') -> (HList s, HList s')<br>splitV = _<br>
</div><br>So I have begun by something which I thought simple:<br><div style="margin-left:40px">type family   HSplit (ts :: [k]) (xs :: [k]) :: ([k], [k])<br>type instance HSplit ts xs = ([xs], SndHSplit ts xs)<br><br>type family   SndHSplit (ts :: [k]) (xs :: [k]) :: [k]<br>
type instance SndHSplit ts '[] = ts<br>type instance SndHSplit (t ': ts) (x ': xs) = SndHSplit ts xs<br></div><br>But I get the following error:<br><div style="margin-left:40px">H.hs:133:50:<br>    The second argument of ‘SndHSplit’ should have kind ‘[k0]’,<br>
      but ‘xs’ has kind ‘*’<br>    In the type ‘([xs], SndHSplit ts xs)’<br>    In the type instance declaration for ‘HSplit’<br></div><br>I don't understand why because xs and the first element of the tuple have the same kind ([k]).<br>
<br>Thanks by advance for your help/explanations.<br></div>