#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
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
