{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE KindSignatures       #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeInType           #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Kind (Constraint, Type)

type Exp a = a -> Type

type family Eval (e :: Exp a) :: a

data MapList :: (a -> Exp b) -> [a] -> Exp b

type instance Eval (MapList f '[]) = '[]
type instance Eval (MapList f (a ': as)) =
    Eval (f a) ': Eval (MapList f as)

{- error:
[1 of 1] Compiling Main             ( tys3.hs, interpreted )

tys3.hs:19:5: error:
    • Occurs check: cannot construct the infinite kind: a0 ~ [a0]
    • In the type ‘Eval (f a) : Eval (MapList f as)’
      In the type instance declaration for ‘Eval’
   |
19 |     Eval (f a) ': Eval (MapList f as)
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

tys3.hs:19:19: error:
    • Occurs check: cannot construct the infinite kind: a0 ~ [a0]
    • In the second argument of ‘(:)’, namely ‘Eval (MapList f as)’
      In the type ‘Eval (f a) : Eval (MapList f as)’
      In the type instance declaration for ‘Eval’
   |
19 |     Eval (f a) ': Eval (MapList f as)

-}