[GHC] #11721: GADT-syntax data constructors don't work well with TypeApplications
#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
#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 simonpj): Could we avoid having the special rules by embodying the type the user wrote in the ''wrapper'' for `MkX`? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11721#comment:1> 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 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 simonpj): That's fine. I just wanted to lay out a design alternative. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11721#comment:3> 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 <eir@…>): 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: goldfire 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): * cc: RyanGlScott (added) * related: => #13848 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11721#comment:6> 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: | -------------------------------------+------------------------------------- Comment (by simonpj): See discussion in #13848 (only closed because duplicate) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11721#comment:8> 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: 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, #12025 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * related: #13848 => #13848, #12025 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11721#comment:10> 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: 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: | -------------------------------------+------------------------------------- Comment (by Ben Gamari <ben@…>): In [changeset:"ef26182e2014b0a2a029ae466a4b121bf235e4e4/ghc" ef26182/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="ef26182e2014b0a2a029ae466a4b121bf235e4e4" Track the order of user-written tyvars in DataCon After typechecking a data constructor's type signature, its type variables are partitioned into two distinct groups: the universally quantified type variables and the existentially quantified type variables. Then, when prompted for the type of the data constructor, GHC gives this: ```lang=haskell MkT :: forall <univs> <exis>. (...) ``` For H98-style datatypes, this is a fine thing to do. But for GADTs, this can sometimes produce undesired results with respect to `TypeApplications`. For instance, consider this datatype: ```lang=haskell data T a where MkT :: forall b a. b -> T a ``` Here, the user clearly intended to have `b` be available for visible type application before `a`. That is, the user would expect `MkT @Int @Char` to be of type `Int -> T Char`, //not// `Char -> T Int`. But alas, up until now that was not how GHC operated—regardless of the order in which the user actually wrote the tyvars, GHC would give `MkT` the type: ```lang=haskell MkT :: forall a b. b -> T a ``` Since `a` is universal and `b` is existential. This makes predicting what order to use for `TypeApplications` quite annoying, as demonstrated in #11721 and #13848. This patch cures the problem by tracking more carefully the order in which a user writes type variables in data constructor type signatures, either explicitly (with a `forall`) or implicitly (without a `forall`, in which case the order is inferred). This is accomplished by adding a new field `dcUserTyVars` to `DataCon`, which is a subset of `dcUnivTyVars` and `dcExTyVars` that is permuted to the order in which the user wrote them. For more details, refer to `Note [DataCon user type variables]` in `DataCon.hs`. An interesting consequence of this design is that more data constructors require wrappers. This is because the workers always expect the first arguments to be the universal tyvars followed by the existential tyvars, so when the user writes the tyvars in a different order, a wrapper type is needed to swizzle the tyvars around to match the order that the worker expects. For more details, refer to `Note [Data con wrappers and GADT syntax]` in `MkId.hs`. Test Plan: ./validate Reviewers: austin, goldfire, bgamari, simonpj Reviewed By: goldfire, simonpj Subscribers: ezyang, goldfire, rwbarton, thomie GHC Trac Issues: #11721, #13848 Differential Revision: https://phabricator.haskell.org/D3687 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11721#comment:12> 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 -------------------------------------+------------------------------------- Changes (by RyanGlScott): * differential: Phab:D3687 => Phab:D3687, Phab:D4070 Comment: Phab:D4070 updates Template Haskell accordingly. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11721#comment:14> 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 <ryan.gl.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 -------------------------------------+------------------------------------- Changes (by RyanGlScott): * testcase: => ghci/scripts/T11721, th/T11721_TH, typecheck/should_compile/T13848 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11721#comment:16> 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
participants (1)
-
GHC