Trying to encode a Sigma like type on haskell with StandaloneKindSignatures

sigma.hs

{-# language RankNTypes, PolyKinds, TypeFamilies, GADTs, StandaloneKindSignatures, DataKinds #-}
module Main where

import Data.Kind (Type)
import Data.Functor.Identity

main :: IO ()
main = return ()

type Tag :: Bool -> Type
data Tag b where
  STrue :: Tag True
  SFalse :: Tag False

type ApplyTag :: Bool -> Type
type family ApplyTag t where
  ApplyTag 'True = Int
  ApplyTag 'False = Char

type Sigma :: forall k. (k -> Type) -> (k -> Type) -> Type
data Sigma t f where
  (:&:) :: forall t f a. t a -> f a -> Sigma t f

ex :: Sigma Tag ApplyTag
ex = STrue :&: 27