Summary

This does work:

-- f :: [a -> Either a ()]
f = [Left @a :: forall a. a -> Either a ()]

This does not:

-- type F :: [a -> Either a ()]
type F = '[Left @a :: forall a. a -> Either a ()]

An unfortunate asymmetry between terms & types. See a related discussion at https://gitlab.haskell.org/ghc/ghc/wikis/ghc-kinds/kind-inference/tlks

Steps to reproduce

ghci> :set -XScopedTypeVariables -XDataKinds -XPolyKinds -XTypeApplications 
ghci> type F = '[Left @a :: forall a. a -> Either a ()]

<interactive>:3:18: error: Not in scope: type variable ‘a’

Expected behavior

No error.

Environment

• GHC version used: HEAD.