diff options
Diffstat (limited to 'compiler')
29 files changed, 1359 insertions, 379 deletions
diff --git a/compiler/GHC/Hs/Decls.hs b/compiler/GHC/Hs/Decls.hs index 701c8b1a06..c43a27cef2 100644 --- a/compiler/GHC/Hs/Decls.hs +++ b/compiler/GHC/Hs/Decls.hs @@ -20,18 +20,20 @@ module GHC.Hs.Decls ( -- * Toplevel declarations HsDecl(..), LHsDecl, HsDataDefn(..), HsDeriving, LHsFunDep, HsDerivingClause(..), LHsDerivingClause, NewOrData(..), newOrDataToFlavour, + StandaloneKindSig(..), LStandaloneKindSig, standaloneKindSigName, -- ** Class or type declarations TyClDecl(..), LTyClDecl, DataDeclRn(..), TyClGroup(..), tyClGroupTyClDecls, tyClGroupInstDecls, tyClGroupRoleDecls, + tyClGroupKindSigs, isClassDecl, isDataDecl, isSynDecl, tcdName, isFamilyDecl, isTypeFamilyDecl, isDataFamilyDecl, isOpenTypeFamilyInfo, isClosedTypeFamilyInfo, tyFamInstDeclName, tyFamInstDeclLName, countTyClDecls, pprTyClDeclFlavour, tyClDeclLName, tyClDeclTyVars, - hsDeclHasCusk, famDeclHasCusk, + hsDeclHasCusk, famResultKindSignature, FamilyDecl(..), LFamilyDecl, -- ** Instance declarations @@ -136,6 +138,7 @@ data HsDecl p | DerivD (XDerivD p) (DerivDecl p) -- ^ Deriving declaration | ValD (XValD p) (HsBind p) -- ^ Value declaration | SigD (XSigD p) (Sig p) -- ^ Signature declaration + | KindSigD (XKindSigD p) (StandaloneKindSig p) -- ^ Standalone kind signature | DefD (XDefD p) (DefaultDecl p) -- ^ 'default' declaration | ForD (XForD p) (ForeignDecl p) -- ^ Foreign declaration | WarningD (XWarningD p) (WarnDecls p) -- ^ Warning declaration @@ -152,6 +155,7 @@ type instance XInstD (GhcPass _) = NoExtField type instance XDerivD (GhcPass _) = NoExtField type instance XValD (GhcPass _) = NoExtField type instance XSigD (GhcPass _) = NoExtField +type instance XKindSigD (GhcPass _) = NoExtField type instance XDefD (GhcPass _) = NoExtField type instance XForD (GhcPass _) = NoExtField type instance XWarningD (GhcPass _) = NoExtField @@ -278,6 +282,7 @@ instance (p ~ GhcPass pass, OutputableBndrId p) => Outputable (HsDecl p) where ppr (DerivD _ deriv) = ppr deriv ppr (ForD _ fd) = ppr fd ppr (SigD _ sd) = ppr sd + ppr (KindSigD _ ksd) = ppr ksd ppr (RuleD _ rd) = ppr rd ppr (WarningD _ wd) = ppr wd ppr (AnnD _ ad) = ppr ad @@ -304,6 +309,7 @@ instance (p ~ GhcPass pass, OutputableBndrId p) => Outputable (HsGroup p) where then Nothing else Just (ppr val_decls), ppr_ds (tyClGroupRoleDecls tycl_decls), + ppr_ds (tyClGroupKindSigs tycl_decls), ppr_ds (tyClGroupTyClDecls tycl_decls), ppr_ds (tyClGroupInstDecls tycl_decls), ppr_ds deriv_decls, @@ -658,7 +664,7 @@ tyClDeclLName :: TyClDecl pass -> Located (IdP pass) tyClDeclLName (FamDecl { tcdFam = FamilyDecl { fdLName = ln } }) = ln tyClDeclLName decl = tcdLName decl -tcdName :: TyClDecl pass -> (IdP pass) +tcdName :: TyClDecl pass -> IdP pass tcdName = unLoc . tyClDeclLName tyClDeclTyVars :: TyClDecl pass -> LHsQTyVars pass @@ -682,25 +688,21 @@ countTyClDecls decls -- | Does this declaration have a complete, user-supplied kind signature? -- See Note [CUSKs: complete user-supplied kind signatures] -hsDeclHasCusk - :: Bool -- True <=> the -XCUSKs extension is enabled - -> TyClDecl GhcRn - -> Bool -hsDeclHasCusk _cusks_enabled@False _ = False -hsDeclHasCusk cusks_enabled (FamDecl { tcdFam = fam_decl }) - = famDeclHasCusk cusks_enabled False fam_decl - -- False: this is not: an associated type of a class with no cusk -hsDeclHasCusk _cusks_enabled@True (SynDecl { tcdTyVars = tyvars, tcdRhs = rhs }) - -- NB: Keep this synchronized with 'getInitialKind' - = hsTvbAllKinded tyvars && rhs_annotated rhs - where - rhs_annotated (L _ ty) = case ty of - HsParTy _ lty -> rhs_annotated lty - HsKindSig {} -> True - _ -> False -hsDeclHasCusk _cusks_enabled@True (DataDecl { tcdDExt = DataDeclRn { tcdDataCusk = cusk }}) = cusk -hsDeclHasCusk _cusks_enabled@True (ClassDecl { tcdTyVars = tyvars }) = hsTvbAllKinded tyvars -hsDeclHasCusk _ (XTyClDecl nec) = noExtCon nec +hsDeclHasCusk :: TyClDecl GhcRn -> Bool +hsDeclHasCusk (FamDecl { tcdFam = + FamilyDecl { fdInfo = fam_info + , fdTyVars = tyvars + , fdResultSig = L _ resultSig } }) = + case fam_info of + ClosedTypeFamily {} -> hsTvbAllKinded tyvars + && isJust (famResultKindSignature resultSig) + _ -> True -- Un-associated open type/data families have CUSKs +hsDeclHasCusk (SynDecl { tcdTyVars = tyvars, tcdRhs = rhs }) + = hsTvbAllKinded tyvars && isJust (hsTyKindSig rhs) +hsDeclHasCusk (DataDecl { tcdDExt = DataDeclRn { tcdDataCusk = cusk }}) = cusk +hsDeclHasCusk (ClassDecl { tcdTyVars = tyvars }) = hsTvbAllKinded tyvars +hsDeclHasCusk (FamDecl { tcdFam = XFamilyDecl nec }) = noExtCon nec +hsDeclHasCusk (XTyClDecl nec) = noExtCon nec -- Pretty-printing TyClDecl -- ~~~~~~~~~~~~~~~~~~~~~~~~ @@ -742,10 +744,13 @@ instance (p ~ GhcPass pass, OutputableBndrId p) => Outputable (TyClGroup p) where ppr (TyClGroup { group_tyclds = tyclds , group_roles = roles + , group_kisigs = kisigs , group_instds = instds } ) - = ppr tyclds $$ + = hang (text "TyClGroup") 2 $ + ppr kisigs $$ + ppr tyclds $$ ppr roles $$ ppr instds ppr (XTyClGroup x) = ppr x @@ -777,8 +782,8 @@ pprTyClDeclFlavour (ClassDecl {}) = text "class" pprTyClDeclFlavour (SynDecl {}) = text "type" pprTyClDeclFlavour (FamDecl { tcdFam = FamilyDecl { fdInfo = info }}) = pprFlavour info <+> text "family" -pprTyClDeclFlavour (FamDecl { tcdFam = XFamilyDecl x}) - = ppr x +pprTyClDeclFlavour (FamDecl { tcdFam = XFamilyDecl nec }) + = noExtCon nec pprTyClDeclFlavour (DataDecl { tcdDataDefn = HsDataDefn { dd_ND = nd } }) = ppr nd pprTyClDeclFlavour (DataDecl { tcdDataDefn = XHsDataDefn x }) @@ -910,6 +915,7 @@ data TyClGroup pass -- See Note [TyClGroups and dependency analysis] = TyClGroup { group_ext :: XCTyClGroup pass , group_tyclds :: [LTyClDecl pass] , group_roles :: [LRoleAnnotDecl pass] + , group_kisigs :: [LStandaloneKindSig pass] , group_instds :: [LInstDecl pass] } | XTyClGroup (XXTyClGroup pass) @@ -926,6 +932,8 @@ tyClGroupInstDecls = concatMap group_instds tyClGroupRoleDecls :: [TyClGroup pass] -> [LRoleAnnotDecl pass] tyClGroupRoleDecls = concatMap group_roles +tyClGroupKindSigs :: [TyClGroup pass] -> [LStandaloneKindSig pass] +tyClGroupKindSigs = concatMap group_kisigs {- ********************************************************************* @@ -1024,6 +1032,7 @@ data FamilyResultSig pass = -- see Note [FamilyResultSig] type instance XNoSig (GhcPass _) = NoExtField type instance XCKindSig (GhcPass _) = NoExtField + type instance XTyVarSig (GhcPass _) = NoExtField type instance XXFamilyResultSig (GhcPass _) = NoExtCon @@ -1081,32 +1090,15 @@ data FamilyInfo pass -- said "type family Foo x where .." | ClosedTypeFamily (Maybe [LTyFamInstEqn pass]) --- | Does this family declaration have a complete, user-supplied kind signature? --- See Note [CUSKs: complete user-supplied kind signatures] -famDeclHasCusk :: Bool -- ^ True <=> the -XCUSKs extension is enabled - -> Bool -- ^ True <=> this is an associated type family, - -- and the parent class has /no/ CUSK - -> FamilyDecl (GhcPass pass) - -> Bool -famDeclHasCusk _cusks_enabled@False _ _ = False -famDeclHasCusk _cusks_enabled@True assoc_with_no_cusk - (FamilyDecl { fdInfo = fam_info - , fdTyVars = tyvars - , fdResultSig = L _ resultSig }) - = case fam_info of - ClosedTypeFamily {} -> hsTvbAllKinded tyvars - && hasReturnKindSignature resultSig - _ -> not assoc_with_no_cusk - -- Un-associated open type/data families have CUSKs - -- Associated type families have CUSKs iff the parent class does - -famDeclHasCusk _ _ (XFamilyDecl nec) = noExtCon nec - --- | Does this family declaration have user-supplied return kind signature? -hasReturnKindSignature :: FamilyResultSig a -> Bool -hasReturnKindSignature (NoSig _) = False -hasReturnKindSignature (TyVarSig _ (L _ (UserTyVar{}))) = False -hasReturnKindSignature _ = True +famResultKindSignature :: FamilyResultSig (GhcPass p) -> Maybe (LHsKind (GhcPass p)) +famResultKindSignature (NoSig _) = Nothing +famResultKindSignature (KindSig _ ki) = Just ki +famResultKindSignature (TyVarSig _ bndr) = + case unLoc bndr of + UserTyVar _ _ -> Nothing + KindedTyVar _ _ ki -> Just ki + XTyVarBndr nec -> noExtCon nec +famResultKindSignature (XFamilyResultSig nec) = noExtCon nec -- | Maybe return name of the result type variable resultVariableName :: FamilyResultSig (GhcPass a) -> Maybe (IdP (GhcPass a)) @@ -1137,7 +1129,7 @@ pprFamilyDecl top_level (FamilyDecl { fdInfo = info, fdLName = ltycon NoSig _ -> empty KindSig _ kind -> dcolon <+> ppr kind TyVarSig _ tv_bndr -> text "=" <+> ppr tv_bndr - XFamilyResultSig x -> ppr x + XFamilyResultSig nec -> noExtCon nec pp_inj = case mb_inj of Just (L _ (InjectivityAnn lhs rhs)) -> hsep [ vbar, ppr lhs, text "->", hsep (map ppr rhs) ] @@ -1149,7 +1141,7 @@ pprFamilyDecl top_level (FamilyDecl { fdInfo = info, fdLName = ltycon Nothing -> text ".." Just eqns -> vcat $ map (ppr_fam_inst_eqn . unLoc) eqns ) _ -> (empty, empty) -pprFamilyDecl _ (XFamilyDecl x) = ppr x +pprFamilyDecl _ (XFamilyDecl nec) = noExtCon nec pprFlavour :: FamilyInfo pass -> SDoc pprFlavour DataFamily = text "data" @@ -1203,6 +1195,7 @@ data HsDataDefn pass -- The payload of a data type defn | XHsDataDefn (XXHsDataDefn pass) type instance XCHsDataDefn (GhcPass _) = NoExtField + type instance XXHsDataDefn (GhcPass _) = NoExtCon -- | Haskell Deriving clause @@ -1269,6 +1262,37 @@ instance (p ~ GhcPass pass, OutputableBndrId p) _ -> (ppDerivStrategy dcs, empty) ppr (XHsDerivingClause x) = ppr x +-- | Located Standalone Kind Signature +type LStandaloneKindSig pass = Located (StandaloneKindSig pass) + +data StandaloneKindSig pass + = StandaloneKindSig (XStandaloneKindSig pass) + (Located (IdP pass)) -- Why a single binder? See #16754 + (LHsSigType pass) -- Why not LHsSigWcType? See Note [Wildcards in standalone kind signatures] + | XStandaloneKindSig (XXStandaloneKindSig pass) + +type instance XStandaloneKindSig (GhcPass p) = NoExtField +type instance XXStandaloneKindSig (GhcPass p) = NoExtCon + +standaloneKindSigName :: StandaloneKindSig (GhcPass p) -> IdP (GhcPass p) +standaloneKindSigName (StandaloneKindSig _ lname _) = unLoc lname +standaloneKindSigName (XStandaloneKindSig nec) = noExtCon nec + +{- Note [Wildcards in standalone kind signatures] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Standalone kind signatures enable polymorphic recursion, and it is unclear how +to reconcile this with partial type signatures, so we disallow wildcards in +them. + +We reject wildcards in 'rnStandaloneKindSignature' by returning False for +'StandaloneKindSigCtx' in 'wildCardsAllowed'. + +The alternative design is to have special treatment for partial standalone kind +signatures, much like we have special treatment for partial type signatures in +terms. However, partial standalone kind signatures are not a proper replacement +for CUSKs, so this would be a separate feature. +-} + data NewOrData = NewType -- ^ @newtype Blah ...@ | DataType -- ^ @data Blah ...@ @@ -1279,6 +1303,7 @@ newOrDataToFlavour :: NewOrData -> TyConFlavour newOrDataToFlavour NewType = NewtypeFlavour newOrDataToFlavour DataType = DataTypeFlavour + -- | Located data Constructor Declaration type LConDecl pass = Located (ConDecl pass) -- ^ May have 'ApiAnnotation.AnnKeywordId' : 'ApiAnnotation.AnnSemi' when @@ -1443,6 +1468,11 @@ instance (p ~ GhcPass pass, OutputableBndrId p) => Outputable (HsDataDefn p) where ppr d = pp_data_defn (\_ -> text "Naked HsDataDefn") d +instance (p ~ GhcPass pass, OutputableBndrId p) + => Outputable (StandaloneKindSig p) where + ppr (StandaloneKindSig _ v ki) = text "type" <+> ppr v <+> text "::" <+> ppr ki + ppr (XStandaloneKindSig nec) = noExtCon nec + instance Outputable NewOrData where ppr NewType = text "newtype" ppr DataType = text "data" diff --git a/compiler/GHC/Hs/Extension.hs b/compiler/GHC/Hs/Extension.hs index f360e1c32e..35afc5f8d3 100644 --- a/compiler/GHC/Hs/Extension.hs +++ b/compiler/GHC/Hs/Extension.hs @@ -280,6 +280,10 @@ type ForallXFixitySig (c :: * -> Constraint) (x :: *) = , c (XXFixitySig x) ) +-- StandaloneKindSig type families +type family XStandaloneKindSig x +type family XXStandaloneKindSig x + -- ===================================================================== -- Type families for the HsDecls extension points @@ -289,6 +293,7 @@ type family XInstD x type family XDerivD x type family XValD x type family XSigD x +type family XKindSigD x type family XDefD x type family XForD x type family XWarningD x @@ -305,6 +310,7 @@ type ForallXHsDecl (c :: * -> Constraint) (x :: *) = , c (XDerivD x) , c (XValD x) , c (XSigD x) + , c (XKindSigD x) , c (XDefD x) , c (XForD x) , c (XWarningD x) diff --git a/compiler/GHC/Hs/Instances.hs b/compiler/GHC/Hs/Instances.hs index d55e20c2e7..b3a33df43c 100644 --- a/compiler/GHC/Hs/Instances.hs +++ b/compiler/GHC/Hs/Instances.hs @@ -86,6 +86,11 @@ deriving instance Data (FixitySig GhcPs) deriving instance Data (FixitySig GhcRn) deriving instance Data (FixitySig GhcTc) +-- deriving instance (DataId p) => Data (StandaloneKindSig p) +deriving instance Data (StandaloneKindSig GhcPs) +deriving instance Data (StandaloneKindSig GhcRn) +deriving instance Data (StandaloneKindSig GhcTc) + -- deriving instance (DataIdLR p p) => Data (HsPatSynDir p) deriving instance Data (HsPatSynDir GhcPs) deriving instance Data (HsPatSynDir GhcRn) diff --git a/compiler/GHC/Hs/Types.hs b/compiler/GHC/Hs/Types.hs index f14d59ba4a..04fd1ee8e6 100644 --- a/compiler/GHC/Hs/Types.hs +++ b/compiler/GHC/Hs/Types.hs @@ -62,6 +62,7 @@ module GHC.Hs.Types ( mkHsOpTy, mkHsAppTy, mkHsAppTys, mkHsAppKindTy, ignoreParens, hsSigType, hsSigWcType, hsLTyVarBndrToType, hsLTyVarBndrsToTypes, + hsTyKindSig, hsConDetailsArgs, -- Printing @@ -79,7 +80,7 @@ import {-# SOURCE #-} GHC.Hs.Expr ( HsSplice, pprSplice ) import GHC.Hs.Extension import Id ( Id ) -import Name( Name ) +import Name( Name, NamedThing(getName) ) import RdrName ( RdrName ) import DataCon( HsSrcBang(..), HsImplBang(..), SrcStrictness(..), SrcUnpackedness(..) ) @@ -505,6 +506,7 @@ data HsTyVarBndr pass type instance XUserTyVar (GhcPass _) = NoExtField type instance XKindedTyVar (GhcPass _) = NoExtField + type instance XXTyVarBndr (GhcPass _) = NoExtCon -- | Does this 'HsTyVarBndr' come with an explicit kind annotation? @@ -517,6 +519,11 @@ isHsKindedTyVar (XTyVarBndr {}) = False hsTvbAllKinded :: LHsQTyVars pass -> Bool hsTvbAllKinded = all (isHsKindedTyVar . unLoc) . hsQTvExplicit +instance NamedThing (HsTyVarBndr GhcRn) where + getName (UserTyVar _ v) = unLoc v + getName (KindedTyVar _ v _) = unLoc v + getName (XTyVarBndr nec) = noExtCon nec + -- | Haskell Type data HsType pass = HsForAllTy -- See Note [HsType binders] @@ -1076,6 +1083,24 @@ hsLTyVarBndrsToTypes :: LHsQTyVars (GhcPass p) -> [LHsType (GhcPass p)] hsLTyVarBndrsToTypes (HsQTvs { hsq_explicit = tvbs }) = map hsLTyVarBndrToType tvbs hsLTyVarBndrsToTypes (XLHsQTyVars nec) = noExtCon nec +-- | Get the kind signature of a type, ignoring parentheses: +-- +-- hsTyKindSig `Maybe ` = Nothing +-- hsTyKindSig `Maybe :: Type -> Type ` = Just `Type -> Type` +-- hsTyKindSig `Maybe :: ((Type -> Type))` = Just `Type -> Type` +-- +-- This is used to extract the result kind of type synonyms with a CUSK: +-- +-- type S = (F :: res_kind) +-- ^^^^^^^^ +-- +hsTyKindSig :: LHsType pass -> Maybe (LHsKind pass) +hsTyKindSig lty = + case unLoc lty of + HsParTy _ lty' -> hsTyKindSig lty' + HsKindSig _ _ k -> Just k + _ -> Nothing + --------------------- ignoreParens :: LHsType pass -> LHsType pass ignoreParens (L _ (HsParTy _ ty)) = ignoreParens ty @@ -1449,7 +1474,7 @@ instance (p ~ GhcPass pass, OutputableBndrId p) => Outputable (HsTyVarBndr p) where ppr (UserTyVar _ n) = ppr n ppr (KindedTyVar _ n k) = parens $ hsep [ppr n, dcolon, ppr k] - ppr (XTyVarBndr n) = ppr n + ppr (XTyVarBndr nec) = noExtCon nec instance (p ~ GhcPass pass,Outputable thing) => Outputable (HsImplicitBndrs p thing) where diff --git a/compiler/GHC/ThToHs.hs b/compiler/GHC/ThToHs.hs index ca38d07ddc..f49d6ff0b2 100644 --- a/compiler/GHC/ThToHs.hs +++ b/compiler/GHC/ThToHs.hs @@ -180,6 +180,12 @@ cvtDec (TH.SigD nm typ) ; returnJustL $ Hs.SigD noExtField (TypeSig noExtField [nm'] (mkLHsSigWcType ty')) } +cvtDec (TH.KiSigD nm ki) + = do { nm' <- tconNameL nm + ; ki' <- cvtType ki + ; let sig' = StandaloneKindSig noExtField nm' (mkLHsSigType ki') + ; returnJustL $ Hs.KindSigD noExtField sig' } + cvtDec (TH.InfixD fx nm) -- Fixity signatures are allowed for variables, constructors, and types -- the renamer automatically looks for types during renaming, even when diff --git a/compiler/basicTypes/NameEnv.hs b/compiler/basicTypes/NameEnv.hs index 5f6bdc5846..03c2150102 100644 --- a/compiler/basicTypes/NameEnv.hs +++ b/compiler/basicTypes/NameEnv.hs @@ -11,7 +11,7 @@ module NameEnv ( NameEnv, -- ** Manipulating these environments - mkNameEnv, + mkNameEnv, mkNameEnvWith, emptyNameEnv, isEmptyNameEnv, unitNameEnv, nameEnvElts, extendNameEnv_C, extendNameEnv_Acc, extendNameEnv, @@ -92,6 +92,7 @@ type NameEnv a = UniqFM a -- Domain is Name emptyNameEnv :: NameEnv a isEmptyNameEnv :: NameEnv a -> Bool mkNameEnv :: [(Name,a)] -> NameEnv a +mkNameEnvWith :: (a -> Name) -> [a] -> NameEnv a nameEnvElts :: NameEnv a -> [a] alterNameEnv :: (Maybe a-> Maybe a) -> NameEnv a -> Name -> NameEnv a extendNameEnv_C :: (a->a->a) -> NameEnv a -> Name -> a -> NameEnv a @@ -121,6 +122,7 @@ extendNameEnvList x l = addListToUFM x l lookupNameEnv x y = lookupUFM x y alterNameEnv = alterUFM mkNameEnv l = listToUFM l +mkNameEnvWith f = mkNameEnv . map (\a -> (f a, a)) elemNameEnv x y = elemUFM x y plusNameEnv x y = plusUFM x y plusNameEnv_C f x y = plusUFM_C f x y diff --git a/compiler/deSugar/DsMeta.hs b/compiler/deSugar/DsMeta.hs index c37d366d5e..7baa748faa 100644 --- a/compiler/deSugar/DsMeta.hs +++ b/compiler/deSugar/DsMeta.hs @@ -140,6 +140,7 @@ repTopDs group@(HsGroup { hs_valds = valds ; _ <- mapM no_splice splcds ; tycl_ds <- mapM repTyClD (tyClGroupTyClDecls tyclds) ; role_ds <- mapM repRoleD (concatMap group_roles tyclds) + ; kisig_ds <- mapM repKiSigD (concatMap group_kisigs tyclds) ; inst_ds <- mapM repInstD instds ; deriv_ds <- mapM repStandaloneDerivD derivds ; fix_ds <- mapM repFixD fixds @@ -155,6 +156,7 @@ repTopDs group@(HsGroup { hs_valds = valds -- more needed ; return (de_loc $ sort_by_loc $ val_ds ++ catMaybes tycl_ds ++ role_ds + ++ kisig_ds ++ (concat fix_ds) ++ inst_ds ++ rule_ds ++ for_ds ++ ann_ds ++ deriv_ds) }) ; @@ -348,6 +350,13 @@ repRoleD (dL->L loc (RoleAnnotDecl _ tycon roles)) repRoleD _ = panic "repRoleD" ------------------------- +repKiSigD :: LStandaloneKindSig GhcRn -> DsM (SrcSpan, Core TH.DecQ) +repKiSigD (dL->L loc kisig) = + case kisig of + StandaloneKindSig _ v ki -> rep_ty_sig kiSigDName loc ki v + XStandaloneKindSig nec -> noExtCon nec + +------------------------- repDataDefn :: Core TH.Name -> Either (Core [TH.TyVarBndrQ]) -- the repTyClD case @@ -870,7 +879,7 @@ rep_ty_sig :: Name -> SrcSpan -> LHsSigType GhcRn -> Located Name -- and Note [Don't quantify implicit type variables in quotes] rep_ty_sig mk_sig loc sig_ty nm | HsIB { hsib_body = hs_ty } <- sig_ty - , (explicit_tvs, ctxt, ty) <- splitLHsSigmaTy hs_ty + , (explicit_tvs, ctxt, ty) <- splitLHsSigmaTyInvis hs_ty = do { nm1 <- lookupLOcc nm ; let rep_in_scope_tv tv = do { name <- lookupBinder (hsLTyVarName tv) ; repTyVarBndrWithKind tv name } diff --git a/compiler/hieFile/HieAst.hs b/compiler/hieFile/HieAst.hs index a1253de735..52f8c59a4d 100644 --- a/compiler/hieFile/HieAst.hs +++ b/compiler/hieFile/HieAst.hs @@ -1254,8 +1254,13 @@ instance ( a ~ GhcPass p XCmd _ -> [] instance ToHie (TyClGroup GhcRn) where - toHie (TyClGroup _ classes roles instances) = concatM + toHie TyClGroup{ group_tyclds = classes + , group_roles = roles + , group_kisigs = sigs + , group_instds = instances } = + concatM [ toHie classes + , toHie sigs , toHie roles , toHie instances ] @@ -1466,6 +1471,17 @@ instance ( HasLoc thing where span = loc a toHie (TS _ (XHsWildCardBndrs _)) = pure [] +instance ToHie (LStandaloneKindSig GhcRn) where + toHie (L sp sig) = concatM [makeNode sig sp, toHie sig] + +instance ToHie (StandaloneKindSig GhcRn) where + toHie sig = concatM $ case sig of + StandaloneKindSig _ name typ -> + [ toHie $ C TyDecl name + , toHie $ TS (ResolvedScopes []) typ + ] + XStandaloneKindSig _ -> [] + instance ToHie (SigContext (LSig GhcRn)) where toHie (SC (SI styp msp) (L sp sig)) = concatM $ makeNode sig sp : case sig of TypeSig _ names typ -> diff --git a/compiler/iface/IfaceSyn.hs b/compiler/iface/IfaceSyn.hs index 688998f96d..f86ca458d7 100644 --- a/compiler/iface/IfaceSyn.hs +++ b/compiler/iface/IfaceSyn.hs @@ -69,6 +69,7 @@ import TyCon ( Role (..), Injectivity(..), tyConBndrVisArgFlag ) import Util( dropList, filterByList, notNull, unzipWith ) import DataCon (SrcStrictness(..), SrcUnpackedness(..)) import Lexeme (isLexSym) +import TysWiredIn ( constraintKindTyConName ) import Control.Monad import System.IO.Unsafe @@ -730,6 +731,14 @@ pprClassRoles ss clas binders roles = binders roles +pprClassStandaloneKindSig :: ShowSub -> IfaceTopBndr -> IfaceKind -> SDoc +pprClassStandaloneKindSig ss clas = + pprStandaloneKindSig (pprPrefixIfDeclBndr (ss_how_much ss) (occName clas)) + +constraintIfaceKind :: IfaceKind +constraintIfaceKind = + IfaceTyConApp (IfaceTyCon constraintKindTyConName (IfaceTyConInfo NotPromoted IfaceNormalTyCon)) IA_Nil + pprIfaceDecl :: ShowSub -> IfaceDecl -> SDoc -- NB: pprIfaceDecl is also used for pretty-printing TyThings in GHCi -- See Note [Pretty-printing TyThings] in PprTyThing @@ -741,10 +750,12 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype, ifBinders = binders }) | gadt = vcat [ pp_roles + , pp_ki_sig , pp_nd <+> pp_lhs <+> pp_kind <+> pp_where , nest 2 (vcat pp_cons) , nest 2 $ ppShowIface ss pp_extra ] | otherwise = vcat [ pp_roles + , pp_ki_sig , hang (pp_nd <+> pp_lhs) 2 (add_bars pp_cons) , nest 2 $ ppShowIface ss pp_extra ] where @@ -759,26 +770,45 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype, cons = visibleIfConDecls condecls pp_where = ppWhen (gadt && not (null cons)) $ text "where" pp_cons = ppr_trim (map show_con cons) :: [SDoc] - pp_kind - | isIfaceLiftedTypeKind kind = empty - | otherwise = dcolon <+> ppr kind + pp_kind = ppUnless (if ki_sig_printable + then isIfaceTauType kind + -- Even in the presence of a standalone kind signature, a non-tau + -- result kind annotation cannot be discarded as it determines the arity. + -- See Note [Arity inference in kcDeclHeader_sig] in TcHsType + else isIfaceLiftedTypeKind kind) + (dcolon <+> ppr kind) pp_lhs = case parent of - IfNoParent -> pprIfaceDeclHead context ss tycon binders Nothing + IfNoParent -> pprIfaceDeclHead suppress_bndr_sig context ss tycon binders IfDataInstance{} -> text "instance" <+> pp_data_inst_forall <+> pprIfaceTyConParent parent pp_roles | is_data_instance = empty - | otherwise = pprRoles (== Representational) - (pprPrefixIfDeclBndr - (ss_how_much ss) - (occName tycon)) - binders roles + | otherwise = pprRoles (== Representational) name_doc binders roles -- Don't display roles for data family instances (yet) -- See discussion on #8672. + ki_sig_printable = + -- If we print a standalone kind signature for a data instance, we leak + -- the internal constructor name: + -- + -- type T15827.R:Dka :: forall k. k -> * + -- data instance forall k (a :: k). D a = MkD (Proxy a) + -- + -- This T15827.R:Dka is a compiler-generated type constructor for the + -- data instance. + not is_data_instance + + pp_ki_sig = ppWhen ki_sig_printable $ + pprStandaloneKindSig name_doc (mkIfaceTyConKind binders kind) + + -- See Note [Suppressing binder signatures] in IfaceType + suppress_bndr_sig = SuppressBndrSig ki_sig_printable + + name_doc = pprPrefixIfDeclBndr (ss_how_much ss) (occName tycon) + add_bars [] = Outputable.empty add_bars (c:cs) = sep ((equals <+> c) : map (vbar <+>) cs) @@ -801,8 +831,11 @@ pprIfaceDecl ss (IfaceClass { ifName = clas , ifBinders = binders , ifBody = IfAbstractClass }) = vcat [ pprClassRoles ss clas binders roles - , text "class" <+> pprIfaceDeclHead [] ss clas binders Nothing - <+> pprFundeps fds ] + , pprClassStandaloneKindSig ss clas (mkIfaceTyConKind binders constraintIfaceKind) + , text "class" <+> pprIfaceDeclHead suppress_bndr_sig [] ss clas binders <+> pprFundeps fds ] + where + -- See Note [Suppressing binder signatures] in IfaceType + suppress_bndr_sig = SuppressBndrSig True pprIfaceDecl ss (IfaceClass { ifName = clas , ifRoles = roles @@ -815,8 +848,8 @@ pprIfaceDecl ss (IfaceClass { ifName = clas ifMinDef = minDef }}) = vcat [ pprClassRoles ss clas binders roles - , text "class" <+> pprIfaceDeclHead context ss clas binders Nothing - <+> pprFundeps fds <+> pp_where + , pprClassStandaloneKindSig ss clas (mkIfaceTyConKind binders constraintIfaceKind) + , text "class" <+> pprIfaceDeclHead suppress_bndr_sig context ss clas binders <+> pprFundeps fds <+> pp_where , nest 2 (vcat [ vcat asocs, vcat dsigs , ppShowAllSubs ss (pprMinDef minDef)])] where @@ -842,31 +875,46 @@ pprIfaceDecl ss (IfaceClass { ifName = clas (\_ def -> cparen (isLexSym def) (ppr def)) 0 minDef <+> text "#-}" + -- See Note [Suppressing binder signatures] in IfaceType + suppress_bndr_sig = SuppressBndrSig True + pprIfaceDecl ss (IfaceSynonym { ifName = tc , ifBinders = binders , ifSynRhs = mono_ty , ifResKind = res_kind}) - = hang (text "type" <+> pprIfaceDeclHead [] ss tc binders Nothing <+> equals) - 2 (sep [ pprIfaceForAll tvs, pprIfaceContextArr theta, ppr tau - , ppUnless (isIfaceLiftedTypeKind res_kind) (dcolon <+> ppr res_kind) ]) + = vcat [ pprStandaloneKindSig name_doc (mkIfaceTyConKind binders res_kind) + , hang (text "type" <+> pprIfaceDeclHead suppress_bndr_sig [] ss tc binders <+> equals) + 2 (sep [ pprIfaceForAll tvs, pprIfaceContextArr theta, ppr tau + , ppUnless (isIfaceLiftedTypeKind res_kind) (dcolon <+> ppr res_kind) ]) + ] where (tvs, theta, tau) = splitIfaceSigmaTy mono_ty + name_doc = pprPrefixIfDeclBndr (ss_how_much ss) (occName tc) + + -- See Note [Suppressing binder signatures] in IfaceType + suppress_bndr_sig = SuppressBndrSig True pprIfaceDecl ss (IfaceFamily { ifName = tycon , ifFamFlav = rhs, ifBinders = binders , ifResKind = res_kind , ifResVar = res_var, ifFamInj = inj }) | IfaceDataFamilyTyCon <- rhs - = text "data family" <+> pprIfaceDeclHead [] ss tycon binders Nothing + = vcat [ pprStandaloneKindSig name_doc (mkIfaceTyConKind binders res_kind) + , text "data family" <+> pprIfaceDeclHead suppress_bndr_sig [] ss tycon binders + ] | otherwise - = hang (text "type family" - <+> pprIfaceDeclHead [] ss tycon binders (Just res_kind) - <+> ppShowRhs ss (pp_where rhs)) - 2 (pp_inj res_var inj <+> ppShowRhs ss (pp_rhs rhs)) - $$ - nest 2 (ppShowRhs ss (pp_branches rhs)) + = vcat [ pprStandaloneKindSig name_doc (mkIfaceTyConKind binders res_kind) + , hang (text "type family" + <+> pprIfaceDeclHead suppress_bndr_sig [] ss tycon binders + <+> ppShowRhs ss (pp_where rhs)) + 2 (pp_inj res_var inj <+> ppShowRhs ss (pp_rhs rhs)) + $$ + nest 2 (ppShowRhs ss (pp_branches rhs)) + ] where + name_doc = pprPrefixIfDeclBndr (ss_how_much ss) (occName tycon) + pp_where (IfaceClosedSynFamilyTyCon {}) = text "where" pp_where _ = empty @@ -900,6 +948,9 @@ pprIfaceDecl ss (IfaceFamily { ifName = tycon $$ ppShowIface ss (text "axiom" <+> ppr ax) pp_branches _ = Outputable.empty + -- See Note [Suppressing binder signatures] in IfaceType + suppress_bndr_sig = SuppressBndrSig True + pprIfaceDecl _ (IfacePatSyn { ifName = name, ifPatUnivBndrs = univ_bndrs, ifPatExBndrs = ex_bndrs, ifPatProvCtxt = prov_ctxt, ifPatReqCtxt = req_ctxt, @@ -948,6 +999,9 @@ pprRoles suppress_if tyCon bndrs roles in ppUnless (all suppress_if froles || null froles) $ text "type role" <+> tyCon <+> hsep (map ppr froles) +pprStandaloneKindSig :: SDoc -> IfaceType -> SDoc +pprStandaloneKindSig tyCon ty = text "type" <+> tyCon <+> text "::" <+> ppr ty + pprInfixIfDeclBndr :: ShowHowMuch -> OccName -> SDoc pprInfixIfDeclBndr (ShowSome _ (AltPpr (Just ppr_bndr))) name = pprInfixVar (isSymOcc name) (ppr_bndr name) @@ -998,16 +1052,16 @@ pprIfaceTyConParent IfNoParent pprIfaceTyConParent (IfDataInstance _ tc tys) = pprIfaceTypeApp topPrec tc tys -pprIfaceDeclHead :: IfaceContext -> ShowSub -> Name +pprIfaceDeclHead :: SuppressBndrSig + -> IfaceContext -> ShowSub -> Name -> [IfaceTyConBinder] -- of the tycon, for invisible-suppression - -> Maybe IfaceKind -> SDoc -pprIfaceDeclHead context ss tc_occ bndrs m_res_kind +pprIfaceDeclHead suppress_sig context ss tc_occ bndrs = sdocWithDynFlags $ \ dflags -> sep [ pprIfaceContextArr context , pprPrefixIfDeclBndr (ss_how_much ss) (occName tc_occ) - <+> pprIfaceTyConBinders (suppressIfaceInvisibles dflags bndrs bndrs) - , maybe empty (\res_kind -> dcolon <+> pprIfaceType res_kind) m_res_kind ] + <+> pprIfaceTyConBinders suppress_sig + (suppressIfaceInvisibles dflags bndrs bndrs) ] pprIfaceConDecl :: ShowSub -> Bool -> IfaceTopBndr diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs index 9e7021bcc9..e3362b7a68 100644 --- a/compiler/iface/IfaceType.hs +++ b/compiler/iface/IfaceType.hs @@ -24,6 +24,7 @@ module IfaceType ( IfaceForAllBndr, ArgFlag(..), AnonArgFlag(..), ForallVisFlag(..), ShowForAllFlag(..), mkIfaceForAllTvBndr, + mkIfaceTyConKind, ifForAllBndrVar, ifForAllBndrName, ifaceBndrName, ifTyConBinderVar, ifTyConBinderName, @@ -35,6 +36,8 @@ module IfaceType ( appArgsIfaceTypes, appArgsIfaceTypesArgFlags, -- Printing + SuppressBndrSig(..), + UseBndrParens(..), pprIfaceType, pprParendIfaceType, pprPrecIfaceType, pprIfaceContext, pprIfaceContextArr, pprIfaceIdBndr, pprIfaceLamBndr, pprIfaceTvBndr, pprIfaceTyConBinders, @@ -44,6 +47,7 @@ module IfaceType ( pprIfaceCoercion, pprParendIfaceCoercion, splitIfaceSigmaTy, pprIfaceTypeApp, pprUserIfaceForAll, pprIfaceCoTcApp, pprTyTcApp, pprIfacePrefixApp, + isIfaceTauType, suppressIfaceInvisibles, stripIfaceInvisVars, @@ -106,6 +110,10 @@ ifaceBndrName :: IfaceBndr -> IfLclName ifaceBndrName (IfaceTvBndr bndr) = ifaceTvBndrName bndr ifaceBndrName (IfaceIdBndr bndr) = ifaceIdBndrName bndr +ifaceBndrType :: IfaceBndr -> IfaceType +ifaceBndrType (IfaceIdBndr (_, t)) = t +ifaceBndrType (IfaceTvBndr (_, t)) = t + type IfaceLamBndr = (IfaceBndr, IfaceOneShot) data IfaceOneShot -- See Note [Preserve OneShotInfo] in CoreTicy @@ -164,6 +172,15 @@ type IfaceForAllBndr = VarBndr IfaceBndr ArgFlag mkIfaceForAllTvBndr :: ArgFlag -> IfaceTvBndr -> IfaceForAllBndr mkIfaceForAllTvBndr vis var = Bndr (IfaceTvBndr var) vis +-- | Build the 'tyConKind' from the binders and the result kind. +-- Keep in sync with 'mkTyConKind' in types/TyCon. +mkIfaceTyConKind :: [IfaceTyConBinder] -> IfaceKind -> IfaceKind +mkIfaceTyConKind bndrs res_kind = foldr mk res_kind bndrs + where + mk :: IfaceTyConBinder -> IfaceKind -> IfaceKind + mk (Bndr tv (AnonTCB af)) k = IfaceFunTy af (ifaceBndrType tv) k + mk (Bndr tv (NamedTCB vis)) k = IfaceForAllTy (Bndr tv vis) k + -- | Stores the arguments in a type application as a list. -- See @Note [Suppressing invisible arguments]@. data IfaceAppArgs @@ -686,11 +703,17 @@ pprIfacePrefixApp ctxt_prec pp_fun pp_tys | otherwise = maybeParen ctxt_prec appPrec $ hang pp_fun 2 (sep pp_tys) +isIfaceTauType :: IfaceType -> Bool +isIfaceTauType (IfaceForAllTy _ _) = False +isIfaceTauType (IfaceFunTy InvisArg _ _) = False +isIfaceTauType _ = True + -- ----------------------------- Printing binders ------------------------------------ instance Outputable IfaceBndr where ppr (IfaceIdBndr bndr) = pprIfaceIdBndr bndr - ppr (IfaceTvBndr bndr) = char '@' <+> pprIfaceTvBndr False bndr + ppr (IfaceTvBndr bndr) = char '@' <+> pprIfaceTvBndr bndr (SuppressBndrSig False) + (UseBndrParens False) pprIfaceBndrs :: [IfaceBndr] -> SDoc pprIfaceBndrs bs = sep (map ppr bs) @@ -702,31 +725,60 @@ pprIfaceLamBndr (b, IfaceOneShot) = ppr b <> text "[OneShot]" pprIfaceIdBndr :: IfaceIdBndr -> SDoc pprIfaceIdBndr (name, ty) = parens (ppr name <+> dcolon <+> ppr ty) -pprIfaceTvBndr :: Bool -> IfaceTvBndr -> SDoc -pprIfaceTvBndr use_parens (tv, ki) +{- Note [Suppressing binder signatures] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When printing the binders in a 'forall', we want to keep the kind annotations: + + forall (a :: k). blah + ^^^^ + good + +On the other hand, when we print the binders of a data declaration in :info, +the kind information would be redundant due to the standalone kind signature: + + type F :: Symbol -> Type + type F (s :: Symbol) = blah + ^^^^^^^^^ + redundant + +Here we'd like to omit the kind annotation: + + type F :: Symbol -> Type + type F s = blah +-} + +-- | Do we want to suppress kind annotations on binders? +-- See Note [Suppressing binder signatures] +newtype SuppressBndrSig = SuppressBndrSig Bool + +newtype UseBndrParens = UseBndrParens Bool + +pprIfaceTvBndr :: IfaceTvBndr -> SuppressBndrSig -> UseBndrParens -> SDoc +pprIfaceTvBndr (tv, ki) (SuppressBndrSig suppress_sig) (UseBndrParens use_parens) + | suppress_sig = ppr tv | isIfaceLiftedTypeKind ki = ppr tv | otherwise = maybe_parens (ppr tv <+> dcolon <+> ppr ki) where maybe_parens | use_parens = parens | otherwise = id -pprIfaceTyConBinders :: [IfaceTyConBinder] -> SDoc -pprIfaceTyConBinders = sep . map go +pprIfaceTyConBinders :: SuppressBndrSig -> [IfaceTyConBinder] -> SDoc +pprIfaceTyConBinders suppress_sig = sep . map go where go :: IfaceTyConBinder -> SDoc go (Bndr (IfaceIdBndr bndr) _) = pprIfaceIdBndr bndr go (Bndr (IfaceTvBndr bndr) vis) = -- See Note [Pretty-printing invisible arguments] case vis of - AnonTCB VisArg -> ppr_bndr True - AnonTCB InvisArg -> char '@' <> braces (ppr_bndr False) + AnonTCB VisArg -> ppr_bndr (UseBndrParens True) + AnonTCB InvisArg -> char '@' <> braces (ppr_bndr (UseBndrParens False)) -- The above case is rare. (See Note [AnonTCB InvisArg] in TyCon.) -- Should we print these differently? - NamedTCB Required -> ppr_bndr True - NamedTCB Specified -> char '@' <> ppr_bndr True - NamedTCB Inferred -> char '@' <> braces (ppr_bndr False) + NamedTCB Required -> ppr_bndr (UseBndrParens True) + NamedTCB Specified -> char '@' <> ppr_bndr (UseBndrParens True) + NamedTCB Inferred -> char '@' <> braces (ppr_bndr (UseBndrParens False)) where - ppr_bndr use_parens = pprIfaceTvBndr use_parens bndr + ppr_bndr = pprIfaceTvBndr bndr suppress_sig instance Binary IfaceBndr where put_ bh (IfaceIdBndr aa) = do @@ -1045,13 +1097,19 @@ pprIfaceForAllCoBndrs :: [(IfLclName, IfaceCoercion)] -> SDoc pprIfaceForAllCoBndrs bndrs = hsep $ map pprIfaceForAllCoBndr bndrs pprIfaceForAllBndr :: IfaceForAllBndr -> SDoc -pprIfaceForAllBndr (Bndr (IfaceTvBndr tv) Inferred) - = sdocWithDynFlags $ \dflags -> - if gopt Opt_PrintExplicitForalls dflags - then braces $ pprIfaceTvBndr False tv - else pprIfaceTvBndr True tv -pprIfaceForAllBndr (Bndr (IfaceTvBndr tv) _) = pprIfaceTvBndr True tv -pprIfaceForAllBndr (Bndr (IfaceIdBndr idv) _) = pprIfaceIdBndr idv +pprIfaceForAllBndr bndr = + case bndr of + Bndr (IfaceTvBndr tv) Inferred -> + sdocWithDynFlags $ \dflags -> + if gopt Opt_PrintExplicitForalls dflags + then braces $ pprIfaceTvBndr tv suppress_sig (UseBndrParens False) + else pprIfaceTvBndr tv suppress_sig (UseBndrParens True) + Bndr (IfaceTvBndr tv) _ -> + pprIfaceTvBndr tv suppress_sig (UseBndrParens True) + Bndr (IfaceIdBndr idv) _ -> pprIfaceIdBndr idv + where + -- See Note [Suppressing binder signatures] in IfaceType + suppress_sig = SuppressBndrSig False pprIfaceForAllCoBndr :: (IfLclName, IfaceCoercion) -> SDoc pprIfaceForAllCoBndr (tv, kind_co) diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs index 02499d2f74..07b266d24b 100644 --- a/compiler/main/DynFlags.hs +++ b/compiler/main/DynFlags.hs @@ -4526,6 +4526,7 @@ xFlagsDeps = [ flagSpec' "TemplateHaskell" LangExt.TemplateHaskell checkTemplateHaskellOk, flagSpec "TemplateHaskellQuotes" LangExt.TemplateHaskellQuotes, + flagSpec "StandaloneKindSignatures" LangExt.StandaloneKindSignatures, flagSpec "TraditionalRecordSyntax" LangExt.TraditionalRecordSyntax, flagSpec "TransformListComp" LangExt.TransformListComp, flagSpec "TupleSections" LangExt.TupleSections, @@ -4653,6 +4654,9 @@ impliedXFlags , (LangExt.TypeInType, turnOn, LangExt.PolyKinds) , (LangExt.TypeInType, turnOn, LangExt.KindSignatures) + -- Standalone kind signatures are a replacement for CUSKs. + , (LangExt.StandaloneKindSignatures, turnOff, LangExt.CUSKs) + -- AutoDeriveTypeable is not very useful without DeriveDataTypeable , (LangExt.AutoDeriveTypeable, turnOn, LangExt.DeriveDataTypeable) diff --git a/compiler/parser/Parser.y b/compiler/parser/Parser.y index 276fcb1c5b..f32ce4a5e0 100644 --- a/compiler/parser/Parser.y +++ b/compiler/parser/Parser.y @@ -1049,6 +1049,7 @@ topdecls_semi :: { OrdList (LHsDecl GhcPs) } topdecl :: { LHsDecl GhcPs } : cl_decl { sL1 $1 (TyClD noExtField (unLoc $1)) } | ty_decl { sL1 $1 (TyClD noExtField (unLoc $1)) } + | standalone_kind_sig { sL1 $1 (KindSigD noExtField (unLoc $1)) } | inst_decl { sL1 $1 (InstD noExtField (unLoc $1)) } | stand_alone_deriving { sLL $1 $> (DerivD noExtField (unLoc $1)) } | role_annot { sL1 $1 (RoleAnnotD noExtField (unLoc $1)) } @@ -1131,6 +1132,19 @@ ty_decl :: { LTyClDecl GhcPs } (snd $ unLoc $4) Nothing) (mj AnnData $1:mj AnnFamily $2:(fst $ unLoc $4)) } +-- standalone kind signature +standalone_kind_sig :: { LStandaloneKindSig GhcPs } + : 'type' sks_vars '::' ktypedoc + {% amms (mkStandaloneKindSig (comb2 $1 $4) $2 $4) + [mj AnnType $1,mu AnnDcolon $3] } + +-- See also: sig_vars +sks_vars :: { Located [Located RdrName] } -- Returned in reverse order + : sks_vars ',' oqtycon + {% addAnnotation (gl $ head $ unLoc $1) AnnComma (gl $2) >> + return (sLL $1 $> ($3 : unLoc $1)) } + | oqtycon { sL1 $1 [$1] } + inst_decl :: { LInstDecl GhcPs } : 'instance' overlap_pragma inst_type where_inst {% do { (binds, sigs, _, ats, adts, _) <- cvBindsAndSigs (snd $ unLoc $4) diff --git a/compiler/parser/RdrHsSyn.hs b/compiler/parser/RdrHsSyn.hs index 538c20cc8a..0686f669d3 100644 --- a/compiler/parser/RdrHsSyn.hs +++ b/compiler/parser/RdrHsSyn.hs @@ -23,6 +23,7 @@ module RdrHsSyn ( mkClassDecl, mkTyData, mkDataFamInst, mkTySynonym, mkTyFamInstEqn, + mkStandaloneKindSig, mkTyFamInst, mkFamDecl, mkLHsSigType, mkInlinePragma, @@ -239,6 +240,30 @@ mkTySynonym loc lhs rhs , tcdFixity = fixity , tcdRhs = rhs })) } +mkStandaloneKindSig + :: SrcSpan + -> Located [Located RdrName] -- LHS + -> LHsKind GhcPs -- RHS + -> P (LStandaloneKindSig GhcPs) +mkStandaloneKindSig loc lhs rhs = + do { vs <- mapM check_lhs_name (unLoc lhs) + ; v <- check_singular_lhs (reverse vs) + ; return $ cL loc $ StandaloneKindSig noExtField v (mkLHsSigType rhs) } + where + check_lhs_name v@(unLoc->name) = + if isUnqual name && isTcOcc (rdrNameOcc name) + then return v + else addFatalError (getLoc v) $ + hang (text "Expected an unqualified type constructor:") 2 (ppr v) + check_singular_lhs vs = + case vs of + [] -> panic "mkStandaloneKindSig: empty left-hand side" + [v] -> return v + _ -> addFatalError (getLoc lhs) $ + vcat [ hang (text "Standalone kind signatures do not support multiple names at the moment:") + 2 (pprWithCommas ppr vs) + , text "See https://gitlab.haskell.org/ghc/ghc/issues/16754 for details." ] + mkTyFamInstEqn :: Maybe [LHsTyVarBndr GhcPs] -> LHsType GhcPs -> LHsType GhcPs diff --git a/compiler/prelude/THNames.hs b/compiler/prelude/THNames.hs index 58f9af770d..0eedeeee9c 100644 --- a/compiler/prelude/THNames.hs +++ b/compiler/prelude/THNames.hs @@ -68,7 +68,7 @@ templateHaskellNames = [ -- Dec funDName, valDName, dataDName, newtypeDName, tySynDName, classDName, instanceWithOverlapDName, - standaloneDerivWithStrategyDName, sigDName, forImpDName, + standaloneDerivWithStrategyDName, sigDName, kiSigDName, forImpDName, pragInlDName, pragSpecDName, pragSpecInlDName, pragSpecInstDName, pragRuleDName, pragCompleteDName, pragAnnDName, defaultSigDName, dataFamilyDName, openTypeFamilyDName, closedTypeFamilyDName, @@ -341,7 +341,7 @@ recSName = libFun (fsLit "recS") recSIdKey -- data Dec = ... funDName, valDName, dataDName, newtypeDName, tySynDName, classDName, - instanceWithOverlapDName, sigDName, forImpDName, pragInlDName, + instanceWithOverlapDName, sigDName, kiSigDName, forImpDName, pragInlDName, pragSpecDName, pragSpecInlDName, pragSpecInstDName, pragRuleDName, pragAnnDName, standaloneDerivWithStrategyDName, defaultSigDName, dataInstDName, newtypeInstDName, tySynInstDName, dataFamilyDName, @@ -357,6 +357,7 @@ classDName = libFun (fsLit "classD") instanceWithOverlapDName = libFun (fsLit "instanceWithOverlapD") instanceWithOverlapDIdKey standaloneDerivWithStrategyDName = libFun (fsLit "standaloneDerivWithStrategyD") standaloneDerivWithStrategyDIdKey sigDName = libFun (fsLit "sigD") sigDIdKey +kiSigDName = libFun (fsLit "kiSigD") kiSigDIdKey defaultSigDName = libFun (fsLit "defaultSigD") defaultSigDIdKey forImpDName = libFun (fsLit "forImpD") forImpDIdKey pragInlDName = libFun (fsLit "pragInlD") pragInlDIdKey @@ -868,7 +869,8 @@ funDIdKey, valDIdKey, dataDIdKey, newtypeDIdKey, tySynDIdKey, classDIdKey, openTypeFamilyDIdKey, closedTypeFamilyDIdKey, dataInstDIdKey, newtypeInstDIdKey, tySynInstDIdKey, standaloneDerivWithStrategyDIdKey, infixLDIdKey, infixRDIdKey, infixNDIdKey, roleAnnotDIdKey, patSynDIdKey, - patSynSigDIdKey, pragCompleteDIdKey, implicitParamBindDIdKey :: Unique + patSynSigDIdKey, pragCompleteDIdKey, implicitParamBindDIdKey, + kiSigDIdKey :: Unique funDIdKey = mkPreludeMiscIdUnique 320 valDIdKey = mkPreludeMiscIdUnique 321 dataDIdKey = mkPreludeMiscIdUnique 322 @@ -901,6 +903,7 @@ patSynDIdKey = mkPreludeMiscIdUnique 348 patSynSigDIdKey = mkPreludeMiscIdUnique 349 pragCompleteDIdKey = mkPreludeMiscIdUnique 350 implicitParamBindDIdKey = mkPreludeMiscIdUnique 351 +kiSigDIdKey = mkPreludeMiscIdUnique 352 -- type Cxt = ... cxtIdKey :: Unique diff --git a/compiler/prelude/TysWiredIn.hs b/compiler/prelude/TysWiredIn.hs index 4b0141aba3..be4bfe1ce9 100644 --- a/compiler/prelude/TysWiredIn.hs +++ b/compiler/prelude/TysWiredIn.hs @@ -93,7 +93,7 @@ module TysWiredIn ( -- * Kinds typeNatKindCon, typeNatKind, typeSymbolKindCon, typeSymbolKind, isLiftedTypeKindTyConName, liftedTypeKind, constraintKind, - liftedTypeKindTyCon, constraintKindTyCon, + liftedTypeKindTyCon, constraintKindTyCon, constraintKindTyConName, liftedTypeKindTyConName, -- * Equality predicates @@ -406,7 +406,7 @@ makeRecoveryTyCon :: TyCon -> TyCon makeRecoveryTyCon tc = mkTcTyCon (tyConName tc) bndrs res_kind - [] -- No scoped vars + noTcTyConScopedTyVars True -- Fully generalised flavour -- Keep old flavour where diff --git a/compiler/rename/RnBinds.hs b/compiler/rename/RnBinds.hs index 811a81bdb1..56caee1a2a 100644 --- a/compiler/rename/RnBinds.hs +++ b/compiler/rename/RnBinds.hs @@ -973,7 +973,7 @@ renameSig ctxt sig@(ClassOpSig _ is_deflt vs ty) ; when (is_deflt && not defaultSigs_on) $ addErr (defaultSigErr sig) ; new_v <- mapM (lookupSigOccRn ctxt sig) vs - ; (new_ty, fvs) <- rnHsSigType ty_ctxt ty + ; (new_ty, fvs) <- rnHsSigType ty_ctxt TypeLevel ty ; return (ClassOpSig noExtField is_deflt new_v new_ty, fvs) } where (v1:_) = vs @@ -981,7 +981,7 @@ renameSig ctxt sig@(ClassOpSig _ is_deflt vs ty) <+> quotes (ppr v1)) renameSig _ (SpecInstSig _ src ty) - = do { (new_ty, fvs) <- rnHsSigType SpecInstSigCtx ty + = do { (new_ty, fvs) <- rnHsSigType SpecInstSigCtx TypeLevel ty ; return (SpecInstSig noExtField src new_ty,fvs) } -- {-# SPECIALISE #-} pragmas can refer to imported Ids @@ -998,7 +998,7 @@ renameSig ctxt sig@(SpecSig _ v tys inl) ty_ctxt = GenericCtx (text "a SPECIALISE signature for" <+> quotes (ppr v)) do_one (tys,fvs) ty - = do { (new_ty, fvs_ty) <- rnHsSigType ty_ctxt ty + = do { (new_ty, fvs_ty) <- rnHsSigType ty_ctxt TypeLevel ty ; return ( new_ty:tys, fvs_ty `plusFV` fvs) } renameSig ctxt sig@(InlineSig _ v s) @@ -1015,7 +1015,7 @@ renameSig ctxt sig@(MinimalSig _ s (L l bf)) renameSig ctxt sig@(PatSynSig _ vs ty) = do { new_vs <- mapM (lookupSigOccRn ctxt sig) vs - ; (ty', fvs) <- rnHsSigType ty_ctxt ty + ; (ty', fvs) <- rnHsSigType ty_ctxt TypeLevel ty ; return (PatSynSig noExtField new_vs ty', fvs) } where ty_ctxt = GenericCtx (text "a pattern synonym signature for" diff --git a/compiler/rename/RnSource.hs b/compiler/rename/RnSource.hs index 229c66fda4..1ab80e755a 100644 --- a/compiler/rename/RnSource.hs +++ b/compiler/rename/RnSource.hs @@ -70,8 +70,9 @@ import Control.Arrow ( first ) import Data.List ( mapAccumL ) import qualified Data.List.NonEmpty as NE import Data.List.NonEmpty ( NonEmpty(..) ) -import Data.Maybe ( isNothing, isJust, fromMaybe ) +import Data.Maybe ( isNothing, fromMaybe, mapMaybe ) import qualified Data.Set as Set ( difference, fromList, toList, null ) +import Data.Function ( on ) {- | @rnSourceDecl@ "renames" declarations. It simultaneously performs dependency analysis and precedence parsing. @@ -370,7 +371,7 @@ rnHsForeignDecl :: ForeignDecl GhcPs -> RnM (ForeignDecl GhcRn, FreeVars) rnHsForeignDecl (ForeignImport { fd_name = name, fd_sig_ty = ty, fd_fi = spec }) = do { topEnv :: HscEnv <- getTopEnv ; name' <- lookupLocatedTopBndrRn name - ; (ty', fvs) <- rnHsSigType (ForeignDeclCtx name) ty + ; (ty', fvs) <- rnHsSigType (ForeignDeclCtx name) TypeLevel ty -- Mark any PackageTarget style imports as coming from the current package ; let unitId = thisPackage $ hsc_dflags topEnv @@ -382,7 +383,7 @@ rnHsForeignDecl (ForeignImport { fd_name = name, fd_sig_ty = ty, fd_fi = spec }) rnHsForeignDecl (ForeignExport { fd_name = name, fd_sig_ty = ty, fd_fe = spec }) = do { name' <- lookupLocatedOccRn name - ; (ty', fvs) <- rnHsSigType (ForeignDeclCtx name) ty + ; (ty', fvs) <- rnHsSigType (ForeignDeclCtx name) TypeLevel ty ; return (ForeignExport { fd_e_ext = noExtField , fd_name = name', fd_sig_ty = ty' , fd_fe = spec } @@ -607,7 +608,7 @@ rnClsInstDecl (ClsInstDecl { cid_poly_ty = inst_ty, cid_binds = mbinds , cid_overlap_mode = oflag , cid_datafam_insts = adts }) = do { (inst_ty', inst_fvs) - <- rnHsSigType (GenericCtx $ text "an instance declaration") inst_ty + <- rnHsSigType (GenericCtx $ text "an instance declaration") TypeLevel inst_ty ; let (ktv_names, _, head_ty') = splitLHsInstDeclTy inst_ty' ; cls <- case hsTyGetAppHead_maybe head_ty' of @@ -1288,17 +1289,17 @@ rnTyClDecls :: [TyClGroup GhcPs] -- Rename the declarations and do dependency analysis on them rnTyClDecls tycl_ds = do { -- Rename the type/class, instance, and role declaraations - tycls_w_fvs <- mapM (wrapLocFstM rnTyClDecl) - (tyClGroupTyClDecls tycl_ds) + ; tycls_w_fvs <- mapM (wrapLocFstM rnTyClDecl) (tyClGroupTyClDecls tycl_ds) ; let tc_names = mkNameSet (map (tcdName . unLoc . fst) tycls_w_fvs) - + ; kisigs_w_fvs <- rnStandaloneKindSignatures tc_names (tyClGroupKindSigs tycl_ds) ; instds_w_fvs <- mapM (wrapLocFstM rnSrcInstDecl) (tyClGroupInstDecls tycl_ds) ; role_annots <- rnRoleAnnots tc_names (tyClGroupRoleDecls tycl_ds) -- Do SCC analysis on the type/class decls ; rdr_env <- getGlobalRdrEnv - ; let tycl_sccs = depAnalTyClDecls rdr_env tycls_w_fvs + ; let tycl_sccs = depAnalTyClDecls rdr_env kisig_fv_env tycls_w_fvs role_annot_env = mkRoleAnnotEnv role_annots + (kisig_env, kisig_fv_env) = mkKindSig_fv_env kisigs_w_fvs inst_ds_map = mkInstDeclFreeVarsMap rdr_env tc_names instds_w_fvs (init_inst_ds, rest_inst_ds) = getInsts [] inst_ds_map @@ -1307,15 +1308,16 @@ rnTyClDecls tycl_ds | null init_inst_ds = [] | otherwise = [TyClGroup { group_ext = noExtField , group_tyclds = [] + , group_kisigs = [] , group_roles = [] , group_instds = init_inst_ds }] (final_inst_ds, groups) - = mapAccumL (mk_group role_annot_env) rest_inst_ds tycl_sccs - + = mapAccumL (mk_group role_annot_env kisig_env) rest_inst_ds tycl_sccs - all_fvs = plusFV (foldr (plusFV . snd) emptyFVs tycls_w_fvs) - (foldr (plusFV . snd) emptyFVs instds_w_fvs) + all_fvs = foldr (plusFV . snd) emptyFVs tycls_w_fvs `plusFV` + foldr (plusFV . snd) emptyFVs instds_w_fvs `plusFV` + foldr (plusFV . snd) emptyFVs kisigs_w_fvs all_groups = first_group ++ groups @@ -1326,32 +1328,91 @@ rnTyClDecls tycl_ds ; return (all_groups, all_fvs) } where mk_group :: RoleAnnotEnv + -> KindSigEnv -> InstDeclFreeVarsMap -> SCC (LTyClDecl GhcRn) -> (InstDeclFreeVarsMap, TyClGroup GhcRn) - mk_group role_env inst_map scc + mk_group role_env kisig_env inst_map scc = (inst_map', group) where tycl_ds = flattenSCC scc bndrs = map (tcdName . unLoc) tycl_ds roles = getRoleAnnots bndrs role_env + kisigs = getKindSigs bndrs kisig_env (inst_ds, inst_map') = getInsts bndrs inst_map group = TyClGroup { group_ext = noExtField , group_tyclds = tycl_ds + , group_kisigs = kisigs , group_roles = roles , group_instds = inst_ds } +-- | Free variables of standalone kind signatures. +newtype KindSig_FV_Env = KindSig_FV_Env (NameEnv FreeVars) + +lookupKindSig_FV_Env :: KindSig_FV_Env -> Name -> FreeVars +lookupKindSig_FV_Env (KindSig_FV_Env e) name + = fromMaybe emptyFVs (lookupNameEnv e name) + +-- | Standalone kind signatures. +type KindSigEnv = NameEnv (LStandaloneKindSig GhcRn) + +mkKindSig_fv_env :: [(LStandaloneKindSig GhcRn, FreeVars)] -> (KindSigEnv, KindSig_FV_Env) +mkKindSig_fv_env kisigs_w_fvs = (kisig_env, kisig_fv_env) + where + kisig_env = mapNameEnv fst compound_env + kisig_fv_env = KindSig_FV_Env (mapNameEnv snd compound_env) + compound_env :: NameEnv (LStandaloneKindSig GhcRn, FreeVars) + = mkNameEnvWith (standaloneKindSigName . unLoc . fst) kisigs_w_fvs + +getKindSigs :: [Name] -> KindSigEnv -> [LStandaloneKindSig GhcRn] +getKindSigs bndrs kisig_env = mapMaybe (lookupNameEnv kisig_env) bndrs + +rnStandaloneKindSignatures + :: NameSet -- names of types and classes in the current TyClGroup + -> [LStandaloneKindSig GhcPs] + -> RnM [(LStandaloneKindSig GhcRn, FreeVars)] +rnStandaloneKindSignatures tc_names kisigs + = do { let (no_dups, dup_kisigs) = removeDups (compare `on` get_name) kisigs + get_name = standaloneKindSigName . unLoc + ; mapM_ dupKindSig_Err dup_kisigs + ; mapM (wrapLocFstM (rnStandaloneKindSignature tc_names)) no_dups + } + +rnStandaloneKindSignature + :: NameSet -- names of types and classes in the current TyClGroup + -> StandaloneKindSig GhcPs + -> RnM (StandaloneKindSig GhcRn, FreeVars) +rnStandaloneKindSignature tc_names (StandaloneKindSig _ v ki) + = do { standalone_ki_sig_ok <- xoptM LangExt.StandaloneKindSignatures + ; unless standalone_ki_sig_ok $ addErr standaloneKiSigErr + ; new_v <- lookupSigCtxtOccRn (TopSigCtxt tc_names) (text "standalone kind signature") v + ; let doc = StandaloneKindSigCtx (ppr v) + ; (new_ki, fvs) <- rnHsSigType doc KindLevel ki + ; return (StandaloneKindSig noExtField new_v new_ki, fvs) + } + where + standaloneKiSigErr :: SDoc + standaloneKiSigErr = + hang (text "Illegal standalone kind signature") + 2 (text "Did you mean to enable StandaloneKindSignatures?") +rnStandaloneKindSignature _ (XStandaloneKindSig nec) = noExtCon nec depAnalTyClDecls :: GlobalRdrEnv + -> KindSig_FV_Env -> [(LTyClDecl GhcRn, FreeVars)] -> [SCC (LTyClDecl GhcRn)] -- See Note [Dependency analysis of type, class, and instance decls] -depAnalTyClDecls rdr_env ds_w_fvs +depAnalTyClDecls rdr_env kisig_fv_env ds_w_fvs = stronglyConnCompFromEdgedVerticesUniq edges where edges :: [ Node Name (LTyClDecl GhcRn) ] - edges = [ DigraphNode d (tcdName (unLoc d)) (map (getParent rdr_env) (nonDetEltsUniqSet fvs)) - | (d, fvs) <- ds_w_fvs ] + edges = [ DigraphNode d name (map (getParent rdr_env) (nonDetEltsUniqSet deps)) + | (d, fvs) <- ds_w_fvs, + let { name = tcdName (unLoc d) + ; kisig_fvs = lookupKindSig_FV_Env kisig_fv_env name + ; deps = fvs `plusFV` kisig_fvs + } + ] -- It's OK to use nonDetEltsUFM here as -- stronglyConnCompFromEdgedVertices is still deterministic -- even if the edges are in nondeterministic order as explained @@ -1391,9 +1452,8 @@ rnRoleAnnots :: NameSet rnRoleAnnots tc_names role_annots = do { -- Check for duplicates *before* renaming, to avoid -- lumping together all the unboundNames - let (no_dups, dup_annots) = removeDups role_annots_cmp role_annots - role_annots_cmp (dL->L _ annot1) (dL->L _ annot2) - = roleAnnotDeclName annot1 `compare` roleAnnotDeclName annot2 + let (no_dups, dup_annots) = removeDups (compare `on` get_name) role_annots + get_name = roleAnnotDeclName . unLoc ; mapM_ dupRoleAnnotErr dup_annots ; mapM (wrapLocM rn_role_annot1) no_dups } where @@ -1421,6 +1481,20 @@ dupRoleAnnotErr list cmp_annot (dL->L loc1 _) (dL->L loc2 _) = loc1 `compare` loc2 +dupKindSig_Err :: NonEmpty (LStandaloneKindSig GhcPs) -> RnM () +dupKindSig_Err list + = addErrAt loc $ + hang (text "Duplicate standalone kind signatures for" <+> + quotes (ppr $ standaloneKindSigName first_decl) <> colon) + 2 (vcat $ map pp_kisig $ NE.toList sorted_list) + where + sorted_list = NE.sortBy cmp_loc list + ((dL->L loc first_decl) :| _) = sorted_list + + pp_kisig (dL->L loc decl) = + hang (ppr decl) 4 (text "-- written at" <+> ppr loc) + + cmp_loc (dL->L loc1 _) (dL->L loc2 _) = loc1 `compare` loc2 {- Note [Role annotations in the renamer] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1495,12 +1569,11 @@ getInsts bndrs inst_decl_map rnTyClDecl :: TyClDecl GhcPs -> RnM (TyClDecl GhcRn, FreeVars) --- All flavours of type family declarations ("type family", "newtype family", --- and "data family"), both top level and (for an associated type) --- in a class decl -rnTyClDecl (FamDecl { tcdFam = decl }) - = do { (decl', fvs) <- rnFamDecl Nothing decl - ; return (FamDecl noExtField decl', fvs) } +-- All flavours of top-level type family declarations ("type family", "newtype +-- family", and "data family") +rnTyClDecl (FamDecl { tcdFam = fam }) + = do { (fam', fvs) <- rnFamDecl Nothing fam + ; return (FamDecl noExtField fam', fvs) } rnTyClDecl (SynDecl { tcdLName = tycon, tcdTyVars = tyvars, tcdFixity = fixity, tcdRhs = rhs }) @@ -1515,9 +1588,7 @@ rnTyClDecl (SynDecl { tcdLName = tycon, tcdTyVars = tyvars, , tcdRhs = rhs', tcdSExt = fvs }, fvs) } } -- "data", "newtype" declarations --- both top level and (for an associated type) in an instance decl -rnTyClDecl (DataDecl _ _ _ _ (XHsDataDefn _)) = - panic "rnTyClDecl: DataDecl with XHsDataDefn" +rnTyClDecl (DataDecl _ _ _ _ (XHsDataDefn nec)) = noExtCon nec rnTyClDecl (DataDecl { tcdLName = tycon, tcdTyVars = tyvars, tcdFixity = fixity, @@ -1529,8 +1600,7 @@ rnTyClDecl (DataDecl ; traceRn "rntycl-data" (ppr tycon <+> ppr kvs) ; bindHsQTyVars doc Nothing Nothing kvs tyvars $ \ tyvars' no_rhs_kvs -> do { (defn', fvs) <- rnDataDefn doc defn - ; cusk <- dataDeclHasCUSK - tyvars' new_or_data no_rhs_kvs (isJust kind_sig) + ; cusk <- data_decl_has_cusk tyvars' new_or_data no_rhs_kvs kind_sig ; let rn_info = DataDeclRn { tcdDataCusk = cusk , tcdFVs = fvs } ; traceRn "rndata" (ppr tycon <+> ppr cusk <+> ppr no_rhs_kvs) @@ -1608,19 +1678,17 @@ rnTyClDecl (ClassDecl { tcdCtxt = context, tcdLName = lcls, rnTyClDecl (XTyClDecl nec) = noExtCon nec -- Does the data type declaration include a CUSK? -dataDeclHasCUSK :: LHsQTyVars pass -> NewOrData -> Bool -> Bool -> RnM Bool -dataDeclHasCUSK tyvars new_or_data no_rhs_kvs has_kind_sig = do +data_decl_has_cusk :: LHsQTyVars pass -> NewOrData -> Bool -> Maybe (LHsKind pass') -> RnM Bool +data_decl_has_cusk tyvars new_or_data no_rhs_kvs kind_sig = do { -- See Note [Unlifted Newtypes and CUSKs], and for a broader -- picture, see Note [Implementation of UnliftedNewtypes]. ; unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes ; let non_cusk_newtype | NewType <- new_or_data = - unlifted_newtypes && not has_kind_sig + unlifted_newtypes && isNothing kind_sig | otherwise = False -- See Note [CUSKs: complete user-supplied kind signatures] in GHC.Hs.Decls - ; cusks_enabled <- xoptM LangExt.CUSKs - ; return $ cusks_enabled && hsTvbAllKinded tyvars && - no_rhs_kvs && not non_cusk_newtype + ; return $ hsTvbAllKinded tyvars && no_rhs_kvs && not non_cusk_newtype } {- Note [Unlifted Newtypes and CUSKs] @@ -1724,7 +1792,7 @@ rnLHsDerivingClause doc , deriv_clause_strategy = dcs , deriv_clause_tys = (dL->L loc' dct) })) = do { (dcs', dct', fvs) - <- rnLDerivStrategy doc dcs $ mapFvRn (rnHsSigType doc) dct + <- rnLDerivStrategy doc dcs $ mapFvRn (rnHsSigType doc TypeLevel) dct ; warnNoDerivStrat dcs' loc ; pure ( cL loc (HsDerivingClause { deriv_clause_ext = noExtField , deriv_clause_strategy = dcs' @@ -1766,7 +1834,7 @@ rnLDerivStrategy doc mds thing_inside AnyclassStrategy -> boring_case AnyclassStrategy NewtypeStrategy -> boring_case NewtypeStrategy ViaStrategy via_ty -> - do (via_ty', fvs1) <- rnHsSigType doc via_ty + do (via_ty', fvs1) <- rnHsSigType doc TypeLevel via_ty let HsIB { hsib_ext = via_imp_tvs , hsib_body = via_body } = via_ty' (via_exp_tv_bndrs, _, _) = splitLHsSigmaTy via_body @@ -2249,6 +2317,11 @@ add gp@(HsGroup {hs_tyclds = ts, hs_fixds = fs}) l (TyClD _ d) ds -- Signatures: fixity sigs go a different place than all others add gp@(HsGroup {hs_fixds = ts}) l (SigD _ (FixSig _ f)) ds = addl (gp {hs_fixds = cL l f : ts}) ds + +-- Standalone kind signatures: added to the TyClGroup +add gp@(HsGroup {hs_tyclds = ts}) l (KindSigD _ s) ds + = addl (gp {hs_tyclds = add_kisig (cL l s) ts}) ds + add gp@(HsGroup {hs_valds = ts}) l (SigD _ d) ds = addl (gp {hs_valds = add_sig (cL l d) ts}) ds @@ -2289,6 +2362,7 @@ add_tycld :: LTyClDecl (GhcPass p) -> [TyClGroup (GhcPass p)] -> [TyClGroup (GhcPass p)] add_tycld d [] = [TyClGroup { group_ext = noExtField , group_tyclds = [d] + , group_kisigs = [] , group_roles = [] , group_instds = [] } @@ -2301,6 +2375,7 @@ add_instd :: LInstDecl (GhcPass p) -> [TyClGroup (GhcPass p)] -> [TyClGroup (GhcPass p)] add_instd d [] = [TyClGroup { group_ext = noExtField , group_tyclds = [] + , group_kisigs = [] , group_roles = [] , group_instds = [d] } @@ -2313,6 +2388,7 @@ add_role_annot :: LRoleAnnotDecl (GhcPass p) -> [TyClGroup (GhcPass p)] -> [TyClGroup (GhcPass p)] add_role_annot d [] = [TyClGroup { group_ext = noExtField , group_tyclds = [] + , group_kisigs = [] , group_roles = [d] , group_instds = [] } @@ -2321,6 +2397,19 @@ add_role_annot d (tycls@(TyClGroup { group_roles = roles }) : rest) = tycls { group_roles = d : roles } : rest add_role_annot _ (XTyClGroup nec: _) = noExtCon nec +add_kisig :: LStandaloneKindSig (GhcPass p) + -> [TyClGroup (GhcPass p)] -> [TyClGroup (GhcPass p)] +add_kisig d [] = [TyClGroup { group_ext = noExtField + , group_tyclds = [] + , group_kisigs = [d] + , group_roles = [] + , group_instds = [] + } + ] +add_kisig d (tycls@(TyClGroup { group_kisigs = kisigs }) : rest) + = tycls { group_kisigs = d : kisigs } : rest +add_kisig _ (XTyClGroup nec : _) = noExtCon nec + add_bind :: LHsBind a -> HsValBinds a -> HsValBinds a add_bind b (ValBinds x bs sigs) = ValBinds x (bs `snocBag` b) sigs add_bind _ (XValBindsLR {}) = panic "RdrHsSyn:add_bind" diff --git a/compiler/rename/RnTypes.hs b/compiler/rename/RnTypes.hs index e982e72f82..5f0a1c62c7 100644 --- a/compiler/rename/RnTypes.hs +++ b/compiler/rename/RnTypes.hs @@ -242,6 +242,7 @@ extraConstraintWildCardsAllowed env TypeSigCtx {} -> True ExprWithTySigCtx {} -> True DerivDeclCtx {} -> True + StandaloneKindSigCtx {} -> False -- See Note [Wildcards in standalone kind signatures] in GHC/Hs/Decls _ -> False -- | Finds free type and kind variables in a type, @@ -295,19 +296,22 @@ of the HsWildCardBndrs structure, and we are done. * * ****************************************************** -} -rnHsSigType :: HsDocContext -> LHsSigType GhcPs +rnHsSigType :: HsDocContext + -> TypeOrKind + -> LHsSigType GhcPs -> RnM (LHsSigType GhcRn, FreeVars) -- Used for source-language type signatures -- that cannot have wildcards -rnHsSigType ctx (HsIB { hsib_body = hs_ty }) +rnHsSigType ctx level (HsIB { hsib_body = hs_ty }) = do { traceRn "rnHsSigType" (ppr hs_ty) ; vars <- extractFilteredRdrTyVarsDups hs_ty ; rnImplicitBndrs (not (isLHsForAllTy hs_ty)) vars $ \ vars -> - do { (body', fvs) <- rnLHsType ctx hs_ty + do { (body', fvs) <- rnLHsTyKi (mkTyKiEnv ctx level RnTypeBody) hs_ty + ; return ( HsIB { hsib_ext = vars , hsib_body = body' } , fvs ) } } -rnHsSigType _ (XHsImplicitBndrs nec) = noExtCon nec +rnHsSigType _ _ (XHsImplicitBndrs nec) = noExtCon nec rnImplicitBndrs :: Bool -- True <=> bring into scope any free type variables -- E.g. f :: forall a. a->b @@ -563,9 +567,9 @@ rnHsTyKi env t@(HsKindSig _ ty k) = do { checkPolyKinds env t ; kind_sigs_ok <- xoptM LangExt.KindSignatures ; unless kind_sigs_ok (badKindSigErr (rtke_ctxt env) ty) - ; (ty', fvs1) <- rnLHsTyKi env ty - ; (k', fvs2) <- rnLHsTyKi (env { rtke_level = KindLevel }) k - ; return (HsKindSig noExtField ty' k', fvs1 `plusFV` fvs2) } + ; (ty', lhs_fvs) <- rnLHsTyKi env ty + ; (k', sig_fvs) <- rnLHsTyKi (env { rtke_level = KindLevel }) k + ; return (HsKindSig noExtField ty' k', lhs_fvs `plusFV` sig_fvs) } -- Unboxed tuples are allowed to have poly-typed arguments. These -- sometimes crop up as a result of CPR worker-wrappering dictionaries. @@ -734,6 +738,7 @@ wildCardsAllowed env FamPatCtx {} -> True -- Not named wildcards though GHCiCtx {} -> True HsTypeCtx {} -> True + StandaloneKindSigCtx {} -> False -- See Note [Wildcards in standalone kind signatures] in GHC/Hs/Decls _ -> False diff --git a/compiler/rename/RnUtils.hs b/compiler/rename/RnUtils.hs index 6678ad6dbf..0da8e30f6a 100644 --- a/compiler/rename/RnUtils.hs +++ b/compiler/rename/RnUtils.hs @@ -458,6 +458,7 @@ checkTupSize tup_size -- Merge TcType.UserTypeContext in to it. data HsDocContext = TypeSigCtx SDoc + | StandaloneKindSigCtx SDoc | PatCtx | SpecInstSigCtx | DefaultDeclCtx @@ -487,6 +488,7 @@ inHsDocContext ctxt = text "In" <+> pprHsDocContext ctxt pprHsDocContext :: HsDocContext -> SDoc pprHsDocContext (GenericCtx doc) = doc pprHsDocContext (TypeSigCtx doc) = text "the type signature for" <+> doc +pprHsDocContext (StandaloneKindSigCtx doc) = text "the standalone kind signature for" <+> doc pprHsDocContext PatCtx = text "a pattern type-signature" pprHsDocContext SpecInstSigCtx = text "a SPECIALISE instance pragma" pprHsDocContext DefaultDeclCtx = text "a `default' declaration" diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs index d2b32e7d7d..d74b38c9fd 100644 --- a/compiler/typecheck/TcDeriv.hs +++ b/compiler/typecheck/TcDeriv.hs @@ -195,6 +195,8 @@ both of them. So we gather defs/uses from deriving just like anything else. data DerivInfo = DerivInfo { di_rep_tc :: TyCon -- ^ The data tycon for normal datatypes, -- or the *representation* tycon for data families + , di_scoped_tvs :: ![(Name,TyVar)] + -- ^ Variables that scope over the deriving clause. , di_clauses :: [LHsDerivingClause GhcRn] , di_ctxt :: SDoc -- ^ error context } @@ -493,8 +495,10 @@ makeDerivSpecs :: Bool -> TcM [EarlyDerivSpec] makeDerivSpecs is_boot deriv_infos deriv_decls = do { eqns1 <- sequenceA - [ deriveClause rep_tc dcs preds err_ctxt - | DerivInfo { di_rep_tc = rep_tc, di_clauses = clauses + [ deriveClause rep_tc scoped_tvs dcs preds err_ctxt + | DerivInfo { di_rep_tc = rep_tc + , di_scoped_tvs = scoped_tvs + , di_clauses = clauses , di_ctxt = err_ctxt } <- deriv_infos , L _ (HsDerivingClause { deriv_clause_strategy = dcs , deriv_clause_tys = L _ preds }) @@ -515,17 +519,21 @@ makeDerivSpecs is_boot deriv_infos deriv_decls ------------------------------------------------------------------ -- | Process the derived classes in a single @deriving@ clause. -deriveClause :: TyCon -> Maybe (LDerivStrategy GhcRn) +deriveClause :: TyCon + -> [(Name, TcTyVar)] -- Scoped type variables taken from tcTyConScopedTyVars + -- See Note [Scoped tyvars in a TcTyCon] in types/TyCon + -> Maybe (LDerivStrategy GhcRn) -> [LHsSigType GhcRn] -> SDoc -> TcM [EarlyDerivSpec] -deriveClause rep_tc mb_lderiv_strat deriv_preds err_ctxt +deriveClause rep_tc scoped_tvs mb_lderiv_strat deriv_preds err_ctxt = addErrCtxt err_ctxt $ do traceTc "deriveClause" $ vcat [ text "tvs" <+> ppr tvs + , text "scoped_tvs" <+> ppr scoped_tvs , text "tc" <+> ppr tc , text "tys" <+> ppr tys , text "mb_lderiv_strat" <+> ppr mb_lderiv_strat ] - tcExtendTyVarEnv tvs $ do + tcExtendNameTyVarEnv scoped_tvs $ do (mb_lderiv_strat', via_tvs) <- tcDerivStrategy mb_lderiv_strat tcExtendTyVarEnv via_tvs $ -- Moreover, when using DerivingVia one can bind type variables in diff --git a/compiler/typecheck/TcEnv.hs b/compiler/typecheck/TcEnv.hs index 3cc1994f5b..2d59dc191b 100644 --- a/compiler/typecheck/TcEnv.hs +++ b/compiler/typecheck/TcEnv.hs @@ -36,6 +36,7 @@ module TcEnv( tcLookup, tcLookupLocated, tcLookupLocalIds, tcLookupId, tcLookupIdMaybe, tcLookupTyVar, + tcLookupTcTyCon, tcLookupLcl_maybe, getInLocalScope, wrongThingErr, pprBinders, @@ -106,6 +107,7 @@ import ListSetOps import ErrUtils import Maybes( MaybeErr(..), orElse ) import qualified GHC.LanguageExtensions as LangExt +import Util ( HasDebugCallStack ) import Data.IORef import Data.List @@ -443,6 +445,13 @@ tcLookupLocalIds ns Just (ATcId { tct_id = id }) -> id _ -> pprPanic "tcLookupLocalIds" (ppr name) +tcLookupTcTyCon :: HasDebugCallStack => Name -> TcM TcTyCon +tcLookupTcTyCon name = do + thing <- tcLookup name + case thing of + ATcTyCon tc -> return tc + _ -> pprPanic "tcLookupTcTyCon" (ppr name) + getInLocalScope :: TcM (Name -> Bool) getInLocalScope = do { lcl_env <- getLclTypeEnv ; return (`elemNameEnv` lcl_env) } diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index 37cc83e4ca..cd65fc0522 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -7,6 +7,7 @@ {-# LANGUAGE CPP, TupleSections, MultiWayIf, RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ViewPatterns #-} @@ -15,6 +16,7 @@ module TcHsType ( kcClassSigType, tcClassSigType, tcHsSigType, tcHsSigWcType, tcHsPartialSigType, + tcStandaloneKindSig, funsSigCtxt, addSigCtxt, pprSigCtxt, tcHsClsInstType, @@ -36,7 +38,9 @@ module TcHsType ( -- Kind-checking types -- No kind generalisation, no checkValidType - kcLHsQTyVars, + InitialKindStrategy(..), + SAKS_or_CUSK(..), + kcDeclHeader, tcNamedWildCardBinders, tcHsLiftedType, tcHsOpenType, tcHsLiftedTypeNC, tcHsOpenTypeNC, @@ -52,6 +56,7 @@ module TcHsType ( -- Sort-checking kinds tcLHsKindSig, checkDataKindSig, DataSort(..), + checkClassKindSig, -- Pattern type signatures tcHsPatSigType, tcPatSig, @@ -74,11 +79,10 @@ import TcUnify import TcIface import TcSimplify import TcHsSyn -import TyCoRep ( Type(..) ) +import TyCoRep import TcErrors ( reportAllUnsolved ) import TcType import Inst ( tcInstInvisibleTyBinders, tcInstInvisibleTyBinder ) -import TyCoRep( TyCoBinder(..) ) -- Used in etaExpandAlgTyCon import Type import TysPrim import RdrName( lookupLocalRdrOcc ) @@ -241,6 +245,17 @@ tcHsSigType ctxt sig_ty where skol_info = SigTypeSkol ctxt +-- Does validity checking and zonking. +tcStandaloneKindSig :: LStandaloneKindSig GhcRn -> TcM (Name, Kind) +tcStandaloneKindSig (L _ kisig) = case kisig of + StandaloneKindSig _ (L _ name) ksig -> + let ctxt = StandaloneKindSigCtxt name in + addSigCtxt ctxt (hsSigType ksig) $ + do { kind <- tcTopLHsType kindLevelMode ksig (expectedKindInCtxt ctxt) + ; checkValidType ctxt kind + ; return (name, kind) } + XStandaloneKindSig nec -> noExtCon nec + tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn -> ContextKind -> TcM (Bool, TcType) -- Kind-checks/desugars an 'LHsSigType', @@ -279,13 +294,13 @@ tc_hs_sig_type skol_info hs_sig_type ctxt_kind tc_hs_sig_type _ (XHsImplicitBndrs nec) _ = noExtCon nec -tcTopLHsType :: LHsSigType GhcRn -> ContextKind -> TcM Type +tcTopLHsType :: TcTyMode -> LHsSigType GhcRn -> ContextKind -> TcM Type -- tcTopLHsType is used for kind-checking top-level HsType where -- we want to fully solve /all/ equalities, and report errors -- Does zonking, but not validity checking because it's used -- for things (like deriving and instances) that aren't -- ordinary types -tcTopLHsType hs_sig_type ctxt_kind +tcTopLHsType mode hs_sig_type ctxt_kind | HsIB { hsib_ext = sig_vars, hsib_body = hs_ty } <- hs_sig_type = do { traceTc "tcTopLHsType {" (ppr hs_ty) ; (spec_tkvs, ty) @@ -293,7 +308,7 @@ tcTopLHsType hs_sig_type ctxt_kind solveEqualities $ bindImplicitTKBndrs_Skol sig_vars $ do { kind <- newExpectedKind ctxt_kind - ; tc_lhs_type typeLevelMode hs_ty kind } + ; tc_lhs_type mode hs_ty kind } ; spec_tkvs <- zonkAndScopedSort spec_tkvs ; let ty1 = mkSpecForAllTys spec_tkvs ty @@ -302,7 +317,7 @@ tcTopLHsType hs_sig_type ctxt_kind ; traceTc "End tcTopLHsType }" (vcat [ppr hs_ty, ppr final_ty]) ; return final_ty} -tcTopLHsType (XHsImplicitBndrs nec) _ = noExtCon nec +tcTopLHsType _ (XHsImplicitBndrs nec) _ = noExtCon nec ----------------- tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], Class, [Type], [Kind]) @@ -315,7 +330,7 @@ tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], Class, [Type], [Kind]) tcHsDeriv hs_ty = do { ty <- checkNoErrs $ -- Avoid redundant error report -- with "illegal deriving", below - tcTopLHsType hs_ty AnyKind + tcTopLHsType typeLevelMode hs_ty AnyKind ; let (tvs, pred) = splitForAllTys ty (kind_args, _) = splitFunTys (tcTypeKind pred) ; case getClassPredTys_maybe pred of @@ -344,7 +359,7 @@ tcDerivStrategy mb_lds tc_deriv_strategy AnyclassStrategy = boring_case AnyclassStrategy tc_deriv_strategy NewtypeStrategy = boring_case NewtypeStrategy tc_deriv_strategy (ViaStrategy ty) = do - ty' <- checkNoErrs $ tcTopLHsType ty AnyKind + ty' <- checkNoErrs $ tcTopLHsType typeLevelMode ty AnyKind let (via_tvs, via_pred) = splitForAllTys ty' pure (ViaStrategy via_pred, via_tvs) @@ -362,7 +377,7 @@ tcHsClsInstType user_ctxt hs_inst_ty -- eagerly avoids follow-on errors when checkValidInstance -- sees an unsolved coercion hole inst_ty <- checkNoErrs $ - tcTopLHsType hs_inst_ty (TheKind constraintKind) + tcTopLHsType typeLevelMode hs_inst_ty (TheKind constraintKind) ; checkValidInstance user_ctxt hs_inst_ty inst_ty ; return inst_ty } @@ -1776,57 +1791,68 @@ newWildTyVar * * ********************************************************************* -} -{- Note [The initial kind of a type constructor] +-- See Note [kcCheckDeclHeader vs kcInferDeclHeader] +data InitialKindStrategy + = InitialKindCheck SAKS_or_CUSK + | InitialKindInfer + +-- Does the declaration have a standalone kind signature (SAKS) or a complete +-- user-specified kind (CUSK)? +data SAKS_or_CUSK + = SAKS Kind -- Standalone kind signature, fully zonked! (zonkTcTypeToType) + | CUSK -- Complete user-specified kind (CUSK) + +instance Outputable SAKS_or_CUSK where + ppr (SAKS k) = text "SAKS" <+> ppr k + ppr CUSK = text "CUSK" + +-- See Note [kcCheckDeclHeader vs kcInferDeclHeader] +kcDeclHeader + :: InitialKindStrategy + -> Name -- ^ of the thing being checked + -> TyConFlavour -- ^ What sort of 'TyCon' is being checked + -> LHsQTyVars GhcRn -- ^ Binders in the header + -> TcM ContextKind -- ^ The result kind + -> TcM TcTyCon -- ^ A suitably-kinded TcTyCon +kcDeclHeader (InitialKindCheck msig) = kcCheckDeclHeader msig +kcDeclHeader InitialKindInfer = kcInferDeclHeader + +{- Note [kcCheckDeclHeader vs kcInferDeclHeader] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -kcLHsQTyVars is responsible for getting the initial kind of -a type constructor. - -It has two cases: - - * The TyCon has a CUSK. In that case, find the full, final, - poly-kinded kind of the TyCon. It's very like a term-level - binding where we have a complete type signature for the - function. - - * It does not have a CUSK. Find a monomorphic kind, with - unification variables in it; they will be generalised later. - It's very like a term-level binding where we do not have - a type signature (or, more accurately, where we have a - partial type signature), so we infer the type and generalise. +kcCheckDeclHeader and kcInferDeclHeader are responsible for getting the initial kind +of a type constructor. + +* kcCheckDeclHeader: the TyCon has a standalone kind signature or a CUSK. In that + case, find the full, final, poly-kinded kind of the TyCon. It's very like a + term-level binding where we have a complete type signature for the function. + +* kcInferDeclHeader: the TyCon has neither a standalone kind signature nor a + CUSK. Find a monomorphic kind, with unification variables in it; they will be + generalised later. It's very like a term-level binding where we do not have a + type signature (or, more accurately, where we have a partial type signature), + so we infer the type and generalise. -} - ------------------------------- --- | Kind-check a 'LHsQTyVars'. If the decl under consideration has a complete, --- user-supplied kind signature (CUSK), generalise the result. --- Used in 'getInitialKind' (for tycon kinds and other kinds) --- and in kind-checking (but not for tycon kinds, which are checked with --- tcTyClDecls). See Note [CUSKs: complete user-supplied kind signatures] --- in GHC.Hs.Decls. --- --- This function does not do telescope checking. -kcLHsQTyVars :: Name -- ^ of the thing being checked - -> TyConFlavour -- ^ What sort of 'TyCon' is being checked - -> Bool -- ^ True <=> the decl being checked has a CUSK - -> LHsQTyVars GhcRn - -> TcM Kind -- ^ The result kind - -> TcM TcTyCon -- ^ A suitably-kinded TcTyCon -kcLHsQTyVars name flav cusk tvs thing_inside - | cusk = kcLHsQTyVars_Cusk name flav tvs thing_inside - | otherwise = kcLHsQTyVars_NonCusk name flav tvs thing_inside - - -kcLHsQTyVars_Cusk, kcLHsQTyVars_NonCusk - :: Name -- ^ of the thing being checked - -> TyConFlavour -- ^ What sort of 'TyCon' is being checked - -> LHsQTyVars GhcRn - -> TcM Kind -- ^ The result kind - -> TcM TcTyCon -- ^ A suitably-kinded TcTyCon - ------------------------------ -kcLHsQTyVars_Cusk name flav +kcCheckDeclHeader + :: SAKS_or_CUSK + -> Name -- ^ of the thing being checked + -> TyConFlavour -- ^ What sort of 'TyCon' is being checked + -> LHsQTyVars GhcRn -- ^ Binders in the header + -> TcM ContextKind -- ^ The result kind. AnyKind == no result signature + -> TcM TcTyCon -- ^ A suitably-kinded generalized TcTyCon +kcCheckDeclHeader (SAKS sig) = kcCheckDeclHeader_sig sig +kcCheckDeclHeader CUSK = kcCheckDeclHeader_cusk + +kcCheckDeclHeader_cusk + :: Name -- ^ of the thing being checked + -> TyConFlavour -- ^ What sort of 'TyCon' is being checked + -> LHsQTyVars GhcRn -- ^ Binders in the header + -> TcM ContextKind -- ^ The result kind + -> TcM TcTyCon -- ^ A suitably-kinded generalized TcTyCon +kcCheckDeclHeader_cusk name flav (HsQTvs { hsq_ext = kv_ns - , hsq_explicit = hs_tvs }) thing_inside + , hsq_explicit = hs_tvs }) kc_res_ki -- CUSK case -- See note [Required, Specified, and Inferred for types] in TcTyClsDecls = addTyConFlavCtxt name flav $ @@ -1835,19 +1861,21 @@ kcLHsQTyVars_Cusk name flav solveEqualities $ bindImplicitTKBndrs_Q_Skol kv_ns $ bindExplicitTKBndrs_Q_Skol ctxt_kind hs_tvs $ - thing_inside + newExpectedKind =<< kc_res_ki -- Now, because we're in a CUSK, -- we quantify over the mentioned kind vars ; let spec_req_tkvs = scoped_kvs ++ tc_tvs all_kinds = res_kind : map tyVarKind spec_req_tkvs - ; candidates <- candidateQTyVarsOfKinds all_kinds + ; candidates' <- candidateQTyVarsOfKinds all_kinds -- 'candidates' are all the variables that we are going to -- skolemise and then quantify over. We do not include spec_req_tvs -- because they are /already/ skolems - ; let inf_candidates = candidates `delCandidates` spec_req_tkvs + ; let non_tc_candidates = filter (not . isTcTyVar) (nonDetEltsUniqSet (tyCoVarsOfTypes all_kinds)) + candidates = candidates' { dv_kvs = dv_kvs candidates' `extendDVarSetList` non_tc_candidates } + inf_candidates = candidates `delCandidates` spec_req_tkvs ; inferred <- quantifyTyVars inf_candidates -- NB: 'inferred' comes back sorted in dependency order @@ -1866,13 +1894,14 @@ kcLHsQTyVars_Cusk name flav all_tv_prs = mkTyVarNamePairs (scoped_kvs ++ tc_tvs) tycon = mkTcTyCon name final_tc_binders res_kind all_tv_prs - True {- it is generalised -} flav + True -- it is generalised + flav -- If the ordering from -- Note [Required, Specified, and Inferred for types] in TcTyClsDecls -- doesn't work, we catch it here, before an error cascade ; checkTyConTelescope tycon - ; traceTc "kcLHsQTyVars: cusk" $ + ; traceTc "kcCheckDeclHeader_cusk " $ vcat [ text "name" <+> ppr name , text "kv_ns" <+> ppr kv_ns , text "hs_tvs" <+> ppr hs_tvs @@ -1891,21 +1920,29 @@ kcLHsQTyVars_Cusk name flav where ctxt_kind | tcFlavourIsOpen flav = TheKind liftedTypeKind | otherwise = AnyKind +kcCheckDeclHeader_cusk _ _ (XLHsQTyVars nec) _ = noExtCon nec -kcLHsQTyVars_Cusk _ _ (XLHsQTyVars nec) _ = noExtCon nec - ------------------------------- -kcLHsQTyVars_NonCusk name flav +-- | Kind-check a 'LHsQTyVars'. Used in 'inferInitialKind' (for tycon kinds and +-- other kinds). +-- +-- This function does not do telescope checking. +kcInferDeclHeader + :: Name -- ^ of the thing being checked + -> TyConFlavour -- ^ What sort of 'TyCon' is being checked + -> LHsQTyVars GhcRn + -> TcM ContextKind -- ^ The result kind + -> TcM TcTyCon -- ^ A suitably-kinded non-generalized TcTyCon +kcInferDeclHeader name flav (HsQTvs { hsq_ext = kv_ns - , hsq_explicit = hs_tvs }) thing_inside - -- Non_CUSK case + , hsq_explicit = hs_tvs }) kc_res_ki + -- No standalane kind signature and no CUSK. -- See note [Required, Specified, and Inferred for types] in TcTyClsDecls = do { (scoped_kvs, (tc_tvs, res_kind)) -- Why bindImplicitTKBndrs_Q_Tv which uses newTyVarTyVar? -- See Note [Inferring kinds for type declarations] in TcTyClsDecls <- bindImplicitTKBndrs_Q_Tv kv_ns $ bindExplicitTKBndrs_Q_Tv ctxt_kind hs_tvs $ - thing_inside + newExpectedKind =<< kc_res_ki -- Why "_Tv" not "_Skol"? See third wrinkle in -- Note [Inferring kinds for type declarations] in TcTyClsDecls, @@ -1931,7 +1968,7 @@ kcLHsQTyVars_NonCusk name flav False -- not yet generalised flav - ; traceTc "kcLHsQTyVars: not-cusk" $ + ; traceTc "kcInferDeclHeader: not-cusk" $ vcat [ ppr name, ppr kv_ns, ppr hs_tvs , ppr scoped_kvs , ppr tc_tvs, ppr (mkTyConKind tc_binders res_kind) ] @@ -1940,8 +1977,414 @@ kcLHsQTyVars_NonCusk name flav ctxt_kind | tcFlavourIsOpen flav = TheKind liftedTypeKind | otherwise = AnyKind -kcLHsQTyVars_NonCusk _ _ (XLHsQTyVars nec) _ = noExtCon nec +kcInferDeclHeader _ _ (XLHsQTyVars nec) _ = noExtCon nec + +-- | Kind-check a declaration header against a standalone kind signature. +-- See Note [Arity inference in kcCheckDeclHeader_sig] +kcCheckDeclHeader_sig + :: Kind -- ^ Standalone kind signature, fully zonked! (zonkTcTypeToType) + -> Name -- ^ of the thing being checked + -> TyConFlavour -- ^ What sort of 'TyCon' is being checked + -> LHsQTyVars GhcRn -- ^ Binders in the header + -> TcM ContextKind -- ^ The result kind. AnyKind == no result signature + -> TcM TcTyCon -- ^ A suitably-kinded TcTyCon +kcCheckDeclHeader_sig kisig name flav ktvs kc_res_ki = + addTyConFlavCtxt name flav $ + pushTcLevelM_ $ + solveEqualities $ -- #16687 + bind_implicit (hsq_ext ktvs) $ \implicit_tcv_prs -> do + + -- Step 1: zip user-written binders with quantifiers from the kind signature. + -- For example: + -- + -- type F :: forall k -> k -> forall j. j -> Type + -- data F i a b = ... + -- + -- Results in the following 'zipped_binders': + -- + -- TyBinder LHsTyVarBndr + -- --------------------------------------- + -- ZippedBinder forall k -> i + -- ZippedBinder k -> a + -- ZippedBinder forall j. + -- ZippedBinder j -> b + -- + let (zipped_binders, excess_bndrs, kisig') = zipBinders kisig (hsq_explicit ktvs) + + -- Report binders that don't have a corresponding quantifier. + -- For example: + -- + -- type T :: Type -> Type + -- data T b1 b2 b3 = ... + -- + -- Here, b1 is zipped with Type->, while b2 and b3 are excess binders. + -- + unless (null excess_bndrs) $ failWithTc (tooManyBindersErr kisig' excess_bndrs) + + -- Convert each ZippedBinder to TyConBinder for tyConBinders + -- and to [(Name, TcTyVar)] for tcTyConScopedTyVars + (vis_tcbs, concat -> explicit_tv_prs) <- mapAndUnzipM zipped_to_tcb zipped_binders + + tcExtendNameTyVarEnv explicit_tv_prs $ do + + -- Check that inline kind annotations on binders are valid. + -- For example: + -- + -- type T :: Maybe k -> Type + -- data T (a :: Maybe j) = ... + -- + -- Here we unify Maybe k ~ Maybe j + mapM_ check_zipped_binder zipped_binders + + -- Kind-check the result kind annotation, if present: + -- + -- data T a b :: res_ki where + -- ^^^^^^^^^ + -- We do it here because at this point the environment has been + -- extended with both 'implicit_tcv_prs' and 'explicit_tv_prs'. + m_res_ki <- kc_res_ki >>= \ctx_k -> + case ctx_k of + AnyKind -> return Nothing + _ -> Just <$> newExpectedKind ctx_k + + -- Step 2: split off invisible binders. + -- For example: + -- + -- type F :: forall k1 k2. (k1, k2) -> Type + -- type family F + -- + -- Does 'forall k1 k2' become a part of 'tyConBinders' or 'tyConResKind'? + -- See Note [Arity inference in kcCheckDeclHeader_sig] + let (invis_binders, r_ki) = split_invis kisig' m_res_ki + + -- Convert each invisible TyCoBinder to TyConBinder for tyConBinders. + invis_tcbs <- mapM invis_to_tcb invis_binders + + -- Check that the inline result kind annotation is valid. + -- For example: + -- + -- type T :: Type -> Maybe k + -- type family T a :: Maybe j where + -- + -- Here we unify Maybe k ~ Maybe j + whenIsJust m_res_ki $ \res_ki -> + discardResult $ -- See Note [discardResult in kcCheckDeclHeader_sig] + unifyKind Nothing r_ki res_ki + + -- Zonk the implicitly quantified variables. + implicit_tv_prs <- mapSndM zonkTcTyVarToTyVar implicit_tcv_prs + + -- Build the final, generalized TcTyCon + let tcbs = vis_tcbs ++ invis_tcbs + all_tv_prs = implicit_tv_prs ++ explicit_tv_prs + tc = mkTcTyCon name tcbs r_ki all_tv_prs True flav + + traceTc "kcCheckDeclHeader_sig done:" $ vcat + [ text "tyConName = " <+> ppr (tyConName tc) + , text "kisig =" <+> debugPprType kisig + , text "tyConKind =" <+> debugPprType (tyConKind tc) + , text "tyConBinders = " <+> ppr (tyConBinders tc) + , text "tcTyConScopedTyVars" <+> ppr (tcTyConScopedTyVars tc) + , text "tyConResKind" <+> debugPprType (tyConResKind tc) + ] + return tc + where + -- Consider this declaration: + -- + -- type T :: forall a. forall b -> (a~b) => Proxy a -> Type + -- data T x p = MkT + -- + -- Here, we have every possible variant of ZippedBinder: + -- + -- TyBinder LHsTyVarBndr + -- ---------------------------------------------- + -- ZippedBinder forall {k}. + -- ZippedBinder forall (a::k). + -- ZippedBinder forall (b::k) -> x + -- ZippedBinder (a~b) => + -- ZippedBinder Proxy a -> p + -- + -- Given a ZippedBinder zipped_to_tcb produces: + -- + -- * TyConBinder for tyConBinders + -- * (Name, TcTyVar) for tcTyConScopedTyVars, if there's a user-written LHsTyVarBndr + -- + zipped_to_tcb :: ZippedBinder -> TcM (TyConBinder, [(Name, TcTyVar)]) + zipped_to_tcb zb = case zb of + + -- Inferred variable, no user-written binder. + -- Example: forall {k}. + ZippedBinder (Named (Bndr v Specified)) Nothing -> + return (mkNamedTyConBinder Specified v, []) + + -- Specified variable, no user-written binder. + -- Example: forall (a::k). + ZippedBinder (Named (Bndr v Inferred)) Nothing -> + return (mkNamedTyConBinder Inferred v, []) + + -- Constraint, no user-written binder. + -- Example: (a~b) => + ZippedBinder (Anon InvisArg bndr_ki) Nothing -> do + name <- newSysName (mkTyVarOccFS (fsLit "ev")) + let tv = mkTyVar name bndr_ki + return (mkAnonTyConBinder InvisArg tv, []) + + -- Non-dependent visible argument with a user-written binder. + -- Example: Proxy a -> + ZippedBinder (Anon VisArg bndr_ki) (Just b) -> + return $ + let v_name = getName b + tv = mkTyVar v_name bndr_ki + tcb = mkAnonTyConBinder VisArg tv + in (tcb, [(v_name, tv)]) + + -- Dependent visible argument with a user-written binder. + -- Example: forall (b::k) -> + ZippedBinder (Named (Bndr v Required)) (Just b) -> + return $ + let v_name = getName b + tcb = mkNamedTyConBinder Required v + in (tcb, [(v_name, v)]) + + -- 'zipBinders' does not produce any other variants of ZippedBinder. + _ -> panic "goVis: invalid ZippedBinder" + + -- Given an invisible binder that comes from 'split_invis', + -- convert it to TyConBinder. + invis_to_tcb :: TyCoBinder -> TcM TyConBinder + invis_to_tcb tb = do + (tcb, stv) <- zipped_to_tcb (ZippedBinder tb Nothing) + MASSERT(null stv) + return tcb + + -- similar to: bindImplicitTKBndrs_Tv + bind_implicit :: [Name] -> ([(Name,TcTyVar)] -> TcM a) -> TcM a + bind_implicit tv_names thing_inside = + do { let new_tv name = do { tcv <- newFlexiKindedTyVarTyVar name + ; return (name, tcv) } + ; tcvs <- mapM new_tv tv_names + ; tcExtendNameTyVarEnv tcvs (thing_inside tcvs) } + + -- Check that the inline kind annotation on a binder is valid + -- by unifying it with the kind of the quantifier. + check_zipped_binder :: ZippedBinder -> TcM () + check_zipped_binder (ZippedBinder _ Nothing) = return () + check_zipped_binder (ZippedBinder tb (Just b)) = + case unLoc b of + UserTyVar _ _ -> return () + KindedTyVar _ v v_hs_ki -> do + v_ki <- tcLHsKindSig (TyVarBndrKindCtxt (unLoc v)) v_hs_ki + discardResult $ -- See Note [discardResult in kcCheckDeclHeader_sig] + unifyKind (Just (HsTyVar noExtField NotPromoted v)) + (tyBinderType tb) + v_ki + XTyVarBndr nec -> noExtCon nec + + -- Split the invisible binders that should become a part of 'tyConBinders' + -- rather than 'tyConResKind'. + -- See Note [Arity inference in kcCheckDeclHeader_sig] + split_invis :: Kind -> Maybe Kind -> ([TyCoBinder], Kind) + split_invis sig_ki Nothing = + -- instantiate all invisible binders + splitPiTysInvisible sig_ki + split_invis sig_ki (Just res_ki) = + -- subtraction a la checkExpectedKind + let n_res_invis_bndrs = invisibleTyBndrCount res_ki + n_sig_invis_bndrs = invisibleTyBndrCount sig_ki + n_inst = n_sig_invis_bndrs - n_res_invis_bndrs + in splitPiTysInvisibleN n_inst sig_ki + +-- A quantifier from a kind signature zipped with a user-written binder for it. +data ZippedBinder = + ZippedBinder TyBinder (Maybe (LHsTyVarBndr GhcRn)) + +-- See Note [Arity inference in kcCheckDeclHeader_sig] +zipBinders + :: Kind -- kind signature + -> [LHsTyVarBndr GhcRn] -- user-written binders + -> ([ZippedBinder], -- zipped binders + [LHsTyVarBndr GhcRn], -- remaining user-written binders + Kind) -- remainder of the kind signature +zipBinders = zip_binders [] + where + zip_binders acc ki [] = (reverse acc, [], ki) + zip_binders acc ki (b:bs) = + case tcSplitPiTy_maybe ki of + Nothing -> (reverse acc, b:bs, ki) + Just (tb, ki') -> + let + (zb, bs') | zippable = (ZippedBinder tb (Just b), bs) + | otherwise = (ZippedBinder tb Nothing, b:bs) + zippable = + case tb of + Named (Bndr _ Specified) -> False + Named (Bndr _ Inferred) -> False + Named (Bndr _ Required) -> True + Anon InvisArg _ -> False + Anon VisArg _ -> True + in + zip_binders (zb:acc) ki' bs' + +tooManyBindersErr :: Kind -> [LHsTyVarBndr GhcRn] -> SDoc +tooManyBindersErr ki bndrs = + hang (text "Not a function kind:") + 4 (ppr ki) $$ + hang (text "but extra binders found:") + 4 (fsep (map ppr bndrs)) + +{- Note [Arity inference in kcCheckDeclHeader_sig] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Given a kind signature 'kisig' and a declaration header, kcCheckDeclHeader_sig +verifies that the declaration conforms to the signature. The end result is a +TcTyCon 'tc' such that: + + tyConKind tc == kisig + +This TcTyCon would be rather easy to produce if we didn't have to worry about +arity. Consider these declarations: + + type family S1 :: forall k. k -> Type + type family S2 (a :: k) :: Type + +Both S1 and S2 can be given the same standalone kind signature: + + type S2 :: forall k. k -> Type + +And, indeed, tyConKind S1 == tyConKind S2. However, tyConKind is built from +tyConBinders and tyConResKind, such that + + tyConKind tc == mkTyConKind (tyConBinders tc) (tyConResKind tc) + +For S1 and S2, tyConBinders and tyConResKind are different: + + tyConBinders S1 == [] + tyConResKind S1 == forall k. k -> Type + tyConKind S1 == forall k. k -> Type + + tyConBinders S2 == [spec k, anon-vis (a :: k)] + tyConResKind S2 == Type + tyConKind S1 == forall k. k -> Type + +This difference determines the arity: + + tyConArity tc == length (tyConBinders tc) + +That is, the arity of S1 is 0, while the arity of S2 is 2. + +'kcCheckDeclHeader_sig' needs to infer the desired arity to split the standalone +kind signature into binders and the result kind. It does so in two rounds: +1. zip user-written binders (vis_tcbs) +2. split off invisible binders (invis_tcbs) + +Consider the following declarations: + + type F :: Type -> forall j. j -> forall k1 k2. (k1, k2) -> Type + type family F a b + + type G :: Type -> forall j. j -> forall k1 k2. (k1, k2) -> Type + type family G a b :: forall r2. (r1, r2) -> Type + +In step 1 (zip user-written binders), we zip the quantifiers in the signature +with the binders in the header using 'zipBinders'. In both F and G, this results in +the following zipped binders: + + TyBinder LHsTyVarBndr + --------------------------------------- + ZippedBinder Type -> a + ZippedBinder forall j. + ZippedBinder j -> b + + +At this point, we have accumulated three zipped binders which correspond to a +prefix of the standalone kind signature: + + Type -> forall j. j -> ... + +In step 2 (split off invisible binders), we have to decide how much remaining +invisible binders of the standalone kind signature to split off: + + forall k1 k2. (k1, k2) -> Type + ^^^^^^^^^^^^^ + split off or not? + +This decision is made in 'split_invis': + +* If a user-written result kind signature is not provided, as in F, + then split off all invisible binders. This is why we need special treatment + for AnyKind. +* If a user-written result kind signature is provided, as in G, + then do as checkExpectedKind does and split off (n_sig - n_res) binders. + That is, split off such an amount of binders that the remainder of the + standalone kind signature and the user-written result kind signature have the + same amount of invisible quantifiers. + +For F, split_invis splits away all invisible binders, and we have 2: + + forall k1 k2. (k1, k2) -> Type + ^^^^^^^^^^^^^ + split away both binders + +The resulting arity of F is 3+2=5. (length vis_tcbs = 3, + length invis_tcbs = 2, + length tcbs = 5) + +For G, split_invis decides to split off 1 invisible binder, so that we have the +same amount of invisible quantifiers left: + + res_ki = forall r2. (r1, r2) -> Type + kisig = forall k1 k2. (k1, k2) -> Type + ^^^ + split off this one. + +The resulting arity of G is 3+1=4. (length vis_tcbs = 3, + length invis_tcbs = 1, + length tcbs = 4) + +-} + +{- Note [discardResult in kcCheckDeclHeader_sig] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We use 'unifyKind' to check inline kind annotations in declaration headers +against the signature. + + type T :: [i] -> Maybe j -> Type + data T (a :: [k1]) (b :: Maybe k2) :: Type where ... + +Here, we will unify: + + [k1] ~ [i] + Maybe k2 ~ Maybe j + Type ~ Type + +The end result is that we fill in unification variables k1, k2: + + k1 := i + k2 := j + +We also validate that the user isn't confused: + + type T :: Type -> Type + data T (a :: Bool) = ... + +This will report that (Type ~ Bool) failed to unify. + +Now, consider the following example: + + type family Id a where Id x = x + type T :: Bool -> Type + type T (a :: Id Bool) = ... + +We will unify (Bool ~ Id Bool), and this will produce a non-reflexive coercion. +However, we are free to discard it, as the kind of 'T' is determined by the +signature, not by the inline kind annotation: + + we have T :: Bool -> Type + rather than T :: Id Bool -> Type + +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] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1956,11 +2399,11 @@ be a tough nut. Previously, we laboriously (with help from the renamer) tried to give T the polymoprhic kind T :: forall ka -> ka -> kappa -> Type -where kappa is a unification variable, even in the getInitialKinds -phase (which is what kcLHsQTyVars_NonCusk is all about). But +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 kcLHsQTyVars_NonCusk give T a straightforward +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. @@ -1970,7 +2413,7 @@ But notice that (#16322 comment:3) * The algorithm successfully kind-checks this declaration: data T2 ka (a::ka) = MkT2 (T2 Type a) - Starting with (getInitialKinds) + Starting with (inferInitialKinds) T2 :: (kappa1 :: kappa2 :: *) -> (kappa3 :: kappa4 :: *) -> * we get kappa4 := kappa1 -- from the (a:ka) kind signature @@ -2037,7 +2480,7 @@ Then `a` first appears /after/ `f`, so the kind of `T2` should be: T2 :: forall f a. f a -> Type -In order to make this distinction, we need to know (in kcLHsQTyVars) which +In order to make this distinction, we need to know (in kcCheckDeclHeader) which type variables have been bound by the parent class (if there is one). With the class-bound variables in hand, we can ensure that we always quantify these first. @@ -2218,7 +2661,6 @@ tcHsQTyVarBndr _ new_tv (KindedTyVar _ (L _ tv_nm) lhs_kind) tcHsQTyVarBndr _ _ (XTyVarBndr nec) = noExtCon nec - -------------------------------------- -- Binding type/class variables in the -- kind-checking and typechecking phases @@ -2238,7 +2680,7 @@ bindTyClTyVars tycon_name thing_inside ; tcExtendNameTyVarEnv scoped_prs $ thing_inside binders res_kind } --- getInitialKind has made a suitably-shaped kind for the type or class +-- inferInitialKind has made a suitably-shaped kind for the type or class -- Look it up in the local environment. This is used only for tycons -- that we're currently type-checking, so we're sure to find a TcTyCon. kcLookupTcTyCon :: Name -> TcM TcTyCon @@ -2539,6 +2981,16 @@ checkDataKindSig data_sort kind = do then text "Perhaps you intended to use UnliftedNewtypes" else empty ] +-- | Checks that the result kind of a class is exactly `Constraint`, rejecting +-- type synonyms and type families that reduce to `Constraint`. See #16826. +checkClassKindSig :: Kind -> TcM () +checkClassKindSig kind = checkTc (tcIsConstraintKind kind) err_msg + where + err_msg :: SDoc + err_msg = + text "Kind signature on a class must end with" <+> ppr constraintKind $$ + text "unobscured by type families" + tcbVisibilities :: TyCon -> [Type] -> [TyConBndrVis] -- Result is in 1-1 correpondence with orig_args tcbVisibilities tc orig_args diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs index e9d75fb17f..c047d13cc8 100644 --- a/compiler/typecheck/TcInstDcls.hs +++ b/compiler/typecheck/TcInstDcls.hs @@ -746,6 +746,7 @@ tcDataFamInstDecl mb_clsinfo L _ [] -> Nothing L _ preds -> Just $ DerivInfo { di_rep_tc = rep_tc + , di_scoped_tvs = mkTyVarNamePairs (tyConTyVars rep_tc) , di_clauses = preds , di_ctxt = tcMkDataFamInstCtxt decl } diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs index a0297c61f5..8a15d9cd44 100644 --- a/compiler/typecheck/TcMType.hs +++ b/compiler/typecheck/TcMType.hs @@ -1587,11 +1587,10 @@ quantifyTyVars dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs }) = return Nothing -- this can happen for a covar that's associated with -- a coercion hole. Test case: typecheck/should_compile/T2494 - | not (isTcTyVar tkv) -- I don't think this can ever happen. - -- Hence the assert - = ASSERT2( False, text "quantifying over a TyVar" <+> ppr tkv) - return (Just tkv) - + | not (isTcTyVar tkv) + = return (Just tkv) -- For associated types in a class with a standalone + -- kind signature, we have the class variables in + -- scope, and they are TyVars not TcTyVars | otherwise = do { deflt_done <- defaultTyVar default_kind tkv ; case deflt_done of diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index 69c909f4a1..904f80827f 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -154,13 +154,17 @@ tcTyClGroup :: TyClGroup GhcRn -- See Note [TyClGroups and dependency analysis] in GHC.Hs.Decls tcTyClGroup (TyClGroup { group_tyclds = tyclds , group_roles = roles + , group_kisigs = kisigs , group_instds = instds }) = do { let role_annots = mkRoleAnnotEnv roles - -- Step 1: Typecheck the type/class declarations + -- Step 1: Typecheck the standalone kind signatures and type/class declarations ; traceTc "---- tcTyClGroup ---- {" empty ; traceTc "Decls for" (ppr (map (tcdName . unLoc) tyclds)) - ; (tyclss, data_deriv_info) <- tcTyClDecls tyclds role_annots + ; (tyclss, data_deriv_info) <- + tcExtendKindEnv (mkPromotionErrorEnv tyclds) $ -- See Note [Type environment evolution] + do { kisig_env <- mkNameEnv <$> traverse tcStandaloneKindSig kisigs + ; tcTyClDecls tyclds kisig_env role_annots } -- Step 1.5: Make sure we don't have any type synonym cycles ; traceTc "Starting synonym cycle check" (ppr tyclss) @@ -196,16 +200,19 @@ tcTyClGroup (TyClGroup { group_tyclds = tyclds tcTyClGroup (XTyClGroup nec) = noExtCon nec +-- Gives the kind for every TyCon that has a standalone kind signature +type KindSigEnv = NameEnv Kind + tcTyClDecls :: [LTyClDecl GhcRn] + -> KindSigEnv -> RoleAnnotEnv -> TcM ([TyCon], [DerivInfo]) -tcTyClDecls tyclds role_annots - = tcExtendKindEnv promotion_err_env $ --- See Note [Type environment evolution] - do { -- Step 1: kind-check this group and returns the final +tcTyClDecls tyclds kisig_env role_annots + = do { -- Step 1: kind-check this group and returns the final -- (possibly-polymorphic) kind of each TyCon and Class -- See Note [Kind checking for type and class decls] - tc_tycons <- kcTyClGroup tyclds + tc_tycons <- kcTyClGroup kisig_env tyclds ; traceTc "tcTyAndCl generalized kinds" (vcat (map ppr_tc_tycon tc_tycons)) -- Step 2: type-check all groups together, returning @@ -236,7 +243,6 @@ tcTyClDecls tyclds role_annots ; return (tycons, concat data_deriv_infos) } } where - promotion_err_env = mkPromotionErrorEnv tyclds ppr_tc_tycon tc = parens (sep [ ppr (tyConName tc) <> comma , ppr (tyConBinders tc) <> comma , ppr (tyConResKind tc) @@ -315,7 +321,7 @@ Consider data T (a :: *) = MkT (S a) -- Has CUSK data S a = MkS (T Int) (S a) -- No CUSK -Via getInitialKinds we get +Via inferInitialKinds we get T :: * -> * S :: kappa -> * @@ -352,7 +358,7 @@ General type functions can be recursive, and hence, appear in `alg_decls'. The kind of an open type family is solely determinded by its kind signature; hence, only kind signatures participate in the construction of the initial -kind environment (as constructed by `getInitialKind'). In fact, we ignore +kind environment (as constructed by `inferInitialKind'). In fact, we ignore instances of families altogether in the following. However, we need to include the kinds of *associated* families into the construction of the initial kind environment. (This is handled by `allDecls'). @@ -371,7 +377,7 @@ TcTyCons are used for two distinct purposes 2. When checking a type/class declaration (in module TcTyClsDecls), we come upon knowledge of the eventual tycon in bits and pieces. - S1) First, we use getInitialKinds to look over the user-provided + S1) First, we use inferInitialKinds to look over the user-provided kind signature of a tycon (including, for example, the number of parameters written to the tycon) to get an initial shape of the tycon's kind. We record that shape in a TcTyCon. @@ -397,7 +403,7 @@ TcTyCons are used for two distinct purposes 4. tyConScopedTyVars. A challenging piece in all of this is that we end up taking three separate passes over every declaration: - - one in getInitialKind (this pass look only at the head, not the body) + - 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) @@ -437,7 +443,7 @@ We do the following steps: MkB :-> DataConPE 2. kcTyCLGroup - - Do getInitialKinds, which will signal a promotion + - Do inferInitialKinds, which will signal a promotion error if B is used in any of the kinds needed to initialise B's kind (e.g. (a :: Type)) here @@ -481,9 +487,9 @@ to Note [Single function non-recursive binding special-case]: Unfortunately this requires reworking a bit of the code in 'kcLTyClDecl' so I've decided to punt unless someone shouts about it. -Note [Don't process associated types in kcLHsQTyVars] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Previously, we processed associated types in the thing_inside in kcLHsQTyVars, +Note [Don't process associated types in getInitialKind] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Previously, we processed associated types in the thing_inside in getInitialKind, but this was wrong -- we want to do ATs sepearately. The consequence for not doing it this way is #15142: @@ -496,7 +502,7 @@ kappa ~ Type, but this gets deferred because we bumped the TcLevel as we bring unified with Type. And then, when we generalize the kind of ListToTuple (which indeed has a CUSK, according to the rules), we skolemize the free metavariable kappa. Note that we wouldn't skolemize kappa when generalizing the kind of ListTuple, -because the solveEqualities in kcLHsQTyVars is at TcLevel 1 and so kappa[1] +because the solveEqualities in kcInferDeclHeader is at TcLevel 1 and so kappa[1] will unify with Type. Bottom line: as associated types should have no effect on a CUSK enclosing class, @@ -505,13 +511,13 @@ been generalized. -} -kcTyClGroup :: [LTyClDecl GhcRn] -> TcM [TcTyCon] +kcTyClGroup :: KindSigEnv -> [LTyClDecl GhcRn] -> TcM [TcTyCon] -- Kind check this group, kind generalize, and return the resulting local env -- This binds the TyCons and Classes of the group, but not the DataCons -- See Note [Kind checking for type and class decls] -- and Note [Inferring kinds for type declarations] -kcTyClGroup decls +kcTyClGroup kisig_env decls = do { mod <- getModule ; traceTc "---- kcTyClGroup ---- {" (text "module" <+> ppr mod $$ vcat (map ppr decls)) @@ -523,19 +529,26 @@ kcTyClGroup decls -- See Note [Kind checking for type and class decls] ; cusks_enabled <- xoptM LangExt.CUSKs - ; let (cusk_decls, no_cusk_decls) - = partition (hsDeclHasCusk cusks_enabled . unLoc) decls + ; let (kindless_decls, kinded_decls) = partitionWith get_kind decls + + get_kind d + | Just ki <- lookupNameEnv kisig_env (tcdName (unLoc d)) + = Right (d, SAKS ki) + + | cusks_enabled && hsDeclHasCusk (unLoc d) + = Right (d, CUSK) - ; poly_cusk_tcs <- getInitialKinds True cusk_decls + | otherwise = Left d - ; mono_tcs - <- tcExtendKindEnvWithTyCons poly_cusk_tcs $ + ; checked_tcs <- checkInitialKinds kinded_decls + ; inferred_tcs + <- tcExtendKindEnvWithTyCons checked_tcs $ pushTcLevelM_ $ -- We are going to kind-generalise, so -- unification variables in here must -- be one level in solveEqualities $ do { -- Step 1: Bind kind variables for all decls - mono_tcs <- getInitialKinds False no_cusk_decls + mono_tcs <- inferInitialKinds kindless_decls ; traceTc "kcTyClGroup: initial kinds" $ ppr_tc_kinds mono_tcs @@ -546,7 +559,7 @@ kcTyClGroup decls -- See Note [Type environment evolution] ; poly_kinds <- xoptM LangExt.PolyKinds ; tcExtendKindEnvWithTyCons mono_tcs $ - mapM_ kcLTyClDecl (if poly_kinds then no_cusk_decls else decls) + mapM_ kcLTyClDecl (if poly_kinds then kindless_decls else decls) -- See Note [Skip decls with CUSKs in kcLTyClDecl] ; return mono_tcs } @@ -555,9 +568,9 @@ kcTyClGroup decls -- Finally, go through each tycon and give it its final kind, -- with all the required, specified, and inferred variables -- in order. - ; poly_no_cusk_tcs <- mapAndReportM generaliseTcTyCon mono_tcs + ; generalized_tcs <- mapAndReportM generaliseTcTyCon inferred_tcs - ; let poly_tcs = poly_cusk_tcs ++ poly_no_cusk_tcs + ; let poly_tcs = checked_tcs ++ generalized_tcs ; traceTc "---- kcTyClGroup end ---- }" (ppr_tc_kinds poly_tcs) ; return poly_tcs } @@ -772,11 +785,11 @@ How it works These design choices are implemented by two completely different code paths for - * Declarations with a complete user-specified kind signature (CUSK) - Handed by the CUSK case of kcLHsQTyVars. + * Declarations with a standalone kind signature or a complete user-specified + kind signature (CUSK). Handled by the kcCheckDeclHeader. - * Declarations without a CUSK are handled by kcTyClDecl; see - Note [Inferring kinds for type declarations]. + * Declarations without a kind signature (standalone or CUSK) are handled by + kcInferDeclHeader; see Note [Inferring kinds for type declarations]. Note that neither code path worries about point (4) above, as this is nicely handled by not mangling the res_kind. (Mangling res_kinds is done @@ -821,7 +834,7 @@ that do not have a CUSK. Consider We do kind inference as follows: -* Step 1: getInitialKinds, and in particular kcLHsQTyVars_NonCusk. +* Step 1: inferInitialKinds, and in particular kcInferDeclHeader. Make a unification variable for each of the Required and Specified type varialbes in the header. @@ -997,17 +1010,34 @@ mk_prom_err_env decl -- Works for family declarations too -------------- -getInitialKinds :: Bool -> [LTyClDecl GhcRn] -> TcM [TcTyCon] +inferInitialKinds :: [LTyClDecl GhcRn] -> TcM [TcTyCon] -- Returns a TcTyCon for each TyCon bound by the decls, -- each with its initial kind -getInitialKinds cusk decls - = do { traceTc "getInitialKinds {" empty - ; tcs <- concatMapM (addLocM (getInitialKind cusk)) decls - ; traceTc "getInitialKinds done }" empty +inferInitialKinds decls + = do { traceTc "inferInitialKinds {" $ ppr (map (tcdName . unLoc) decls) + ; tcs <- concatMapM infer_initial_kind decls + ; traceTc "inferInitialKinds done }" empty ; return tcs } + where + infer_initial_kind = addLocM (getInitialKind InitialKindInfer) + +-- Check type/class declarations against their standalone kind signatures or +-- CUSKs, producing a generalized TcTyCon for each. +checkInitialKinds :: [(LTyClDecl GhcRn, SAKS_or_CUSK)] -> TcM [TcTyCon] +checkInitialKinds decls + = do { traceTc "checkInitialKinds {" $ ppr (mapFst (tcdName . unLoc) decls) + ; tcs <- concatMapM check_initial_kind decls + ; traceTc "checkInitialKinds done }" empty + ; return tcs } + where + check_initial_kind (ldecl, msig) = + addLocM (getInitialKind (InitialKindCheck msig)) ldecl + +-- | Get the initial kind of a TyClDecl, either generalized or non-generalized, +-- depending on the 'InitialKindStrategy'. +getInitialKind :: InitialKindStrategy -> TyClDecl GhcRn -> TcM [TcTyCon] -getInitialKind :: Bool -> TyClDecl GhcRn -> TcM [TcTyCon] -- Allocate a fresh kind variable for each TyCon and Class -- For each tycon, return a TcTyCon with kind k -- where k is the kind of tc, derived from the LHS @@ -1020,108 +1050,208 @@ getInitialKind :: Bool -> TyClDecl GhcRn -> TcM [TcTyCon] -- * The kind signatures on type-variable binders -- * The result kinds signature on a TyClDecl -- --- No family instances are passed to getInitialKinds - -getInitialKind cusk +-- No family instances are passed to checkInitialKinds/inferInitialKinds +getInitialKind strategy (ClassDecl { tcdLName = dL->L _ name , tcdTyVars = ktvs , tcdATs = ats }) - = do { tycon <- kcLHsQTyVars name ClassFlavour cusk ktvs $ - return constraintKind - ; let parent_tv_prs = tcTyConScopedTyVars tycon - -- See Note [Don't process associated types in kcLHsQTyVars] - ; inner_tcs <- tcExtendNameTyVarEnv parent_tv_prs $ - getFamDeclInitialKinds cusk (Just tycon) ats - ; return (tycon : inner_tcs) } - -getInitialKind cusk + = do { cls <- kcDeclHeader strategy name ClassFlavour ktvs $ + return (TheKind constraintKind) + ; let parent_tv_prs = tcTyConScopedTyVars cls + -- See Note [Don't process associated types in getInitialKind] + ; inner_tcs <- + tcExtendNameTyVarEnv parent_tv_prs $ + mapM (addLocM (getAssocFamInitialKind cls)) ats + ; return (cls : inner_tcs) } + where + getAssocFamInitialKind cls = + case strategy of + InitialKindInfer -> get_fam_decl_initial_kind (Just cls) + InitialKindCheck _ -> check_initial_kind_assoc_fam cls + +getInitialKind strategy (DataDecl { tcdLName = dL->L _ name , tcdTyVars = ktvs , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig , dd_ND = new_or_data } }) = do { let flav = newOrDataToFlavour new_or_data - ; tc <- kcLHsQTyVars name flav cusk ktvs $ - -- See Note [Implementation of UnliftedNewtypes] - do { unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes - ; case m_sig of - Just ksig -> tcLHsKindSig (DataKindCtxt name) ksig - Nothing - | NewType <- new_or_data - , unlifted_newtypes -> newOpenTypeKind - | otherwise -> pure liftedTypeKind - } + ctxt = DataKindCtxt name + ; tc <- kcDeclHeader strategy name flav ktvs $ + case m_sig of + Just ksig -> TheKind <$> tcLHsKindSig ctxt ksig + Nothing -> dataDeclDefaultResultKind new_or_data ; return [tc] } -getInitialKind cusk (FamDecl { tcdFam = decl }) - = do { tc <- getFamDeclInitialKind cusk Nothing decl +getInitialKind InitialKindInfer (FamDecl { tcdFam = decl }) + = do { tc <- get_fam_decl_initial_kind Nothing decl ; return [tc] } -getInitialKind cusk (SynDecl { tcdLName = dL->L _ name - , tcdTyVars = ktvs - , tcdRhs = rhs }) - = do { cusks_enabled <- xoptM LangExt.CUSKs - ; tycon <- kcLHsQTyVars name TypeSynonymFlavour cusk ktvs $ - case kind_annotation cusks_enabled rhs of - Just ksig -> tcLHsKindSig (TySynKindCtxt name) ksig - Nothing -> newMetaKindVar - ; return [tycon] } - where - -- Keep this synchronized with 'hsDeclHasCusk'. - kind_annotation - :: Bool -- cusks_enabled? - -> LHsType GhcRn -- rhs - -> Maybe (LHsKind GhcRn) - kind_annotation False = const Nothing - kind_annotation True = go - where - go (dL->L _ ty) = case ty of - HsParTy _ lty -> go lty - HsKindSig _ _ k -> Just k - _ -> Nothing +getInitialKind (InitialKindCheck msig) (FamDecl { tcdFam = + FamilyDecl { fdLName = unLoc -> name + , fdTyVars = ktvs + , fdResultSig = unLoc -> resultSig + , fdInfo = info } } ) + = do { let flav = getFamFlav Nothing info + ctxt = TyFamResKindCtxt name + ; tc <- kcDeclHeader (InitialKindCheck msig) name flav ktvs $ + case famResultKindSignature resultSig of + Just ksig -> TheKind <$> tcLHsKindSig ctxt ksig + Nothing -> + case msig of + CUSK -> return (TheKind liftedTypeKind) + SAKS _ -> return AnyKind + ; return [tc] } + +getInitialKind strategy + (SynDecl { tcdLName = dL->L _ name + , tcdTyVars = ktvs + , tcdRhs = rhs }) + = do { let ctxt = TySynKindCtxt name + ; tc <- kcDeclHeader strategy name TypeSynonymFlavour ktvs $ + case hsTyKindSig rhs of + Just rhs_sig -> TheKind <$> tcLHsKindSig ctxt rhs_sig + Nothing -> return AnyKind + ; return [tc] } getInitialKind _ (DataDecl _ _ _ _ (XHsDataDefn nec)) = noExtCon nec +getInitialKind _ (FamDecl {tcdFam = XFamilyDecl nec}) = noExtCon nec getInitialKind _ (XTyClDecl nec) = noExtCon nec ---------------------------------- -getFamDeclInitialKinds - :: Bool -- ^ True <=> cusk - -> Maybe TyCon -- ^ Just cls <=> this is an associated family of class cls - -> [LFamilyDecl GhcRn] - -> TcM [TcTyCon] -getFamDeclInitialKinds cusk mb_parent_tycon decls - = mapM (addLocM (getFamDeclInitialKind cusk mb_parent_tycon)) decls - -getFamDeclInitialKind - :: Bool -- ^ True <=> cusk - -> Maybe TyCon -- ^ Just cls <=> this is an associated family of class cls +get_fam_decl_initial_kind + :: Maybe TcTyCon -- ^ Just cls <=> this is an associated family of class cls -> FamilyDecl GhcRn -> TcM TcTyCon -getFamDeclInitialKind parent_cusk mb_parent_tycon - decl@(FamilyDecl { fdLName = (dL->L _ name) - , fdTyVars = ktvs - , fdResultSig = (dL->L _ resultSig) - , fdInfo = info }) - = do { cusks_enabled <- xoptM LangExt.CUSKs - ; kcLHsQTyVars name flav (fam_cusk cusks_enabled) ktvs $ - case resultSig of - KindSig _ ki -> tcLHsKindSig ctxt ki - TyVarSig _ (dL->L _ (KindedTyVar _ _ ki)) -> tcLHsKindSig ctxt ki - _ -- open type families have * return kind by default - | tcFlavourIsOpen flav -> return liftedTypeKind - -- closed type families have their return kind inferred - -- by default - | otherwise -> newMetaKindVar - } +get_fam_decl_initial_kind mb_parent_tycon + FamilyDecl { fdLName = (dL->L _ name) + , fdTyVars = ktvs + , fdResultSig = (dL->L _ resultSig) + , fdInfo = info } + = kcDeclHeader InitialKindInfer name flav ktvs $ + case resultSig of + KindSig _ ki -> TheKind <$> tcLHsKindSig ctxt ki + TyVarSig _ (dL->L _ (KindedTyVar _ _ ki)) -> TheKind <$> tcLHsKindSig ctxt ki + _ -- open type families have * return kind by default + | tcFlavourIsOpen flav -> return (TheKind liftedTypeKind) + -- closed type families have their return kind inferred + -- by default + | otherwise -> return AnyKind where - assoc_with_no_cusk = isJust mb_parent_tycon && not parent_cusk - fam_cusk cusks_enabled = famDeclHasCusk cusks_enabled assoc_with_no_cusk decl - flav = case info of - DataFamily -> DataFamilyFlavour mb_parent_tycon - OpenTypeFamily -> OpenTypeFamilyFlavour mb_parent_tycon - ClosedTypeFamily _ -> ASSERT( isNothing mb_parent_tycon ) - ClosedTypeFamilyFlavour - ctxt = TyFamResKindCtxt name -getFamDeclInitialKind _ _ (XFamilyDecl nec) = noExtCon nec + flav = getFamFlav mb_parent_tycon info + ctxt = TyFamResKindCtxt name +get_fam_decl_initial_kind _ (XFamilyDecl nec) = noExtCon nec + +-- See Note [Standalone kind signatures for associated types] +check_initial_kind_assoc_fam + :: TcTyCon -- parent class + -> FamilyDecl GhcRn + -> TcM TcTyCon +check_initial_kind_assoc_fam cls + FamilyDecl + { fdLName = unLoc -> name + , fdTyVars = ktvs + , fdResultSig = unLoc -> resultSig + , fdInfo = info } + = kcDeclHeader (InitialKindCheck CUSK) name flav ktvs $ + case famResultKindSignature resultSig of + Just ksig -> TheKind <$> tcLHsKindSig ctxt ksig + Nothing -> return (TheKind liftedTypeKind) + where + ctxt = TyFamResKindCtxt name + flav = getFamFlav (Just cls) info +check_initial_kind_assoc_fam _ (XFamilyDecl nec) = noExtCon nec + +{- Note [Standalone kind signatures for associated types] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +If associated types had standalone kind signatures, would they wear them + +---------------------------+------------------------------ + like this? (OUT) | or like this? (IN) +---------------------------+------------------------------ + type T :: Type -> Type | class C a where + class C a where | type T :: Type -> Type + type T a | type T a + +The (IN) variant is syntactically ambiguous: + + class C a where + type T :: a -- standalone kind signature? + type T :: a -- declaration header? + +The (OUT) variant does not suffer from this issue, but it might not be the +direction in which we want to take Haskell: we seek to unify type families and +functions, and, by extension, associated types with class methods. And yet we +give class methods their signatures inside the class, not outside. Neither do +we have the counterpart of InstanceSigs for StandaloneKindSignatures. + +For now, we dodge the question by using CUSKs for associated types instead of +standalone kind signatures. This is a simple addition to the rule we used to +have before standalone kind signatures: + + old rule: associated type has a CUSK iff its parent class has a CUSK + new rule: associated type has a CUSK iff its parent class has a CUSK or a standalone kind signature + +-} + +-- See Note [Data declaration default result kind] +dataDeclDefaultResultKind :: NewOrData -> TcM ContextKind +dataDeclDefaultResultKind new_or_data = do + -- See Note [Implementation of UnliftedNewtypes] + unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes + return $ case new_or_data of + NewType | unlifted_newtypes -> OpenKind + _ -> TheKind liftedTypeKind + +{- Note [Data declaration default result kind] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +When the user has not written an inline result kind annotation on a data +declaration, we assume it to be 'Type'. That is, the following declarations +D1 and D2 are considered equivalent: + + data D1 where ... + data D2 :: Type where ... + +The consequence of this assumption is that we reject D3 even though we +accept D4: + + data D3 where + MkD3 :: ... -> D3 param + + data D4 :: Type -> Type where + MkD4 :: ... -> D4 param + +However, there's a twist: when -XUnliftedNewtypes are enabled, we must relax +the assumed result kind to (TYPE r) for newtypes: + + newtype D5 where + MkD5 :: Int# -> D5 + +dataDeclDefaultResultKind takes care to produce the appropriate result kind. +-} + +--------------------------------- +getFamFlav + :: Maybe TcTyCon -- ^ Just cls <=> this is an associated family of class cls + -> FamilyInfo pass + -> TyConFlavour +getFamFlav mb_parent_tycon info = + case info of + DataFamily -> DataFamilyFlavour mb_parent_tycon + OpenTypeFamily -> OpenTypeFamilyFlavour mb_parent_tycon + ClosedTypeFamily _ -> ASSERT( isNothing mb_parent_tycon ) -- See Note [Closed type family mb_parent_tycon] + ClosedTypeFamilyFlavour + +{- Note [Closed type family mb_parent_tycon] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +There's no way to write a closed type family inside a class declaration: + + class C a where + type family F a where -- error: parse error on input ‘where’ + +In fact, it is not clear what the meaning of such a declaration would be. +Therefore, 'mb_parent_tycon' of any closed type family has to be Nothing. +-} ------------------------------------------------------------------------ kcLTyClDecl :: LTyClDecl GhcRn -> TcM () @@ -1139,7 +1269,7 @@ kcTyClDecl :: TyClDecl GhcRn -> TcM () -- This function is used solely for its side effect on kind variables -- NB kind signatures on the type variables and -- result kind signature have already been dealt with --- by getInitialKind, so we can ignore them here. +-- by inferInitialKind, so we can ignore them here. kcTyClDecl (DataDecl { tcdLName = (dL->L _ name) , tcdDataDefn = defn }) @@ -1150,7 +1280,7 @@ kcTyClDecl (DataDecl { tcdLName = (dL->L _ name) -- See Note [Implementation of UnliftedNewtypes] STEP 2 ; kcConDecls new_or_data (tyConResKind tyCon) cons } - -- hs_tvs and dd_kindSig already dealt with in getInitialKind + -- hs_tvs and dd_kindSig already dealt with in inferInitialKind -- This must be a GADT-style decl, -- (see invariants of DataDefn declaration) -- so (a) we don't need to bring the hs_tvs into scope, because the @@ -1170,7 +1300,7 @@ kcTyClDecl (SynDecl { tcdLName = dL->L _ name, tcdRhs = rhs }) = bindTyClTyVars name $ \ _ res_kind -> discardResult $ tcCheckLHsType rhs res_kind -- NB: check against the result kind that we allocated - -- in getInitialKinds. + -- in inferInitialKinds. kcTyClDecl (ClassDecl { tcdLName = (dL->L _ name) , tcdCtxt = ctxt, tcdSigs = sigs }) @@ -1304,7 +1434,7 @@ corner, to pass to kcConDecl c.f. #16828. Hence the splitPiTys here. I am a bit concerned about tycons with a declaration like data T a :: Type -> forall k. k -> Type where ... -It does not have a CUSK, so kcLHsQTyVars_NonCusk will make a TcTyCon +It does not have a CUSK, so kcInferDeclHeader will make a TcTyCon with tyConResKind of Type -> forall k. k -> Type. Even that is fine: the splitPiTys will look past the forall. But I'm bothered about what if the type "in the corner" metions k? This is incredibly @@ -1468,7 +1598,7 @@ Expected behavior of UnliftedNewtypes: What follows is a high-level overview of the implementation of the proposal. -STEP 1: Getting the initial kind, as done by getInitialKind. We have +STEP 1: Getting the initial kind, as done by inferInitialKind. We have two sub-cases (assuming we have a newtype and -XUnliftedNewtypes is enabled): * With a CUSK: no change in kind-checking; the tycon is given the kind @@ -1489,7 +1619,7 @@ enabled (we use r0 to denote a unification variable): newtype Foo rep = MkFoo (forall (a :: TYPE rep). a) + kcConDecl unifies (TYPE r0) with (TYPE rep), where (TYPE r0) - is the kind that getInitialKind invented for (Foo rep). + is the kind that inferInitialKind invented for (Foo rep). data Color = Red | Blue type family Interpret (x :: Color) :: RuntimeRep where @@ -1587,6 +1717,10 @@ wiredInDerivInfo tycon decl | DataDecl { tcdDataDefn = dataDefn } <- decl , HsDataDefn { dd_derivs = derivs } <- dataDefn = [ DerivInfo { di_rep_tc = tycon + , di_scoped_tvs = + if isFunTyCon tycon || isPrimTyCon tycon + then [] -- no tyConTyVars + else mkTyVarNamePairs (tyConTyVars tycon) , di_clauses = unLoc derivs , di_ctxt = tcMkDeclCtxt decl } ] wiredInDerivInfo _ _ = [] @@ -1645,8 +1779,7 @@ tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs = fixM $ \ clas -> -- We need the knot because 'clas' is passed into tcClassATs bindTyClTyVars class_name $ \ binders res_kind -> - do { MASSERT2( tcIsConstraintKind res_kind - , ppr class_name $$ ppr res_kind ) + do { checkClassKindSig res_kind ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr binders) ; let tycon_name = class_name -- We use the same name roles = roles_info tycon_name -- for TyCon and Class @@ -1983,7 +2116,8 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info -- Process the equations, creating CoAxBranches ; let tc_fam_tc = mkTcTyCon tc_name binders res_kind - [] False {- this doesn't matter here -} + noTcTyConScopedTyVars + False {- this doesn't matter here -} ClosedTypeFamilyFlavour ; branches <- mapAndReportM (tcTyFamInstEqn tc_fam_tc NotAssociated) eqns @@ -2082,7 +2216,7 @@ tcDataDefn err_ctxt (HsDataDefn { dd_ND = new_or_data, dd_cType = cType , dd_ctxt = ctxt , dd_kindSig = mb_ksig -- Already in tc's kind - -- via getInitialKinds + -- via inferInitialKinds , dd_cons = cons , dd_derivs = derivs }) = do { gadt_syntax <- dataDeclChecks tc_name new_or_data ctxt cons @@ -2122,7 +2256,11 @@ tcDataDefn err_ctxt stupid_theta tc_rhs (VanillaAlgTyCon tc_rep_nm) gadt_syntax) } + ; tctc <- tcLookupTcTyCon tc_name + -- 'tctc' is a 'TcTyCon' and has the 'tcTyConScopedTyVars' that we need + -- unlike the finalized 'tycon' defined above which is an 'AlgTyCon' ; let deriv_info = DerivInfo { di_rep_tc = tycon + , di_scoped_tvs = tcTyConScopedTyVars tctc , di_clauses = unLoc derivs , di_ctxt = err_ctxt } ; traceTc "tcDataDefn" (ppr tc_name $$ ppr tycon_binders $$ ppr extra_bndrs) @@ -2299,7 +2437,7 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty -- have checked that the number of patterns matches tyConArity -- This code is closely related to the code - -- in TcHsType.kcLHsQTyVars_Cusk + -- in TcHsType.kcCheckDeclHeader_cusk ; (imp_tvs, (exp_tvs, (lhs_ty, rhs_ty))) <- pushTcLevelM_ $ solveEqualities $ @@ -4098,7 +4236,7 @@ badMethPred sel_id pred noClassTyVarErr :: Class -> TyCon -> SDoc noClassTyVarErr clas fam_tc - = sep [ text "The associated type" <+> quotes (ppr fam_tc) + = sep [ text "The associated type" <+> quotes (ppr fam_tc <+> hsep (map ppr (tyConTyVars fam_tc))) , text "mentions none of the type or kind variables of the class" <+> quotes (ppr clas <+> hsep (map ppr (classTyVars clas)))] diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index 7fe947678a..7fa45ae8f3 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -596,6 +596,8 @@ data UserTypeCtxt | InfSigCtxt Name -- Inferred type for function | ExprSigCtxt -- Expression type signature | KindSigCtxt -- Kind signature + | StandaloneKindSigCtxt -- Standalone kind signature + Name -- Name of the type/class | TypeAppCtxt -- Visible type application | ConArgCtxt Name -- Data constructor argument | TySynCtxt Name -- RHS of a type synonym decl @@ -653,6 +655,7 @@ pprUserTypeCtxt (InfSigCtxt n) = text "the inferred type for" <+> quotes (ppr pprUserTypeCtxt (RuleSigCtxt n) = text "a RULE for" <+> quotes (ppr n) pprUserTypeCtxt ExprSigCtxt = text "an expression type signature" pprUserTypeCtxt KindSigCtxt = text "a kind signature" +pprUserTypeCtxt (StandaloneKindSigCtxt n) = text "a standalone kind signature for" <+> quotes (ppr n) pprUserTypeCtxt TypeAppCtxt = text "a type argument" pprUserTypeCtxt (ConArgCtxt c) = text "the type of the constructor" <+> quotes (ppr c) pprUserTypeCtxt (TySynCtxt c) = text "the RHS of the type synonym" <+> quotes (ppr c) diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs index eaec2dbd2f..307ec6d0c5 100644 --- a/compiler/typecheck/TcValidity.hs +++ b/compiler/typecheck/TcValidity.hs @@ -232,6 +232,7 @@ wantAmbiguityCheck ctxt GhciCtxt {} -> False TySynCtxt {} -> False TypeAppCtxt -> False + StandaloneKindSigCtxt{} -> False _ -> True checkUserTypeError :: Type -> TcM () @@ -280,6 +281,10 @@ In a few places we do not want to check a user-specified type for ambiguity f @ty No need to check ty for ambiguity +* StandaloneKindSigCtxt: type T :: ksig + Kinds need a different ambiguity check than types, and the currently + implemented check is only good for types. See #14419, in particular + https://gitlab.haskell.org/ghc/ghc/issues/14419#note_160844 ************************************************************************ * * @@ -343,6 +348,7 @@ checkValidType ctxt ty ExprSigCtxt -> rank1 KindSigCtxt -> rank1 + StandaloneKindSigCtxt{} -> rank1 TypeAppCtxt | impred_flag -> ArbitraryRank | otherwise -> tyConArgMonoType -- Normally, ImpredicativeTypes is handled in check_arg_type, @@ -463,6 +469,7 @@ allConstraintsAllowed (TyVarBndrKindCtxt {}) = False allConstraintsAllowed (DataKindCtxt {}) = False allConstraintsAllowed (TySynKindCtxt {}) = False allConstraintsAllowed (TyFamResKindCtxt {}) = False +allConstraintsAllowed (StandaloneKindSigCtxt {}) = False allConstraintsAllowed _ = True -- | Returns 'True' if the supplied 'UserTypeCtxt' is unambiguously not the @@ -482,6 +489,7 @@ allConstraintsAllowed _ = True vdqAllowed :: UserTypeCtxt -> Bool -- Currently allowed in the kinds of types... vdqAllowed (KindSigCtxt {}) = True +vdqAllowed (StandaloneKindSigCtxt {}) = True vdqAllowed (TySynCtxt {}) = True vdqAllowed (ThBrackCtxt {}) = True vdqAllowed (GhciCtxt {}) = True @@ -1329,6 +1337,7 @@ okIPCtxt (TySynCtxt {}) = True -- e.g. type Blah = ?x::Int -- #11466 okIPCtxt (KindSigCtxt {}) = False +okIPCtxt (StandaloneKindSigCtxt {}) = False okIPCtxt (ClassSCCtxt {}) = False okIPCtxt (InstDeclCtxt {}) = False okIPCtxt (SpecInstCtxt {}) = False @@ -2149,7 +2158,7 @@ checkFamPatBinders fam_tc qtvs pats rhs -- data T = MkT (forall (a::k). blah) -- data family D Int = MkD (forall (a::k). blah) -- In both cases, 'k' is not bound on the LHS, but is used on the RHS - -- We catch the former in kcLHsQTyVars, and the latter right here + -- We catch the former in kcDeclHeader, and the latter right here -- See Note [Check type-family instance binders] ; check_tvs bad_rhs_tvs (text "mentioned in the RHS") (text "bound on the LHS of") diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs index 19f3f0ee56..7af2bc0ad7 100644 --- a/compiler/types/TyCon.hs +++ b/compiler/types/TyCon.hs @@ -41,6 +41,7 @@ module TyCon( mkFamilyTyCon, mkPromotedDataCon, mkTcTyCon, + noTcTyConScopedTyVars, -- ** Predicates on TyCons isAlgTyCon, isVanillaAlgTyCon, @@ -477,6 +478,8 @@ isInvisibleTyConBinder :: VarBndr tv TyConBndrVis -> Bool -- Works for IfaceTyConBinder too isInvisibleTyConBinder tcb = not (isVisibleTyConBinder tcb) +-- Build the 'tyConKind' from the binders and the result kind. +-- Keep in sync with 'mkTyConKind' in iface/IfaceType. mkTyConKind :: [TyConBinder] -> Kind -> Kind mkTyConKind bndrs res_kind = foldr mk res_kind bndrs where @@ -1702,6 +1705,10 @@ mkTcTyCon name binders res_kind scoped_tvs poly flav , tcTyConIsPoly = poly , tcTyConFlavour = flav } +-- | No scoped type variables (to be used with mkTcTyCon). +noTcTyConScopedTyVars :: [(Name, TcTyVar)] +noTcTyConScopedTyVars = [] + -- | Create an unlifted primitive 'TyCon', such as @Int#@. mkPrimTyCon :: Name -> [TyConBinder] -> Kind -- ^ /result/ kind, never levity-polymorphic diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs index d8664eba62..f8cd1da078 100644 --- a/compiler/types/Type.hs +++ b/compiler/types/Type.hs @@ -42,7 +42,8 @@ module Type ( mkSpecForAllTy, mkSpecForAllTys, mkVisForAllTys, mkTyCoInvForAllTy, mkInvForAllTy, mkInvForAllTys, - splitForAllTys, splitForAllTysSameVis, splitForAllVarBndrs, + splitForAllTys, splitForAllTysSameVis, + splitForAllVarBndrs, splitForAllTy_maybe, splitForAllTy, splitForAllTy_ty_maybe, splitForAllTy_co_maybe, splitPiTy_maybe, splitPiTy, splitPiTys, |