[Haskell-cafe] convert structures from type to value level

[Zoran Bošnjak]

Dear haskell cafe,
I would like to describe some structures as types (something like 
servant does) and I would also need to use the same structure in 
run-time as a value. I am trying to figure out how could I use 
GHC.Generics or something to do this for several user defined 
structures.

Currently I am doing it manually (with does not work, but it might serve 
as intention), for example:

-- generic example structure
data GTest s n = GTest0 | GTest1 s | GTest2 n

type TTest = GTest Symbol Nat     -- type level
type VTest = GTest String Integer -- value level

For all my user defined structure, at the type level it will always be 
only (Symbol, Nat) which should translate to (Text, Int) or (String, 
Integer) for simplicity.

-- | Convert schema from type to value
class IsSchema t a where
     schema :: a

instance KnownNat n => IsSchema n Integer where
     schema = natVal (Proxy @n)

instance KnownSymbol s => IsSchema s String where
     schema = symbolVal (Proxy @s)

instance IsSchema 'GTest0 VTest where
     schema = GTest0

instance
     ( IsSchema s String
     ) => IsSchema ('GTest1 s) VTest where
     schema = GTest1 (schema @s)

instance
     ( IsSchema n Integer
     ) => IsSchema ('GTest2 n) VTest where
     schema = GTest2 (schema @n)

I would like to generalize the process, by saying something like (not 
sure if I even need this):

data Usage = TypeLevel | ValueLevel

data GTest ? = Gtest0 | GTest1 ? | GTest2 ? (deriving ?)

... and be able to use the same Test structure in both cases, such as:

Use it as a phantom type in some other type:

data Item (t :: TTest) where
     Item0 :: Item 'GTest0
     Item1 :: String -> Item ('GTest1 s)
     Item2 :: Integer -> Item ('GTest2 n)

And use it as value, something like:

data SomeItem = forall t a. IsSchema t a => SomeItem a (Item t)

In other words... I would like to work with exact types (Item t) or 
generically with SomeItem, when the type is not exactly known, but the 
value level schema is known.

I came far with manual approach, but I could not create SomeItem from 
the value schema. So, for example this does not compile (the error is 
about KnownSymbol/KnownNat):

mkSomeItem :: VTest -> SomeItem
mkSomeItem sch = case sch of
     GTest0 -> SomeItem sch Item0
     GTest1 s -> SomeItem sch (Item1 (s <> s))
     GTest2 n -> SomeItem sch (Item2 (succ n))

I am curious to know how to fix this problem. But the manual conversion 
approach is something I would like to avoid in the first place. 
Appreciate your help.

regards,
Zoran