#13365: Kind-inference for poly-kinded GADTs -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: goldfire (added) Comment: I think there are actually two problems here: 1. The fact that this doesn't typecheck. I //think// this is a known limitation of type inference having to do with the fact that you didn't give a **c**omplete, **u**ser-specified **k**ind **s**ignature (CUSK) for `C`. For reference, if you had typed this: {{{#!hs {-# LANGUAGE PolyKinds, GADTs #-} import GHC.TypeLits data C (x :: k) (a :: k2) where C1 :: (KnownNat x) => a -> C x a C2 :: a -> C Int a }}} Then it works. I'll cc goldfire, out preeminent expert on CUSKs, to be sure. 2. The error message is quite awful. The issue is with `a`, not `x`, so I don't know why GHC is complaining about `x`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13365#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13365: Kind-inference for poly-kinded GADTs -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by crockeea: Old description:

With `-XPolyKinds`, GADTs require kind signatures where they should be inferred. Moreover, the error when these kind sigs are omitted is baffling.

{{{ {-# LANGUAGE PolyKinds, GADTs #-}

import GHC.TypeLits

data C (x :: k) a where C1 :: (KnownNat x) => a -> Foo x a C2 :: a -> Foo Int a }}}

{{{ error: • Expected kind ‘k’, but ‘x1’ has kind ‘Nat’ • In the first argument of ‘Foo’, namely ‘x’ In the type ‘Foo x a’ In the definition of data constructor ‘C1’ }}}

From this error, I would never expect that putting a kind signature on `a` would help here. But a signature shouldn't be required at all: it's clear from the GADT constructors that `a :: *`.

New description: With `-XPolyKinds`, GADTs require kind signatures where they should be inferred. Moreover, the error when these kind sigs are omitted is baffling. {{{ {-# LANGUAGE PolyKinds, GADTs #-} import GHC.TypeLits data Foo (x :: k) a where C1 :: (KnownNat x) => a -> Foo x a C2 :: a -> Foo Int a }}} {{{ error: • Expected kind ‘k’, but ‘x1’ has kind ‘Nat’ • In the first argument of ‘Foo’, namely ‘x’ In the type ‘Foo x a’ In the definition of data constructor ‘C1’ }}} From this error, I would never expect that putting a kind signature on `a` would help here. But a signature shouldn't be required at all: it's clear from the GADT constructors that `a :: *`. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13365#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13365: Kind-inference for poly-kinded GADTs -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType, | CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * keywords: TypeInType => TypeInType, CUSKs -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13365#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13365: Kind-inference for poly-kinded GADTs -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType, | CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14139 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): See also #14139 for another example. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13365#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13365: Notify user when adding a CUSK might help fix a type error -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType, | CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14139, #14207 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13365#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler