[GHC] #13365: Kind-inference for poly-kinded GADTs

[GHC]

#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