Reflecting Heterogeneous Promoted Types back to Values, Compositionally

I've been playing with -XDataKinds recently, and would like to take a promoted structure build with type families and pull it back down to the value level. I believe this is possible because the compositional components are very simple, and the terminal expressions are just as straight forward.

Background

I would like to demote / reflect simple rose trees of Strings, which become types of kind Tree Symbol (when using GHC.TypeLits.Symbol as a type-level string). Here is my boilerplate code:

{-# LANGUAGE DataKinds #-}

import GHC.TypeLits
import Data.Proxy

data Tree a = Node a [Tree a]

type TestInput = '[ 'Node "foo" '[ 'Node "bar" '[]
                                 , 'Node "baz" '[]
                                 ]
                  , 'Node "bar" '[]
                  ]

It's a simple type-level rose forest that looks like this very detailed diagram:

 *-- "foo" -- "bar"
 |         \_ "baz"
  \_ "bar"

Attempted Solution

Ideally, I would like to traverse this structure and give a 1-to-1 mapping back to values of kind *, but it's not very obvious how to do this heterogeneously while still carrying-over the (necessary) instances due to overloading.

vanila on #haskell suggested I use type classes to bind the two worlds, but it seems a bit trickier than I thought. My first attempt tried to encode the contents of a type-level pattern match via an instance head constraint, but my associated type (to encode the *-kinded type result of the mapping) overlapped - apparently instance heads are somewhat ignored by GHC.

Ideally, I would also like the reflection of lists and trees to be generic, which seems to be causing problems - it's like using type classes to organize the type/kind strata.

Here is a non-functional example of what I would like:

class Reflect (a :: k) where
  type Result :: *
  reflect :: Proxy a -> Result

class ReflectEmpty (empty :: [k]) where
  reflectEmpty :: forall q. Proxy empty -> [q]
  reflectEmpty _ = []

instance ReflectEmpty '[] where

instance ReflectEmpty a => Reflect a where
  type Result = forall q. [q]
  reflect = reflectEmpty

-- | The superclass constraint is where we get compositional
class Reflect (x :: k) => ReflectCons (cons :: [x]) where
  reflectCons :: PostReflection x ~ c => Proxy cons -> [c]

instance ( Reflect x
         , ReflectCons xs ) => ReflectCons (x ': xs) where
  reflectCons _ = reflect (Proxy :: Proxy x) :
    reflectCons (Proxy :: Proxy xs)

instance ( Reflect x
         , ReflectEmpty e ) => ReflectCons (x ': e) where
  reflectCons _ = reflect (Proxy :: Proxy x) :
    reflectEmpty (Proxy :: Proxy e)

...

There are a couple of thing generally wrong about this code. Here is what I see: - I need some form of look-ahead to know the result of a higher-kinded reflection for generic type-level list reflection - PostReflection type function - I'm needing to create and destroy Proxy's on the fly. I'm not sure if this won't compile currently, but I don't feel confident that the types will unify as I expect them to.

But, this typeclass heirarchy feels like the only way to capture a heterogeneous grammar, so this may still be a start. Any help with this would be tremendous!