Hi Everyone,

I tried to come up with a solution, but it has plenty of drawbacks.

data Tag = Hdf5 | Cbf | Unchecked

data A :: Tag -> Type where
  Ca :: Symbol -> A Unchecked
  Ch :: A Hdf5
  Cb :: A Cbf

type family Typestring (a :: A Unchecked) :: Type
type instance Typestring (Ca "hdf5") = A Hdf5
type instance Typestring (Ca "cbf") = A Cbf

data SUnchecked a where
  Sh :: SUnchecked (Ca "hdf5")
  Sc :: SUnchecked (Ca "cbf")

This checkValue function is useless, because you need to pass A Unchecked, and constructor (Ca) takes Symbol rather than String,  and value of type SUnchecked a.
checkValue :: forall (a :: A Unchecked). A Unchecked ->  SUnchecked a -> Typestring a
checkValue  (Ca x) Sh = Ch
checkValue  (Ca x) Sc = Cb

When I tried to run the above code

*Main> :t checkValue (Ca (someSymbolVal "hdf5"))

<interactive>:1:17: error:
    • Couldn't match expected type ‘Symbol’
                  with actual type ‘GHC.TypeLits.SomeSymbol’
    • In the first argument of ‘Ca’, namely ‘(someSymbolVal "hdf5")’
      In the first argument of ‘checkValue’, namely
        ‘(Ca (someSymbolVal "hdf5"))’
      In the expression: checkValue (Ca (someSymbolVal "hdf5"))

 What I really want is something like this, but the problem is I can't do pattern matching on symbols, and if I change the data type to String from Symbol then it won't compile .

Could some one point me how to solve this problem? 

 checkValue :: forall (a :: A Unchecked). SUnchecked a => A Unchecked -> Typestring a
 checkValue (Ca "hdf5") = Ch
 checkValue (Ca "cbf") = Cb

Best regards,

Mukesh