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)

fromHomSum :: forall x f xs . (All ((~) x) xs) => NS f xs -> f x
fromHomSum = hcollapse . hcmap (Proxy @((~) x)) K

toHomProd :: [f x] -> (forall xs . (All ((~) x) xs) => NP f xs -> r) -> r
toHomProd []       k = k Nil
toHomProd (x : xs) k = toHomProd xs $ \ np -> k (x :* np)

class (xs ~ '[x]) => Wrapped x xs
instance (xs ~ '[x]) => Wrapped x xs

rotate :: AllZip Wrapped xs xss => NP f xs -> NP (NP f) xss
rotate = htrans (Proxy @Wrapped) (:* Nil)

class Wrapped x xs => UnWrapped xs x
instance Wrapped x xs => UnWrapped xs x

unrotate :: AllZip UnWrapped xss xs => NS (NP f) xss -> NS f xs
unrotate = htrans (Proxy @UnWrapped) (\ (x :* Nil) -> x)

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