Singledongs.hs

{- To be clear, I mean exporting this: -}

data family Sing (a :: k)

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

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

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




{- And some TH that given an enum type like Foo: -}

data Foo = Bar | Qux




{- Will generate this: -}
  
data instance Sing (a :: Foo) where
  SBar :: Sing 'Bar
  SQux :: Sing 'Qux

instance SingKind Foo where
  type Demote Foo = Foo
  fromSing = \case
    SBar -> Bar
    SQux -> Qux
  toSing = \case
    Bar -> SomeSing SBar
    Qux -> SomeSing SQux

instance SingI 'Bar where sing = SBar
instance SingI 'Qux where sing = SQux

instance TestEquality (Sing :: Foo -> *) where
  testEquality SBar SBar = Just Refl
  testEquality SQux SQux = Just Refl
  testEquality _ _ = Nothing



{- Personally, I need this to compile with GHCJS, which at 
   the moment mostly means using GHC 8.6 features -}