[Git][ghc/ghc][wip/int-index/emb-type] VDQ-related Notes
Vladislav Zavialov (@int-index)
gitlab at gitlab.haskell.org
Fri Jul 21 02:05:33 UTC 2023
Vladislav Zavialov pushed to branch wip/int-index/emb-type at Glasgow Haskell Compiler / GHC
Commits:
0bf33f76 by Vladislav Zavialov at 2023-07-21T04:05:09+02:00
VDQ-related Notes
- - - - -
4 changed files:
- compiler/GHC/Core/DataCon.hs
- compiler/GHC/Core/TyCon.hs
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Types/Var.hs
Changes:
=====================================
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
=====================================
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.
-}
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -791,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.
--
@@ -804,15 +805,13 @@ 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
@@ -875,27 +874,235 @@ tc_inst_forall_arg conc_tvs (tvb, inner_ty) hs_ty
, text "insted_ty" <+> debugPprType insted_ty ])
; return (ty_arg, insted_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.
-
-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
+
+The proposals have not been fully implemented at the time of writing this Note,
+so we offer an overview of the design mixed with commentary on the implementation status.
+
+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).
+ 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,
+ the types have been desugared 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
+----------------------
+* Type applications are represented with the following constructors
+ f True -- HsApp (c.o. HsExpr, plain function application)
+ f @True -- HsAppType (c.o. HsExpr, function application with `@`)
+ type True -- HsEmbTy (c.o. HsExpr, embed a type into an expression with `type`)
+
+* The HsAppType constructor is only used with Specified type variables
+ f @True -- only valid for f :: forall a. t
+
+* 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)
+
+* The HsApp constructor with an HsEmbTy argument is only used
+ with Required type variables
+ f (type True) -- valid for f :: forall (a :: Bool) -> t
+
+ 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 `@`.
+
+Syntax of abstractions
+----------------------
+* Type abstractions are represented with the following constructors
+ \ (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:
+ \ (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)
+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.
+
+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. (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 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 ->
+ ]
+
+This 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]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [VTA for out-of-scope functions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose 'wurble' is not in scope, and we have
(wurble @Int @Bool True 'x')
=====================================
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.
-}
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0bf33f76357b046cb047cef6a5bbce9f9433550e
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0bf33f76357b046cb047cef6a5bbce9f9433550e
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/20230720/e9ecc119/attachment-0001.html>
More information about the ghc-commits
mailing list