content: {-# LANGUAGE ConstraintKinds #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE UndecidableInstances #-}
  module T18747B where
  
  import Data.Kind
  import Data.Type.Equality
  
  type family Sing :: k -> Type
  
  data SomeSing (k :: Type) where
    SomeSing :: Sing (a :: k) -> SomeSing k
  
  type family Promote (k :: Type) :: Type
  type family PromoteX (a :: k) :: Promote k
  
  type family Demote (k :: Type) :: Type
  type family DemoteX (a :: k) :: Demote k
  
  type SingKindX (a :: k) = (PromoteX (DemoteX a) ~~ a)
  
  class SingKindX k => SingKind k where
    toSing :: Demote k -> SomeSing k
  
  type instance Demote Type = Type
  type instance Promote Type = Type
  type instance DemoteX (a :: Type) = Demote a
  type instance PromoteX (a :: Type) = Promote a
  
  type instance Demote Bool = Bool
  type instance Promote Bool = Bool
  
  data Foo (a :: Type) where MkFoo :: Foo Bool
  
  data SFoo :: forall a. Foo a -> Type where
    SMkFoo :: SFoo MkFoo
  type instance Sing = SFoo
  
  type instance Demote (Foo a) = Foo (DemoteX a)
  type instance Promote (Foo a) = Foo (PromoteX a)
  
  instance SingKindX a => SingKind (Foo a) where
    toSing MkFoo = SomeSing SMkFoo
  
  