Promote/Error.hs:0:0: Splicing declarations
    promote
      [d| head :: [a] -> a
          head (a : _) = a
          head [] = error "Data.Singletons.List.head: empty list" |]
  ======>
    Promote/Error.hs:(0,0)-(0,0)
    head :: forall a. [a] -> a
    head (a GHC.Types.: _) = a
    head GHC.Types.[] = error "Data.Singletons.List.head: empty list"
    type family Head (a :: [a]) :: a
    type instance Head (GHC.Types.: a z) = a
    type instance Head GHC.Types.[] =
        Apply ErrorSym0 "Data.Singletons.List.head: empty list"
    data HeadSym0 (k :: TyFun [a] a)
    type instance Apply HeadSym0 a = Head a