diff options
64 files changed, 813 insertions, 148 deletions
diff --git a/compiler/basicTypes/Var.hs b/compiler/basicTypes/Var.hs index 7e451e5407..f397793bf7 100644 --- a/compiler/basicTypes/Var.hs +++ b/compiler/basicTypes/Var.hs @@ -62,7 +62,7 @@ module Var ( -- * ArgFlags ArgFlag(..), isVisibleArgFlag, isInvisibleArgFlag, sameVis, - AnonArgFlag(..), + AnonArgFlag(..), ForallVisFlag(..), argToForallVisFlag, -- * TyVar's VarBndr(..), TyCoVarBinder, TyVarBinder, @@ -425,15 +425,17 @@ instance Binary ArgFlag where 1 -> return Specified _ -> return Inferred --- The non-dependent version of ArgFlag, namely AnonArgFlag, --- appears here partly so that it's together with its friend ArgFlag, +-- | The non-dependent version of 'ArgFlag'. + +-- Appears here partly so that it's together with its friend ArgFlag, -- but also because it is used in IfaceType, rather early in the -- compilation chain +-- See Note [AnonArgFlag vs. ForallVisFlag] data AnonArgFlag - = VisArg -- Used for (->): an ordinary non-dependent arrow - -- The argument is visible in source code - | InvisArg -- Used for (=>): a non-dependent predicate arrow - -- The argument is invisible in source code + = VisArg -- ^ Used for @(->)@: an ordinary non-dependent arrow. + -- The argument is visible in source code. + | InvisArg -- ^ Used for @(=>)@: a non-dependent predicate arrow. + -- The argument is invisible in source code. deriving (Eq, Ord, Data) instance Outputable AnonArgFlag where @@ -450,6 +452,47 @@ instance Binary AnonArgFlag where 0 -> return VisArg _ -> return InvisArg +-- | Is a @forall@ invisible (e.g., @forall a b. {...}@, with a dot) or visible +-- (e.g., @forall a b -> {...}@, with an arrow)? + +-- See Note [AnonArgFlag vs. ForallVisFlag] +data ForallVisFlag + = ForallVis -- ^ A visible @forall@ (with an arrow) + | ForallInvis -- ^ An invisible @forall@ (with a dot) + deriving (Eq, Ord, Data) + +instance Outputable ForallVisFlag where + ppr f = text $ case f of + ForallVis -> "ForallVis" + ForallInvis -> "ForallInvis" + +-- | Convert an 'ArgFlag' to its corresponding 'ForallVisFlag'. +argToForallVisFlag :: ArgFlag -> ForallVisFlag +argToForallVisFlag Required = ForallVis +argToForallVisFlag Specified = ForallInvis +argToForallVisFlag Inferred = ForallInvis + +{- +Note [AnonArgFlag vs. ForallVisFlag] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The AnonArgFlag and ForallVisFlag data types are quite similar at a first +glance: + + data AnonArgFlag = VisArg | InvisArg + data ForallVisFlag = ForallVis | ForallInvis + +Both data types keep track of visibility of some sort. AnonArgFlag tracks +whether a FunTy has a visible argument (->) or an invisible predicate argument +(=>). ForallVisFlag tracks whether a `forall` quantifier is visible +(forall a -> {...}) or invisible (forall a. {...}). + +Given their similarities, it's tempting to want to combine these two data types +into one, but they actually represent distinct concepts. AnonArgFlag reflects a +property of *Core* types, whereas ForallVisFlag reflects a property of the GHC +AST. In other words, AnonArgFlag is all about internals, whereas ForallVisFlag +is all about surface syntax. Therefore, they are kept as separate data types. +-} + {- ********************************************************************* * * * VarBndr, TyCoVarBinder diff --git a/compiler/deSugar/DsMeta.hs b/compiler/deSugar/DsMeta.hs index a8a4fb6b40..5e0976d1a2 100644 --- a/compiler/deSugar/DsMeta.hs +++ b/compiler/deSugar/DsMeta.hs @@ -1144,18 +1144,21 @@ repLTys tys = mapM repLTy tys repLTy :: LHsType GhcRn -> DsM (Core TH.TypeQ) repLTy ty = repTy (unLoc ty) -repForall :: HsType GhcRn -> DsM (Core TH.TypeQ) +repForall :: ForallVisFlag -> HsType GhcRn -> DsM (Core TH.TypeQ) -- Arg of repForall is always HsForAllTy or HsQualTy -repForall ty +repForall fvf ty | (tvs, ctxt, tau) <- splitLHsSigmaTy (noLoc ty) = addHsTyVarBinds tvs $ \bndrs -> do { ctxt1 <- repLContext ctxt ; ty1 <- repLTy tau - ; repTForall bndrs ctxt1 ty1 } + ; case fvf of + ForallVis -> repTForallVis bndrs ty1 -- forall a -> {...} + ForallInvis -> repTForall bndrs ctxt1 ty1 -- forall a. C a => {...} + } repTy :: HsType GhcRn -> DsM (Core TH.TypeQ) -repTy ty@(HsForAllTy {}) = repForall ty -repTy ty@(HsQualTy {}) = repForall ty +repTy ty@(HsForAllTy {hst_fvf = fvf}) = repForall fvf ty +repTy ty@(HsQualTy {}) = repForall ForallInvis ty repTy (HsTyVar _ _ (dL->L _ n)) | isLiftedTypeKindTyConName n = repTStar @@ -2467,6 +2470,10 @@ repTForall :: Core [TH.TyVarBndrQ] -> Core TH.CxtQ -> Core TH.TypeQ repTForall (MkC tvars) (MkC ctxt) (MkC ty) = rep2 forallTName [tvars, ctxt, ty] +repTForallVis :: Core [TH.TyVarBndrQ] -> Core TH.TypeQ + -> DsM (Core TH.TypeQ) +repTForallVis (MkC tvars) (MkC ty) = rep2 forallVisTName [tvars, ty] + repTvar :: Core TH.Name -> DsM (Core TH.TypeQ) repTvar (MkC s) = rep2 varTName [s] diff --git a/compiler/hieFile/HieAst.hs b/compiler/hieFile/HieAst.hs index 9752403054..2b112153bd 100644 --- a/compiler/hieFile/HieAst.hs +++ b/compiler/hieFile/HieAst.hs @@ -1386,7 +1386,7 @@ instance ToHie (LHsType GhcRn) where instance ToHie (TScoped (LHsType GhcRn)) where toHie (TS tsc (L span t)) = concatM $ makeNode t span : case t of - HsForAllTy _ bndrs body -> + HsForAllTy _ _ bndrs body -> [ toHie $ tvScopes tsc (mkScope $ getLoc body) bndrs , toHie body ] diff --git a/compiler/hsSyn/Convert.hs b/compiler/hsSyn/Convert.hs index 1a801bb1b1..364bcb06c2 100644 --- a/compiler/hsSyn/Convert.hs +++ b/compiler/hsSyn/Convert.hs @@ -1405,11 +1405,18 @@ cvtTypeKind ty_str ty ; let pcxt = parenthesizeHsContext funPrec cxt' ; ty' <- cvtType ty ; loc <- getL - ; let hs_ty = mkHsForAllTy tvs loc tvs' rho_ty + ; let hs_ty = mkHsForAllTy tvs loc ForallInvis tvs' rho_ty rho_ty = mkHsQualTy cxt loc pcxt ty' ; return hs_ty } + ForallVisT tvs ty + | null tys' + -> do { tvs' <- cvtTvs tvs + ; ty' <- cvtType ty + ; loc <- getL + ; pure $ mkHsForAllTy tvs loc ForallVis tvs' ty' } + SigT ty ki -> do { ty' <- cvtType ty ; ki' <- cvtKind ki @@ -1638,7 +1645,8 @@ cvtPatSynSigTy (ForallT univs reqs (ForallT exis provs ty)) ; univs' <- hsQTvExplicit <$> cvtTvs univs ; ty' <- cvtType (ForallT exis provs ty) ; let forTy = HsForAllTy - { hst_bndrs = univs' + { hst_fvf = ForallInvis + , hst_bndrs = univs' , hst_xforall = noExt , hst_body = cL l cxtTy } cxtTy = HsQualTy { hst_ctxt = cL l [] @@ -1692,15 +1700,19 @@ mkHsForAllTy :: [TH.TyVarBndr] -> SrcSpan -- ^ The location of the returned 'LHsType' if it needs an -- explicit forall + -> ForallVisFlag + -- ^ Whether this is @forall@ is visible (e.g., @forall a ->@) + -- or invisible (e.g., @forall a.@) -> LHsQTyVars GhcPs -- ^ The converted type variable binders -> LHsType GhcPs -- ^ The converted rho type -> LHsType GhcPs -- ^ The complete type, quantified with a forall if necessary -mkHsForAllTy tvs loc tvs' rho_ty +mkHsForAllTy tvs loc fvf tvs' rho_ty | null tvs = rho_ty - | otherwise = cL loc $ HsForAllTy { hst_bndrs = hsQTvExplicit tvs' + | otherwise = cL loc $ HsForAllTy { hst_fvf = fvf + , hst_bndrs = hsQTvExplicit tvs' , hst_xforall = noExt , hst_body = rho_ty } diff --git a/compiler/hsSyn/HsDecls.hs b/compiler/hsSyn/HsDecls.hs index c18a9ae1fc..f8709fbe1e 100644 --- a/compiler/hsSyn/HsDecls.hs +++ b/compiler/hsSyn/HsDecls.hs @@ -1457,7 +1457,7 @@ pprConDecl (ConDeclH98 { con_name = L _ con , con_mb_cxt = mcxt , con_args = args , con_doc = doc }) - = sep [ppr_mbDoc doc, pprHsForAll ex_tvs cxt, ppr_details args] + = sep [ppr_mbDoc doc, pprHsForAll ForallInvis ex_tvs cxt, ppr_details args] where ppr_details (InfixCon t1 t2) = hsep [ppr t1, pprInfixOcc con, ppr t2] ppr_details (PrefixCon tys) = hsep (pprPrefixOcc con @@ -1470,7 +1470,7 @@ pprConDecl (ConDeclGADT { con_names = cons, con_qvars = qvars , con_mb_cxt = mcxt, con_args = args , con_res_ty = res_ty, con_doc = doc }) = ppr_mbDoc doc <+> ppr_con_names cons <+> dcolon - <+> (sep [pprHsForAll (hsq_explicit qvars) cxt, + <+> (sep [pprHsForAll ForallInvis (hsq_explicit qvars) cxt, ppr_arrow_chain (get_args args ++ [ppr res_ty]) ]) where get_args (PrefixCon args) = map ppr args @@ -1777,7 +1777,7 @@ pprHsFamInstLHS :: (OutputableBndrId (GhcPass p)) -> LHsContext (GhcPass p) -> SDoc pprHsFamInstLHS thing bndrs typats fixity mb_ctxt - = hsep [ pprHsExplicitForAll bndrs + = hsep [ pprHsExplicitForAll ForallInvis bndrs , pprLHsContext mb_ctxt , pp_pats typats ] where diff --git a/compiler/hsSyn/HsTypes.hs b/compiler/hsSyn/HsTypes.hs index fa87613416..aabe9f4597 100644 --- a/compiler/hsSyn/HsTypes.hs +++ b/compiler/hsSyn/HsTypes.hs @@ -19,7 +19,7 @@ HsTypes: Abstract syntax: user-defined types module HsTypes ( HsType(..), NewHsTypeX(..), LHsType, HsKind, LHsKind, - HsTyVarBndr(..), LHsTyVarBndr, + HsTyVarBndr(..), LHsTyVarBndr, ForallVisFlag(..), LHsQTyVars(..), HsQTvsRn(..), HsImplicitBndrs(..), HsWildCardBndrs(..), @@ -56,7 +56,8 @@ module HsTypes ( hsLTyVarName, hsLTyVarLocName, hsExplicitLTyVarNames, splitLHsInstDeclTy, getLHsInstDeclHead, getLHsInstDeclClass_maybe, splitLHsPatSynTy, - splitLHsForAllTy, splitLHsQualTy, splitLHsSigmaTy, + splitLHsForAllTy, splitLHsForAllTyInvis, + splitLHsQualTy, splitLHsSigmaTy, splitLHsSigmaTyInvis, splitHsFunType, hsTyGetAppHead_maybe, mkHsOpTy, mkHsAppTy, mkHsAppTys, mkHsAppKindTy, ignoreParens, hsSigType, hsSigWcType, @@ -142,13 +143,18 @@ is a bit complicated. Here's how it works. * In a HsType, HsForAllTy represents an /explicit, user-written/ 'forall' - e.g. forall a b. ... + e.g. forall a b. {...} or + forall a b -> {...} HsQualTy represents an /explicit, user-written/ context e.g. (Eq a, Show a) => ... The context can be empty if that's what the user wrote These constructors represent what the user wrote, no more and no less. +* The ForallVisFlag field of HsForAllTy represents whether a forall is + invisible (e.g., forall a b. {...}, with a dot) or visible + (e.g., forall a b -> {...}, with an arrow). + * HsTyVarBndr describes a quantified type variable written by the user. For example f :: forall a (b :: *). blah @@ -512,8 +518,10 @@ hsTvbAllKinded = all (isHsKindedTyVar . unLoc) . hsQTvExplicit -- | Haskell Type data HsType pass = HsForAllTy -- See Note [HsType binders] - { hst_xforall :: XForAllTy pass, - hst_bndrs :: [LHsTyVarBndr pass] + { hst_xforall :: XForAllTy pass + , hst_fvf :: ForallVisFlag -- Is this `forall a -> {...}` or + -- `forall a. {...}`? + , hst_bndrs :: [LHsTyVarBndr pass] -- Explicit, user-supplied 'forall a b c' , hst_body :: LHsType pass -- body type } @@ -1137,6 +1145,13 @@ The SrcSpan is the span of the original HsPar -} -------------------------------- + +-- | Decompose a pattern synonym type signature into its constituent parts. +-- +-- Note that this function looks through parentheses, so it will work on types +-- such as @(forall a. <...>)@. The downside to this is that it is not +-- generally possible to take the returned types and reconstruct the original +-- type (parentheses and all) from them. splitLHsPatSynTy :: LHsType pass -> ( [LHsTyVarBndr pass] -- universals , LHsContext pass -- required constraints @@ -1145,11 +1160,18 @@ splitLHsPatSynTy :: LHsType pass , LHsType pass) -- body type splitLHsPatSynTy ty = (univs, reqs, exis, provs, ty4) where - (univs, ty1) = splitLHsForAllTy ty + (univs, ty1) = splitLHsForAllTyInvis ty (reqs, ty2) = splitLHsQualTy ty1 - (exis, ty3) = splitLHsForAllTy ty2 + (exis, ty3) = splitLHsForAllTyInvis ty2 (provs, ty4) = splitLHsQualTy ty3 +-- | Decompose a sigma type (of the form @forall <tvs>. context => body@) +-- into its constituent parts. +-- +-- Note that this function looks through parentheses, so it will work on types +-- such as @(forall a. <...>)@. The downside to this is that it is not +-- generally possible to take the returned types and reconstruct the original +-- type (parentheses and all) from them. splitLHsSigmaTy :: LHsType pass -> ([LHsTyVarBndr pass], LHsContext pass, LHsType pass) splitLHsSigmaTy ty @@ -1157,22 +1179,82 @@ splitLHsSigmaTy ty , (ctxt, ty2) <- splitLHsQualTy ty1 = (tvs, ctxt, ty2) +-- | Like 'splitLHsSigmaTy', but only splits type variable binders that were +-- quantified invisibly (e.g., @forall a.@, with a dot). +-- +-- This function is used to split apart certain types, such as instance +-- declaration types, which disallow visible @forall@s. For instance, if GHC +-- split apart the @forall@ in @instance forall a -> Show (Blah a)@, then that +-- declaration would mistakenly be accepted! +-- +-- Note that this function looks through parentheses, so it will work on types +-- such as @(forall a. <...>)@. The downside to this is that it is not +-- generally possible to take the returned types and reconstruct the original +-- type (parentheses and all) from them. +splitLHsSigmaTyInvis :: LHsType pass + -> ([LHsTyVarBndr pass], LHsContext pass, LHsType pass) +splitLHsSigmaTyInvis ty + | (tvs, ty1) <- splitLHsForAllTyInvis ty + , (ctxt, ty2) <- splitLHsQualTy ty1 + = (tvs, ctxt, ty2) + +-- | Decompose a type of the form @forall <tvs>. body@) into its constituent +-- parts. +-- +-- Note that this function looks through parentheses, so it will work on types +-- such as @(forall a. <...>)@. The downside to this is that it is not +-- generally possible to take the returned types and reconstruct the original +-- type (parentheses and all) from them. splitLHsForAllTy :: LHsType pass -> ([LHsTyVarBndr pass], LHsType pass) splitLHsForAllTy (L _ (HsParTy _ ty)) = splitLHsForAllTy ty splitLHsForAllTy (L _ (HsForAllTy { hst_bndrs = tvs, hst_body = body })) = (tvs, body) splitLHsForAllTy body = ([], body) +-- | Like 'splitLHsForAllTy', but only splits type variable binders that +-- were quantified invisibly (e.g., @forall a.@, with a dot). +-- +-- This function is used to split apart certain types, such as instance +-- declaration types, which disallow visible @forall@s. For instance, if GHC +-- split apart the @forall@ in @instance forall a -> Show (Blah a)@, then that +-- declaration would mistakenly be accepted! +-- +-- Note that this function looks through parentheses, so it will work on types +-- such as @(forall a. <...>)@. The downside to this is that it is not +-- generally possible to take the returned types and reconstruct the original +-- type (parentheses and all) from them. +splitLHsForAllTyInvis :: LHsType pass -> ([LHsTyVarBndr pass], LHsType pass) +splitLHsForAllTyInvis lty@(L _ ty) = + case ty of + HsParTy _ ty' -> splitLHsForAllTyInvis ty' + HsForAllTy { hst_fvf = fvf', hst_bndrs = tvs', hst_body = body' } + | fvf' == ForallInvis + -> (tvs', body') + _ -> ([], lty) + +-- | Decompose a type of the form @context => body@ into its constituent parts. +-- +-- Note that this function looks through parentheses, so it will work on types +-- such as @(context => <...>)@. The downside to this is that it is not +-- generally possible to take the returned types and reconstruct the original +-- type (parentheses and all) from them. splitLHsQualTy :: LHsType pass -> (LHsContext pass, LHsType pass) splitLHsQualTy (L _ (HsParTy _ ty)) = splitLHsQualTy ty splitLHsQualTy (L _ (HsQualTy { hst_ctxt = ctxt, hst_body = body })) = (ctxt, body) splitLHsQualTy body = (noLHsContext, body) +-- | Decompose a type class instance type (of the form +-- @forall <tvs>. context => instance_head@) into its constituent parts. +-- +-- Note that this function looks through parentheses, so it will work on types +-- such as @(forall <tvs>. <...>)@. The downside to this is that it is not +-- generally possible to take the returned types and reconstruct the original +-- type (parentheses and all) from them. splitLHsInstDeclTy :: LHsSigType GhcRn -> ([Name], LHsContext GhcRn, LHsType GhcRn) -- Split up an instance decl type, returning the pieces splitLHsInstDeclTy (HsIB { hsib_ext = itkvs , hsib_body = inst_ty }) - | (tvs, cxt, body_ty) <- splitLHsSigmaTy inst_ty + | (tvs, cxt, body_ty) <- splitLHsSigmaTyInvis inst_ty = (itkvs ++ map hsLTyVarName tvs, cxt, body_ty) -- Return implicitly bound type and kind vars -- For an instance decl, all of them are in scope @@ -1180,7 +1262,7 @@ splitLHsInstDeclTy (XHsImplicitBndrs _) = panic "splitLHsInstDeclTy" getLHsInstDeclHead :: LHsSigType pass -> LHsType pass getLHsInstDeclHead inst_ty - | (_tvs, _cxt, body_ty) <- splitLHsSigmaTy (hsSigType inst_ty) + | (_tvs, _cxt, body_ty) <- splitLHsSigmaTyInvis (hsSigType inst_ty) = body_ty getLHsInstDeclClass_maybe :: LHsSigType (GhcPass p) @@ -1326,10 +1408,11 @@ instance (p ~ GhcPass pass,Outputable thing) pprAnonWildCard :: SDoc pprAnonWildCard = char '_' --- | Prints a forall; When passed an empty list, prints @forall.@ only when --- @-dppr-debug@ +-- | Prints a forall; When passed an empty list, prints @forall .@/@forall ->@ +-- only when @-dppr-debug@ is enabled. pprHsForAll :: (OutputableBndrId (GhcPass p)) - => [LHsTyVarBndr (GhcPass p)] -> LHsContext (GhcPass p) -> SDoc + => ForallVisFlag -> [LHsTyVarBndr (GhcPass p)] + -> LHsContext (GhcPass p) -> SDoc pprHsForAll = pprHsForAllExtra Nothing -- | Version of 'pprHsForAll' that can also print an extra-constraints @@ -1340,20 +1423,31 @@ pprHsForAll = pprHsForAllExtra Nothing -- from the actual context and type, and stored in a separate field, thus just -- printing the type will not print the extra-constraints wildcard. pprHsForAllExtra :: (OutputableBndrId (GhcPass p)) - => Maybe SrcSpan -> [LHsTyVarBndr (GhcPass p)] + => Maybe SrcSpan -> ForallVisFlag + -> [LHsTyVarBndr (GhcPass p)] -> LHsContext (GhcPass p) -> SDoc -pprHsForAllExtra extra qtvs cxt +pprHsForAllExtra extra fvf qtvs cxt = pp_forall <+> pprLHsContextExtra (isJust extra) cxt where - pp_forall | null qtvs = whenPprDebug (forAllLit <> dot) - | otherwise = forAllLit <+> interppSP qtvs <> dot + pp_forall | null qtvs = whenPprDebug (forAllLit <> separator) + | otherwise = forAllLit <+> interppSP qtvs <> separator + + separator = ppr_forall_separator fvf --- | Version of 'pprHsForall' or 'pprHsForallExtra' that will always print +-- | Version of 'pprHsForAll' or 'pprHsForAllExtra' that will always print -- @forall.@ when passed @Just []@. Prints nothing if passed 'Nothing' pprHsExplicitForAll :: (OutputableBndrId (GhcPass p)) - => Maybe [LHsTyVarBndr (GhcPass p)] -> SDoc -pprHsExplicitForAll (Just qtvs) = forAllLit <+> interppSP qtvs <> dot -pprHsExplicitForAll Nothing = empty + => ForallVisFlag + -> Maybe [LHsTyVarBndr (GhcPass p)] -> SDoc +pprHsExplicitForAll fvf (Just qtvs) = forAllLit <+> interppSP qtvs + <> ppr_forall_separator fvf +pprHsExplicitForAll _ Nothing = empty + +-- | Prints an arrow for visible @forall@s (e.g., @forall a ->@) and a dot for +-- invisible @forall@s (e.g., @forall a.@). +ppr_forall_separator :: ForallVisFlag -> SDoc +ppr_forall_separator ForallVis = space <> arrow +ppr_forall_separator ForallInvis = dot pprLHsContext :: (OutputableBndrId (GhcPass p)) => LHsContext (GhcPass p) -> SDoc @@ -1413,8 +1507,8 @@ ppr_mono_lty :: (OutputableBndrId (GhcPass p)) => LHsType (GhcPass p) -> SDoc ppr_mono_lty ty = ppr_mono_ty (unLoc ty) ppr_mono_ty :: (OutputableBndrId (GhcPass p)) => HsType (GhcPass p) -> SDoc -ppr_mono_ty (HsForAllTy { hst_bndrs = tvs, hst_body = ty }) - = sep [pprHsForAll tvs noLHsContext, ppr_mono_lty ty] +ppr_mono_ty (HsForAllTy { hst_fvf = fvf, hst_bndrs = tvs, hst_body = ty }) + = sep [pprHsForAll fvf tvs noLHsContext, ppr_mono_lty ty] ppr_mono_ty (HsQualTy { hst_ctxt = ctxt, hst_body = ty }) = sep [pprLHsContextAlways ctxt, ppr_mono_lty ty] diff --git a/compiler/hsSyn/HsUtils.hs b/compiler/hsSyn/HsUtils.hs index 16b2cf9dfd..62c153ef52 100644 --- a/compiler/hsSyn/HsUtils.hs +++ b/compiler/hsSyn/HsUtils.hs @@ -658,9 +658,10 @@ typeToLHsType ty , hst_xqual = noExt , hst_body = go tau }) - go ty@(ForAllTy {}) - | (tvs, tau) <- tcSplitForAllTys ty - = noLoc (HsForAllTy { hst_bndrs = map go_tv tvs + go ty@(ForAllTy (Bndr _ argf) _) + | (tvs, tau) <- tcSplitForAllTysSameVis argf ty + = noLoc (HsForAllTy { hst_fvf = argToForallVisFlag argf + , hst_bndrs = map go_tv tvs , hst_xforall = noExt , hst_body = go tau }) go (TyVarTy tv) = nlHsTyVar (getRdrName tv) diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs index 985a612940..e2235ab01f 100644 --- a/compiler/iface/IfaceType.hs +++ b/compiler/iface/IfaceType.hs @@ -21,7 +21,8 @@ module IfaceType ( IfaceTyLit(..), IfaceAppArgs(..), IfaceContext, IfaceBndr(..), IfaceOneShot(..), IfaceLamBndr, IfaceTvBndr, IfaceIdBndr, IfaceTyConBinder, - IfaceForAllBndr, ArgFlag(..), AnonArgFlag(..), ShowForAllFlag(..), + IfaceForAllBndr, ArgFlag(..), AnonArgFlag(..), + ForallVisFlag(..), ShowForAllFlag(..), mkIfaceForAllTvBndr, ifForAllBndrVar, ifForAllBndrName, ifaceBndrName, diff --git a/compiler/parser/Parser.y b/compiler/parser/Parser.y index 63473b4540..739090f3f6 100644 --- a/compiler/parser/Parser.y +++ b/compiler/parser/Parser.y @@ -1852,6 +1852,10 @@ unpackedness :: { Located ([AddAnn], SourceText, SrcUnpackedness) } : '{-# UNPACK' '#-}' { sLL $1 $> ([mo $1, mc $2], getUNPACK_PRAGs $1, SrcUnpack) } | '{-# NOUNPACK' '#-}' { sLL $1 $> ([mo $1, mc $2], getNOUNPACK_PRAGs $1, SrcNoUnpack) } +forall_vis_flag :: { (AddAnn, ForallVisFlag) } + : '.' { (mj AnnDot $1, ForallInvis) } + | '->' { (mj AnnRarrow $1, ForallVis) } + -- A ktype/ktypedoc is a ctype/ctypedoc, possibly with a kind annotation ktype :: { LHsType GhcPs } : ctype { $1 } @@ -1865,12 +1869,15 @@ ktypedoc :: { LHsType GhcPs } -- A ctype is a for-all type ctype :: { LHsType GhcPs } - : 'forall' tv_bndrs '.' ctype {% hintExplicitForall $1 >> + : 'forall' tv_bndrs forall_vis_flag ctype + {% let (fv_ann, fv_flag) = $3 in + hintExplicitForall $1 *> ams (sLL $1 $> $ - HsForAllTy { hst_bndrs = $2 + HsForAllTy { hst_fvf = fv_flag + , hst_bndrs = $2 , hst_xforall = noExt , hst_body = $4 }) - [mu AnnForall $1, mj AnnDot $3] } + [mu AnnForall $1,fv_ann] } | context '=>' ctype {% addAnnotation (gl $1) (toUnicodeAnn AnnDarrow $2) (gl $2) >> return (sLL $1 $> $ HsQualTy { hst_ctxt = $1 @@ -1892,12 +1899,15 @@ ctype :: { LHsType GhcPs } -- to 'field' or to 'Int'. So we must use `ctype` to describe the type. ctypedoc :: { LHsType GhcPs } - : 'forall' tv_bndrs '.' ctypedoc {% hintExplicitForall $1 >> + : 'forall' tv_bndrs forall_vis_flag ctypedoc + {% let (fv_ann, fv_flag) = $3 in + hintExplicitForall $1 *> ams (sLL $1 $> $ - HsForAllTy { hst_bndrs = $2 + HsForAllTy { hst_fvf = fv_flag + , hst_bndrs = $2 , hst_xforall = noExt , hst_body = $4 }) - [mu AnnForall $1,mj AnnDot $3] } + [mu AnnForall $1,fv_ann] } | context '=>' ctypedoc {% addAnnotation (gl $1) (toUnicodeAnn AnnDarrow $2) (gl $2) >> return (sLL $1 $> $ HsQualTy { hst_ctxt = $1 diff --git a/compiler/parser/RdrHsSyn.hs b/compiler/parser/RdrHsSyn.hs index 0c3ed74c3b..480b7307dc 100644 --- a/compiler/parser/RdrHsSyn.hs +++ b/compiler/parser/RdrHsSyn.hs @@ -692,7 +692,7 @@ mkGadtDecl names ty , anns1 ++ anns2) where (ty'@(dL->L l _),anns1) = peel_parens ty [] - (tvs, rho) = splitLHsForAllTy ty' + (tvs, rho) = splitLHsForAllTyInvis ty' (mcxt, tau, anns2) = split_rho rho [] split_rho (dL->L _ (HsQualTy { hst_ctxt = cxt, hst_body = tau })) ann diff --git a/compiler/prelude/THNames.hs b/compiler/prelude/THNames.hs index 40ef6a4062..140b3df6f8 100644 --- a/compiler/prelude/THNames.hs +++ b/compiler/prelude/THNames.hs @@ -96,9 +96,9 @@ templateHaskellNames = [ -- PatSynArgs (for pattern synonyms) prefixPatSynName, infixPatSynName, recordPatSynName, -- Type - forallTName, varTName, conTName, infixTName, appTName, appKindTName, - equalityTName, tupleTName, unboxedTupleTName, unboxedSumTName, - arrowTName, listTName, sigTName, litTName, + forallTName, forallVisTName, varTName, conTName, infixTName, appTName, + appKindTName, equalityTName, tupleTName, unboxedTupleTName, + unboxedSumTName, arrowTName, listTName, sigTName, litTName, promotedTName, promotedTupleTName, promotedNilTName, promotedConsTName, wildCardTName, implicitParamTName, -- TyLit @@ -429,12 +429,13 @@ infixPatSynName = libFun (fsLit "infixPatSyn") infixPatSynIdKey recordPatSynName = libFun (fsLit "recordPatSyn") recordPatSynIdKey -- data Type = ... -forallTName, varTName, conTName, infixTName, tupleTName, unboxedTupleTName, - unboxedSumTName, arrowTName, listTName, appTName, appKindTName, - sigTName, equalityTName, litTName, promotedTName, +forallTName, forallVisTName, varTName, conTName, infixTName, tupleTName, + unboxedTupleTName, unboxedSumTName, arrowTName, listTName, appTName, + appKindTName, sigTName, equalityTName, litTName, promotedTName, promotedTupleTName, promotedNilTName, promotedConsTName, wildCardTName, implicitParamTName :: Name forallTName = libFun (fsLit "forallT") forallTIdKey +forallVisTName = libFun (fsLit "forallVisT") forallVisTIdKey varTName = libFun (fsLit "varT") varTIdKey conTName = libFun (fsLit "conT") conTIdKey tupleTName = libFun (fsLit "tupleT") tupleTIdKey @@ -950,79 +951,80 @@ infixPatSynIdKey = mkPreludeMiscIdUnique 381 recordPatSynIdKey = mkPreludeMiscIdUnique 382 -- data Type = ... -forallTIdKey, varTIdKey, conTIdKey, tupleTIdKey, unboxedTupleTIdKey, - unboxedSumTIdKey, arrowTIdKey, listTIdKey, appTIdKey, appKindTIdKey, - sigTIdKey, equalityTIdKey, litTIdKey, promotedTIdKey, +forallTIdKey, forallVisTIdKey, varTIdKey, conTIdKey, tupleTIdKey, + unboxedTupleTIdKey, unboxedSumTIdKey, arrowTIdKey, listTIdKey, appTIdKey, + appKindTIdKey, sigTIdKey, equalityTIdKey, litTIdKey, promotedTIdKey, promotedTupleTIdKey, promotedNilTIdKey, promotedConsTIdKey, wildCardTIdKey, implicitParamTIdKey, infixTIdKey :: Unique forallTIdKey = mkPreludeMiscIdUnique 390 -varTIdKey = mkPreludeMiscIdUnique 391 -conTIdKey = mkPreludeMiscIdUnique 392 -tupleTIdKey = mkPreludeMiscIdUnique 393 -unboxedTupleTIdKey = mkPreludeMiscIdUnique 394 -unboxedSumTIdKey = mkPreludeMiscIdUnique 395 -arrowTIdKey = mkPreludeMiscIdUnique 396 -listTIdKey = mkPreludeMiscIdUnique 397 -appTIdKey = mkPreludeMiscIdUnique 398 -appKindTIdKey = mkPreludeMiscIdUnique 399 -sigTIdKey = mkPreludeMiscIdUnique 400 -equalityTIdKey = mkPreludeMiscIdUnique 401 -litTIdKey = mkPreludeMiscIdUnique 402 -promotedTIdKey = mkPreludeMiscIdUnique 403 -promotedTupleTIdKey = mkPreludeMiscIdUnique 404 -promotedNilTIdKey = mkPreludeMiscIdUnique 405 -promotedConsTIdKey = mkPreludeMiscIdUnique 406 -wildCardTIdKey = mkPreludeMiscIdUnique 407 -implicitParamTIdKey = mkPreludeMiscIdUnique 408 -infixTIdKey = mkPreludeMiscIdUnique 409 +forallVisTIdKey = mkPreludeMiscIdUnique 391 +varTIdKey = mkPreludeMiscIdUnique 392 +conTIdKey = mkPreludeMiscIdUnique 393 +tupleTIdKey = mkPreludeMiscIdUnique 394 +unboxedTupleTIdKey = mkPreludeMiscIdUnique 395 +unboxedSumTIdKey = mkPreludeMiscIdUnique 396 +arrowTIdKey = mkPreludeMiscIdUnique 397 +listTIdKey = mkPreludeMiscIdUnique 398 +appTIdKey = mkPreludeMiscIdUnique 399 +appKindTIdKey = mkPreludeMiscIdUnique 400 +sigTIdKey = mkPreludeMiscIdUnique 401 +equalityTIdKey = mkPreludeMiscIdUnique 402 +litTIdKey = mkPreludeMiscIdUnique 403 +promotedTIdKey = mkPreludeMiscIdUnique 404 +promotedTupleTIdKey = mkPreludeMiscIdUnique 405 +promotedNilTIdKey = mkPreludeMiscIdUnique 406 +promotedConsTIdKey = mkPreludeMiscIdUnique 407 +wildCardTIdKey = mkPreludeMiscIdUnique 408 +implicitParamTIdKey = mkPreludeMiscIdUnique 409 +infixTIdKey = mkPreludeMiscIdUnique 410 -- data TyLit = ... numTyLitIdKey, strTyLitIdKey :: Unique -numTyLitIdKey = mkPreludeMiscIdUnique 410 -strTyLitIdKey = mkPreludeMiscIdUnique 411 +numTyLitIdKey = mkPreludeMiscIdUnique 411 +strTyLitIdKey = mkPreludeMiscIdUnique 412 -- data TyVarBndr = ... plainTVIdKey, kindedTVIdKey :: Unique -plainTVIdKey = mkPreludeMiscIdUnique 412 -kindedTVIdKey = mkPreludeMiscIdUnique 413 +plainTVIdKey = mkPreludeMiscIdUnique 413 +kindedTVIdKey = mkPreludeMiscIdUnique 414 -- data Role = ... nominalRIdKey, representationalRIdKey, phantomRIdKey, inferRIdKey :: Unique -nominalRIdKey = mkPreludeMiscIdUnique 414 -representationalRIdKey = mkPreludeMiscIdUnique 415 -phantomRIdKey = mkPreludeMiscIdUnique 416 -inferRIdKey = mkPreludeMiscIdUnique 417 +nominalRIdKey = mkPreludeMiscIdUnique 415 +representationalRIdKey = mkPreludeMiscIdUnique 416 +phantomRIdKey = mkPreludeMiscIdUnique 417 +inferRIdKey = mkPreludeMiscIdUnique 418 -- data Kind = ... varKIdKey, conKIdKey, tupleKIdKey, arrowKIdKey, listKIdKey, appKIdKey, starKIdKey, constraintKIdKey :: Unique -varKIdKey = mkPreludeMiscIdUnique 418 -conKIdKey = mkPreludeMiscIdUnique 419 -tupleKIdKey = mkPreludeMiscIdUnique 420 -arrowKIdKey = mkPreludeMiscIdUnique 421 -listKIdKey = mkPreludeMiscIdUnique 422 -appKIdKey = mkPreludeMiscIdUnique 423 -starKIdKey = mkPreludeMiscIdUnique 424 -constraintKIdKey = mkPreludeMiscIdUnique 425 +varKIdKey = mkPreludeMiscIdUnique 419 +conKIdKey = mkPreludeMiscIdUnique 420 +tupleKIdKey = mkPreludeMiscIdUnique 421 +arrowKIdKey = mkPreludeMiscIdUnique 422 +listKIdKey = mkPreludeMiscIdUnique 423 +appKIdKey = mkPreludeMiscIdUnique 424 +starKIdKey = mkPreludeMiscIdUnique 425 +constraintKIdKey = mkPreludeMiscIdUnique 426 -- data FamilyResultSig = ... noSigIdKey, kindSigIdKey, tyVarSigIdKey :: Unique -noSigIdKey = mkPreludeMiscIdUnique 426 -kindSigIdKey = mkPreludeMiscIdUnique 427 -tyVarSigIdKey = mkPreludeMiscIdUnique 428 +noSigIdKey = mkPreludeMiscIdUnique 427 +kindSigIdKey = mkPreludeMiscIdUnique 428 +tyVarSigIdKey = mkPreludeMiscIdUnique 429 -- data InjectivityAnn = ... injectivityAnnIdKey :: Unique -injectivityAnnIdKey = mkPreludeMiscIdUnique 429 +injectivityAnnIdKey = mkPreludeMiscIdUnique 430 -- data Callconv = ... cCallIdKey, stdCallIdKey, cApiCallIdKey, primCallIdKey, javaScriptCallIdKey :: Unique -cCallIdKey = mkPreludeMiscIdUnique 430 -stdCallIdKey = mkPreludeMiscIdUnique 431 -cApiCallIdKey = mkPreludeMiscIdUnique 432 -primCallIdKey = mkPreludeMiscIdUnique 433 -javaScriptCallIdKey = mkPreludeMiscIdUnique 434 +cCallIdKey = mkPreludeMiscIdUnique 431 +stdCallIdKey = mkPreludeMiscIdUnique 432 +cApiCallIdKey = mkPreludeMiscIdUnique 433 +primCallIdKey = mkPreludeMiscIdUnique 434 +javaScriptCallIdKey = mkPreludeMiscIdUnique 435 -- data Safety = ... unsafeIdKey, safeIdKey, interruptibleIdKey :: Unique diff --git a/compiler/prelude/TysWiredIn.hs b/compiler/prelude/TysWiredIn.hs index 4e7cd84276..aaeb902754 100644 --- a/compiler/prelude/TysWiredIn.hs +++ b/compiler/prelude/TysWiredIn.hs @@ -154,7 +154,6 @@ import NameSet ( NameSet, mkNameSet, elemNameSet ) import BasicTypes ( Arity, Boxity(..), TupleSort(..), ConTagZ, SourceText(..) ) import ForeignCall -import Var ( AnonArgFlag(..) ) import SrcLoc ( noSrcSpan ) import Unique import Data.Array diff --git a/compiler/rename/RnTypes.hs b/compiler/rename/RnTypes.hs index 499fd74bd9..b84bbe3bae 100644 --- a/compiler/rename/RnTypes.hs +++ b/compiler/rename/RnTypes.hs @@ -170,11 +170,13 @@ rnWcBody ctxt nwc_rdrs hs_ty rn_ty :: RnTyKiEnv -> HsType GhcPs -> RnM (HsType GhcRn, FreeVars) -- A lot of faff just to allow the extra-constraints wildcard to appear - rn_ty env hs_ty@(HsForAllTy { hst_bndrs = tvs, hst_body = hs_body }) + rn_ty env hs_ty@(HsForAllTy { hst_fvf = fvf, hst_bndrs = tvs + , hst_body = hs_body }) = bindLHsTyVarBndrs (rtke_ctxt env) (Just $ inTypeDoc hs_ty) Nothing tvs $ \ tvs' -> do { (hs_body', fvs) <- rn_lty env hs_body - ; return (HsForAllTy { hst_xforall = noExt, hst_bndrs = tvs' - , hst_body = hs_body' }, fvs) } + ; return (HsForAllTy { hst_fvf = fvf, hst_xforall = noExt + , hst_bndrs = tvs', hst_body = hs_body' } + , fvs) } rn_ty env (HsQualTy { hst_ctxt = dL->L cx hs_ctxt , hst_body = hs_ty }) @@ -479,13 +481,14 @@ rnLHsTyKi env (dL->L loc ty) rnHsTyKi :: RnTyKiEnv -> HsType GhcPs -> RnM (HsType GhcRn, FreeVars) -rnHsTyKi env ty@(HsForAllTy { hst_bndrs = tyvars, hst_body = tau }) +rnHsTyKi env ty@(HsForAllTy { hst_fvf = fvf, hst_bndrs = tyvars + , hst_body = tau }) = do { checkPolyKinds env ty ; bindLHsTyVarBndrs (rtke_ctxt env) (Just $ inTypeDoc ty) Nothing tyvars $ \ tyvars' -> do { (tau', fvs) <- rnLHsTyKi env tau - ; return ( HsForAllTy { hst_xforall = noExt, hst_bndrs = tyvars' - , hst_body = tau' } + ; return ( HsForAllTy { hst_fvf = fvf, hst_xforall = noExt + , hst_bndrs = tyvars' , hst_body = tau' } , fvs) } } rnHsTyKi env ty@(HsQualTy { hst_ctxt = lctxt, hst_body = tau }) diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs index 6078a7a7ff..4736ded2f2 100644 --- a/compiler/typecheck/TcDeriv.hs +++ b/compiler/typecheck/TcDeriv.hs @@ -725,7 +725,8 @@ tcStandaloneDerivInstType ctxt HsIB { hsib_ext = vars , hsib_body = L (getLoc deriv_ty_body) $ - HsForAllTy { hst_bndrs = tvs + HsForAllTy { hst_fvf = ForallInvis + , hst_bndrs = tvs , hst_xforall = noExt , hst_body = rho }} let (tvs, _theta, cls, inst_tys) = tcSplitDFunTy dfun_ty diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index ef038e119b..24b416c6e8 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -666,14 +666,18 @@ tc_hs_type mode (HsOpTy _ ty1 (L _ op) ty2) exp_kind = tc_fun_type mode ty1 ty2 exp_kind --------- Foralls -tc_hs_type mode forall@(HsForAllTy { hst_bndrs = hs_tvs, hst_body = ty }) exp_kind +tc_hs_type mode forall@(HsForAllTy { hst_fvf = fvf, hst_bndrs = hs_tvs + , hst_body = ty }) exp_kind = do { (tclvl, wanted, (tvs', ty')) <- pushLevelAndCaptureConstraints $ bindExplicitTKBndrs_Skol hs_tvs $ tc_lhs_type mode ty exp_kind -- Do not kind-generalise here! See Note [Kind generalisation] -- Why exp_kind? See Note [Body kind of HsForAllTy] - ; let bndrs = mkTyVarBinders Specified tvs' + ; let argf = case fvf of + ForallVis -> Required + ForallInvis -> Specified + bndrs = mkTyVarBinders argf tvs' skol_info = ForAllSkol (ppr forall) m_telescope = Just (sep (map ppr hs_tvs)) diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs index 76d1510aa3..fcac5cb33d 100644 --- a/compiler/typecheck/TcRnDriver.hs +++ b/compiler/typecheck/TcRnDriver.hs @@ -2311,7 +2311,8 @@ getGhciStepIO = do ioM = nlHsAppTy (nlHsTyVar ioTyConName) (nlHsTyVar a_tv) step_ty = noLoc $ HsForAllTy - { hst_bndrs = [noLoc $ UserTyVar noExt (noLoc a_tv)] + { hst_fvf = ForallInvis + , hst_bndrs = [noLoc $ UserTyVar noExt (noLoc a_tv)] , hst_xforall = noExt , hst_body = nlHsFunTy ghciM ioM } diff --git a/compiler/typecheck/TcSigs.hs b/compiler/typecheck/TcSigs.hs index 027a4013ab..17e3f54893 100644 --- a/compiler/typecheck/TcSigs.hs +++ b/compiler/typecheck/TcSigs.hs @@ -366,8 +366,8 @@ tcPatSynSig :: Name -> LHsSigType GhcRn -> TcM TcPatSynInfo tcPatSynSig name sig_ty | HsIB { hsib_ext = implicit_hs_tvs , hsib_body = hs_ty } <- sig_ty - , (univ_hs_tvs, hs_req, hs_ty1) <- splitLHsSigmaTy hs_ty - , (ex_hs_tvs, hs_prov, hs_body_ty) <- splitLHsSigmaTy hs_ty1 + , (univ_hs_tvs, hs_req, hs_ty1) <- splitLHsSigmaTyInvis hs_ty + , (ex_hs_tvs, hs_prov, hs_body_ty) <- splitLHsSigmaTyInvis hs_ty1 = do { traceTc "tcPatSynSig 1" (ppr sig_ty) ; (implicit_tvs, (univ_tvs, (ex_tvs, (req, prov, body_ty)))) <- pushTcLevelM_ $ diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs index 631c777ab7..1aba34e802 100644 --- a/compiler/typecheck/TcSplice.hs +++ b/compiler/typecheck/TcSplice.hs @@ -1814,7 +1814,8 @@ reifyType :: TyCoRep.Type -> TcM TH.Type reifyType ty | tcIsLiftedTypeKind ty = return TH.StarT -- Make sure to use tcIsLiftedTypeKind here, since we don't want to confuse it -- with Constraint (#14869). -reifyType ty@(ForAllTy {}) = reify_for_all ty +reifyType ty@(ForAllTy (Bndr _ argf) _) + = reify_for_all argf ty reifyType (LitTy t) = do { r <- reifyTyLit t; return (TH.LitT r) } reifyType (TyVarTy tv) = return (TH.VarT (reifyName tv)) reifyType (TyConApp tc tys) = reify_tc_app tc tys -- Do not expand type synonyms here @@ -1836,19 +1837,24 @@ reifyType ty@(AppTy {}) = do filterByList (map isVisibleArgFlag $ appTyArgFlags ty_head ty_args) ty_args reifyType ty@(FunTy { ft_af = af, ft_arg = t1, ft_res = t2 }) - | InvisArg <- af = reify_for_all ty -- Types like ((?x::Int) => Char -> Char) + | InvisArg <- af = reify_for_all Inferred ty -- Types like ((?x::Int) => Char -> Char) | otherwise = do { [r1,r2] <- reifyTypes [t1,t2] ; return (TH.ArrowT `TH.AppT` r1 `TH.AppT` r2) } reifyType (CastTy t _) = reifyType t -- Casts are ignored in TH reifyType ty@(CoercionTy {})= noTH (sLit "coercions in types") (ppr ty) -reify_for_all :: TyCoRep.Type -> TcM TH.Type -reify_for_all ty - = do { cxt' <- reifyCxt cxt; - ; tau' <- reifyType tau - ; tvs' <- reifyTyVars tvs - ; return (TH.ForallT tvs' cxt' tau') } +reify_for_all :: TyCoRep.ArgFlag -> TyCoRep.Type -> TcM TH.Type +-- Arg of reify_for_all is always ForAllTy or a predicate FunTy +reify_for_all argf ty = do + tvs' <- reifyTyVars tvs + case argToForallVisFlag argf of + ForallVis -> do phi' <- reifyType phi + pure $ TH.ForallVisT tvs' phi' + ForallInvis -> do let (cxt, tau) = tcSplitPhiTy phi + cxt' <- reifyCxt cxt + tau' <- reifyType tau + pure $ TH.ForallT tvs' cxt' tau' where - (tvs, cxt, tau) = tcSplitSigmaTy ty + (tvs, phi) = tcSplitForAllTysSameVis argf ty reifyTyLit :: TyCoRep.TyLit -> TcM TH.TyLit reifyTyLit (NumTyLit n) = return (TH.NumTyLit n) diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index 1f6372cd0a..155037b775 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -59,7 +59,8 @@ module TcType ( -- These are important because they do not look through newtypes getTyVar, tcSplitForAllTy_maybe, - tcSplitForAllTys, tcSplitPiTys, tcSplitPiTy_maybe, tcSplitForAllVarBndrs, + tcSplitForAllTys, tcSplitForAllTysSameVis, + tcSplitPiTys, tcSplitPiTy_maybe, tcSplitForAllVarBndrs, tcSplitPhiTy, tcSplitPredFunTy_maybe, tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcFunResultTyN, tcSplitFunTysN, @@ -128,7 +129,8 @@ module TcType ( -------------------------------- -- Rexported from Type - Type, PredType, ThetaType, TyCoBinder, ArgFlag(..), AnonArgFlag(..), + Type, PredType, ThetaType, TyCoBinder, + ArgFlag(..), AnonArgFlag(..), ForallVisFlag(..), mkForAllTy, mkForAllTys, mkTyCoInvForAllTys, mkSpecForAllTys, mkTyCoInvForAllTy, mkInvForAllTy, mkInvForAllTys, @@ -1354,6 +1356,14 @@ tcSplitForAllTys ty = ASSERT( all isTyVar (fst sty) ) sty where sty = splitForAllTys ty +-- | Like 'tcSplitForAllTys', but only splits a 'ForAllTy' if +-- @'sameVis' argf supplied_argf@ is 'True', where @argf@ is the visibility +-- of the @ForAllTy@'s binder and @supplied_argf@ is the visibility provided +-- as an argument to this function. +tcSplitForAllTysSameVis :: ArgFlag -> Type -> ([TyVar], Type) +tcSplitForAllTysSameVis supplied_argf ty = ASSERT( all isTyVar (fst sty) ) sty + where sty = splitForAllTysSameVis supplied_argf ty + -- | Like 'tcSplitForAllTys', but splits off only named binders. tcSplitForAllVarBndrs :: Type -> ([TyVarBinder], Type) tcSplitForAllVarBndrs ty = ASSERT( all isTyVarBinder (fst sty)) sty diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs index 8ab63f49cc..d17ac0f567 100644 --- a/compiler/typecheck/TcValidity.hs +++ b/compiler/typecheck/TcValidity.hs @@ -464,6 +464,55 @@ allConstraintsAllowed (TySynKindCtxt {}) = False allConstraintsAllowed (TyFamResKindCtxt {}) = False allConstraintsAllowed _ = True +-- | Returns 'True' if the supplied 'UserTypeCtxt' is unambiguously not the +-- context for the type of a term, where visible, dependent quantification is +-- currently disallowed. +-- +-- An example of something that is unambiguously the type of a term is the +-- @forall a -> a -> a@ in @foo :: forall a -> a -> a@. On the other hand, the +-- same type in @type family Foo :: forall a -> a -> a@ is unambiguously the +-- kind of a type, not the type of a term, so it is permitted. +-- +-- For more examples, see +-- @testsuite/tests/dependent/should_compile/T16326_Compile*.hs@ (for places +-- where VDQ is permitted) and +-- @testsuite/tests/dependent/should_fail/T16326_Fail*.hs@ (for places where +-- VDQ is disallowed). +vdqAllowed :: UserTypeCtxt -> Bool +-- Currently allowed in the kinds of types... +vdqAllowed (KindSigCtxt {}) = True +vdqAllowed (TySynCtxt {}) = True +vdqAllowed (ThBrackCtxt {}) = True +vdqAllowed (GhciCtxt {}) = True +vdqAllowed (TyVarBndrKindCtxt {}) = True +vdqAllowed (DataKindCtxt {}) = True +vdqAllowed (TySynKindCtxt {}) = True +vdqAllowed (TyFamResKindCtxt {}) = True +-- ...but not in the types of terms. +vdqAllowed (ConArgCtxt {}) = False + -- We could envision allowing VDQ in data constructor types so long as the + -- constructor is only ever used at the type level, but for now, GHC adopts + -- the stance that VDQ is never allowed in data constructor types. +vdqAllowed (FunSigCtxt {}) = False +vdqAllowed (InfSigCtxt {}) = False +vdqAllowed (ExprSigCtxt {}) = False +vdqAllowed (TypeAppCtxt {}) = False +vdqAllowed (PatSynCtxt {}) = False +vdqAllowed (PatSigCtxt {}) = False +vdqAllowed (RuleSigCtxt {}) = False +vdqAllowed (ResSigCtxt {}) = False +vdqAllowed (ForSigCtxt {}) = False +vdqAllowed (DefaultDeclCtxt {}) = False +-- We count class constraints as "types of terms". All of the cases below deal +-- with class constraints. +vdqAllowed (InstDeclCtxt {}) = False +vdqAllowed (SpecInstCtxt {}) = False +vdqAllowed (GenSigCtxt {}) = False +vdqAllowed (ClassSCCtxt {}) = False +vdqAllowed (SigmaCtxt {}) = False +vdqAllowed (DataTyCtxt {}) = False +vdqAllowed (DerivClauseCtxt {}) = False + {- Note [Correctness and performance of type synonym validity checking] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -615,9 +664,8 @@ check_type ve (CastTy ty _) = check_type ve ty -- -- Critically, this case must come *after* the case for TyConApp. -- See Note [Liberal type synonyms]. -check_type ve@(ValidityEnv{ ve_tidy_env = env - , ve_rank = rank - , ve_expand = expand }) ty +check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt + , ve_rank = rank, ve_expand = expand }) ty | not (null tvbs && null theta) = do { traceTc "check_type" (ppr ty $$ ppr (forAllAllowed rank)) ; checkTcM (forAllAllowed rank) (forAllTyErr env rank ty) @@ -628,6 +676,12 @@ check_type ve@(ValidityEnv{ ve_tidy_env = env -- Reject forall (a :: Eq b => b). blah -- In a kind signature we don't allow constraints + ; checkTcM (all (isInvisibleArgFlag . binderArgFlag) tvbs + || vdqAllowed ctxt) + (illegalVDQTyErr env ty) + -- Reject visible, dependent quantification in the type of a + -- term (e.g., `f :: forall a -> a -> Maybe a`) + ; check_valid_theta env' SigmaCtxt expand theta -- Allow type T = ?x::Int => Int -> Int -- but not type T = ?x::Int @@ -851,6 +905,15 @@ constraintTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc) constraintTyErr env ty = (env, text "Illegal constraint in a kind:" <+> ppr_tidy env ty) +-- | Reject a use of visible, dependent quantification in the type of a term. +illegalVDQTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc) +illegalVDQTyErr env ty = + (env, vcat + [ hang (text "Illegal visible, dependent quantification" <+> + text "in the type of a term:") + 2 (ppr_tidy env ty) + , text "(GHC does not yet support this)" ] ) + {- Note [Liberal type synonyms] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs index 3594c7a3a3..86f72b88f2 100644 --- a/compiler/types/TyCoRep.hs +++ b/compiler/types/TyCoRep.hs @@ -32,7 +32,7 @@ module TyCoRep ( KindOrType, Kind, KnotTied, PredType, ThetaType, -- Synonyms - ArgFlag(..), AnonArgFlag(..), + ArgFlag(..), AnonArgFlag(..), ForallVisFlag(..), -- * Coercions Coercion(..), diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs index 473e9e5ef8..7ff5bb4c84 100644 --- a/compiler/types/Type.hs +++ b/compiler/types/Type.hs @@ -14,7 +14,7 @@ module Type ( -- $type_classification -- $representation_types - TyThing(..), Type, ArgFlag(..), AnonArgFlag, + TyThing(..), Type, ArgFlag(..), AnonArgFlag(..), ForallVisFlag(..), KindOrType, PredType, ThetaType, Var, TyVar, isTyVar, TyCoVar, TyCoBinder, TyCoVarBinder, TyVarBinder, KnotTied, @@ -42,7 +42,7 @@ module Type ( mkSpecForAllTy, mkSpecForAllTys, mkVisForAllTys, mkTyCoInvForAllTy, mkInvForAllTy, mkInvForAllTys, - splitForAllTys, splitForAllVarBndrs, + splitForAllTys, splitForAllTysSameVis, splitForAllVarBndrs, splitForAllTy_maybe, splitForAllTy, splitForAllTy_ty_maybe, splitForAllTy_co_maybe, splitPiTy_maybe, splitPiTy, splitPiTys, @@ -1455,6 +1455,18 @@ splitForAllTys ty = split ty ty [] split _ (ForAllTy (Bndr tv _) ty) tvs = split ty ty (tv:tvs) split orig_ty _ tvs = (reverse tvs, orig_ty) +-- | Like 'splitForAllTys', but only splits a 'ForAllTy' if +-- @'sameVis' argf supplied_argf@ is 'True', where @argf@ is the visibility +-- of the @ForAllTy@'s binder and @supplied_argf@ is the visibility provided +-- as an argument to this function. +splitForAllTysSameVis :: ArgFlag -> Type -> ([TyCoVar], Type) +splitForAllTysSameVis supplied_argf ty = split ty ty [] + where + split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs + split _ (ForAllTy (Bndr tv argf) ty) tvs + | argf `sameVis` supplied_argf = split ty ty (tv:tvs) + split orig_ty _ tvs = (reverse tvs, orig_ty) + -- | Like splitForAllTys, but split only for tyvars. -- This always succeeds, even if it returns only an empty list. Note that the -- result type returned may have free variables that were bound by a forall. diff --git a/docs/users_guide/8.10.1-notes.rst b/docs/users_guide/8.10.1-notes.rst index cfe07deb81..cd865e257f 100644 --- a/docs/users_guide/8.10.1-notes.rst +++ b/docs/users_guide/8.10.1-notes.rst @@ -44,6 +44,16 @@ Language type T = Just (Nothing :: Maybe a) -- no longer accepted type T = Just Nothing :: Maybe (Maybe a) -- still accepted +- GHC now parses visible, dependent quantifiers (as proposed in + `GHC proposal 35 + <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0035-forall-arrow.rst>`__), + such as the following: :: + + data Proxy :: forall k -> k -> Type + + See the `section on explicit kind quantification + <#explicit-kind-quantification>`__ for more details. + Compiler ~~~~~~~~ diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst index 9ba8fa2daf..67be116ae4 100644 --- a/docs/users_guide/glasgow_exts.rst +++ b/docs/users_guide/glasgow_exts.rst @@ -9170,6 +9170,8 @@ GHC reports an error, saying that the kind of ``a`` should be a kind variable restricted to be ``Type``. The function definition is then rejected for being more specific than its type signature. +.. _explicit-kind-quantification: + Explicit kind quantification ---------------------------- @@ -9253,6 +9255,53 @@ Closed type family instances are subject to the same rules: :: type family F :: Maybe (Maybe k) where F @k = 'Just ('Nothing :: Maybe k) -- accepted +Kind variables can also be quantified in *visible* positions. Consider the +following two examples: :: + + data ProxyKInvis (a :: k) + data ProxyKVis k (a :: k) + +In the first example, the kind variable ``k`` is an *invisible* argument to +``ProxyKInvis``. In other words, a user does not need to instantiate ``k`` +explicitly, as kind inference automatically determines what ``k`` should be. +For instance, in ``ProxyKInvis True``, ``k`` is inferred to be ``Bool``. +This is reflected in the kind of ``ProxyKInvis``: :: + + ProxyKInvis :: forall k. k -> Type + +In the second example, ``k`` is a *visible* argument to ``ProxyKVis``. That is +to say, ``k`` is an argument that users must provide explicitly when applying +``ProxyKVis``. For example, ``ProxyKVis Bool True`` is a well formed type. + +What is the kind of ``ProxyKVis``? One might say +``forall k. Type -> k -> Type``, but this isn't quite right, since this would +allow incorrect things like ``ProxyKVis Bool Int``, which should be rejected +due to the fact that ``Int`` is not of kind ``Bool``. The key observation is that +the kind of the second argument *depend* on the first argument. GHC indicates +this dependency in the syntax that it gives for the kind of ``ProxyKVis``: :: + + ProxyKVis :: forall k -> k -> Type + +This kind is similar to the kind of ``ProxyKInvis``, but with a key difference: +the type variables quantified by the ``forall`` are followed by an arrow +(``->``), not a dot (``.``). This is a visible, dependent quantifier. It is +visible in that it the user must pass in a type for ``k`` explicitly, and it is +dependent in the sense that ``k`` appears later in the kind of ``ProxyKVis``. +As a counterpart, the ``k`` binder in ``forall k. k -> Type`` can be thought +of as an *invisible*, dependent quantifier. + +GHC permits writing kinds with this syntax, provided that the +``ExplicitForAll`` and ``PolyKinds`` language extensions are enabled. Just +like the invisible ``forall``, one can put explicit kind signatures on visibly +bound kind variables, so the following is syntactically valid: :: + + ProxyKVis :: forall (k :: Type) -> k -> Type + +Currently, the ability to write visible, dependent quantifiers is limited to +kinds. Consequently, visible dependent quantifiers are rejected in any context +that is unambiguously the type of a term. They are also rejected in the types +of data constructors. + Kind-indexed GADTs ------------------ diff --git a/docs/users_guide/index.rst b/docs/users_guide/index.rst index c20aec7e56..c886722859 100644 --- a/docs/users_guide/index.rst +++ b/docs/users_guide/index.rst @@ -14,6 +14,7 @@ Contents: intro 8.6.1-notes 8.8.1-notes + 8.10.1-notes ghci runghc usage diff --git a/libraries/template-haskell/Language/Haskell/TH/Lib.hs b/libraries/template-haskell/Language/Haskell/TH/Lib.hs index 60527b6c82..69a40428b8 100644 --- a/libraries/template-haskell/Language/Haskell/TH/Lib.hs +++ b/libraries/template-haskell/Language/Haskell/TH/Lib.hs @@ -52,10 +52,10 @@ module Language.Haskell.TH.Lib ( bindS, letS, noBindS, parS, recS, -- *** Types - forallT, varT, conT, appT, appKindT, arrowT, infixT, uInfixT, parensT, - equalityT, listT, tupleT, unboxedTupleT, unboxedSumT, sigT, litT, - wildCardT, promotedT, promotedTupleT, promotedNilT, promotedConsT, - implicitParamT, + forallT, forallVisT, varT, conT, appT, appKindT, arrowT, infixT, + uInfixT, parensT, equalityT, listT, tupleT, unboxedTupleT, unboxedSumT, + sigT, litT, wildCardT, promotedT, promotedTupleT, promotedNilT, + promotedConsT, implicitParamT, -- **** Type literals numTyLit, strTyLit, -- **** Strictness diff --git a/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs b/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs index ec9ca4fafb..14ef0a02a8 100644 --- a/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs +++ b/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs @@ -646,6 +646,9 @@ forallT tvars ctxt ty = do ty1 <- ty return $ ForallT tvars1 ctxt1 ty1 +forallVisT :: [TyVarBndrQ] -> TypeQ -> TypeQ +forallVisT tvars ty = ForallVisT <$> sequenceA tvars <*> ty + varT :: Name -> TypeQ varT = return . VarT diff --git a/libraries/template-haskell/Language/Haskell/TH/Ppr.hs b/libraries/template-haskell/Language/Haskell/TH/Ppr.hs index c25b2fb702..fa00c8c537 100644 --- a/libraries/template-haskell/Language/Haskell/TH/Ppr.hs +++ b/libraries/template-haskell/Language/Haskell/TH/Ppr.hs @@ -647,12 +647,23 @@ commaSepApplied :: [Name] -> Doc commaSepApplied = commaSepWith (pprName' Applied) pprForall :: [TyVarBndr] -> Cxt -> Doc -pprForall tvs cxt +pprForall = pprForall' ForallInvis + +pprForallVis :: [TyVarBndr] -> Cxt -> Doc +pprForallVis = pprForall' ForallVis + +pprForall' :: ForallVisFlag -> [TyVarBndr] -> Cxt -> Doc +pprForall' fvf tvs cxt -- even in the case without any tvs, there could be a non-empty -- context cxt (e.g., in the case of pattern synonyms, where there -- are multiple forall binders and contexts). | [] <- tvs = pprCxt cxt - | otherwise = text "forall" <+> hsep (map ppr tvs) <+> char '.' <+> pprCxt cxt + | otherwise = text "forall" <+> hsep (map ppr tvs) + <+> separator <+> pprCxt cxt + where + separator = case fvf of + ForallVis -> text "->" + ForallInvis -> char '.' pprRecFields :: [(Name, Strict, Type)] -> Type -> Doc pprRecFields vsts ty @@ -750,6 +761,7 @@ pprParendType tuple | (TupleT n, args) <- split tuple pprParendType (ImplicitParamT n t)= text ('?':n) <+> text "::" <+> ppr t pprParendType EqualityT = text "(~)" pprParendType t@(ForallT {}) = parens (ppr t) +pprParendType t@(ForallVisT {}) = parens (ppr t) pprParendType t@(AppT {}) = parens (ppr t) pprParendType t@(AppKindT {}) = parens (ppr t) @@ -759,6 +771,7 @@ pprUInfixT t = ppr t instance Ppr Type where ppr (ForallT tvars ctxt ty) = sep [pprForall tvars ctxt, ppr ty] + ppr (ForallVisT tvars ty) = sep [pprForallVis tvars [], ppr ty] ppr ty = pprTyApp (split ty) -- Works, in a degnerate way, for SigT, and puts parens round (ty :: kind) -- See Note [Pretty-printing kind signatures] @@ -791,10 +804,15 @@ pprTyApp (fun, args) = pprParendType fun <+> sep (map pprParendTypeArg args) pprFunArgType :: Type -> Doc -- Should really use a precedence argument -- Everything except forall and (->) binds more tightly than (->) pprFunArgType ty@(ForallT {}) = parens (ppr ty) +pprFunArgType ty@(ForallVisT {}) = parens (ppr ty) pprFunArgType ty@((ArrowT `AppT` _) `AppT` _) = parens (ppr ty) pprFunArgType ty@(SigT _ _) = parens (ppr ty) pprFunArgType ty = ppr ty +data ForallVisFlag = ForallVis -- forall a -> {...} + | ForallInvis -- forall a. {...} + deriving Show + data TypeArg = TANormal Type | TyArg Kind diff --git a/libraries/template-haskell/Language/Haskell/TH/Syntax.hs b/libraries/template-haskell/Language/Haskell/TH/Syntax.hs index 7bff489650..22c6cd1def 100644 --- a/libraries/template-haskell/Language/Haskell/TH/Syntax.hs +++ b/libraries/template-haskell/Language/Haskell/TH/Syntax.hs @@ -2099,6 +2099,7 @@ data PatSynArgs deriving( Show, Eq, Ord, Data, Generic ) data Type = ForallT [TyVarBndr] Cxt Type -- ^ @forall \<vars\>. \<ctxt\> => \<type\>@ + | ForallVisT [TyVarBndr] Type -- ^ @forall \<vars\> -> \<type\>@ | AppT Type Type -- ^ @T a b@ | AppKindT Type Kind -- ^ @T \@k t@ | SigT Type Kind -- ^ @t :: k@ diff --git a/libraries/template-haskell/changelog.md b/libraries/template-haskell/changelog.md index cfed120471..a64795b5b9 100644 --- a/libraries/template-haskell/changelog.md +++ b/libraries/template-haskell/changelog.md @@ -5,6 +5,9 @@ * Introduce a `liftTyped` method to the `Lift` class and set the default implementations of `lift`/`liftTyped` to be in terms of each other. + * Add a `ForallVisT` constructor to `Type` to represent visible, dependent + quantification. + ## 2.15.0.0 *TBA* * In `Language.Haskell.TH.Syntax`, `DataInstD`, `NewTypeInstD`, `TySynEqn`, diff --git a/testsuite/tests/dependent/should_compile/T16326_Compile1.hs b/testsuite/tests/dependent/should_compile/T16326_Compile1.hs new file mode 100644 index 0000000000..109b18e9f7 --- /dev/null +++ b/testsuite/tests/dependent/should_compile/T16326_Compile1.hs @@ -0,0 +1,40 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UnicodeSyntax #-} +module T16326_Compile1 where + +import Data.Kind + +type DApply a (b :: a -> Type) (f :: forall (x :: a) -> b x) (x :: a) = + f x + +type DComp a + (b :: a -> Type) + (c :: forall (x :: a). b x -> Type) + (f :: forall (x :: a). forall (y :: b x) -> c y) + (g :: forall (x :: a) -> b x) + (x :: a) = + f (g x) + +type family ElimList a + (p :: [a] -> Type) + (s :: [a]) + (pNil :: p '[]) + (pCons :: forall (x :: a) (xs :: [a]) -> p xs -> p (x:xs)) + :: p s where + forall a p pNil (pCons :: forall (x :: a) (xs :: [a]) -> p xs -> p (x:xs)). + ElimList a p '[] pNil pCons = + pNil + forall a p x xs pNil (pCons :: forall (x :: a) (xs :: [a]) -> p xs -> p (x:xs)). + ElimList a p (x:xs) pNil pCons = + pCons x xs (ElimList a p xs pNil pCons) + +data Proxy' :: forall k -> k -> Type where + MkProxy' :: forall k (a :: k). Proxy' k a + +type family Proxy2' ∷ ∀ k → k → Type where + Proxy2' = Proxy' diff --git a/testsuite/tests/dependent/should_compile/T16326_Compile2.hs b/testsuite/tests/dependent/should_compile/T16326_Compile2.hs new file mode 100644 index 0000000000..ac528e28d1 --- /dev/null +++ b/testsuite/tests/dependent/should_compile/T16326_Compile2.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ImpredicativeTypes #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +module T16326_Compile2 where + +import Data.Kind + +type family Wat :: forall a. a +type Lol = Wat @(forall a -> a) (forall a -> a) (forall a. a) @(forall a. a) + Type Bool diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T index ca5f436174..e630f1a90a 100644 --- a/testsuite/tests/dependent/should_compile/all.T +++ b/testsuite/tests/dependent/should_compile/all.T @@ -65,3 +65,5 @@ test('T15076c', normal, compile, ['']) test('T15829', normal, compile, ['']) test('T14729', normal, compile, ['-ddump-types -fprint-typechecker-elaboration -fprint-explicit-coercions']) test('T14729kind', normal, ghci_script, ['T14729kind.script']) +test('T16326_Compile1', normal, compile, ['']) +test('T16326_Compile2', normal, compile, ['']) diff --git a/testsuite/tests/dependent/should_fail/T15859.stderr b/testsuite/tests/dependent/should_fail/T15859.stderr index c4dc1ef086..ec0e091055 100644 --- a/testsuite/tests/dependent/should_fail/T15859.stderr +++ b/testsuite/tests/dependent/should_fail/T15859.stderr @@ -1,6 +1,8 @@ -T15859.hs:14:5: error: - • Cannot apply expression of type ‘forall k -> k -> *’ - to a visible type argument ‘Int’ - • In the expression: (undefined :: KindOf A) @Int - In an equation for ‘a’: a = (undefined :: KindOf A) @Int +T15859.hs:14:19: error: + • Illegal visible, dependent quantification in the type of a term: + forall k -> k -> * + (GHC does not yet support this) + • In the expansion of type synonym ‘KindOf’ + In an expression type signature: KindOf A + In the expression: undefined :: KindOf A diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail1.hs b/testsuite/tests/dependent/should_fail/T16326_Fail1.hs new file mode 100644 index 0000000000..eccbae3deb --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T16326_Fail1.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +module T16326_Fail1 where + +id1 :: forall a -> a -> a +id1 _ x = x + +type Foo = forall a -> a -> a +id2 :: Foo +id2 _ x = x diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail1.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail1.stderr new file mode 100644 index 0000000000..c56bd105db --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T16326_Fail1.stderr @@ -0,0 +1,13 @@ + +T16326_Fail1.hs:5:8: error: + • Illegal visible, dependent quantification in the type of a term: + forall a -> a -> a + (GHC does not yet support this) + • In the type signature: id1 :: forall a -> a -> a + +T16326_Fail1.hs:9:8: error: + • Illegal visible, dependent quantification in the type of a term: + forall a -> a -> a + (GHC does not yet support this) + • In the expansion of type synonym ‘Foo’ + In the type signature: id2 :: Foo diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail10.hs b/testsuite/tests/dependent/should_fail/T16326_Fail10.hs new file mode 100644 index 0000000000..e9fdb16c64 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T16326_Fail10.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +module T16326_Fail10 where + +import Data.Kind + +type Const a b = a + +flurmp :: a -> () +flurmp _ = () +{-# RULES "flurmp" + forall (x :: forall a -> a -> a). flurmp x = () #-} diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail10.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail10.stderr new file mode 100644 index 0000000000..bceccb1dcd --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T16326_Fail10.stderr @@ -0,0 +1,7 @@ + +T16326_Fail10.hs:12:18: error: + • Illegal visible, dependent quantification in the type of a term: + forall a -> a -> a + (GHC does not yet support this) + • In a RULE for ‘x’: forall a -> a -> a + When checking the transformation rule "flurmp" diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail11.hs b/testsuite/tests/dependent/should_fail/T16326_Fail11.hs new file mode 100644 index 0000000000..2ed92c3675 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T16326_Fail11.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE ImpredicativeTypes #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +module T16326_Fail11 where + +class C a where + m :: b -> a + default m :: (forall x -> x) ~ b => b -> a + m = undefined diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail11.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail11.stderr new file mode 100644 index 0000000000..396010dbd7 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T16326_Fail11.stderr @@ -0,0 +1,7 @@ + +T16326_Fail11.hs:9:11: error: + • Illegal visible, dependent quantification in the type of a term: + forall x -> x + (GHC does not yet support this) + • When checking the class method: m :: forall a b. C a => b -> a + In the class declaration for ‘C’ diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail12.hs b/testsuite/tests/dependent/should_fail/T16326_Fail12.hs new file mode 100644 index 0000000000..5db0c2eb3a --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T16326_Fail12.hs @@ -0,0 +1,6 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE RankNTypes #-} +module T16326_Fail12 where + +class (forall a -> Show a) => C a diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail12.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail12.stderr new file mode 100644 index 0000000000..30b35de4f7 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T16326_Fail12.stderr @@ -0,0 +1,8 @@ + +T16326_Fail12.hs:6:1: error: + • Illegal visible, dependent quantification in the type of a term: + forall a -> Show a + (GHC does not yet support this) + • In the context: forall a -> Show a + While checking the super-classes of class ‘C’ + In the class declaration for ‘C’ diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail2.hs b/testsuite/tests/dependent/should_fail/T16326_Fail2.hs new file mode 100644 index 0000000000..398c0d586e --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T16326_Fail2.hs @@ -0,0 +1,6 @@ +{-# LANGUAGE ForeignFunctionInterface #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +module T16326_Fail2 where + +foreign import ccall "blah" blah :: forall a -> a -> IO () diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail2.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail2.stderr new file mode 100644 index 0000000000..3e3f0c1128 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T16326_Fail2.stderr @@ -0,0 +1,8 @@ + +T16326_Fail2.hs:6:37: error: + • Illegal visible, dependent quantification in the type of a term: + forall a -> a -> IO () + (GHC does not yet support this) + • In the type signature: blah :: forall a -> a -> IO () + When checking declaration: + foreign import ccall safe "blah" blah :: forall a -> a -> IO () diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail3.hs b/testsuite/tests/dependent/should_fail/T16326_Fail3.hs new file mode 100644 index 0000000000..4d598d6564 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T16326_Fail3.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +module T16326_Fail3 where + +pattern Nil :: forall a -> [a] +pattern Nil <- undefined diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail3.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail3.stderr new file mode 100644 index 0000000000..27ed998b45 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T16326_Fail3.stderr @@ -0,0 +1,5 @@ + +T16326_Fail3.hs:6:1: error: + Illegal visible, dependent quantification in the type of a term: + forall a -> [a] + (GHC does not yet support this) diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail4.hs b/testsuite/tests/dependent/should_fail/T16326_Fail4.hs new file mode 100644 index 0000000000..b1ba79dddc --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T16326_Fail4.hs @@ -0,0 +1,6 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +module T16326_Fail4 where + +foo :: Maybe a -> Maybe a -> Maybe a +foo xs ys = zipWith ((<>) :: forall a -> Maybe a -> Maybe a -> Maybe a) xs ys diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail4.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail4.stderr new file mode 100644 index 0000000000..258fc08607 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T16326_Fail4.stderr @@ -0,0 +1,11 @@ + +T16326_Fail4.hs:6:30: error: + • Illegal visible, dependent quantification in the type of a term: + forall a1 -> Maybe a1 -> Maybe a1 -> Maybe a1 + (GHC does not yet support this) + • In an expression type signature: + forall a -> Maybe a -> Maybe a -> Maybe a + In the first argument of ‘zipWith’, namely + ‘((<>) :: forall a -> Maybe a -> Maybe a -> Maybe a)’ + In the expression: + zipWith ((<>) :: forall a -> Maybe a -> Maybe a -> Maybe a) xs ys diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail5.hs b/testsuite/tests/dependent/should_fail/T16326_Fail5.hs new file mode 100644 index 0000000000..e5b18181c7 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T16326_Fail5.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +module T16326_Fail5 where + +isJust :: Maybe a -> Bool +isJust (Nothing :: forall a -> Maybe a) = False +isJust (Just _) = True diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail5.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail5.stderr new file mode 100644 index 0000000000..59c27c2464 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T16326_Fail5.stderr @@ -0,0 +1,9 @@ + +T16326_Fail5.hs:7:20: error: + • Illegal visible, dependent quantification in the type of a term: + forall a1 -> Maybe a1 + (GHC does not yet support this) + • In a pattern type signature: forall a -> Maybe a + In the pattern: Nothing :: forall a -> Maybe a + In an equation for ‘isJust’: + isJust (Nothing :: forall a -> Maybe a) = False diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail6.hs b/testsuite/tests/dependent/should_fail/T16326_Fail6.hs new file mode 100644 index 0000000000..75f4f9a674 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T16326_Fail6.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +module T16326_Fail6 where + +import Data.Kind + +data Foo :: Type -> Type where + MkFoo :: forall a -> a -> Foo a diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail6.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail6.stderr new file mode 100644 index 0000000000..bb78e2f457 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T16326_Fail6.stderr @@ -0,0 +1,7 @@ + +T16326_Fail6.hs:9:3: error: + • GADT constructor type signature cannot contain nested ‘forall’s or contexts + Suggestion: instead use this type signature: + MkFoo :: forall a. a -> Foo a + • In the definition of data constructor ‘MkFoo’ + In the data type declaration for ‘Foo’ diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail7.hs b/testsuite/tests/dependent/should_fail/T16326_Fail7.hs new file mode 100644 index 0000000000..9c3801faf0 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T16326_Fail7.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE PolyKinds #-} +module T16326_Fail7 where + +import Data.Kind + +-- Make sure that this doesn't parse as something goofy like +-- forall (forall :: Type -> Type) (k :: Type). forall k -> k -> Type +data Foo :: forall k -> k -> Type diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail7.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail7.stderr new file mode 100644 index 0000000000..13fc416995 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T16326_Fail7.stderr @@ -0,0 +1,5 @@ + +T16326_Fail7.hs:8:13: error: + Illegal symbol ‘forall’ in type + Perhaps you intended to use RankNTypes or a similar language + extension to enable explicit-forall syntax: forall <tvs>. <type> diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail8.hs b/testsuite/tests/dependent/should_fail/T16326_Fail8.hs new file mode 100644 index 0000000000..3a214edc31 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T16326_Fail8.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +module T16326_Fail8 where + +class C a +data Blah a +instance forall a -> C (Blah a) diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail8.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail8.stderr new file mode 100644 index 0000000000..16c2aa617e --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T16326_Fail8.stderr @@ -0,0 +1,6 @@ + +T16326_Fail8.hs:7:10: error: + Illegal class instance: ‘forall a -> C (Blah a)’ + Class instances must be of the form + context => C ty_1 ... ty_n + where ‘C’ is a class diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail9.hs b/testsuite/tests/dependent/should_fail/T16326_Fail9.hs new file mode 100644 index 0000000000..084a908a3a --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T16326_Fail9.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE ImpredicativeTypes #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeApplications #-} +module T16326_Fail9 where + +lol :: forall a. a +lol = undefined + +t :: Bool +t = lol @(forall a -> a -> a) undefined True diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail9.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail9.stderr new file mode 100644 index 0000000000..3ad4e754a9 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T16326_Fail9.stderr @@ -0,0 +1,8 @@ + +T16326_Fail9.hs:11:5: error: + • Illegal visible, dependent quantification in the type of a term: + forall a -> a -> a + (GHC does not yet support this) + • In the expression: lol @(forall a -> a -> a) undefined True + In an equation for ‘t’: + t = lol @(forall a -> a -> a) undefined True diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T index 4b258cc065..ca8a50addf 100644 --- a/testsuite/tests/dependent/should_fail/all.T +++ b/testsuite/tests/dependent/should_fail/all.T @@ -40,3 +40,15 @@ test('T15743d', normal, compile_fail, ['']) test('T15825', normal, compile_fail, ['']) test('T15859', normal, compile_fail, ['']) test('T15264', normal, compile_fail, ['']) +test('T16326_Fail1', normal, compile_fail, ['']) +test('T16326_Fail2', normal, compile_fail, ['']) +test('T16326_Fail3', normal, compile_fail, ['']) +test('T16326_Fail4', normal, compile_fail, ['']) +test('T16326_Fail5', normal, compile_fail, ['']) +test('T16326_Fail6', normal, compile_fail, ['']) +test('T16326_Fail7', normal, compile_fail, ['']) +test('T16326_Fail8', normal, compile_fail, ['']) +test('T16326_Fail9', normal, compile_fail, ['']) +test('T16326_Fail10', normal, compile_fail, ['']) +test('T16326_Fail11', normal, compile_fail, ['']) +test('T16326_Fail12', normal, compile_fail, ['']) diff --git a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr index 9a0c6b8e6e..1bc285ac3b 100644 --- a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr +++ b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr @@ -379,6 +379,7 @@ ({ DumpRenamedAst.hs:19:11-33 } (HsForAllTy (NoExt) + (ForallInvis) [({ DumpRenamedAst.hs:19:18-19 } (UserTyVar (NoExt) diff --git a/testsuite/tests/th/T16326_TH.hs b/testsuite/tests/th/T16326_TH.hs new file mode 100644 index 0000000000..df546b9df2 --- /dev/null +++ b/testsuite/tests/th/T16326_TH.hs @@ -0,0 +1,24 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} +module T16326_TH where + +import Control.Monad.IO.Class +import Data.Kind +import Data.Proxy +import Language.Haskell.TH hiding (Type) +import System.IO + +data Foo :: forall a -> a -> Type +type family Foo2 :: forall a -> a -> Type where + Foo2 = Foo + +$(do info <- reify ''Foo2 + liftIO $ hPutStrLn stderr $ pprint info + + dec <- [d| data Nested :: forall a. forall b -> forall c. + forall d -> forall e. + Proxy '[a,b,c,d,e] -> Type |] + liftIO $ hPutStrLn stderr $ pprint dec + pure dec) diff --git a/testsuite/tests/th/T16326_TH.stderr b/testsuite/tests/th/T16326_TH.stderr new file mode 100644 index 0000000000..8a41fd116d --- /dev/null +++ b/testsuite/tests/th/T16326_TH.stderr @@ -0,0 +1,22 @@ +type family T16326_TH.Foo2 :: forall (a_0 :: *) -> a_0 -> * where + T16326_TH.Foo2 = T16326_TH.Foo +data Nested_0 :: forall a_1 . + forall b_2 -> + forall c_3 . + forall d_4 -> + forall e_5 . + Data.Proxy.Proxy ('(:) a_1 + ('(:) b_2 ('(:) c_3 ('(:) d_4 ('(:) e_5 '[]))))) -> + * +T16326_TH.hs:(17,3)-(24,13): Splicing declarations + do info <- reify ''Foo2 + liftIO $ hPutStrLn stderr $ pprint info + dec <- [d| data Nested :: forall a. + forall b -> + forall c. forall d -> forall e. Proxy '[a, b, c, d, e] -> Type |] + liftIO $ hPutStrLn stderr $ pprint dec + pure dec + ======> + data Nested :: forall a. + forall b -> + forall c. forall d -> forall e. Proxy '[a, b, c, d, e] -> Type diff --git a/testsuite/tests/th/all.T b/testsuite/tests/th/all.T index 7d6340bc43..70070a4687 100644 --- a/testsuite/tests/th/all.T +++ b/testsuite/tests/th/all.T @@ -13,7 +13,7 @@ if config.have_ext_interp : setTestOpts(extra_ways(['ext-interp'])) setTestOpts(only_ways(['normal','ghci','ext-interp'])) -broken_tests = ["ClosedFam1TH","T10620","T10828","T11721_TH","T11797","T12045TH2","T12478_1","T12646","T13642","T14060","T15502","T15738","T15792","T15845","T16180","T1835","T3920","T4135","T4188","T5037","T5362","T7477","T7910","T8761","T8884","T8953","T9262","T9692","T9738","TH_Lift","TH_RichKinds","TH_RichKinds2","TH_Roles3","TH_TyInstWhere2","TH_implicitParams","TH_recursiveDo","TH_reifyDecl1","TH_reifyExplicitForAllFams","TH_reifyInstances","TH_reifyMkName","TH_repE2","TH_repGuard","TH_repPrim","TH_repPrim2","TH_repUnboxedTuples","TH_spliceE6"] +broken_tests = ["ClosedFam1TH","T10620","T10828","T11721_TH","T11797","T12045TH2","T12478_1","T12646","T13642","T14060","T15502","T15738","T15792","T15845","T16180","T1835","T3920","T4135","T4188","T5037","T5362","T7477","T7910","T8761","T8884","T8953","T9262","T9692","T9738","TH_Lift","TH_RichKinds","TH_RichKinds2","TH_Roles3","TH_TyInstWhere2","TH_implicitParams","TH_recursiveDo","TH_reifyDecl1","TH_reifyExplicitForAllFams","TH_reifyInstances","TH_reifyMkName","TH_repE2","TH_repGuard","TH_repPrim","TH_repPrim2","TH_repUnboxedTuples","TH_spliceE6","T16326_TH"] # ext-interp, integer-gmp and llvm is broken see #16087 def broken_ext_interp(name, opts): if name in broken_tests and config.ghc_built_by_llvm: @@ -471,3 +471,4 @@ test('T16180', normal, compile_and_run, ['-package ghc']) test('T16183', normal, compile, ['-v0 -ddump-splices -dsuppress-uniques']) test('T16195', normal, multimod_compile, ['T16195.hs', '-v0']) test('T16293b', normal, compile, ['']) +test('T16326_TH', normal, compile, ['-v0 -ddump-splices -dsuppress-uniques']) diff --git a/utils/haddock b/utils/haddock -Subproject c323c257be0bc118a0501416f06bda8fd51c92f +Subproject 8459c600e0f6da3f85abefdefe651bbe3ed3da4 |