[GHC] #9882: Kind mismatch with singleton [Nat]

[GHC]

#9882: Kind mismatch with singleton [Nat]
-------------------------------------+-------------------------------------
              Reporter:  Roel van    |            Owner:
  Dijk                               |           Status:  new
                  Type:  bug         |        Milestone:
              Priority:  normal      |          Version:  7.8.3
             Component:  Compiler    |         Keywords:
            Resolution:              |     Architecture:  Unknown/Multiple
      Operating System:  Linux       |       Difficulty:  Unknown
       Type of failure:  GHC         |       Blocked By:
  rejects valid program              |  Related Tickets:
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
Description changed by Roel van Dijk:

Old description:

> {{{#!hs
> {-# LANGUAGE DataKinds      #-}
> {-# LANGUAGE KindSignatures #-}
> {-# LANGUAGE TypeOperators  #-}
>
> import GHC.TypeLits ( Nat )
>
> data Foo (n :: [Nat]) = Foo
>
> x :: Foo ('(:) 42 '[])
> x = Foo
>
> y :: Foo (42 ': '[])
> y = Foo
>
> z :: Foo [42]
> z = Foo
> }}}
>
> {{{
> Expected kind ‘*’, but ‘42’ has kind ‘Nat’
> In the type signature for ‘z’: z :: Foo [42]
> }}}
>
> I would expected z to be identical to both x and y. The error occurs in
> both GHCi and GHC.

New description:

 {{{#!hs
 {-# LANGUAGE DataKinds      #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE TypeOperators  #-}

 import GHC.TypeLits ( Nat )

 data Foo (n :: [Nat]) = Foo

 x :: Foo ('(:) 42 '[])
 x = Foo

 y :: Foo (42 ': '[])
 y = Foo

 z :: Foo [42]
 z = Foo
 }}}

 {{{
 Expected kind ‘*’, but ‘42’ has kind ‘Nat’
 In the type signature for ‘z’: z :: Foo [42]
 }}}

 I would expected z to be identical to both x and y. The error occurs in
 both GHCi and GHC.

 Some more tests:
 {{{#!hs
 a_works = Foo '[]
 a_fails = Foo []
 z_works = Foo '[42]
 }}}

--

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9882#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler