Vladislav Zavialov pushed to branch wip/int-index/visible-forall-gadts at Glasgow Haskell Compiler / GHC

Commits:

3 changed files:

Changes:

  • compiler/GHC/Core/DataCon.hs
    ... ... @@ -642,12 +642,17 @@ Note [DataCon user type variable binders]
    642 642 
     A DataCon has two different sets of type variables:
    643 643
    644 644 
     * dcUserTyVarBinders, for the type variables binders in the order in which they
    645 
    -  originally arose in the user-written type signature.
    645 
    +  originally arose in the user-written type signature, and with user-specified
    646 
    +  visibilities.
    646 647
    647 648 
       - They are the forall'd binders of the data con /wrapper/, which the user calls.
    648 649
    649 
    -  - Their order *does* matter for TypeApplications, so they are full TyVarBinders,
    650 
    -    complete with visibilities.
    650 
    +  - With RequiredTypeArguments, some of the foralls may be visible, e.g.
    651 
    +      MkT :: forall a b. forall c -> (a, b, c) -> T a b c
    652 
    +    so the binders are full TyVarBinders, complete with visibilities.
    653 
    +
    654 
    +  - Even if we only consider invisible foralls, the order and specificity of
    655 
    +    binders matter for TypeApplications.
    651 656
    652 657 
     * dcUnivTyVars and dcExTyCoVars, for the "true underlying" (i.e. of the data
    653 658 
       con worker) universal type variable and existential type/coercion variables,
    ... ... @@ -659,8 +664,8 @@ A DataCon has two different sets of type variables:
    659 664 
         and as a consequence, they do not come equipped with visibilities
    660 665 
         (that is, they are TyVars/TyCoVars instead of ForAllTyBinders).
    661 666
    662 
    -Often (dcUnivTyVars ++ dcExTyCoVars) = dcUserTyVarBinders; but they may differ
    663 
    -for two reasons, coming next:
    667 
    +Often (dcUnivTyVars ++ dcExTyCoVars) = binderVars dcUserTyVarBinders; but they
    668 
    +may differ for two reasons, coming next:
    664 669
    665 670 
     --- Reason (R1): Order of quantification in GADT syntax ---
    666 671

  • docs/users_guide/exts/gadt_syntax.rst
    ... ... @@ -124,19 +124,26 @@ grammar is subject to change in the future.
    124 124
    125 125 
     .. code-block:: none
    126 126
    127 
    -  gadt_con ::= conids '::' opt_forall opt_ctxt gadt_body
    127 
    +  gadt_con ::= conids '::' foralls opt_ctxt gadt_body
    128 128
    129 129 
       conids ::= conid
    130 130 
               |  conid ',' conids
    131 131
    132 
    -  opt_forall ::= <empty>
    133 
    -              |  'forall' tv_bndrs '.'
    132 
    +  foralls ::= <empty>
    133 
    +           | forall_telescope foralls
    134 134
    135 
    -  tv_bndrs ::= <empty>
    136 
    -            |  tv_bndr tv_bndrs
    135 
    +  forall_telescope ::= 'forall' tv_bndrs_spec '.'
    136 
    +                    |  'forall' tv_bndrs      '->'   -- with RequiredTypeArguments
    137 137
    138 
    -  tv_bndr ::= tyvar
    139 
    -           |  '(' tyvar '::' ctype ')'
    138 
    +  tv_bndrs      ::= <empty> | tv_bndr      tv_bndrs
    139 
    +  tv_bndrs_spec ::= <empty> | tv_bndr_spec tv_bndrs_spec
    140 
    +
    141 
    +  tv_bndr       ::= tyvar
    142 
    +                 |  '(' tyvar '::' ctype ')'
    143 
    +
    144 
    +  tv_bndr_spec  ::= tv_bndr
    145 
    +                 |  '{' tyvar '}'
    146 
    +                 |  '{' tyvar '::' ctype '}'
    140 147
    141 148 
       opt_ctxt ::= <empty>
    142 149 
                 |  btype '=>'
    ... ... @@ -162,7 +169,7 @@ grammar is subject to change in the future.
    162 169 
                   |  fieldname ',' fieldnames
    163 170
    164 171 
       opt_unpack ::= opt_bang
    165 
    -              :  {-# UNPACK #-} opt_bang
    172 
    +              |  {-# UNPACK #-} opt_bang
    166 173 
                   |  {-# NOUNPACK #-} opt_bang
    167 174
    168 175 
       opt_bang ::= <empty>
    ... ... @@ -188,22 +195,25 @@ syntactically allowed. Some further various observations about this grammar:
    188 195 
     - GADT constructor types are currently not permitted to have nested ``forall``\ s
    189 196 
       or ``=>``\ s. (e.g., something like ``MkT :: Int -> forall a. a -> T`` would be
    190 197 
       rejected.) As a result, ``gadt_sig`` puts all of its quantification and
    191 
    -  constraints up front with ``opt_forall`` and ``opt_context``. Note that
    198 
    +  constraints up front with ``foralls`` and ``opt_context``. Note that
    192 199 
       higher-rank ``forall``\ s and ``=>``\ s are only permitted if they do not appear
    193 200 
       directly to the right of a function arrow in a `prefix_gadt_body`. (e.g.,
    194 201 
       something like ``MkS :: Int -> (forall a. a) -> S`` is allowed, since
    195 202 
       parentheses separate the ``forall`` from the ``->``.)
    203 
    +
    196 204 
     - Furthermore, GADT constructors do not permit outermost parentheses that
    197 
    -  surround the ``opt_forall`` or ``opt_ctxt``, if at least one of them are
    205 
    +  surround the ``foralls`` or ``opt_ctxt``, if at least one of them are
    198 206 
       used. For example, ``MkU :: (forall a. a -> U)`` would be rejected, since
    199 207 
       it would treat the ``forall`` as being nested.
    200 208
    201 209 
       Note that it is acceptable to use parentheses in a ``prefix_gadt_body``.
    202 210 
       For instance, ``MkV1 :: forall a. (a) -> (V1)`` is acceptable, as is
    203 211 
       ``MkV2 :: forall a. (a -> V2)``.
    212 
    +
    204 213 
     - The function arrows in a ``prefix_gadt_body``, as well as the function
    205 214 
       arrow in a ``record_gadt_body``, are required to be used infix. For
    206 215 
       example, ``MkA :: (->) Int A`` would be rejected.
    216 
    +
    207 217 
     - GHC uses the function arrows in a ``prefix_gadt_body`` and
    208 218 
       ``prefix_gadt_body`` to syntactically demarcate the function and result
    209 219 
       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:
    224 234
    225 235 
         data B where
    226 236 
           MkB :: B1 -> B2
    237 
    +
    227 238 
     - GHC will accept any combination of ``!``/``~`` and
    228 239 
       ``{-# UNPACK #-}``/``{-# NOUNPACK #-}``, although GHC will ignore some
    229 240 
       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.
    427 427 
     The :extension:`RequiredTypeArguments` extension does not add dependent
    428 428 
     functions, which would be a much bigger step. Rather :extension:`RequiredTypeArguments`
    429 429 
     just makes it possible for the type arguments of a function to be compulsory.
    430 
    +
    431 
    +Visible forall in GADTs
    432 
    +~~~~~~~~~~~~~~~~~~~~~~~
    433 
    +
    434 
    +**Since:** GHC 9.14
    435 
    +
    436 
    +When :extension:`RequiredTypeArguments` is in effect, the use of ``forall a ->``
    437 
    +in data constructor declarations is allowed: ::
    438 
    +
    439 
    +  data T a where
    440 
    +    Typed :: forall a -> a -> T a
    441 
    +
    442 
    +There are no restrictions placed on the flavour of the parent declaration:
    443 
    +the data constructor may be introduced as part of a ``data``, ``data instance``,
    444 
    +``newtype``, or ``newtype instance`` declaration.
    445 
    +
    446 
    +The use of visible forall in the type of a data constructor imposes no
    447 
    +restrictions on where the data constructor may occur.  Examples:
    448 
    +
    449 
    +* in expressions ::
    450 
    +
    451 
    +      t1 = Typed Int 42
    452 
    +      t2 = Typed String "hello"
    453 
    +      t3 = Typed (Int -> Bool) even
    454 
    +
    455 
    +* in patterns ::
    456 
    +
    457 
    +      f1 (Typed a x) = x :: a
    458 
    +      f2 (Typed Int n) = n*2
    459 
    +      f3 (Typed ((->) w Bool) g) = not . g
    460 
    +
    461 
    +* in types (with :extension:`DataKinds`) ::
    462 
    +
    463 
    +      type T1 = Typed Nat 42
    464 
    +      type T2 = Typed Symbol "hello"
    465 
    +      type T3 = Typed (Type -> Constraint) Num
    466 
    +
    467 
    +At the moment, all foralls in the type of a data constructor (including visible
    468 
    +foralls) must occur before constraints or value arguments: ::
    469 
    +
    470 
    +  data D x where
    471 
    +    -- OK (one forall at the front of the type)
    472 
    +    MkD1 :: forall a b ->
    473 
    +            a ->
    474 
    +            b ->
    475 
    +            D (a, b)
    476 
    +
    477 
    +    -- OK (multpile foralls at the front of the type)
    478 
    +    MkD2 :: forall a.
    479 
    +            forall b ->
    480 
    +            a ->
    481 
    +            b ->
    482 
    +            D (a, b)
    483 
    +
    484 
    +    -- Rejected (forall after a value argument)
    485 
    +    MkD3 :: forall a ->
    486 
    +            a ->
    487 
    +            forall b ->
    488 
    +            b ->
    489 
    +            D (a, b)
    490 
    +
    491 
    +This restriction is intended to be lifted in the future (:ghc-ticket:`18389`).
    492 
    +
    493 
    +The use of visible forall instead of invisible forall has no effect on how data
    494 
    +is represented on the heap.

    • —
    View it on GitLab.
    You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications · Help