Re: [GHC] #8105: unhelpful error message PolyKinds + GADTs

31 Jul 2013

      #8105: unhelpful error message PolyKinds + GADTs
-------------------------------------------------+-------------------------
        Reporter:  wvv                           |            Owner:
            Type:  bug                           |           Status:
        Priority:  normal                        |  closed
       Component:  Compiler                      |        Milestone:
      Resolution:  invalid                       |          Version:  7.6.3
Operating System:  Unknown/Multiple              |         Keywords:
 Type of failure:  Incorrect warning at          |     Architecture:
  compile-time                                   |  Unknown/Multiple
       Test Case:                                |       Difficulty:
        Blocking:                                |  Unknown
                                                 |       Blocked By:
                                                 |  Related Tickets:
-------------------------------------------------+-------------------------
Changes (by goldfire):

 * status:  new => closed
 * resolution:   => invalid

Comment:

 I would say that GHC's behavior there is correct. The GADT-syntax
 equivalent of your first example is

 {{{
 data Foo (a::k) where
   Foo :: a -> Foo a
 }}}

 In GHC 7.6.3, I get this sensible error:

 {{{
     Kind mis-match
     The first argument of `Foo' should have kind `k1',
     but `a' has kind `*'
     In the type `Foo a'
     In the definition of data constructor `Foo'
     In the data declaration for `Foo'
 }}}

 The problem with your code is that GADT syntax requires just the name of
 the data constructor to the left of the `::`. Anything else there really
 is a parse error.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8105#comment:1
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler