Type family inference

type-family-map.hs

{-# LANGUAGE GADTs, TypeFamilies, DataKinds, TypeOperators #-}

import Type.Reflection

type family Map f xs where
    Map f '[] = '[]
    Map f (x ': xs) = f x ': Map f xs
    
data HList xs where
    HNil :: HList '[]
    HCons :: a -> HList xs -> HList (a ': xs)
    
foo :: HList (Map TypeRep xs) -> HList xs
foo HNil = HNil

{-
main.hs:15:12: error:
    * Could not deduce: xs ~ '[]
      from the context: Map TypeRep xs ~ '[]
        bound by a pattern with constructor: HNil :: HList '[],
                 in an equation for `foo'
        at main.hs:15:5-8
      `xs' is a rigid type variable bound by
        the type signature for:
          foo :: forall (m :: * -> *) (xs :: [*]).
                 Monad m =>
                 HList (Map TypeRep xs) -> m (HList xs)
        at main.hs:14:1-56
      Expected type: m (HList xs)
        Actual type: m (HList '[])
    * In the expression: return HNil
      In an equation for `foo': foo HNil = return HNil
    * Relevant bindings include
        foo :: HList (Map TypeRep xs) -> m (HList xs)
          (bound at main.hs:15:1)
   |
15 | foo HNil = return HNil
   |            ^^^^^^^^^^^
-}