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

6 Mar 2017

      #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