[GHC] #7420: mis-attributed kind in the explict type/kind signature

[GHC]

#7420: mis-attributed kind in the explict type/kind signature
--------------------------------------+-------------------------------------
Reporter:  guest                      |          Owner:                
    Type:  bug                        |         Status:  new           
Priority:  normal                     |      Component:  Compiler      
 Version:  7.4.2                      |       Keywords:                
      Os:  FreeBSD                    |   Architecture:  x86_64 (amd64)
 Failure:  GHC rejects valid program  |      Blockedby:                
Blocking:                             |        Related:                
--------------------------------------+-------------------------------------
 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.

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7420>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler