#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

#9882: Kind mismatch with singleton [Nat] -------------------------------------+------------------------------------- Reporter: Roel van | Owner: Dijk | Status: closed Type: bug | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: Resolution: invalid | Architecture: Unknown/Multiple Operating System: Linux | Difficulty: Unknown Type of failure: GHC | Blocked By: rejects valid program | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by Roel van Dijk): * status: new => closed * resolution: => invalid -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9882#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9882: Kind mismatch with singleton [Nat] -------------------------------------+------------------------------------- Reporter: Roel van | Owner: Dijk | Status: closed Type: bug | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: Resolution: invalid | Architecture: Unknown/Multiple Operating System: Linux | Difficulty: Unknown Type of failure: GHC | Blocked By: rejects valid program | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones ): In [changeset:"a3e6915431f93ebc0aaee22b7b9f118bffb01cae/ghc"]: {{{ #!CommitTicketReference repository="ghc" revision="a3e6915431f93ebc0aaee22b7b9f118bffb01cae" Wibbles to documentation for promoted lists and tuples (Trac #9882) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9882#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler