Vladislav Zavialov pushed to branch wip/int-index/visible-forall-gadts at Glasgow Haskell Compiler / GHC Commits: 1c4190ad by Vladislav Zavialov at 2025-06-10T01:13:41+03:00 Update documentation and comments - - - - - 3 changed files: - compiler/GHC/Core/DataCon.hs - docs/users_guide/exts/gadt_syntax.rst - docs/users_guide/exts/required_type_arguments.rst Changes: ===================================== compiler/GHC/Core/DataCon.hs ===================================== @@ -642,12 +642,17 @@ Note [DataCon user type variable binders] A DataCon has two different sets of type variables: * dcUserTyVarBinders, for the type variables binders in the order in which they - originally arose in the user-written type signature. + originally arose in the user-written type signature, and with user-specified + visibilities. - They are the forall'd binders of the data con /wrapper/, which the user calls. - - Their order *does* matter for TypeApplications, so they are full TyVarBinders, - complete with visibilities. + - With RequiredTypeArguments, some of the foralls may be visible, e.g. + MkT :: forall a b. forall c -> (a, b, c) -> T a b c + so the binders are full TyVarBinders, complete with visibilities. + + - Even if we only consider invisible foralls, the order and specificity of + binders matter for TypeApplications. * dcUnivTyVars and dcExTyCoVars, for the "true underlying" (i.e. of the data con worker) universal type variable and existential type/coercion variables, @@ -659,8 +664,8 @@ A DataCon has two different sets of type variables: and as a consequence, they do not come equipped with visibilities (that is, they are TyVars/TyCoVars instead of ForAllTyBinders). -Often (dcUnivTyVars ++ dcExTyCoVars) = dcUserTyVarBinders; but they may differ -for two reasons, coming next: +Often (dcUnivTyVars ++ dcExTyCoVars) = binderVars dcUserTyVarBinders; but they +may differ for two reasons, coming next: --- Reason (R1): Order of quantification in GADT syntax --- ===================================== docs/users_guide/exts/gadt_syntax.rst ===================================== @@ -124,19 +124,26 @@ grammar is subject to change in the future. .. code-block:: none - gadt_con ::= conids '::' opt_forall opt_ctxt gadt_body + gadt_con ::= conids '::' foralls opt_ctxt gadt_body conids ::= conid | conid ',' conids - opt_forall ::= <empty> - | 'forall' tv_bndrs '.' + foralls ::= <empty> + | forall_telescope foralls - tv_bndrs ::= <empty> - | tv_bndr tv_bndrs + forall_telescope ::= 'forall' tv_bndrs_spec '.' + | 'forall' tv_bndrs '->' -- with RequiredTypeArguments - tv_bndr ::= tyvar - | '(' tyvar '::' ctype ')' + tv_bndrs ::= <empty> | tv_bndr tv_bndrs + tv_bndrs_spec ::= <empty> | tv_bndr_spec tv_bndrs_spec + + tv_bndr ::= tyvar + | '(' tyvar '::' ctype ')' + + tv_bndr_spec ::= tv_bndr + | '{' tyvar '}' + | '{' tyvar '::' ctype '}' opt_ctxt ::= <empty> | btype '=>' @@ -162,7 +169,7 @@ grammar is subject to change in the future. | fieldname ',' fieldnames opt_unpack ::= opt_bang - : {-# UNPACK #-} opt_bang + | {-# UNPACK #-} opt_bang | {-# NOUNPACK #-} opt_bang opt_bang ::= <empty> @@ -188,22 +195,25 @@ syntactically allowed. Some further various observations about this grammar: - GADT constructor types are currently not permitted to have nested ``forall``\ s or ``=>``\ s. (e.g., something like ``MkT :: Int -> forall a. a -> T`` would be rejected.) As a result, ``gadt_sig`` puts all of its quantification and - constraints up front with ``opt_forall`` and ``opt_context``. Note that + constraints up front with ``foralls`` and ``opt_context``. Note that higher-rank ``forall``\ s and ``=>``\ s are only permitted if they do not appear directly to the right of a function arrow in a `prefix_gadt_body`. (e.g., something like ``MkS :: Int -> (forall a. a) -> S`` is allowed, since parentheses separate the ``forall`` from the ``->``.) + - Furthermore, GADT constructors do not permit outermost parentheses that - surround the ``opt_forall`` or ``opt_ctxt``, if at least one of them are + surround the ``foralls`` or ``opt_ctxt``, if at least one of them are used. For example, ``MkU :: (forall a. a -> U)`` would be rejected, since it would treat the ``forall`` as being nested. Note that it is acceptable to use parentheses in a ``prefix_gadt_body``. For instance, ``MkV1 :: forall a. (a) -> (V1)`` is acceptable, as is ``MkV2 :: forall a. (a -> V2)``. + - The function arrows in a ``prefix_gadt_body``, as well as the function arrow in a ``record_gadt_body``, are required to be used infix. For example, ``MkA :: (->) Int A`` would be rejected. + - GHC uses the function arrows in a ``prefix_gadt_body`` and ``prefix_gadt_body`` to syntactically demarcate the function and result types. Note that GHC does not attempt to be clever about looking through @@ -224,6 +234,7 @@ syntactically allowed. Some further various observations about this grammar: data B where MkB :: B1 -> B2 + - GHC will accept any combination of ``!``/``~`` and ``{-# UNPACK #-}``/``{-# NOUNPACK #-}``, although GHC will ignore some combinations. For example, GHC will produce a warning if you write ===================================== docs/users_guide/exts/required_type_arguments.rst ===================================== @@ -427,3 +427,68 @@ coming from dependently-typed languages or proof assistants. The :extension:`RequiredTypeArguments` extension does not add dependent functions, which would be a much bigger step. Rather :extension:`RequiredTypeArguments` just makes it possible for the type arguments of a function to be compulsory. + +Visible forall in GADTs +~~~~~~~~~~~~~~~~~~~~~~~ + +**Since:** GHC 9.14 + +When :extension:`RequiredTypeArguments` is in effect, the use of ``forall a ->`` +in data constructor declarations is allowed: :: + + data T a where + Typed :: forall a -> a -> T a + +There are no restrictions placed on the flavour of the parent declaration: +the data constructor may be introduced as part of a ``data``, ``data instance``, +``newtype``, or ``newtype instance`` declaration. + +The use of visible forall in the type of a data constructor imposes no +restrictions on where the data constructor may occur. Examples: + +* in expressions :: + + t1 = Typed Int 42 + t2 = Typed String "hello" + t3 = Typed (Int -> Bool) even + +* in patterns :: + + f1 (Typed a x) = x :: a + f2 (Typed Int n) = n*2 + f3 (Typed ((->) w Bool) g) = not . g + +* in types (with :extension:`DataKinds`) :: + + type T1 = Typed Nat 42 + type T2 = Typed Symbol "hello" + type T3 = Typed (Type -> Constraint) Num + +At the moment, all foralls in the type of a data constructor (including visible +foralls) must occur before constraints or value arguments: :: + + data D x where + -- OK (one forall at the front of the type) + MkD1 :: forall a b -> + a -> + b -> + D (a, b) + + -- OK (multpile foralls at the front of the type) + MkD2 :: forall a. + forall b -> + a -> + b -> + D (a, b) + + -- Rejected (forall after a value argument) + MkD3 :: forall a -> + a -> + forall b -> + b -> + D (a, b) + +This restriction is intended to be lifted in the future (:ghc-ticket:`18389`). + +The use of visible forall instead of invisible forall has no effect on how data +is represented on the heap. View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1c4190ad44f5bd2624ac275cd4a630df... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1c4190ad44f5bd2624ac275cd4a630df... You're receiving this email because of your account on gitlab.haskell.org.