Generic construction of Rec fields

{-# LANGUAGE
    DataKinds
  , ExistentialQuantification
  , PolyKinds
  , TypeFamilies
  , TypeOperators
  #-}

module Main where

import Data.Vinyl
import Data.Vinyl.TypeLevel
import Data.Singletons

data Fields = Name | Age | Sleeping | Master deriving Show
data instance Sing '(Fields, Name)     = SName
data instance Sing '(Fields, Age)      = SAge
data instance Sing '(Fields, Sleeping) = SSleeping
data instance Sing '(Fields, Master)   = SMaster

type LifeForm = [Name, Age, Sleeping]

class Field f where
   type ElF f (t :: k) :: *
   data Attr f (t :: k) :: *
   (=:) :: sing '(f,k) -> ElF f k -> Attr f k
   _unAttr :: Attr f k -> ElF f k

instance Field Fields where
   type ElF Fields Name     = String
   type ElF Fields Age      = Int
   type ElF Fields Sleeping = Bool
   type ElF Fields Master   = Rec (Attr Fields) LifeForm
   data Attr Fields k = Attr (ElF Fields k)
   _ =: x = Attr x
   _unAttr (Attr x) = x

--jon :: Rec (Attr Fields) LifeForm
jon = (SName =: "jon") :& (SAge =: 2) :& (SSleeping =: False) :& RNil

--tucker :: Rec (Attr Fields) (LifeForm ++ '[Master])
tucker = (SName =: "tucker") :& (SAge =: 9) :& (SSleeping =: True) :& (SMaster =: jon) :& RNil

data Other = Foo | Bar | Baz deriving Show
data instance Sing '(Other, Foo) = SFoo
data instance Sing '(Other, Bar) = SBar
data instance Sing '(Other, Baz) = SBaz

instance Field Other where
   type ElF Other Foo = Int
   type ElF Other Bar = Double
   type ElF Other Baz = String
   data Attr Other k = Attr' (ElF Other k)
   _ =: x = Attr' x
   _unAttr (Attr' x) = x

foo = (SFoo =: 2) :& (SBar =: 3.0) :& (SBaz =: "baz") :& RNil

main = putStrLn "hello,world"