Sym1.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}

import Data.String (IsString, fromString)
import GHC.TypeLits (KnownSymbol, Symbol, someSymbolVal, symbolVal)


-- Singletons for built-in symbols.

data SingSymbol :: Symbol -> * where
  SS :: forall s. KnownSymbol s => SingSymbol s

unsingSymbol :: forall s. SingSymbol s -> String
unsingSymbol ss@SS = symbolVal ss

data SomeSingSymbol :: * where
  SSS :: forall s. SingSymbol s -> SomeSingSymbol
  
singSymbol :: String -> SomeSingSymbol
singSymbol s = SSS SS

{-

Sym1.hs:23:20: error:
    • No instance for (KnownSymbol s0) arising from a use of ‘SS’
    • In the first argument of ‘SSS’, namely ‘SS’
      In the expression: SSS SS
      In an equation for ‘singSymbol’: singSymbol s = SSS SS
Failed, modules loaded: none.

-}