#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 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Yes, we could. Then the wrapper implementation would just match up the tyvars. I don't think it would be that hard. But I've grown increasingly worried about my ability to graduate before my new job starts, and I've just had to draw the line somewhere. I am currently validating my last round of patches and hope very much to focus primarily on my dissertation immediately thereafter. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11721#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg ): In [changeset:"35e937973f61a7e5534ecd0b1c67111cd82d4238/ghc" 35e93797/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="35e937973f61a7e5534ecd0b1c67111cd82d4238" Track specified/invisible more carefully. In particular, this allows correct tracking of specified/invisible for variables in Haskell98 data constructors and in pattern synonyms. GADT-syntax constructors are harder, and are left until #11721. This was all inspired by Simon's comments to my fix for #11512, which this subsumes. Test case: ghci/scripts/TypeAppData [skip ci] (The test case fails because of an unrelated problem fixed in the next commit.) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11721#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11721: GADT-syntax data constructors don't work well with TypeApplications -------------------------------------+------------------------------------- Reporter: goldfire | Owner: RyanGlScott Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13848 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * owner: goldfire => RyanGlScott Comment: I'm working on this at the moment. A very rough attempt at this is located at Phab:D3687, but it's nowhere near ready to be merged (the changes I've introduced bring out many inscrutable Core Lint errors, which I'll need to puzzle over). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11721#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11721: GADT-syntax data constructors don't work well with TypeApplications -------------------------------------+------------------------------------- Reporter: goldfire | Owner: RyanGlScott Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13848 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * cc: Iceland_jack (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11721#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11721: GADT-syntax data constructors don't work well with TypeApplications -------------------------------------+------------------------------------- Reporter: goldfire | Owner: RyanGlScott Type: bug | Status: patch Priority: normal | Milestone: 8.4.1 Component: Compiler | Version: 8.1 Resolution: | 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 RyanGlScott): * status: new => patch * differential: => Phab:D3687 Comment: Phab:D3687 is now ready for review. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11721#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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

#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: | Phab:D4070 -------------------------------------+------------------------------------- Comment (by Ryan Scott ): In [changeset:"341d3a7896385f14580d048ea7681232e5b242ce/ghc" 341d3a78/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="341d3a7896385f14580d048ea7681232e5b242ce" Incorporate changes from #11721 into Template Haskell Summary: #11721 changed the order of type variables in GADT constructor type signatures, but these changes weren't reflected in Template Haskell reification of GADTs. Let's do that. Along the way, I: * noticed that the `T13885` test was claiming to test TH reification of GADTs, but the reified data type wasn't actually a GADT! Since this patch touches that part of the codebase, I decided to fix this. * incorporated some feedback from @simonpj in https://phabricator.haskell.org/D3687#113566. (These changes alone don't account for any different in behavior.) Test Plan: make test TEST=T11721_TH Reviewers: goldfire, austin, bgamari, simonpj Reviewed By: goldfire, bgamari, simonpj Subscribers: rwbarton, thomie, simonpj GHC Trac Issues: #11721 Differential Revision: https://phabricator.haskell.org/D4070 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11721#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | ghci/scripts/T11721, th/T11721_TH, | typecheck/should_compile/T13848 Blocked By: | Blocking: Related Tickets: #13848, #12025 | Differential Rev(s): Phab:D3687, Wiki Page: | Phab:D4070 -------------------------------------+------------------------------------- Comment (by dfeuer): Aha. Simon, this was the problem I mentioned on today's call. The documentation wasn't updated to reflect the fix until fairly recently, and I didn't notice. Sorry for the noise. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11721#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler