#13848: Unexpected order of variable quantification with GADT constructor -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | 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 RyanGlScott): Above, I implied that GHC was inferring the topological order for `a` and `n` in the type signature for `VCons` even with an explicit `forall`. I just realized there's more to it after reading `Note [mkGADTVars]`. [http://git.haskell.org/ghc.git/blob/5c93df90a96494229b60bbed0971a4b08c0326a6... The relevant excerpt]: {{{ Note [mkGADTVars] ~~~~~~~~~~~~~~~~~ Running example: data T (k1 :: *) (k2 :: *) (a :: k2) (b :: k2) where MkT :: T x1 * (Proxy (y :: x1), z) z We need the rejigged type to be MkT :: forall (x1 :: *) (k2 :: *) (a :: k2) (b :: k2). forall (y :: x1) (z :: *). (k2 ~ *, a ~ (Proxy x1 y, z), b ~ z) => T x1 k2 a b You might naively expect that z should become a universal tyvar, not an existential. (After all, x1 becomes a universal tyvar.) The problem is that the universal tyvars must have exactly the same kinds as the tyConTyVars. z has kind * while b has kind k2. So we need an existential tyvar and a heterogeneous equality constraint. }}} So what's //really// going on is that GHC is putting all of the universally quantified variables (`a`) before the existentially quantified ones (`n`). Still, I still think that GHC ought to adhere to what the user wrote if they bother to write an explicit `forall`, because otherwise you have to trace out the variable order that GHC happens to infer. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13848#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13848: Unexpected order of variable quantification with GADT constructor -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | 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): Hmm. Fortunately we already have just the hook we need. Every interesting data constructor (including every GADT data con) has a wrapper; it is built by `MkId.mkDataConRep`. Look at `wrapper_reqd` to see which data cons have wrappers. The wrapper mediates between the nice user view of the data constructor and the internal "representation data constructor" that GHC uses internally. So for example {{{ data T a where MkT :: forall p q. p -> q -> T (p,q) }}} The representation data con has this type {{{ MkT :: forall r. forall p q. (r ~ (p,q)) => p -> q -> T r }}} But the wrapper is defined like this {{{ $WMkT :: forall p q. p -> q -> T (p,q) $WMkT = /\p q. \(x::p) (y::q). MkT @(p,q) @p @q <(p,q)> x y }}} The `<(p,q)>` is a coercion argument (refl) witnessing `(p,q)~(p,q)` Now currently `dataConUserType` (which claims to show the user-written type of the data con) is thus (in `DataCon`): {{{ dataConUserType (MkData { dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs, dcEqSpec = eq_spec, dcOtherTheta = theta, dcOrigArgTys = arg_tys, dcOrigResTy = res_ty }) = mkForAllTys (filterEqSpec eq_spec univ_tvs) $ mkForAllTys ex_tvs $ mkFunTys theta $ mkFunTys arg_tys $ res_ty }}} This `filterEqSpec` business is fishy! But now we understand about wrappers, for data constructors that have wrappers we could insead use the type of the wrapper, thus: {{{ dataConUserTYpe (MkData { dcRep = rep , dcRepType = rep_ty } = case rep of DCR { dcr_wrap_id = wrap_id } -> idType wrap_id NoDataConRep -> rep_ty -- If there is no wrapper, the "rep-type" is the same -- as the "user type" }}} Whizzo. Now, to return to the ticket, * We should ensure that the wrapper type reflects exactly the type the user wrote including type variable order * That in turn may force to make a wrapper when we don't right now, just to swizzle round the type variables Make sense? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13848#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13848: Unexpected order of variable quantification with GADT constructor -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | 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): Well it would take a bit more plumbing, I agree. You'd need to take the `qtkvs` returned by `tcGadtSigType` in `TcTyClsDecls.tcConDecl` and pass it on to `buildDataCon`, which can in turn give them to `mkDataConRep` to use instead of calling `dataConUserType`. I'm not certain that's all, but I think so. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13848#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13848: Unexpected order of variable quantification with GADT constructor -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | 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): Yes you are right. So yes, we have to put more info in the `IfaceConDecl`. Putting in the wrapper type doesn't feel right -- duplicates too much. Better to put in the original tyvars. And in that case we may as well record them in the `DataCon` too, as you suggested earlier. Then we wouldn't need to pass them to `mkDataConRep` after all, because they'll be in the `DataCon`. One fiddly thing I'm not sure about: in the declaration of `IfaceConDecl` we see {{{ data IfaceConDecl = IfCon { ifConName :: IfaceTopBndr, -- Constructor name ifConWrapper :: Bool, -- True <=> has a wrapper ifConInfix :: Bool, -- True <=> declared infix -- The universal type variables are precisely those -- of the type constructor of this data constructor -- This is *easy* to guarantee when creating the IfCon -- but it's not so easy for the original TyCon/DataCon -- So this guarantee holds for IfaceConDecl, but *not* for DataCon }}} Reasoning is explained in `MkIface` where we convert a `DataCon` to a `ConDecl` {{{ -- Tidy the univ_tvs of the data constructor to be identical -- to the tyConTyVars of the type constructor. This means -- (a) we don't need to redundantly put them into the interface file -- (b) when pretty-printing an Iface data declaration in H98-style syntax, -- we know that the type variables will line up -- The latter (b) is important because we pretty-print type constructors -- by converting to IfaceSyn and pretty-printing that con_env1 = (fst tc_env1, mkVarEnv (zipEqual "ifaceConDecl" univ_tvs tc_tyvars)) -- A bit grimy, perhaps, but it's simple! }}} Meddling with `IfaceConDecl` is not a big deal... it's just a serialisation format, and changes are very localised. So feel free to suggest what to do. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13848#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13848: Unexpected order of variable quantification with GADT constructor -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: duplicate | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11721 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Ben Gamari ): 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/13848#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler