SOPExt.hs

type family Repeat (n :: Nat) (a :: *) :: [*] where
  Repeat 'Zero     a = '[]
  Repeat ('Succ n) a = a ': Repeat n a

fromHomSum :: SNat n -> NS f (Repeat n a) -> f a
fromHomSum SZero     ns     = case ns of {}
fromHomSum (SSucc _) (Z a)  = a
fromHomSum (SSucc n) (S as) = fromHomSum n as

toHomProd :: [f a] -> (forall n. SListI (Repeat n a) => SNat n -> NP f (Repeat n a) -> b) -> b
toHomProd []     k = k SZero Nil
toHomProd (a:as) k = toHomProd as $ \n np -> k (SSucc n) (a :* np)

type family Rotate (xs :: [*]) :: [[*]] where
  Rotate '[]       = '[]
  Rotate (x ': xs) = '[x] ': Rotate xs

rotate :: NP f xs -> (SListI2 (Rotate xs) => NP (NP f) (Rotate xs) -> b) -> b
rotate Nil       k = k $ Nil
rotate (x :* xs) k = rotate xs $ \xss -> k $ ((x :* Nil) :* xss)

unrotate :: SListI xs => NS (NP f) (Rotate xs) -> NS f xs
unrotate = go sList
  where
    go :: SList xs -> NS (NP f) (Rotate xs) -> NS f xs
    go SNil  ns             = case ns of {}
    go SCons (Z (x :* Nil)) = Z x
    go SCons (S ns)         = S (go sList ns)

Or you could use hd in unrotate rather than (\ (x :* Nil) -> x) ...