Printing field names with the new-vinyl branch of Vinyl

gistfile1.hs

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators  #-}
{-# LANGUAGE GADTs  #-}
{-# LANGUAGE ConstraintKinds  #-}
{-# LANGUAGE LambdaCase  #-}
{-# LANGUAGE TemplateHaskell  #-}
{-# LANGUAGE FlexibleInstances  #-}
{-# LANGUAGE StandaloneDeriving  #-}
module VinylTest where
import Data.Singletons
import Data.Singletons.TH
import Data.Typeable
import Data.Vinyl
import Data.Vinyl.TypeLevel
import Data.Vinyl.Functor
import qualified Data.Constraint as D
import GHC.Exts

data DictP c (u :: k) where
  DictP :: c u => Proxy u -> DictP c u

data Product :: (k -> *) -> (k -> *) -> k -> * where
  Pair :: f a -> g a -> Product f g a

type family AllU (c :: u -> Constraint) (xs :: [u]) :: Constraint where
  AllU c '[] =  ()
  AllU c (r ':  rs) = (c r, AllU c rs)

asProxyOf :: f x -> Proxy x
asProxyOf _ = Proxy

reifyUConstraint 
  :: AllU c rs 
  => proxy c
  -> Rec f rs
  -> Rec (DictP c) rs
reifyUConstraint prx rs = case rs of
    RNil -> RNil
    (x :& xs) -> DictP (asProxyOf x) :& reifyUConstraint prx xs

-- The first exercise is I need to go from a Rec 
toFields :: AllU SingI xs => Rec f xs -> Rec Sing xs
toFields xs 
  = rmap (\(DictP p) -> singByProxy p) 
  $ reifyUConstraint (Proxy :: Proxy SingI) xs

class ToName (a :: *) where
  toName :: a -> String

toAllNames :: RecAll Sing xs ToName => Rec Sing xs -> Rec (Const String) xs
toAllNames xs = rmap (\(Compose (Dict x)) -> Const $ toName x) 
              $ reifyConstraint (Proxy :: Proxy ToName) xs

showNames :: (RecAll Sing xs ToName, AllU SingI xs) 
            => Rec f xs -> Rec (Const String) xs
showNames xs = toAllNames $ toFields xs

-- Test
singletons [d| data Fields = A | B | C |]

instance ToName (Sing A) where toName _ = "a"
instance ToName (Sing B) where toName _ = "b"
instance ToName (Sing C) where toName _ = "c"

-- Dummy eval
data Eval :: k -> * where
  E :: Eval a
  
deriving instance Show (Eval a)

test :: Rec Eval [A, B, C]
test = E :& E :& E :& RNil

-- prints: ["a","b","c"]
test2 :: [String]
test2 = recordToList $ showNames test