From ef26182e2014b0a2a029ae466a4b121bf235e4e4 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 3 Oct 2017 14:58:27 -0400 Subject: Track the order of user-written tyvars in DataCon MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 . (...) ``` 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 --- compiler/prelude/TysWiredIn.hs | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) (limited to 'compiler/prelude') diff --git a/compiler/prelude/TysWiredIn.hs b/compiler/prelude/TysWiredIn.hs index 01579830f8..2033fcff36 100644 --- a/compiler/prelude/TysWiredIn.hs +++ b/compiler/prelude/TysWiredIn.hs @@ -490,12 +490,15 @@ pcTyCon is_enum name cType tyvars cons False -- Not in GADT syntax pcDataCon :: Name -> [TyVar] -> [Type] -> TyCon -> DataCon -pcDataCon n univs = pcDataConWithFixity False n univs [] -- no ex_tvs +pcDataCon n univs = pcDataConWithFixity False n univs + [] -- no ex_tvs + univs -- the univs are precisely the user-written tyvars pcDataConWithFixity :: Bool -- ^ declared infix? -> Name -- ^ datacon name -> [TyVar] -- ^ univ tyvars -> [TyVar] -- ^ ex tyvars + -> [TyVar] -- ^ user-written tyvars -> [Type] -- ^ args -> TyCon -> DataCon @@ -509,19 +512,20 @@ pcDataConWithFixity infx n = pcDataConWithFixity' infx n (dataConWorkerUnique (n -- one DataCon unique per pair of Ints. pcDataConWithFixity' :: Bool -> Name -> Unique -> RuntimeRepInfo - -> [TyVar] -> [TyVar] + -> [TyVar] -> [TyVar] -> [TyVar] -> [Type] -> TyCon -> DataCon -- The Name should be in the DataName name space; it's the name -- of the DataCon itself. -pcDataConWithFixity' declared_infix dc_name wrk_key rri tyvars ex_tyvars arg_tys tycon +pcDataConWithFixity' declared_infix dc_name wrk_key rri + tyvars ex_tyvars user_tyvars arg_tys tycon = data_con where data_con = mkDataCon dc_name declared_infix prom_info (map (const no_bang) arg_tys) [] -- No labelled fields - (mkTyVarBinders Specified tyvars) - (mkTyVarBinders Specified ex_tyvars) + tyvars ex_tyvars + (mkTyVarBinders Specified user_tyvars) [] -- No equality spec [] -- No theta arg_tys (mkTyConApp tycon (mkTyVarTys tyvars)) @@ -552,7 +556,7 @@ mkDataConWorkerName data_con wrk_key = pcSpecialDataCon :: Name -> [Type] -> TyCon -> RuntimeRepInfo -> DataCon pcSpecialDataCon dc_name arg_tys tycon rri = pcDataConWithFixity' False dc_name (dataConWorkerUnique (nameUnique dc_name)) rri - [] [] arg_tys tycon + [] [] [] arg_tys tycon {- ************************************************************************ @@ -1418,7 +1422,8 @@ nilDataCon = pcDataCon nilDataConName alpha_tyvar [] listTyCon consDataCon :: DataCon consDataCon = pcDataConWithFixity True {- Declared infix -} consDataConName - alpha_tyvar [] [alphaTy, mkTyConApp listTyCon alpha_ty] listTyCon + alpha_tyvar [] alpha_tyvar + [alphaTy, mkTyConApp listTyCon alpha_ty] listTyCon -- Interesting: polymorphic recursion would help here. -- We can't use (mkListTy alphaTy) in the defn of consDataCon, else mkListTy -- gets the over-specific type (Type -> Type) -- cgit v1.2.1