[GHC] #11721: GADT-syntax data constructors don't work well with TypeApplications

[GHC]

#11721: GADT-syntax data constructors don't work well with TypeApplications
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:  goldfire
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.2.1
          Component:  Compiler       |           Version:  8.1
           Keywords:                 |  Operating System:  Unknown/Multiple
  TypeApplications                   |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Consider

 {{{
 data X a where
   MkX :: b -> Proxy a -> X a
 }}}

 According to the rules around specified vs. generalized variables around
 `TypeApplications`, the type of `MkX` should be

 {{{
 MkX :: forall {k} (b :: *) (a :: k). b -> Proxy a -> X a
 }}}

 A few things to note:
  * The `k` isn't available for `TypeApplications` (that's why it's in
 braces), because it is not user-written.
  * The `b` is quantified before the `a`, because `b` comes before `a` in
 the user-written type signature for `MkX`.

 Both of these bullets are currently violated. GHCi reports `MkX`'s type as

 {{{
 MkX :: forall k (a :: k) b. b -> Proxy a -> X a
 }}}

 It turns out that this is a hard to fix. The problem is that GHC expects
 data constructors to have their universal variables followed by their
 existential variables, always. And yet that's violated in the desired type
 for `MkX`. Furthermore, given the way that GHC deals with GADT return
 types ("rejigging", in technical parlance), it's inconvenient to get the
 specified/generalized distinction correct.

 Given time constraints, I'm afraid fixing this all won't make it for 8.0.

 Happily, there is are easy-to-articulate rules governing GHC's current
 (wrong) behavior. In a GADT-syntax data constructor:
  * All kind and type variables are considered specified and available for
 visible type application.
  * Universal variables always come first, in precisely the order they
 appear in the tycon. Note that universals that are constrained by a GADT
 return type are missing from the datacon.
  * Existential variables come next. Their order is determined by a user-
 written `forall`; or, if there is none, by taking the left-to-right order
 in the datacon's type and doing a stable topological sort. (This stable
 topological sort step is the same as for other user-written type
 signatures.)

 Despite the existence of these rules, it would still be better not to have
 special rules for GADT-syntax data constructors. This ticket is intended
 to capture that eventual goal.

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