mis-attributed kind in the explict type/kind signature

The following simple code

{-# LANGUAGE DataKinds #-}[[BR]]
{-# LANGUAGE KindSignatures #-}[[BR]]
{-# LANGUAGE PolyKinds #-}[[BR]]
{-# LANGUAGE ScopedTypeVariables #-}[[BR]]

data Proxy tp 

hUpdateAtLabel :: forall l (n::Bool) v. v -> () -> ()

hUpdateAtLabel _ () = undefined (undefined::Proxy (n::Bool))

fails to type-check. The error message betrays a deep confusion in the kind checker:

/tmp/s3.hs:9:52:
    Kind mis-match
    An enclosing kind signature specified kind `Bool',
    but `n' has kind `l'
    In an expression type signature: Proxy (n :: Bool)
    In the first argument of `undefined', namely
      `(undefined :: Proxy (n :: Bool))'
    In the expression: undefined (undefined :: Proxy (n :: Bool))

If I write

hUpdateAtLabel :: forall (l :: *) (n::Bool) v. v -> () -> ()
hUpdateAtLabel _ () = undefined (undefined::Proxy (n::Bool))

the code type-checks. However,

hUpdateAtLabel :: forall l1 (l :: *) (n::Bool) v. v -> () -> ()
hUpdateAtLabel _ () = undefined (undefined::Proxy (n::Bool))

reports an error

    Kind mis-match
    An enclosing kind signature specified kind `Bool',
    but `n' has kind `*'

It looks like an off-by-one error, at least in the error message.