diff options
Diffstat (limited to 'docs')
| -rw-r--r-- | docs/users_guide/glasgow_exts.rst | 68 | ||||
| -rw-r--r-- | docs/users_guide/using-warnings.rst | 20 |
2 files changed, 78 insertions, 10 deletions
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst index 366dd98052..196350348f 100644 --- a/docs/users_guide/glasgow_exts.rst +++ b/docs/users_guide/glasgow_exts.rst @@ -7572,6 +7572,17 @@ instance for ``GMap`` is :: In this example, the declaration has only one variant. In general, it can be any number. +When :extension:`ExplicitForAll` is enabled, type or kind variables used on +the left hand side can be explicitly bound. For example: :: + + data instance forall a (b :: Proxy a). F (Proxy b) = FProxy Bool + +When an explicit ``forall`` is present, all *type* variables mentioned must +be bound by the ``forall``. Kind variables will be implicitly bound if +necessary, for example: :: + + data instance forall (a :: k). F a = FOtherwise + When the flag :ghc-flag:`-Wunused-type-patterns` is enabled, type variables that are mentioned in the patterns on the left hand side, but not used on the right hand side are reported. Variables that occur multiple times @@ -7585,6 +7596,9 @@ This resembles the wildcards that can be used in No error messages reporting the inferred types are generated, nor does the extension :extension:`PartialTypeSignatures` have any effect. +A type or kind variable explicitly bound using :extension:`ExplicitForAll` but +not used on the left hand side will generate an error, not a warning. + Data and newtype instance declarations are only permitted when an appropriate family declaration is in scope - just as a class instance declaration requires the class declaration to be visible. Moreover, each @@ -7737,6 +7751,10 @@ with underscores to avoid warnings when the :ghc-flag:`-Wunused-type-patterns` flag is enabled. The same rules apply as for :ref:`data-instance-declarations`. +Also in the same way as :ref:`data-instance-declarations`, when +:extension:`ExplicitForAll` is enabled, type and kind variables can be +explicilty bound in a type instance declaration. + Type family instance declarations are only legitimate when an appropriate family declaration is in scope - just like class instances require the class declaration to be visible. Moreover, each instance @@ -7771,8 +7789,14 @@ Note that GHC must be sure that ``a`` cannot unify with ``Int`` or their code, GHC will not be able to simplify the type. After all, ``a`` might later be instantiated with ``Int``. -A closed type family's equations have the same restrictions as the -equations for open type family instances. +A closed type family's equations have the same restrictions and extensions as +the equations for open type family instances. For instance, when +:extension:`ExplicitForAll` is enabled, type or kind variables used on the +left hand side of an equation can be explicitly bound, such as in: :: + + type family R a where + forall t a. R (t a) = [a] + forall a. R a = a A closed type family may be declared with no equations. Such closed type families are opaque type-level definitions that will never reduce, are @@ -8000,7 +8024,7 @@ Hence, the following contrived example is admissible: :: Here ``c`` and ``a`` are class parameters, but the type is also indexed on a third parameter ``x``. -.. _assoc-data-inst: +.. _assoc-inst: Associated instances ~~~~~~~~~~~~~~~~~~~~ @@ -8075,6 +8099,15 @@ Note the following points: cannot give any *subsequent* instances for ``(GMap Flob ...)``, this facility is most useful when the free indexed parameter is of a kind with a finite number of alternatives (unlike ``Type``). + +- When :extension:`ExplicitForAll` is enabled, type and kind variables can be + explicily bound in associated data or type family instances in the same way + (and with the same restrictions) as :ref:`data-instance-declarations` or + :ref:`type-instance-declarations`. For example, adapting the above, the + following is accepted: :: + + instance Eq (Elem [e]) => Collects [e] where + type forall e. Elem [e] = e .. _assoc-decl-defs: @@ -8111,6 +8144,10 @@ Note the following points: variables that are explicitly bound on the left hand side. This restriction is relaxed for *kind* variables, however, as the right hand side is allowed to mention kind variables that are implicitly bound on the left hand side. + + Because of this, unlike :ref:`assoc-inst`, explicit binding of type/kind + variables in default declarations is not permitted by + :extension:`ExplicitForAll`. - Unlike the associated type family declaration itself, the type variables of the default instance are independent of those of the parent class. @@ -9989,6 +10026,10 @@ means this: :: The two are treated identically, except that the latter may bring type variables into scope (see :ref:`scoped-type-variables`). +This extension also enables explicit quantification of type and kind variables +in :ref:`data-instance-declarations`, :ref:`type-instance-declarations`, +:ref:`closed-type-families`, :ref:`assoc-inst`, and :ref:`rewrite-rules`. + Notes: - With :extension:`ExplicitForAll`, ``forall`` becomes a keyword; you can't use ``forall`` as a @@ -15172,7 +15213,7 @@ From a syntactic point of view: is never run by GHC, but is nevertheless parsed, typechecked etc, so that it is available to the plugin. -- Each variable mentioned in a rule must either be in scope (e.g. +- Each (term) variable mentioned in a rule must either be in scope (e.g. ``map``), or bound by the ``forall`` (e.g. ``f``, ``g``, ``xs``). The variables bound by the ``forall`` are called the *pattern* variables. They are separated by spaces, just like in a type ``forall``. @@ -15186,6 +15227,25 @@ From a syntactic point of view: Since ``g`` has a polymorphic type, it must have a type signature. +- If :extension:`ExplicitForAll` is enabled, type/kind variables can also be + explicitly bound. For example: :: + + {-# RULES "id" forall a. forall (x :: a). id @a x = x #-} + + When a type-level explicit ``forall`` is present, each type/kind variable + mentioned must now also be either in scope or bound by the ``forall``. In + particular, unlike some other places in Haskell, this means free kind + variables will not be implicitly bound. For example: :: + + "this_is_bad" forall (c :: k). forall (x :: Proxy c) ... + "this_is_ok" forall k (c :: k). forall (x :: Proxy c) ... + + When bound type/kind variables are needed, both foralls must always be + included, though if no pattern variables are needed, the second can be left + empty. For example: :: + + {-# RULES "map/id" forall a. forall. map (id @a) = id @[a] #-} + - The left hand side of a rule must consist of a top-level variable applied to arbitrary expressions. For example, this is *not* OK: :: diff --git a/docs/users_guide/using-warnings.rst b/docs/users_guide/using-warnings.rst index f603a4cf28..f0c4ac4fd5 100644 --- a/docs/users_guide/using-warnings.rst +++ b/docs/users_guide/using-warnings.rst @@ -1503,7 +1503,7 @@ of ``-W(no-)*``. do { mapM_ popInt xs ; return 10 } .. ghc-flag:: -Wunused-type-patterns - :shortdesc: warn about unused type variables which arise from patterns + :shortdesc: warn about unused type variables which arise from patterns in in type family and data family instances :type: dynamic :reverse: -Wno-unused-type-patterns @@ -1513,22 +1513,30 @@ of ``-W(no-)*``. single: unused type patterns, warning single: type patterns, unused - Report all unused type variables which arise from patterns in type family - and data family instances. For instance: :: + Report all unused implicitly bound type variables which arise from + patterns in type family and data family instances. For instance: :: type instance F x y = [] - would report ``x`` and ``y`` as unused. The warning is suppressed if the - type variable name begins with an underscore, like so: :: + would report ``x`` and ``y`` as unused on the right hand side. The warning + is suppressed if the type variable name begins with an underscore, like + so: :: type instance F _x _y = [] + When :extension:`ExplicitForAll` is enabled, explicitly quantified type + variables may also be identified as unused. For instance: :: + + type instance forall x y. F x y = [] + + would still report ``x`` and ``y`` as unused on the right hand side + Unlike :ghc-flag:`-Wunused-matches`, :ghc-flag:`-Wunused-type-patterns` is not implied by :ghc-flag:`-Wall`. The rationale for this decision is that unlike term-level pattern names, type names are often chosen expressly for documentation purposes, so using underscores in type names can make the documentation harder to read. - + .. ghc-flag:: -Wunused-foralls :shortdesc: warn about type variables in user-written ``forall``\\s that are unused |