[Git][ghc/ghc][wip/int-index/emb-type] Further docs from Simon
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Fri Jul 21 16:19:20 UTC 2023
Simon Peyton Jones pushed to branch wip/int-index/emb-type at Glasgow Haskell Compiler / GHC
Commits:
0f660202 by Simon Peyton Jones at 2023-07-21T17:18:54+01:00
Further docs from Simon
- - - - -
5 changed files:
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Gen/Match.hs
- compiler/GHC/Tc/Gen/Pat.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
Changes:
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -955,48 +955,46 @@ Syntax of types
Syntax of applications in HsExpr
--------------------------------
-* We represent applications like this (ignoring parameterisation)
- data HsExpr = HsApp HsExpr HsExpr -- (f True) plain function application)
- | HsTyApp HsExpr HsType -- (f @True) function application with `@`)
- | HsEmbType HsType -- (type ty) embed a type into an expression with `type`)
+* 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 `@`)
+ | HsEmbType HsType -- (type ty) embed a type into an expression with `type`)
+ | ...
-* The HsAppType constructor is only used for Specified type variables
- f @True -- only valid for f :: forall a. t
+* So (f @ty) is represented, just as you might expect:
+ HsAppType f ty
-* The HsApp constructor without HsEmbTy is used with ordinary function application
- and with Required type variables
- f True -- valid for f :: Bool -> t
- -- and f :: forall (a :: Bool) -> t (NB. not implemented)
+* But (f (type ty)) is represented by:
+ HsApp f (HsEmbType ty)
-* The HsApp constructor with an HsEmbTy argument is only used
- with Required type variables
- f (type True) -- valid for f :: forall (a :: Bool) -> t
+ Why the difference? Because we /also/ need to express these /nested/ uses of `type`:
- The HsEmbTy node can occur nested inside a larger type argument,
- or even multiple times
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 `@`.
- The HsEmbTy mainly just switches name-space, and affects the term-to-type transformation.
+ This nesting makes `type` rather different from `@`. Remember, the HsEmbTy mainly just
+ switches name-space, and affects the term-to-type transformation.
Syntax of abstractions in Pat
-----------------------------
-similary...
+* Type patterns are represented in HsPat roughly like this
+ data HsPat = ConPat ConLike [HsTyPat] [HsPat]
+ | EmbPat HsTyPat
+ | ...
+ data HsTyPat = HsTP LHsType
+ (In ConPat, the type and term arguments are actually inside HsConPatDetails.)
+ * Similar to HsTypeApp in HsExpr, the [HsTyPat] in ConPat is used just for @ty arguments
+ * Similar to HsEmbType in HsSxpr, EmbPat lets you embed a type in a pattern
-data HsPat = ConPat [HsTyPat] [HsPat]
-
- | EmbPat HsTyPat
-
-* Type abstractions are represented with the following constructors
+* 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)
-* The type pattern itself is not necessarily a plain variable. At the very least,
- we support kind signatures and wildcards:
+* A HsTyPat is not necessarily a plain variable. At the very least,
+l we support kind signatures and wildcards:
\ (type _) -> rhs
\ (type (b :: Bool)) -> rhs
\ (type (_ :: Bool)) -> rhs
@@ -1004,8 +1002,6 @@ data HsPat = ConPat [HsTyPat] [HsPat]
\ (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:
@@ -1014,13 +1010,11 @@ rnExpr delegates renaming of type arguments to rnHsWcType if possible:
But what about:
f t -- HsApp, no HsEmbTy (NB. not implemented)
-Is `t` a term argument or a type argument? This depends on f's type
- f :: A -> B -- t is a term argument
- f :: forall (a :: A) -> B -- t is a type argument
-But we don't want types to affect name resolution (Lexical Scoping Principle).
-So we always rename `t` as a term using a recursive call to rnExpr.
-The idea is to convert it to a type argument later. The details are spelled out
-in the "Resolved Syntax Tree" and "T2T-Mapping" sections of GHC Proposal #281.
+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
--------------------------
@@ -1032,8 +1026,9 @@ 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:
+to a type pattern later.
+
+One particularly prickly issue is that of implicit quantification. Consider:
f :: forall a -> ...
f t = ... -- binding site of `t`
@@ -1042,12 +1037,13 @@ implicit quantification. Consider:
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. (NB. not implemented)
+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
@@ -1070,36 +1066,42 @@ 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.
+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
+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.
+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 tcPats.
+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
+ * 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 ->
+ [ ExpForAllPatTy ... -- forall a ->
+ , ExpForAllPatTy ... -- forall b ->
, ExpFunPatTy ... -- a ->
, ExpFunPatTy ... -- b ->
]
-This allows us to use different code paths for type abstractions
+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.
+
+Teh [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)
@@ -1111,10 +1113,9 @@ This would allow us to support
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]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [VTA for out-of-scope functions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose 'wurble' is not in scope, and we have
(wurble @Int @Bool True 'x')
=====================================
compiler/GHC/Tc/Gen/Match.hs
=====================================
@@ -246,7 +246,7 @@ tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches
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
+ match_fun_pat_ty ExpForAllPatTy{} = Nothing
-------------
tcMatch :: (AnnoBody body) => TcMatchCtxt body
@@ -281,7 +281,7 @@ tcMatch ctxt pat_tys rhs_ty match
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
+ is_fun_pat_ty ExpForAllPatTy{} = False
-------------
tcGRHSs :: AnnoBody body
=====================================
compiler/GHC/Tc/Gen/Pat.hs
=====================================
@@ -387,7 +387,7 @@ 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_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
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -463,11 +463,11 @@ 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
+ | 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
+ ppr (ExpForAllPatTy tv) = text "forall" <+> ppr tv
{- *********************************************************************
* *
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -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,8 +404,14 @@ 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 Required, ty') <- splitForAllForAllTyBinder_maybe 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'
@@ -451,7 +457,7 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside
; let ty' = substTy subst' ty
; (ev_binds, (wrap_res, result)) <-
checkConstraints (getSkolemInfo skol_info) [tv'] [] $
- go (ExpForallPatTy tv' : acc_arg_tys) (n - 1) ty'
+ go (ExpForAllPatTy tv' : acc_arg_tys) (n - 1) ty'
; let wrap_gen = mkWpVisTyLam tv' ty' <.> mkWpLet ev_binds
; return (wrap_gen <.> wrap_res, result) }
@@ -481,7 +487,7 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside
where
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)
+ prepare_arg_ty (ExpForAllPatTy tv) = Named (Bndr tv Required)
-- this is safe b/c we're called from "go"
mkFunTysMsg :: TidyEnv
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0f6602026512b62a8a571a1fa662e850ab07669c
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0f6602026512b62a8a571a1fa662e850ab07669c
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/20230721/2578a5bc/attachment-0001.html>
More information about the ghc-commits
mailing list