TypeApplications allows instantiation of implicitly-quantified kind variables

TypeApplications doesn't allow unticked list constructor even when it is unambiguous:

GHCi, version 8.0.1: http://www.haskell.org/ghc/  :? for help
> :set -XDataKinds
> :set -XTypeApplications
> :set -XScopedTypeVariables
> :set -XKindSignatures
> let foo :: forall (xs :: [Nat]). (); foo = ()
> foo @'[0]
()
> foo @[0]

<interactive>:17:6: error:
    * Expected kind `[Nat]', but `[0]' has kind `*'
    * In the type `[0]'
      In the expression: foo @[0]
      In an equation for `it': it = foo @[0]

<interactive>:17:7: error:
    * Expected a type, but `0' has kind `Nat'
    * In the type `[0]'
      In the expression: foo @[0]
      In an equation for `it': it = foo @[0]

why [0] has kind * here?

However this is legal:

> let foo :: forall (x :: Bool). (); foo = ()
> foo @True
()
> foo @'True
()

and this is wierd:

> :set -XPolyKinds
> let foo :: forall (x :: k). (); foo = ()
> foo @'True

<interactive>:12:6: error:
    * Expected a type, but 'True has kind `Bool'
    * In the type `True'
      In the expression: foo @True
      In an equation for `it': it = foo @True
> foo @True

<interactive>:13:6: error:
    * Expected a type, but 'True has kind `Bool'
    * In the type `True'
      In the expression: foo @True
      In an equation for `it': it = foo @True

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture