title: How can I generate term-level lists from a type-level ones?
body: <p>I'm trying to generate term-level values out of type-level ones. I have the following code</p>
  <pre class="lang-hs prettyprint-override"><code>class Term a where
    type family Result a :: Type
    term :: Result a
  
  instance (KnownSymbol s) =&gt; Term s where
    type instance Result s = String
    term = symbolVal (Proxy @s)
  
  instance (KnownNat n) =&gt; Term n where
    type instance Result n = Integer
    term = natVal (Proxy @n)
  </code></pre>
  <p>This works just fine:</p>
  <pre class="lang-hs prettyprint-override"><code>&gt;&gt;&gt; :t term @&quot;hello&quot;
  term @&quot;hello&quot; :: String
  &gt;&gt;&gt; term @&quot;hello&quot;
  &quot;hello&quot;
  </code></pre>
  <p>How can I propagate this idea on type-level lists? When I try something like this</p>
  <pre class="lang-hs prettyprint-override"><code>instance Term '[] where
    type instance Result ('[] :: [a]) = [a]
    term = []
  
  instance (Term a, Term as) =&gt; Term (a ': as) where
    type instance Result (a ': as) = Result a ': Result as
    term = term @a : term @as
  </code></pre>
  <p>GHC says that RHS of <code>Result (a ': as)</code> has kind [*], but a <code>type</code> was expected.</p>
  <pre class="lang-sh prettyprint-override"><code>• Expected a type, but ‘Result a : Result as’ has kind ‘[*]’
      • In the type ‘Result a : Result as’
        In the type instance declaration for ‘Result’
        In the instance declaration for ‘Term (a : as)’
  </code></pre>
  <p>I've got only one solution that compiles, but it expectedly evaluates only the first element:</p>
  <pre class="lang-hs prettyprint-override"><code>instance (Term a, Term as) =&gt; Term (a ': as) where
    type instance Result (a ': as) = [Result a]
    term = [term @a]
  </code></pre>
  <pre class="lang-hs prettyprint-override"><code>&gt;&gt;&gt; term @'[&quot;hello&quot;, &quot;world&quot;]
  [&quot;hello&quot;]
  </code></pre>
  <p>Is it possible to recursively transform type-level lists to terms?</p>
  <p>Full code:</p>
  <pre class="lang-hs prettyprint-override"><code>{-# LANGUAGE TypeApplications    #-}
  {-# LANGUAGE TypeFamilies        #-} 
  {-# LANGUAGE TypeOperators       #-} 
  {-# LANGUAGE PolyKinds           #-}
  {-# LANGUAGE AllowAmbiguousTypes #-}
  {-# LANGUAGE FlexibleInstances   #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  
  module Term where
  
  import           Data.Kind
  import           Data.Proxy
  import           GHC.TypeLits
  
  class Term a where
    type family Result a :: Type
    term :: Result a
  
  instance (KnownSymbol s) =&gt; Term s where
    type instance Result s = String
    term = symbolVal (Proxy @s)
  
  instance (KnownNat n) =&gt; Term n where
    type instance Result n = Integer
    term = natVal (Proxy @n)
  
  instance Term '[] where
    type instance Result ('[] :: [a]) = [a]
    term = []
  
  instance (Term a, Term as) =&gt; Term (a ': as) where
    type instance Result (a ': as) = Result a ': Result as
    term = term @a : term @as
  </code></pre>