[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          |   Milestone:                           
   Component:  Compiler        |     Version:  7.4.2                    
    Keywords:                  |          Os:  FreeBSD                  
Architecture:  x86_64 (amd64)  |     Failure:  GHC rejects valid program
  Difficulty:  Unknown         |    Testcase:                           
   Blockedby:                  |    Blocking:                           
     Related:                  |  
-------------------------------+--------------------------------------------
Changes (by simonpj):

  * difficulty:  => Unknown


Old description:

> 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.

New description:

 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#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler