title: How to compile heterogeneous hash map like object using type level keys in Haskell?
body: <p>I want to use something like "heterogeneous hash map using type level keys".
  After struggling, I wrote a code bellow (though in fact, it is just a list like structure rather than hash map), but it does not be successfully complied.</p>
  
  <p>The error message is as follows.</p>
  
  <pre><code>• Couldn't match expected type ‘ValueType
                                    (Proxy k') (NamedVal v k :. b)’
                with actual type ‘ValueType (Proxy k') b’
    NB: ‘ValueType’ is a type function, and may not be injective
  • In the expression: get (Proxy :: Proxy k') b
  </code></pre>
  
  <p>It seems type family declaration is not understood by compiler as I meant.
  How do I compile this code?</p>
  
  <pre><code>{-# LANGUAGE DataKinds #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeInType #-}
  {-# LANGUAGE InstanceSigs #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE IncoherentInstances #-}
  
  module TypeLevelKV where
  
  {- | The goal of this module is to get the value with a type level key.
  
  &gt;&gt;&gt; get (Proxy :: Proxy "foo") sampleList
  "str"
  
  &gt;&gt;&gt; get (Proxy :: Proxy "bar") sampleList
  34
  -}
  
  import Data.Proxy (Proxy(..))
  import Data.Typeable (Typeable)
  import GHC.TypeLits (KnownSymbol, symbolVal)
  
  sampleList =
    (namedVal "str"   :: NamedVal String "foo") :.
    (namedVal 34      :: NamedVal Int "bar") :.
    (namedVal True    :: NamedVal Bool "baz") :. Null
  
  {- | A value with type level index.
   -}
  type NamedVal v key = (Proxy key, v)
  
  {- | Type level list cons
   -}
  data a :. b = a :. b
      deriving (Typeable, Eq, Show)
  infixr 8 :.
  
  {- | Type level @[]@
   -}
  data Null = Null
      deriving (Typeable, Eq, Show)
  
  type family ValueType pkey list where
    ValueType (Proxy k) (NamedVal v k :. b) = v
    ValueType (Proxy k') (NamedVal v k :. b) = ValueType (Proxy k') b
    ValueType (Proxy k) Null = Null
  
  class HasKey pkey list where
    get :: pkey -&gt; list -&gt; (ValueType pkey list)
  
  instance (KnownSymbol k) =&gt;
    HasKey (Proxy k) (NamedVal v k :. b) where
    get _ ((_, a) :. _) = a
  
  instance (KnownSymbol k, KnownSymbol k', HasKey (Proxy k') b) =&gt;
    HasKey (Proxy k') (NamedVal v k :. b) where
    get _ (_ :. b) = get (Proxy :: Proxy k') b
  
  instance (KnownSymbol k) =&gt;
    HasKey (Proxy k) Null where
    get _ Null = Null
  
  namedVal :: forall k v
           . (KnownSymbol k)
           =&gt; v -&gt; NamedVal v k
  namedVal a = (Proxy, a)
  </code></pre>
  
  <h2>Followings are reply for the @Benjamin Hodgson 's comment</h2>
  
  <p>One of the reason I need this is that I want to use it with template haskell as follows and ensure that all the variables required by <code>sampleQ</code> is same type as needed.</p>
  
  <pre><code>withDict :: [String] -&gt; Q Exp -&gt; Q Exp
  withDict keys q = undefined
  -- e.g., `withDict (Proxy :: Proxy MyType) sampleQ` generates
  -- \(dict :: MyType) -&gt;
  --   let
  --     foo = get (Proxy :: Proxy "foo") dict
  --     bar = get (Proxy :: Proxy "bar") dict
  --     baz = get (Proxy :: Proxy "baz") dict
  --     defaultValue = "If no \"defaultValue\" key exists, this default value is provided to sampleQ"
  --   in
  --     $(sampleQ)
  
  type MyType =
    NamedVal String "foo" :.
    NamedVal Int "bar" :.
    NamedVal Bool "baz" :. Null
  </code></pre>
  
  <p>After defining this, we can inject any values with variable name into a <code>Q Exp</code> such as Shakespearen template.</p>
  
  <pre><code>renderWith :: IO ()
  renderWith = do
    foo &lt;- getLine
    bar &lt;- readLn
    baz &lt;- readLn
    let
      sampleList :: MyType
      sampleList =
        (namedVal foo   :: NamedVal String "foo") :.
        (namedVal bar   :: NamedVal Int "bar") :.
        (namedVal baz   :: NamedVal Bool "baz") :. Null
    putStrLn $ $(withDict (Proxy :: Proxy MyType) renderSomeFile) sampleList
  </code></pre>