title: Type-level Map with DataKinds
body: <p>I have a common pattern where I have a type-level list of kind <code>[*]</code>, and I would like to apply a type constructor of kind <code>* -&gt; *</code> to each element in the list. For example, I would like to change the type <code>'[Int, Double, Integer]</code> to <code>'[Maybe Int, Maybe Double, Maybe Integer]</code>.</p>
  
  <p>Here's my attempt to implement a type-level <code>map</code>.</p>
  
  <pre><code>{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, TypeOperators, DataKinds, ScopedTypeVariables, GADTs #-}
  
  -- turns a type list '[b1, b2, b3]
  -- into the type list '[a b1, a b2, a b3]
  class TypeMap (a :: * -&gt; *) (bs :: [*]) where
      type Map a bs :: [*]
  
  instance TypeMap a '[b] where
      type Map a '[b] = '[a b]
  
  instance TypeMap a (b1 ': b2 ': bs) where
      type Map a (b1 ': b2 ': bs) = ((a b1) ': (Map a (b2 ': bs)))
  
  
  data HList :: [*] -&gt; * where
                HNil :: HList '[]
                HCons :: a -&gt; HList as -&gt; HList (a ': as)
  
  class Foo as where
      toLists :: HList as -&gt; HList (Map [] as)
  
  instance Foo '[a] where
      toLists (HCons a HNil) = HCons [a] HNil
  
  instance (Foo (a2 ': as)) =&gt;  Foo (a1 ': a2 ': as) where
      toLists (HCons a as) = 
          let as' = case (toLists as) of
                      (HCons a2 as'') -&gt; HCons [head a2] as'' -- ERROR
          in HCons [a] as'
  </code></pre>
  
  <p>This results in the error </p>
  
  <pre><code>Could not deduce (a3 ~ [t0])
      from the context (Foo ((':) * a2 as))
        bound by the instance declaration at Test.hs:35:10-50
      or from ((':) * a1 ((':) * a2 as) ~ (':) * a as1)
        bound by a pattern with constructor
                   HCons :: forall a (as :: [*]).
                            a -&gt; HList as -&gt; HList ((':) * a as),
                 in an equation for `toLists'
        at Test.hs:36:14-23
      or from (Map [] as1 ~ (':) * a3 as2)
        bound by a pattern with constructor
                   HCons :: forall a (as :: [*]).
                            a -&gt; HList as -&gt; HList ((':) * a as),
                 in a case alternative
        at Test.hs:38:22-34
        `a3' is a rigid type variable bound by
             a pattern with constructor
               HCons :: forall a (as :: [*]).
                        a -&gt; HList as -&gt; HList ((':) * a as),
             in a case alternative
             at Test.hs:38:22
      Expected type: HList (Map [] ((':) * a2 as))
        Actual type: HList ((':) * [t0] as2)
      In the return type of a call of `HCons'
      In the expression: HCons [head a2] as''
      In a case alternative: (HCons a2 as'') -&gt; HCons [head a2] as''
  </code></pre>
  
  <p>I've tried adding copious type annotations, but the error more or less comes out the same: GHC can't even infer that the first element of the HList is a (normal) list. Am I doing something silly here? Something illegal? Or is there any way around? </p>