[Git][ghc/ghc][wip/sand-witch/types-in-terms] Simplify, add comments
Vladislav Zavialov (@int-index)
gitlab at gitlab.haskell.org
Wed Jul 31 21:50:01 UTC 2024
Vladislav Zavialov pushed to branch wip/sand-witch/types-in-terms at Glasgow Haskell Compiler / GHC
Commits:
ef0a33b8 by Vladislav Zavialov at 2024-08-01T00:49:29+03:00
Simplify, add comments
- - - - -
7 changed files:
- compiler/GHC/Hs/Expr.hs
- compiler/GHC/Parser/PostProcess.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Tc/Types/Origin.hs
- compiler/GHC/ThToHs.hs
- compiler/Language/Haskell/Syntax/Expr.hs
- compiler/Language/Haskell/Syntax/Extension.hs
Changes:
=====================================
compiler/GHC/Hs/Expr.hs
=====================================
@@ -381,14 +381,14 @@ type instance XEmbTy GhcTc = DataConCantHappen
-- A free-standing HsEmbTy is an error.
-- Valid usages are immediately desugared into Type.
-type instance XQual GhcPs = NoExtField
-type instance XQual GhcRn = NoExtField
-type instance XQual GhcTc = DataConCantHappen
-
type instance XForAll GhcPs = NoExtField
type instance XForAll GhcRn = NoExtField
type instance XForAll GhcTc = DataConCantHappen
+type instance XQual GhcPs = NoExtField
+type instance XQual GhcRn = NoExtField
+type instance XQual GhcTc = DataConCantHappen
+
type instance XFunArr GhcPs = NoExtField
type instance XFunArr GhcRn = NoExtField
type instance XFunArr GhcTc = DataConCantHappen
=====================================
compiler/GHC/Parser/PostProcess.hs
=====================================
@@ -107,7 +107,7 @@ module GHC.Parser.PostProcess (
ecpFromPat,
ArrowParsingMode(..),
withArrowParsingMode, withArrowParsingMode',
- setTelescopeBndrsNamespace,
+ setTelescopeBndrsNameSpace,
PatBuilder,
hsHoleExpr,
@@ -844,7 +844,8 @@ mkGadtDecl loc names dcol ty = do
setRdrNameSpace :: RdrName -> NameSpace -> RdrName
-- ^ This rather gruesome function is used mainly by the parser.
--- When parsing:
+--
+-- Case #1. When parsing:
--
-- > data T a = T | T1 Int
--
@@ -856,6 +857,13 @@ setRdrNameSpace :: RdrName -> NameSpace -> RdrName
-- > data [] a = [] | a : [a]
--
-- For the exact-name case we return an original name.
+--
+-- Case #2. When parsing:
+--
+-- > x = fn (forall a. a) -- RequiredTypeArguments
+--
+-- we use setRdrNameSpace to set the namespace of forall-bound variables.
+--
setRdrNameSpace (Unqual occ) ns = Unqual (setOccNameSpace ns occ)
setRdrNameSpace (Qual m occ) ns = Qual m (setOccNameSpace ns occ)
setRdrNameSpace (Orig m occ) ns = Orig m (setOccNameSpace ns occ)
@@ -1984,7 +1992,7 @@ instance DisambECP (HsExpr GhcPs) where
return $ mkMultExpr pct t
mkHsForallPV l telescope ty =
return $ L (noAnnSrcSpan l) $
- HsForAll noExtField (setTelescopeBndrsNamespace varName telescope) ty
+ HsForAll noExtField (setTelescopeBndrsNameSpace varName telescope) ty
checkContextPV = checkContextExpr
mkQualPV l qual ty =
return $ L (noAnnSrcSpan l) $
@@ -2143,9 +2151,11 @@ This depends on the enabled extensions:
ViewPatterns, RequiredTypeArguments => view pattern
ViewPatterns, NoRequiredTypeArguments => view pattern
-The decision how to parse the arrow pattern is captured by the
-`ArrowParsingMode` data type. Naively, one might expect to see the following
-definition:
+The decision how to parse arrow patterns (p1 -> p2) is captured by the
+`ArrowParsingMode` data type, produced in `withArrowParsingMode` and
+consumed in `mkHsArrowPV`.
+
+Naively, one might expect to see the following definition:
-- a simple (but insufficient) definition
data ArrowParsingMode = ArrowIsViewPat | ArrowIsFunType
@@ -2208,18 +2218,27 @@ withArrowParsingMode cont = do
withArrowParsingMode' :: DisambECP b => (forall lhs. DisambECP lhs => ArrowParsingMode lhs b -> PV (LocatedA b)) -> PV (LocatedA b)
withArrowParsingMode' = withArrowParsingMode
-setTelescopeBndrsNamespace :: NameSpace -> HsForAllTelescope GhcPs -> HsForAllTelescope GhcPs
-setTelescopeBndrsNamespace ns forall_telescope = case forall_telescope of
- HsForAllInvis x invis_bndrs -> HsForAllInvis x (map set_bndr_ns invis_bndrs)
- HsForAllVis x vis_bndrs -> HsForAllVis x (map set_bndr_ns vis_bndrs)
+-- When a forall-type occurs in term syntax, forall-bound variables should
+-- inhabit the term namespace `varName` rather than the usual `tvName`.
+-- See Note [Types in terms].
+--
+-- Since type variable binders in a `HsForAllTelescope` produced by the
+-- `forall_telescope` nonterminal have their namespaces set to `tvName`,
+-- we use `setTelescopeBndrsNameSpace` to fix them up.
+setTelescopeBndrsNameSpace :: NameSpace -> HsForAllTelescope GhcPs -> HsForAllTelescope GhcPs
+setTelescopeBndrsNameSpace ns forall_telescope =
+ case forall_telescope of
+ HsForAllInvis x bndrs -> HsForAllInvis x (map set_bndr_ns bndrs)
+ HsForAllVis x bndrs -> HsForAllVis x (map set_bndr_ns bndrs)
where
set_bndr_ns :: LHsTyVarBndr flag GhcPs -> LHsTyVarBndr flag GhcPs
- set_bndr_ns (L l bndr) = L l $ case bndr of
- UserTyVar x flag rdr -> UserTyVar x flag (set_rdr_ns rdr)
- KindedTyVar x flag rdr kind -> KindedTyVar x flag (set_rdr_ns rdr) kind
+ set_bndr_ns (L l bndr) =
+ L l $ case bndr of
+ UserTyVar x flag rdr -> UserTyVar x flag (set_rdr_ns rdr)
+ KindedTyVar x flag rdr kind -> KindedTyVar x flag (set_rdr_ns rdr) kind
- set_rdr_ns (L l (Unqual occ)) = L l (Unqual occ{occNameSpace = ns})
- set_rdr_ns rdr = rdr
+ set_rdr_ns :: LocatedN RdrName -> LocatedN RdrName
+ set_rdr_ns (L l rdr) = L l (setRdrNameSpace rdr ns)
-- | Ensure that a literal pattern isn't of type Addr#, Float#, Double#.
checkUnboxedLitPat :: Located (HsLit GhcPs) -> PV ()
=====================================
compiler/GHC/Tc/Errors/Types.hs
=====================================
@@ -6812,11 +6812,13 @@ data TcRnNoDerivStratSpecifiedInfo where
-> LHsSigWcType GhcRn -- ^ The instance signature (e.g @Show a => Show (T a)@)
-> TcRnNoDerivStratSpecifiedInfo
+-- | Label for syntax that may occur in terms (expressions) only as part of a
+-- required type argument.
data TypeSyntax
- = TypeKeywordSyntax
- | ContextArrowSyntax
- | FunctionArrowSyntax
- | ForallTelescopeSyntax
+ = TypeKeywordSyntax -- ^ @type t@
+ | ContextArrowSyntax -- ^ @ctx => t@
+ | FunctionArrowSyntax -- ^ @t1 -> t2@
+ | ForallTelescopeSyntax -- ^ @forall tvs. t@
deriving Generic
typeSyntaxExtension :: TypeSyntax -> LangExt.Extension
=====================================
compiler/GHC/Tc/Types/Origin.hs
=====================================
@@ -751,9 +751,9 @@ 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 (HsQual {}) = Shouldn'tHappenOrigin "constraint context"
-exprCtOrigin (HsForAll {}) = Shouldn'tHappenOrigin "forall telescope"
-exprCtOrigin (HsFunArr {}) = Shouldn'tHappenOrigin "function arrow"
+exprCtOrigin (HsForAll {}) = Shouldn'tHappenOrigin "forall telescope" -- See Note [Types in terms]
+exprCtOrigin (HsQual {}) = Shouldn'tHappenOrigin "constraint context" -- See Note [Types in terms]
+exprCtOrigin (HsFunArr {}) = Shouldn'tHappenOrigin "function arrow" -- See Note [Types in terms]
exprCtOrigin (XExpr (ExpandedThingRn thing _)) | OrigExpr a <- thing = exprCtOrigin a
| OrigStmt _ <- thing = DoOrigin
| OrigPat p <- thing = DoPatOrigin p
=====================================
compiler/GHC/ThToHs.hs
=====================================
@@ -1187,16 +1187,18 @@ cvtl e = wrapLA (cvt e)
cvt (ConstrainedE ctx body) = do { ctx' <- mapM cvtl ctx
; body' <- cvtl body
; return $ HsQual noExtField (L noAnn ctx') body' }
- cvt exp
- | ForallE tvs body <- exp = forall_builder tvs body mkHsForAllInvisTele
- | ForallVisE tvs body <- exp = forall_builder tvs body mkHsForAllVisTele
- where
- forall_builder tvs body build_forall_tele
- = do { tvs' <- cvtTvs tvs
- ; body' <- cvtl body
- ; let tele = setTelescopeBndrsNamespace varName $
- build_forall_tele noAnn tvs'
- ; return $ HsForAll noExtField tele body'}
+ cvt (ForallE tvs body) =
+ do { tvs' <- cvtTvs tvs
+ ; body' <- cvtl body
+ ; let tele = setTelescopeBndrsNameSpace varName $
+ mkHsForAllInvisTele noAnn tvs'
+ ; return $ HsForAll noExtField tele body' }
+ cvt (ForallVisE tvs body) =
+ do { tvs' <- cvtTvs tvs
+ ; body' <- cvtl body
+ ; let tele = setTelescopeBndrsNameSpace varName $
+ mkHsForAllVisTele noAnn tvs'
+ ; return $ HsForAll noExtField tele body' }
{- | #16895 Ensure an infix expression's operator is a variable/constructor.
Consider this example:
=====================================
compiler/Language/Haskell/Syntax/Expr.hs
=====================================
@@ -260,6 +260,80 @@ extension field, The typechecker keeps HsRecSel as HsRecSel, and
transforms the record-selector Name to an Id.
-}
+{- Note [Types in terms]
+~~~~~~~~~~~~~~~~~~~~~~~~
+Types-in-terms is a notion introduced by GHC Proposal #281. It refers
+to the extension of term syntax (HsExpr in the AST, infixexp2 in Parser.y)
+with constructs that previously could only occur at the type level:
+
+ * Function arrows: a -> b
+ * Multiplicity-polymorphic function arrows: a %m -> b (LinearTypes)
+ * Constraint arrows: a => b
+ * Universal quantification: forall a. b
+ * Visible universal quantification: forall a -> b
+
+This syntax can't be used to construct a type at the term level because `Type`
+is not inhabited by any terms. Its use is limited to required type arguments:
+
+ -- Error:
+ t :: Type
+ t = (Int -> String)
+ -- Not supported by GHC, `tcExpr` emits `TcRnIllegalTypeExpr`
+
+ -- OK:
+ s :: String
+ s = vfun (Int -> String)
+ -- Valid use in a required type argument,
+ -- see `expr_to_type` (GHC.Tc.Gen.App)
+ where
+ vfun :: forall t -> Typeable t => String
+ vfun t = show (typeRep @t)
+
+In GHC, types-in-terms are implemented by the following additions to the AST of
+expressions and their grammar:
+
+ -- Language/Haskell/Syntax/Expr.hs
+ data HsExpr p =
+ ...
+ | HsForAll (XForAll p) (HsForAllTelescope p) (LHsExpr p)
+ | HsQual (XQual p) (XRec p [LHsExpr p]) (LHsExpr p)
+ | HsFunArr (XFunArr p) (HsArrowOf (LHsExpr p) p) (LHsExpr p) (LHsExpr p)
+
+ -- GHC/Parser.y
+ infixexp2 :: { ECP }
+ : infixexp %shift { ... }
+ | infixexp '->' infixexp2 { ... }
+ | infixexp expmult '->' infixexp2 { ... }
+ | infixexp '->.' infixexp2 { ... }
+ | expcontext '=>' infixexp2 { ... }
+ | forall_telescope infixexp2 { ... }
+
+These constructors and non-terminals mirror those found in HsType
+
+ HsType | HsExpr
+ -------------+-----------
+ HsForAllTy | HsForAll
+ HsFunTy | HsQual
+ HsQualTy | HsFunArr
+
+The resulting code duplication can be removed if we unify HsExpr and HsType
+into one type (#25121).
+
+Per the proposal, the constituents of types-in-terms are parsed and renamed
+as terms, and forall-bound variables inhabit the term namespace. Example:
+
+ h = \a -> g (forall a. Maybe a) a
+
+To ensure that the `a` in `Maybe a` refers to the innermost binding (i.e. to the
+forall-bound `a` and not to the lambda-bound `a`), we must consistently use the
+term namespace `varName` throughout the expression. We set the correct namespace
+using `setTelescopeBndrsNameSpace` in GHC.Parser.PostProcess and GHC.ThToHs.
+
+`exprCtOrigin` returns `Shouldn'tHappenOrigin` for types-in-terms because
+they either undergo the T2T translation `expr_to_type` in `tcVDQ` or result
+in `TcRnIllegalTypeExpr`.
+-}
+
-- | A Haskell expression.
data HsExpr p
= HsVar (XVar p)
@@ -574,14 +648,23 @@ data HsExpr p
| HsPragE (XPragE p) (HsPragE p) (LHsExpr p)
-- Embed the syntax of types into expressions.
- -- Used with RequiredTypeArguments, e.g. fn (type (Int -> Bool))
+ -- Used with @RequiredTypeArguments@, e.g. @fn (type (Int -> Bool))@.
| HsEmbTy (XEmbTy p)
(LHsWcType (NoGhcTc p))
- | HsQual (XQual p) (XRec p [LHsExpr p]) (LHsExpr p)
-
+ -- | Forall-types @forall tvs. t@ and @forall tvs -> t at .
+ -- Used with @RequiredTypeArguments@, e.g. @fn (forall a. Proxy a)@.
+ -- See Note [Types in terms]
| HsForAll (XForAll p) (HsForAllTelescope p) (LHsExpr p)
+ -- Constrained types @ctx => t at .
+ -- Used with @RequiredTypeArguments@, e.g. @fn (Bounded a => a)@.
+ -- See Note [Types in terms]
+ | HsQual (XQual p) (XRec p [LHsExpr p]) (LHsExpr p)
+
+ -- | Function types @a -> b at .
+ -- Used with @RequiredTypeArguments@, e.g. @fn (Int -> Bool)@.
+ -- See Note [Types in terms]
| HsFunArr (XFunArr p) (HsArrowOf (LHsExpr p) p) (LHsExpr p) (LHsExpr p)
| XExpr !(XXExpr p)
=====================================
compiler/Language/Haskell/Syntax/Extension.hs
=====================================
@@ -448,8 +448,8 @@ type family XTick x
type family XBinTick x
type family XPragE x
type family XEmbTy x
-type family XQual x
type family XForAll x
+type family XQual x
type family XFunArr x
type family XXExpr x
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ef0a33b84666ba8610dc2809ef0cd23f6486cdaf
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ef0a33b84666ba8610dc2809ef0cd23f6486cdaf
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20240731/6ddf7869/attachment-0001.html>
More information about the ghc-commits
mailing list