diff options
author | Ryan Scott <ryan.gl.scott@gmail.com> | 2020-04-07 18:08:17 -0400 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2020-04-12 11:22:10 -0400 |
commit | 54ca66a7d30d7f7cfbf3753ebe547f5a20d76b96 (patch) | |
tree | af83038fc466f23590bc9c66964f42219fd8c8cd /docs | |
parent | 0efaf301fec9ed9ea827392cbe03de3335e995c7 (diff) | |
download | haskell-54ca66a7d30d7f7cfbf3753ebe547f5a20d76b96.tar.gz |
Use conLikeUserTyVarBinders to quantify field selector types
This patch:
1. Writes up a specification for how the types of top-level field
selectors should be determined in a new section of the GHC User's
Guide, and
2. Makes GHC actually implement that specification by using
`conLikeUserTyVarBinders` in `mkOneRecordSelector` to preserve the
order and specificity of type variables written by the user.
Fixes #18023.
Diffstat (limited to 'docs')
-rw-r--r-- | docs/users_guide/8.12.1-notes.rst | 30 | ||||
-rw-r--r-- | docs/users_guide/exts/existential_quantification.rst | 6 | ||||
-rw-r--r-- | docs/users_guide/exts/field_selectors_and_type_applications.rst | 122 | ||||
-rw-r--r-- | docs/users_guide/exts/gadt.rst | 3 | ||||
-rw-r--r-- | docs/users_guide/exts/rank_polymorphism.rst | 2 | ||||
-rw-r--r-- | docs/users_guide/exts/records.rst | 1 |
6 files changed, 162 insertions, 2 deletions
diff --git a/docs/users_guide/8.12.1-notes.rst b/docs/users_guide/8.12.1-notes.rst index 75adb1fb41..4d151d0ab1 100644 --- a/docs/users_guide/8.12.1-notes.rst +++ b/docs/users_guide/8.12.1-notes.rst @@ -18,6 +18,34 @@ Full details Language ~~~~~~~~ +* Record field selectors are now given type signatures that preserve the + user-written order of quantified type variables. Moreover, field selector + type signatures no longer make inferred type variables avaiable for explicit + type application. See :ref:`field-selectors-and-type-applications` for more + details. + + In certain situations, this will constitute a breaking change as this can + affect :extension:`TypeApplications`. For instance, given the following + definitions: :: + + {-# LANGUAGE PolyKinds #-} + + newtype P a = MkP { unP :: Proxy a } + + newtype N :: Type -> Type -> Type where + MkN :: forall b a. { unN :: Either a b } -> N a b + + Previous versions of GHC would give the following types to ``unP`` and + ``unN``: :: + + unP :: forall k (a :: k). P a -> Proxy a + unN :: forall a b. N a b -> Either a b + + GHC will now give them the following types instead: :: + + unP :: forall {k} (a :: k). P a -> Proxy a + unN :: forall b a. N a b -> Either a b + * In obscure scenarios, GHC now rejects programs it previously accepted, but with unhelpful types. For example, if (with ``-XPartialTypeSignatures``) you were to write ``x :: forall (f :: forall a (b :: a -> Type). b _). f _``, GHC previously @@ -40,7 +68,7 @@ Language There is a chance we will tweak the lookup scheme in the future, to make this workaround unnecessary. - + Compiler ~~~~~~~~ diff --git a/docs/users_guide/exts/existential_quantification.rst b/docs/users_guide/exts/existential_quantification.rst index e4c5a79149..c9cde919dd 100644 --- a/docs/users_guide/exts/existential_quantification.rst +++ b/docs/users_guide/exts/existential_quantification.rst @@ -116,7 +116,11 @@ example: :: } Here ``tag`` is a public field, with a well-typed selector function -``tag :: Counter a -> a``. The ``self`` type is hidden from the outside; +``tag :: Counter a -> a``. See :ref:`field-selectors-and-type-applications` +for a full description of how the types of top-level field selectors are +determined. + +The ``self`` type is hidden from the outside; any attempt to apply ``_this``, ``_inc`` or ``_display`` as functions will raise a compile-time error. In other words, *GHC defines a record selector function only for fields whose type does not mention the diff --git a/docs/users_guide/exts/field_selectors_and_type_applications.rst b/docs/users_guide/exts/field_selectors_and_type_applications.rst new file mode 100644 index 0000000000..c01e6ee519 --- /dev/null +++ b/docs/users_guide/exts/field_selectors_and_type_applications.rst @@ -0,0 +1,122 @@ +.. _field-selectors-and-type-applications: + +Field selectors and ``TypeApplications`` +---------------------------------------- + +Field selectors can be used in conjunction with :extension:`TypeApplications`, +as described in :ref:`visible-type-application`. The type of a field selector +is constructed by using the surrounding definition as context. This section +provides a specification for how this construction works. We will explain it +by considering three different forms of field selector, each of which is a +minor variation of the same general theme. + +Field selectors for Haskell98-style data constructors +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Consider the following example: :: + + data T a b = MkT { unT :: forall e. Either e a } + +This data type uses a Haskell98-style declaration. The only part of this data +type that is not Haskell98 code is ``unT``, whose type uses higher-rank +polymorphism (:ref:`arbitrary-rank-polymorphism`). To construct the type of +the ``unT`` field selector, we will assemble the following: + +1. The type variables quantified by the data type head + (``forall a b. <...>``). +2. The return type of the data constructor + (``<...> T a b -> <...>``). By virtue of this being a Haskell98-style + declaration, the order of type variables in the return type will always + coincide with the order in which they are quantified. +3. The type of the field + (``<...> forall e. Either e a``). + +The final type of ``unT`` is therefore +``forall a b. T a b -> forall e. Either e a``. As a result, one way to use +``unT`` with :extension:`TypeApplications` is +``unT @Int @Bool (MkT (Right 1)) @Char``. + +Field selectors for GADT constructors +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Field selectors for GADT constructors (:ref:`gadt-style`) are slightly more +involved. Consider the following example: :: + + data G a b where + MkG :: forall x n a. (Eq a, Show n) + => { unG1 :: forall e. Either e (a, x), unG2 :: n } -> G a (Maybe x) + +The ``MkG`` GADT constructor has two records, ``unG1`` and ``unG2``. +However, only ``unG1`` can be used as a top-level field selector. ``unG2`` +cannot because it is a "hidden" selector (see :ref:`existential-records`); its +type mentions a free variable ``n`` that does not appear in the result type +``G a (Maybe x)``. On the other hand, the only free type variables in the type +of ``unG1`` are ``a`` and ``x``, so ``unG1`` is fine to use as a top-level +function. + +To construct the type of the ``unG1`` field selector, we will assemble +the following: + +1. The subset of type variables quantified by the GADT constructor that are + mentioned in the return type. Note that the order of these variables follows + the same principles as in :ref:`ScopedSort`. + If the constructor explicitly quantifies its type variables at the beginning + of the type, then the field selector type will quantify them in the same + order (modulo any variables that are dropped due to not being mentioned in + the return type). + If the constructor implicitly quantifies its type variables, then the field + selector type will quantify them in the left-to-right order that they appear + in the field itself. + + In this example, ``MkG`` explicitly quantifies ``forall x n a.``, and of + those type variables, ``a`` and ``x`` are mentioned in the return type. + Therefore, the type of ``unG1`` starts as ``forall x a. <...>``. + If ``MkG`` had not used an explicit ``forall``, then they would have instead + been ordered as ``forall a x. <...>``, since ``a`` appears to the left of + ``x`` in the field type. +2. The GADT return type + (``<...> G a (Maybe x) -> ...``). +3. The type of the field + (``<...> -> forall e. Either e (a, x)``). + +The final type of ``unG1`` is therefore +``forall x a. G a (Maybe x) -> forall e. Either e (a, x)``. As a result, one +way to use ``unG1`` with :extension:`TypeApplications` is +``unG1 @Int @Bool (MkG (Right (True, 42)) ()) @Char``. + +Field selectors for pattern synonyms +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Certain record pattern synonyms (:ref:`record-patsyn`) can give rise to +top-level field selectors. Consider the following example: :: + + pattern P :: forall a. Read a + => forall n. (Eq a, Show n) + => (forall e. Either e (a, Bool)) -> n -> G a (Maybe Bool) + pattern P {unP1, unP2} = MkG unP1 unP2 + +We can only make field selectors for pattern synonym records that do not +mention any existential type variables whatsoever in their types, per +:ref:`record-patsyn`. (This is a stronger requirement than for GADT records, +whose types can mention existential type variables provided that they are also +mentioned in the return type.) We can see that ``unP2`` cannot be used as a +top-level field selector since its type has a free type variable ``n``, which +is existential. ``unP1`` is fine, on the other hand, as its type only has one +free variable, the universal type variable ``a``. + +To construct the type of the ``unP1`` field selector, we will assemble +the following: + +1. The universal type variables + (``forall a. <...>``). +2. The required constraints + (``<...> Read a => <...>``). +3. The pattern synonym return type + (``<...> G a (Maybe Bool) -> <...>``). +4. The type of the field + (``<...> -> forall e. Either e (a, Bool)``). + +The final type of ``unP1`` is therefore +``forall a. Read a => G a (Maybe Bool) -> forall e. Either e (a, Bool)``. As a +result, one way to use ``unP1`` with :extension:`TypeApplications` is +``unP1 @Double (MkG (Right (4.5, True)) ()) @Char``. diff --git a/docs/users_guide/exts/gadt.rst b/docs/users_guide/exts/gadt.rst index c8f0e750bd..388a055d28 100644 --- a/docs/users_guide/exts/gadt.rst +++ b/docs/users_guide/exts/gadt.rst @@ -118,6 +118,9 @@ also sets :extension:`GADTSyntax` and :extension:`MonoLocalBinds`. num :: Term Int -> Term Int arg :: Term Bool -> Term Int + See :ref:`field-selectors-and-type-applications` for a full description of + how the types of top-level field selectors are determined. + - When pattern-matching against data constructors drawn from a GADT, for example in a ``case`` expression, the following rules apply: diff --git a/docs/users_guide/exts/rank_polymorphism.rst b/docs/users_guide/exts/rank_polymorphism.rst index 3b33b01d7e..32447228c7 100644 --- a/docs/users_guide/exts/rank_polymorphism.rst +++ b/docs/users_guide/exts/rank_polymorphism.rst @@ -1,3 +1,5 @@ +.. _arbitrary-rank-polymorphism: + Arbitrary-rank polymorphism =========================== diff --git a/docs/users_guide/exts/records.rst b/docs/users_guide/exts/records.rst index 66c1b90c76..28f8988220 100644 --- a/docs/users_guide/exts/records.rst +++ b/docs/users_guide/exts/records.rst @@ -7,6 +7,7 @@ Records :maxdepth: 1 traditional_record_syntax + field_selectors_and_type_applications disambiguate_record_fields duplicate_record_fields record_puns |