# Pastebin OmivBcRe
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Kind (Type)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)

data Pet = Cat | Dog | Horse

data Pets a where
  Cats :: Pets 'Cat
  Dogs :: Pets 'Dog
  Horses :: Pets 'Horse

-- | From package "dependent-sum".
data DSum tag f = forall a. !(tag a) :=> f a

data family PetData (pet :: Pet) :: Type
newtype instance PetData 'Cat = C (Map String String)
newtype instance PetData 'Dog = D [Int]
newtype instance PetData 'Horse = H (Set Bool)

catState :: DSum Pets PetData
catState = Cats :=> C (Map.fromList [("meow", "meow")])

dogState :: DSum Pets PetData
dogState = Dogs :=> D [1, 2, 3]

horsesState :: DSum Pets PetData
horsesState = Horses :=> H mempty