content: -- Based on https://github.com/idris-lang/Idris-dev/blob/v0.9.10/libs/effects/Effects.idr
  
  {-# LANGUAGE DataKinds, PolyKinds, ScopedTypeVariables, TypeOperators,
               TypeApplications, GADTs, TypeFamilies, AllowAmbiguousTypes #-}
  
  module T12442 where
  
  import Data.Kind
  
  data family Sing (a :: k)
  data TyFun :: Type -> Type -> Type
  type a ~> b = TyFun a b -> Type
  infixr 0 ~>
  type family (a :: k1 ~> k2) @@ (b :: k1) :: k2
  
  data TyCon1 :: (Type -> Type) -> (Type ~> Type)
  type instance (TyCon1 t) @@ x = t x
  
  data TyCon2 :: (Type -> Type -> Type) -> (Type ~> Type ~> Type)
  type instance (TyCon2 t) @@ x = (TyCon1 (t x))
  
  data TyCon3 :: (Type -> Type -> Type -> Type) -> (Type ~> Type ~> Type ~> Type)
  type instance (TyCon3 t) @@ x = (TyCon2 (t x))
  
  type Effect = Type ~> Type ~> Type ~> Type
  
  data EFFECT :: Type where
    MkEff :: Type -> Effect -> EFFECT
  
  data EffElem :: (Type ~> Type ~> Type ~> Type) -> Type -> [EFFECT] -> Type where
    Here :: EffElem x a (MkEff a x ': xs)
  
  data instance Sing (elem :: EffElem x a xs) where
    SHere :: Sing Here
  
  type UpdateResTy :: forall e a. forall b t xs ->
                      EffElem e a xs -> e @@ a @@ b @@ t -> [EFFECT]
  type family UpdateResTy b t xs elem thing where
    UpdateResTy b _ (MkEff a e ': xs) Here n = MkEff b e ': xs
  
  data EffM :: (Type ~> Type) -> [EFFECT] -> [EFFECT] -> Type -> Type
  
  effect :: forall e a b t xs prf eff m.
            Sing (prf :: EffElem e a xs)
         -> Sing (eff :: e @@ a @@ b @@ t)
         -> EffM m xs (UpdateResTy b t xs prf eff) t
  effect = undefined
  
  data State :: Type -> Type -> Type -> Type where
    Get :: State a a a
  
  data instance Sing (e :: State a b c) where
    SGet :: Sing Get
  
  type STATE t = MkEff t (TyCon3 State)
  
  get_ :: forall m x. EffM m '[STATE x] '[STATE x] x
  get_ = effect @(TyCon3 State) SHere SGet
  