How do I make an empty HVecF?

[kozross]

My understanding is that I have to use constructF, but I cannot understand how I would use it, since it seems to return a function.

[Shimuuar]

If you want to construct vector v f where ElemF v ~ '[] then you indeed can use constructF. In that case its type is TFun f '[] (v f). Now TFun is just newtype over Fn f '[] (v f) ~ v f. So what you need is just: unTFun constructF