diff --git a/compiler/GHC/Builtin/Names/TH.hs b/compiler/GHC/Builtin/Names/TH.hs
index 3a7d65acd0f2d5039d1d1b6f3dbbb99748f55ae0..b01a4705ec029d740b48a6f720257e21ea9651f0 100644
--- a/compiler/GHC/Builtin/Names/TH.hs
+++ b/compiler/GHC/Builtin/Names/TH.hs
@@ -47,6 +47,7 @@ templateHaskellNames = [
litPName, varPName, tupPName, unboxedTupPName, unboxedSumPName,
conPName, tildePName, bangPName, infixPName,
asPName, wildPName, recPName, listPName, sigPName, viewPName,
+ typePName,
-- FieldPat
fieldPatName,
-- Match
@@ -61,6 +62,7 @@ templateHaskellNames = [
fromEName, fromThenEName, fromToEName, fromThenToEName,
listEName, sigEName, recConEName, recUpdEName, staticEName, unboundVarEName,
labelEName, implicitParamVarEName, getFieldEName, projectionEName,
+ typeEName,
-- FieldExp
fieldExpName,
-- Body
@@ -268,7 +270,7 @@ charPrimLName = libFun (fsLit "charPrimL") charPrimLIdKey
-- data Pat = ...
litPName, varPName, tupPName, unboxedTupPName, unboxedSumPName, conPName,
infixPName, tildePName, bangPName, asPName, wildPName, recPName, listPName,
- sigPName, viewPName :: Name
+ sigPName, viewPName, typePName :: Name
litPName = libFun (fsLit "litP") litPIdKey
varPName = libFun (fsLit "varP") varPIdKey
tupPName = libFun (fsLit "tupP") tupPIdKey
@@ -284,6 +286,7 @@ recPName = libFun (fsLit "recP") recPIdKey
listPName = libFun (fsLit "listP") listPIdKey
sigPName = libFun (fsLit "sigP") sigPIdKey
viewPName = libFun (fsLit "viewP") viewPIdKey
+typePName = libFun (fsLit "typeP") typePIdKey
-- type FieldPat = ...
fieldPatName :: Name
@@ -302,7 +305,7 @@ varEName, conEName, litEName, appEName, appTypeEName, infixEName, infixAppName,
sectionLName, sectionRName, lamEName, lamCaseEName, lamCasesEName, tupEName,
unboxedTupEName, unboxedSumEName, condEName, multiIfEName, letEName,
caseEName, doEName, mdoEName, compEName, staticEName, unboundVarEName,
- labelEName, implicitParamVarEName, getFieldEName, projectionEName :: Name
+ labelEName, implicitParamVarEName, getFieldEName, projectionEName, typeEName :: Name
varEName = libFun (fsLit "varE") varEIdKey
conEName = libFun (fsLit "conE") conEIdKey
litEName = libFun (fsLit "litE") litEIdKey
@@ -343,6 +346,7 @@ labelEName = libFun (fsLit "labelE") labelEIdKey
implicitParamVarEName = libFun (fsLit "implicitParamVarE") implicitParamVarEIdKey
getFieldEName = libFun (fsLit "getFieldE") getFieldEIdKey
projectionEName = libFun (fsLit "projectionE") projectionEIdKey
+typeEName = libFun (fsLit "typeE") typeEIdKey
-- type FieldExp = ...
fieldExpName :: Name
@@ -808,7 +812,7 @@ liftStringIdKey = mkPreludeMiscIdUnique 230
-- data Pat = ...
litPIdKey, varPIdKey, tupPIdKey, unboxedTupPIdKey, unboxedSumPIdKey, conPIdKey,
infixPIdKey, tildePIdKey, bangPIdKey, asPIdKey, wildPIdKey, recPIdKey,
- listPIdKey, sigPIdKey, viewPIdKey :: Unique
+ listPIdKey, sigPIdKey, viewPIdKey, typePIdKey :: Unique
litPIdKey = mkPreludeMiscIdUnique 240
varPIdKey = mkPreludeMiscIdUnique 241
tupPIdKey = mkPreludeMiscIdUnique 242
@@ -824,6 +828,7 @@ recPIdKey = mkPreludeMiscIdUnique 251
listPIdKey = mkPreludeMiscIdUnique 252
sigPIdKey = mkPreludeMiscIdUnique 253
viewPIdKey = mkPreludeMiscIdUnique 254
+typePIdKey = mkPreludeMiscIdUnique 255
-- type FieldPat = ...
fieldPatIdKey :: Unique
@@ -846,7 +851,7 @@ varEIdKey, conEIdKey, litEIdKey, appEIdKey, appTypeEIdKey, infixEIdKey,
fromEIdKey, fromThenEIdKey, fromToEIdKey, fromThenToEIdKey,
listEIdKey, sigEIdKey, recConEIdKey, recUpdEIdKey, staticEIdKey,
unboundVarEIdKey, labelEIdKey, implicitParamVarEIdKey, mdoEIdKey,
- getFieldEIdKey, projectionEIdKey :: Unique
+ getFieldEIdKey, projectionEIdKey, typeEIdKey :: Unique
varEIdKey = mkPreludeMiscIdUnique 270
conEIdKey = mkPreludeMiscIdUnique 271
litEIdKey = mkPreludeMiscIdUnique 272
@@ -883,28 +888,29 @@ implicitParamVarEIdKey = mkPreludeMiscIdUnique 302
mdoEIdKey = mkPreludeMiscIdUnique 303
getFieldEIdKey = mkPreludeMiscIdUnique 304
projectionEIdKey = mkPreludeMiscIdUnique 305
+typeEIdKey = mkPreludeMiscIdUnique 306
-- type FieldExp = ...
fieldExpIdKey :: Unique
-fieldExpIdKey = mkPreludeMiscIdUnique 306
+fieldExpIdKey = mkPreludeMiscIdUnique 307
-- data Body = ...
guardedBIdKey, normalBIdKey :: Unique
-guardedBIdKey = mkPreludeMiscIdUnique 307
-normalBIdKey = mkPreludeMiscIdUnique 308
+guardedBIdKey = mkPreludeMiscIdUnique 308
+normalBIdKey = mkPreludeMiscIdUnique 309
-- data Guard = ...
normalGEIdKey, patGEIdKey :: Unique
-normalGEIdKey = mkPreludeMiscIdUnique 309
-patGEIdKey = mkPreludeMiscIdUnique 310
+normalGEIdKey = mkPreludeMiscIdUnique 310
+patGEIdKey = mkPreludeMiscIdUnique 311
-- data Stmt = ...
bindSIdKey, letSIdKey, noBindSIdKey, parSIdKey, recSIdKey :: Unique
-bindSIdKey = mkPreludeMiscIdUnique 311
-letSIdKey = mkPreludeMiscIdUnique 312
-noBindSIdKey = mkPreludeMiscIdUnique 313
-parSIdKey = mkPreludeMiscIdUnique 314
-recSIdKey = mkPreludeMiscIdUnique 315
+bindSIdKey = mkPreludeMiscIdUnique 312
+letSIdKey = mkPreludeMiscIdUnique 313
+noBindSIdKey = mkPreludeMiscIdUnique 314
+parSIdKey = mkPreludeMiscIdUnique 315
+recSIdKey = mkPreludeMiscIdUnique 316
-- data Dec = ...
funDIdKey, valDIdKey, dataDIdKey, newtypeDIdKey, tySynDIdKey, classDIdKey,
diff --git a/compiler/GHC/Core/DataCon.hs b/compiler/GHC/Core/DataCon.hs
index bb1fb96a29976764e3a0b87194f7772e05f1d99e..480f784239cc35e3b02c6e8b4c9b1154e504c148 100644
--- a/compiler/GHC/Core/DataCon.hs
+++ b/compiler/GHC/Core/DataCon.hs
@@ -572,12 +572,10 @@ data DataCon
{- Note [TyVarBinders in DataCons]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-For the TyVarBinders in a DataCon and PatSyn:
-
- * Each argument flag is Inferred or Specified.
- None are Required. (A DataCon is a term-level function; see
- Note [No Required PiTyBinder in terms] in GHC.Core.TyCo.Rep.)
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+For the TyVarBinders in a DataCon and PatSyn,
+each argument flag is either Inferred or Specified, never Required.
+Lifting this restriction is tracked at #18389 (DataCon) and #23704 (PatSyn).
Why do we need the TyVarBinders, rather than just the TyVars? So that
we can construct the right type for the DataCon with its foralls
diff --git a/compiler/GHC/Core/TyCon.hs b/compiler/GHC/Core/TyCon.hs
index 3aa17fe0b6aa2d25fde2296f8545099657cfd224..2afeae415599590f4d4b0f9047b644e02676dfdb 100644
--- a/compiler/GHC/Core/TyCon.hs
+++ b/compiler/GHC/Core/TyCon.hs
@@ -599,10 +599,11 @@ So tyConTyVarBinders converts TyCon's TyConBinders into TyVarBinders:
- but changing Anon/Required to Specified
The last part about Required->Specified comes from this:
- data T k (a:k) b = MkT (a b)
-Here k is Required in T's kind, but we don't have Required binders in
-the PiTyBinders for a term (see Note [No Required PiTyBinder in terms]
-in GHC.Core.TyCo.Rep), so we change it to Specified when making MkT's PiTyBinders
+ data T k (a :: k) b = MkT (a b)
+Here k is Required in T's kind, but we didn't have Required binders in
+types of terms before the advent of the new, experimental RequiredTypeArguments
+extension. So we historically changed Required to Specified when making MkT's PiTyBinders
+and now continue to do so to avoid a breaking change.
-}
diff --git a/compiler/GHC/Driver/Session.hs b/compiler/GHC/Driver/Session.hs
index 853befe5d6ff7617b11feb31e02620b24ae7c0cd..60ba6526bbb23be35d38860ed487bbb05fdf417a 100644
--- a/compiler/GHC/Driver/Session.hs
+++ b/compiler/GHC/Driver/Session.hs
@@ -2704,6 +2704,7 @@ xFlagsDeps = [
depFlagSpecCond "RelaxedPolyRec" LangExt.RelaxedPolyRec
not
"You can't turn off RelaxedPolyRec any more",
+ flagSpec "RequiredTypeArguments" LangExt.RequiredTypeArguments,
flagSpec "RoleAnnotations" LangExt.RoleAnnotations,
flagSpec "ScopedTypeVariables" LangExt.ScopedTypeVariables,
flagSpec "StandaloneDeriving" LangExt.StandaloneDeriving,
diff --git a/compiler/GHC/Hs/Expr.hs b/compiler/GHC/Hs/Expr.hs
index 3fcb4ef1a15e6ee6db4496c8e73a6d8253d247b4..2420d6c1517e5a0abb7f15a720d0d6f06bc3d3b4 100644
--- a/compiler/GHC/Hs/Expr.hs
+++ b/compiler/GHC/Hs/Expr.hs
@@ -380,6 +380,12 @@ type instance XStatic GhcTc = (NameSet, Type)
-- Free variables and type of expression, this is stored for convenience as wiring in
-- StaticPtr is a bit tricky (see #20150)
+type instance XEmbTy GhcPs = NoExtField
+type instance XEmbTy GhcRn = NoExtField
+type instance XEmbTy GhcTc = DataConCantHappen
+ -- A free-standing HsEmbTy is an error.
+ -- Valid usages are immediately desugared into Type.
+
type instance XPragE (GhcPass _) = NoExtField
type instance Anno [LocatedA ((StmtLR (GhcPass pl) (GhcPass pr) (LocatedA (body (GhcPass pr)))))] = SrcSpanAnnL
@@ -702,6 +708,9 @@ ppr_expr (HsProc _ pat (L _ (HsCmdTop _ cmd)))
ppr_expr (HsStatic _ e)
= hsep [text "static", ppr e]
+ppr_expr (HsEmbTy _ _ ty)
+ = hsep [text "type", ppr ty]
+
ppr_expr (XExpr x) = case ghcPass @p of
#if __GLASGOW_HASKELL__ < 811
GhcPs -> ppr x
@@ -843,6 +852,7 @@ hsExprNeedsParens prec = go
go (HsRecSel{}) = False
go (HsProjection{}) = True
go (HsGetField{}) = False
+ go (HsEmbTy{}) = prec > topPrec
go (XExpr x) = case ghcPass @p of
GhcTc -> go_x_tc x
GhcRn -> go_x_rn x
diff --git a/compiler/GHC/Hs/Pat.hs b/compiler/GHC/Hs/Pat.hs
index 4161de9fe28a321ac2f55012003f0b6fd41086c5..304c9f56e8a70795f0ffa762b55f7070cf1ab864 100644
--- a/compiler/GHC/Hs/Pat.hs
+++ b/compiler/GHC/Hs/Pat.hs
@@ -155,6 +155,10 @@ type instance XSigPat GhcPs = EpAnn [AddEpAnn]
type instance XSigPat GhcRn = NoExtField
type instance XSigPat GhcTc = Type
+type instance XEmbTyPat GhcPs = NoExtField
+type instance XEmbTyPat GhcRn = NoExtField
+type instance XEmbTyPat GhcTc = Type
+
type instance XXPat GhcPs = DataConCantHappen
type instance XXPat GhcRn = HsPatExpansion (Pat GhcRn) (Pat GhcRn)
-- Original pattern and its desugaring/expansion.
@@ -376,6 +380,7 @@ pprPat (ConPat { pat_con = con
, cpt_dicts = dicts
, cpt_binds = binds
} = ext
+pprPat (EmbTyPat _ toktype tp) = ppr toktype <+> ppr tp
pprPat (XPat ext) = case ghcPass @p of
#if __GLASGOW_HASKELL__ < 811
@@ -583,6 +588,10 @@ isIrrefutableHsPat is_strict = goL
-- since we cannot know until the splice is evaluated.
go (SplicePat {}) = False
+ -- The behavior of this case is unimportant, as GHC will throw an error shortly
+ -- after reaching this case for other reasons (see TcRnIllegalTypePattern).
+ go (EmbTyPat {}) = True
+
go (XPat ext) = case ghcPass @p of
#if __GLASGOW_HASKELL__ < 811
GhcPs -> dataConCantHappen ext
@@ -651,6 +660,7 @@ isBoringHsPat = goL
NPat {} -> True
NPlusKPat {} -> True
SplicePat {} -> False
+ EmbTyPat {} -> True
XPat ext ->
case ghcPass @p of
GhcRn -> case ext of
@@ -747,6 +757,7 @@ patNeedsParens p = go @p
= conPatNeedsParens p ds
go (SigPat {}) = p >= sigPrec
go (ViewPat {}) = True
+ go (EmbTyPat {}) = True
go (XPat ext) = case ghcPass @q of
#if __GLASGOW_HASKELL__ < 901
GhcPs -> dataConCantHappen ext
diff --git a/compiler/GHC/Hs/Syn/Type.hs b/compiler/GHC/Hs/Syn/Type.hs
index edcdc39ea04beabd9474693b24daf70b587ec654..0b45ff88fd0eb1a461c238a05fcb0a055ab05eea 100644
--- a/compiler/GHC/Hs/Syn/Type.hs
+++ b/compiler/GHC/Hs/Syn/Type.hs
@@ -63,6 +63,7 @@ hsPatType (ConPat { pat_con = lcon
hsPatType (SigPat ty _ _) = ty
hsPatType (NPat ty _ _ _) = ty
hsPatType (NPlusKPat ty _ _ _ _ _) = ty
+hsPatType (EmbTyPat ty _ _) = typeKind ty
hsPatType (XPat ext) =
case ext of
CoPat _ _ ty -> ty
@@ -142,6 +143,7 @@ hsExprType (HsUntypedSplice ext _) = dataConCantHappen ext
hsExprType (HsProc _ _ lcmd_top) = lhsCmdTopType lcmd_top
hsExprType (HsStatic (_, ty) _s) = ty
hsExprType (HsPragE _ _ e) = lhsExprType e
+hsExprType (HsEmbTy x _ _) = dataConCantHappen x
hsExprType (XExpr (WrapExpr (HsWrap wrap e))) = hsWrapperType wrap $ hsExprType e
hsExprType (XExpr (ExpansionExpr (HsExpanded _ tc_e))) = hsExprType tc_e
hsExprType (XExpr (ConLikeTc con _ _)) = conLikeType con
diff --git a/compiler/GHC/Hs/Utils.hs b/compiler/GHC/Hs/Utils.hs
index afa7821031761eb942dc714f0d5440454b6a6ce1..7f9883432e19253e2f967e009f026cd5760b6ddf 100644
--- a/compiler/GHC/Hs/Utils.hs
+++ b/compiler/GHC/Hs/Utils.hs
@@ -1233,11 +1233,15 @@ collect_pat flag pat bndrs = case pat of
NPat {} -> bndrs
NPlusKPat _ n _ _ _ _ -> unXRec @p n : bndrs
SigPat _ pat sig -> case flag of
- CollVarTyVarBinders -> collect_lpat flag pat bndrs
- ++ collectPatSigBndrs sig
- _ -> collect_lpat flag pat bndrs
+ CollNoDictBinders -> collect_lpat flag pat bndrs
+ CollWithDictBinders -> collect_lpat flag pat bndrs
+ CollVarTyVarBinders -> collect_lpat flag pat bndrs ++ collectPatSigBndrs sig
XPat ext -> collectXXPat @p flag ext bndrs
SplicePat ext _ -> collectXSplicePat @p flag ext bndrs
+ EmbTyPat _ _ tp -> case flag of
+ CollNoDictBinders -> bndrs
+ CollWithDictBinders -> bndrs
+ CollVarTyVarBinders -> collectTyPatBndrs tp ++ bndrs
-- See Note [Dictionary binders in ConPatOut]
ConPat {pat_args=ps} -> case flag of
CollNoDictBinders -> foldr (collect_lpat flag) bndrs (hsConPatArgs ps)
diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs
index 29fc3a5713c356a695c7e444f8f4697923e8499a..59970138dd1b27d194350cb5efaf384ec8878257 100644
--- a/compiler/GHC/HsToCore/Expr.hs
+++ b/compiler/GHC/HsToCore/Expr.hs
@@ -365,6 +365,8 @@ dsExpr (ExplicitSum types alt arity expr)
dsExpr (HsPragE _ prag expr) =
ds_prag_expr prag expr
+dsExpr (HsEmbTy x _ _) = dataConCantHappen x
+
dsExpr (HsCase ctxt discrim matches)
= do { core_discrim <- dsLExpr discrim
; ([discrim_var], matching_code) <- matchWrapper ctxt (Just [discrim]) matches
diff --git a/compiler/GHC/HsToCore/Match.hs b/compiler/GHC/HsToCore/Match.hs
index 54f9741f01b617d17d25fc0705b8e0e15e7fc9b0..5914371dc97263bb935af4050888087f2470521b 100644
--- a/compiler/GHC/HsToCore/Match.hs
+++ b/compiler/GHC/HsToCore/Match.hs
@@ -1265,6 +1265,7 @@ patGroup _ (NPlusKPat _ _ (L _ (OverLit {ol_val=oval})) _ _ _) =
_ -> pprPanic "patGroup NPlusKPat" (ppr oval)
patGroup _ (ViewPat _ expr p) = PgView expr (hsPatType (unLoc p))
patGroup platform (LitPat _ lit) = PgLit (hsLitKey platform lit)
+patGroup _ EmbTyPat{} = PgAny
patGroup platform (XPat ext) = case ext of
CoPat _ p _ -> PgCo (hsPatType p) -- Type of innelexp pattern
ExpansionPat _ p -> patGroup platform p
diff --git a/compiler/GHC/HsToCore/Pmc/Desugar.hs b/compiler/GHC/HsToCore/Pmc/Desugar.hs
index 118feb87af9f8ed60ba58e187416803d7af8766d..0382ee61d6a03e5177182baeeda36db8c6b149b3 100644
--- a/compiler/GHC/HsToCore/Pmc/Desugar.hs
+++ b/compiler/GHC/HsToCore/Pmc/Desugar.hs
@@ -123,6 +123,7 @@ desugarPat x pat = case pat of
AsPat _ (L _ y) _ p -> (mkPmLetVar y x ++) <$> desugarLPat y p
SigPat _ p _ty -> desugarLPat x p
+ EmbTyPat _ _ _ -> pure []
XPat ext -> case ext of
diff --git a/compiler/GHC/HsToCore/Quote.hs b/compiler/GHC/HsToCore/Quote.hs
index 69db68f8652b034e103f59040511f3c622fcbedf..0e37c632ecb8ae62cd21f69f09605bf154ed73e7 100644
--- a/compiler/GHC/HsToCore/Quote.hs
+++ b/compiler/GHC/HsToCore/Quote.hs
@@ -1666,6 +1666,9 @@ repE (HsGetField _ e (L _ (DotFieldOcc _ (L _ (FieldLabelString f))))) = do
e1 <- repLE e
repGetField e1 f
repE (HsProjection _ xs) = repProjection (fmap (field_label . unLoc . dfoLabel . unLoc) xs)
+repE (HsEmbTy _ _ t) = do
+ t1 <- repLTy (hswc_body t)
+ rep2 typeEName [unC t1]
repE (XExpr (HsExpanded orig_expr ds_expr))
= do { rebindable_on <- lift $ xoptM LangExt.RebindableSyntax
; if rebindable_on -- See Note [Quotation and rebindable syntax]
@@ -2123,6 +2126,8 @@ repP p@(NPat _ (L _ l) (Just _) _)
repP (SigPat _ p t) = do { p' <- repLP p
; t' <- repLTy (hsPatSigType t)
; repPsig p' t' }
+repP (EmbTyPat _ _ t) = do { t' <- repLTy (hstp_body t)
+ ; repPtype t' }
repP (SplicePat (HsUntypedSpliceNested n) _) = rep_splice n
repP p@(SplicePat (HsUntypedSpliceTop _ _) _) = pprPanic "repP: top level splice" (ppr p)
repP other = notHandled (ThExoticPattern other)
@@ -2379,6 +2384,9 @@ repPview (MkC e) (MkC p) = rep2 viewPName [e,p]
repPsig :: Core (M TH.Pat) -> Core (M TH.Type) -> MetaM (Core (M TH.Pat))
repPsig (MkC p) (MkC t) = rep2 sigPName [p, t]
+repPtype :: Core (M TH.Type) -> MetaM (Core (M TH.Pat))
+repPtype (MkC t) = rep2 typePName [t]
+
--------------- Expressions -----------------
repVarOrCon :: Name -> Core TH.Name -> MetaM (Core (M TH.Exp))
repVarOrCon vc str
diff --git a/compiler/GHC/HsToCore/Ticks.hs b/compiler/GHC/HsToCore/Ticks.hs
index c3b50537855f78c2c562f7c86ac3062644ae225a..cf6fbac0677ebc82cc3d68e0cbb768f5d36c9dfb 100644
--- a/compiler/GHC/HsToCore/Ticks.hs
+++ b/compiler/GHC/HsToCore/Ticks.hs
@@ -478,6 +478,7 @@ addTickHsExpr e@(HsIPVar {}) = return e
addTickHsExpr e@(HsOverLit {}) = return e
addTickHsExpr e@(HsOverLabel{}) = return e
addTickHsExpr e@(HsLit {}) = return e
+addTickHsExpr e@(HsEmbTy {}) = return e
addTickHsExpr (HsLam x mg) = liftM (HsLam x)
(addTickMatchGroup True mg)
addTickHsExpr (HsLamCase x lc_variant mgs) = liftM (HsLamCase x lc_variant)
diff --git a/compiler/GHC/Iface/Ext/Ast.hs b/compiler/GHC/Iface/Ext/Ast.hs
index a2578641ca909c395eb886cc247dfe1579c68a7e..26d3578b0fb669617d0f57dab91836e03d32e06e 100644
--- a/compiler/GHC/Iface/Ext/Ast.hs
+++ b/compiler/GHC/Iface/Ext/Ast.hs
@@ -1027,6 +1027,9 @@ instance HiePass p => ToHie (PScoped (LocatedA (Pat (GhcPass p)))) where
sig
HieRn -> pure []
]
+ EmbTyPat _ _ tp ->
+ [ toHie $ TS (ResolvedScopes [scope, pscope]) tp
+ ]
XPat e ->
case hiePass @p of
HieRn -> case e of
@@ -1199,6 +1202,9 @@ instance HiePass p => ToHie (LocatedA (HsExpr (GhcPass p))) where
HsStatic _ expr ->
[ toHie expr
]
+ HsEmbTy _ _ ty ->
+ [ toHie $ TS (ResolvedScopes []) ty
+ ]
HsTypedBracket xbracket b -> case hiePass @p of
HieRn ->
[ toHie b
diff --git a/compiler/GHC/Parser.y b/compiler/GHC/Parser.y
index 6af984715868e747f672551c86c758743e34b7ee..3b089726b680caeb635cfcd5ba031e0d2676ce84 100644
--- a/compiler/GHC/Parser.y
+++ b/compiler/GHC/Parser.y
@@ -2738,6 +2738,11 @@ exp :: { ECP }
| infixexp %shift { $1 }
| exp_prag(exp) { $1 } -- See Note [Pragmas and operator fixity]
+ -- Embed types into expressions and patterns for required type arguments
+ | 'type' atype
+ {% do { requireExplicitNamespaces (getLoc $1)
+ ; return $ ECP $ mkHsEmbTyPV (comb2 $1 (reLoc $>)) (hsTok $1) $2 } }
+
infixexp :: { ECP }
: exp10 { $1 }
| infixexp qop exp10p -- See Note [Pragmas and operator fixity]
diff --git a/compiler/GHC/Parser/PostProcess.hs b/compiler/GHC/Parser/PostProcess.hs
index caa0c35f0d8fb3abd15a900e36f1feab12760784..ea8f19053a1c3194e94cc97c6178f565d6f73eaf 100644
--- a/compiler/GHC/Parser/PostProcess.hs
+++ b/compiler/GHC/Parser/PostProcess.hs
@@ -96,6 +96,7 @@ module GHC.Parser.PostProcess (
failOpFewArgs,
failNotEnabledImportQualifiedPost,
failImportQualifiedTwice,
+ requireExplicitNamespaces,
SumOrTuple (..),
@@ -1643,6 +1644,8 @@ class (b ~ (Body b) GhcPs, AnnoBody b) => DisambECP b where
-- | Disambiguate tuple sections and unboxed sums
mkSumOrTuplePV
:: SrcSpanAnnA -> Boxity -> SumOrTuple b -> [AddEpAnn] -> PV (LocatedA b)
+ -- | Disambiguate "type t" (embedded type)
+ mkHsEmbTyPV :: SrcSpan -> LHsToken "type" GhcPs -> LHsType GhcPs -> PV (LocatedA b)
-- | Validate infixexp LHS to reject unwanted {-# SCC ... #-} pragmas
rejectPragmaPV :: LocatedA b -> PV ()
@@ -1762,6 +1765,7 @@ instance DisambECP (HsCmd GhcPs) where
mkHsBangPatPV l c _ = cmdFail l $
text "!" <> ppr c
mkSumOrTuplePV l boxity a _ = cmdFail (locA l) (pprSumOrTuple boxity a)
+ mkHsEmbTyPV l _ ty = cmdFail l (text "type" <+> ppr ty)
rejectPragmaPV _ = return ()
cmdFail :: SrcSpan -> SDoc -> PV a
@@ -1858,6 +1862,9 @@ instance DisambECP (HsExpr GhcPs) where
mkHsBangPatPV l e _ = addError (mkPlainErrorMsgEnvelope l $ PsErrBangPatWithoutSpace e)
>> return (L (noAnnSrcSpan l) (hsHoleExpr noAnn))
mkSumOrTuplePV = mkSumOrTupleExpr
+ mkHsEmbTyPV l toktype ty =
+ return $ L (noAnnSrcSpan l) $
+ HsEmbTy noExtField toktype (mkHsWildCardBndrs ty)
rejectPragmaPV (L _ (OpApp _ _ _ e)) =
-- assuming left-associative parsing of operators
rejectPragmaPV e
@@ -1943,6 +1950,9 @@ instance DisambECP (PatBuilder GhcPs) where
hintBangPat l pb
return $ L (noAnnSrcSpan l) (PatBuilderPat pb)
mkSumOrTuplePV = mkSumOrTuplePat
+ mkHsEmbTyPV l toktype ty =
+ return $ L (noAnnSrcSpan l) $
+ PatBuilderPat (EmbTyPat noExtField toktype (mkHsTyPat noAnn ty))
rejectPragmaPV _ = return ()
-- | Ensure that a literal pattern isn't of type Addr#, Float#, Double#.
@@ -2894,9 +2904,7 @@ mkModuleImpExp warning anns (L l specname) subs = do
mkTypeImpExp :: LocatedN RdrName -- TcCls or Var name space
-> P (LocatedN RdrName)
mkTypeImpExp name =
- do allowed <- getBit ExplicitNamespacesBit
- unless allowed $ addError $ mkPlainErrorMsgEnvelope (getLocA name) $
- PsErrIllegalExplicitNamespace
+ do requireExplicitNamespaces (getLocA name)
return (fmap (`setRdrNameSpace` tcClsName) name)
checkImportSpec :: LocatedL [LIE GhcPs] -> P (LocatedL [LIE GhcPs])
@@ -2947,6 +2955,12 @@ failOpFewArgs (L loc op) =
; addFatalError $ mkPlainErrorMsgEnvelope (locA loc) $
(PsErrOpFewArgs is_star_type op) }
+requireExplicitNamespaces :: MonadP m => SrcSpan -> m ()
+requireExplicitNamespaces l = do
+ allowed <- getBit ExplicitNamespacesBit
+ unless allowed $
+ addError $ mkPlainErrorMsgEnvelope l PsErrIllegalExplicitNamespace
+
-----------------------------------------------------------------------------
-- Misc utils
diff --git a/compiler/GHC/Rename/Bind.hs b/compiler/GHC/Rename/Bind.hs
index 9d415328123a485cdaa4c930386a4cb269313dd2..bf0cc6abc65ae9384f42c6fd3eb7249927b1bd06 100644
--- a/compiler/GHC/Rename/Bind.hs
+++ b/compiler/GHC/Rename/Bind.hs
@@ -581,6 +581,10 @@ isOkNoBindPattern (L _ pat) =
ConPat _ _ cpd -> any lpatternContainsSplice (hsConPatArgs cpd)
XPat (HsPatExpanded _orig new) -> patternContainsSplice new
+ -- The behavior of this case is unimportant, as GHC will throw an error shortly
+ -- after reaching this case for other reasons (see TcRnIllegalTypePattern).
+ EmbTyPat{} -> True
+
{- Note [Pattern bindings that bind no variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Generally, we want to warn about pattern bindings like
diff --git a/compiler/GHC/Rename/Expr.hs b/compiler/GHC/Rename/Expr.hs
index 2965d290126ea77bb15f55264a278c35cf96e97d..03dd39f00eee7e6b73930fff09a8bc358ab36414 100644
--- a/compiler/GHC/Rename/Expr.hs
+++ b/compiler/GHC/Rename/Expr.hs
@@ -564,6 +564,10 @@ rnExpr (ArithSeq _ _ seq)
else
return (ArithSeq noExtField Nothing new_seq, fvs) }
+rnExpr (HsEmbTy _ toktype ty)
+ = do { (ty', fvs) <- rnHsWcType HsTypeCtx ty
+ ; return (HsEmbTy noExtField toktype ty', fvs) }
+
{-
************************************************************************
* *
@@ -2301,6 +2305,11 @@ isStrictPattern (L loc pat) =
NPat{} -> True
NPlusKPat{} -> True
SplicePat{} -> True
+
+ -- The behavior of this case is unimportant, as GHC will throw an error shortly
+ -- after reaching this case for other reasons (see TcRnIllegalTypePattern).
+ EmbTyPat{} -> False
+
XPat ext -> case ghcPass @p of
#if __GLASGOW_HASKELL__ < 811
GhcPs -> dataConCantHappen ext
diff --git a/compiler/GHC/Rename/Pat.hs b/compiler/GHC/Rename/Pat.hs
index 59e596a37934079cca860d3dfc3c38bc942d1b41..7412f0bfd536081483b7b71f9d064eb7dadebefc 100644
--- a/compiler/GHC/Rename/Pat.hs
+++ b/compiler/GHC/Rename/Pat.hs
@@ -633,6 +633,10 @@ rnPatAndThen mk (SplicePat _ splice)
(rn_splice, HsUntypedSpliceNested splice_name) -> return (SplicePat (HsUntypedSpliceNested splice_name) rn_splice) -- Splice was nested and thus already renamed
}
+rnPatAndThen _ (EmbTyPat _ toktype tp)
+ = do { tp' <- rnHsTyPat HsTypePatCtx tp
+ ; return (EmbTyPat noExtField toktype tp') }
+
--------------------
rnConPatAndThen :: NameMaker
-> LocatedN RdrName -- the constructor
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index 27ca34f9fc0c617f7ab485b88344a5947c37e7b7..a698af9dff4b8ea8bf202e3f4fcba2d9bac5a982 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -435,11 +435,10 @@ instance Diagnostic TcRnMessage where
TcRnIllegalInstance reason ->
mkSimpleDecorated $ pprIllegalInstance reason
TcRnVDQInTermType mb_ty
- -> mkSimpleDecorated $ vcat
- [ case mb_ty of
+ -> mkSimpleDecorated $
+ case mb_ty of
Nothing -> main_msg
Just ty -> hang (main_msg <> char ':') 2 (pprType ty)
- , text "(GHC does not yet support this)" ]
where
main_msg =
text "Illegal visible, dependent quantification" <+>
@@ -1231,6 +1230,25 @@ instance Diagnostic TcRnMessage where
hang (text "Missing role annotation" <> colon)
2 (text "type role" <+> ppr name <+> hsep (map ppr roles))
+ TcRnIllformedTypePattern p
+ -> mkSimpleDecorated $
+ hang (text "Ill-formed type pattern:") 2 (ppr p) $$
+ text "Expected a type pattern introduced with the"
+ <+> quotes (text "type") <+> text "keyword."
+ TcRnIllegalTypePattern
+ -> mkSimpleDecorated $
+ text "Illegal type pattern." $$
+ text "A type pattern must be checked against a visible forall."
+ TcRnIllformedTypeArgument e
+ -> mkSimpleDecorated $
+ hang (text "Ill-formed type argument:") 2 (ppr e) $$
+ text "Expected a type expression introduced with the"
+ <+> quotes (text "type") <+> text "keyword."
+ TcRnIllegalTypeExpr
+ -> mkSimpleDecorated $
+ text "Illegal type expression." $$
+ text "A type expression must be used to instantiate a visible forall."
+
TcRnCapturedTermName tv_name shadowed_term_names
-> mkSimpleDecorated $
text "The type variable" <+> quotes (ppr tv_name) <+>
@@ -2418,6 +2436,14 @@ instance Diagnostic TcRnMessage where
-> WarningWithFlag Opt_WarnImplicitRhsQuantification
TcRnPatersonCondFailure{}
-> ErrorWithoutFlag
+ TcRnIllformedTypePattern{}
+ -> ErrorWithoutFlag
+ TcRnIllegalTypePattern{}
+ -> ErrorWithoutFlag
+ TcRnIllformedTypeArgument{}
+ -> ErrorWithoutFlag
+ TcRnIllegalTypeExpr{}
+ -> ErrorWithoutFlag
diagnosticHints = \case
TcRnUnknownMessage m
@@ -2537,8 +2563,9 @@ instance Diagnostic TcRnMessage where
-> noHints
TcRnForAllEscapeError{}
-> noHints
- TcRnVDQInTermType{}
- -> noHints
+ TcRnVDQInTermType mb_ty
+ | isJust mb_ty -> [suggestExtension LangExt.RequiredTypeArguments]
+ | otherwise -> []
TcRnBadQuantPredHead{}
-> noHints
TcRnIllegalTupleConstraint{}
@@ -3061,6 +3088,14 @@ instance Diagnostic TcRnMessage where
-> [SuggestBindTyVarOnLhs (unLoc kv)]
TcRnPatersonCondFailure{}
-> [suggestExtension LangExt.UndecidableInstances]
+ TcRnIllformedTypePattern{}
+ -> noHints
+ TcRnIllegalTypePattern{}
+ -> noHints
+ TcRnIllformedTypeArgument{}
+ -> noHints
+ TcRnIllegalTypeExpr{}
+ -> noHints
diagnosticCode :: TcRnMessage -> Maybe DiagnosticCode
diagnosticCode = constructorCode
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index 8b566a095b6e4bf05d6e95b2d08809abbd65a78b..2d9e197d69f631df0bca8e2c51f680d76b361558 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -4027,6 +4027,77 @@ data TcRnMessage where
-}
TcRnImplicitRhsQuantification :: LocatedN RdrName -> TcRnMessage
+ {-| TcRnIllformedTypePattern is an error raised when the pattern
+ corresponding to a required type argument (visible forall)
+ does not have a form that can be interpreted as a type pattern.
+
+ At the moment, only patterns constructed using the @type@ keyword
+ are considered well-formed, but this restriction will be relaxed
+ when part 2 of GHC Proposal #281 is implemented.
+
+ Example:
+
+ vfun :: forall (a :: k) -> ()
+ vfun x = ()
+ -- ^
+ -- expected `type x` instead of `x`
+
+ Test cases:
+ T22326_fail_raw_pat
+ -}
+ TcRnIllformedTypePattern :: !(Pat GhcRn) -> TcRnMessage
+
+ {-| TcRnIllegalTypePattern is an error raised when a pattern constructed
+ with the @type@ keyword occurs in a position that does not correspond
+ to a required type argument (visible forall).
+
+ Example:
+
+ case x of
+ (type _) -> True -- the (type _) pattern is illegal here
+ _ -> False
+
+ Test cases:
+ T22326_fail_ado
+ T22326_fail_caseof
+ -}
+ TcRnIllegalTypePattern :: TcRnMessage
+
+ {-| TcRnIllformedTypeArgument is an error raised when an argument
+ that specifies a required type argument (instantiates a visible forall)
+ does not have a form that can be interpreted as a type argument.
+
+ At the moment, only expressions constructed using the @type@ keyword
+ are considered well-formed, but this restriction will be relaxed
+ when part 2 of GHC Proposal #281 is implemented.
+
+ Example:
+
+ vfun :: forall (a :: k) -> ()
+ x = vfun Int
+ -- ^^^
+ -- expected `type Int` instead of `Int`
+
+ Test cases:
+ T22326_fail_raw_arg
+ -}
+ TcRnIllformedTypeArgument :: !(LHsExpr GhcRn) -> TcRnMessage
+
+ {-| TcRnIllegalTypeExpr is an error raised when an expression constructed
+ with the @type@ keyword occurs in a position that does not correspond
+ to a required type argument (visible forall).
+
+ Example:
+
+ xtop = type Int -- not a function argument
+ xarg = length (type Int) -- `length` does not expect a required type argument
+
+ Test cases:
+ T22326_fail_app
+ T22326_fail_top
+ -}
+ TcRnIllegalTypeExpr :: TcRnMessage
+
deriving Generic
diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs
index 7d1a7cbbffbf512c5a8871c9becb2b916cd1e588..317d1b856ecbb94bc759285e68236a7d6d60a65f 100644
--- a/compiler/GHC/Tc/Gen/App.hs
+++ b/compiler/GHC/Tc/Gen/App.hs
@@ -597,6 +597,11 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args
-- go1: fun_ty is not filled-in instantiation variable
-- ('go' dealt with that case)
+ -- Handle out-of-scope functions gracefully
+ go1 delta acc so_far fun_ty (arg : rest_args)
+ | fun_is_out_of_scope, looks_like_type_arg arg -- See Note [VTA for out-of-scope functions]
+ = go delta acc so_far fun_ty rest_args
+
-- Rule IALL from Fig 4 of the QL paper
-- c.f. GHC.Tc.Utils.Instantiate.topInstantiate
go1 delta acc so_far fun_ty args
@@ -630,6 +635,14 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args
-- Going around again means we deal easily with
-- nested forall a. Eq a => forall b. Show b => blah
+ -- Rule ITVDQ from the GHC Proposal #281
+ go1 delta acc so_far fun_ty ((EValArg { eva_arg = ValArg arg }) : rest_args)
+ | Just (tvb, body) <- tcSplitForAllTyVarBinder_maybe fun_ty
+ , binderFlag tvb == Required
+ = do { (ty_arg, inst_body) <- tcVDQ fun_conc_tvs (tvb, body) arg
+ ; let wrap = mkWpTyApps [ty_arg]
+ ; go delta (addArgWrap wrap acc) so_far inst_body rest_args }
+
-- Rule IRESULT from Fig 4 of the QL paper
go1 delta acc _ fun_ty []
= do { traceTc "tcInstFun:ret" (ppr fun_ty)
@@ -644,10 +657,6 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args
-- Rule ITYARG from Fig 4 of the QL paper
go1 delta acc so_far fun_ty ( ETypeArg { eva_ctxt = ctxt, eva_at = at, eva_hs_ty = hs_ty }
: rest_args )
- | fun_is_out_of_scope -- See Note [VTA for out-of-scope functions]
- = go delta acc so_far fun_ty rest_args
-
- | otherwise
= do { (ty_arg, inst_ty) <- tcVTA fun_conc_tvs fun_ty hs_ty
; let arg' = ETypeArg { eva_ctxt = ctxt, eva_at = at, eva_hs_ty = hs_ty, eva_ty = ty_arg }
; go delta (arg' : acc) so_far inst_ty rest_args }
@@ -727,6 +736,31 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args
: addArgWrap wrap acc
; go delta' acc' (arg_ty:so_far) res_ty rest_args }
+-- Is the argument supposed to instantiate a forall?
+--
+-- In other words, given a function application `fn arg`,
+-- can we look at the `arg` and conclude that `fn :: forall x. t`
+-- or `fn :: forall x -> t`?
+--
+-- This is a conservative heuristic that returns `False` for "don't know".
+-- Used to improve error messages only.
+-- See Note [VTA for out-of-scope functions].
+looks_like_type_arg :: HsExprArg 'TcpRn -> Bool
+looks_like_type_arg ETypeArg{} =
+ -- The argument is clearly supposed to instantiate an invisible forall,
+ -- i.e. when we see `f @a`, we expect `f :: forall x. t`.
+ True
+looks_like_type_arg EValArg{ eva_arg = ValArg (L _ e) } =
+ -- Check if the argument is supposed to instantiate a visible forall,
+ -- i.e. when we see `f (type Int)`, we expect `f :: forall x -> t`,
+ -- but not if we see `f True`.
+ -- We can't say for sure though. Part 2 of GHC Proposal #281 allows
+ -- type arguments without the `type` qualifier, so `f True` could
+ -- instantiate `forall (b :: Bool) -> t`.
+ case stripParensHsExpr e of
+ HsEmbTy _ _ _ -> True
+ _ -> False
+looks_like_type_arg _ = False
addArgCtxt :: AppCtxt -> LHsExpr GhcRn
-> TcM a -> TcM a
@@ -757,6 +791,7 @@ addArgCtxt ctxt (L arg_loc arg) thing_inside
* *
********************************************************************* -}
+-- See Note [Visible type application and abstraction]
tcVTA :: ConcreteTyVars
-- ^ Type variables that must be instantiated to concrete types.
--
@@ -770,9 +805,28 @@ tcVTA :: ConcreteTyVars
tcVTA conc_tvs fun_ty hs_ty
| Just (tvb, inner_ty) <- tcSplitForAllTyVarBinder_maybe fun_ty
, binderFlag tvb == Specified
- -- It really can't be Inferred, because we've just
- -- instantiated those. But, oddly, it might just be Required.
- -- See Note [Required quantifiers in the type of a term]
+ = do { tc_inst_forall_arg conc_tvs (tvb, inner_ty) hs_ty }
+
+ | otherwise
+ = do { (_, fun_ty) <- liftZonkM $ zonkTidyTcType emptyTidyEnv fun_ty
+ ; failWith $ TcRnInvalidTypeApplication fun_ty hs_ty }
+
+-- See Note [Visible type application and abstraction]
+tcVDQ :: ConcreteTyVars -- See Note [Representation-polymorphism checking built-ins]
+ -> (ForAllTyBinder, TcType) -- Function type
+ -> LHsExpr GhcRn -- Argument type
+ -> TcM (TcType, TcType)
+tcVDQ conc_tvs (tvb, inner_ty) arg
+ = do { hs_ty <- case stripParensLHsExpr arg of
+ L _ (HsEmbTy _ _ hs_ty) -> return hs_ty
+ e -> failWith $ TcRnIllformedTypeArgument e
+ ; tc_inst_forall_arg conc_tvs (tvb, inner_ty) hs_ty }
+
+tc_inst_forall_arg :: ConcreteTyVars -- See Note [Representation-polymorphism checking built-ins]
+ -> (ForAllTyBinder, TcType) -- Function type
+ -> LHsWcType GhcRn -- Argument type
+ -> TcM (TcType, TcType)
+tc_inst_forall_arg conc_tvs (tvb, inner_ty) hs_ty
= do { let tv = binderVar tvb
kind = tyVarKind tv
tv_nm = tyVarName tv
@@ -805,40 +859,260 @@ tcVTA conc_tvs fun_ty hs_ty
; inner_ty <- liftZonkM $ zonkTcType inner_ty
-- See Note [Visible type application zonk]
- ; let in_scope = mkInScopeSet (tyCoVarsOfTypes [fun_ty, ty_arg])
+ ; let fun_ty = mkForAllTy tvb inner_ty
+ in_scope = mkInScopeSet (tyCoVarsOfTypes [fun_ty, ty_arg])
insted_ty = substTyWithInScope in_scope [tv] [ty_arg] inner_ty
-- NB: tv and ty_arg have the same kind, so this
-- substitution is kind-respecting
- ; traceTc "VTA" (vcat [ text "fun_ty" <+> ppr fun_ty
- , text "tv" <+> ppr tv <+> dcolon <+> debugPprType kind
- , text "ty_arg" <+> debugPprType ty_arg <+> dcolon
- <+> debugPprType (typeKind ty_arg)
- , text "inner_ty" <+> debugPprType inner_ty
- , text "insted_ty" <+> debugPprType insted_ty ])
- ; return (ty_arg, insted_ty) }
-
- | otherwise
- = do { (_, fun_ty) <- liftZonkM $ zonkTidyTcType emptyTidyEnv fun_ty
- ; failWith $ TcRnInvalidTypeApplication fun_ty hs_ty }
-
-{- Note [Required quantifiers in the type of a term]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider (#15859)
-
- data A k :: k -> Type -- A :: forall k -> k -> Type
- type KindOf (a :: k) = k -- KindOf :: forall k. k -> Type
- a = (undefined :: KindOf A) @Int
-With ImpredicativeTypes (thin ice, I know), we instantiate
-KindOf at type (forall k -> k -> Type), so
- KindOf A = forall k -> k -> Type
-whose first argument is Required
-
-We want to reject this type application to Int, but in earlier
-GHCs we had an ASSERT that Required could not occur here.
+ ; traceTc "tc_inst_forall_arg (VTA/VDQ)" (
+ vcat [ text "fun_ty" <+> ppr fun_ty
+ , text "tv" <+> ppr tv <+> dcolon <+> debugPprType kind
+ , text "ty_arg" <+> debugPprType ty_arg <+> dcolon
+ <+> debugPprType (typeKind ty_arg)
+ , text "inner_ty" <+> debugPprType inner_ty
+ , text "insted_ty" <+> debugPprType insted_ty ])
+ ; return (ty_arg, insted_ty) }
-The ice is thin; c.f. Note [No Required PiTyBinder in terms]
-in GHC.Core.TyCo.Rep.
+{- Note [Visible type application and abstraction]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+GHC supports the types
+ forall {a}. a -> t -- ForAllTyFlag is Inferred
+ forall a. a -> t -- ForAllTyFlag is Specified
+ forall a -> a -> t -- ForAllTyFlag is Required
+
+The design of type abstraction and type application for those types has gradually
+evolved over time, and is based on the following papers and proposals:
+ - "Visible Type Application"
+ https://richarde.dev/papers/2016/type-app/visible-type-app.pdf
+ - "Type Variables in Patterns"
+ https://richarde.dev/papers/2018/pat-tyvars/pat-tyvars.pdf
+ - "Modern Scoped Type Variables"
+ https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0448-type-variable-scoping.rst
+ - "Visible forall in types of terms"
+ https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst
+
+Here we offer an overview of the design mixed with commentary on the
+implementation status. The proposals have not been fully implemented at the
+time of writing this Note (see "not implemented" in the rest of this Note).
+
+Now consider functions
+ fi :: forall {a}. a -> t -- Inferred: type argument cannot be supplied
+ fs :: forall a. a -> t -- Specified: type argument may be supplied
+ fr :: forall a -> a -> t -- Required: type argument must be supplied
+
+At a call site we may have calls looking like this
+ fi True -- Inferred: no visible type argument
+ fs True -- Specified: type argument omitted
+ fs @Bool True -- Specified: type argument supplied
+ fr (type Bool) True -- Required: type argument is compulsory, `type` qualifier used
+ fr Bool True -- Required: type argument is compulsory, `type` qualifier omitted (NB: not implemented)
+
+At definition sites we may have type /patterns/ to abstract over type variables
+ fi x = rhs -- Inferred: no type pattern
+ fs x = rhs -- Specified: type pattern omitted
+ fs @a (x :: a) = rhs -- Specified: type pattern supplied (NB: not implemented)
+ fr (type a) (x :: a) = rhs -- Required: type pattern is compulsory, `type` qualifier used
+ fr a (x :: a) = rhs -- Required: type pattern is compulsory, `type` qualifier omitted (NB: not implemented)
+
+Type patterns in lambdas work the same way as they do in a function LHS
+ fs = \ x -> rhs -- Specified: type pattern omitted
+ fs = \ @a (x :: a) -> rhs -- Specified: type pattern supplied (NB: not implemented)
+ fr = \ (type a) (x :: a) -> rhs -- Required: type pattern is compulsory, `type` qualifier used
+ fr = \ a (x :: a) -> rhs -- Required: type pattern is compulsory, `type` qualifier omitted (NB: not implemented)
+
+Type patterns may also occur in a constructor pattern. Consider the following data declaration
+ data T where
+ MkTI :: forall {a}. Show a => a -> T -- Inferred
+ MkTS :: forall a. Show a => a -> T -- Specified
+ MkTR :: forall a -> Show a => a -> T -- Required (NB: not implemented)
+
+Matching on its constructors may look like this
+ f (MkTI x) = rhs -- Inferred: no type pattern
+ f (MkTS x) = rhs -- Specified: type pattern omitted
+ f (MkTS @a (x :: a)) = rhs -- Specified: type pattern supplied
+ f (MkTR (type a) (x :: a)) = rhs -- Required: type pattern is compulsory, `type` qualifier used (NB: not implemented)
+ f (MkTR a (x :: a)) = rhs -- Required: type pattern is compulsory, `type` qualifier omitted (NB: not implemented)
+
+The moving parts are as follows:
+ (abbreviations used: "c.o." = "constructor of")
+
+Syntax of types
+---------------
+* The types are all initially represented with HsForAllTy (c.o. HsType).
+ The binders are in the (hst_tele :: HsForAllTelescope pass) field of the HsForAllTy
+ At this stage, we have
+ forall {a}. t -- HsForAllInvis (c.o. HsForAllTelescope) and InferredSpec (c.o. Specificity)
+ forall a. t -- HsForAllInvis (c.o. HsForAllTelescope) and SpecifiedSpec (c.o. Specificity)
+ forall a -> t -- HsForAllVis (c.o. HsForAllTelescope)
+
+* By the time we get to checking applications/abstractions (e.g. GHC.Tc.Gen.App)
+ the types have been kind-checked (e.g. by tcLHsType) into ForAllTy (c.o. Type).
+ At this stage, we have:
+ forall {a}. t -- ForAllTy (c.o. Type) and Inferred (c.o. ForAllTyFlag)
+ forall a. t -- ForAllTy (c.o. Type) and Specified (c.o. ForAllTyFlag)
+ forall a -> t -- ForAllTy (c.o. Type) and Required (c.o. ForAllTyFlag)
+
+Syntax of applications in HsExpr
+--------------------------------
+* We represent type applications in HsExpr like this (ignoring parameterisation)
+ data HsExpr = HsApp HsExpr HsExpr -- (f True) (plain function application)
+ | HsAppType HsExpr HsType -- (f @True) (function application with `@`)
+ | HsEmbTy HsType -- (type Int) (embed a type into an expression with `type`)
+ | ...
+
+* So (f @ty) is represented, just as you might expect:
+ HsAppType f ty
+
+* But (f (type ty)) is represented by:
+ HsApp f (HsEmbTy ty)
+
+ Why the difference? Because we /also/ need to express these /nested/ uses of `type`:
+
+ g (Maybe (type Int)) -- valid for g :: forall (a :: Type) -> t (NB. not implemented)
+ g (Either (type Int) (type Bool)) -- valid for g :: forall (a :: Type) -> t (NB. not implemented)
+
+ This nesting makes `type` rather different from `@`. Remember, the HsEmbTy mainly just
+ switches namespace, and is subject to the term-to-type transformation.
+
+Syntax of abstractions in Pat
+-----------------------------
+* Type patterns are represented in Pat roughly like this
+ data Pat = ConPat ConLike [HsTyPat] [Pat] -- (Con @tp1 @tp2 p1 p2) (constructor pattern)
+ | EmbTyPat HsTyPat -- (type tp) (embed a type into a pattern with `type`)
+ | ...
+ data HsTyPat = HsTP LHsType
+ (In ConPat, the type and term arguments are actually inside HsConPatDetails.)
+
+ * Similar to HsAppType in HsExpr, the [HsTyPat] in ConPat is used just for @ty arguments
+ * Similar to HsEmbTy in HsExpr, EmbTyPat lets you embed a type in a pattern
+
+* Examples:
+ \ (MkT @a (x :: a)) -> rhs -- ConPat (c.o. Pat) and HsConPatTyArg (c.o. HsConPatTyArg)
+ \ (type a) (x :: a) -> rhs -- EmbTyPat (c.o. Pat)
+ \ a (x :: a) -> rhs -- VarPat (c.o. Pat) (NB. not implemented)
+ \ @a (x :: a) -> rhs -- to be decided (NB. not implemented)
+
+* A HsTyPat is not necessarily a plain variable. At the very least,
+ we support kind signatures and wildcards:
+ \ (type _) -> rhs
+ \ (type (b :: Bool)) -> rhs
+ \ (type (_ :: Bool)) -> rhs
+ But in constructor patterns we also support full-on types
+ \ (P @(a -> Either b c)) -> rhs
+ All these forms are represented with HsTP (c.o. HsTyPat).
+
+Renaming type applications
+--------------------------
+rnExpr delegates renaming of type arguments to rnHsWcType if possible:
+ f @t -- HsAppType, t is renamed with rnHsWcType
+ f (type t) -- HsApp and HsEmbTy, t is renamed with rnHsWcType
+
+But what about:
+ f t -- HsApp, no HsEmbTy (NB. not implemented)
+We simply rename `t` as a term using a recursive call to rnExpr; in particular,
+the type of `f` does not affect name resolution (Lexical Scoping Principle).
+We will later convert `t` from a `HsExpr` to a `Type`, see "Typechecking type
+applications" later in this Note. The details are spelled out in the "Resolved
+Syntax Tree" and "T2T-Mapping" sections of GHC Proposal #281.
+
+Renaming type abstractions
+--------------------------
+rnPat delegates renaming of type arguments to rnHsTyPat if possible:
+ f (P @t) = rhs -- ConPat, t is renamed with rnHsTyPat
+ f (type t) = rhs -- EmbTyPat, t is renamed with rnHsTyPat
+
+But what about:
+ f t = rhs -- VarPat
+The solution is as before (see previous section), mutatis mutandis.
+Rename `t` as a pattern using a recursive call to `rnPat`, convert it
+to a type pattern later.
+
+One particularly prickly issue is that of implicit quantification. Consider:
+
+ f :: forall a -> ...
+ f t = ... -- binding site of `t`
+ where
+ g :: t -> t -- use site of `t` or a fresh variable?
+ g = ...
+
+Does the signature of `g` refer to `t` bound in `f`, or is it a fresh,
+implicitly quantified variable? This is normally controlled by
+ScopedTypeVariables, but in this example the renamer can't tell `t` from a term
+variable. Only later (in the type checker) will we find out that it stands for
+the forall-bound type variable `a`. So when RequiredTypeArguments is in effect,
+we change implicit quantification to take term variables into account; that is,
+we do not implicitly quantify the signature of `g` to `g :: forall t. t->t`
+because of the term-level `t` that is in scope. (NB. not implemented)
+See Note [Term variable capture and implicit quantification].
+
+Typechecking type applications
+------------------------------
+Type applications are checked alongside ordinary function applications
+in tcInstFun.
+
+First of all, we assume that the function type is known (i.e. not a metavariable)
+and contains a `forall`. Consider:
+ f :: forall a. a -> a
+ f x = const x (f @Int 5)
+If the type signature is removed, the definition results in an error:
+ Cannot apply expression of type ‘t1’
+ to a visible type argument ‘Int’
+
+The same principle applies to required type arguments:
+ f :: forall a -> a -> a
+ f (type a) x = const x (f (type Int) 5)
+If the type signature is removed, the error is:
+ Illegal type pattern.
+ A type pattern must be checked against a visible forall.
+
+When the type of the function is known and contains a `forall`, all we need to
+do is instantiate the forall-bound variable with the supplied type argument.
+This is done by tcVTA (if Specified) and tcVDQ (if Required).
+
+tcVDQ unwraps the HsEmbTy and uses the type contained within it. Crucially, in
+tcVDQ we know that we are expecting a type argument. This means that we can
+support
+ f (Maybe Int) -- HsApp, no HsEmbTy (NB. not implemented)
+The type argument (Maybe Int) is represented as an HsExpr, but tcVDQ can easily
+convert it to HsType. This conversion is called the "T2T-Mapping" in GHC
+Proposal #281.
+
+Typechecking type abstractions
+------------------------------
+Type abstractions are checked alongside ordinary patterns in GHC.Tc.Gen.Pat.tcPats.
+One of its inputs is a list of ExpPatType that has two constructors
+ * ExpFunPatTy ... -- the type A of a function A -> B
+ * ExpForAllPatTy ... -- the binder (a::A) of forall (a::A) -> B
+so when we are checking
+ f :: forall a b -> a -> b -> ...
+ f (type a) (type b) (x :: a) (y :: b) = ...
+our expected pattern types are
+ [ ExpForAllPatTy ... -- forall a ->
+ , ExpForAllPatTy ... -- forall b ->
+ , ExpFunPatTy ... -- a ->
+ , ExpFunPatTy ... -- b ->
+ ]
+
+The [ExpPatType] is initially constructed by GHC.Tc.Utils.Unify.matchExpectedFunTys,
+by decomposing the type signature for `f` in our example. If we are given a
+definition
+ g (type a) = ...
+we never /infer/ a type g :: forall a -> blah. We can only /check/
+explicit type abstractions in terms.
+
+The [ExpPatType] allows us to use different code paths for type abstractions
+and ordinary patterns:
+ * tc_pat :: Scaled ExpSigmaTypeFRR -> Checker (Pat GhcRn) (Pat GhcTc)
+ * tc_forall_pat :: Checker (Pat GhcRn, TcTyVar) (Pat GhcTc)
+
+tc_forall_pat unwraps the EmbTyPat and uses the type pattern contained
+within it. This is another spot where the "T2T-Mapping" can take place.
+This would allow us to support
+ f a (x :: a) = rhs -- no EmbTyPat (NB. not implemented)
+
+Type patterns in constructor patterns are handled in with tcConTyArg.
+Both tc_forall_pat and tcConTyArg delegate most of the work to tcHsTyPat.
Note [VTA for out-of-scope functions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -861,14 +1135,19 @@ give its type.
Fortunately in tcInstFun we still have access to the function, so we
can check if it is a HsUnboundVar. We use this info to simply skip
-over any visible type arguments. We've already inferred the type of
-the function (in tcInferAppHead), so we'll /already/ have emitted a
+over any visible type arguments. We'll /already/ have emitted a
Hole constraint; failing preserves that constraint.
We do /not/ want to fail altogether in this case (via failM) because
that may abandon an entire instance decl, which (in the presence of
-fdefer-type-errors) leads to leading to #17792.
+What about required type arguments? Suppose we see
+ f (type Int)
+where `f` is out of scope. Then again we don't want to crash because f's
+type (which will be just a fresh unification variable) isn't a visible forall.
+Instead we just skip the `(type Int)` argument, as before.
+
Downside: the typechecked term has lost its visible type arguments; we
don't even kind-check them. But let's jump that bridge if we come to
it. Meanwhile, let's not crash!
diff --git a/compiler/GHC/Tc/Gen/Arrow.hs b/compiler/GHC/Tc/Gen/Arrow.hs
index 0f06b5f9d7337de41f188c79398206ffa9d94572..e41b82ec59e88f1148f30fdb0dff62594ddcb462 100644
--- a/compiler/GHC/Tc/Gen/Arrow.hs
+++ b/compiler/GHC/Tc/Gen/Arrow.hs
@@ -359,7 +359,7 @@ tcCmdMatchLambda env
-- Check the patterns, and the GRHSs inside
tc_match arg_tys cmd_stk' (L mtch_loc (Match { m_pats = pats, m_grhss = grhss }))
= do { (pats', grhss') <- setSrcSpanA mtch_loc $
- tcPats match_ctxt pats arg_tys $
+ tcPats match_ctxt pats (map ExpFunPatTy arg_tys) $
tc_grhss grhss cmd_stk' (mkCheckExpType res_ty)
; return $ L mtch_loc (Match { m_ext = noAnn
diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs
index bfbbe9906a7bdd61b59fb7e75e8c3bf51f0796f8..0ab15dd2923607bd2a429a00ad5be12c48e60845 100644
--- a/compiler/GHC/Tc/Gen/Expr.hs
+++ b/compiler/GHC/Tc/Gen/Expr.hs
@@ -452,6 +452,8 @@ tcExpr (HsStatic fvs expr) res_ty
(L (noAnnSrcSpan loc) (HsStatic (fvs, mkTyConApp static_ptr_ty_con [expr_ty]) expr'))
}
+tcExpr (HsEmbTy _ _ _) _ = failWith TcRnIllegalTypeExpr
+
{-
************************************************************************
* *
@@ -789,7 +791,7 @@ tcSynArgE orig op sigma_ty syn_ty thing_inside
, res_wrapper ) -- :: res_ty_out "->" res_ty
, arg_wrapper1, [], arg_wrapper2 ) ) -- :: arg_ty "->" arg_ty_out
<- matchExpectedFunTys herald GenSigCtxt 1 (mkCheckExpType rho_ty) $
- \ [arg_ty] res_ty ->
+ \ [ExpFunPatTy arg_ty] res_ty ->
do { arg_tc_ty <- expTypeToType (scaledThing arg_ty)
; res_tc_ty <- expTypeToType res_ty
diff --git a/compiler/GHC/Tc/Gen/Match.hs b/compiler/GHC/Tc/Gen/Match.hs
index c77c66b8b417cb1677cc1d5d3f2a1ef08ce1726a..5bfdfd7f537b8c9072413b790587b568a2210859 100644
--- a/compiler/GHC/Tc/Gen/Match.hs
+++ b/compiler/GHC/Tc/Gen/Match.hs
@@ -80,6 +80,7 @@ import GHC.Types.SrcLoc
import Control.Monad
import Control.Arrow ( second )
import qualified Data.List.NonEmpty as NE
+import Data.Maybe (mapMaybe)
{-
************************************************************************
@@ -106,7 +107,7 @@ tcMatchesFun fun_name matches exp_ty
-- sensible location. Note: we have to do this odd
-- ann-grabbing, because we don't always have annotations in
-- hand when we call tcMatchesFun...
- traceTc "tcMatchesFun" (ppr fun_name $$ ppr exp_ty)
+ traceTc "tcMatchesFun" (ppr fun_name $$ ppr exp_ty $$ ppr arity)
; checkArgCounts what matches
; matchExpectedFunTys herald ctxt arity exp_ty $ \ pat_tys rhs_ty ->
@@ -139,7 +140,7 @@ tcMatchesFun fun_name matches exp_ty
parser guarantees that each equation has exactly one argument.
-}
-tcMatchesCase :: (AnnoBody body) =>
+tcMatchesCase :: (AnnoBody body, Outputable (body GhcTc)) =>
TcMatchCtxt body -- ^ Case context
-> Scaled TcSigmaTypeFRR -- ^ Type of scrutinee
-> MatchGroup GhcRn (LocatedA (body GhcRn)) -- ^ The case alternatives
@@ -149,7 +150,7 @@ tcMatchesCase :: (AnnoBody body) =>
-- wrapper goes from MatchGroup's ty to expected ty
tcMatchesCase ctxt (Scaled scrut_mult scrut_ty) matches res_ty
- = tcMatches ctxt [Scaled scrut_mult (mkCheckExpType scrut_ty)] res_ty matches
+ = tcMatches ctxt [ExpFunPatTy (Scaled scrut_mult (mkCheckExpType scrut_ty))] res_ty matches
tcMatchLambda :: ExpectedFunTyOrigin -- see Note [Herald for matchExpectedFunTys] in GHC.Tc.Utils.Unify
-> TcMatchCtxt HsExpr
@@ -209,8 +210,9 @@ type AnnoBody body
)
-- | Type-check a MatchGroup.
-tcMatches :: (AnnoBody body ) => TcMatchCtxt body
- -> [Scaled ExpSigmaTypeFRR] -- ^ Expected pattern types.
+tcMatches :: (AnnoBody body, Outputable (body GhcTc)) =>
+ TcMatchCtxt body
+ -> [ExpPatType] -- ^ Expected pattern types.
-> ExpRhoType -- ^ Expected result-type of the Match.
-> MatchGroup GhcRn (LocatedA (body GhcRn))
-> TcM (MatchGroup GhcTc (LocatedA (body GhcTc)))
@@ -222,7 +224,7 @@ tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches
-- when in inference mode, so we must do it ourselves,
-- here, using expTypeToType
= do { tcEmitBindingUsage bottomUE
- ; pat_tys <- mapM scaledExpTypeToType pat_tys
+ ; pat_tys <- mapM scaledExpTypeToType (filter_out_forall_pat_tys pat_tys)
; rhs_ty <- expTypeToType rhs_ty
; return (MG { mg_alts = L l []
, mg_ext = MatchGroupTc pat_tys rhs_ty origin
@@ -232,15 +234,23 @@ tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches
= do { umatches <- mapM (tcCollectingUsage . tcMatch ctxt pat_tys rhs_ty) matches
; let (usages,matches') = unzip umatches
; tcEmitBindingUsage $ supUEs usages
- ; pat_tys <- mapM readScaledExpType pat_tys
+ ; pat_tys <- mapM readScaledExpType (filter_out_forall_pat_tys pat_tys)
; rhs_ty <- readExpType rhs_ty
+ ; traceTc "tcMatches" (ppr matches' $$ ppr pat_tys $$ ppr rhs_ty)
; return (MG { mg_alts = L l matches'
, mg_ext = MatchGroupTc pat_tys rhs_ty origin
}) }
+ where
+ -- We filter out foralls because we have no use for them in HsToCore.
+ filter_out_forall_pat_tys :: [ExpPatType] -> [Scaled ExpSigmaTypeFRR]
+ filter_out_forall_pat_tys = mapMaybe match_fun_pat_ty
+ where
+ match_fun_pat_ty (ExpFunPatTy t) = Just t
+ match_fun_pat_ty ExpForAllPatTy{} = Nothing
-------------
tcMatch :: (AnnoBody body) => TcMatchCtxt body
- -> [Scaled ExpSigmaType] -- Expected pattern types
+ -> [ExpPatType] -- Expected pattern types
-> ExpRhoType -- Expected result-type of the Match.
-> LMatch GhcRn (LocatedA (body GhcRn))
-> TcM (LMatch GhcTc (LocatedA (body GhcTc)))
@@ -254,7 +264,8 @@ tcMatch ctxt pat_tys rhs_ty match
do { (pats', grhss') <- tcPats (mc_what ctxt) pats pat_tys $
tcGRHSs ctxt grhss rhs_ty
; return (Match { m_ext = noAnn
- , m_ctxt = mc_what ctxt, m_pats = pats'
+ , m_ctxt = mc_what ctxt
+ , m_pats = filter_out_type_pats pats'
, m_grhss = grhss' }) }
-- For (\x -> e), tcExpr has already said "In the expression \x->e"
@@ -264,6 +275,14 @@ tcMatch ctxt pat_tys rhs_ty match
LambdaExpr -> thing_inside
_ -> addErrCtxt (pprMatchInCtxt match) thing_inside
+ -- We filter out type patterns because we have no use for them in HsToCore.
+ -- Type variable bindings have already been converted to HsWrappers.
+ filter_out_type_pats :: [LPat GhcTc] -> [LPat GhcTc]
+ filter_out_type_pats = filterByList (map is_fun_pat_ty pat_tys)
+ where
+ is_fun_pat_ty ExpFunPatTy{} = True
+ is_fun_pat_ty ExpForAllPatTy{} = False
+
-------------
tcGRHSs :: AnnoBody body
=> TcMatchCtxt body -> GRHSs GhcRn (LocatedA (body GhcRn)) -> ExpRhoType
diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs
index 79495ff3544aa30013160ebd1cfb6c634dcfcd61..ab2f6518259c4f5156596958174d5545b48c5788 100644
--- a/compiler/GHC/Tc/Gen/Pat.hs
+++ b/compiler/GHC/Tc/Gen/Pat.hs
@@ -104,7 +104,7 @@ tcLetPat sig_fn no_gen pat pat_ty thing_inside
-----------------
tcPats :: HsMatchContext GhcTc
-> [LPat GhcRn] -- ^ atterns
- -> [Scaled ExpSigmaTypeFRR] -- ^ types of the patterns
+ -> [ExpPatType] -- ^ types of the patterns
-> TcM a -- ^ checker for the body
-> TcM ([LPat GhcTc], a)
@@ -120,7 +120,7 @@ tcPats :: HsMatchContext GhcTc
-- 4. Check that no existentials escape
tcPats ctxt pats pat_tys thing_inside
- = tc_lpats pat_tys penv pats thing_inside
+ = tc_tt_lpats pat_tys penv pats thing_inside
where
penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin }
@@ -350,6 +350,14 @@ tc_lpat pat_ty penv (L span pat) thing_inside
thing_inside
; return (L span pat', res) }
+tc_tt_lpat :: ExpPatType
+ -> Checker (LPat GhcRn) (LPat GhcTc)
+tc_tt_lpat pat_ty penv (L span pat) thing_inside
+ = setSrcSpanA span $
+ do { (pat', res) <- maybeWrapPatCtxt pat (tc_tt_pat pat_ty penv pat)
+ thing_inside
+ ; return (L span pat', res) }
+
tc_lpats :: [Scaled ExpSigmaTypeFRR]
-> Checker [LPat GhcRn] [LPat GhcTc]
tc_lpats tys penv pats
@@ -358,11 +366,39 @@ tc_lpats tys penv pats
penv
(zipEqual "tc_lpats" pats tys)
+tc_tt_lpats :: [ExpPatType] -> Checker [LPat GhcRn] [LPat GhcTc]
+tc_tt_lpats tys penv pats
+ = assertPpr (equalLength pats tys) (ppr pats $$ ppr tys) $
+ tcMultiple (\ penv' (p,t) -> tc_tt_lpat t penv' p)
+ penv
+ (zipEqual "tc_tt_lpats" pats tys)
+
--------------------
-- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
checkManyPattern :: Scaled a -> TcM HsWrapper
checkManyPattern pat_ty = tcSubMult NonLinearPatternOrigin ManyTy (scaledMult pat_ty)
+tc_tt_pat
+ :: ExpPatType
+ -- ^ Fully refined result type
+ -> Checker (Pat GhcRn) (Pat GhcTc)
+ -- ^ Translated pattern
+tc_tt_pat pat_ty penv (ParPat x lpar pat rpar) thing_inside = do
+ { (pat', res) <- tc_tt_lpat pat_ty penv pat thing_inside
+ ; return (ParPat x lpar pat' rpar, res) }
+tc_tt_pat (ExpFunPatTy pat_ty) penv pat thing_inside = tc_pat pat_ty penv pat thing_inside
+tc_tt_pat (ExpForAllPatTy tv) penv pat thing_inside = tc_forall_pat penv (pat, tv) thing_inside
+
+tc_forall_pat :: Checker (Pat GhcRn, TcTyVar) (Pat GhcTc)
+tc_forall_pat _ (EmbTyPat _ toktype tp, tv) thing_inside
+ = do { (sig_wcs, sig_ibs, arg_ty) <- tcHsTyPat tp (varType tv)
+ ; _ <- unifyType Nothing arg_ty (mkTyVarTy tv)
+ ; result <- tcExtendNameTyVarEnv sig_wcs $
+ tcExtendNameTyVarEnv sig_ibs $
+ thing_inside
+ ; return (EmbTyPat arg_ty toktype tp, result) }
+tc_forall_pat _ (pat, _) _ = failWith $ TcRnIllformedTypePattern pat
+
tc_pat :: Scaled ExpSigmaTypeFRR
-- ^ Fully refined result type
-> Checker (Pat GhcRn) (Pat GhcTc)
@@ -702,6 +738,8 @@ AST is used for the subtraction operation.
SplicePat (HsUntypedSpliceNested _) _ -> panic "tc_pat: nested splice in splice pat"
+ EmbTyPat _ _ _ -> failWith TcRnIllegalTypePattern
+
XPat (HsPatExpanded lpat rpat) -> do
{ (rpat', res) <- tc_pat pat_ty penv rpat thing_inside
; return (XPat $ ExpansionPat lpat rpat', res) }
diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs b/compiler/GHC/Tc/TyCl/PatSyn.hs
index c34e9159cb588de80c8a765cd96546848e474bc9..71e4b5f319bb28e2cc4952aa162ba686f5a27a6f 100644
--- a/compiler/GHC/Tc/TyCl/PatSyn.hs
+++ b/compiler/GHC/Tc/TyCl/PatSyn.hs
@@ -1073,6 +1073,10 @@ tcPatToExpr args pat = go pat
| otherwise = return $ HsOverLit noAnn n
go1 (SplicePat (HsUntypedSpliceTop _ pat) _) = go1 pat
go1 (SplicePat (HsUntypedSpliceNested _) _) = panic "tcPatToExpr: invalid nested splice"
+ go1 (EmbTyPat _ toktype tp) = return $ HsEmbTy noExtField toktype (hstp_to_hswc tp)
+ where hstp_to_hswc :: HsTyPat GhcRn -> LHsWcType GhcRn
+ hstp_to_hswc (HsTP { hstp_ext = HsTPRn { hstp_nwcs = wcs }, hstp_body = hs_ty })
+ = HsWC { hswc_ext = wcs, hswc_body = hs_ty }
go1 (XPat (HsPatExpanded _ pat))= go1 pat
-- See Note [Invertible view patterns]
diff --git a/compiler/GHC/Tc/Types/Evidence.hs b/compiler/GHC/Tc/Types/Evidence.hs
index 81266433f117900063e2bcc63d904a6c048b0f56..e9937d0f953af5532be1f33c1703ab36aa0e0b78 100644
--- a/compiler/GHC/Tc/Types/Evidence.hs
+++ b/compiler/GHC/Tc/Types/Evidence.hs
@@ -7,7 +7,7 @@ module GHC.Tc.Types.Evidence (
-- * HsWrapper
HsWrapper(..),
- (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams,
+ (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpVisTyLam,
mkWpEvLams, mkWpLet, mkWpFun, mkWpCastN, mkWpCastR, mkWpEta,
collectHsWrapBinders,
idHsWrapper, isIdHsWrapper,
@@ -258,6 +258,21 @@ mkWpEvVarApps vs = mk_co_app_fn WpEvApp (map (EvExpr . evId) vs)
mkWpTyLams :: [TyVar] -> HsWrapper
mkWpTyLams ids = mk_co_lam_fn WpTyLam ids
+-- Construct a type lambda and cast its type
+-- from `forall tv. res` to `forall tv -> res`.
+--
+-- (\ @tv -> e )
+-- `cast` (forall (tv[spec]~[req] :: <*>_N). <res>_R -- ForAllCo is the evidence that...
+-- :: (forall tv. res) ~R# (forall tv -> res)) -- invisible and visible foralls are representationally equal
+--
+mkWpVisTyLam :: TyVar -> Type -> HsWrapper
+mkWpVisTyLam tv res =
+ WpCast (mkForAllCo tv coreTyLamForAllTyFlag Required kind_co body_co)
+ <.> WpTyLam tv
+ where
+ kind_co = mkNomReflCo (varType tv)
+ body_co = mkRepReflCo res
+
mkWpEvLams :: [Var] -> HsWrapper
mkWpEvLams ids = mk_co_lam_fn WpEvLam ids
diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index 10b0c795a815d9dd4a5a64e5102428cdb7471cfd..686b384d061224a955a59aa4341060485addc830 100644
--- a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ -739,6 +739,7 @@ exprCtOrigin (HsTypedSplice {}) = Shouldn'tHappenOrigin "TH typed splice"
exprCtOrigin (HsUntypedSplice {}) = Shouldn'tHappenOrigin "TH untyped splice"
exprCtOrigin (HsProc {}) = Shouldn'tHappenOrigin "proc"
exprCtOrigin (HsStatic {}) = Shouldn'tHappenOrigin "static expression"
+exprCtOrigin (HsEmbTy {}) = Shouldn'tHappenOrigin "type expression"
exprCtOrigin (XExpr (HsExpanded a _)) = exprCtOrigin a
-- | Extract a suitable CtOrigin from a MatchGroup
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index 5dedeef9a3f5251b0ab463d2356072da183b2e0c..b4d98b2ab0d297044a281aef2bde62a8868d5dd3 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -33,6 +33,8 @@ module GHC.Tc.Utils.TcType (
mkCheckExpType,
checkingExpType_maybe, checkingExpType,
+ ExpPatType(..),
+
SyntaxOpType(..), synKnownType, mkSynFunTys,
--------------------------------
@@ -458,6 +460,15 @@ checkingExpType :: String -> ExpType -> TcType
checkingExpType _ (Check ty) = ty
checkingExpType err et = pprPanic "checkingExpType" (text err $$ ppr et)
+-- Expected type of a pattern in a lambda or a function left-hand side.
+data ExpPatType =
+ ExpFunPatTy (Scaled ExpSigmaTypeFRR) -- the type A of a function A -> B
+ | ExpForAllPatTy TcTyVar -- the binder (a::A) of forall (a::A) -> B
+
+instance Outputable ExpPatType where
+ ppr (ExpFunPatTy t) = ppr t
+ ppr (ExpForAllPatTy tv) = text "forall" <+> ppr tv
+
{- *********************************************************************
* *
SyntaxOpType
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index 5c31049cabcb04f8c88366636a61df932ad18aa5..c591b1be49c9d7fd8f76a67b19a11fa3c2a89222 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -183,7 +183,7 @@ matchActualFunTySigma herald mb_thing err_info fun_ty
------------
mk_ctxt :: TcType -> TidyEnv -> ZonkM (TidyEnv, SDoc)
- mk_ctxt res_ty env = mkFunTysMsg env herald (reverse arg_tys_so_far)
+ mk_ctxt res_ty env = mkFunTysMsg env herald [Anon t visArgTypeLike | t <- reverse arg_tys_so_far]
res_ty n_val_args_in_call
(n_val_args_in_call, arg_tys_so_far) = err_info
@@ -376,7 +376,7 @@ matchExpectedFunTys :: forall a.
-> UserTypeCtxt
-> Arity
-> ExpRhoType -- Skolemised
- -> ([Scaled ExpSigmaTypeFRR] -> ExpRhoType -> TcM a)
+ -> ([ExpPatType] -> ExpRhoType -> TcM a)
-> TcM (HsWrapper, a)
-- If matchExpectedFunTys n ty = (wrap, _)
-- then wrap : (t1 -> ... -> tn -> ty_r) ~> ty,
@@ -386,11 +386,11 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside
Check ty -> go [] arity ty
_ -> defer [] arity orig_ty
where
- -- Skolemise any foralls /before/ the zero-arg case
+ -- Skolemise any /invisible/ foralls /before/ the zero-arg case
-- so that we guarantee to return a rho-type
go acc_arg_tys n ty
- | (tvs, theta, _) <- tcSplitSigmaTy ty
- , not (null tvs && null theta)
+ | (tvs, theta, _) <- tcSplitSigmaTy ty -- Invisible binders only!
+ , not (null tvs && null theta) -- Visible ones handled below
= do { (wrap_gen, (wrap_res, result)) <- tcTopSkolemise ctx ty $ \ty' ->
go acc_arg_tys n ty'
; return (wrap_gen <.> wrap_res, result) }
@@ -404,11 +404,22 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside
go acc_arg_tys n ty
| Just ty' <- coreView ty = go acc_arg_tys n ty'
+ -- Decompose /visible/ (forall a -> blah), to give an ExpForAllPat
+ -- NB: invisible binders are handled by tcSplitSigmaTy/tcTopSkolemise above
+ -- NB: visible foralls "count" for the Arity argument; they correspond
+ -- to syntactically visible patterns in the source program
+ -- See Note [Visible type application and abstraction] in GHC.Tc.Gen.App
+ go acc_arg_tys n ty
+ | Just (Bndr tv vis, ty') <- splitForAllForAllTyBinder_maybe ty
+ , Required <- vis
+ = let init_subst = mkEmptySubst (mkInScopeSet (tyCoVarsOfType ty))
+ in goVdq init_subst acc_arg_tys n ty tv ty'
+
go acc_arg_tys n (FunTy { ft_af = af, ft_mult = mult, ft_arg = arg_ty, ft_res = res_ty })
= assert (isVisibleFunArg af) $
do { let arg_pos = 1 + length acc_arg_tys -- for error messages only
; (arg_co, arg_ty) <- hasFixedRuntimeRep (FRRExpectedFunTy herald arg_pos) arg_ty
- ; (wrap_res, result) <- go ((Scaled mult $ mkCheckExpType arg_ty) : acc_arg_tys)
+ ; (wrap_res, result) <- go ((ExpFunPatTy $ Scaled mult $ mkCheckExpType arg_ty) : acc_arg_tys)
(n-1) res_ty
; let wrap_arg = mkWpCastN arg_co
fun_wrap = mkWpFun wrap_arg wrap_res (Scaled mult arg_ty) res_ty
@@ -439,13 +450,24 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside
go acc_arg_tys n ty = addErrCtxtM (mk_ctxt acc_arg_tys ty) $
defer acc_arg_tys n (mkCheckExpType ty)
+ goVdq subst acc_arg_tys n expected_ty tv ty =
+ do { rec { (subst', [tv']) <- tcInstSkolTyVarsX skol_info subst [tv]
+ ; let tv_prs = [(tyVarName tv, tv')]
+ ; skol_info <- mkSkolemInfo (SigSkol ctx expected_ty tv_prs) }
+ ; let ty' = substTy subst' ty
+ ; (ev_binds, (wrap_res, result)) <-
+ checkConstraints (getSkolemInfo skol_info) [tv'] [] $
+ go (ExpForAllPatTy tv' : acc_arg_tys) (n - 1) ty'
+ ; let wrap_gen = mkWpVisTyLam tv' ty' <.> mkWpLet ev_binds
+ ; return (wrap_gen <.> wrap_res, result) }
+
------------
- defer :: [Scaled ExpSigmaTypeFRR] -> Arity -> ExpRhoType -> TcM (HsWrapper, a)
+ defer :: [ExpPatType] -> Arity -> ExpRhoType -> TcM (HsWrapper, a)
defer acc_arg_tys n fun_ty
= do { let last_acc_arg_pos = length acc_arg_tys
; more_arg_tys <- mapM new_exp_arg_ty [last_acc_arg_pos + 1 .. last_acc_arg_pos + n]
; res_ty <- newInferExpType
- ; result <- thing_inside (reverse acc_arg_tys ++ more_arg_tys) res_ty
+ ; result <- thing_inside (reverse acc_arg_tys ++ map ExpFunPatTy more_arg_tys) res_ty
; more_arg_tys <- mapM (\(Scaled m t) -> Scaled m <$> readExpType t) more_arg_tys
; res_ty <- readExpType res_ty
; let unif_fun_ty = mkScaledFunTys more_arg_tys res_ty
@@ -459,30 +481,40 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside
<*> newInferExpTypeFRR (FRRExpectedFunTy herald arg_pos)
------------
- mk_ctxt :: [Scaled ExpSigmaTypeFRR] -> TcType -> TidyEnv -> ZonkM (TidyEnv, SDoc)
+ mk_ctxt :: [ExpPatType] -> TcType -> TidyEnv -> ZonkM (TidyEnv, SDoc)
mk_ctxt arg_tys res_ty env
= mkFunTysMsg env herald arg_tys' res_ty arity
where
- arg_tys' = map (\(Scaled u v) -> Scaled u (checkingExpType "matchExpectedFunTys" v)) $
- reverse arg_tys
+ arg_tys' = map prepare_arg_ty (reverse arg_tys)
+ prepare_arg_ty (ExpFunPatTy (Scaled u v)) = Anon (Scaled u (checkingExpType "matchExpectedFunTys" v)) visArgTypeLike
+ prepare_arg_ty (ExpForAllPatTy tv) = Named (Bndr tv Required)
-- this is safe b/c we're called from "go"
mkFunTysMsg :: TidyEnv
-> ExpectedFunTyOrigin
- -> [Scaled TcType] -> TcType -> Arity
+ -> [PiTyBinder] -- only visible quantifiers `t1 -> t2` and `forall (x :: t1) -> t2`
+ -> TcType
+ -> Arity
-> ZonkM (TidyEnv, SDoc)
mkFunTysMsg env herald arg_tys res_ty n_val_args_in_call
- = do { (env', fun_rho) <- zonkTidyTcType env $
- mkScaledFunTys arg_tys res_ty
+ = do { (env', fun_ty) <- zonkTidyTcType env $
+ mkPiTys arg_tys res_ty
+
+ ; let (all_arg_tys, _) =
+ -- No invisible quantifiers here (neither `ctx => t` nor `forall x. t`)
+ -- because `mkFunTysMsg` never gets those as input in the first place,
+ -- so there is no need to filter them out.
+ splitPiTys fun_ty
- ; let (all_arg_tys, _) = splitFunTys fun_rho
+ -- `all_arg_tys` contains visible quantifiers only, so their number matches
+ -- the number of arguments that the user needs to pass to the function.
n_fun_args = length all_arg_tys
msg | n_val_args_in_call <= n_fun_args -- Enough args, in the end
= text "In the result of a function call"
| otherwise
= hang (full_herald <> comma)
- 2 (sep [ text "but its type" <+> quotes (pprType fun_rho)
+ 2 (sep [ text "but its type" <+> quotes (pprType fun_ty)
, if n_fun_args == 0 then text "has none"
else text "has only" <+> speakN n_fun_args])
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index 9f5846ba85b24b174f790f95153ad8af9ff89d88..394de6c8e0af3a25ac048e074b98052af07e2432 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -993,7 +993,8 @@ checkConstraintsOK ve theta ty
checkVdqOK :: ValidityEnv -> [TyVarBinder] -> Type -> TcM ()
checkVdqOK ve tvbs ty = do
- checkTcM (vdqAllowed ctxt || no_vdq)
+ required_type_arguments <- xoptM LangExt.RequiredTypeArguments
+ checkTcM (required_type_arguments || vdqAllowed ctxt || no_vdq)
(env, TcRnVDQInTermType (Just (tidyType env ty)))
where
no_vdq = all (isInvisibleForAllTyFlag . binderFlag) tvbs
diff --git a/compiler/GHC/Tc/Zonk/Type.hs b/compiler/GHC/Tc/Zonk/Type.hs
index 58069d1b05f515995b00ac1c38116339ac840985..7d5d15396e28cc3d369a25f8b3e12b81a2765bba 100644
--- a/compiler/GHC/Tc/Zonk/Type.hs
+++ b/compiler/GHC/Tc/Zonk/Type.hs
@@ -1064,6 +1064,8 @@ zonkExpr (HsStatic (fvs, ty) expr)
= do new_ty <- zonkTcTypeToTypeX ty
HsStatic (fvs, new_ty) <$> zonkLExpr expr
+zonkExpr (HsEmbTy x _ _) = dataConCantHappen x
+
zonkExpr (XExpr (WrapExpr (HsWrap co_fn expr)))
= runZonkBndrT (zonkCoFn co_fn) $ \ new_co_fn ->
do new_expr <- zonkExpr expr
@@ -1577,6 +1579,10 @@ zonk_pat (NPlusKPat ty (L loc n) (L l lit1) lit2 e1 e2)
; n' <- zonkIdBndrX n
; return (NPlusKPat ty' (L loc n') (L l lit1') lit2' e1' e2') }
+zonk_pat (EmbTyPat ty toktype tp)
+ = do { ty' <- noBinders $ zonkTcTypeToTypeX ty
+ ; return (EmbTyPat ty' toktype tp) }
+
zonk_pat (XPat ext) = case ext of
{ ExpansionPat orig pat->
do { pat' <- zonk_pat pat
diff --git a/compiler/GHC/ThToHs.hs b/compiler/GHC/ThToHs.hs
index 4b35c92cba92e487baa449fdeca5d6607d74358e..e884c5b2cec073ec78a3b11ca2f2992291d7a70b 100644
--- a/compiler/GHC/ThToHs.hs
+++ b/compiler/GHC/ThToHs.hs
@@ -1164,6 +1164,8 @@ cvtl e = wrapLA (cvt e)
; return $ HsTypedSplice (noAnn, noAnn) e' }
cvt (TypedBracketE e) = do { e' <- cvtl e
; return $ HsTypedBracket noAnn e' }
+ cvt (TypeE t) = do { t' <- cvtType t
+ ; return $ HsEmbTy noExtField noHsTok (mkHsWildCardBndrs t') }
{- | #16895 Ensure an infix expression's operator is a variable/constructor.
Consider this example:
@@ -1480,6 +1482,8 @@ cvtp (SigP p t) = do { p' <- cvtPat p; t' <- cvtType t
; return $ SigPat noAnn p' (mkHsPatSigType noAnn t') }
cvtp (ViewP e p) = do { e' <- cvtl e; p' <- cvtPat p
; return $ ViewPat noAnn e' p'}
+cvtp (TypeP t) = do { t' <- cvtType t
+ ; return $ EmbTyPat noExtField noHsTok (mkHsTyPat noAnn t') }
cvtPatFld :: (TH.Name, TH.Pat) -> CvtM (LHsRecField GhcPs (LPat GhcPs))
cvtPatFld (s,p)
diff --git a/compiler/GHC/Types/Error/Codes.hs b/compiler/GHC/Types/Error/Codes.hs
index 8be60f2c85d8f935c3107e49c1b952297b61af95..90a918c8f0206e4882078cabafe1e30647694a53 100644
--- a/compiler/GHC/Types/Error/Codes.hs
+++ b/compiler/GHC/Types/Error/Codes.hs
@@ -624,6 +624,10 @@ type family GhcDiagnosticCode c = n | n -> c where
GhcDiagnosticCode "HasConstructorContext" = 17440
GhcDiagnosticCode "HasExistentialTyVar" = 07525
GhcDiagnosticCode "HasStrictnessAnnotation" = 04049
+ GhcDiagnosticCode "TcRnIllformedTypePattern" = 88754
+ GhcDiagnosticCode "TcRnIllegalTypePattern" = 70206
+ GhcDiagnosticCode "TcRnIllformedTypeArgument" = 29092
+ GhcDiagnosticCode "TcRnIllegalTypeExpr" = 35499
-- TcRnBadRecordUpdate
GhcDiagnosticCode "NoConstructorHasAllFields" = 14392
diff --git a/compiler/GHC/Types/Var.hs b/compiler/GHC/Types/Var.hs
index bbc5454c9fc009396d8643bfb26acac080ee804f..ec50a364af5cec8963c235c0d054255598a64307 100644
--- a/compiler/GHC/Types/Var.hs
+++ b/compiler/GHC/Types/Var.hs
@@ -920,8 +920,7 @@ This table summarises the visibility rules:
| tvis = Inferred: f :: forall {a}. type Arg not allowed: f
f :: forall {co}. type Arg not allowed: f
| tvis = Specified: f :: forall a. type Arg optional: f or f @Int
-| tvis = Required: T :: forall k -> type Arg required: T *
-| This last form is illegal in terms: See Note [No Required PiTyBinder in terms]
+| tvis = Required: f :: forall k -> type Arg required: f (type Int)
|
| Bndr k cvis :: TyConBinder, in the TyConBinders of a TyCon
| cvis :: TyConBndrVis
@@ -952,22 +951,28 @@ This table summarises the visibility rules:
f3 :: forall a. a -> a; f3 x = x
So f3 gets the type f3 :: forall a. a -> a, with 'a' Specified
+* Required. Function defn, with signature (explicit forall):
+ f4 :: forall a -> a -> a; f4 (type _) x = x
+ So f4 gets the type f4 :: forall a -> a -> a, with 'a' Required
+ This is the experimental RequiredTypeArguments extension,
+ see GHC Proposal #281 "Visible forall in types of terms"
+
* Inferred. Function defn, with signature (explicit forall), marked as inferred:
- f4 :: forall {a}. a -> a; f4 x = x
- So f4 gets the type f4 :: forall {a}. a -> a, with 'a' Inferred
+ f5 :: forall {a}. a -> a; f5 x = x
+ So f5 gets the type f5 :: forall {a}. a -> a, with 'a' Inferred
It's Inferred because the user marked it as such, even though it does appear
- in the user-written signature for f4
+ in the user-written signature for f5
* Inferred/Specified. Function signature with inferred kind polymorphism.
- f5 :: a b -> Int
- So 'f5' gets the type f5 :: forall {k} (a:k->*) (b:k). a b -> Int
+ f6 :: a b -> Int
+ So 'f6' gets the type f6 :: forall {k} (a :: k -> Type) (b :: k). a b -> Int
Here 'k' is Inferred (it's not mentioned in the type),
but 'a' and 'b' are Specified.
* Specified. Function signature with explicit kind polymorphism
- f6 :: a (b :: k) -> Int
+ f7 :: a (b :: k) -> Int
This time 'k' is Specified, because it is mentioned explicitly,
- so we get f6 :: forall (k:*) (a:k->*) (b:k). a b -> Int
+ so we get f7 :: forall (k :: Type) (a :: k -> Type) (b :: k). a b -> Int
* Similarly pattern synonyms:
Inferred - from inferred types (e.g. no pattern type signature)
@@ -1027,7 +1032,7 @@ See also Note [Required, Specified, and Inferred for types] in GHC.Tc.TyCl
const :: forall a b. a -> b -> a
Inferred: like Specified, but every binder is written in braces:
- f :: forall {k} (a:k). S k a -> Int
+ f :: forall {k} (a :: k). S k a -> Int
Required: binders are put between `forall` and `->`:
T :: forall k -> *
@@ -1039,19 +1044,6 @@ See also Note [Required, Specified, and Inferred for types] in GHC.Tc.TyCl
* Inferred variables correspond to "generalized" variables from the
Visible Type Applications paper (ESOP'16).
-
-Note [No Required PiTyBinder in terms]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We don't allow Required foralls for term variables, including pattern
-synonyms and data constructors. Why? Because then an application
-would need a /compulsory/ type argument (possibly without an "@"?),
-thus (f Int); and we don't have concrete syntax for that.
-
-We could change this decision, but Required, Named PiTyBinders are rare
-anyway. (Most are Anons.)
-
-However the type of a term can (just about) have a required quantifier;
-see Note [Required quantifiers in the type of a term] in GHC.Tc.Gen.Expr.
-}
diff --git a/compiler/Language/Haskell/Syntax/Expr.hs b/compiler/Language/Haskell/Syntax/Expr.hs
index c79b54518a4b1e8e2a715765e9c8544590e8c8d2..8707d300384dd8ba125dfff660bf4c7b261205f7 100644
--- a/compiler/Language/Haskell/Syntax/Expr.hs
+++ b/compiler/Language/Haskell/Syntax/Expr.hs
@@ -579,6 +579,12 @@ data HsExpr p
-- Expressions annotated with pragmas, written as {-# ... #-}
| HsPragE (XPragE p) (HsPragE p) (LHsExpr p)
+ -- Embed the syntax of types into expressions.
+ -- Used with RequiredTypeArguments, e.g. fn (type (Int -> Bool))
+ | HsEmbTy (XEmbTy p)
+ !(LHsToken "type" p)
+ (LHsWcType (NoGhcTc p))
+
| XExpr !(XXExpr p)
-- Note [Trees That Grow] in Language.Haskell.Syntax.Extension for the
-- general idea, and Note [Rebindable syntax and HsExpansion] in GHC.Hs.Expr
diff --git a/compiler/Language/Haskell/Syntax/Extension.hs b/compiler/Language/Haskell/Syntax/Extension.hs
index 4069bb8cf00bd8f52e5ae808328c81aa88098214..82edc341f2c4ddc3974782731b418a14dcef9491 100644
--- a/compiler/Language/Haskell/Syntax/Extension.hs
+++ b/compiler/Language/Haskell/Syntax/Extension.hs
@@ -447,6 +447,7 @@ type family XStatic x
type family XTick x
type family XBinTick x
type family XPragE x
+type family XEmbTy x
type family XXExpr x
-- -------------------------------------
@@ -606,6 +607,7 @@ type family XLitPat x
type family XNPat x
type family XNPlusKPat x
type family XSigPat x
+type family XEmbTyPat x
type family XCoPat x
type family XXPat x
type family XHsFieldBind x
diff --git a/compiler/Language/Haskell/Syntax/Pat.hs b/compiler/Language/Haskell/Syntax/Pat.hs
index 8ff31fd8dbebee850b44ca4f8ea38cacb3a6f40f..4a4230abb176dfe1e11be46ae2b0466d891e44c9 100644
--- a/compiler/Language/Haskell/Syntax/Pat.hs
+++ b/compiler/Language/Haskell/Syntax/Pat.hs
@@ -219,6 +219,12 @@ data Pat p
-- ^ Pattern with a type signature
+ -- Embed the syntax of types into patterns.
+ -- Used with RequiredTypeArguments, e.g. fn (type t) = rhs
+ | EmbTyPat (XEmbTyPat p)
+ !(LHsToken "type" p)
+ (HsTyPat (NoGhcTc p))
+
-- Extension point; see Note [Trees That Grow] in Language.Haskell.Syntax.Extension
| XPat
!(XXPat p)
diff --git a/docs/users_guide/9.10.1-notes.rst b/docs/users_guide/9.10.1-notes.rst
index d33c6565a997dba1660b5b409f14ce0311612bb9..57fbd5177bd5602b4f79c0f21039382e5b9136dd 100644
--- a/docs/users_guide/9.10.1-notes.rst
+++ b/docs/users_guide/9.10.1-notes.rst
@@ -6,6 +6,18 @@ Version 9.10.1
Language
~~~~~~~~
+- Part 1 of GHC Proposal `#281
+ <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst>`_
+ "Visible forall in types of terms" has been implemented.
+ The following code is now accepted by GHC::
+
+ idv :: forall a -> a -> a
+ idv (type a) (x :: a) = x
+
+ x = idv (type Int) 42
+
+ This feature is guarded behind :extension:`RequiredTypeArguments` and :extension:`ExplicitNamespaces`.
+
Compiler
~~~~~~~~
@@ -30,6 +42,10 @@ Runtime system
``template-haskell`` library
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+- Extend ``Pat`` with ``TypeP`` and ``Exp`` with ``TypeE``,
+ introduce functions ``typeP`` and ``typeE`` (Template Haskell support for GHC Proposal `#281
+ <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst>`_).
+
Included libraries
~~~~~~~~~~~~~~~~~~
diff --git a/docs/users_guide/exts/explicit_namespaces.rst b/docs/users_guide/exts/explicit_namespaces.rst
index 64058f25de69b4f1ad5762ac1a815f8df30d047b..04c6ba099c46b5ca572a7710d7532ee46d02d777 100644
--- a/docs/users_guide/exts/explicit_namespaces.rst
+++ b/docs/users_guide/exts/explicit_namespaces.rst
@@ -11,7 +11,7 @@ Explicit namespaces in import/export
:implied by: :extension:`TypeOperators`, :extension:`TypeFamilies`
:since: 7.6.1
- Enable use of explicit namespaces in module export lists.
+ Enable use of explicit namespaces in module export lists, patterns, and expressions.
In an import or export list, such as ::
@@ -41,3 +41,11 @@ In addition, with :extension:`PatternSynonyms` you can prefix the name of a
data constructor in an import or export list with the keyword
``pattern``, to allow the import or export of a data constructor without
its parent type constructor (see :ref:`patsyn-impexp`).
+
+Furthermore, :extension:`ExplicitNamespaces` permits the use of the ``type``
+keyword in patterns and expressions::
+
+ f (type t) x = ... -- in a pattern
+ r = f (type Integer) 10 -- in an expression
+
+This is used in conjunction with :extension:`RequiredTypeArguments`.
\ No newline at end of file
diff --git a/docs/users_guide/exts/required_type_arguments.rst b/docs/users_guide/exts/required_type_arguments.rst
new file mode 100644
index 0000000000000000000000000000000000000000..7876b841322601e2182b953a5ebe21ba98a2613f
--- /dev/null
+++ b/docs/users_guide/exts/required_type_arguments.rst
@@ -0,0 +1,113 @@
+Required type arguments
+=======================
+
+.. extension:: RequiredTypeArguments
+ :shortdesc: Enable required type arguments in terms.
+
+ :since: 9.10.1
+ :status: Experimental
+
+ Allow visible dependent quantification ``forall x ->`` in types of terms.
+
+**This feature is only partially implemented in GHC.** In this section we
+describe the implemented subset, while the full specification can be found in
+`GHC Proposal #281 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst>`__.
+
+The :extension:`RequiredTypeArguments` extension enables the use of visible
+dependent quantification in types of terms::
+
+ id :: forall a. a -> a -- invisible dependent quantification
+ id_vdq :: forall a -> a -> a -- visible dependent quantification
+
+Note that the arrow in ``forall a ->`` is part of the syntax and not a function
+arrow, just like the dot in ``forall a.`` is not a type operator. The essence of
+a ``forall`` is the same regardless of whether it is followed by a dot or an
+arrow: it introduces a type variable. But the way we bind and specify this type
+variable at the term level differs.
+
+When we define ``id``, we can use a lambda to bind a variable that stands for
+the function argument::
+
+ -- For reference: id :: forall a. a -> a
+ id = \x -> x
+
+At the same time, there is no mention of ``a`` in this definition at all. It is
+bound by the compiler behind the scenes, and that is why we call the ordinary
+``forall a.`` an *invisible* quantifier. Compare that to ``forall a ->``, which
+is considered *visible*::
+
+ -- For reference: id_vdq :: forall a -> a -> a
+ id_vdq = \(type t) x -> x
+
+This time we have two binders in the lambda:
+* ``type t``, corresponding to ``forall a ->`` in the signature
+* ``x``, corresponding to ``a ->`` in the signature
+
+And of course, now we also have the option of using the bound ``t`` in a
+subsequent pattern, as well as on the right-hand side of the lambda::
+
+ -- For reference: id_vdq :: forall a -> a -> a
+ id_vdq = \(type t) (x :: t) -> x :: t
+ -- ↑ ↑ ↑
+ -- bound used used
+
+At use sites, we also instantiate this type variable explicitly::
+
+ n = id_vdq (type Integer) 42
+ s = id_vdq (type String) "Hello"
+
+Relation to :extension:`TypeApplications`
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+:extension:`RequiredTypeArguments` are similar to :extension:`TypeApplications`
+in that we pass a type to a function as an explicit argument. The difference is
+that type applications are optional: it is up to the caller whether to write
+``id @Bool True`` or ``id True``. By default, the compiler infers that the
+type variable is instantiated to ``Bool``. The existence of a type argument is
+not reflected syntactically in the expression, it is invisible unless we use a
+*visibility override*, i.e. ``@``.
+
+Required type arguments are compulsory. They must appear syntactically at call
+sites::
+
+ x1 = id_vdq (type Bool) True -- OK
+ x2 = id_vdq True -- not OK
+
+You may use an underscore to infer a required type argument::
+
+ x3 = id_vdq (type _) True -- OK
+
+That is, it is mostly a matter of syntax whether to use ``forall a.`` with type
+applications or ``forall a ->``. One advantage of required type arguments is that
+they are never ambiguous. Consider the type of ``Foreign.Storable.sizeOf``::
+
+ sizeOf :: forall a. Storable a => a -> Int
+
+The value parameter is not actually used, its only purpose is to drive type
+inference. At call sites, one might write ``sizeOf (undefined :: Bool)`` or
+``sizeOf @Bool undefined``. Either way, the ``undefined`` is entirely
+superfluous and exists only to avoid an ambiguous type variable.
+
+With :extension:`RequiredTypeArguments`, we can imagine a slightly different API::
+
+ sizeOf :: forall a -> Storable a => Int
+
+If ``sizeOf`` had this type, we could write ``sizeOf (type Bool)`` without
+passing a dummy value.
+
+Relation to :extension:`ExplicitNamespaces`
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The ``type`` keyword that we used in the examples is not actually part of
+:extension:`RequiredTypeArguments`. It is guarded behind
+:extension:`ExplicitNamespaces`. As described in the proposal, required type
+arguments can be passed without a syntactic marker, making them syntactically
+indistinguishble from ordinary function arguments::
+
+ n = id_vdq Integer 42
+
+In this example we pass ``Integer`` as opposed to ``(type Integer)``.
+**This is not currently implemented**, but it demonstrates how
+:extension:`RequiredTypeArguments` is not tied to the ``type`` syntax.
+For this reason, using the ``type`` syntax requires enabling the
+:extension:`ExplicitNamespaces` extension separately.
\ No newline at end of file
diff --git a/docs/users_guide/exts/types.rst b/docs/users_guide/exts/types.rst
index 8d2b6f9f908e13327a48c67ba457b224f708d017..c11bed1da78b6702e1f704d6060b9ee80cb9104c 100644
--- a/docs/users_guide/exts/types.rst
+++ b/docs/users_guide/exts/types.rst
@@ -22,6 +22,7 @@ Types
type_literals
type_applications
type_abstractions
+ required_type_arguments
rank_polymorphism
impredicative_types
linear_types
diff --git a/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs b/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
index e3bd35cbbb00725c17adc05b6b84d5e3c720318c..2b14665a789c93eb83d6a6cd361db83accc41936 100644
--- a/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
+++ b/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
@@ -77,6 +77,7 @@ data Extension
| InstanceSigs
| ApplicativeDo
| LinearTypes
+ | RequiredTypeArguments -- Visible forall (VDQ) in types of terms
| StandaloneDeriving
| DeriveDataTypeable
diff --git a/libraries/template-haskell/Language/Haskell/TH/Lib.hs b/libraries/template-haskell/Language/Haskell/TH/Lib.hs
index 1bf8d29b884ca417dc88393b0f8f8a3aa3f0c54a..88d6baa7954cfa4ea26b29cd50c355b8566a4cea 100644
--- a/libraries/template-haskell/Language/Haskell/TH/Lib.hs
+++ b/libraries/template-haskell/Language/Haskell/TH/Lib.hs
@@ -33,7 +33,7 @@ module Language.Haskell.TH.Lib (
-- *** Patterns
litP, varP, tupP, unboxedTupP, unboxedSumP, conP, uInfixP, parensP,
infixP, tildeP, bangP, asP, wildP, recP,
- listP, sigP, viewP,
+ listP, sigP, viewP, typeP,
fieldPat,
-- *** Pattern Guards
@@ -44,7 +44,7 @@ module Language.Haskell.TH.Lib (
appE, appTypeE, uInfixE, parensE, infixE, infixApp, sectionL, sectionR,
lamE, lam1E, lamCaseE, lamCasesE, tupE, unboxedTupE, unboxedSumE, condE,
multiIfE, letE, caseE, appsE, listE, sigE, recConE, recUpdE, stringE,
- fieldExp, getFieldE, projectionE, typedSpliceE, typedBracketE,
+ fieldExp, getFieldE, projectionE, typedSpliceE, typedBracketE, typeE,
-- **** Ranges
fromE, fromThenE, fromToE, fromThenToE,
diff --git a/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs b/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs
index 2ec036ee5ae6cd406d4045e9a276680c4208eb26..4da31ac144dd896d24b79d579b1275bea7d5374c 100644
--- a/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs
+++ b/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs
@@ -160,6 +160,9 @@ sigP :: Quote m => m Pat -> m Type -> m Pat
sigP p t = do p' <- p
t' <- t
pure (SigP p' t')
+typeP :: Quote m => m Type -> m Pat
+typeP t = do t' <- t
+ pure (TypeP t')
viewP :: Quote m => m Exp -> m Pat -> m Pat
viewP e p = do e' <- e
p' <- p
@@ -401,6 +404,8 @@ fromThenToE :: Quote m => m Exp -> m Exp -> m Exp -> m Exp
fromThenToE x y z = do { a <- x; b <- y; c <- z;
pure (ArithSeqE (FromThenToR a b c)) }
+typeE :: Quote m => m Type -> m Exp
+typeE = fmap TypeE
-------------------------------------------------------------------------------
-- * Dec
diff --git a/libraries/template-haskell/Language/Haskell/TH/Ppr.hs b/libraries/template-haskell/Language/Haskell/TH/Ppr.hs
index 001d82b50b92ef8099b5fbd831d2c7cbc5a83998..958d7a0882482ae932bcb60008c692e2119fa48d 100644
--- a/libraries/template-haskell/Language/Haskell/TH/Ppr.hs
+++ b/libraries/template-haskell/Language/Haskell/TH/Ppr.hs
@@ -234,6 +234,7 @@ pprExp _ (GetFieldE e f) = pprExp appPrec e <> text ('.': f)
pprExp _ (ProjectionE xs) = parens $ hcat $ map ((char '.'<>) . text) $ toList xs
pprExp _ (TypedBracketE e) = text "[||" <> ppr e <> text "||]"
pprExp _ (TypedSpliceE e) = text "$$" <> pprExp appPrec e
+pprExp i (TypeE t) = parensIf (i > noPrec) $ text "type" <+> ppr t
pprFields :: [(Name,Exp)] -> Doc
pprFields = sep . punctuate comma . map (\(s,e) -> pprName' Applied s <+> equals <+> ppr e)
@@ -385,6 +386,7 @@ pprPat _ (RecP nm fs)
pprPat _ (ListP ps) = brackets (commaSep ps)
pprPat i (SigP p t) = parensIf (i > noPrec) $ ppr p <+> dcolon <+> ppr t
pprPat _ (ViewP e p) = parens $ pprExp noPrec e <+> text "->" <+> pprPat noPrec p
+pprPat _ (TypeP t) = parens $ text "type" <+> ppr t
------------------------------
instance Ppr Dec where
diff --git a/libraries/template-haskell/Language/Haskell/TH/Syntax.hs b/libraries/template-haskell/Language/Haskell/TH/Syntax.hs
index b3b730ee83c9cbedb8db6a4d486ee17627adf53e..d9928029e0dd405a0ced3087ef3199e1ae35d79c 100644
--- a/libraries/template-haskell/Language/Haskell/TH/Syntax.hs
+++ b/libraries/template-haskell/Language/Haskell/TH/Syntax.hs
@@ -2307,6 +2307,7 @@ data Pat
| ListP [ Pat ] -- ^ @{ [1,2,3] }@
| SigP Pat Type -- ^ @{ p :: t }@
| ViewP Exp Pat -- ^ @{ e -> p }@
+ | TypeP Type -- ^ @{ type p }@
deriving( Show, Eq, Ord, Data, Generic )
type FieldPat = (Name,Pat)
@@ -2406,6 +2407,7 @@ data Exp
| ProjectionE (NonEmpty String) -- ^ @(.x)@ or @(.x.y)@ (Record projections)
| TypedBracketE Exp -- ^ @[|| e ||]@
| TypedSpliceE Exp -- ^ @$$e@
+ | TypeE Type -- ^ @{ type t }@
deriving( Show, Eq, Ord, Data, Generic )
type FieldExp = (Name,Exp)
diff --git a/libraries/template-haskell/changelog.md b/libraries/template-haskell/changelog.md
index 3c77fc1d2f7f4f126ee940632574ed5f6a1a03a7..0efa706750fa6e457bf4baf861e0123ab332047a 100644
--- a/libraries/template-haskell/changelog.md
+++ b/libraries/template-haskell/changelog.md
@@ -5,6 +5,9 @@
* The kind of `Code` was changed from `forall r. (Type -> Type) -> TYPE r -> Type`
to `(Type -> Type) -> forall r. TYPE r -> Type`. This enables higher-kinded usage.
+ * Extend `Pat` with `TypeP` and `Exp` with `TypeE`,
+ introduce functions `typeP` and `typeE` (GHC Proposal #281).
+
## 2.21.0.0
* Record fields now belong to separate `NameSpace`s, keyed by the parent of
diff --git a/testsuite/tests/dependent/should_fail/T15859.stderr b/testsuite/tests/dependent/should_fail/T15859.stderr
index 30b24b1206e69dbf436232a2acf6efaff0db008c..6562200e392049b5724a1231ffdce791e0d9f8e3 100644
--- a/testsuite/tests/dependent/should_fail/T15859.stderr
+++ b/testsuite/tests/dependent/should_fail/T15859.stderr
@@ -2,8 +2,8 @@
T15859.hs:9:19: error: [GHC-51580]
• Illegal visible, dependent quantification in the type of a term:
forall k -> k -> *
- (GHC does not yet support this)
• In an expression type signature: forall k -> k -> Type
In the expression: (undefined :: forall k -> k -> Type) @Int
In an equation for ‘a’:
a = (undefined :: forall k -> k -> Type) @Int
+ Suggested fix: Perhaps you intended to use RequiredTypeArguments
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail1.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail1.stderr
index da66f380c21a341da82f9c52fca19b229ad28261..993f19468071daed53145a39ae920a948676a286 100644
--- a/testsuite/tests/dependent/should_fail/T16326_Fail1.stderr
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail1.stderr
@@ -2,12 +2,12 @@
T16326_Fail1.hs:5:8: error: [GHC-51580]
• 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
+ Suggested fix: Perhaps you intended to use RequiredTypeArguments
T16326_Fail1.hs:9:8: error: [GHC-51580]
• 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
+ Suggested fix: Perhaps you intended to use RequiredTypeArguments
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail10.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail10.stderr
index 3c0ce349b97b436db5b37960f3732cc8ea51d078..bdb7eb9af09853d1cb51e7fa9a61897c30c9125e 100644
--- a/testsuite/tests/dependent/should_fail/T16326_Fail10.stderr
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail10.stderr
@@ -2,6 +2,6 @@
T16326_Fail10.hs:12:18: error: [GHC-51580]
• Illegal visible, dependent quantification in the type of a term:
forall a -> a -> a
- (GHC does not yet support this)
• In the type signature for ‘x’: forall a -> a -> a
When checking the rewrite rule "flurmp"
+ Suggested fix: Perhaps you intended to use RequiredTypeArguments
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail11.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail11.stderr
index f96814d281cdad1314283858273c12ac3c668e69..741598d1016fc18a5c8af21633f4ec9cc46feac6 100644
--- a/testsuite/tests/dependent/should_fail/T16326_Fail11.stderr
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail11.stderr
@@ -2,6 +2,6 @@
T16326_Fail11.hs:9:11: error: [GHC-51580]
• 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’
+ Suggested fix: Perhaps you intended to use RequiredTypeArguments
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail12.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail12.stderr
index 91044c0577a37f7a1772348d23121dd53a82661b..30bd04b484df768b57405a1fbd0b2d27774bab43 100644
--- a/testsuite/tests/dependent/should_fail/T16326_Fail12.stderr
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail12.stderr
@@ -2,7 +2,7 @@
T16326_Fail12.hs:6:1: error: [GHC-51580]
• 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’
+ Suggested fix: Perhaps you intended to use RequiredTypeArguments
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail2.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail2.stderr
index 1e991a28ba2b3b340becfc52e247226f0e1cf0da..2446580ad3b3f2e886dc992cf0ab693854aa830b 100644
--- a/testsuite/tests/dependent/should_fail/T16326_Fail2.stderr
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail2.stderr
@@ -2,7 +2,7 @@
T16326_Fail2.hs:6:37: error: [GHC-51580]
• 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 ()
+ Suggested fix: Perhaps you intended to use RequiredTypeArguments
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail3.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail3.stderr
index e7990218ecb746c15b88206c07ea2efe42904afc..4b2321d93bce90e3df03c07d5150b3549b667656 100644
--- a/testsuite/tests/dependent/should_fail/T16326_Fail3.stderr
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail3.stderr
@@ -2,4 +2,4 @@
T16326_Fail3.hs:6:1: error: [GHC-51580]
Illegal visible, dependent quantification in the type of a term:
forall a -> [a]
- (GHC does not yet support this)
+ Suggested fix: Perhaps you intended to use RequiredTypeArguments
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail4.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail4.stderr
index 5039c07f89fd99c058089ee976643935932a283c..d881bd6476dc87f9800c1f2580d28ba29c4bab56 100644
--- a/testsuite/tests/dependent/should_fail/T16326_Fail4.stderr
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail4.stderr
@@ -2,10 +2,10 @@
T16326_Fail4.hs:6:30: error: [GHC-51580]
• 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
+ Suggested fix: Perhaps you intended to use RequiredTypeArguments
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail5.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail5.stderr
index ba84b8a21a0d4757f68e628fd051b83b74c22e9c..afa5830013ab454d33533fe3f77fa78aaeef0ff3 100644
--- a/testsuite/tests/dependent/should_fail/T16326_Fail5.stderr
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail5.stderr
@@ -2,8 +2,8 @@
T16326_Fail5.hs:7:20: error: [GHC-51580]
• 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
+ Suggested fix: Perhaps you intended to use RequiredTypeArguments
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail6.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail6.stderr
index 6790247a364d8011d627fe4b599f98f012c904dc..bc42133775c7ecc7183f81dcad42f6000890f397 100644
--- a/testsuite/tests/dependent/should_fail/T16326_Fail6.stderr
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail6.stderr
@@ -1,5 +1,4 @@
T16326_Fail6.hs:9:12: error: [GHC-51580]
- Illegal visible, dependent quantification in the type of a term
- (GHC does not yet support this)
- In the definition of data constructor ‘MkFoo’
+ • Illegal visible, dependent quantification in the type of a term
+ • In the definition of data constructor ‘MkFoo’
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail8.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail8.stderr
index b464931e6e04d29495aeb18e08669d20605642f5..2896c7c336f81cacc989b4ff9220216d5a15990a 100644
--- a/testsuite/tests/dependent/should_fail/T16326_Fail8.stderr
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail8.stderr
@@ -1,5 +1,4 @@
T16326_Fail8.hs:7:10: error: [GHC-51580]
- Illegal visible, dependent quantification in the type of a term
- (GHC does not yet support this)
- In an instance declaration
+ • Illegal visible, dependent quantification in the type of a term
+ • In an instance declaration
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail9.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail9.stderr
index 29afc29d93edc850e193455ce21eda027029c76b..2fcfe69e2876ca2d6a1ddc2d7ca4303d75ca92fc 100644
--- a/testsuite/tests/dependent/should_fail/T16326_Fail9.stderr
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail9.stderr
@@ -2,7 +2,7 @@
T16326_Fail9.hs:11:5: error: [GHC-51580]
• 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
+ Suggested fix: Perhaps you intended to use RequiredTypeArguments
diff --git a/testsuite/tests/dependent/should_fail/T17687.stderr b/testsuite/tests/dependent/should_fail/T17687.stderr
index 03d9106e1dccc5a45a00d92af75821ee734ccb13..4983421a6ca595db43e1570ef27c72f2d0d6888d 100644
--- a/testsuite/tests/dependent/should_fail/T17687.stderr
+++ b/testsuite/tests/dependent/should_fail/T17687.stderr
@@ -2,5 +2,5 @@
T17687.hs:5:6: error: [GHC-51580]
• Illegal visible, dependent quantification in the type of a term:
forall a -> a -> a
- (GHC does not yet support this)
• In the type signature: x :: forall a -> a -> a
+ Suggested fix: Perhaps you intended to use RequiredTypeArguments
diff --git a/testsuite/tests/dependent/should_fail/T18271.stderr b/testsuite/tests/dependent/should_fail/T18271.stderr
index 8d906b3b2d89a45f0f25ac282888eb61ff6b9dee..bd99d085b2f32076bfb8a57f7ca0302e52b8087d 100644
--- a/testsuite/tests/dependent/should_fail/T18271.stderr
+++ b/testsuite/tests/dependent/should_fail/T18271.stderr
@@ -1,5 +1,4 @@
T18271.hs:7:19: error: [GHC-51580]
- Illegal visible, dependent quantification in the type of a term
- (GHC does not yet support this)
- In a deriving declaration
+ • Illegal visible, dependent quantification in the type of a term
+ • In a deriving declaration
diff --git a/testsuite/tests/driver/T4437.hs b/testsuite/tests/driver/T4437.hs
index 3c07aa56790d901441bc135b725b40406474a6db..8a805298f9c8e07d1e6e1235685fe3b53b7d1322 100644
--- a/testsuite/tests/driver/T4437.hs
+++ b/testsuite/tests/driver/T4437.hs
@@ -53,7 +53,5 @@ expectedCabalOnlyExtensions = ["Generics",
"Unsafe",
"Trustworthy",
"MonadFailDesugaring",
- "MonoPatBinds",
- -- https://github.com/haskell/cabal/pull/8521
- "RequiredTypeArguments"
+ "MonoPatBinds"
]
diff --git a/testsuite/tests/hiefile/should_run/HieVdq.hs b/testsuite/tests/hiefile/should_run/HieVdq.hs
new file mode 100644
index 0000000000000000000000000000000000000000..f02d2bd01db58fba99b3daca885e5629fe4dbefb
--- /dev/null
+++ b/testsuite/tests/hiefile/should_run/HieVdq.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module Main where
+
+import GHC.Types.Name (nameSrcSpan)
+import TestUtils
+import qualified Data.Map as M
+import Data.Foldable
+import Data.Either
+
+f :: forall a -> a -> Maybe a
+f (type t) (x :: t) = Just (x :: t)
+-- ^p1 ^p2 ^p3
+
+p1,p2 :: (Int,Int)
+p1 = (13,9)
+p2 = (13,18)
+p3 = (13,34)
+
+selectPoint' :: HieFile -> (Int,Int) -> HieAST Int
+selectPoint' hf loc =
+ maybe (error "point not found") id $ selectPoint hf loc
+
+main = do
+ (df, hf) <- readTestHie "HieVdq.hie"
+ forM_ [p1,p2,p3] $ \point -> do
+ putStr $ "At " ++ show point ++ ", got names: "
+ let names =
+ concatMap (rights . M.keys . nodeIdentifiers) $
+ M.elems $ getSourcedNodeInfo $
+ sourcedNodeInfo $ selectPoint' hf point
+ forM_ names $ \name -> do
+ putStrLn (render df (nameSrcSpan name, name))
diff --git a/testsuite/tests/hiefile/should_run/HieVdq.stdout b/testsuite/tests/hiefile/should_run/HieVdq.stdout
new file mode 100644
index 0000000000000000000000000000000000000000..edfc21d527f0fe42083ab59452ab99dba01f0a06
--- /dev/null
+++ b/testsuite/tests/hiefile/should_run/HieVdq.stdout
@@ -0,0 +1,3 @@
+At (13,9), got names: (HieVdq.hs:13:9, t)
+At (13,18), got names: (HieVdq.hs:13:9, t)
+At (13,34), got names: (HieVdq.hs:13:9, t)
diff --git a/testsuite/tests/hiefile/should_run/all.T b/testsuite/tests/hiefile/should_run/all.T
index 2fc72443cc65326372ebaed0f96a8acfa6d02741..2628adb2ad311f1bc1287057b1c347a5d95f0bb1 100644
--- a/testsuite/tests/hiefile/should_run/all.T
+++ b/testsuite/tests/hiefile/should_run/all.T
@@ -4,3 +4,4 @@ test('T20341', [extra_run_opts('"' + config.libdir + '"'), extra_files(['TestUti
test('T23492', [extra_run_opts('"' + config.libdir + '"'), extra_files(['TestUtils.hs'])], compile_and_run, ['-package ghc -fwrite-ide-info'])
test('RecordDotTypes', [extra_run_opts('"' + config.libdir + '"'), extra_files(['TestUtils.hs'])], compile_and_run, ['-package ghc -fwrite-ide-info'])
test('SpliceTypes', [req_th, extra_run_opts('"' + config.libdir + '"'), extra_files(['TestUtils.hs'])], compile_and_run, ['-package ghc -fwrite-ide-info'])
+test('HieVdq', [extra_run_opts('"' + config.libdir + '"'), extra_files(['TestUtils.hs'])], compile_and_run, ['-package ghc -fwrite-ide-info'])
diff --git a/testsuite/tests/vdq-rta/should_compile/Makefile b/testsuite/tests/vdq-rta/should_compile/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..bced01ff9b62f2c19d86ae87e96035574fca2c4a
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/Makefile
@@ -0,0 +1,3 @@
+TOP=../../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_compile/T14158_vdq.hs b/testsuite/tests/vdq-rta/should_compile/T14158_vdq.hs
new file mode 100644
index 0000000000000000000000000000000000000000..2cb043a6901a84e5439102124672d4aa4e7b6a28
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/T14158_vdq.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T14158_vdq where
+
+import Data.Kind
+import qualified Control.Category as Cat
+
+civ ::
+ forall {k}.
+ forall (cat :: k -> k -> Type) ->
+ forall (a :: k).
+ Cat.Category cat =>
+ cat a a
+civ (type cat) = Cat.id @cat
+
+f = (civ (type (->)) >>=)
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_compile/T17792_vdq.hs b/testsuite/tests/vdq-rta/should_compile/T17792_vdq.hs
new file mode 100644
index 0000000000000000000000000000000000000000..ac5e8f8520c9655e36cee7257447c59219a7247a
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/T17792_vdq.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE RequiredTypeArguments #-}
+{-# OPTIONS_GHC -fdefer-type-errors #-}
+
+module T17792_vdq where
+
+class C a where
+ m :: a
+
+-- Check that instantiating an out-of-scope identifier with a
+-- required type argument in a class instance and with deferred
+-- type errors does not lead to a panic.
+--
+-- This problem was observed with TypeApplications in #17792.
+-- Here we check that RequiredTypeArguments, a somewhat related
+-- feature, is not affected.
+instance C Bool where
+ m = notInScope (type Word)
diff --git a/testsuite/tests/vdq-rta/should_compile/T17792_vdq.stderr b/testsuite/tests/vdq-rta/should_compile/T17792_vdq.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..7678b29c906e5e92eb8debeb702e8d067cf31308
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/T17792_vdq.stderr
@@ -0,0 +1,3 @@
+
+T17792_vdq.hs:18:7: warning: [GHC-88464] [-Wdeferred-out-of-scope-variables (in -Wdefault)]
+ Variable not in scope: notInScope :: Bool
diff --git a/testsuite/tests/vdq-rta/should_compile/T22326_callStack.hs b/testsuite/tests/vdq-rta/should_compile/T22326_callStack.hs
new file mode 100644
index 0000000000000000000000000000000000000000..dc2730e25e268b2721ddd74e9bb8647a67135023
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/T22326_callStack.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T22326_callStack where
+
+import Data.Kind (Type)
+import GHC.Stack
+
+f :: forall (a :: Type) -> CallStack
+f (type _) = callStack
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_compile/T22326_idv.hs b/testsuite/tests/vdq-rta/should_compile/T22326_idv.hs
new file mode 100644
index 0000000000000000000000000000000000000000..b6372039b4a57049a1536e52b2bc2159b0c977f1
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/T22326_idv.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE RequiredTypeArguments #-}
+{-# LANGUAGE TypeApplications #-}
+
+module T22326_idv where
+
+-- Definition:
+idv :: forall a -> a -> a
+idv (type t) x = x :: t
+
+-- Usage:
+rInt = idv (type Int) 42
+rDouble = idv (type Double) 42
+rBool = idv (type Bool) True
+rChar = idv (type Char) 'x'
+rList = idv (type [Int]) [1,2,3]
+rTup = idv (type (Int,Bool)) (0,False)
+
+-- Definition (using a lambda)
+idv_lam :: forall a -> a -> a
+idv_lam = \(type t) x -> x :: t
+
+-- Definition (eta-reduced)
+idv_eta :: forall a -> a -> a
+idv_eta = idv
+
+-- Definition (using vta on the rhs)
+idv_vta :: forall a -> a -> a
+idv_vta (type t) = id @t
+
+-- Definition (using sig on the rhs)
+idv_sig :: forall a -> a -> a
+idv_sig (type t) = id :: t -> t
+
+-- Definition (using a wildcard)
+idv_wild :: forall a -> a -> a
+idv_wild (type _) x = x
+
+-- Usage (using a wildcard)
+rBool' = idv (type _) True
+rChar' = idv (type _) 'x'
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_compile/T22326_noext.hs b/testsuite/tests/vdq-rta/should_compile/T22326_noext.hs
new file mode 100644
index 0000000000000000000000000000000000000000..02088fac3cf71b82a9dc21c96007737268547d61
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/T22326_noext.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE NoRequiredTypeArguments #-} -- VDQ/RTA is disabled
+{-# LANGUAGE ExplicitNamespaces #-}
+
+module T22326_noext where
+
+import T22326_noext_def
+
+-- The calls to id_vdq are accepted, even though RequiredTypeArguments are
+-- disabled in this module.
+--
+-- The extension is only required at definition site, not at use sites.
+--
+s = id_vdq (type String) "Hello"
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_compile/T22326_noext_def.hs b/testsuite/tests/vdq-rta/should_compile/T22326_noext_def.hs
new file mode 100644
index 0000000000000000000000000000000000000000..b571298f410fae6b0a0c352a926fd630ba4dd6ae
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/T22326_noext_def.hs
@@ -0,0 +1,10 @@
+-- Helper module for use in T22326_noext.
+-- Defines id_vdq.
+
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T22326_noext_def (id_vdq) where
+
+id_vdq :: forall a -> a -> a
+id_vdq = \(type _) -> id
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_compile/T22326_sig.hs b/testsuite/tests/vdq-rta/should_compile/T22326_sig.hs
new file mode 100644
index 0000000000000000000000000000000000000000..17b3a96e7ec1caf66d4cfc020093007a3313378f
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/T22326_sig.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE RequiredTypeArguments #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module T22326_sig where
+
+import Data.Kind
+import Data.Type.Bool
+import Data.Proxy
+
+data SBool b where
+ SFalse :: SBool False
+ STrue :: SBool True
+
+class KnownBool b where
+ boolSing :: SBool b
+
+boolVal :: forall b -> KnownBool b => Bool
+boolVal (type b) =
+ case boolSing @b of
+ SFalse -> False
+ STrue -> True
+
+f :: forall x -> x -> ()
+f (type (x :: Type)) x = ()
+
+g :: forall b -> KnownBool b => If b Integer String
+g (type (b :: Bool)) =
+ case boolSing @b of
+ SFalse -> "Hello"
+ STrue -> 42
+
+type FromJust :: Maybe a -> a
+type family FromJust m where
+ FromJust (Just x) = x
+
+type KindOf :: k -> Type
+type KindOf (a :: k) = k
+
+h :: forall m -> Proxy (KindOf (FromJust m))
+h (type (m :: Maybe a)) = Proxy @a
+
+hBool :: Proxy Bool
+hBool = h (type (Just True))
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_compile/T22326_sizeOf.hs b/testsuite/tests/vdq-rta/should_compile/T22326_sizeOf.hs
new file mode 100644
index 0000000000000000000000000000000000000000..ee55357b105f6f5733a4da74f2c9ca5eef1e27e5
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/T22326_sizeOf.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T22326_sizeOf where
+
+import Foreign.Storable
+
+-- Definition:
+sizeOfVis :: forall a -> Storable a => Int
+sizeOfVis (type t) = sizeOf (undefined :: t)
+
+-- Usage:
+sInt = sizeOfVis (type Int)
+sDouble = sizeOfVis (type Double)
+sBool = sizeOfVis (type Bool)
+sChar = sizeOfVis (type Char)
+sUnit = sizeOfVis (type ())
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_compile/T22326_symbolVal.hs b/testsuite/tests/vdq-rta/should_compile/T22326_symbolVal.hs
new file mode 100644
index 0000000000000000000000000000000000000000..3061dbc3678a1f3b551dccfa69e780818f7a5335
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/T22326_symbolVal.hs
@@ -0,0 +1,81 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE RequiredTypeArguments #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T22326_symbolVal where
+
+import Data.Kind
+import Data.Proxy
+import GHC.TypeLits
+
+-- Definition:
+symbolValVis :: forall s -> KnownSymbol s => String
+symbolValVis (type s) = symbolVal (Proxy :: Proxy s)
+
+-- Usage:
+strHelloWorld = symbolValVis (type ("Hello, " `AppendSymbol` "World"))
+
+-- Operator taking a term-level argument before a required type argument:
+(++.) :: String -> forall (s :: Symbol) -> KnownSymbol s => String
+s1 ++. (type s2) = s1 ++ symbolValVis (type s2)
+infixr 5 ++.
+
+strTmPlusTy = "Tm" ++ "+" ++. (type "Ty")
+
+-------------------------------------------------
+-- Required type arguments in class methods --
+-- and in higher-rank positions --
+-------------------------------------------------
+
+-- Continuation-passing encoding of a list spine:
+--
+-- data Spine xs where
+-- Cons :: Spine xs -> Spine (x : xs)
+-- Nil :: Spine '[]
+--
+type WithSpine :: [k] -> Constraint
+class WithSpine xs where
+ onSpine ::
+ forall r.
+ forall xs' -> (xs' ~ xs) => -- workaround b/c it's not possible to make xs visible
+ ((xs ~ '[]) => r) ->
+ (forall y ys -> (xs ~ (y : ys)) => WithSpine ys => r) ->
+ r
+
+instance WithSpine '[] where
+ onSpine (type xs) onNil _ = onNil
+
+instance forall x xs. WithSpine xs => WithSpine (x : xs) where
+ onSpine (type xs') _ onCons = onCons (type x) (type xs)
+
+type All :: (k -> Constraint) -> [k] -> Constraint
+type family All c xs where
+ All c '[] = ()
+ All c (a : as) = (c a, All c as)
+
+type KnownSymbols :: [Symbol] -> Constraint
+class All KnownSymbol ss => KnownSymbols ss
+instance All KnownSymbol ss => KnownSymbols ss
+
+symbolVals :: forall ss -> (KnownSymbols ss, WithSpine ss) => [String]
+symbolVals (type ss) =
+ onSpine (type ss) [] $ \(type s) (type ss') ->
+ symbolValVis (type s) : symbolVals (type ss')
+
+-- Reify a type-level list of strings at the term level.
+strsLoremIpsum = symbolVals (type ["lorem", "ipsum", "dolor", "sit", "amet"])
+
+-- Pass a required type argument to a continuation:
+withSymbolVis :: String -> (forall s -> KnownSymbol s => r) -> r
+withSymbolVis str cont =
+ case someSymbolVal str of
+ SomeSymbol (Proxy :: Proxy s) -> cont (type s)
+
+-- Use a required type argument in a continuation:
+strLengthViaSymbol :: String -> Int
+strLengthViaSymbol str =
+ withSymbolVis str $ \(type s) ->
+ length (symbolValVis (type s))
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_compile/T22326_th_dump1.hs b/testsuite/tests/vdq-rta/should_compile/T22326_th_dump1.hs
new file mode 100644
index 0000000000000000000000000000000000000000..08eaf6cf8c8b38c4e50938f3eaeed060b921b1a7
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/T22326_th_dump1.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE RequiredTypeArguments #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+module T22326_th_dump1 where
+
+$([d| f :: Integer -> forall a -> Num a => a
+ f n (type t) = fromInteger n :: t
+ |])
+
+$([d| x = 42 `f` (type Double)
+ n = f 42 (type Integer)
+ |])
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_compile/T22326_th_dump1.stderr b/testsuite/tests/vdq-rta/should_compile/T22326_th_dump1.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..8158fcd8d3abddb9d6de8e7447ce86d69b3c74d9
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/T22326_th_dump1.stderr
@@ -0,0 +1,12 @@
+T22326_th_dump1.hs:(7,2)-(9,7): Splicing declarations
+ [d| f :: Integer -> forall a -> Num a => a
+ f n (type t) = fromInteger n :: t |]
+ ======>
+ f :: Integer -> forall a -> Num a => a
+ f n (type t) = fromInteger n :: t
+T22326_th_dump1.hs:(11,2)-(13,7): Splicing declarations
+ [d| x = 42 `f` (type Double)
+ n = f 42 (type Integer) |]
+ ======>
+ x = (42 `f` (type Double))
+ n = f 42 (type Integer)
diff --git a/testsuite/tests/vdq-rta/should_compile/T22326_th_pprint1.hs b/testsuite/tests/vdq-rta/should_compile/T22326_th_pprint1.hs
new file mode 100644
index 0000000000000000000000000000000000000000..69279a6a888da5d144c1be8f49d8421163e94840
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/T22326_th_pprint1.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE RequiredTypeArguments #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+module T22326_th_pprint1 where
+
+import System.IO
+import Language.Haskell.TH
+
+do decls <-
+ [d|
+ -- Definition:
+ f :: Integer -> forall a -> Num a => a
+ f n (type _) = fromInteger n
+
+ -- Usage:
+ x = 42 `f` (type Double)
+ n = f 42 (type Integer)
+ |]
+ runIO $ hPutStrLn stderr $ pprint decls
+ return []
diff --git a/testsuite/tests/vdq-rta/should_compile/T22326_th_pprint1.stderr b/testsuite/tests/vdq-rta/should_compile/T22326_th_pprint1.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..5bb1b6da12a4d60dde6d26eb32989a1361c588a6
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/T22326_th_pprint1.stderr
@@ -0,0 +1,5 @@
+f_0 :: GHC.Num.Integer.Integer ->
+ forall a_1 -> GHC.Num.Num a_1 => a_1
+f_0 n_2 (type _) = GHC.Num.fromInteger n_2
+x_3 = 42 `f_0` (type GHC.Types.Double)
+n_4 = f_0 42 (type GHC.Num.Integer.Integer)
diff --git a/testsuite/tests/vdq-rta/should_compile/T22326_typeRep.hs b/testsuite/tests/vdq-rta/should_compile/T22326_typeRep.hs
new file mode 100644
index 0000000000000000000000000000000000000000..3c00a55901b87a8f2114b92ee3793af295a2a8f9
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/T22326_typeRep.hs
@@ -0,0 +1,40 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE RequiredTypeArguments #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE DataKinds #-}
+
+module T22326_typeRep where
+
+import Type.Reflection
+import Data.Kind
+import GHC.TypeLits
+
+-- Definition:
+typeRepVis :: forall a -> Typeable a => TypeRep a
+typeRepVis (type t) = typeRep @t
+
+-- Usage:
+tMaybe = typeRepVis (type Maybe)
+tMaybeString = typeRepVis (type (Maybe String))
+tFunctor = typeRepVis (type Functor)
+tHello = typeRepVis (type "Hello")
+tTupFun = typeRepVis (type ((Int,Bool,Char) -> Double))
+
+-- Definition (using a lambda)
+typeRepVis_lam :: forall a -> Typeable a => TypeRep a
+typeRepVis_lam = \(type t) -> typeRep @t
+
+-- Definition (with explicit kind quantification)
+typeRepVis_kforall :: forall k. forall (a :: k) -> Typeable a => TypeRep a
+typeRepVis_kforall = typeRepVis
+
+-- Definition (with required kind parameter):
+typeRepKiVis :: forall k (a :: k) -> Typeable a => TypeRep a
+typeRepKiVis (type k) (type a) = typeRep @(a :: k)
+
+-- Usage (with required kind parameter):
+tMaybe' = typeRepKiVis (type (Type -> Type)) (type Maybe)
+tMaybeString' = typeRepKiVis (type Type) (type (Maybe String))
+tFunctor' = typeRepKiVis (type ((Type -> Type) -> Constraint)) (type Functor)
+tHello' = typeRepKiVis (type Symbol) (type "Hello")
+tTupFun' = typeRepKiVis (type Type) (type ((Int,Bool,Char) -> Double))
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_compile/WithSpineVDQ_LintErr.hs b/testsuite/tests/vdq-rta/should_compile/WithSpineVDQ_LintErr.hs
new file mode 100644
index 0000000000000000000000000000000000000000..d154f1280a132881a22f0c70699bc8055d3156dc
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/WithSpineVDQ_LintErr.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE RequiredTypeArguments #-}
+{-# LANGUAGE DataKinds #-}
+
+module WithSpineVDQ_LintErr (uSSZ) where
+
+import Data.Kind
+
+data Peano = Z | S Peano
+
+type WithSpine :: Peano -> Constraint
+class WithSpine n where
+ -- Single-method class (newtype dict)
+ onSpine ::
+ forall n' -> (n' ~ n) => -- workaround b/c it's not possible to make `n` visible
+ (forall m -> (n ~ S m) => WithSpine m => ()) ->
+ ()
+
+instance WithSpine Z where
+ onSpine (type n) _ = ()
+
+instance forall m. WithSpine m => WithSpine (S m) where
+ onSpine (type n) f = f (type m)
+
+getUnit :: forall n -> WithSpine n => ()
+getUnit (type n) = onSpine (type n) (\(type n') -> getUnit (type n'))
+
+-- uSSZ :: ()
+uSSZ = getUnit (type (S (S Z)))
diff --git a/testsuite/tests/vdq-rta/should_compile/all.T b/testsuite/tests/vdq-rta/should_compile/all.T
new file mode 100644
index 0000000000000000000000000000000000000000..598048af1987fd845ab44a4ddefe1d4d3e06627a
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/all.T
@@ -0,0 +1,15 @@
+setTestOpts(normalise_version('base','ghc-prim'))
+
+test('T22326_idv', normal, compile, [''])
+test('T22326_typeRep', normal, compile, [''])
+test('T22326_sizeOf', normal, compile, [''])
+test('T22326_symbolVal', normal, compile, [''])
+test('T22326_noext', extra_files(['T22326_noext_def.hs']), multimod_compile, ['T22326_noext', '-v0'])
+test('T22326_callStack', normal, compile, [''])
+test('T22326_sig', normal, compile, [''])
+test('T17792_vdq', normal, compile, [''])
+test('T14158_vdq', normal, compile, [''])
+test('WithSpineVDQ_LintErr', normal, compile, [''])
+
+test('T22326_th_dump1', req_th, compile, ['-v0 -ddump-splices -dsuppress-uniques'])
+test('T22326_th_pprint1', req_th, compile, [''])
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_fail/Makefile b/testsuite/tests/vdq-rta/should_fail/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..bced01ff9b62f2c19d86ae87e96035574fca2c4a
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/Makefile
@@ -0,0 +1,3 @@
+TOP=../../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_ado.hs b/testsuite/tests/vdq-rta/should_fail/T22326_fail_ado.hs
new file mode 100644
index 0000000000000000000000000000000000000000..8f1dc3493840d7e8a6062544951bfa9fd2d89862
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_ado.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE RequiredTypeArguments #-}
+{-# LANGUAGE ApplicativeDo #-}
+
+module T22326_fail_ado where
+
+m :: IO ()
+m = do
+ type a <- undefined
+ pure ()
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_ado.stderr b/testsuite/tests/vdq-rta/should_fail/T22326_fail_ado.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..64a0c19b67bcc48deac19d7a536dbfee0cf615dc
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_ado.stderr
@@ -0,0 +1,9 @@
+
+T22326_fail_ado.hs:9:3: error: [GHC-70206]
+ • Illegal type pattern.
+ A type pattern must be checked against a visible forall.
+ • In the pattern: type a
+ In a stmt of a 'do' block: type a <- undefined
+ In the expression:
+ do type a <- undefined
+ return ()
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_app.hs b/testsuite/tests/vdq-rta/should_fail/T22326_fail_app.hs
new file mode 100644
index 0000000000000000000000000000000000000000..b2de7829662f90f79b0b42841b0227467b026288
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_app.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T22326_fail_app where
+
+xhead = (type Maybe) undefined
+xarg = undefined (type Int)
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_app.stderr b/testsuite/tests/vdq-rta/should_fail/T22326_fail_app.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..137f47df7b29f81ca63c780fbde1f9d4809decf2
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_app.stderr
@@ -0,0 +1,13 @@
+
+T22326_fail_app.hs:6:10: error: [GHC-35499]
+ • Illegal type expression.
+ A type expression must be used to instantiate a visible forall.
+ • In the expression: (type Maybe) undefined
+ In an equation for ‘xhead’: xhead = (type Maybe) undefined
+
+T22326_fail_app.hs:7:20: error: [GHC-35499]
+ • Illegal type expression.
+ A type expression must be used to instantiate a visible forall.
+ • In the first argument of ‘undefined’, namely ‘(type Int)’
+ In the expression: undefined (type Int)
+ In an equation for ‘xarg’: xarg = undefined (type Int)
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_caseof.hs b/testsuite/tests/vdq-rta/should_fail/T22326_fail_caseof.hs
new file mode 100644
index 0000000000000000000000000000000000000000..f1a0127b8b301fa4180ed2d874dc0c7f950a41f4
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_caseof.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T22326_fail_caseof where
+
+f :: Int -> Bool
+f x =
+ case x of
+ (type _) -> True
+ _ -> False
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_caseof.stderr b/testsuite/tests/vdq-rta/should_fail/T22326_fail_caseof.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..63315bc2e09b3848a1d2bbb1e4257a83b5e04f73
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_caseof.stderr
@@ -0,0 +1,10 @@
+
+T22326_fail_caseof.hs:9:6: error: [GHC-70206]
+ • Illegal type pattern.
+ A type pattern must be checked against a visible forall.
+ • In the pattern: type _
+ In a case alternative: (type _) -> True
+ In the expression:
+ case x of
+ (type _) -> True
+ _ -> False
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_ext1.hs b/testsuite/tests/vdq-rta/should_fail/T22326_fail_ext1.hs
new file mode 100644
index 0000000000000000000000000000000000000000..444d4b5187d25cb87d9f817603e63b394a8d825a
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_ext1.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+{-# LANGUAGE NoExplicitNamespaces #-}
+
+module T22326_fail_ext1 where
+
+-- Using the (type ...) syntax requires the ExplicitNamespaces extension,
+-- which is disabled in this module.
+--
+-- This is not related to whether the RequiredTypeArguments extension is
+-- enabled, as Part 2 of the proposal (https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst)
+-- shows how the feature could be used without the ‘type’ keyword.
+x = undefined (type Int)
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_ext1.stderr b/testsuite/tests/vdq-rta/should_fail/T22326_fail_ext1.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..fed2bb02f328d1ccbc64a0c79b8df9cb73165543
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_ext1.stderr
@@ -0,0 +1,4 @@
+
+T22326_fail_ext1.hs:12:16: error: [GHC-47007]
+ Illegal keyword 'type'
+ Suggested fix: Perhaps you intended to use ExplicitNamespaces
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_ext2.hs b/testsuite/tests/vdq-rta/should_fail/T22326_fail_ext2.hs
new file mode 100644
index 0000000000000000000000000000000000000000..391e9b516ec3898e911a17367b2f03877dabe219
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_ext2.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE NoRequiredTypeArguments #-}
+
+module T22326_fail_ext2 where
+
+-- Using visible forall in the type of a term is only possible
+-- with the RequiredTypeArguments extension, which is disabled
+-- in this module.
+f :: forall x -> ()
+f = f
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_ext2.stderr b/testsuite/tests/vdq-rta/should_fail/T22326_fail_ext2.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..a3a1996981430e5573e71edc0542a6c5a9cf4ead
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_ext2.stderr
@@ -0,0 +1,6 @@
+
+T22326_fail_ext2.hs:8:6: error: [GHC-51580]
+ • Illegal visible, dependent quantification in the type of a term:
+ forall {k}. forall (x :: k) -> ()
+ • In the type signature: f :: forall x -> ()
+ Suggested fix: Perhaps you intended to use RequiredTypeArguments
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_match.hs b/testsuite/tests/vdq-rta/should_fail/T22326_fail_match.hs
new file mode 100644
index 0000000000000000000000000000000000000000..64120ddd62e62dd8e9a0873e4de0b7404400ae42
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_match.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+
+module T22326_fail_match where
+
+f :: forall t -> t -> ()
+f (type (Maybe a)) x = ()
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_match.stderr b/testsuite/tests/vdq-rta/should_fail/T22326_fail_match.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..591855176fe711a985c36abc2c927dac05af13b0
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_match.stderr
@@ -0,0 +1,9 @@
+
+T22326_fail_match.hs:7:4: error: [GHC-25897]
+ • Couldn't match expected type ‘t’ with actual type ‘Maybe a’
+ ‘t’ is a rigid type variable bound by
+ a type expected by the context:
+ forall t -> t -> ()
+ at T22326_fail_match.hs:7:1-25
+ • In the pattern: type (Maybe a)
+ In an equation for ‘f’: f (type (Maybe a)) x = ()
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_n_args.hs b/testsuite/tests/vdq-rta/should_fail/T22326_fail_n_args.hs
new file mode 100644
index 0000000000000000000000000000000000000000..ba0f7a468a39901d3c61ce39087b6212605bf04b
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_n_args.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE RequiredTypeArguments, ExplicitNamespaces #-}
+
+module T22326_fail_n_args where
+
+f :: a -> forall b -> b
+f x (type y) z = undefined
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_n_args.stderr b/testsuite/tests/vdq-rta/should_fail/T22326_fail_n_args.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..b313b93601b612c0bb0b8c96e0a0a5f02f00e724
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_n_args.stderr
@@ -0,0 +1,9 @@
+
+T22326_fail_n_args.hs:6:1: error: [GHC-25897]
+ • Couldn't match expected type ‘b’ with actual type ‘p0 -> a0’
+ ‘b’ is a rigid type variable bound by
+ a type expected by the context:
+ forall b -> b
+ at T22326_fail_n_args.hs:6:1-26
+ • The equation for ‘f’ has three value arguments,
+ but its type ‘a -> forall b -> b’ has only two
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_nonlinear.hs b/testsuite/tests/vdq-rta/should_fail/T22326_fail_nonlinear.hs
new file mode 100644
index 0000000000000000000000000000000000000000..ce9f13cc96992438a31dfa43eda25d43364082af
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_nonlinear.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T22326_fail_nonlinear where
+
+import Data.Kind (Type)
+
+f :: forall (a :: Type) (b :: Type) -> ()
+f (type t) (type t) = ()
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_nonlinear.stderr b/testsuite/tests/vdq-rta/should_fail/T22326_fail_nonlinear.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..513315502b6b99f8e0c8d265667c5630ee9e5529
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_nonlinear.stderr
@@ -0,0 +1,6 @@
+
+T22326_fail_nonlinear.hs:9:9: error: [GHC-10498]
+ • Conflicting definitions for ‘t’
+ Bound at: T22326_fail_nonlinear.hs:9:9
+ T22326_fail_nonlinear.hs:9:18
+ • In an equation for ‘f’
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_notInScope.hs b/testsuite/tests/vdq-rta/should_fail/T22326_fail_notInScope.hs
new file mode 100644
index 0000000000000000000000000000000000000000..a4a882cbfbe3b022f6154a36983569a9fd959d20
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_notInScope.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T22326_fail_notInScope where
+
+x = notInScope (type Int)
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_notInScope.stderr b/testsuite/tests/vdq-rta/should_fail/T22326_fail_notInScope.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..242fa221ffc88a9d0e9f4b9ccb0e6bfa0cf302cc
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_notInScope.stderr
@@ -0,0 +1,3 @@
+
+T22326_fail_notInScope.hs:6:5: error: [GHC-88464]
+ Variable not in scope: notInScope
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_pat.hs b/testsuite/tests/vdq-rta/should_fail/T22326_fail_pat.hs
new file mode 100644
index 0000000000000000000000000000000000000000..c1625451362b60a64c1ff291dd079ba52042d9b5
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_pat.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T22326_fail_pat where
+
+import Data.Kind (Type)
+
+f :: forall (a :: Type) -> ()
+f (type Int) = ()
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_pat.stderr b/testsuite/tests/vdq-rta/should_fail/T22326_fail_pat.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..49deefd8211f03f3592fcb1ad55ef95914e85615
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_pat.stderr
@@ -0,0 +1,9 @@
+
+T22326_fail_pat.hs:9:4: error: [GHC-25897]
+ • Couldn't match expected type ‘a’ with actual type ‘Int’
+ ‘a’ is a rigid type variable bound by
+ a type expected by the context:
+ forall a -> ()
+ at T22326_fail_pat.hs:9:1-17
+ • In the pattern: type Int
+ In an equation for ‘f’: f (type Int) = ()
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_patsyn.hs b/testsuite/tests/vdq-rta/should_fail/T22326_fail_patsyn.hs
new file mode 100644
index 0000000000000000000000000000000000000000..89593ccec14a1a50c92a1430ed081bef72682a5f
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_patsyn.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE PatternSynonyms #-}
+
+module T22326_fail_patsyn where
+
+pattern MyPat = type Int
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_patsyn.stderr b/testsuite/tests/vdq-rta/should_fail/T22326_fail_patsyn.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..fef46bb00a2f1e04758eedd0d3a157357a92bd1b
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_patsyn.stderr
@@ -0,0 +1,6 @@
+
+T22326_fail_patsyn.hs:6:17: error: [GHC-70206]
+ • Illegal type pattern.
+ A type pattern must be checked against a visible forall.
+ • In the pattern: type Int
+ In the declaration for pattern synonym ‘MyPat’
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_raw_arg.hs b/testsuite/tests/vdq-rta/should_fail/T22326_fail_raw_arg.hs
new file mode 100644
index 0000000000000000000000000000000000000000..519194599c63692882b6d71a2e132aa590b9aa26
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_raw_arg.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T22326_fail_raw_arg where
+
+f :: forall (a :: k) -> ()
+f (type _) = ()
+
+x = f (\_ -> _)
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_raw_arg.stderr b/testsuite/tests/vdq-rta/should_fail/T22326_fail_raw_arg.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..ffc0940a9808d1f5df68eedd077cdba93d91f7d2
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_raw_arg.stderr
@@ -0,0 +1,6 @@
+
+T22326_fail_raw_arg.hs:9:5: error: [GHC-29092]
+ • Ill-formed type argument: \ _ -> _
+ Expected a type expression introduced with the ‘type’ keyword.
+ • In the expression: f (\ _ -> _)
+ In an equation for ‘x’: x = f (\ _ -> _)
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_raw_pat.hs b/testsuite/tests/vdq-rta/should_fail/T22326_fail_raw_pat.hs
new file mode 100644
index 0000000000000000000000000000000000000000..2b8ca18a2eafa83e0fa6b0efe88973a4c812fad4
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_raw_pat.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T22326_fail_raw_pat where
+
+f :: forall (a :: k) -> ()
+f x = ()
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_raw_pat.stderr b/testsuite/tests/vdq-rta/should_fail/T22326_fail_raw_pat.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..cae79feb09f417c1187c92fc2dd51c3dacb0021c
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_raw_pat.stderr
@@ -0,0 +1,5 @@
+
+T22326_fail_raw_pat.hs:7:3: error: [GHC-88754]
+ • Ill-formed type pattern: x
+ Expected a type pattern introduced with the ‘type’ keyword.
+ • In an equation for ‘f’: f x = ()
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_top.hs b/testsuite/tests/vdq-rta/should_fail/T22326_fail_top.hs
new file mode 100644
index 0000000000000000000000000000000000000000..a2701fe7c334fb4fbffb8e7894c8f95266892308
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_top.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T22326_fail_top where
+
+xtop = type Int
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_top.stderr b/testsuite/tests/vdq-rta/should_fail/T22326_fail_top.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..0dfd5a144f63d6ca534d17f4b18b4249bead67e3
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_top.stderr
@@ -0,0 +1,6 @@
+
+T22326_fail_top.hs:6:9: error: [GHC-35499]
+ • Illegal type expression.
+ A type expression must be used to instantiate a visible forall.
+ • In the expression: type Int
+ In an equation for ‘xtop’: xtop = type Int
diff --git a/testsuite/tests/vdq-rta/should_fail/all.T b/testsuite/tests/vdq-rta/should_fail/all.T
new file mode 100644
index 0000000000000000000000000000000000000000..2dee99b6e8acac0515dda7190ce05713e9024e31
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/all.T
@@ -0,0 +1,14 @@
+test('T22326_fail_ext1', normal, compile_fail, [''])
+test('T22326_fail_ext2', normal, compile_fail, [''])
+test('T22326_fail_top', normal, compile_fail, [''])
+test('T22326_fail_app', normal, compile_fail, [''])
+test('T22326_fail_notInScope', normal, compile_fail, [''])
+test('T22326_fail_raw_pat', normal, compile_fail, [''])
+test('T22326_fail_raw_arg', normal, compile_fail, [''])
+test('T22326_fail_pat', normal, compile_fail, [''])
+test('T22326_fail_nonlinear', normal, compile_fail, [''])
+test('T22326_fail_caseof', normal, compile_fail, [''])
+test('T22326_fail_ado', normal, compile_fail, [''])
+test('T22326_fail_n_args', normal, compile_fail, [''])
+test('T22326_fail_patsyn', normal, compile_fail, [''])
+test('T22326_fail_match', normal, compile_fail, [''])
\ No newline at end of file
diff --git a/utils/check-exact/ExactPrint.hs b/utils/check-exact/ExactPrint.hs
index 3bf8b77be296534ba5c02d014d86a51a5dae8299..1eaa26853e410c8fc88a614b2a53b57e9d51375a 100644
--- a/utils/check-exact/ExactPrint.hs
+++ b/utils/check-exact/ExactPrint.hs
@@ -2656,6 +2656,7 @@ instance ExactPrint (HsExpr GhcPs) where
getAnnotationEntry (HsProc an _ _) = fromAnn an
getAnnotationEntry (HsStatic an _) = fromAnn an
getAnnotationEntry (HsPragE{}) = NoEntryVal
+ getAnnotationEntry (HsEmbTy{}) = NoEntryVal
setAnnotationAnchor a@(HsVar{}) _ _s = a
setAnnotationAnchor (HsUnboundVar an a) anc cs = (HsUnboundVar (setAnchorEpa an anc cs) a)
@@ -2694,6 +2695,7 @@ instance ExactPrint (HsExpr GhcPs) where
setAnnotationAnchor (HsProc an a b) anc cs = (HsProc (setAnchorEpa an anc cs) a b)
setAnnotationAnchor (HsStatic an a) anc cs = (HsStatic (setAnchorEpa an anc cs) a)
setAnnotationAnchor a@(HsPragE{}) _ _s = a
+ setAnnotationAnchor a@(HsEmbTy{}) _ _s = a
exact (HsVar x n) = do
n' <- markAnnotated n
@@ -4559,6 +4561,7 @@ instance ExactPrint (Pat GhcPs) where
getAnnotationEntry (NPat an _ _ _) = fromAnn an
getAnnotationEntry (NPlusKPat an _ _ _ _ _) = fromAnn an
getAnnotationEntry (SigPat an _ _) = fromAnn an
+ getAnnotationEntry (EmbTyPat _ _ _) = NoEntryVal
setAnnotationAnchor a@(WildPat _) _ _s = a
setAnnotationAnchor a@(VarPat _ _) _ _s = a
@@ -4576,6 +4579,7 @@ instance ExactPrint (Pat GhcPs) where
setAnnotationAnchor (NPat an a b c) anc cs = (NPat (setAnchorEpa an anc cs) a b c)
setAnnotationAnchor (NPlusKPat an a b c d e) anc cs = (NPlusKPat (setAnchorEpa an anc cs) a b c d e)
setAnnotationAnchor (SigPat an a b) anc cs = (SigPat (setAnchorEpa an anc cs) a b)
+ setAnnotationAnchor a@(EmbTyPat _ _ _) _ _s = a
exact (WildPat w) = do
anchor <- getAnchorU
@@ -4665,6 +4669,11 @@ instance ExactPrint (Pat GhcPs) where
sig' <- markAnnotated sig
return (SigPat an0 pat' sig')
+ exact (EmbTyPat x toktype tp) = do
+ toktype' <- markToken toktype
+ tp' <- markAnnotated tp
+ return (EmbTyPat x toktype' tp')
+
-- ---------------------------------------------------------------------
instance ExactPrint (HsPatSigType GhcPs) where