Re: Data kind syntax

Hi Simon, I'm free to talk now, do you mind doing a google hangout instead? I'm having trouble getting skype installed on linux. Thanks! --trevor On Fri 13 Sep 2013 08:22:18 AM PDT, Simon Peyton-Jones wrote:

Trevor

Thanks for working on the data-kind stuff. I've had a terribly crammed week, so I have only just looked at it properly.

The first thing I look for is a wiki page articulating the design you have chosen. I think it's this: http://ghc.haskell.org/trac/ghc/wiki/GhcKinds/KindsWithoutData Is that it? By which I mean, are there really *zero* wrinkles, dark corners?

Second, I'm not so happy about introducing a whole new constructor, KindDecl, in TyClDecl; plus associated clobber like a new data type TyConDecl. That brings lots of new code to treat those new declarations.

All that new code makes sense for things that differ radically -- for example a class declaration is very different to a data type declaration. BUT this 'data kind' stuff is really very very similar to an ordinary data type declaration! You just treat a very restricted form.

Moreover, it won't be long before Stephanie and Richard are seeking GADTs at the kind level, and then you'll have to expand it, duplicating yet more code.

One way to recover the commonality would be to really treat it as a data type declaration, but to restrict what is actually brought into scope (just as 'data type' will do). But then what about the use of '*' in data kind? data kind T = A * | B T T Well, that's really just a parsing issue! The parser can parse it as a kind, so that it understands the star correctly. But having parsed it, we can treat it largely like an ordinary data type declaration, can't we?

What do you think? Want to Skype? Sadly I'm out Mon/Tues.

Simon

| -----Original Message----- | From: ghc-commits [mailto:ghc-commits-bounces@haskell.org] On Behalf Of | git@git.haskell.org | Sent: 09 September 2013 04:54 | To: ghc-commits@haskell.org | Subject: [commit: ghc] data-kind-syntax: Fix how we're using roles with | `data kind` declarations (13d4096) | | Repository : ssh://git@git.haskell.org/ghc | | On branch : data-kind-syntax | Link : | http://ghc.haskell.org/trac/ghc/changeset/13d4096e0668e9f80a8601122affc6 | 4f8be295de/ghc | | >--------------------------------------------------------------- | | commit 13d4096e0668e9f80a8601122affc64f8be295de | Author: Trevor Elliott | Date: Sun Sep 8 17:46:48 2013 -0700 | | Fix how we're using roles with `data kind` declarations | | | >--------------------------------------------------------------- | | 13d4096e0668e9f80a8601122affc64f8be295de | compiler/iface/IfaceSyn.lhs | 11 +++++++---- | compiler/iface/MkIface.lhs | 3 ++- | compiler/iface/TcIface.lhs | 5 +++-- | compiler/typecheck/TcTyClsDecls.lhs | 15 ++++++++------- | compiler/types/TyCon.lhs | 8 ++++---- | 5 files changed, 24 insertions(+), 18 deletions(-) | | diff --git a/compiler/iface/IfaceSyn.lhs b/compiler/iface/IfaceSyn.lhs | index b12906b..ca772ac 100644 | --- a/compiler/iface/IfaceSyn.lhs | +++ b/compiler/iface/IfaceSyn.lhs | @@ -436,19 +436,22 @@ instance Binary IfaceBang where | | data IfaceTyConDecl | = IfTyCon { | - ifTyConOcc :: OccName, -- constructor name | - ifTyConArgKs :: [IfaceKind] -- constructor argument kinds | + ifTyConOcc :: OccName, -- constructor name | + ifTyConArgKs :: [IfaceKind], -- constructor argument kinds | + ifTyConRoles :: [Role] -- constructor argument roles | } | | instance Binary IfaceTyConDecl where | - put_ bh (IfTyCon a1 a2) = do | + put_ bh (IfTyCon a1 a2 a3) = do | put_ bh (occNameFS a1) | put_ bh a2 | + put_ bh a3 | get bh = do | a1 <- get bh | a2 <- get bh | + a3 <- get bh | occ <- return $! mkOccNameFS tcName a1 | - return (IfTyCon occ a2) | + return (IfTyCon occ a2 a3) | | data IfaceClsInst | = IfaceClsInst { ifInstCls :: IfExtName, -- See | comments with | diff --git a/compiler/iface/MkIface.lhs b/compiler/iface/MkIface.lhs | index 6764c91..3fff2b8 100644 | --- a/compiler/iface/MkIface.lhs | +++ b/compiler/iface/MkIface.lhs | @@ -1566,7 +1566,8 @@ tyConToIfaceDecl env tycon | | ifaceTyConDecl ty_con | = IfTyCon { ifTyConOcc = getOccName (tyConName ty_con), | - ifTyConArgKs = map (tidyToIfaceType emptyTidyEnv) | args } | + ifTyConArgKs = map (tidyToIfaceType emptyTidyEnv) | args, | + ifTyConRoles = tyConRoles ty_con } | where | (args,_) = splitFunTys (tyConKind ty_con) | | diff --git a/compiler/iface/TcIface.lhs b/compiler/iface/TcIface.lhs | index d6b6a55..2d18a74 100644 | --- a/compiler/iface/TcIface.lhs | +++ b/compiler/iface/TcIface.lhs | @@ -668,11 +668,12 @@ tcIfaceDataCons tycon_name tycon _ if_cons | ; return (HsUnpack (Just co)) } | | tcIfaceTyConDecl :: Kind -> KCon -> IfaceTyConDecl -> IfL TyCon | -tcIfaceTyConDecl kind kcon IfTyCon { ifTyConOcc = occ_name, | ifTyConArgKs = args } | +tcIfaceTyConDecl kind kcon IfTyCon { ifTyConOcc = occ_name, | ifTyConArgKs = args, | + ifTyConRoles = roles } | = do name <- lookupIfaceTop occ_name | -- See the comment in tc_con_decl of tcIfaceDataCons for why | forkM | kinds <- forkM pp_name (mapM tcIfaceKind args) | - return (mkDataKindTyCon kcon name (mkFunTys kinds kind)) | + return (mkDataKindTyCon kcon name (mkFunTys kinds kind) roles) | where | pp_name = ptext (sLit "Type constructor") <+> ppr occ_name | | diff --git a/compiler/typecheck/TcTyClsDecls.lhs | b/compiler/typecheck/TcTyClsDecls.lhs | index 99a3584..d348e8b 100644 | --- a/compiler/typecheck/TcTyClsDecls.lhs | +++ b/compiler/typecheck/TcTyClsDecls.lhs | @@ -118,7 +118,7 @@ tcTyAndClassDecls boot_details tyclds_s | -- remaining groups are typecheck in the extended global | env | | tcTyClGroup :: ModDetails -> TyClGroup Name -> TcM TcGblEnv | -tcTyClGroup boot_details decls | +tcTyClGroup _boot_details decls | | all (isKindDecl . unLoc) decls | = do (kcons, _) <- fixM $ \ ~(_, conss) -> do | let rec_info = panic "tcTyClGroup" "rec_info" | @@ -820,13 +820,12 @@ mkKindCon _rec_info tycons KindDecl { tcdLName = | L _ kind_name | kind_name | sKind | kvars | - [] -- XXX roles here? | + (replicate (length kvars) Nominal) -- no interesting kind | equality | Nothing | [] | (DataKindTyCon tycons) | NoParentTyCon | - -- TODO, make the rec_info work | - NonRecursive --(rti_is_rec rec_info kind_name) | + NonRecursive -- XXX is this OK? | False | NotPromotable | where | @@ -838,8 +837,8 @@ mkKindCon _ _ _ = | panic "mkKindCon" "non 'data kind' declaration" | | tcKindDecl :: RecTyInfo -> TyClDecl Name -> TcM [TyCon] | -tcKindDecl rec_info KindDecl { tcdLName = L _ kind_name, tcdKVars = | lknames | - , tcdTypeCons = cons } | +tcKindDecl _rec_info KindDecl { tcdLName = L _ kind_name, tcdKVars = | lknames | + , tcdTypeCons = cons } | = do traceTc "tcKindDecl" (ppr kind_name) | | ~(ATyCon kcon) <- tcLookupGlobal kind_name | @@ -1394,7 +1393,9 @@ tcTyConDecl kvars kind TyConDecl { tycon_name = | name, tycon_details = details } | RecCon {} -> panic "tcTyConDecl" "unexpected record | constructor" | let (kcon,_) = splitTyConApp kind | con_kind = mkPiKinds kvars (mkFunTys ks kind) | - return (mkDataKindTyCon kcon (unLoc name) con_kind) | + roles = replicate (length kvars) Nominal | + ++ replicate (length ks) Representational | + return (mkDataKindTyCon kcon (unLoc name) con_kind roles) | | | \end{code} | diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs | index 8ccbcc9..9308713 100644 | --- a/compiler/types/TyCon.lhs | +++ b/compiler/types/TyCon.lhs | @@ -1087,13 +1087,13 @@ mkPromotedDataCon con name unique kind roles | | -- | Construct a type constructor for a type introduced by a 'data | kind' | -- declaration. | -mkDataKindTyCon :: TyCon -> Name -> Kind -> TyCon | -mkDataKindTyCon kc name kind | +mkDataKindTyCon :: TyCon -> Name -> Kind -> [Role] -> TyCon | +mkDataKindTyCon kc name kind roles | = PromotedDataCon { | tyConName = name, | tyConUnique = nameUnique name, | - tyConArity = 0, | - tc_roles = [], -- XXX is this correct? | + tyConArity = length roles, | + tc_roles = roles, | tc_kind = kind, | parentTyCon = kc | } | | | _______________________________________________ | ghc-commits mailing list | ghc-commits@haskell.org | http://www.haskell.org/mailman/listinfo/ghc-commits