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

2 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
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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 :: *`.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13365
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler