content: {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
  {-# LANGUAGE ConstraintKinds #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE QuasiQuotes #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE FlexibleInstances #-}
  
  module SingletonsBug where
  
  import Control.Applicative
  import Data.Traversable (for)
  import Data.Kind (Type, Constraint)
  
  -----------------------------------
  -- From 'constraints' library
  -- import Data.Constraint (Dict(..))
  data Dict :: Constraint -> Type where
    Dict :: a => Dict a
  
  -----------------------------------
  -- From 'singletons' library
  -- import Data.Singletons hiding( withSomeSing )
  
  class SingI (a :: k) where
    -- | Produce the singleton explicitly. You will likely need the @ScopedTypeVariables@
    -- extension to use this method the way you want.
    sing :: Sing a
  
  data family Sing (a :: k)
  
  data KProxy (a :: Type) = KProxy
  
  data SomeSing (kproxy :: KProxy k) where
    SomeSing :: Sing (a :: k) -> SomeSing ('KProxy :: KProxy k)
  
  -- SingKind :: forall k. KProxy k -> Constraint
  class (kparam ~ 'KProxy) => SingKind (kparam :: KProxy k) where
    -- | Get a base type from a proxy for the promoted kind. For example,
    -- @DemoteRep ('KProxy :: KProxy Bool)@ will be the type @Bool@.
    type DemoteRep kparam :: Type
  
    -- | Convert a singleton to its unrefined version.
    fromSing :: Sing (a :: k) -> DemoteRep kparam
  
    -- | Convert an unrefined type to an existentially-quantified singleton type.
    toSing   :: DemoteRep kparam -> SomeSing kparam
  
  withSomeSing :: SingKind ('KProxy :: KProxy k)
               => DemoteRep ('KProxy :: KProxy k)
               -> (forall (a :: k). Sing a -> r)
               -> r
  withSomeSing _ _ = error "urk"
  
  -----------------------------------
  
  data SubscriptionChannel = BookingsChannel
  type BookingsChannelSym0 = BookingsChannel
  data instance Sing (z_a5I7 :: SubscriptionChannel) where
     SBookingsChannel :: Sing BookingsChannel
  
  instance SingKind ('KProxy :: KProxy SubscriptionChannel) where
    type DemoteRep ('KProxy :: KProxy SubscriptionChannel) = SubscriptionChannel
    fromSing SBookingsChannel = BookingsChannel
    toSing BookingsChannel = SomeSing SBookingsChannel
  
  instance SingI BookingsChannel where
    sing = SBookingsChannel
  
  type family T (c :: SubscriptionChannel) :: Type
  type instance T 'BookingsChannel = Bool
  
  witnessC :: Sing channel -> Dict (Show (T channel), SingI channel)
  witnessC SBookingsChannel = Dict
  
  forAllSubscriptionChannels
    :: forall m r. (Applicative m)
    => (forall channel. (SingI channel, Show (T channel)) => Sing channel -> m r)
    -> m r
  forAllSubscriptionChannels f =
    withSomeSing BookingsChannel $ \(sChannel) ->
      case witnessC sChannel of
        Dict -> f sChannel
  