diff options
| author | Vladislav Zavialov <vlad.z.4096@gmail.com> | 2022-12-01 21:14:25 +0300 |
|---|---|---|
| committer | Vladislav Zavialov <vlad.z.4096@gmail.com> | 2023-02-03 16:09:24 +0300 |
| commit | 21cfded1b061bb1ad02537de0c8e8681a5c63f43 (patch) | |
| tree | 3894826fa3843531dd358e7a1398dbfda501500d | |
| parent | 8feb93013cf6f093e025c9e9a3213ae1fa0f73a0 (diff) | |
| download | haskell-21cfded1b061bb1ad02537de0c8e8681a5c63f43.tar.gz | |
Invisible binders in type declarations (#22560)wip/int-index/decl-invis-binders
This patch implements @k-binders introduced in GHC Proposal #425
and guarded behind the TypeAbstractions extension:
type D :: forall k j. k -> j -> Type
data D @k @j a b = ...
^^ ^^
To represent the new syntax, we modify LHsQTyVars as follows:
- hsq_explicit :: [LHsTyVarBndr () pass]
+ hsq_explicit :: [LHsTyVarBndr (HsBndrVis pass) pass]
HsBndrVis is a new data type that records the distinction between
type variable binders written with and without the @ sign:
data HsBndrVis pass
= HsBndrRequired
| HsBndrInvisible (LHsToken "@" pass)
The rest of the patch updates GHC, template-haskell, and haddock
to handle the new syntax.
Parser:
The PsErrUnexpectedTypeAppInDecl error message is removed.
The syntax it used to reject is now permitted.
Renamer:
The @ sign does not affect the scope of a binder, so the changes to
the renamer are minimal. See rnLHsTyVarBndrVisFlag.
Type checker:
There are three code paths that were updated to deal with the newly
introduced invisible type variable binders:
1. checking SAKS: see kcCheckDeclHeader_sig, matchUpSigWithDecl
2. checking CUSK: see kcCheckDeclHeader_cusk
3. inference: see kcInferDeclHeader, rejectInvisibleBinders
Helper functions bindExplicitTKBndrs_Q_Skol and bindExplicitTKBndrs_Q_Tv
are generalized to work with HsBndrVis.
Updates the haddock submodule.
Metric Increase:
MultiLayerModulesTH_OneShot
Co-authored-by: Simon Peyton Jones <simon.peytonjones@gmail.com>
78 files changed, 1173 insertions, 420 deletions
diff --git a/compiler/GHC/Builtin/Names/TH.hs b/compiler/GHC/Builtin/Names/TH.hs index bea3b9715f..251b171970 100644 --- a/compiler/GHC/Builtin/Names/TH.hs +++ b/compiler/GHC/Builtin/Names/TH.hs @@ -109,8 +109,11 @@ templateHaskellNames = [ -- TyVarBndr plainTVName, kindedTVName, plainInvisTVName, kindedInvisTVName, + plainBndrTVName, kindedBndrTVName, -- Specificity specifiedSpecName, inferredSpecName, + -- Visibility + bndrReqName, bndrInvisName, -- Role nominalRName, representationalRName, phantomRName, inferRName, -- Kind @@ -156,7 +159,9 @@ templateHaskellNames = [ expQTyConName, fieldExpTyConName, predTyConName, stmtTyConName, decsTyConName, conTyConName, bangTypeTyConName, varBangTypeTyConName, typeQTyConName, expTyConName, decTyConName, - typeTyConName, tyVarBndrUnitTyConName, tyVarBndrSpecTyConName, clauseTyConName, + typeTyConName, + tyVarBndrUnitTyConName, tyVarBndrSpecTyConName, tyVarBndrVisTyConName, + clauseTyConName, patQTyConName, funDepTyConName, decsQTyConName, ruleBndrTyConName, tySynEqnTyConName, roleTyConName, codeTyConName, injAnnTyConName, kindTyConName, @@ -492,11 +497,20 @@ plainInvisTVName, kindedInvisTVName :: Name plainInvisTVName = libFun (fsLit "plainInvisTV") plainInvisTVIdKey kindedInvisTVName = libFun (fsLit "kindedInvisTV") kindedInvisTVIdKey +plainBndrTVName, kindedBndrTVName :: Name +plainBndrTVName = libFun (fsLit "plainBndrTV") plainBndrTVIdKey +kindedBndrTVName = libFun (fsLit "kindedBndrTV") kindedBndrTVIdKey + -- data Specificity = ... specifiedSpecName, inferredSpecName :: Name specifiedSpecName = libFun (fsLit "specifiedSpec") specifiedSpecKey inferredSpecName = libFun (fsLit "inferredSpec") inferredSpecKey +-- data BndrVis = ... +bndrReqName, bndrInvisName :: Name +bndrReqName = libFun (fsLit "bndrReq") bndrReqKey +bndrInvisName = libFun (fsLit "bndrInvis") bndrInvisKey + -- data Role = ... nominalRName, representationalRName, phantomRName, inferRName :: Name nominalRName = libFun (fsLit "nominalR") nominalRIdKey @@ -569,7 +583,7 @@ patQTyConName, expQTyConName, stmtTyConName, varBangTypeTyConName, typeQTyConName, decsQTyConName, ruleBndrTyConName, tySynEqnTyConName, roleTyConName, derivClauseTyConName, kindTyConName, - tyVarBndrUnitTyConName, tyVarBndrSpecTyConName, + tyVarBndrUnitTyConName, tyVarBndrSpecTyConName, tyVarBndrVisTyConName, derivStrategyTyConName :: Name -- These are only used for the types of top-level splices expQTyConName = libTc (fsLit "ExpQ") expQTyConKey @@ -589,6 +603,7 @@ derivClauseTyConName = thTc (fsLit "DerivClause") derivClauseTyConKey kindTyConName = thTc (fsLit "Kind") kindTyConKey tyVarBndrUnitTyConName = libTc (fsLit "TyVarBndrUnit") tyVarBndrUnitTyConKey tyVarBndrSpecTyConName = libTc (fsLit "TyVarBndrSpec") tyVarBndrSpecTyConKey +tyVarBndrVisTyConName = libTc (fsLit "TyVarBndrVis") tyVarBndrVisTyConKey derivStrategyTyConName = thTc (fsLit "DerivStrategy") derivStrategyTyConKey -- quasiquoting @@ -652,7 +667,7 @@ quoteClassKey = mkPreludeClassUnique 201 expTyConKey, matchTyConKey, clauseTyConKey, qTyConKey, expQTyConKey, patTyConKey, stmtTyConKey, conTyConKey, typeQTyConKey, typeTyConKey, - tyVarBndrUnitTyConKey, tyVarBndrSpecTyConKey, + tyVarBndrUnitTyConKey, tyVarBndrSpecTyConKey, tyVarBndrVisTyConKey, decTyConKey, bangTypeTyConKey, varBangTypeTyConKey, fieldExpTyConKey, fieldPatTyConKey, nameTyConKey, patQTyConKey, funDepTyConKey, predTyConKey, @@ -694,6 +709,7 @@ decsTyConKey = mkPreludeTyConUnique 236 tyVarBndrSpecTyConKey = mkPreludeTyConUnique 237 codeTyConKey = mkPreludeTyConUnique 238 modNameTyConKey = mkPreludeTyConUnique 239 +tyVarBndrVisTyConKey = mkPreludeTyConUnique 240 {- ********************************************************************* * * @@ -1022,6 +1038,10 @@ plainInvisTVIdKey, kindedInvisTVIdKey :: Unique plainInvisTVIdKey = mkPreludeMiscIdUnique 482 kindedInvisTVIdKey = mkPreludeMiscIdUnique 483 +plainBndrTVIdKey, kindedBndrTVIdKey :: Unique +plainBndrTVIdKey = mkPreludeMiscIdUnique 484 +kindedBndrTVIdKey = mkPreludeMiscIdUnique 485 + -- data Role = ... nominalRIdKey, representationalRIdKey, phantomRIdKey, inferRIdKey :: Unique nominalRIdKey = mkPreludeMiscIdUnique 416 @@ -1106,6 +1126,11 @@ specifiedSpecKey, inferredSpecKey :: Unique specifiedSpecKey = mkPreludeMiscIdUnique 498 inferredSpecKey = mkPreludeMiscIdUnique 499 +-- data BndrVis = ... +bndrReqKey, bndrInvisKey :: Unique +bndrReqKey = mkPreludeMiscIdUnique 800 -- TODO (int-index): make up some room in the 5** numberspace? +bndrInvisKey = mkPreludeMiscIdUnique 801 + {- ************************************************************************ * * diff --git a/compiler/GHC/Core/TyCon.hs b/compiler/GHC/Core/TyCon.hs index 0311ba32bd..b549fb7cb1 100644 --- a/compiler/GHC/Core/TyCon.hs +++ b/compiler/GHC/Core/TyCon.hs @@ -25,7 +25,8 @@ module GHC.Core.TyCon( mkRequiredTyConBinder, mkAnonTyConBinder, mkAnonTyConBinders, tyConBinderForAllTyFlag, tyConBndrVisForAllTyFlag, isNamedTyConBinder, - isVisibleTyConBinder, isInvisibleTyConBinder, isVisibleTcbVis, + isVisibleTyConBinder, isInvisibleTyConBinder, + isVisibleTcbVis, isInvisSpecTcbVis, -- ** Field labels tyConFieldLabels, lookupTyConFieldLabel, @@ -508,6 +509,10 @@ isVisibleTcbVis :: TyConBndrVis -> Bool isVisibleTcbVis (NamedTCB vis) = isVisibleForAllTyFlag vis isVisibleTcbVis AnonTCB = True +isInvisSpecTcbVis :: TyConBndrVis -> Bool +isInvisSpecTcbVis (NamedTCB Specified) = True +isInvisSpecTcbVis _ = False + isInvisibleTyConBinder :: VarBndr tv TyConBndrVis -> Bool -- Works for IfaceTyConBinder too isInvisibleTyConBinder tcb = not (isVisibleTyConBinder tcb) @@ -883,8 +888,8 @@ data TyConDetails = promDcInfo :: PromDataConInfo -- ^ See comments with 'PromDataConInfo' } - -- | These exist only during type-checking. See Note [How TcTyCons work] - -- in "GHC.Tc.TyCl" + -- | These exist only during type-checking. + -- See Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon] in "GHC.Tc.TyCl" | TcTyCon { -- NB: the tyConArity of a TcTyCon must match -- the number of Required (positional, user-specified) @@ -918,7 +923,7 @@ where * tyConArity = length required_tvs tcTyConScopedTyVars are used only for MonoTcTyCons, not PolyTcTyCons. -See Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon] in GHC.Tc.Utils.TcType. +See Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon] in GHC.Tc.TyCl Note [Representation-polymorphic TyCons] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1837,13 +1842,11 @@ mkSumTyCon name binders res_kind cons parent -- right-hand side. It lives only during the type-checking of a -- mutually-recursive group of tycons; it is then zonked to a proper -- TyCon in zonkTcTyCon. --- See also Note [Kind checking recursive type and class declarations] --- in "GHC.Tc.TyCl". +-- See Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon] in "GHC.Tc.TyCl" mkTcTyCon :: Name -> [TyConBinder] -> Kind -- ^ /result/ kind only -> [(Name,TcTyVar)] -- ^ Scoped type variables; - -- see Note [How TcTyCons work] in GHC.Tc.TyCl -> Bool -- ^ Is this TcTyCon generalised already? -> TyConFlavour -- ^ What sort of 'TyCon' this represents -> TyCon @@ -1988,7 +1991,7 @@ isInjectiveTyCon (TyCon { tyConDetails = details }) role go (TcTyCon {}) _ = True -- Reply True for TcTyCon to minimise knock on type errors - -- See Note [How TcTyCons work] item (1) in GHC.Tc.TyCl + -- See (W1) in Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon] in GHC.Tc.TyCl -- | 'isGenerativeTyCon' is true of 'TyCon's for which this property holds diff --git a/compiler/GHC/Hs/Instances.hs b/compiler/GHC/Hs/Instances.hs index 74d75fb7be..7ffd65c1c4 100644 --- a/compiler/GHC/Hs/Instances.hs +++ b/compiler/GHC/Hs/Instances.hs @@ -450,6 +450,11 @@ deriving instance (Data body) => Data (HsRecFields GhcTc body) -- --------------------------------------------------------------------- -- Data derivations from GHC.Hs.Type ---------------------------------- +-- deriving instance Data (HsBndrVis p) +deriving instance Data (HsBndrVis GhcPs) +deriving instance Data (HsBndrVis GhcRn) +deriving instance Data (HsBndrVis GhcTc) + -- deriving instance (DataIdLR p p) => Data (LHsQTyVars p) deriving instance Data (LHsQTyVars GhcPs) deriving instance Data (LHsQTyVars GhcRn) diff --git a/compiler/GHC/Hs/Type.hs b/compiler/GHC/Hs/Type.hs index 313b8e8fe2..33ed0a20e6 100644 --- a/compiler/GHC/Hs/Type.hs +++ b/compiler/GHC/Hs/Type.hs @@ -32,6 +32,7 @@ module GHC.Hs.Type ( HsType(..), HsCoreTy, LHsType, HsKind, LHsKind, HsForAllTelescope(..), EpAnnForallTy, HsTyVarBndr(..), LHsTyVarBndr, + HsBndrVis(..), isHsBndrInvisible, LHsQTyVars(..), HsOuterTyVarBndrs(..), HsOuterFamEqnTyVarBndrs, HsOuterSigTyVarBndrs, HsWildCardBndrs(..), @@ -80,7 +81,7 @@ module GHC.Hs.Type ( mkHsOpTy, mkHsAppTy, mkHsAppTys, mkHsAppKindTy, ignoreParens, hsSigWcType, hsPatSigType, hsTyKindSig, - setHsTyVarBndrFlag, hsTyVarBndrFlag, + setHsTyVarBndrFlag, hsTyVarBndrFlag, updateHsTyVarBndrFlag, -- Printing pprHsType, pprHsForAll, @@ -184,7 +185,7 @@ mkHsForAllInvisTele :: EpAnnForallTy mkHsForAllInvisTele an invis_bndrs = HsForAllInvis { hsf_xinvis = an, hsf_invis_bndrs = invis_bndrs } -mkHsQTvs :: [LHsTyVarBndr () GhcPs] -> LHsQTyVars GhcPs +mkHsQTvs :: [LHsTyVarBndr (HsBndrVis GhcPs) GhcPs] -> LHsQTyVars GhcPs mkHsQTvs tvs = HsQTvs { hsq_ext = noExtField, hsq_explicit = tvs } emptyLHsQTvs :: LHsQTyVars GhcRn @@ -285,6 +286,8 @@ type instance XXTyVarBndr (GhcPass _) = DataConCantHappen hsTyVarBndrFlag :: HsTyVarBndr flag (GhcPass pass) -> flag hsTyVarBndrFlag (UserTyVar _ fl _) = fl hsTyVarBndrFlag (KindedTyVar _ fl _ _) = fl +-- By specialising to (GhcPass p) we know that XXTyVarBndr is DataConCantHappen +-- so these two equations are exhaustive: extension construction can't happen -- | Set the attached flag setHsTyVarBndrFlag :: flag -> HsTyVarBndr flag' (GhcPass pass) @@ -292,6 +295,14 @@ setHsTyVarBndrFlag :: flag -> HsTyVarBndr flag' (GhcPass pass) setHsTyVarBndrFlag f (UserTyVar x _ l) = UserTyVar x f l setHsTyVarBndrFlag f (KindedTyVar x _ l k) = KindedTyVar x f l k +-- | Update the attached flag +updateHsTyVarBndrFlag + :: (flag -> flag') + -> HsTyVarBndr flag (GhcPass pass) + -> HsTyVarBndr flag' (GhcPass pass) +updateHsTyVarBndrFlag f (UserTyVar x flag name) = UserTyVar x (f flag) name +updateHsTyVarBndrFlag f (KindedTyVar x flag name ki) = KindedTyVar x (f flag) name ki + -- | Do all type variables in this 'LHsQTyVars' come with kind annotations? hsTvbAllKinded :: LHsQTyVars (GhcPass p) -> Bool hsTvbAllKinded = all (isHsKindedTyVar . unLoc) . hsQTvExplicit @@ -964,6 +975,15 @@ instance OutputableBndrFlag Specificity p where pprTyVarBndr (KindedTyVar _ SpecifiedSpec n k) = parens $ hsep [ppr n, dcolon, ppr k] pprTyVarBndr (KindedTyVar _ InferredSpec n k) = braces $ hsep [ppr n, dcolon, ppr k] +instance OutputableBndrFlag (HsBndrVis p') p where + pprTyVarBndr (UserTyVar _ vis n) = pprHsBndrVis vis $ ppr n + pprTyVarBndr (KindedTyVar _ vis n k) = + pprHsBndrVis vis $ parens $ hsep [ppr n, dcolon, ppr k] + +pprHsBndrVis :: HsBndrVis pass -> SDoc -> SDoc +pprHsBndrVis HsBndrRequired d = d +pprHsBndrVis (HsBndrInvisible _) d = char '@' <> d + instance OutputableBndrId p => Outputable (HsSigType (GhcPass p)) where ppr (HsSig { sig_bndrs = outer_bndrs, sig_body = body }) = pprHsOuterSigTyVarBndrs outer_bndrs <+> ppr body diff --git a/compiler/GHC/HsToCore/Quote.hs b/compiler/GHC/HsToCore/Quote.hs index 63094c21dd..88c0c727f5 100644 --- a/compiler/GHC/HsToCore/Quote.hs +++ b/compiler/GHC/HsToCore/Quote.hs @@ -2,6 +2,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} @@ -513,7 +514,7 @@ repKiSigD (L loc kisig) = ------------------------- repDataDefn :: Core TH.Name - -> Either (Core [(M (TH.TyVarBndr ()))]) + -> Either (Core [(M (TH.TyVarBndr TH.BndrVis))]) -- the repTyClD case (Core (Maybe [(M (TH.TyVarBndr ()))]), Core (M TH.Type)) -- the repDataFamInstD case @@ -536,7 +537,7 @@ repDataDefn tc opts derivs1 } } -repSynDecl :: Core TH.Name -> Core [(M (TH.TyVarBndr ()))] +repSynDecl :: Core TH.Name -> Core [(M (TH.TyVarBndr TH.BndrVis))] -> LHsType GhcRn -> MetaM (Core (M TH.Dec)) repSynDecl tc bndrs ty @@ -1179,6 +1180,17 @@ rep_flag :: Specificity -> MetaM (Core TH.Specificity) rep_flag SpecifiedSpec = rep2_nw specifiedSpecName [] rep_flag InferredSpec = rep2_nw inferredSpecName [] +instance RepTV (HsBndrVis GhcRn) TH.BndrVis where + tyVarBndrName = tyVarBndrVisTyConName + repPlainTV (MkC nm) vis = do { (MkC vis') <- rep_bndr_vis vis + ; rep2 plainBndrTVName [nm, vis'] } + repKindedTV (MkC nm) vis (MkC ki) = do { (MkC vis') <- rep_bndr_vis vis + ; rep2 kindedBndrTVName [nm, vis', ki] } + +rep_bndr_vis :: HsBndrVis GhcRn -> MetaM (Core TH.BndrVis) +rep_bndr_vis HsBndrRequired = rep2_nw bndrReqName [] +rep_bndr_vis (HsBndrInvisible _) = rep2_nw bndrInvisName [] + addHsOuterFamEqnTyVarBinds :: HsOuterFamEqnTyVarBndrs GhcRn -> (Core (Maybe [M TH.TyVarBndrUnit]) -> MetaM (Core (M a))) @@ -1284,7 +1296,7 @@ addHsTyVarBinds fresh_or_reuse exp_tvs thing_inside addQTyVarBinds :: FreshOrReuse -> LHsQTyVars GhcRn -- the binders to be added - -> (Core [(M (TH.TyVarBndr ()))] -> MetaM (Core (M a))) -- action in the ext env + -> (Core [(M (TH.TyVarBndr TH.BndrVis))] -> MetaM (Core (M a))) -- action in the ext env -> MetaM (Core (M a)) addQTyVarBinds fresh_or_reuse qtvs thing_inside = let HsQTvs { hsq_ext = imp_tvs @@ -2537,7 +2549,7 @@ repFun (MkC nm) (MkC b) = rep2 funDName [nm, b] repData :: Bool -- ^ @True@ for a @type data@ declaration. -- See Note [Type data declarations] in GHC.Rename.Module -> Core (M TH.Cxt) -> Core TH.Name - -> Either (Core [(M (TH.TyVarBndr ()))]) + -> Either (Core [(M (TH.TyVarBndr TH.BndrVis))]) (Core (Maybe [(M (TH.TyVarBndr ()))]), Core (M TH.Type)) -> Core (Maybe (M TH.Kind)) -> Core [(M TH.Con)] -> Core [M TH.DerivClause] -> MetaM (Core (M TH.Dec)) @@ -2549,7 +2561,7 @@ repData _ (MkC cxt) (MkC _) (Right (MkC mb_bndrs, MkC ty)) (MkC ksig) (MkC cons) = rep2 dataInstDName [cxt, mb_bndrs, ty, ksig, cons, derivs] repNewtype :: Core (M TH.Cxt) -> Core TH.Name - -> Either (Core [(M (TH.TyVarBndr ()))]) + -> Either (Core [(M (TH.TyVarBndr TH.BndrVis))]) (Core (Maybe [(M (TH.TyVarBndr ()))]), Core (M TH.Type)) -> Core (Maybe (M TH.Kind)) -> Core (M TH.Con) -> Core [M TH.DerivClause] -> MetaM (Core (M TH.Dec)) @@ -2560,7 +2572,7 @@ repNewtype (MkC cxt) (MkC _) (Right (MkC mb_bndrs, MkC ty)) (MkC ksig) (MkC con) (MkC derivs) = rep2 newtypeInstDName [cxt, mb_bndrs, ty, ksig, con, derivs] -repTySyn :: Core TH.Name -> Core [(M (TH.TyVarBndr ()))] +repTySyn :: Core TH.Name -> Core [(M (TH.TyVarBndr TH.BndrVis))] -> Core (M TH.Type) -> MetaM (Core (M TH.Dec)) repTySyn (MkC nm) (MkC tvs) (MkC rhs) = rep2 tySynDName [nm, tvs, rhs] @@ -2618,7 +2630,7 @@ repOverlap mb = just = coreJust overlapTyConName -repClass :: Core (M TH.Cxt) -> Core TH.Name -> Core [(M (TH.TyVarBndr ()))] +repClass :: Core (M TH.Cxt) -> Core TH.Name -> Core [(M (TH.TyVarBndr TH.BndrVis))] -> Core [TH.FunDep] -> Core [(M TH.Dec)] -> MetaM (Core (M TH.Dec)) repClass (MkC cxt) (MkC cls) (MkC tvs) (MkC fds) (MkC ds) @@ -2667,13 +2679,13 @@ repTySynInst :: Core (M TH.TySynEqn) -> MetaM (Core (M TH.Dec)) repTySynInst (MkC eqn) = rep2 tySynInstDName [eqn] -repDataFamilyD :: Core TH.Name -> Core [(M (TH.TyVarBndr ()))] +repDataFamilyD :: Core TH.Name -> Core [(M (TH.TyVarBndr TH.BndrVis))] -> Core (Maybe (M TH.Kind)) -> MetaM (Core (M TH.Dec)) repDataFamilyD (MkC nm) (MkC tvs) (MkC kind) = rep2 dataFamilyDName [nm, tvs, kind] repOpenFamilyD :: Core TH.Name - -> Core [(M (TH.TyVarBndr ()))] + -> Core [(M (TH.TyVarBndr TH.BndrVis))] -> Core (M TH.FamilyResultSig) -> Core (Maybe TH.InjectivityAnn) -> MetaM (Core (M TH.Dec)) @@ -2681,7 +2693,7 @@ repOpenFamilyD (MkC nm) (MkC tvs) (MkC result) (MkC inj) = rep2 openTypeFamilyDName [nm, tvs, result, inj] repClosedFamilyD :: Core TH.Name - -> Core [(M (TH.TyVarBndr ()))] + -> Core [(M (TH.TyVarBndr TH.BndrVis))] -> Core (M TH.FamilyResultSig) -> Core (Maybe TH.InjectivityAnn) -> Core [(M TH.TySynEqn)] diff --git a/compiler/GHC/Parser/Errors/Ppr.hs b/compiler/GHC/Parser/Errors/Ppr.hs index aadb2a0a79..b54f64eb93 100644 --- a/compiler/GHC/Parser/Errors/Ppr.hs +++ b/compiler/GHC/Parser/Errors/Ppr.hs @@ -430,14 +430,6 @@ instance Diagnostic PsMessage where -> mkSimpleDecorated $ text "Malformed" <+> what <+> text "declaration for" <+> quotes (ppr for) - PsErrUnexpectedTypeAppInDecl ki what for - -> mkSimpleDecorated $ - vcat [ text "Unexpected type application" - <+> text "@" <> ppr ki - , text "In the" <+> what - <+> text "declaration for" - <+> quotes (ppr for) - ] PsErrNotADataCon name -> mkSimpleDecorated $ text "Not a data constructor:" <+> quotes (ppr name) PsErrInferredTypeVarNotAllowed @@ -626,7 +618,6 @@ instance Diagnostic PsMessage where PsErrAtInPatPos -> ErrorWithoutFlag PsErrParseErrorOnInput{} -> ErrorWithoutFlag PsErrMalformedDecl{} -> ErrorWithoutFlag - PsErrUnexpectedTypeAppInDecl{} -> ErrorWithoutFlag PsErrNotADataCon{} -> ErrorWithoutFlag PsErrInferredTypeVarNotAllowed -> ErrorWithoutFlag PsErrIllegalTraditionalRecordSyntax{} -> ErrorWithoutFlag @@ -767,7 +758,6 @@ instance Diagnostic PsMessage where PsErrAtInPatPos -> noHints PsErrParseErrorOnInput{} -> noHints PsErrMalformedDecl{} -> noHints - PsErrUnexpectedTypeAppInDecl{} -> noHints PsErrNotADataCon{} -> noHints PsErrInferredTypeVarNotAllowed -> noHints PsErrIllegalTraditionalRecordSyntax{} -> [suggestExtension LangExt.TraditionalRecordSyntax] diff --git a/compiler/GHC/Parser/Errors/Types.hs b/compiler/GHC/Parser/Errors/Types.hs index 87f7f8d509..d9e8a4dbdd 100644 --- a/compiler/GHC/Parser/Errors/Types.hs +++ b/compiler/GHC/Parser/Errors/Types.hs @@ -367,9 +367,6 @@ data PsMessage -- | Malformed ... declaration for ... | PsErrMalformedDecl !SDoc !RdrName - -- | Unexpected type application in a declaration - | PsErrUnexpectedTypeAppInDecl !(LHsType GhcPs) !SDoc !RdrName - -- | Not a data constructor | PsErrNotADataCon !RdrName diff --git a/compiler/GHC/Parser/PostProcess.hs b/compiler/GHC/Parser/PostProcess.hs index 48e4320faf..890133ff6d 100644 --- a/compiler/GHC/Parser/PostProcess.hs +++ b/compiler/GHC/Parser/PostProcess.hs @@ -890,38 +890,37 @@ checkTyVars pp_what equals_or_where tc tparms = do { tvs <- mapM check tparms ; return (mkHsQTvs tvs) } where - check (HsTypeArg _ ki@(L loc _)) = addFatalError $ mkPlainErrorMsgEnvelope (locA loc) $ - (PsErrUnexpectedTypeAppInDecl ki pp_what (unLoc tc)) - check (HsValArg ty) = chkParens [] [] emptyComments ty + check (HsTypeArg at ki) = chkParens [] [] emptyComments (HsBndrInvisible at) ki + check (HsValArg ty) = chkParens [] [] emptyComments HsBndrRequired ty check (HsArgPar sp) = addFatalError $ mkPlainErrorMsgEnvelope sp $ (PsErrMalformedDecl pp_what (unLoc tc)) -- Keep around an action for adjusting the annotations of extra parens - chkParens :: [AddEpAnn] -> [AddEpAnn] -> EpAnnComments -> LHsType GhcPs - -> P (LHsTyVarBndr () GhcPs) - chkParens ops cps cs (L l (HsParTy an ty)) + chkParens :: [AddEpAnn] -> [AddEpAnn] -> EpAnnComments -> HsBndrVis GhcPs -> LHsType GhcPs + -> P (LHsTyVarBndr (HsBndrVis GhcPs) GhcPs) + chkParens ops cps cs bvis (L l (HsParTy an ty)) = let (o,c) = mkParensEpAnn (realSrcSpan $ locA l) in - chkParens (o:ops) (c:cps) (cs Semi.<> epAnnComments an) ty - chkParens ops cps cs ty = chk ops cps cs ty + chkParens (o:ops) (c:cps) (cs Semi.<> epAnnComments an) bvis ty + chkParens ops cps cs bvis ty = chk ops cps cs bvis ty -- Check that the name space is correct! - chk :: [AddEpAnn] -> [AddEpAnn] -> EpAnnComments -> LHsType GhcPs -> P (LHsTyVarBndr () GhcPs) - chk ops cps cs (L l (HsKindSig annk (L annt (HsTyVar ann _ (L lv tv))) k)) + chk :: [AddEpAnn] -> [AddEpAnn] -> EpAnnComments -> HsBndrVis GhcPs -> LHsType GhcPs -> P (LHsTyVarBndr (HsBndrVis GhcPs) GhcPs) + chk ops cps cs bvis (L l (HsKindSig annk (L annt (HsTyVar ann _ (L lv tv))) k)) | isRdrTyVar tv = let an = (reverse ops) ++ cps in return (L (widenLocatedAn (l Semi.<> annt) an) - (KindedTyVar (addAnns (annk Semi.<> ann) an cs) () (L lv tv) k)) - chk ops cps cs (L l (HsTyVar ann _ (L ltv tv))) + (KindedTyVar (addAnns (annk Semi.<> ann) an cs) bvis (L lv tv) k)) + chk ops cps cs bvis (L l (HsTyVar ann _ (L ltv tv))) | isRdrTyVar tv = let an = (reverse ops) ++ cps in return (L (widenLocatedAn l an) - (UserTyVar (addAnns ann an cs) () (L ltv tv))) - chk _ _ _ t@(L loc _) + (UserTyVar (addAnns ann an cs) bvis (L ltv tv))) + chk _ _ _ _ t@(L loc _) = addFatalError $ mkPlainErrorMsgEnvelope (locA loc) $ (PsErrUnexpectedTypeInDecl t pp_what (unLoc tc) tparms equals_or_where) diff --git a/compiler/GHC/Rename/HsType.hs b/compiler/GHC/Rename/HsType.hs index f9720a53e1..519b1ce318 100644 --- a/compiler/GHC/Rename/HsType.hs +++ b/compiler/GHC/Rename/HsType.hs @@ -975,7 +975,8 @@ bindHsQTyVars doc mb_assoc body_kv_occs hsq_bndrs thing_inside -- This is the only call site for bindLHsTyVarBndrs where we pass -- NoWarnUnusedForalls, which suppresses -Wunused-foralls warnings. -- See Note [Suppress -Wunused-foralls when binding LHsQTyVars]. - do { let -- The SrcSpan that rnImplicitTvOccs will attach to each Name will + do { rn_bndrs <- traverse rnLHsTyVarBndrVisFlag rn_bndrs + ; let -- The SrcSpan that rnImplicitTvOccs will attach to each Name will -- span the entire declaration to which the LHsQTyVars belongs, -- which will be reflected in warning and error messages. We can -- be a little more precise than that by pointing to the location @@ -1003,7 +1004,7 @@ bindHsQTyVars doc mb_assoc body_kv_occs hsq_bndrs thing_inside -- The in-tree API annotations extend the LHsTyVarBndr location to -- include surrounding parens. for error messages to be -- compatible, we recreate the location from the contents - get_bndr_loc :: LHsTyVarBndr () GhcPs -> SrcSpan + get_bndr_loc :: LHsTyVarBndr flag GhcPs -> SrcSpan get_bndr_loc (L _ (UserTyVar _ _ ln)) = getLocA ln get_bndr_loc (L _ (KindedTyVar _ _ ln lk)) = combineSrcSpans (getLocA ln) (getLocA lk) @@ -1239,6 +1240,25 @@ bindLHsTyVarBndr doc mb_assoc (L loc (KindedTyVar x fl lrdr@(L lv _) kind)) $ thing_inside (L loc (KindedTyVar x fl (L lv tv_nm) kind')) ; return (b, fvs1 `plusFV` fvs2) } +-- Check for TypeAbstractions and update the type parameter of HsBndrVis. +-- The binder itself is already renamed and is returned unmodified. +rnLHsTyVarBndrVisFlag + :: LHsTyVarBndr (HsBndrVis GhcPs) GhcRn + -> RnM (LHsTyVarBndr (HsBndrVis GhcRn) GhcRn) +rnLHsTyVarBndrVisFlag (L loc bndr) = do + let lbndr = L loc (updateHsTyVarBndrFlag rnHsBndrVis bndr) + unlessXOptM LangExt.TypeAbstractions $ + when (isHsBndrInvisible (hsTyVarBndrFlag bndr)) $ + addErr (TcRnIllegalInvisTyVarBndr lbndr) + return lbndr + +-- rnHsBndrVis is a no-op. We could use 'coerce' in an ideal world, +-- but GHC can't crack this nut because type families are involved: +-- HsBndrInvisible stores (LHsToken "@" pass), which is defined via XRec. +rnHsBndrVis :: HsBndrVis GhcPs -> HsBndrVis GhcRn +rnHsBndrVis HsBndrRequired = HsBndrRequired +rnHsBndrVis (HsBndrInvisible at) = HsBndrInvisible at + newTyVarNameRn :: Maybe a -- associated class -> LocatedN RdrName -> RnM Name newTyVarNameRn mb_assoc lrdr@(L _ rdr) diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs index 9880c13a9c..aba12a139f 100644 --- a/compiler/GHC/Tc/Errors/Ppr.hs +++ b/compiler/GHC/Tc/Errors/Ppr.hs @@ -1307,6 +1307,30 @@ instance Diagnostic TcRnMessage where sigs = sig1 : sig2 : otherSigs + TcRnIllegalInvisTyVarBndr bndr -> + mkSimpleDecorated $ + hang (text "Illegal invisible type variable binder:") + 2 (ppr bndr) + + TcRnInvalidInvisTyVarBndr name hs_bndr -> + mkSimpleDecorated $ + vcat [ hang (text "Invalid invisible type variable binder:") + 2 (ppr hs_bndr) + , text "There is no matching forall-bound variable" + , text "in the standalone kind signature for" <+> quotes (ppr name) <> dot + , text "NB." <+> vcat [ + text "Only" <+> quotes (text "forall a.") <+> text "-quantification matches invisible binders,", + text "whereas" <+> quotes (text "forall {a}.") <+> text "and" <+> quotes (text "forall a ->") <+> text "do not." + ]] + + TcRnInvisBndrWithoutSig _ hs_bndr -> + mkSimpleDecorated $ + vcat [ hang (text "Invalid invisible type variable binder:") + 2 (ppr hs_bndr) + , text "Either a standalone kind signature (SAKS)" + , text "or a complete user-supplied kind (CUSK, legacy feature)" + , text "is required to use invisible binders." ] + diagnosticReason = \case TcRnUnknownMessage m -> diagnosticReason m @@ -1734,6 +1758,12 @@ instance Diagnostic TcRnMessage where -> ErrorWithoutFlag TcRnDuplicateMinimalSig{} -> ErrorWithoutFlag + TcRnIllegalInvisTyVarBndr{} + -> ErrorWithoutFlag + TcRnInvalidInvisTyVarBndr{} + -> ErrorWithoutFlag + TcRnInvisBndrWithoutSig{} + -> ErrorWithoutFlag diagnosticHints = \case TcRnUnknownMessage m @@ -2173,6 +2203,12 @@ instance Diagnostic TcRnMessage where -> noHints TcRnDuplicateMinimalSig{} -> noHints + TcRnIllegalInvisTyVarBndr{} + -> [suggestExtension LangExt.TypeAbstractions] + TcRnInvalidInvisTyVarBndr{} + -> noHints + TcRnInvisBndrWithoutSig name _ + -> [SuggestAddStandaloneKindSignature name] diagnosticCode = constructorCode diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs index c1b8461839..7166828ef5 100644 --- a/compiler/GHC/Tc/Errors/Types.hs +++ b/compiler/GHC/Tc/Errors/Types.hs @@ -2011,7 +2011,7 @@ data TcRnMessage where Test cases: saks/should_fail/saks_fail008 -} - TcRnTooManyBinders :: !Kind -> ![LHsTyVarBndr () GhcRn] -> TcRnMessage + TcRnTooManyBinders :: !Kind -> ![LHsTyVarBndr (HsBndrVis GhcRn) GhcRn] -> TcRnMessage {- TcRnDifferentNamesForTyVar is an error that indicates different names being used for the same type variable. @@ -2923,6 +2923,49 @@ data TcRnMessage where Test cases: rename/should_fail/RnMultipleMinimalPragmaFail -} TcRnDuplicateMinimalSig :: LSig GhcPs -> LSig GhcPs -> [LSig GhcPs] -> TcRnMessage + {-| 'TcRnIllegalInvisTyVarBndr' is an error that occurs + when invisible type variable binders in type declarations + are used without enabling the @TypeAbstractions@ extension. + + Example: + {-# LANGUAGE NoTypeAbstractions #-} -- extension disabled + data T @k (a :: k) @(j :: Type) (b :: j) + ^^ ^^^^^^^^^^^^ + + Test case: T22560_fail_ext + -} + TcRnIllegalInvisTyVarBndr + :: !(LHsTyVarBndr (HsBndrVis GhcRn) GhcRn) + -> TcRnMessage + + {-| 'TcRnInvalidInvisTyVarBndr' is an error that occurs + when an invisible type variable binder has no corresponding + @forall k.@ quantifier in the standalone kind signature. + + Example: + type P :: forall a -> Type + data P @a = MkP + + Test cases: T22560_fail_a T22560_fail_b + -} + TcRnInvalidInvisTyVarBndr + :: !Name + -> !(LHsTyVarBndr (HsBndrVis GhcRn) GhcRn) + -> TcRnMessage + + {-| 'TcRnInvisBndrWithoutSig' is an error triggered by attempting to use + an invisible type variable binder in a type declaration without a + standalone kind signature or a complete user-supplied kind. + + Example: + data T @k (a :: k) -- No CUSK, no SAKS + + Test case: T22560_fail_d + -} + TcRnInvisBndrWithoutSig + :: !Name + -> !(LHsTyVarBndr (HsBndrVis GhcRn) GhcRn) + -> TcRnMessage deriving Generic diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs index bf15393048..01d5df6782 100644 --- a/compiler/GHC/Tc/Gen/HsType.hs +++ b/compiler/GHC/Tc/Gen/HsType.hs @@ -2304,10 +2304,10 @@ data InitialKindStrategy | InitialKindInfer -- Does the declaration have a standalone kind signature (SAKS) or a complete --- user-specified kind (CUSK)? +-- user-supplied kind (CUSK)? data SAKS_or_CUSK = SAKS Kind -- Standalone kind signature, fully zonked! (zonkTcTypeToType) - | CUSK -- Complete user-specified kind (CUSK) + | CUSK -- Complete user-supplied kind (CUSK) instance Outputable SAKS_or_CUSK where ppr (SAKS k) = text "SAKS" <+> ppr k @@ -2364,7 +2364,7 @@ kcCheckDeclHeader_cusk name flav -- See Note [Required, Specified, and Inferred for types] in GHC.Tc.TyCl = addTyConFlavCtxt name flav $ do { skol_info <- mkSkolemInfo skol_info_anon - ; (tclvl, wanted, (scoped_kvs, (tc_tvs, res_kind))) + ; (tclvl, wanted, (scoped_kvs, (tc_bndrs, res_kind))) <- pushLevelAndSolveEqualitiesX "kcCheckDeclHeader_cusk" $ bindImplicitTKBndrs_Q_Skol skol_info kv_ns $ bindExplicitTKBndrs_Q_Skol skol_info ctxt_kind hs_tvs $ @@ -2372,7 +2372,7 @@ kcCheckDeclHeader_cusk name flav -- Now, because we're in a CUSK, -- we quantify over the mentioned kind vars - ; let spec_req_tkvs = scoped_kvs ++ tc_tvs + ; let spec_req_tkvs = scoped_kvs ++ binderVars tc_bndrs all_kinds = res_kind : map tyVarKind spec_req_tkvs ; candidates <- candidateQTyVarsOfKinds all_kinds @@ -2384,9 +2384,9 @@ kcCheckDeclHeader_cusk name flav candidates `delCandidates` spec_req_tkvs -- NB: 'inferred' comes back sorted in dependency order - ; scoped_kvs <- mapM zonkTyCoVarKind scoped_kvs -- scoped_kvs and tc_tvs are skolems, - ; tc_tvs <- mapM zonkTyCoVarKind tc_tvs -- so zonkTyCoVarKind suffices - ; res_kind <- zonkTcType res_kind + ; scoped_kvs <- mapM zonkTyCoVarKind scoped_kvs -- scoped_kvs and tc_bndrs are skolems, + ; tc_bndrs <- mapM zonkTyCoVarBndrKind tc_bndrs -- so zonkTyCoVarKind suffices + ; res_kind <- zonkTcType res_kind ; let mentioned_kv_set = candidateKindVars candidates specified = scopedSort scoped_kvs @@ -2394,15 +2394,15 @@ kcCheckDeclHeader_cusk name flav all_tcbs = mkNamedTyConBinders Inferred inferred ++ mkNamedTyConBinders Specified specified - ++ map (mkRequiredTyConBinder mentioned_kv_set) tc_tvs + ++ map (mkExplicitTyConBinder mentioned_kv_set) tc_bndrs -- Eta expand if necessary; we are building a PolyTyCon ; (eta_tcbs, res_kind) <- etaExpandAlgTyCon flav skol_info all_tcbs res_kind - ; let all_tv_prs = mkTyVarNamePairs (scoped_kvs ++ tc_tvs) + ; let all_tv_prs = mkTyVarNamePairs (scoped_kvs ++ binderVars tc_bndrs) final_tcbs = all_tcbs `chkAppend` eta_tcbs tycon = mkTcTyCon name final_tcbs res_kind all_tv_prs - True -- it is generalised + True -- Make a PolyTcTyCon, fully generalised flav ; reportUnsolvedEqualities skol_info (binderVars final_tcbs) @@ -2422,7 +2422,7 @@ kcCheckDeclHeader_cusk name flav , text "scoped_kvs" <+> ppr scoped_kvs , text "spec_req_tvs" <+> pprTyVars spec_req_tkvs , text "all_kinds" <+> ppr all_kinds - , text "tc_tvs" <+> pprTyVars tc_tvs + , text "tc_tvs" <+> pprTyVars (binderVars tc_bndrs) , text "res_kind" <+> ppr res_kind , text "inferred" <+> ppr inferred , text "specified" <+> ppr specified @@ -2437,6 +2437,15 @@ kcCheckDeclHeader_cusk name flav ctxt_kind | tcFlavourIsOpen flav = TheKind liftedTypeKind | otherwise = AnyKind +-- | Create a TyConBinder for a user-written type variable binder. +mkExplicitTyConBinder :: TyCoVarSet -- variables that are used dependently + -> VarBndr TyVar (HsBndrVis GhcRn) + -> TyConBinder +mkExplicitTyConBinder dep_set (Bndr tv flag) = + case flag of + HsBndrRequired -> mkRequiredTyConBinder dep_set tv + HsBndrInvisible{} -> mkNamedTyConBinder Specified tv + -- | Kind-check a 'LHsQTyVars'. Used in 'inferInitialKind' (for tycon kinds and -- other kinds). -- @@ -2449,15 +2458,16 @@ kcInferDeclHeader -> TcM MonoTcTyCon -- ^ A suitably-kinded non-generalized TcTyCon kcInferDeclHeader name flav (HsQTvs { hsq_ext = kv_ns - , hsq_explicit = hs_tvs }) kc_res_ki + , hsq_explicit = hs_bndrs }) kc_res_ki -- No standalone kind signature and no CUSK. -- See Note [Required, Specified, and Inferred for types] in GHC.Tc.TyCl = addTyConFlavCtxt name flav $ - do { (scoped_kvs, (tc_tvs, res_kind)) + do { rejectInvisibleBinders name hs_bndrs + ; (scoped_kvs, (tc_bndrs, res_kind)) -- Why bindImplicitTKBndrs_Q_Tv which uses newTyVarTyVar? -- See Note [Inferring kinds for type declarations] in GHC.Tc.TyCl - <- bindImplicitTKBndrs_Q_Tv kv_ns $ - bindExplicitTKBndrs_Q_Tv ctxt_kind hs_tvs $ + <- bindImplicitTKBndrs_Q_Tv kv_ns $ + bindExplicitTKBndrs_Q_Tv ctxt_kind hs_bndrs $ newExpectedKind =<< kc_res_ki -- Why "_Tv" not "_Skol"? See third wrinkle in -- Note [Inferring kinds for type declarations] in GHC.Tc.TyCl, @@ -2467,12 +2477,17 @@ kcInferDeclHeader name flav -- recursive group. -- See Note [Inferring kinds for type declarations] in GHC.Tc.TyCl + tc_tvs = binderVars tc_bndrs + -- Discard visibility flags. We made sure all of them are HsBndrRequired + -- by the call to rejectInvisibleBinders above. + tc_binders = mkAnonTyConBinders tc_tvs - -- Also, note that tc_binders has the tyvars from only the - -- user-written tyvarbinders. See S1 in Note [How TcTyCons work] - -- in GHC.Tc.TyCl + -- This has to be mkAnonTyConBinder! + -- See Note [No polymorphic recursion in type decls] in GHC.Tc.TyCl -- - -- mkAnonTyConBinder: see Note [No polymorphic recursion] + -- Also, note that tc_binders has the tyvars from only the + -- user-written type variable binders. + -- See S1 Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon] in GHC.Tc.TyCl all_tv_prs = mkTyVarNamePairs (scoped_kvs ++ tc_tvs) -- NB: bindExplicitTKBndrs_Q_Tv does not clone; @@ -2480,11 +2495,11 @@ kcInferDeclHeader name flav -- See Note [Cloning for type variable binders] tycon = mkTcTyCon name tc_binders res_kind all_tv_prs - False -- not yet generalised + False -- Make a MonoTcTyCon flav ; traceTc "kcInferDeclHeader: not-cusk" $ - vcat [ ppr name, ppr kv_ns, ppr hs_tvs + vcat [ ppr name, ppr kv_ns, ppr hs_bndrs , ppr scoped_kvs , ppr tc_tvs, ppr (mkTyConKind tc_binders res_kind) ] ; return tycon } @@ -2492,6 +2507,17 @@ kcInferDeclHeader name flav ctxt_kind | tcFlavourIsOpen flav = TheKind liftedTypeKind | otherwise = AnyKind +-- rejectInvisibleBinders is called on on the inference code path; there is +-- no standalone kind signature, nor CUSK. +-- See Note [No inference for invisible binders in type decls] in GHC.Tc.TyCl +rejectInvisibleBinders :: Name -> [LHsTyVarBndr (HsBndrVis GhcRn) GhcRn] -> TcM () +rejectInvisibleBinders name = mapM_ check_bndr_vis + where + check_bndr_vis :: LHsTyVarBndr (HsBndrVis GhcRn) GhcRn -> TcM () + check_bndr_vis bndr = + when (isHsBndrInvisible (hsTyVarBndrFlag (unLoc bndr))) $ + addErr (TcRnInvisBndrWithoutSig name bndr) + -- | Kind-check a declaration header against a standalone kind signature. -- See Note [kcCheckDeclHeader_sig] kcCheckDeclHeader_sig @@ -2521,7 +2547,7 @@ kcCheckDeclHeader_sig sig_kind name flav ; (tclvl, wanted, (implicit_tvs, (skol_tcbs, (extra_tcbs, tycon_res_kind)))) <- pushLevelAndSolveEqualitiesX "kcCheckDeclHeader_sig" $ -- #16687 bindImplicitTKBndrs_Q_Tv implicit_nms $ -- Q means don't clone - matchUpSigWithDecl sig_tcbs sig_res_kind hs_tv_bndrs $ \ excess_sig_tcbs sig_res_kind -> + matchUpSigWithDecl name sig_tcbs sig_res_kind hs_tv_bndrs $ \ excess_sig_tcbs sig_res_kind -> do { -- Kind-check the result kind annotation, if present: -- data T a b :: res_ki where ... -- ^^^^^^^^^ @@ -2600,7 +2626,9 @@ kcCheckDeclHeader_sig sig_kind name flav -- NB: all_tcbs must bind the tyvars in the range of all_tv_prs -- because the tv_prs is used when (say) typechecking the RHS of -- a type synonym. - ; let tc = mkTcTyCon name swizzled_tcbs swizzled_kind all_tv_prs True flav + ; let tc = mkTcTyCon name swizzled_tcbs swizzled_kind all_tv_prs + True -- Make a PolyTcTyCon, fully generalised + flav ; traceTc "kcCheckDeclHeader_sig }" $ vcat [ text "tyConName = " <+> ppr (tyConName tc) @@ -2612,9 +2640,10 @@ kcCheckDeclHeader_sig sig_kind name flav ; return tc } matchUpSigWithDecl - :: [TcTyConBinder] -- TcTyConBinders (with skolem TcTyVars) from the separate kind signature + :: Name -- Name of the type constructor for error messages + -> [TcTyConBinder] -- TcTyConBinders (with skolem TcTyVars) from the separate kind signature -> TcKind -- The tail end of the kind signature - -> [LHsTyVarBndr () GhcRn] -- User-written binders in decl + -> [LHsTyVarBndr (HsBndrVis GhcRn) GhcRn] -- User-written binders in decl -> ([TcTyConBinder] -> TcKind -> TcM a) -- All user-written binders are in scope -- Argument is excess TyConBinders and tail kind -> TcM ( [TcTyConBinder] -- Skolemised binders, with TcTyVars @@ -2622,7 +2651,7 @@ matchUpSigWithDecl -- See Note [Matching a kind signature with a declaration] -- Invariant: Length of returned TyConBinders + length of excess TyConBinders -- = length of incoming TyConBinders -matchUpSigWithDecl sig_tcbs sig_res_kind hs_bndrs thing_inside +matchUpSigWithDecl name sig_tcbs sig_res_kind hs_bndrs thing_inside = go emptySubst sig_tcbs hs_bndrs where go subst tcbs [] @@ -2633,23 +2662,22 @@ matchUpSigWithDecl sig_tcbs sig_res_kind hs_bndrs thing_inside go _ [] hs_bndrs = failWithTc (TcRnTooManyBinders sig_res_kind hs_bndrs) - go subst (tcb : tcbs') hs_bndrs - | Bndr tv vis <- tcb - , isVisibleTcbVis vis - , (L _ hs_bndr : hs_bndrs') <- hs_bndrs -- hs_bndrs is non-empty + go subst (tcb : tcbs') hs_bndrs@(hs_bndr : hs_bndrs') + | zippable (binderFlag tcb) (hsTyVarBndrFlag (unLoc hs_bndr)) = -- Visible TyConBinder, so match up with the hs_bndrs - do { let tv' = updateTyVarKind (substTy subst) $ + do { let Bndr tv vis = tcb + tv' = updateTyVarKind (substTy subst) $ setTyVarName tv (getName hs_bndr) -- Give the skolem the Name of the HsTyVarBndr, so that if it -- appears in an error message it has a name and binding site -- that come from the type declaration, not the kind signature subst' = extendTCvSubstWithClone subst tv tv' - ; tc_hs_bndr hs_bndr (tyVarKind tv') + ; tc_hs_bndr (unLoc hs_bndr) (tyVarKind tv') ; (tcbs', res) <- tcExtendTyVarEnv [tv'] $ go subst' tcbs' hs_bndrs' ; return (Bndr tv' vis : tcbs', res) } - | otherwise + | skippable (binderFlag tcb) = -- Invisible TyConBinder, so do not consume one of the hs_bndrs do { let (subst', tcb') = substTyConBinderX subst tcb ; (tcbs', res) <- go subst' tcbs' hs_bndrs @@ -2657,7 +2685,14 @@ matchUpSigWithDecl sig_tcbs sig_res_kind hs_bndrs thing_inside -- HsTyVarBndr for an invisible TyConBinder ; return (tcb' : tcbs', res) } - tc_hs_bndr :: HsTyVarBndr () GhcRn -> TcKind -> TcM () + | otherwise = + -- At this point we conclude that: + -- * the quantifier (tcb) is visible: (ty -> ...), (forall a -> ...) + -- * the binder (hs_bndr) is invisible: @t, @(t :: k) + -- Any other combination should have been handled by the zippable/skippable clauses. + failWithTc (TcRnInvalidInvisTyVarBndr name hs_bndr) + + tc_hs_bndr :: HsTyVarBndr (HsBndrVis GhcRn) GhcRn -> TcKind -> TcM () tc_hs_bndr (UserTyVar _ _ _) _ = return () tc_hs_bndr (KindedTyVar _ _ (L _ hs_nm) lhs_kind) expected_kind @@ -2665,6 +2700,17 @@ matchUpSigWithDecl sig_tcbs sig_res_kind hs_bndrs thing_inside ; discardResult $ -- See Note [discardResult in kcCheckDeclHeader_sig] unifyKind (Just (NameThing hs_nm)) sig_kind expected_kind } + -- See GHC Proposal #425, section "Kind checking", + -- where zippable and skippable are defined. + zippable :: TyConBndrVis -> HsBndrVis GhcRn -> Bool + zippable vis HsBndrRequired = isVisibleTcbVis vis + zippable vis (HsBndrInvisible _) = isInvisSpecTcbVis vis + + -- See GHC Proposal #425, section "Kind checking", + -- where zippable and skippable are defined. + skippable :: TyConBndrVis -> Bool + skippable vis = not (isVisibleTcbVis vis) + substTyConBinderX :: Subst -> TyConBinder -> (Subst, TyConBinder) substTyConBinderX subst (Bndr tv vis) = (subst', Bndr tv' vis) @@ -2704,7 +2750,7 @@ Basic plan is this: NB: these TyConBinders contain TyVars, not TcTyVars. * matchUpSigWithDecl: match the [TyConBinder] from the signature with - the [LHsTyVarBndr () GhcRn] from the declaration. The latter are the + the [LHsTyVarBndr (HsBndrVis GhcRn) GhcRn] from the declaration. The latter are the explicit, user-written binders. e.g. data T (a :: k) b = .... There may be more of the former than the latter, because the former @@ -2853,54 +2899,6 @@ signature, not by the inline kind annotation: This (Id Bool) will not show up anywhere after we're done validating it, so we have no use for the produced coercion. --} - -{- Note [No polymorphic recursion] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Should this kind-check? - data T ka (a::ka) b = MkT (T Type Int Bool) - (T (Type -> Type) Maybe Bool) - -Notice that T is used at two different kinds in its RHS. No! -This should not kind-check. Polymorphic recursion is known to -be a tough nut. - -Previously, we laboriously (with help from the renamer) -tried to give T the polymorphic kind - T :: forall ka -> ka -> kappa -> Type -where kappa is a unification variable, even in the inferInitialKinds -phase (which is what kcInferDeclHeader is all about). But -that is dangerously fragile (see the ticket). - -Solution: make kcInferDeclHeader give T a straightforward -monomorphic kind, with no quantification whatsoever. That's why -we use mkAnonTyConBinder for all arguments when figuring out -tc_binders. - -But notice that (#16322 comment:3) - -* The algorithm successfully kind-checks this declaration: - data T2 ka (a::ka) = MkT2 (T2 Type a) - - Starting with (inferInitialKinds) - T2 :: (kappa1 :: kappa2 :: *) -> (kappa3 :: kappa4 :: *) -> * - we get - kappa4 := kappa1 -- from the (a:ka) kind signature - kappa1 := Type -- From application T2 Type - - These constraints are soluble so generaliseTcTyCon gives - T2 :: forall (k::Type) -> k -> * - - But now the /typechecking/ (aka desugaring, tcTyClDecl) phase - fails, because the call (T2 Type a) in the RHS is ill-kinded. - - We'd really prefer all errors to show up in the kind checking - phase. - -* This algorithm still accepts (in all phases) - data T3 ka (a::ka) = forall b. MkT3 (T3 Type b) - although T3 is really polymorphic-recursive too. - Perhaps we should somehow reject that. Note [Kind variable ordering for associated types] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -3047,7 +3045,7 @@ tcTKTelescope mode tele thing_inside = case tele of -- HsOuterTyVarBndrs -------------------------------------- -bindOuterTKBndrsX :: OutputableBndrFlag flag 'Renamed +bindOuterTKBndrsX :: OutputableBndrFlag flag 'Renamed -- Only to support traceTc => SkolemMode -> HsOuterTyVarBndrs flag GhcRn -> TcM a @@ -3124,7 +3122,7 @@ bindOuterFamEqnTKBndrs skol_info -- sm_clone=False: see Note [Cloning for type variable binders] --------------- -tcOuterTKBndrs :: OutputableBndrFlag flag 'Renamed +tcOuterTKBndrs :: OutputableBndrFlag flag 'Renamed -- Only to support traceTc => SkolemInfo -> HsOuterTyVarBndrs flag GhcRn -> TcM a -> TcM (HsOuterTyVarBndrs flag GhcTc, a) @@ -3135,7 +3133,7 @@ tcOuterTKBndrs skol_info -- Do not clone the outer binders -- See Note [Cloning for type variable binders] under "must not" -tcOuterTKBndrsX :: OutputableBndrFlag flag 'Renamed +tcOuterTKBndrsX :: OutputableBndrFlag flag 'Renamed -- Only to support traceTc => SkolemMode -> SkolemInfo -> HsOuterTyVarBndrs flag GhcRn -> TcM a -> TcM (HsOuterTyVarBndrs flag GhcTc, a) @@ -3156,7 +3154,7 @@ tcOuterTKBndrsX skol_mode skol_info outer_bndrs thing_inside -- Explicit tyvar binders -------------------------------------- -tcExplicitTKBndrs :: OutputableBndrFlag flag 'Renamed +tcExplicitTKBndrs :: OutputableBndrFlag flag 'Renamed -- Only to suppor traceTc => SkolemInfo -> [LHsTyVarBndr flag GhcRn] -> TcM a @@ -3164,7 +3162,7 @@ tcExplicitTKBndrs :: OutputableBndrFlag flag 'Renamed tcExplicitTKBndrs skol_info = tcExplicitTKBndrsX (smVanilla { sm_clone = True, sm_tvtv = SMDSkolemTv skol_info }) -tcExplicitTKBndrsX :: OutputableBndrFlag flag 'Renamed +tcExplicitTKBndrsX :: OutputableBndrFlag flag 'Renamed -- Only to suppor traceTc => SkolemMode -> [LHsTyVarBndr flag GhcRn] -> TcM a @@ -3199,14 +3197,14 @@ tcExplicitTKBndrsX skol_mode bndrs thing_inside = case nonEmpty bndrs of -- | Skolemise the 'HsTyVarBndr's in an 'HsForAllTelescope' with the supplied -- 'TcTyMode'. bindExplicitTKBndrs_Skol - :: (OutputableBndrFlag flag 'Renamed) + :: (OutputableBndrFlag flag 'Renamed) -- Only to suppor traceTc => SkolemInfo -> [LHsTyVarBndr flag GhcRn] -> TcM a -> TcM ([VarBndr TyVar flag], a) bindExplicitTKBndrs_Tv - :: (OutputableBndrFlag flag 'Renamed) + :: (OutputableBndrFlag flag 'Renamed) -- Only to suppor traceTc => [LHsTyVarBndr flag GhcRn] -> TcM a -> TcM ([VarBndr TyVar flag], a) @@ -3216,33 +3214,34 @@ bindExplicitTKBndrs_Tv = bindExplicitTKBndrsX (smVanilla { sm_clone = True, sm -- sm_clone: see Note [Cloning for type variable binders] bindExplicitTKBndrs_Q_Skol - :: SkolemInfo + :: (OutputableBndrFlag flag 'Renamed) -- Only to support traceTc + => SkolemInfo -> ContextKind - -> [LHsTyVarBndr () GhcRn] + -> [LHsTyVarBndr flag GhcRn] -> TcM a - -> TcM ([TcTyVar], a) + -> TcM ([VarBndr TyVar flag], a) bindExplicitTKBndrs_Q_Tv - :: ContextKind - -> [LHsTyVarBndr () GhcRn] + :: (OutputableBndrFlag flag 'Renamed) -- Only to support traceTc + => ContextKind + -> [LHsTyVarBndr flag GhcRn] -> TcM a - -> TcM ([TcTyVar], a) + -> TcM ([VarBndr TyVar flag], a) -- These do not clone: see Note [Cloning for type variable binders] bindExplicitTKBndrs_Q_Skol skol_info ctxt_kind hs_bndrs thing_inside - = mapFst binderVars $ - bindExplicitTKBndrsX (smVanilla { sm_clone = False, sm_parent = True + = bindExplicitTKBndrsX (smVanilla { sm_clone = False, sm_parent = True , sm_kind = ctxt_kind, sm_tvtv = SMDSkolemTv skol_info }) hs_bndrs thing_inside -- sm_clone=False: see Note [Cloning for type variable binders] bindExplicitTKBndrs_Q_Tv ctxt_kind hs_bndrs thing_inside - = mapFst binderVars $ - bindExplicitTKBndrsX (smVanilla { sm_clone = False, sm_parent = True + = bindExplicitTKBndrsX (smVanilla { sm_clone = False, sm_parent = True , sm_tvtv = SMDTyVarTv, sm_kind = ctxt_kind }) hs_bndrs thing_inside -- sm_clone=False: see Note [Cloning for type variable binders] -bindExplicitTKBndrsX :: (OutputableBndrFlag flag 'Renamed) +bindExplicitTKBndrsX + :: (OutputableBndrFlag flag 'Renamed) -- Only to support traceTc => SkolemMode -> [LHsTyVarBndr flag GhcRn] -> TcM a diff --git a/compiler/GHC/Tc/Gen/Splice.hs b/compiler/GHC/Tc/Gen/Splice.hs index 943c8dcbd2..9192490847 100644 --- a/compiler/GHC/Tc/Gen/Splice.hs +++ b/compiler/GHC/Tc/Gen/Splice.hs @@ -2135,7 +2135,7 @@ reifyTyCon tc injRHS = map (reifyName . tyVarName) (filterByList ms tvs) in (sig, inj) - ; tvs' <- reifyTyVars (tyConVisibleTyVars tc) + ; tvs' <- reifyTyConBinders tc ; let tfHead = TH.TypeFamilyHead (reifyName tc) tvs' resultSig injectivity ; if isOpenTypeFamilyTyCon tc @@ -2156,7 +2156,7 @@ reifyTyCon tc ; kind' <- fmap Just (reifyKind res_kind) - ; tvs' <- reifyTyVars (tyConVisibleTyVars tc) + ; tvs' <- reifyTyConBinders tc ; fam_envs <- tcGetFamInstEnvs ; instances <- reifyFamilyInstances tc (familyInstances fam_envs tc) ; return (TH.FamilyI @@ -2164,7 +2164,7 @@ reifyTyCon tc | Just (_, rhs) <- synTyConDefn_maybe tc -- Vanilla type synonym = do { rhs' <- reifyType rhs - ; tvs' <- reifyTyVars (tyConVisibleTyVars tc) + ; tvs' <- reifyTyConBinders tc ; return (TH.TyConI (TH.TySynD (reifyName tc) tvs' rhs')) } @@ -2182,7 +2182,7 @@ reifyTyCon tc dataCons = tyConDataCons tc isGadt = isGadtSyntaxTyCon tc ; cons <- mapM (reifyDataCon isGadt (mkTyVarTys tvs)) dataCons - ; r_tvs <- reifyTyVars (tyConVisibleTyVars tc) + ; r_tvs <- reifyTyConBinders tc ; let name = reifyName tc deriv = [] -- Don't know about deriving decl | isTypeDataTyCon tc = @@ -2310,7 +2310,7 @@ reifyClass cls ; insts <- reifyClassInstances cls (InstEnv.classInstances inst_envs cls) ; assocTys <- concatMapM reifyAT ats ; ops <- concatMapM reify_op op_stuff - ; tvs' <- reifyTyVars (tyConVisibleTyVars (classTyCon cls)) + ; tvs' <- reifyTyConBinders (classTyCon cls) ; let dec = TH.ClassD cxt (reifyName cls) tvs' fds' (assocTys ++ ops) ; return (TH.ClassI dec insts) } where @@ -2654,6 +2654,43 @@ instance ReifyFlag Specificity TH.Specificity where reifyFlag SpecifiedSpec = TH.SpecifiedSpec reifyFlag InferredSpec = TH.InferredSpec +instance ReifyFlag TyConBndrVis (Maybe TH.BndrVis) where + reifyFlag AnonTCB = Just TH.BndrReq + reifyFlag (NamedTCB Required) = Just TH.BndrReq + reifyFlag (NamedTCB (Invisible _)) = + Nothing -- See Note [Reifying invisible type variable binders] and #22828. + +-- Currently does not return invisible type variable binders (@k-binders). +-- See Note [Reifying invisible type variable binders] and #22828. +reifyTyConBinders :: TyCon -> TcM [TH.TyVarBndr TH.BndrVis] +reifyTyConBinders tc = fmap (mapMaybe get_bndr) (reifyTyVarBndrs (tyConBinders tc)) + where + get_bndr :: TH.TyVarBndr (Maybe flag) -> Maybe (TH.TyVarBndr flag) + get_bndr = sequenceA + +{- Note [Reifying invisible type variable binders] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In reifyFlag for TyConBndrVis, we have the following clause: + + reifyFlag (NamedTCB (Invisible _)) = Nothing + +This means that reifyTyConBinders doesn't reify invisible type variables as +@k-binders. However, it is possible (and not hard) to change this. +Just replace the above clause with: + + reifyFlag (NamedTCB Specified) = Just TH.BndrInvis + reifyFlag (NamedTCB Inferred) = Nothing -- Inferred variables can not be bound + +There are two reasons we opt not to do that for now. + 1. It would be a (sometimes silent) breaking change affecting th-abstraction, + aeson, and other libraries that assume that reified binders are visible. + 2. It would create an asymmetry with visible kind applications, which are + not reified either. + +This decision is not set in stone. If a use case for reifying invisible type +variable binders presents itself, we can reconsider. See #22828. +-} + reifyTyVars :: [TyVar] -> TcM [TH.TyVarBndr ()] reifyTyVars = reifyTyVarBndrs . map mk_bndr where diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs index f3e02c0fd0..904fdab397 100644 --- a/compiler/GHC/Tc/TyCl.hs +++ b/compiler/GHC/Tc/TyCl.hs @@ -347,6 +347,268 @@ support making synonyms of types with higher-rank kinds. But you can always specify a CUSK directly to make this work out. See tc269 for an example. +Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +A TcTyCon is one of the variants of TyCon. First, here are its invariants: + +* TcTyCon: a TyCon built with the TcTyCon constructor + A TcTyCon contains TcTyVars in its binders and kind + +* TcTyConBinder: a TyConBinder with a TcTyVar inside (not a TyVar) + +* MonoTcTyCon: a form of TcTyCon + - Flag tcTyConIsPoly = False + + - tyConBinders are TcTyConBinders: they contain TcTyVars, which are + unification variables (TyVarTv), and whose kinds may contain + unification variables. + + - tyConKind: the Monomorphic Recursion Principle: + a MonoTcTyCon has a /monomorphic kind/. + See Note [No polymorphic recursion in type decls]. + But the tyConKind may contain free unification variables. + + - tyConScopedTyVars is important; maps a Name to a TyVarTv unification variable + The order matters: Specified then Required variables. + E.g. in + data T a (b :: k) = ... + the order will be [k, a, b]. + + We do not allow @k-binders in inference mode, so we do not need to worry about + data T a @k (b :: k) = ... + where we would have to put `k` (Specified) after `a` (Required) + + NB: There are no Inferred binders in tyConScopedTyVars; 'a' may + also be poly-kinded, but that kind variable will be added by + generaliseTcTyCon, in the passage to a PolyTcTyCon. + + - tyConBinders are irrelevant; we just use tcTyConScopedTyVars + Well not /quite/ irrelevant: + * its length gives the number of explicit binders, and so allows us to + distinguish between the implicit and explicit elements of + tyConScopedTyVars. + * at construction time (mkTcTyCon) for a MonoTcTyCon (the call to mkTcTyCon + in GHC.Tc.Gen.HsType.kcInferDeclHeader) the tyConBinders are used to + construct the tyConKind; all must have AnonTCB visiblity so we we get + a monokind. + +* PolyTcTyCon: a form of TcTyCon + - Flag tcTyConIsPoly = True; this is used only to short-cut zonking + + - tyConBinders are still TcTyConBinders, but they are /skolem/ TcTyVars, + with fixed kinds, and accurate skolem info: no unification variables here + + tyConBinders includes the Inferred binders if any + + tyConBinders uses the Names from the original, renamed program. + + - tcTyConScopedTyVars is irrelevant: just use (binderVars tyConBinders) + All the types have been swizzled back to use the original Names + See Note [tyConBinders and lexical scoping] in GHC.Core.TyCon + +The main purpose of these TcTyCons is during kind-checking of +type/class declarations (in GHC.Tc.TyCl). During kind checking we +come upon knowledge of the eventual tycon in bits and pieces, and we +use a TcTyCon to record what we know before we are ready to build the +final TyCon. Here is the plan: + +* Step 1 (inferInitialKinds, called from kcTyClGroup + inference only, skipped for checking): + Make a MonoTcTyCon whose binders are TcTyVars, + that may contain free unification variables. + See Note [No polymorphic recursion in type decls] + +* Step 2 (kcTyClDecl, called from kcTyClGroup) + Kind-check the declarations of the group; this step just does + unifications that affect the unification variables created in + Step 1 + +* Step 3 (generaliseTcTyCon, called from kcTyClGroup) + Generalise that MonoTcTyCon to make a PolyTcTyCon + Its binders are skolem TcTyVars, with accurate SkolemInfo + +* Step 4 (tcTyClDecl, called from tcTyClDecls) + Typecheck the type and class decls to produce a final TyCon + Its binders are final TyVars, not TcTyVars + +Note that a MonoTcTyCon can contain unification variables, but a +PolyTcTyCon does not: only skolem TcTyVars. See the invariants above. + +More details about /kind inference/: + +S1) In kcTyClGroup, we use inferInitialKinds to look over the + declaration of any TyCon that lacks a kind signature or + CUSK, to determine its "shape"; for example, the number of + parameters, and any kind signatures. + + We record that shape record that shape in a MonoTcTyCon; it is + "mono" because it has not been been generalised, and its binders + and result kind may have free unification variables. + +S2) Still in kcTyClGroup, we use kcLTyClDecl to kind-check the + body (class methods, data constructors, etc.) of each of + these MonoTcTyCons, which has the effect of filling in the + metavariables in the tycon's initial kind. + +S3) Still in kcTyClGroup, we use generaliseTyClDecl to generalize + each MonoTcTyCon to get a PolyTcTyCon, with skolem TcTyVars in it, + and a final, fixed kind. + +S4) Finally, back in tcTyClDecls, we extend the environment with + the PolyTcTyCons, and typecheck each declaration (regardless + of kind signatures etc) to get final TyCon. + +More details about /kind checking/ + +S5) In kcTyClGroup, we use checkInitialKinds to get the + utterly-final Kind of all TyCons in the group that + (a) have a standalone kind signature or + (b) have a CUSK. + This produces a PolyTcTyCon, that is, a TcTyCon in which the binders + and result kind are full of TyVars (not TcTyVars). No unification + variables here; everything is in its final form. + +Wrinkles: + +(W1) When recovering from a type error in a type declaration, + we want to put the erroneous TyCon in the environment in a + way that won't lead to more errors. We use a PolyTcTyCon for this; + see makeRecoveryTyCon. + +(W2) tyConScopedTyVars. A challenging piece in all of this is that we + end up taking three separate passes over every declaration: + - one in inferInitialKind (this pass look only at the head, not the body) + - one in kcTyClDecls (to kind-check the body) + - a final one in tcTyClDecls (to desugar) + + In the latter two passes, we need to connect the user-written type + variables in an LHsQTyVars with the variables in the tycon's + inferred kind. Because the tycon might not have a CUSK, this + matching up is, in general, quite hard to do. (Look through the + git history between Dec 2015 and Apr 2016 for + GHC.Tc.Gen.HsType.splitTelescopeTvs!) + + Instead of trying, we just store the list of type variables to + bring into scope, in the tyConScopedTyVars field of a MonoTcTyCon. + These tyvars are brought into scope by the calls to + tcExtendNameTyVarEnv (tcTyConScopedTyVars tycon) + in kcTyClDecl. + + In a TcTyCon, why is tyConScopedTyVars :: [(Name,TcTyVar)] rather + than just [TcTyVar]? Consider these mutually-recursive decls + data T (a :: k1) b = MkT (S a b) + data S (c :: k2) d = MkS (T c d) + We start with k1 bound to kappa1, and k2 to kappa2; so initially + in the (Name,TcTyVar) pairs the Name is that of the TcTyVar. But + then kappa1 and kappa2 get unified; so after the zonking in + 'generalise' in 'kcTyClGroup' the Name and TcTyVar may differ. + +See also Note [Type checking recursive type and class declarations]. + +Note [No polymorphic recursion in type decls] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In GHC.Tc.HsType.kcInferDeclHeader we use mkAnonTyConBinders to make +the TyConBinders for the MonoTcTyCon. Here is why. + +Should this kind-check (cf #16344)? + data T ka (a::ka) b = MkT (T Type Int Bool) + (T (Type -> Type) Maybe Bool) + +Notice that T is used at two different kinds in its RHS. No! +This should not kind-check. Polymorphic recursion is known to +be a tough nut. + +Many moons ago, we laboriously (with help from the renamer) tried to give T +the polymorphic kind + T :: forall ka -> ka -> kappa -> Type +where kappa is a unification variable, even in the inferInitialKinds phase +(which is what kcInferDeclHeader is all about). But that is dangerously +fragile (see #16344), because `kappa` might get unified with `ka`, and +depending on just /when/ that unification happens, the instantiation of T's +kind would vary between different call sites of T. + +We encountered similar trickiness with invisible binders in type +declarations: see Note [No inference for invisible binders in type decls] + +Solution: the Monomorphic Recursion Principle: + + A MonoTcTyCon has a monomoprhic kind (no foralls!) + +See the invariants on MonoTcTyCon in Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon]. + +So kcInferDeclHeader gives T a straightforward monomorphic kind, with no +quantification whatsoever. That's why we always use mkAnonTyConBinder for +all arguments when figuring out tc_binders. + +But notice that (#16344 comment:3) + +* Consider this declaration: + data T2 ka (a::ka) = MkT2 (T2 Type a) + + Starting with inferInitialKinds + (Step 1 of Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon]): + MonoTcTyCon binders: + ka[tyv] :: (kappa1[tau] :: Type) + a[tyv] :: (ka[tyv] :: Type) + MonoTcTyCon kind: + T2 :: kappa1[tau] -> ka[tyv] -> Type + + Given this kind for T2, in Step 2 we kind-check (T2 Type a) + from where we see + T2's first arg: (kappa1 ~ Type) + T2's second arg: (ka ~ ka) + These constraints are soluble by (kappa1 := Type) + so generaliseTcTyCon (Step 3) gives + T2 :: forall (k::Type) -> k -> * + + But now the /typechecking/ (Step 4, aka desugaring, tcTyClDecl) + phase fails, because the call (T2 Type a) in the RHS is ill-kinded. + + We'd really prefer all errors to show up in the kind checking phase. + +* This algorithm still accepts (in all phases) + data T3 ka (a::ka) = forall b. MkT3 (T3 Type b) + although T3 is really polymorphic-recursive too. + Perhaps we should somehow reject that. + +Note [No inference for invisible binders in type decls] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have (#22560): + data T @k (a::k) = MkT (...(T ty)...) +What monokind can we give to T after step 1 of the kind inference +algorithm described in Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon]? +Remember: Step 1 generates a MonoTcTyCon. + +It can't be + T :: kappa1 -> kappa2 -> Type +because the invocation `(T ty)` doesn't have a visible argument for `kappa`. +Nor can it be + T :: forall k. kappa2 -> Type +because that breaks the Monomorphic Recursion Principle: MonoTcTyCons have +monomorphic kinds; see Note [No polymorphic recursion in type decls]. It could be + T :: kappa1 ->. kappa2 -> type +where `->.` is a new kind of arrow in kinds, which (like a type-class argument +in terms) is invisibly instantiated. Or we could fake it with + T :: forall _. kappa2 -> Type +where `_` is a completely fresh variable, but that seems very smelly and makes it +harder to talk about the Monomorphic Recursion Principle. Moreover we'd need +some extra fancy types in TyConBinders to record this extra information. + +Note that in *terms* we do not allow + f @a (x::a) = rhs +unless `f` has a type signature. So we do the same for types: + + We allow `@` binders in data type declarations ONLY if the + type constructor has a standalone kind signature (or a CUSK). + +That means that GHC.Tc.Gen.HsType.kcInferDeclHeader, which is used when we +don't have a kind signature or CUSK, and builds a MonoTcTyCon, we can simply +reject invisible binders outright (GHC.Tc.Gen.HsType.rejectInvisibleBinders); +and continue to use mkAnonTyConBinders as described in +Note [No polymorphic recursion in type decls]. + +If we get cries of pain we can revist this decision. + Note [CUSKs and PolyKinds] ~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider @@ -398,100 +660,6 @@ environment. (This is handled by `allDecls'). See also Note [Kind checking recursive type and class declarations] -Note [How TcTyCons work] -~~~~~~~~~~~~~~~~~~~~~~~~ -TcTyCons are used for two distinct purposes - -1. When recovering from a type error in a type declaration, - we want to put the erroneous TyCon in the environment in a - way that won't lead to more errors. We use a TcTyCon for this; - see makeRecoveryTyCon. - -2. When checking a type/class declaration (in module GHC.Tc.TyCl), we come - upon knowledge of the eventual tycon in bits and pieces, and we use - a TcTyCon to record what we know before we are ready to build the - final TyCon. Here is the plan: - - Step 1 (inferInitialKinds, inference only, skipped for checking): - Make a MonoTcTyCon whose binders are TcTyVars, - which may contain free unification variables - - Step 2 (generaliseTcTyCon) - Generalise that MonoTcTyCon to make a PolyTcTyCon - Its binders are skolem TcTyVars, with accurate SkolemInfo - - Step 3 (tcTyClDecl) - Typecheck the type and class decls to produce a final TyCon - Its binders are final TyVars, not TcTyVars - - Note that a MonoTcTyCon can contain unification variables, - but a PolyTcTyCon does not: only skolem TcTyVars. See - Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon] in GHC.Tc.Utils.TcType - - More details about /kind inference/: - - S1) In kcTyClGroup, we use inferInitialKinds to look over the - declaration of any TyCon that lacks a kind signature or - CUSK, to determine its "shape"; for example, the number of - parameters, and any kind signatures. - - We record that shape record that shape in a MonoTcTyCon; it is - "mono" because it has not been been generalised, and its binders - and result kind may have free unification variables. - - S2) Still in kcTyClGroup, we use kcLTyClDecl to kind-check the - body (class methods, data constructors, etc.) of each of - these MonoTcTyCons, which has the effect of filling in the - metavariables in the tycon's initial kind. - - S3) Still in kcTyClGroup, we use generaliseTyClDecl to generalize - each MonoTcTyCon to get a PolyTcTyCon, with skolem TcTyVars in it, - and a final, fixed kind. - - S4) Finally, back in TcTyClDecls, we extend the environment with - the PolyTcTyCons, and typecheck each declaration (regardless - of kind signatures etc) to get final TyCon. - - More details about /kind checking/ - - S5) In kcTyClGroup, we use checkInitialKinds to get the - utterly-final Kind of all TyCons in the group that - (a) have a separate kind signature or - (b) have a CUSK. - This produces a PolyTcTyCon, that is, a TcTyCon in which the binders - and result kind are full of TyVars (not TcTyVars). No unification - variables here; everything is in its final form. - -3. tyConScopedTyVars. A challenging piece in all of this is that we - end up taking three separate passes over every declaration: - - one in inferInitialKind (this pass look only at the head, not the body) - - one in kcTyClDecls (to kind-check the body) - - a final one in tcTyClDecls (to desugar) - - In the latter two passes, we need to connect the user-written type - variables in an LHsQTyVars with the variables in the tycon's - inferred kind. Because the tycon might not have a CUSK, this - matching up is, in general, quite hard to do. (Look through the - git history between Dec 2015 and Apr 2016 for - GHC.Tc.Gen.HsType.splitTelescopeTvs!) - - Instead of trying, we just store the list of type variables to - bring into scope, in the tyConScopedTyVars field of a MonoTcTyCon. - These tyvars are brought into scope by the calls to - tcExtendNameTyVarEnv (tcTyConScopedTyVars tycon) - in kcTyClDecl. - - In a TcTyCon, why is tyConScopedTyVars :: [(Name,TcTyVar)] rather - than just [TcTyVar]? Consider these mutually-recursive decls - data T (a :: k1) b = MkT (S a b) - data S (c :: k2) d = MkS (T c d) - We start with k1 bound to kappa1, and k2 to kappa2; so initially - in the (Name,TcTyVar) pairs the Name is that of the TcTyVar. But - then kappa1 and kappa2 get unified; so after the zonking in - 'generalise' in 'kcTyClGroup' the Name and TcTyVar may differ. - -See also Note [Type checking recursive type and class declarations]. - Note [Swizzling the tyvars before generaliseTcTyCon] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ This Note only applies when /inferring/ the kind of a TyCon. @@ -1090,7 +1258,7 @@ Test cases (and tickets) relevant to these design decisions Note [Inferring kinds for type declarations] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ This note deals with /inference/ for type declarations -that do not have a CUSK. Consider +that do not have a CUSK or a SAKS. Consider data T (a :: k1) k2 (x :: k2) = MkT (S a k2 x) data S (b :: k3) k4 (y :: k4) = MkS (T b k4 y) @@ -1254,18 +1422,17 @@ It's hard to know when we've actually been tripped up by polymorphic recursion specifically, so we just include a note to users whenever we infer VDQ. The testsuite did not show up a single spurious inclusion of this message. -The context is added in addVDQNote, which looks for a visible TyConBinder -that also appears in the TyCon's kind. (I first looked at the kind for -a visible, dependent quantifier, but Note [No polymorphic recursion] in -GHC.Tc.Gen.HsType defeats that approach.) addVDQNote is used in kcTyClDecl, -which is used only when inferring the kind of a tycon (never with a CUSK or -SAK). +The context is added in addVDQNote, which looks for a visible +TyConBinder that also appears in the TyCon's kind. (I first looked at +the kind for a visible, dependent quantifier, but + Note [No polymorphic recursion in type decls] +in GHC.Tc.Gen.HsType defeats that approach.) addVDQNote is used in +kcTyClDecl, which is used only when inferring the kind of a tycon +(never with a CUSK or SAKS). Once upon a time, I (Richard E) thought that the tycon-kind could not be a forall-type. But this is wrong: data T :: forall k. k -> Type (with -XNoCUSKs) could end up here. And this is all OK. - - -} -------------- @@ -1583,7 +1750,7 @@ kcTyClDecl :: TyClDecl GhcRn -> MonoTcTyCon -> TcM () -- TcTyVars rather than create skolemised variables for the bound variables. -- - inferInitialKinds makes the TcTyCon where the tyvars are TcTyVars -- - In this function, those TcTyVars are unified with other kind variables during --- kind inference (see [How TcTyCons work]) +-- kind inference (see GHC.Tc.TyCl Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon]) kcTyClDecl (DataDecl { tcdLName = (L _ _name), tcdDataDefn = HsDataDefn { dd_ctxt = ctxt, dd_cons = cons } }) tycon = tcExtendNameTyVarEnv (tcTyConScopedTyVars tycon) $ @@ -5130,7 +5297,7 @@ tcMkDeclCtxt decl = hsep [text "In the", pprTyClDeclFlavour decl, addVDQNote :: TcTyCon -> TcM a -> TcM a -- See Note [Inferring visible dependent quantification] --- Only types without a signature (CUSK or SAK) here +-- Only types without a signature (CUSK or SAKS) here addVDQNote tycon thing_inside | assertPpr (isMonoTcTyCon tycon) (ppr tycon $$ ppr tc_kind) has_vdq diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index 89614378cd..8395bd5540 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -79,6 +79,7 @@ module GHC.Tc.Utils.TcMType ( zonkTcType, zonkTcTypes, zonkCo, zonkTyCoVarKind, + zonkTyCoVarBndrKind, zonkEvVar, zonkWC, zonkImplication, zonkSimples, zonkId, zonkCoVar, zonkCt, zonkSkolemInfo, zonkSkolemInfoAnon, @@ -2317,6 +2318,11 @@ zonkTyCoVarKind :: TyCoVar -> TcM TyCoVar zonkTyCoVarKind tv = do { kind' <- zonkTcType (tyVarKind tv) ; return (setTyVarKind tv kind') } +zonkTyCoVarBndrKind :: VarBndr TyCoVar flag -> TcM (VarBndr TyCoVar flag) +zonkTyCoVarBndrKind (Bndr tv flag) = + do { tv' <- zonkTyCoVarKind tv + ; return (Bndr tv' flag) } + {- ************************************************************************ * * diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs index 67b19c032a..648a508d4b 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs +++ b/compiler/GHC/Tc/Utils/TcType.hs @@ -368,7 +368,7 @@ type TcTyVarBinder = TyVarBinder type TcInvisTVBinder = InvisTVBinder type TcReqTVBinder = ReqTVBinder --- See Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon] +-- See Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon] in GHC.Tc.TyCl type TcTyCon = TyCon type MonoTcTyCon = TcTyCon type PolyTcTyCon = TcTyCon @@ -402,50 +402,6 @@ type TcTyCoVarSet = TyCoVarSet type TcDTyVarSet = DTyVarSet type TcDTyCoVarSet = DTyCoVarSet -{- Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -See Note [How TcTyCons work] in GHC.Tc.TyCl - -Invariants: - -* TcTyCon: a TyCon built with the TcTyCon constructor - -* TcTyConBinder: a TyConBinder with a TcTyVar inside (not a TyVar) - -* TcTyCons contain TcTyVars - -* MonoTcTyCon: - - Flag tcTyConIsPoly = False - - - tyConScopedTyVars is important; maps a Name to a TyVarTv unification variable - The order is important: Specified then Required variables. E.g. in - data T a (b :: k) = ... - the order will be [k, a, b]. - - NB: There are no Inferred binders in tyConScopedTyVars; 'a' may - also be poly-kinded, but that kind variable will be added by - generaliseTcTyCon, in the passage to a PolyTcTyCon. - - - tyConBinders are irrelevant; we just use tcTyConScopedTyVars - Well not /quite/ irrelevant: its length gives the number of Required binders, - and so allows up to distinguish between the Specified and Required elements of - tyConScopedTyVars. - -* PolyTcTyCon: - - Flag tcTyConIsPoly = True; this is used only to short-cut zonking - - - tyConBinders are still TcTyConBinders, but they are /skolem/ TcTyVars, - with fixed kinds, and accurate skolem info: no unification variables here - - tyConBinders includes the Inferred binders if any - - tyConBinders uses the Names from the original, renamed program. - - - tcTyConScopedTyVars is irrelevant: just use (binderVars tyConBinders) - All the types have been swizzled back to use the original Names - See Note [tyConBinders and lexical scoping] in GHC.Core.TyCon - --} {- ********************************************************************* * * diff --git a/compiler/GHC/ThToHs.hs b/compiler/GHC/ThToHs.hs index 498a17694f..cc3f2fdab7 100644 --- a/compiler/GHC/ThToHs.hs +++ b/compiler/GHC/ThToHs.hs @@ -2,6 +2,7 @@ {-# LANGUAGE ConstrainedClassMethods #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE MultiWayIf #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -464,7 +465,7 @@ cvtDec (TH.ImplicitParamBindD _ _) = failWith InvalidImplicitParamBinding -- Convert a @data@ declaration. -cvtDataDec :: TH.Cxt -> TH.Name -> [TH.TyVarBndr ()] +cvtDataDec :: TH.Cxt -> TH.Name -> [TH.TyVarBndr TH.BndrVis] -> Maybe TH.Kind -> [TH.Con] -> [TH.DerivClause] -> CvtM (Maybe (LHsDecl GhcPs)) cvtDataDec = cvtGenDataDec False @@ -472,14 +473,14 @@ cvtDataDec = cvtGenDataDec False -- Convert a @type data@ declaration. -- These have neither contexts nor derived clauses. -- See Note [Type data declarations] in GHC.Rename.Module. -cvtTypeDataDec :: TH.Name -> [TH.TyVarBndr ()] -> Maybe TH.Kind -> [TH.Con] +cvtTypeDataDec :: TH.Name -> [TH.TyVarBndr TH.BndrVis] -> Maybe TH.Kind -> [TH.Con] -> CvtM (Maybe (LHsDecl GhcPs)) cvtTypeDataDec tc tvs ksig constrs = cvtGenDataDec True [] tc tvs ksig constrs [] -- Convert a @data@ or @type data@ declaration (flagged by the Bool arg). -- See Note [Type data declarations] in GHC.Rename.Module. -cvtGenDataDec :: Bool -> TH.Cxt -> TH.Name -> [TH.TyVarBndr ()] +cvtGenDataDec :: Bool -> TH.Cxt -> TH.Name -> [TH.TyVarBndr TH.BndrVis] -> Maybe TH.Kind -> [TH.Con] -> [TH.DerivClause] -> CvtM (Maybe (LHsDecl GhcPs)) cvtGenDataDec type_data ctxt tc tvs ksig constrs derivs @@ -568,7 +569,7 @@ cvt_ci_decs declDescr decs ; return (listToBag binds', sigs', fams', ats', adts') } ---------------- -cvt_tycl_hdr :: TH.Cxt -> TH.Name -> [TH.TyVarBndr ()] +cvt_tycl_hdr :: TH.Cxt -> TH.Name -> [TH.TyVarBndr TH.BndrVis] -> CvtM ( LHsContext GhcPs , LocatedN RdrName , LHsQTyVars GhcPs) @@ -1488,6 +1489,10 @@ instance CvtFlag TH.Specificity Hs.Specificity where cvtFlag TH.SpecifiedSpec = Hs.SpecifiedSpec cvtFlag TH.InferredSpec = Hs.InferredSpec +instance CvtFlag TH.BndrVis (HsBndrVis GhcPs) where + cvtFlag TH.BndrReq = HsBndrRequired + cvtFlag TH.BndrInvis = HsBndrInvisible noHsTok + cvtTvs :: CvtFlag flag flag' => [TH.TyVarBndr flag] -> CvtM [LHsTyVarBndr flag' GhcPs] cvtTvs tvs = mapM cvt_tv tvs diff --git a/compiler/GHC/Types/Error/Codes.hs b/compiler/GHC/Types/Error/Codes.hs index d7b57113ee..e188c89471 100644 --- a/compiler/GHC/Types/Error/Codes.hs +++ b/compiler/GHC/Types/Error/Codes.hs @@ -253,7 +253,6 @@ type family GhcDiagnosticCode c = n | n -> c where GhcDiagnosticCode "PsErrAtInPatPos" = 08382 GhcDiagnosticCode "PsErrParseErrorOnInput" = 66418 GhcDiagnosticCode "PsErrMalformedDecl" = 85316 - GhcDiagnosticCode "PsErrUnexpectedTypeAppInDecl" = 45054 GhcDiagnosticCode "PsErrNotADataCon" = 25742 GhcDiagnosticCode "PsErrInferredTypeVarNotAllowed" = 57342 GhcDiagnosticCode "PsErrIllegalTraditionalRecordSyntax" = 65719 @@ -512,6 +511,9 @@ type family GhcDiagnosticCode c = n | n -> c where GhcDiagnosticCode "TcRnUnexpectedDefaultSig" = 40700 GhcDiagnosticCode "TcRnBindInBootFile" = 11247 GhcDiagnosticCode "TcRnDuplicateMinimalSig" = 85346 + GhcDiagnosticCode "TcRnIllegalInvisTyVarBndr" = 58589 + GhcDiagnosticCode "TcRnInvalidInvisTyVarBndr" = 57916 + GhcDiagnosticCode "TcRnInvisBndrWithoutSig" = 92337 -- IllegalNewtypeReason GhcDiagnosticCode "DoesNotHaveSingleField" = 23517 @@ -619,6 +621,7 @@ type family GhcDiagnosticCode c = n | n -> c where GhcDiagnosticCode "Example outdated error" = 00000 GhcDiagnosticCode "TcRnNameByTemplateHaskellQuote" = 40027 GhcDiagnosticCode "TcRnIllegalBindingOfBuiltIn" = 69639 + GhcDiagnosticCode "PsErrUnexpectedTypeAppInDecl" = 45054 {- ********************************************************************* * * diff --git a/compiler/GHC/Types/Hint.hs b/compiler/GHC/Types/Hint.hs index 9f897feb7f..2c965b7815 100644 --- a/compiler/GHC/Types/Hint.hs +++ b/compiler/GHC/Types/Hint.hs @@ -324,6 +324,14 @@ data GhcHint -} | SuggestAddStandaloneDerivation + {-| Suggests to add a standalone kind signature when GHC + can't perform kind inference. + + Triggered by: 'GHC.Tc.Errors.Types.TcRnInvisBndrWithoutSig' + Test case(s): typecheck/should_fail/T22560_fail_d + -} + | SuggestAddStandaloneKindSignature Name + {-| Suggests the user to fill in the wildcard constraint to disambiguate which constraint that is. diff --git a/compiler/GHC/Types/Hint/Ppr.hs b/compiler/GHC/Types/Hint/Ppr.hs index 96fbd9f74f..40f261a630 100644 --- a/compiler/GHC/Types/Hint/Ppr.hs +++ b/compiler/GHC/Types/Hint/Ppr.hs @@ -143,6 +143,8 @@ instance Outputable GhcHint where Just (DataFamilyInst {}) -> text "data family" SuggestAddStandaloneDerivation -> text "Use a standalone deriving declaration instead" + SuggestAddStandaloneKindSignature name + -> text "Add a standalone kind signature for" <+> quotes (ppr name) SuggestFillInWildcardConstraint -> text "Fill in the wildcard constraint yourself" SuggestRenameForall diff --git a/compiler/Language/Haskell/Syntax/Type.hs b/compiler/Language/Haskell/Syntax/Type.hs index 8898d2400b..f6cbb5443b 100644 --- a/compiler/Language/Haskell/Syntax/Type.hs +++ b/compiler/Language/Haskell/Syntax/Type.hs @@ -25,6 +25,7 @@ module Language.Haskell.Syntax.Type ( HsLinearArrowTokens(..), HsType(..), LHsType, HsKind, LHsKind, + HsBndrVis(..), isHsBndrInvisible, HsForAllTelescope(..), HsTyVarBndr(..), LHsTyVarBndr, LHsQTyVars(..), HsOuterTyVarBndrs(..), HsOuterFamEqnTyVarBndrs, HsOuterSigTyVarBndrs, @@ -342,12 +343,12 @@ type LHsTyVarBndr flag pass = XRec pass (HsTyVarBndr flag pass) data LHsQTyVars pass -- See Note [HsType binders] = HsQTvs { hsq_ext :: XHsQTvs pass - , hsq_explicit :: [LHsTyVarBndr () pass] + , hsq_explicit :: [LHsTyVarBndr (HsBndrVis pass) pass] -- Explicit variables, written by the user } | XLHsQTyVars !(XXLHsQTyVars pass) -hsQTvExplicit :: LHsQTyVars pass -> [LHsTyVarBndr () pass] +hsQTvExplicit :: LHsQTyVars pass -> [LHsTyVarBndr (HsBndrVis pass) pass] hsQTvExplicit = hsq_explicit ------------------------------------------------ @@ -713,6 +714,21 @@ data HsTyVarBndr flag pass | XTyVarBndr !(XXTyVarBndr pass) +data HsBndrVis pass + = HsBndrRequired + -- Binder for a visible (required) variable: + -- type Dup a = (a, a) + -- ^^^ + + | HsBndrInvisible (LHsToken "@" pass) + -- Binder for an invisible (specified) variable: + -- type KindOf @k (a :: k) = k + -- ^^^ + +isHsBndrInvisible :: HsBndrVis pass -> Bool +isHsBndrInvisible HsBndrInvisible{} = True +isHsBndrInvisible HsBndrRequired = False + -- | Does this 'HsTyVarBndr' come with an explicit kind annotation? isHsKindedTyVar :: HsTyVarBndr flag pass -> Bool isHsKindedTyVar (UserTyVar {}) = False diff --git a/docs/users_guide/9.8.1-notes.rst b/docs/users_guide/9.8.1-notes.rst index 14c6d5bff6..cc7c76da3e 100644 --- a/docs/users_guide/9.8.1-notes.rst +++ b/docs/users_guide/9.8.1-notes.rst @@ -6,6 +6,15 @@ Version 9.8.1 Language ~~~~~~~~ +- GHC Proposal `#425 + <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0425-decl-invis-binders.rst>`_ + has been partially implemented. Namely, the ``@k``-binders in type declarations are now permitted:: + + type T :: forall k. k -> forall j. j -> Type + data T @k (a :: k) @(j :: Type) (b :: j) + + This feature is guarded behind :extension:`TypeAbstractions`. + Compiler ~~~~~~~~ diff --git a/docs/users_guide/exts/primitives.rst b/docs/users_guide/exts/primitives.rst index 9caab6b146..3db2517c68 100644 --- a/docs/users_guide/exts/primitives.rst +++ b/docs/users_guide/exts/primitives.rst @@ -378,7 +378,7 @@ only required for ``newtype instance`` declarations, such as ``FooKeyBoolC`` and ``BarTypeWorkRepC`` above. This extension impacts the determination of whether or not a newtype has -a Complete User-Specified Kind Signature (CUSK). The exact impact is specified +a Complete User-Supplied Kind (CUSK). The exact impact is specified `the section on CUSKs <#complete-kind-signatures>`__. Unlifted Datatypes diff --git a/docs/users_guide/exts/type_abstractions.rst b/docs/users_guide/exts/type_abstractions.rst index ca8761f405..2e5e8ecab7 100644 --- a/docs/users_guide/exts/type_abstractions.rst +++ b/docs/users_guide/exts/type_abstractions.rst @@ -93,3 +93,99 @@ additional conservative restriction, that type variables occurring in patterns m already be in scope, and so are always new variables that only bind whatever type is matched, rather than ever referring to a variable from an outer scope. Type wildcards ``_`` may be used in any place where no new variable needs binding. + +.. _invisible-binders-in-type-declarations: + +Invisible Binders in Type Declarations +-------------------------------------- + +Syntax +~~~~~~ + +The type abstraction syntax can be used in type declaration headers, including +``type``, ``data``, ``newtype``, ``class``, ``type family``, and ``data family`` +declarations. Here are a few examples:: + + type C :: forall k. k -> Constraint + class C @k a where ... + ^^ + + type D :: forall k j. k -> j -> Type + data D @k @j (a :: k) (b :: j) = ... + ^^ ^^ + + type F :: forall p q. p -> q -> (p, q) + type family F @p @q a b where ... + ^^ ^^ + +Just as ordinary type parameters, invisible type variable binders may have kind +annotations:: + + type F :: forall p q. p -> q -> (p, q) + type family F @(p :: Type) @(q :: Type) (a :: p) (b :: q) where ... + +Scope +~~~~~ + +The ``@k``-binders scope over the body of the declaration and can be used to bring +implicit type or kind variables into scope. Consider:: + + type C :: forall i. (i -> i -> i) -> Constraint + class C @i a where + p :: P a i + +Without the ``@i`` binder in ``C @i a``, the ``i`` in ``P a i`` would no longer +refer to the class variable ``i`` and would be implicitly quantified in the +method signature instead. + +Type checking +~~~~~~~~~~~~~ + +Invisible type variable binders require either a standalone kind signature or a +complete user-supplied kind. + +If a standalone kind signature is given, GHC will match up ``@k``-binders with +the corresponding ``forall k.`` quantifiers in the signature:: + + type B :: forall k. k -> forall j. j -> Type + data B @k (a :: k) @j (b :: j) + ++------------------------------------+ +| Quantifier-binder pairs of ``B`` | ++==============+=====================+ +| ``forall k.``| ``@k`` | ++--------------+---------------------+ +| ``k ->`` | ``(a :: k)`` | ++--------------+---------------------+ +| ``forall j.``| ``@j`` | ++--------------+---------------------+ +| ``j ->`` | ``(b :: j)`` | ++--------------+---------------------+ + +The matching is done left-to-right. Consider:: + + type S :: forall a b. a -> b -> Type + type S @k x y = ... + +In this example, ``@k`` is matched with ``forall a.``, not ``forall b.``: + ++-------------------------------------+ +| Quantifier-binder pairs of ``S`` | ++==============+======================+ +| ``forall a.``| ``@k`` | ++--------------+----------------------+ +| ``forall b.``| | ++--------------+----------------------+ +| ``a ->`` | ``x`` | ++--------------+----------------------+ +| ``b ->`` | ``y`` | ++--------------+----------------------+ + +When a standalone kind signature is absent but the definition has a complete +user-supplied kind (and the :extension:`CUSKs` extension is enabled), +a ``@k``-binder gives rise to a ``forall k.`` quantifier in the inferred kind +signature. The inferred ``forall k.`` does not float to the left; the order of +quantifiers continues to match the order of binders in the header:: + + -- Inferred kind: forall k. k -> forall j. j -> Type + data B @(k :: Type) (a :: k) @(j :: Type) (b :: j)
\ No newline at end of file diff --git a/libraries/ghci/GHCi/TH/Binary.hs b/libraries/ghci/GHCi/TH/Binary.hs index 236229a9df..6d5447e329 100644 --- a/libraries/ghci/GHCi/TH/Binary.hs +++ b/libraries/ghci/GHCi/TH/Binary.hs @@ -27,6 +27,7 @@ instance Binary TH.Info instance Binary TH.Type instance Binary TH.TyLit instance Binary TH.Specificity +instance Binary TH.BndrVis instance Binary flag => Binary (TH.TyVarBndr flag) instance Binary TH.Role instance Binary TH.Lit diff --git a/libraries/template-haskell/Language/Haskell/TH.hs b/libraries/template-haskell/Language/Haskell/TH.hs index ea5df6b1f9..22f434d4e5 100644 --- a/libraries/template-haskell/Language/Haskell/TH.hs +++ b/libraries/template-haskell/Language/Haskell/TH.hs @@ -89,6 +89,7 @@ module Language.Haskell.TH( -- ** Types Type(..), TyVarBndr(..), TyLit(..), Kind, Cxt, Pred, Syntax.Role(..), Syntax.Specificity(..), + Syntax.BndrVis(..), FamilyResultSig(..), Syntax.InjectivityAnn(..), PatSynType, BangType, VarBangType, -- ** Documentation diff --git a/libraries/template-haskell/Language/Haskell/TH/Lib.hs b/libraries/template-haskell/Language/Haskell/TH/Lib.hs index b52de5b0d3..33a60d771d 100644 --- a/libraries/template-haskell/Language/Haskell/TH/Lib.hs +++ b/libraries/template-haskell/Language/Haskell/TH/Lib.hs @@ -24,7 +24,7 @@ module Language.Haskell.TH.Lib ( BangTypeQ, VarBangTypeQ, StrictTypeQ, VarStrictTypeQ, FieldExpQ, PatQ, FieldPatQ, RuleBndrQ, TySynEqnQ, PatSynDirQ, PatSynArgsQ, FamilyResultSigQ, DerivStrategyQ, - TyVarBndrUnit, TyVarBndrSpec, + TyVarBndrUnit, TyVarBndrSpec, TyVarBndrVis, -- ** Constructors lifted to 'Q' -- *** Literals @@ -77,9 +77,12 @@ module Language.Haskell.TH.Lib ( varK, conK, tupleK, arrowK, listK, appK, starK, constraintK, -- *** Type variable binders + DefaultBndrFlag(defaultBndrFlag), plainTV, kindedTV, plainInvisTV, kindedInvisTV, + plainBndrTV, kindedBndrTV, specifiedSpec, inferredSpec, + bndrReq, bndrInvis, -- *** Roles nominalR, representationalR, phantomR, inferR, @@ -192,10 +195,10 @@ import Prelude hiding (Applicative(..)) ------------------------------------------------------------------------------- -- * Dec -tySynD :: Quote m => Name -> [TyVarBndr ()] -> m Type -> m Dec +tySynD :: Quote m => Name -> [TyVarBndr BndrVis] -> m Type -> m Dec tySynD tc tvs rhs = do { rhs1 <- rhs; return (TySynD tc tvs rhs1) } -dataD :: Quote m => m Cxt -> Name -> [TyVarBndr ()] -> Maybe Kind -> [m Con] -> [m DerivClause] +dataD :: Quote m => m Cxt -> Name -> [TyVarBndr BndrVis] -> Maybe Kind -> [m Con] -> [m DerivClause] -> m Dec dataD ctxt tc tvs ksig cons derivs = do @@ -204,7 +207,7 @@ dataD ctxt tc tvs ksig cons derivs = derivs1 <- sequenceA derivs return (DataD ctxt1 tc tvs ksig cons1 derivs1) -newtypeD :: Quote m => m Cxt -> Name -> [TyVarBndr ()] -> Maybe Kind -> m Con -> [m DerivClause] +newtypeD :: Quote m => m Cxt -> Name -> [TyVarBndr BndrVis] -> Maybe Kind -> m Con -> [m DerivClause] -> m Dec newtypeD ctxt tc tvs ksig con derivs = do @@ -213,14 +216,14 @@ newtypeD ctxt tc tvs ksig con derivs = derivs1 <- sequenceA derivs return (NewtypeD ctxt1 tc tvs ksig con1 derivs1) -typeDataD :: Quote m => Name -> [TyVarBndr ()] -> Maybe Kind -> [m Con] +typeDataD :: Quote m => Name -> [TyVarBndr BndrVis] -> Maybe Kind -> [m Con] -> m Dec typeDataD tc tvs ksig cons = do cons1 <- sequenceA cons return (TypeDataD tc tvs ksig cons1) -classD :: Quote m => m Cxt -> Name -> [TyVarBndr ()] -> [FunDep] -> [m Dec] -> m Dec +classD :: Quote m => m Cxt -> Name -> [TyVarBndr BndrVis] -> [FunDep] -> [m Dec] -> m Dec classD ctxt cls tvs fds decs = do decs1 <- sequenceA decs @@ -255,16 +258,16 @@ newtypeInstD ctxt tc tys ksig con derivs = derivs1 <- sequenceA derivs return (NewtypeInstD ctxt1 Nothing ty1 ksig con1 derivs1) -dataFamilyD :: Quote m => Name -> [TyVarBndr ()] -> Maybe Kind -> m Dec +dataFamilyD :: Quote m => Name -> [TyVarBndr BndrVis] -> Maybe Kind -> m Dec dataFamilyD tc tvs kind = pure $ DataFamilyD tc tvs kind -openTypeFamilyD :: Quote m => Name -> [TyVarBndr ()] -> FamilyResultSig +openTypeFamilyD :: Quote m => Name -> [TyVarBndr BndrVis] -> FamilyResultSig -> Maybe InjectivityAnn -> m Dec openTypeFamilyD tc tvs res inj = pure $ OpenTypeFamilyD (TypeFamilyHead tc tvs res inj) -closedTypeFamilyD :: Quote m => Name -> [TyVarBndr ()] -> FamilyResultSig +closedTypeFamilyD :: Quote m => Name -> [TyVarBndr BndrVis] -> FamilyResultSig -> Maybe InjectivityAnn -> [m TySynEqn] -> m Dec closedTypeFamilyD tc tvs result injectivity eqns = do eqns1 <- sequenceA eqns @@ -298,11 +301,23 @@ sigT t k ------------------------------------------------------------------------------- -- * Kind -plainTV :: Name -> TyVarBndr () -plainTV n = PlainTV n () +class DefaultBndrFlag flag where + defaultBndrFlag :: flag -kindedTV :: Name -> Kind -> TyVarBndr () -kindedTV n k = KindedTV n () k +instance DefaultBndrFlag () where + defaultBndrFlag = () + +instance DefaultBndrFlag Specificity where + defaultBndrFlag = SpecifiedSpec + +instance DefaultBndrFlag BndrVis where + defaultBndrFlag = BndrReq + +plainTV :: DefaultBndrFlag flag => Name -> TyVarBndr flag +plainTV n = PlainTV n defaultBndrFlag + +kindedTV :: DefaultBndrFlag flag => Name -> Kind -> TyVarBndr flag +kindedTV n k = KindedTV n defaultBndrFlag k starK :: Kind starK = StarT diff --git a/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs b/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs index 35bca47d25..b066061944 100644 --- a/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs +++ b/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs @@ -79,6 +79,7 @@ type InjectivityAnn = TH.InjectivityAnn type TyVarBndrUnit = TyVarBndr () type TyVarBndrSpec = TyVarBndr Specificity +type TyVarBndrVis = TyVarBndr BndrVis ---------------------------------------------------------- -- * Lowercase pattern syntax functions @@ -412,14 +413,14 @@ funD nm cs = ; pure (FunD nm cs1) } -tySynD :: Quote m => Name -> [m (TyVarBndr ())] -> m Type -> m Dec +tySynD :: Quote m => Name -> [m (TyVarBndr BndrVis)] -> m Type -> m Dec tySynD tc tvs rhs = do { tvs1 <- sequenceA tvs ; rhs1 <- rhs ; pure (TySynD tc tvs1 rhs1) } -dataD :: Quote m => m Cxt -> Name -> [m (TyVarBndr ())] -> Maybe (m Kind) -> [m Con] +dataD :: Quote m => m Cxt -> Name -> [m (TyVarBndr BndrVis)] -> Maybe (m Kind) -> [m Con] -> [m DerivClause] -> m Dec dataD ctxt tc tvs ksig cons derivs = do @@ -430,7 +431,7 @@ dataD ctxt tc tvs ksig cons derivs = derivs1 <- sequenceA derivs pure (DataD ctxt1 tc tvs1 ksig1 cons1 derivs1) -newtypeD :: Quote m => m Cxt -> Name -> [m (TyVarBndr ())] -> Maybe (m Kind) -> m Con +newtypeD :: Quote m => m Cxt -> Name -> [m (TyVarBndr BndrVis)] -> Maybe (m Kind) -> m Con -> [m DerivClause] -> m Dec newtypeD ctxt tc tvs ksig con derivs = do @@ -441,7 +442,7 @@ newtypeD ctxt tc tvs ksig con derivs = derivs1 <- sequenceA derivs pure (NewtypeD ctxt1 tc tvs1 ksig1 con1 derivs1) -typeDataD :: Quote m => Name -> [m (TyVarBndr ())] -> Maybe (m Kind) -> [m Con] +typeDataD :: Quote m => Name -> [m (TyVarBndr BndrVis)] -> Maybe (m Kind) -> [m Con] -> m Dec typeDataD tc tvs ksig cons = do @@ -450,7 +451,7 @@ typeDataD tc tvs ksig cons = cons1 <- sequenceA cons pure (TypeDataD tc tvs1 ksig1 cons1) -classD :: Quote m => m Cxt -> Name -> [m (TyVarBndr ())] -> [FunDep] -> [m Dec] -> m Dec +classD :: Quote m => m Cxt -> Name -> [m (TyVarBndr BndrVis)] -> [FunDep] -> [m Dec] -> m Dec classD ctxt cls tvs fds decs = do tvs1 <- sequenceA tvs @@ -571,20 +572,20 @@ tySynInstD eqn = eqn1 <- eqn pure (TySynInstD eqn1) -dataFamilyD :: Quote m => Name -> [m (TyVarBndr ())] -> Maybe (m Kind) -> m Dec +dataFamilyD :: Quote m => Name -> [m (TyVarBndr BndrVis)] -> Maybe (m Kind) -> m Dec dataFamilyD tc tvs kind = do tvs' <- sequenceA tvs kind' <- sequenceA kind pure $ DataFamilyD tc tvs' kind' -openTypeFamilyD :: Quote m => Name -> [m (TyVarBndr ())] -> m FamilyResultSig +openTypeFamilyD :: Quote m => Name -> [m (TyVarBndr BndrVis)] -> m FamilyResultSig -> Maybe InjectivityAnn -> m Dec openTypeFamilyD tc tvs res inj = do tvs' <- sequenceA tvs res' <- res pure $ OpenTypeFamilyD (TypeFamilyHead tc tvs' res' inj) -closedTypeFamilyD :: Quote m => Name -> [m (TyVarBndr ())] -> m FamilyResultSig +closedTypeFamilyD :: Quote m => Name -> [m (TyVarBndr BndrVis)] -> m FamilyResultSig -> Maybe InjectivityAnn -> [m TySynEqn] -> m Dec closedTypeFamilyD tc tvs result injectivity eqns = do tvs1 <- sequenceA tvs @@ -879,18 +880,30 @@ plainTV n = pure $ PlainTV n () plainInvisTV :: Quote m => Name -> Specificity -> m (TyVarBndr Specificity) plainInvisTV n s = pure $ PlainTV n s +plainBndrTV :: Quote m => Name -> BndrVis -> m (TyVarBndr BndrVis) +plainBndrTV n v = pure $ PlainTV n v + kindedTV :: Quote m => Name -> m Kind -> m (TyVarBndr ()) kindedTV n = fmap (KindedTV n ()) kindedInvisTV :: Quote m => Name -> Specificity -> m Kind -> m (TyVarBndr Specificity) kindedInvisTV n s = fmap (KindedTV n s) +kindedBndrTV :: Quote m => Name -> BndrVis -> m Kind -> m (TyVarBndr BndrVis) +kindedBndrTV n v = fmap (KindedTV n v) + specifiedSpec :: Specificity specifiedSpec = SpecifiedSpec inferredSpec :: Specificity inferredSpec = InferredSpec +bndrReq :: BndrVis +bndrReq = BndrReq + +bndrInvis :: BndrVis +bndrInvis = BndrInvis + varK :: Name -> Kind varK = VarT @@ -1091,7 +1104,7 @@ funD_doc nm cs mfun_doc arg_docs = do Nothing -> funD nm cs -- | Variant of 'dataD' that attaches Haddock documentation. -dataD_doc :: Q Cxt -> Name -> [Q (TyVarBndr ())] -> Maybe (Q Kind) +dataD_doc :: Q Cxt -> Name -> [Q (TyVarBndr BndrVis)] -> Maybe (Q Kind) -> [(Q Con, Maybe String, [Maybe String])] -- ^ List of constructors, documentation for the constructor, and -- documentation for the arguments @@ -1105,7 +1118,7 @@ dataD_doc ctxt tc tvs ksig cons_with_docs derivs mdoc = do maybe dec (flip withDecDoc dec) mdoc -- | Variant of 'newtypeD' that attaches Haddock documentation. -newtypeD_doc :: Q Cxt -> Name -> [Q (TyVarBndr ())] -> Maybe (Q Kind) +newtypeD_doc :: Q Cxt -> Name -> [Q (TyVarBndr BndrVis)] -> Maybe (Q Kind) -> (Q Con, Maybe String, [Maybe String]) -- ^ The constructor, documentation for the constructor, and -- documentation for the arguments @@ -1119,7 +1132,7 @@ newtypeD_doc ctxt tc tvs ksig con_with_docs@(con, _, _) derivs mdoc = do maybe dec (flip withDecDoc dec) mdoc -- | Variant of 'typeDataD' that attaches Haddock documentation. -typeDataD_doc :: Name -> [Q (TyVarBndr ())] -> Maybe (Q Kind) +typeDataD_doc :: Name -> [Q (TyVarBndr BndrVis)] -> Maybe (Q Kind) -> [(Q Con, Maybe String, [Maybe String])] -- ^ List of constructors, documentation for the constructor, and -- documentation for the arguments diff --git a/libraries/template-haskell/Language/Haskell/TH/Ppr.hs b/libraries/template-haskell/Language/Haskell/TH/Ppr.hs index cedb974976..33fbcf8427 100644 --- a/libraries/template-haskell/Language/Haskell/TH/Ppr.hs +++ b/libraries/template-haskell/Language/Haskell/TH/Ppr.hs @@ -947,6 +947,14 @@ instance PprFlag Specificity where pprTyVarBndr (KindedTV nm SpecifiedSpec k) = parens (ppr nm <+> dcolon <+> ppr k) pprTyVarBndr (KindedTV nm InferredSpec k) = braces (ppr nm <+> dcolon <+> ppr k) +instance PprFlag BndrVis where + pprTyVarBndr (PlainTV nm vis) = pprBndrVis vis (ppr nm) + pprTyVarBndr (KindedTV nm vis k) = pprBndrVis vis (parens (ppr nm <+> dcolon <+> ppr k)) + +pprBndrVis :: BndrVis -> Doc -> Doc +pprBndrVis BndrReq d = d +pprBndrVis BndrInvis d = char '@' <> d + instance PprFlag flag => Ppr (TyVarBndr flag) where ppr bndr = pprTyVarBndr bndr diff --git a/libraries/template-haskell/Language/Haskell/TH/Syntax.hs b/libraries/template-haskell/Language/Haskell/TH/Syntax.hs index 0304eb130b..af1ae4f8ab 100644 --- a/libraries/template-haskell/Language/Haskell/TH/Syntax.hs +++ b/libraries/template-haskell/Language/Haskell/TH/Syntax.hs @@ -3,7 +3,8 @@ RankNTypes, RoleAnnotations, ScopedTypeVariables, MagicHash, KindSignatures, PolyKinds, TypeApplications, DataKinds, GADTs, UnboxedTuples, UnboxedSums, TypeOperators, - Trustworthy, DeriveFunctor, BangPatterns, RecordWildCards, ImplicitParams #-} + Trustworthy, DeriveFunctor, DeriveTraversable, + BangPatterns, RecordWildCards, ImplicitParams #-} {-# OPTIONS_GHC -fno-warn-inline-rule-shadowing #-} @@ -2392,22 +2393,22 @@ data Range = FromR Exp | FromThenR Exp Exp data Dec = FunD Name [Clause] -- ^ @{ f p1 p2 = b where decs }@ | ValD Pat Body [Dec] -- ^ @{ p = b where decs }@ - | DataD Cxt Name [TyVarBndr ()] + | DataD Cxt Name [TyVarBndr BndrVis] (Maybe Kind) -- Kind signature (allowed only for GADTs) [Con] [DerivClause] -- ^ @{ data Cxt x => T x = A x | B (T x) -- deriving (Z,W) -- deriving stock Eq }@ - | NewtypeD Cxt Name [TyVarBndr ()] + | NewtypeD Cxt Name [TyVarBndr BndrVis] (Maybe Kind) -- Kind signature Con [DerivClause] -- ^ @{ newtype Cxt x => T x = A (B x) -- deriving (Z,W Q) -- deriving stock Eq }@ - | TypeDataD Name [TyVarBndr ()] + | TypeDataD Name [TyVarBndr BndrVis] (Maybe Kind) -- Kind signature (allowed only for GADTs) [Con] -- ^ @{ type data T x = A x | B (T x) }@ - | TySynD Name [TyVarBndr ()] Type -- ^ @{ type T x = (x,x) }@ - | ClassD Cxt Name [TyVarBndr ()] + | TySynD Name [TyVarBndr BndrVis] Type -- ^ @{ type T x = (x,x) }@ + | ClassD Cxt Name [TyVarBndr BndrVis] [FunDep] [Dec] -- ^ @{ class Eq a => Ord a where ds }@ | InstanceD (Maybe Overlap) Cxt Type [Dec] -- ^ @{ instance {\-\# OVERLAPS \#-\} @@ -2424,7 +2425,7 @@ data Dec | PragmaD Pragma -- ^ @{ {\-\# INLINE [1] foo \#-\} }@ -- | data families (may also appear in [Dec] of 'ClassD' and 'InstanceD') - | DataFamilyD Name [TyVarBndr ()] + | DataFamilyD Name [TyVarBndr BndrVis] (Maybe Kind) -- ^ @{ data family T a b c :: * }@ @@ -2548,7 +2549,7 @@ type PatSynType = Type -- @TypeFamilyHead@ is defined to be the elements of the declaration -- between @type family@ and @where@. data TypeFamilyHead = - TypeFamilyHead Name [TyVarBndr ()] FamilyResultSig (Maybe InjectivityAnn) + TypeFamilyHead Name [TyVarBndr BndrVis] FamilyResultSig (Maybe InjectivityAnn) deriving( Show, Eq, Ord, Data, Generic ) -- | One equation of a type family instance or closed type family. The @@ -2804,9 +2805,19 @@ data Specificity = SpecifiedSpec -- ^ @a@ | InferredSpec -- ^ @{a}@ deriving( Show, Eq, Ord, Data, Generic ) +-- | The @flag@ type parameter is instantiated to one of the following types: +-- +-- * 'Specificity' (examples: 'ForallC', 'ForallT') +-- * 'BndrVis' (examples: 'DataD', 'ClassD', etc.) +-- * '()', a catch-all type for other forms of binders, including 'ForallVisT', 'DataInstD', 'RuleP', and 'TyVarSig' +-- data TyVarBndr flag = PlainTV Name flag -- ^ @a@ | KindedTV Name flag Kind -- ^ @(a :: k)@ - deriving( Show, Eq, Ord, Data, Generic, Functor ) + deriving( Show, Eq, Ord, Data, Generic, Functor, Foldable, Traversable ) + +data BndrVis = BndrReq -- ^ @a@ + | BndrInvis -- ^ @\@a@ + deriving( Show, Eq, Ord, Data, Generic ) -- | Type family result signature data FamilyResultSig = NoSig -- ^ no signature diff --git a/libraries/template-haskell/changelog.md b/libraries/template-haskell/changelog.md index bf63b6e689..90810b27f8 100644 --- a/libraries/template-haskell/changelog.md +++ b/libraries/template-haskell/changelog.md @@ -1,5 +1,14 @@ # Changelog for [`template-haskell` package](http://hackage.haskell.org/package/template-haskell) +## 2.21.0.0 + + * Add `BndrVis` to support invisible binders + in type declarations (GHC Proposal #425). + + * The binder flag type in `plainTV` and `kindedTV` is generalized from `()` + to any data type with a `DefaultBndrFlag` instance, including `()`, + `Specificity`, and `BndrVis`. + ## 2.20.0.0 * The `Ppr.pprInfixT` function has gained a `Precedence` argument. diff --git a/testsuite/tests/dependent/should_compile/T16344b.hs b/testsuite/tests/dependent/should_compile/T16344b.hs index b89304f3b8..1b11c48708 100644 --- a/testsuite/tests/dependent/should_compile/T16344b.hs +++ b/testsuite/tests/dependent/should_compile/T16344b.hs @@ -5,6 +5,6 @@ module T16344 where import Data.Kind -- This one is accepted, even though it is polymorphic-recursive. --- See Note [No polymorphic recursion] in GHC.Tc.Gen.HsType +-- See Note [No polymorphic recursion in type decls] in GHC.Tc.TyCl data T3 ka (a::ka) = forall b. MkT3 (T3 Type b) diff --git a/testsuite/tests/dependent/should_fail/T16344a.hs b/testsuite/tests/dependent/should_fail/T16344a.hs index 989352eb3d..fa75ed9618 100644 --- a/testsuite/tests/dependent/should_fail/T16344a.hs +++ b/testsuite/tests/dependent/should_fail/T16344a.hs @@ -6,6 +6,6 @@ import Data.Kind -- This one is rejected, but in the typechecking phase -- which is a bit nasty. --- See Note [No polymorphic recursion] in GHC.Tc.Gen.HsType +-- See Note [No polymorphic recursion in type decls] in GHC.Tc.TyCl data T2 ka (a::ka) = MkT2 (T2 Type a) diff --git a/testsuite/tests/haddock/should_compile_flag_haddock/T17544.stderr b/testsuite/tests/haddock/should_compile_flag_haddock/T17544.stderr index 484a56ecc0..8712e4e43c 100644 --- a/testsuite/tests/haddock/should_compile_flag_haddock/T17544.stderr +++ b/testsuite/tests/haddock/should_compile_flag_haddock/T17544.stderr @@ -76,7 +76,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { T17544.hs:5:10 }) (Unqual @@ -213,7 +213,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { T17544.hs:9:10 }) (Unqual @@ -348,7 +348,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { T17544.hs:13:10 }) (Unqual @@ -486,7 +486,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { T17544.hs:17:10 }) (Unqual @@ -684,7 +684,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { T17544.hs:22:10 }) (Unqual @@ -722,7 +722,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { T17544.hs:22:28 }) (Unqual @@ -961,7 +961,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { T17544.hs:28:10 }) (Unqual @@ -999,7 +999,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { T17544.hs:28:28 }) (Unqual @@ -1238,7 +1238,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { T17544.hs:34:10 }) (Unqual @@ -1276,7 +1276,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { T17544.hs:34:28 }) (Unqual @@ -1515,7 +1515,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { T17544.hs:40:10 }) (Unqual @@ -1553,7 +1553,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { T17544.hs:40:28 }) (Unqual @@ -1792,7 +1792,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { T17544.hs:46:10 }) (Unqual @@ -1830,7 +1830,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { T17544.hs:46:28 }) (Unqual @@ -2069,7 +2069,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { T17544.hs:52:11 }) (Unqual @@ -2107,7 +2107,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { T17544.hs:52:30 }) (Unqual diff --git a/testsuite/tests/haddock/should_compile_flag_haddock/T17544_kw.stderr b/testsuite/tests/haddock/should_compile_flag_haddock/T17544_kw.stderr index 1efed5e02e..d6f5038cf5 100644 --- a/testsuite/tests/haddock/should_compile_flag_haddock/T17544_kw.stderr +++ b/testsuite/tests/haddock/should_compile_flag_haddock/T17544_kw.stderr @@ -296,7 +296,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { T17544_kw.hs:21:11 }) (Unqual diff --git a/testsuite/tests/indexed-types/should_fail/T9160.hs b/testsuite/tests/indexed-types/should_fail/T9160.hs index cefa18d6f3..fb3a3ba336 100644 --- a/testsuite/tests/indexed-types/should_fail/T9160.hs +++ b/testsuite/tests/indexed-types/should_fail/T9160.hs @@ -7,7 +7,7 @@ $( do { cls_nm <- newName "C" ; a_nm <- newName "a" ; k_nm <- newName "k" ; f_nm <- newName "F" - ; return [ClassD [] cls_nm [KindedTV a_nm () (VarT k_nm)] [] + ; return [ClassD [] cls_nm [KindedTV a_nm BndrReq (VarT k_nm)] [] [OpenTypeFamilyD (TypeFamilyHead f_nm [] (KindSig (VarT k_nm)) Nothing)]]}) diff --git a/testsuite/tests/parser/should_compile/DumpParsedAst.stderr b/testsuite/tests/parser/should_compile/DumpParsedAst.stderr index 677988f0df..588d35efba 100644 --- a/testsuite/tests/parser/should_compile/DumpParsedAst.stderr +++ b/testsuite/tests/parser/should_compile/DumpParsedAst.stderr @@ -399,7 +399,7 @@ ,(AddEpAnn AnnCloseP (EpaSpan { DumpParsedAst.hs:10:30 }))] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { DumpParsedAst.hs:10:21-22 }) (Unqual @@ -491,7 +491,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { DumpParsedAst.hs:15:8 }) (Unqual @@ -508,7 +508,7 @@ ,(AddEpAnn AnnCloseP (EpaSpan { DumpParsedAst.hs:15:17 }))] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { DumpParsedAst.hs:15:11 }) (Unqual @@ -803,7 +803,7 @@ ,(AddEpAnn AnnCloseP (EpaSpan { DumpParsedAst.hs:17:23 }))] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { DumpParsedAst.hs:17:17 }) (Unqual @@ -835,7 +835,7 @@ ,(AddEpAnn AnnCloseP (EpaSpan { DumpParsedAst.hs:17:40 }))] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { DumpParsedAst.hs:17:26 }) (Unqual diff --git a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr index e297ee8b84..31f8d36bb3 100644 --- a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr +++ b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr @@ -306,7 +306,7 @@ ,(AddEpAnn AnnCloseP (EpaSpan { DumpRenamedAst.hs:12:30 }))] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { DumpRenamedAst.hs:12:21-22 }) {Name: as}) @@ -754,7 +754,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { DumpRenamedAst.hs:22:8 }) {Name: f}))) @@ -770,7 +770,7 @@ ,(AddEpAnn AnnCloseP (EpaSpan { DumpRenamedAst.hs:22:17 }))] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { DumpRenamedAst.hs:22:11 }) {Name: a}) @@ -965,7 +965,7 @@ ,(AddEpAnn AnnCloseP (EpaSpan { DumpRenamedAst.hs:24:23 }))] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { DumpRenamedAst.hs:24:17 }) {Name: a}) @@ -989,7 +989,7 @@ ,(AddEpAnn AnnCloseP (EpaSpan { DumpRenamedAst.hs:24:40 }))] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { DumpRenamedAst.hs:24:26 }) {Name: f}) @@ -1075,7 +1075,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { DumpRenamedAst.hs:27:9 }) {Name: a})))]) @@ -1105,7 +1105,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { DumpRenamedAst.hs:28:10 }) {Name: a}))) @@ -1119,7 +1119,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { DumpRenamedAst.hs:28:12 }) {Name: b})))]) diff --git a/testsuite/tests/parser/should_compile/DumpSemis.stderr b/testsuite/tests/parser/should_compile/DumpSemis.stderr index 4e283a73fe..72edeebe9c 100644 --- a/testsuite/tests/parser/should_compile/DumpSemis.stderr +++ b/testsuite/tests/parser/should_compile/DumpSemis.stderr @@ -1079,7 +1079,7 @@ ,(AddEpAnn AnnCloseP (EpaSpan { DumpSemis.hs:28:38 }))] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { DumpSemis.hs:28:24-28 }) (Unqual diff --git a/testsuite/tests/parser/should_compile/KindSigs.stderr b/testsuite/tests/parser/should_compile/KindSigs.stderr index df228cb912..60712f7b3b 100644 --- a/testsuite/tests/parser/should_compile/KindSigs.stderr +++ b/testsuite/tests/parser/should_compile/KindSigs.stderr @@ -177,7 +177,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { KindSigs.hs:11:17 }) (Unqual @@ -226,7 +226,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { KindSigs.hs:15:10 }) (Unqual @@ -412,7 +412,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { KindSigs.hs:16:11 }) (Unqual @@ -1163,7 +1163,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { KindSigs.hs:28:12 }) (Unqual @@ -1513,3 +1513,5 @@ {OccName: True}))))))] (EmptyLocalBinds (NoExtField)))))])))))])) + + diff --git a/testsuite/tests/parser/should_compile/T15323.stderr b/testsuite/tests/parser/should_compile/T15323.stderr index a3bc49d34f..176bab97a2 100644 --- a/testsuite/tests/parser/should_compile/T15323.stderr +++ b/testsuite/tests/parser/should_compile/T15323.stderr @@ -71,7 +71,7 @@ [] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { T15323.hs:5:19 }) (Unqual diff --git a/testsuite/tests/parser/should_compile/T20452.stderr b/testsuite/tests/parser/should_compile/T20452.stderr index f05cef65b8..92260a5df4 100644 --- a/testsuite/tests/parser/should_compile/T20452.stderr +++ b/testsuite/tests/parser/should_compile/T20452.stderr @@ -73,7 +73,7 @@ ,(AddEpAnn AnnCloseP (EpaSpan { T20452.hs:5:21 }))] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { T20452.hs:5:15 }) (Unqual @@ -163,7 +163,7 @@ ,(AddEpAnn AnnCloseP (EpaSpan { T20452.hs:6:22 }))] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { T20452.hs:6:15 }) (Unqual @@ -265,7 +265,7 @@ ,(AddEpAnn AnnCloseP (EpaSpan { T20452.hs:8:26 }))] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { T20452.hs:8:16-18 }) (Unqual @@ -297,7 +297,7 @@ ,(AddEpAnn AnnCloseP (EpaSpan { T20452.hs:8:45 }))] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { T20452.hs:8:31-34 }) (Unqual @@ -329,7 +329,7 @@ ,(AddEpAnn AnnCloseP (EpaSpan { T20452.hs:8:75 }))] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { T20452.hs:8:50-52 }) (Unqual @@ -461,7 +461,7 @@ ,(AddEpAnn AnnCloseP (EpaSpan { T20452.hs:9:27 }))] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { T20452.hs:9:16-18 }) (Unqual @@ -495,7 +495,7 @@ ,(AddEpAnn AnnCloseP (EpaSpan { T20452.hs:9:46 }))] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { T20452.hs:9:31-34 }) (Unqual @@ -529,7 +529,7 @@ ,(AddEpAnn AnnCloseP (EpaSpan { T20452.hs:9:76 }))] (EpaComments [])) - (()) + (HsBndrRequired) (L (SrcSpanAnn (EpAnnNotUsed) { T20452.hs:9:50-52 }) (Unqual diff --git a/testsuite/tests/polykinds/T7022a.hs b/testsuite/tests/polykinds/T7022a.hs index ee71b806c1..62643cba4b 100644 --- a/testsuite/tests/polykinds/T7022a.hs +++ b/testsuite/tests/polykinds/T7022a.hs @@ -9,5 +9,5 @@ makeSList :: Q [Dec] makeSList = do a <- newName "a" k <- newName "k" - return [TySynD (mkName "SList") [KindedTV a () (AppT ListT (VarT k))] + return [TySynD (mkName "SList") [KindedTV a BndrReq (AppT ListT (VarT k))] (AppT (ConT (mkName "Sing")) (VarT a))] diff --git a/testsuite/tests/th/ClosedFam2TH.hs b/testsuite/tests/th/ClosedFam2TH.hs index 43ccf216f8..8786e24aa6 100644 --- a/testsuite/tests/th/ClosedFam2TH.hs +++ b/testsuite/tests/th/ClosedFam2TH.hs @@ -8,8 +8,8 @@ import Language.Haskell.TH $( return [ ClosedTypeFamilyD (TypeFamilyHead (mkName "Equals") - [ KindedTV (mkName "a") () (VarT (mkName "k")) - , KindedTV (mkName "b") () (VarT (mkName "k")) ] + [ KindedTV (mkName "a") BndrReq (VarT (mkName "k")) + , KindedTV (mkName "b") BndrReq (VarT (mkName "k")) ] ( TyVarSig (KindedTV (mkName "r") () (VarT (mkName "k")))) Nothing) [ TySynEqn Nothing @@ -30,7 +30,7 @@ b = False $( return [ ClosedTypeFamilyD (TypeFamilyHead (mkName "Foo") - [ KindedTV (mkName "a") () (VarT (mkName "k"))] + [ KindedTV (mkName "a") BndrReq (VarT (mkName "k"))] (KindSig StarT ) Nothing ) [ TySynEqn Nothing (AppT (AppKindT (ConT (mkName "Foo")) StarT) diff --git a/testsuite/tests/th/T10828.hs b/testsuite/tests/th/T10828.hs index ffb4525f6a..99bc28a777 100644 --- a/testsuite/tests/th/T10828.hs +++ b/testsuite/tests/th/T10828.hs @@ -31,7 +31,7 @@ $( do { decl <- [d| data family D a :: Type -> Type $( return [ DataD [] (mkName "T") - [ PlainTV (mkName "a") () ] + [ PlainTV (mkName "a") BndrReq ] (Just StarT) [ GadtC [(mkName "MkT")] [ ( Bang NoSourceUnpackedness NoSourceStrictness diff --git a/testsuite/tests/th/T10828a.hs b/testsuite/tests/th/T10828a.hs index d66547bad7..85866e5a77 100644 --- a/testsuite/tests/th/T10828a.hs +++ b/testsuite/tests/th/T10828a.hs @@ -8,7 +8,7 @@ import System.IO -- attempting to place a kind signature on a H98 data type $( return [ DataD [] (mkName "T") - [ PlainTV (mkName "a") () ] + [ PlainTV (mkName "a") BndrReq ] (Just StarT) [ NormalC (mkName "MkT") [ ( Bang NoSourceUnpackedness NoSourceStrictness diff --git a/testsuite/tests/th/T10828b.hs b/testsuite/tests/th/T10828b.hs index 03706d6b7c..9dd12d9a06 100644 --- a/testsuite/tests/th/T10828b.hs +++ b/testsuite/tests/th/T10828b.hs @@ -8,7 +8,7 @@ import System.IO -- attempting to mix GADT and normal constructors $( return [ DataD [] (mkName "T") - [ PlainTV (mkName "a") () ] + [ PlainTV (mkName "a") BndrReq ] (Just StarT) [ NormalC (mkName "MkT") diff --git a/testsuite/tests/th/T11345.hs b/testsuite/tests/th/T11345.hs index 2288cdad15..913671e3e0 100644 --- a/testsuite/tests/th/T11345.hs +++ b/testsuite/tests/th/T11345.hs @@ -15,7 +15,7 @@ $(do gadtName <- newName "GADT2" prefixName <- newName "Prefix2" infixName <- newName ":****:" a <- newName "a" - return [ DataD [] gadtName [KindedTV a () StarT] Nothing + return [ DataD [] gadtName [KindedTV a BndrReq StarT] Nothing [ GadtC [prefixName] [ (Bang NoSourceUnpackedness NoSourceStrictness,ConT ''Int) , (Bang NoSourceUnpackedness NoSourceStrictness,ConT ''Int) diff --git a/testsuite/tests/th/T12503.hs b/testsuite/tests/th/T12503.hs index d1e3f27a93..f811763ce2 100644 --- a/testsuite/tests/th/T12503.hs +++ b/testsuite/tests/th/T12503.hs @@ -9,7 +9,7 @@ import Language.Haskell.TH data T1 k class C1 a -$(do TyConI (DataD [] tName [ KindedTV kName () kKind] _ _ _) +$(do TyConI (DataD [] tName [KindedTV kName BndrReq kKind] _ _ _) <- reify ''T1 d <- instanceD (cxt []) (conT ''C1 `appT` diff --git a/testsuite/tests/th/T13098.hs b/testsuite/tests/th/T13098.hs index e6a541cc55..6679d21238 100644 --- a/testsuite/tests/th/T13098.hs +++ b/testsuite/tests/th/T13098.hs @@ -6,7 +6,7 @@ module T13098 where import Language.Haskell.TH -$( sequence [ dataD (cxt []) (mkName "T") [PlainTV (mkName "a") ()] +$( sequence [ dataD (cxt []) (mkName "T") [PlainTV (mkName "a") BndrReq] Nothing [normalC (mkName "T") []] [] , pragCompleteD [mkName "T"] Nothing ] ) diff --git a/testsuite/tests/th/T6018th.hs b/testsuite/tests/th/T6018th.hs index 4fa0eb3716..a75989806e 100644 --- a/testsuite/tests/th/T6018th.hs +++ b/testsuite/tests/th/T6018th.hs @@ -14,7 +14,7 @@ import Language.Haskell.TH $( return [ OpenTypeFamilyD (TypeFamilyHead (mkName "F") - [ PlainTV (mkName "a") (), PlainTV (mkName "b") (), PlainTV (mkName "c") () ] + [ PlainTV (mkName "a") BndrReq, PlainTV (mkName "b") BndrReq, PlainTV (mkName "c") BndrReq ] (TyVarSig (KindedTV (mkName "result") () (VarT (mkName "k")))) (Just $ InjectivityAnn (mkName "result") [(mkName "a"), (mkName "b"), (mkName "c") ])) @@ -41,7 +41,7 @@ $( return $( return [ OpenTypeFamilyD (TypeFamilyHead (mkName "J") - [ PlainTV (mkName "a") (), KindedTV (mkName "b") () (VarT (mkName "k")) ] + [ PlainTV (mkName "a") BndrReq, KindedTV (mkName "b") BndrReq (VarT (mkName "k")) ] (TyVarSig (PlainTV (mkName "r") ())) (Just $ InjectivityAnn (mkName "r") [mkName "a"])) , TySynInstD @@ -60,8 +60,8 @@ $( return $( return [ ClosedTypeFamilyD (TypeFamilyHead (mkName "I") - [ KindedTV (mkName "a") () StarT, KindedTV (mkName "b") () StarT - , KindedTV (mkName "c") () StarT ] + [ KindedTV (mkName "a") BndrReq StarT, KindedTV (mkName "b") BndrReq StarT + , KindedTV (mkName "c") BndrReq StarT ] (TyVarSig (PlainTV (mkName "r") ())) (Just $ InjectivityAnn (mkName "r") [(mkName "a"), (mkName "b")])) @@ -98,7 +98,7 @@ $( do { decl@([ClosedTypeFamilyD (TypeFamilyHead _ _ _ (Just inj)) _]) <- $( return [ OpenTypeFamilyD (TypeFamilyHead (mkName "H") - [ PlainTV (mkName "a") (), PlainTV (mkName "b") (), PlainTV (mkName "c") () ] + [ PlainTV (mkName "a") BndrReq, PlainTV (mkName "b") BndrReq, PlainTV (mkName "c") BndrReq ] (TyVarSig (PlainTV (mkName "r") ())) (Just $ InjectivityAnn (mkName "r") [(mkName "a"), (mkName "b") ])) diff --git a/testsuite/tests/th/T7667.hs b/testsuite/tests/th/T7667.hs index eef6fd2cb0..e2730a3587 100644 --- a/testsuite/tests/th/T7667.hs +++ b/testsuite/tests/th/T7667.hs @@ -4,5 +4,5 @@ module T7667 where import Language.Haskell.TH -$( return [ TySynD (mkName "+") [PlainTV (mkName "a") (), PlainTV (mkName "b") ()] +$( return [ TySynD (mkName "+") [PlainTV (mkName "a") BndrReq, PlainTV (mkName "b") BndrReq] (AppT (AppT (ConT ''Either) (VarT $ mkName "a")) (VarT $ mkName "b")) ] ) diff --git a/testsuite/tests/th/T8499.hs b/testsuite/tests/th/T8499.hs index d9278b4113..fcc70c73b2 100644 --- a/testsuite/tests/th/T8499.hs +++ b/testsuite/tests/th/T8499.hs @@ -8,5 +8,5 @@ import Language.Haskell.TH $( do TyConI (DataD _ _ [KindedTV tvb_a _ _] _ _ _) <- reify ''Maybe my_a <- newName "a" return [TySynD (mkName "SMaybe") - [KindedTV my_a () (AppT (ConT ''Maybe) (VarT tvb_a))] + [KindedTV my_a BndrReq (AppT (ConT ''Maybe) (VarT tvb_a))] (TupleT 0)] ) diff --git a/testsuite/tests/th/TH_RichKinds2.hs b/testsuite/tests/th/TH_RichKinds2.hs index 00387c7b4c..6be859bda8 100644 --- a/testsuite/tests/th/TH_RichKinds2.hs +++ b/testsuite/tests/th/TH_RichKinds2.hs @@ -14,10 +14,10 @@ import Data.List (splitAt, span, elemIndex) import Language.Haskell.TH $(return [OpenTypeFamilyD (TypeFamilyHead - (mkName "Map") [KindedTV (mkName "f") () + (mkName "Map") [KindedTV (mkName "f") BndrReq (AppT (AppT ArrowT (VarT (mkName "k1"))) (VarT (mkName "k2"))), - KindedTV (mkName "l") () + KindedTV (mkName "l") BndrReq (AppT ListT (VarT (mkName "k1")))] (KindSig (AppT ListT (VarT (mkName "k2")))) Nothing)]) diff --git a/testsuite/tests/th/TH_Roles1.hs b/testsuite/tests/th/TH_Roles1.hs index 6ac6128885..83db2d7a80 100644 --- a/testsuite/tests/th/TH_Roles1.hs +++ b/testsuite/tests/th/TH_Roles1.hs @@ -4,6 +4,6 @@ module TH_Roles1 where import Language.Haskell.TH -$( return [ DataD [] (mkName "T") [PlainTV (mkName "a") ()] Nothing [] [] +$( return [ DataD [] (mkName "T") [PlainTV (mkName "a") BndrReq] Nothing [] [] , RoleAnnotD (mkName "T") [RepresentationalR] ] ) diff --git a/testsuite/tests/th/TH_Roles2.hs b/testsuite/tests/th/TH_Roles2.hs index e6a0df0c52..71b9f47c37 100644 --- a/testsuite/tests/th/TH_Roles2.hs +++ b/testsuite/tests/th/TH_Roles2.hs @@ -4,7 +4,7 @@ module TH_Roles2 where import Language.Haskell.TH -$( return [ DataD [] (mkName "T") [KindedTV (mkName "a") () (VarT (mkName "k"))] +$( return [ DataD [] (mkName "T") [KindedTV (mkName "a") BndrReq (VarT (mkName "k"))] Nothing [] [] , RoleAnnotD (mkName "T") [RepresentationalR] ] ) diff --git a/testsuite/tests/th/TH_reifyDecl1.stderr b/testsuite/tests/th/TH_reifyDecl1.stderr index 2c1ee67d88..7bf28179b2 100644 --- a/testsuite/tests/th/TH_reifyDecl1.stderr +++ b/testsuite/tests/th/TH_reifyDecl1.stderr @@ -1,6 +1,9 @@ -data TH_reifyDecl1.T = TH_reifyDecl1.A | TH_reifyDecl1.B +data TH_reifyDecl1.T + = TH_reifyDecl1.A + | TH_reifyDecl1.B data TH_reifyDecl1.R (a_0 :: *) - = TH_reifyDecl1.C a_0 | TH_reifyDecl1.D + = TH_reifyDecl1.C a_0 + | TH_reifyDecl1.D data TH_reifyDecl1.List (a_0 :: *) = TH_reifyDecl1.Nil | TH_reifyDecl1.Cons a_0 (TH_reifyDecl1.List a_0) diff --git a/testsuite/tests/typecheck/should_compile/T22560a.hs b/testsuite/tests/typecheck/should_compile/T22560a.hs new file mode 100644 index 0000000000..3bf71bda67 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T22560a.hs @@ -0,0 +1,39 @@ +{-# LANGUAGE TypeFamilies #-} + +module T22560a where + +import Data.Kind +import Data.Proxy + +-- Invisible binders in type declarations with standalone kind signatures: +-- +-- 1. data +-- 2. newtype +-- 3. type +-- 4. class +-- 5. type family +-- 6. data family +-- +-- Properties that we test: +-- +-- a) the @-binder syntax is accepted in type declaration headers +-- b) the bound variable is in scope in subsequent binders and on the RHS +-- c) the name of the variable in the standalone kind signature and in the +-- type declaration header need not coincide (we use k/j) + +type D :: forall k. k -> Type +data D @j (a :: j) = MkD (Proxy j) (Proxy a) + +type N :: forall k. k -> Type +newtype N @j (a :: j) = MkN (Proxy a -> Proxy j) + +type S :: forall k. k -> Type +type S @j (a :: j) = Proxy a -> Proxy j + +type C :: forall k. k -> Constraint +class C @j (a :: j) where + f :: Proxy a -> Proxy j + +type F :: forall k. k -> k +type family F @j (a :: j) where + F a = a
\ No newline at end of file diff --git a/testsuite/tests/typecheck/should_compile/T22560b.hs b/testsuite/tests/typecheck/should_compile/T22560b.hs new file mode 100644 index 0000000000..dbfb1189eb --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T22560b.hs @@ -0,0 +1,20 @@ +{-# LANGUAGE DataKinds #-} + +module T22560b where + +import Data.Kind + +data P a b = MkP + +type C :: forall i. (i -> i -> i) -> Constraint +class C @i a where + p :: P a i + +p' :: forall i (a :: i -> i -> i). C a => P a i +p' = p + +type T1 :: forall k. Maybe k +type T1 @a = Nothing :: Maybe a + +type T2 :: forall k. Maybe (Maybe k) +type T2 @a = Just (Nothing :: Maybe a)
\ No newline at end of file diff --git a/testsuite/tests/typecheck/should_compile/T22560c.hs b/testsuite/tests/typecheck/should_compile/T22560c.hs new file mode 100644 index 0000000000..3398e207a0 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T22560c.hs @@ -0,0 +1,29 @@ +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE DataKinds #-} + +module T22560c where + +import Data.Kind +import Data.Proxy + +-- Associated type and data families with @-binders +type C :: forall k. k -> Constraint +class C @j (a :: j) where + type F @j a + data D @j a + f :: Proxy a -> F @j a + g :: Proxy a -> D @j a + +-- Instance with an @-binder in F, D +instance C True where + type F @Bool True = () + data D @Bool True = MkTrue + f _ = () + g _ = MkTrue + +-- Instance without an @-binder in F, D +instance C False where + type F False = () + data D False = MkFalse + f _ = () + g _ = MkFalse
\ No newline at end of file diff --git a/testsuite/tests/typecheck/should_compile/T22560d.hs b/testsuite/tests/typecheck/should_compile/T22560d.hs new file mode 100644 index 0000000000..eef8e74806 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T22560d.hs @@ -0,0 +1,33 @@ +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE CUSKs #-} + +module T22560d where + +import Data.Kind +import Data.Proxy + +-- type B :: forall k. k -> forall j. j -> Type +data B @(k :: Type) (a :: k) @(j :: Type) (b :: j) + +-- type D :: forall k. k -> Type +data D @(k :: Type) (a :: k) = MkD (Proxy k) (Proxy a) + +-- type N :: forall k. k -> Type +newtype N @(k :: Type) (a :: k) = MkN (Proxy a -> Proxy k) + +-- type S :: forall k. k -> Type +type S @(k :: Type) (a :: k) = Proxy a -> Proxy k :: Type + +-- type C :: forall k. k -> Constraint +class C @(k :: Type) (a :: k) where + f :: Proxy a -> Proxy k + +-- type F :: forall k. k -> k +type family F @(k :: Type) (a :: k) :: k where + F a = a + +-- type U :: forall k (a :: k). Type +type U @(a :: k) = Int :: Type + +-- type Z :: forall k -> forall (a :: k). Type +type Z (k :: Type) @(a :: k) = Proxy a :: Type
\ No newline at end of file diff --git a/testsuite/tests/typecheck/should_compile/T22560d.script b/testsuite/tests/typecheck/should_compile/T22560d.script new file mode 100644 index 0000000000..e5c67edafb --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T22560d.script @@ -0,0 +1,10 @@ +:load T22560d.hs +:set -fprint-explicit-foralls -XNoStarIsType +:kind B +:kind D +:kind N +:kind S +:kind C +:kind F +:kind U +:kind Z
\ No newline at end of file diff --git a/testsuite/tests/typecheck/should_compile/T22560d.stdout b/testsuite/tests/typecheck/should_compile/T22560d.stdout new file mode 100644 index 0000000000..cb08cfc9e1 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T22560d.stdout @@ -0,0 +1,8 @@ +B :: forall k. k -> forall j. j -> Type +D :: forall k. k -> Type +N :: forall k. k -> Type +S :: forall k. k -> Type +C :: forall k. k -> Constraint +F :: forall k. k -> k +U :: forall k (a :: k). Type +Z :: forall k -> forall (a :: k). Type diff --git a/testsuite/tests/typecheck/should_compile/T22560e.hs b/testsuite/tests/typecheck/should_compile/T22560e.hs new file mode 100644 index 0000000000..0b97632b9e --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T22560e.hs @@ -0,0 +1,9 @@ +module T22560e where + +import Data.Kind +import Data.Proxy + +type X = forall k. k -> Type + +type Y :: X +type Y @k (a :: k) = Proxy a
\ No newline at end of file diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 07d39cebd3..09b0951047 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -857,3 +857,8 @@ test('T22647', normal, compile, ['']) test('T19577', normal, compile, ['']) test('T22383', normal, compile, ['']) test('T21501', normal, compile, ['']) +test('T22560a', normal, compile, ['']) +test('T22560b', normal, compile, ['']) +test('T22560c', normal, compile, ['']) +test('T22560d', extra_files(['T22560d.hs']), ghci_script, ['T22560d.script']) +test('T22560e', normal, compile, ['']) diff --git a/testsuite/tests/typecheck/should_fail/T22560_fail_a.hs b/testsuite/tests/typecheck/should_fail/T22560_fail_a.hs new file mode 100644 index 0000000000..e30a2f8391 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T22560_fail_a.hs @@ -0,0 +1,7 @@ +module T22560_fail_a where + +import Data.Kind (Type) + +-- NB: the inferred forall is always skipped +type P :: forall {k}. k -> Type +data P @k a = MkP k
\ No newline at end of file diff --git a/testsuite/tests/typecheck/should_fail/T22560_fail_a.stderr b/testsuite/tests/typecheck/should_fail/T22560_fail_a.stderr new file mode 100644 index 0000000000..7b929d8104 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T22560_fail_a.stderr @@ -0,0 +1,8 @@ + +T22560_fail_a.hs:7:1: error: [GHC-57916] + • Invalid invisible type variable binder: @k + There is no matching forall-bound variable + in the standalone kind signature for ‘P’. + NB. Only ‘forall a.’ -quantification matches invisible binders, + whereas ‘forall {a}.’ and ‘forall a ->’ do not. + • In the data type declaration for ‘P’ diff --git a/testsuite/tests/typecheck/should_fail/T22560_fail_b.hs b/testsuite/tests/typecheck/should_fail/T22560_fail_b.hs new file mode 100644 index 0000000000..8d824c9996 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T22560_fail_b.hs @@ -0,0 +1,6 @@ +module T22560_fail_b where + +import Data.Kind (Type) + +type P :: forall a -> Type +data P @a = MkP
\ No newline at end of file diff --git a/testsuite/tests/typecheck/should_fail/T22560_fail_b.stderr b/testsuite/tests/typecheck/should_fail/T22560_fail_b.stderr new file mode 100644 index 0000000000..9693cac827 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T22560_fail_b.stderr @@ -0,0 +1,8 @@ + +T22560_fail_b.hs:6:1: error: [GHC-57916] + • Invalid invisible type variable binder: @a + There is no matching forall-bound variable + in the standalone kind signature for ‘P’. + NB. Only ‘forall a.’ -quantification matches invisible binders, + whereas ‘forall {a}.’ and ‘forall a ->’ do not. + • In the data type declaration for ‘P’ diff --git a/testsuite/tests/typecheck/should_fail/T22560_fail_c.hs b/testsuite/tests/typecheck/should_fail/T22560_fail_c.hs new file mode 100644 index 0000000000..1d111c7162 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T22560_fail_c.hs @@ -0,0 +1,6 @@ +module T22560_fail_c where + +import Data.Kind + +type Dup :: forall k j. k -> Type +data Dup @k @k (a :: k)
\ No newline at end of file diff --git a/testsuite/tests/typecheck/should_fail/T22560_fail_c.stderr b/testsuite/tests/typecheck/should_fail/T22560_fail_c.stderr new file mode 100644 index 0000000000..115c70cc5a --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T22560_fail_c.stderr @@ -0,0 +1,5 @@ + +T22560_fail_c.hs:6:11: error: + Conflicting definitions for ‘k’ + Bound at: T22560_fail_c.hs:6:11 + T22560_fail_c.hs:6:14 diff --git a/testsuite/tests/typecheck/should_fail/T22560_fail_d.hs b/testsuite/tests/typecheck/should_fail/T22560_fail_d.hs new file mode 100644 index 0000000000..65fc4282d2 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T22560_fail_d.hs @@ -0,0 +1,5 @@ +module T22560_fail_d where + +import Data.Kind + +data T @k (a :: k) -- No CUSK, no SAKS
\ No newline at end of file diff --git a/testsuite/tests/typecheck/should_fail/T22560_fail_d.stderr b/testsuite/tests/typecheck/should_fail/T22560_fail_d.stderr new file mode 100644 index 0000000000..b59036c29e --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T22560_fail_d.stderr @@ -0,0 +1,8 @@ + +T22560_fail_d.hs:5:1: error: [GHC-92337] + • Invalid invisible type variable binder: @k + Either a standalone kind signature (SAKS) + or a complete user-supplied kind (CUSK, legacy feature) + is required to use invisible binders. + • In the data type declaration for ‘T’ + Suggested fix: Add a standalone kind signature for ‘T’ diff --git a/testsuite/tests/typecheck/should_fail/T22560_fail_ext.hs b/testsuite/tests/typecheck/should_fail/T22560_fail_ext.hs new file mode 100644 index 0000000000..f301767a98 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T22560_fail_ext.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE NoTypeAbstractions #-} + +module T22560_fail_ext where + +import Data.Kind + +data T @k (a :: k) @(j :: Type) (b :: j)
\ No newline at end of file diff --git a/testsuite/tests/typecheck/should_fail/T22560_fail_ext.stderr b/testsuite/tests/typecheck/should_fail/T22560_fail_ext.stderr new file mode 100644 index 0000000000..890c356d4e --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T22560_fail_ext.stderr @@ -0,0 +1,8 @@ + +T22560_fail_ext.hs:7:1: error: [GHC-58589] + Illegal invisible type variable binder: @(j :: Type) + Suggested fix: Perhaps you intended to use TypeAbstractions + +T22560_fail_ext.hs:7:1: error: [GHC-58589] + Illegal invisible type variable binder: @k + Suggested fix: Perhaps you intended to use TypeAbstractions diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T index a7e9f6a678..c0ba90e673 100644 --- a/testsuite/tests/typecheck/should_fail/all.T +++ b/testsuite/tests/typecheck/should_fail/all.T @@ -667,3 +667,8 @@ test('T22570', normal, compile_fail, ['']) test('T22645', normal, compile_fail, ['']) test('T20666', normal, compile_fail, ['']) test('T20666a', normal, compile_fail, ['']) +test('T22560_fail_a', normal, compile_fail, ['']) +test('T22560_fail_b', normal, compile_fail, ['']) +test('T22560_fail_c', normal, compile_fail, ['']) +test('T22560_fail_d', normal, compile_fail, ['']) +test('T22560_fail_ext', normal, compile_fail, ['']) diff --git a/utils/check-exact/ExactPrint.hs b/utils/check-exact/ExactPrint.hs index a569b803d4..0dfca9ec1a 100644 --- a/utils/check-exact/ExactPrint.hs +++ b/utils/check-exact/ExactPrint.hs @@ -3756,6 +3756,16 @@ instance ExactPrintTVFlag Specificity where SpecifiedSpec -> (AnnOpenP, AnnCloseP) InferredSpec -> (AnnOpenC, AnnCloseC) +instance ExactPrintTVFlag (HsBndrVis GhcPs) where + exactTVDelimiters an0 bvis thing_inside = do + case bvis of + HsBndrRequired -> return () + HsBndrInvisible at -> markToken at >> return () + an1 <- markEpAnnAllL an0 lid AnnOpenP + r <- thing_inside + an2 <- markEpAnnAllL an1 lid AnnCloseP + return (an2, r) + instance ExactPrintTVFlag flag => ExactPrint (HsTyVarBndr flag GhcPs) where getAnnotationEntry (UserTyVar an _ _) = fromAnn an getAnnotationEntry (KindedTyVar an _ _ _) = fromAnn an diff --git a/utils/haddock b/utils/haddock -Subproject 519a95998b09a2c9c7a42c3a0cf2ca0c4358bb4 +Subproject 4f66a44a10fca90834c27a2afdcf3b5b494af86 |