{-# LANGUAGE GADTs, KindSignatures, PolyKinds, TypeFamilies, RankNTypes #-}
module Singlethongs.Internal
 ( Sing
 , SingI(sing)
 , SomeSing(SomeSing)
 , withSomeSing
 , SingKind(Demote, fromSing, toSing)
 ) where

data family Sing (a :: k)

class SingI (a :: k) where
  sing :: Sing a

data SomeSing k where
  SomeSing :: Sing (a :: k) -> SomeSing k

withSomeSing :: SingKind k => Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing :: Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing x :: Demote k
x f :: forall (a :: k). Sing a -> r
f = case Demote k -> SomeSing k
forall k. SingKind k => Demote k -> SomeSing k
toSing Demote k
x of SomeSing x' :: Sing a
x' -> Sing a -> r
forall (a :: k). Sing a -> r
f Sing a
x'
{-# INLINE withSomeSing #-}

class SingKind k where
  type Demote k :: *
  fromSing :: Sing (a :: k) -> Demote k
  toSing :: Demote k -> SomeSing k