[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:  RyanGlScott
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:  8.4.1
       Component:  Compiler          |              Version:  8.1
      Resolution:  fixed             |             Keywords:
                                     |  TypeApplications
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #13848, #12025    |  Differential Rev(s):  Phab:D3687
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by bgamari):

 * status:  patch => closed
 * resolution:   => fixed


Old description:

> 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.

New description:

 Consider

 {{{#!hs
 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

 {{{#!hs
 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#comment:13>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler