{-# LANGUAGE PolyKinds #-} module Codec.Borsh.Internal.Util.SOP ( indices ) where import Data.SOP import Data.Word indices :: forall k (xs :: [k]). SListI xs => NP (K Word8) xs indices :: forall k (xs :: [k]). SListI xs => NP (K Word8) xs indices = forall {k} (xs' :: [k]). SList xs' -> Word8 -> NP (K Word8) xs' go forall {k} (xs :: [k]). SListI xs => SList xs sList Word8 0 where go :: forall xs'. SList xs' -> Word8 -> NP (K Word8) xs' go :: forall {k} (xs' :: [k]). SList xs' -> Word8 -> NP (K Word8) xs' go SList xs' SNil Word8 _ = forall {k} (a :: k -> *). NP a '[] Nil go SList xs' SCons Word8 ix = forall k a (b :: k). a -> K a b K Word8 ix forall {k} (a :: k -> *) (x :: k) (xs :: [k]). a x -> NP a xs -> NP a (x : xs) :* forall {k} (xs' :: [k]). SList xs' -> Word8 -> NP (K Word8) xs' go forall {k} (xs :: [k]). SListI xs => SList xs sList (forall a. Enum a => a -> a succ Word8 ix)