for https://qiita.com/as_capabl/items/2031fe28e577e77dc269

Siri.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Siri where

import GHC.TypeLits (Nat)
import GHC.TypeLits.List (KnownNats, natsVal, NatList(..), natsList)
import Data.Proxy (Proxy(..))
import Control.Category (Category(..))
import Data.Singletons
import Data.Constraint
import Data.Singletons.Prelude.List ((:++), Sing(SNil, SCons))
import Data.Singletons.TypeLits (withKnownNat)
import Prelude hiding ((.))

data Siri (xs :: [Nat]) (a :: Nat) (b :: Nat) where
  SiriUnit :: Proxy a -> Siri '[a] a a
  SiriCons :: Proxy a -> (Siri ys b c) -> Siri (a ': ys) a c

siriConcat :: Siri xs a b -> Siri xs' b c -> Siri (xs :++ xs') a c
siriConcat (SiriUnit proxy) ks = SiriCons proxy ks
siriConcat (SiriCons proxy ks) ks' = SiriCons proxy (ks `siriConcat` ks')

showSiri :: KnownNats xs => Siri xs a b -> String
showSiri (_ :: Siri xs a b) = map (toEnum . fromEnum) $ natsVal (Proxy @xs)

data AllSiri a b where
  AllSiriId :: AllSiri a a
  AllSiriContent :: KnownNats xs => Siri xs a b -> AllSiri a b

instance Category AllSiri where
  id = AllSiriId
  f . g = g `allSiriConcat` f

allSiriConcat :: AllSiri a b -> AllSiri b c -> AllSiri a c
allSiriConcat AllSiriId k = k
allSiriConcat k AllSiriId = k
allSiriConcat (AllSiriContent x) (AllSiriContent y) = withDict (go x y) $ AllSiriContent $ siriConcat x y where
  go :: (KnownNats xs, KnownNats ys) => Siri xs a b -> Siri ys b c -> Dict (KnownNats (xs :++ ys))
  go x' y' = typeLevelConcatPreservesKnownNatsConstraint (toD x') (toD y') where
    toD :: KnownNats xs => Siri xs a b -> Dict (KnownNats xs)
    toD _ = Dict

singToDict :: Sing xs -> Dict (KnownNats xs)
singToDict SNil = Dict
singToDict (SCons x xs) = withKnownNat x $ (\Dict -> Dict) (singToDict xs)

dictToSing :: Dict (KnownNats xs) -> Sing xs
dictToSing d = withDict d $ go natsList where
  go :: NatList ns -> Sing ns
  go ØNL = SNil
  go (_ :<# ns) = SCons sing (go ns)

typeLevelConcatPreservesKnownNatsConstraint :: Dict (KnownNats xs) -> Dict (KnownNats ys) -> Dict (KnownNats (xs :++ ys))
typeLevelConcatPreservesKnownNatsConstraint = go . dictToSing where
  go :: Sing xs -> Dict (KnownNats ys) -> Dict (KnownNats (xs :++ ys))
  go SNil ys = ys
  go (SCons x xs) ys = singToDict $ SCons x $ dictToSing $ go xs ys