view pattern expression are in scope. For example: ::
example :: Maybe ((String -> Integer,Integer), String) -> Bool
- example Just ((f,_), f -> 4) = True
+ example (Just ((f,_), f -> 4)) = True
Additionally, in function definitions, variables bound by matching
earlier curried arguments may be used in view pattern expressions
- An integer literal ``368`` means "``fromInteger (368::Integer)``",
rather than "``Prelude.fromInteger (368::Integer)``".
-- Fractional literals are handed in just the same way, except that the
+- Fractional literals are handled in just the same way, except that the
translation is ``fromRational (3.68::Rational)``.
+- String literals are also handled the same way, except that the
+ translation is ``fromString ("368"::String)``.
+
- The equality test in an overloaded numeric pattern uses whatever
``(==)`` is in scope.
.. index::
single: forall
- Stolen (in types) by: :extension:`ExplicitForAll`, and hence by
- :extension:`ScopedTypeVariables`, :extension:`LiberalTypeSynonyms`,
- :extension:`RankNTypes`, :extension:`ExistentialQuantification`
+ Stolen (in types) by default (see :ref:`infelicities-lexical`). ``forall`` is
+ a reserved keyword and never a type variable, in accordance with `GHC Proposal #43
+ <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0043-forall-keyword.rst>`__.
+
``mdo``
.. index::
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
.. extension:: FlexibleContexts
- :shortdesc: Enable flexible contexts. Implied by
- :extension:`ImplicitParams`.
+ :shortdesc: Enable flexible contexts.
:since: 6.8.1
.. extension:: FlexibleInstances
:shortdesc: Enable flexible instances.
Implies :extension:`TypeSynonymInstances`.
- Implied by :extension:`ImplicitParams`.
:implies: :extension:`TypeSynonymInstances`
:since: 6.8.1
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 which
+are not already in scope 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
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
: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
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
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
~~~~~~~~~~~~~~~~~~~~
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:
Associated type synonym defaults
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.
:implies: :extension:`PolyKinds`, :extension:`DataKinds`, :extension:`KindSignatures`
:since: 8.0.1
- In the past this extension used to enable advanced type-level programming
- techniques. Now it's a shorthand for a couple of other extensions.
+ The extension :extension:`TypeInType` is now deprecated: its sole effect is
+ to switch on :extension:`PolyKinds`
+ (and hence :extension:`KindSignatures`) and :extension:`DataKinds`.
.. extension:: PolyKinds
:shortdesc: Enable kind polymorphism.
The general principle is this:
-- *When there is a right-hand side, GHC infers the most polymorphic
- kind consistent with the right-hand side.* Examples: ordinary data
+- When there is a right-hand side, GHC infers the most polymorphic
+ kind consistent with the right-hand side. Examples: ordinary data
type and GADT declarations, class declarations. In the case of a
class declaration the role of "right hand side" is played by the
class method signatures.
-- *When there is no right hand side, GHC defaults argument and result
- kinds to ``Type``, except when directed otherwise by a kind signature*.
+- When there is no right hand side, GHC defaults argument and result
+ kinds to ``Type``, except when directed otherwise by a kind signature.
Examples: data and open type family declarations.
This rule has occasionally-surprising consequences (see
-:ghc-ticket:`10132`. ::
+:ghc-ticket:`10132`). ::
class C a where -- Class declarations are generalised
-- so C :: forall k. k -> Constraint
The kind-polymorphism from the class declaration makes ``D1``
kind-polymorphic, but not so ``D2``; and similarly ``F1``, ``F1``.
+.. _inferring-variable-order:
+
+Inferring the order of variables in a type/class declaration
+------------------------------------------------------------
+
+It is possible to get intricate dependencies among the type variables
+introduced in a type or class declaration. Here is an example::
+
+ data T a (b :: k) c = MkT (a c)
+
+After analysing this declaration, GHC will discover that ``a`` and
+``c`` can be kind-polymorphic, with ``a :: k2 -> Type`` and
+``c :: k2``. We thus infer the following kind::
+
+ T :: forall {k2 :: Type} (k :: Type). (k2 -> Type) -> k -> k2 -> Type
+
+Note that ``k2`` is placed *before* ``k``, and that ``k`` is placed *before*
+``a``. Also, note that ``k2`` is written here in braces. As explained with
+:extension:`TypeApplications` (:ref:`inferred-vs-specified`),
+type and kind variables that GHC generalises
+over, but not written in the original program, are not available for visible
+type application. (These are called *inferred* variables.)
+Such variables are written in braces with
+:ghc-flag:`-fprint-explicit-foralls` enabled.
+
+The general principle is this:
+
+ * Variables not available for type application come first.
+
+ * Then come variables the user has written, implicitly brought into scope
+ in a type variable's kind.
+
+ * Lastly come the normal type variables of a declaration.
+
+ * Variables not given an explicit ordering by the user are sorted according
+ to ScopedSort (:ref:`ScopedSort`).
+
+With the ``T`` example above, we could bind ``k`` *after* ``a``; doing so
+would not violate dependency concerns. However, it would violate our general
+principle, and so ``k`` comes first.
+
+Sometimes, this ordering does not respect dependency. For example::
+
+ data T2 k (a :: k) (c :: Proxy '[a, b])
+
+It must be that ``a`` and ``b`` have the same kind. Note also that ``b``
+is implicitly declared in ``c``\'s kind. Thus, according to our general
+principle, ``b`` must come *before* ``k``. However, ``b`` *depends on*
+``k``. We thus reject ``T2`` with a suitable error message.
+
+In associated types, we order the type variables as if the type family was a
+top-level declaration, ignoring the visibilities of the class's type variable
+binders. Here is an example: ::
+
+ class C (a :: k) b where
+ type F (c :: j) (d :: Proxy m) a b
+
+We infer these kinds::
+
+ C :: forall {k1 :: Type} (k :: Type). k -> k1 -> Constraint
+ F :: forall {k1 :: Type} {k2 :: Type} {k3 :: Type} j (m :: k1).
+ j -> Proxy m -> k2 -> k3 -> Type
+
+Note that the kind of ``a`` is specified in the kind of ``C`` but inferred in
+the kind of ``F``.
+
+The "general principle" described here is meant to make all this more
+predictable for users. It would not be hard to extend GHC to relax
+this principle. If you should want a change here, consider writing
+a `proposal <https://github.com/ghc-proposals/ghc-proposals/>`_ to
+do so.
+
.. index::
single: CUSK
single: complete user-supplied kind signature
Constraints in kinds
--------------------
-As kinds and types are the same, kinds can (with :extension:`PolyKinds`)
-contain type constraints. Only equality constraints are currently supported,
-however. We expect this to extend to other constraints in the future.
+As kinds and types are the same, kinds can (with :extension:`TypeInType`)
+contain type constraints. However, only equality constraints are supported.
Here is an example of a constrained kind: ::
data RuntimeRep = LiftedRep -- for things like `Int`
| UnliftedRep -- for things like `Array#`
| IntRep -- for `Int#`
- | TupleRep [RuntimeRep] -- unboxed tuples, indexed by the representations of the elements
- | SumRep [RuntimeRep] -- unboxed sums, indexed by the representations of the disjuncts
+ | TupleRep [RuntimeRep] -- unboxed tuples, indexed by the representations of the elements
+ | SumRep [RuntimeRep] -- unboxed sums, indexed by the representations of the disjuncts
| ...
type Type = TYPE LiftedRep -- Type is just an ordinary type synonym
of Roles (:ref:`roles`). It is exported by :base-ref:`Data.Coerce.`, which also
contains the documentation. More details and discussion can be found in the
paper
-`"Safe Coercions" <http://www.cis.upenn.edu/~eir/papers/2014/coercible/coercible.pdf>`__.
+`"Safe Coercions" <https://www.microsoft.com/en-us/research/uploads/prod/2018/05/coercible-JFP.pdf>`__.
.. _constraint-kind:
The two are treated identically, except that the latter may bring type variables
into scope (see :ref:`scoped-type-variables`).
-Notes:
+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`.
-- With :extension:`ExplicitForAll`, ``forall`` becomes a keyword; you can't use ``forall`` as a
- type variable any more!
+Notes:
- As well in type signatures, you can also use an explicit ``forall``
in an instance declaration: ::
========================
.. extension:: TypeApplications
- :shortdesc: Enable type application syntax.
+ :shortdesc: Enable type application syntax in terms and types.
:since: 8.0.1
the identifier has been given a type signature. If the identifier does
not have a type signature, visible type application cannot be used.
-Here are the details:
+GHC also permits visible kind application, where users can declare the kind
+arguments to be instantiated in kind-polymorphic cases. Its usage parallels
+visible type application in the term level, as specified above.
-- If an identifier's type signature does not include an
- explicit ``forall``, the type variable arguments appear
- in the left-to-right order in which the variables appear in the type.
- So, ``foo :: Monad m => a b -> m (a c)``
- will have its type variables
- ordered as ``m, a, b, c``.
+.. _inferred-vs-specified:
+
+Inferred vs. specified type variables
+-------------------------------------
+
+.. index::
+ single: type variable; inferred vs. specified
+
+GHC tracks a distinction between what we call *inferred* and *specified*
+type variables. Only specified type variables are available for instantiation
+with visible type application. An example illustrates this well::
+
+ f :: (Eq b, Eq a) => a -> b -> Bool
+ f x y = (x == x) && (y == y)
+
+ g x y = (x == x) && (y == y)
+
+The functions ``f`` and ``g`` have the same body, but only ``f`` is given
+a type signature. When GHC is figuring out how to process a visible type application,
+it must know what variable to instantiate. It thus must be able to provide
+an ordering to the type variables in a function's type.
+
+If the user has supplied a type signature, as in ``f``, then this is easy:
+we just take the ordering from the type signature, going left to right and
+using the first occurrence of a variable to choose its position within the
+ordering. Thus, the variables in ``f`` will be ``b``, then ``a``.
+
+In contrast, there is no reliable way to do this for ``g``; we will not know
+whether ``Eq a`` or ``Eq b`` will be listed first in the constraint in ``g``\'s
+type. In order to have visible type application be robust between releases of
+GHC, we thus forbid its use with ``g``.
+
+We say that the type variables in ``f`` are *specified*, while those in
+``g`` are *inferred*. The general rule is this: if the user has written
+a type variable in the source program, it is *specified*; if not, it is
+*inferred*.
+
+Thus rule applies in datatype declarations, too. For example, if we have
+``data Proxy a = Proxy`` (and :extension:`PolyKinds` is enabled), then
+``a`` will be assigned kind ``k``, where ``k`` is a fresh kind variable.
+Because ``k`` was not written by the user, it will be unavailable for
+type application in the type of the constructor ``Proxy``; only the ``a``
+will be available.
+
+When :ghc-flag:`-fprint-explicit-foralls` is enabled, inferred variables
+are printed in braces. Thus, the type of the data constructor ``Proxy``
+from the previous example would be ``forall {k} (a :: k). Proxy a``.
+We can observe this behavior in a GHCi session: ::
+
+ > :set -XTypeApplications -fprint-explicit-foralls
+ > let myLength1 :: Foldable f => f a -> Int; myLength1 = length
+ > :type +v myLength1
+ myLength1 :: forall (f :: * -> *) a. Foldable f => f a -> Int
+ > let myLength2 = length
+ > :type +v myLength2
+ myLength2 :: forall {a} {t :: * -> *}. Foldable t => t a -> Int
+ > :type +v myLength2 @[]
+
+ <interactive>:1:1: error:
+ • Cannot apply expression of type ‘t0 a0 -> Int’
+ to a visible type argument ‘[]’
+ • In the expression: myLength2 @[]
+
+Notice that since ``myLength1`` was defined with an explicit type signature,
+:ghci-cmd:`:type +v` reports that all of its type variables are available
+for type application. On the other hand, ``myLength2`` was not given a type
+signature. As a result, all of its type variables are surrounded with braces,
+and trying to use visible type application with ``myLength2`` fails.
+
+Also note the use of :ghci-cmd:`:type +v` in the GHCi session above instead
+of :ghci-cmd:`:type`. This is because :ghci-cmd:`:type` gives you the type
+that would be inferred for a variable assigned to the expression provided
+(that is, the type of ``x`` in ``let x = <expr>``). As we saw above with
+``myLength2``, this type will have no variables available to visible type
+application. On the other hand, :ghci-cmd:`:type +v` gives you the actual
+type of the expression provided. To illustrate this: ::
+
+ > :type myLength1
+ myLength1 :: forall {a} {f :: * -> *}. Foldable f => f a -> Int
+ > :type myLength2
+ myLength2 :: forall {a} {t :: * -> *}. Foldable t => t a -> Int
+
+Using :ghci-cmd:`:type` might lead one to conclude that none of the type
+variables in ``myLength1``'s type signature are available for type
+application. This isn't true, however! Be sure to use :ghci-cmd:`:type +v`
+if you want the most accurate information with respect to visible type
+application properties.
+
+.. index::
+ single: ScopedSort
+
+.. _ScopedSort:
+
+Ordering of specified variables
+-------------------------------
+
+In the simple case of the previous section, we can say that specified variables
+appear in left-to-right order. However, not all cases are so simple. Here are
+the rules in the subtler cases:
+
+- If an identifier's type has a ``forall``, then the order of type variables
+ as written in the ``forall`` is retained.
- If the type signature includes any kind annotations (either on variable
binders or as annotations on types), any variables used in kind
of the variables are *kind* variables), the variables are reordered
so that kind variables come before type variables, preserving the
left-to-right order as much as possible. That is, GHC performs a
- stable topological sort on the variables. Examples::
+ stable topological sort on the variables. Example::
h :: Proxy (a :: (j, k)) -> Proxy (b :: Proxy a) -> ()
-- as if h :: forall j k a b. ...
are not reordered with respect to each other, even though doing so would
not violate dependency conditions.
-- Visible type application is available to instantiate only user-specified
- type variables. This means that in ``data Proxy a = Proxy``, the unmentioned
- kind variable used in ``a``'s kind is *not* available for visible type
- application.
+ A "stable topological sort" here, we mean that we perform this algorithm
+ (which we call *ScopedSort*):
+
+ * Work left-to-right through the input list of type variables, with a cursor.
+ * If variable ``v`` at the cursor is depended on by any earlier variable ``w``,
+ move ``v`` immediately before the leftmost such ``w``.
- Class methods' type arguments include the class type
variables, followed by any variables an individual method is polymorphic
application. If you want to specify only the second type argument to
``wurble``, then you can say ``wurble @_ @Int``.
The first argument is a wildcard, just like in a partial type signature.
- However, if used in a visible type application, it is *not*
- necessary to specify :extension:`PartialTypeSignatures` and your
+ However, if used in a visible type application/visible kind application,
+ it is *not* necessary to specify :extension:`PartialTypeSignatures` and your
code will not generate a warning informing you of the omitted type.
-- When printing types with :ghc-flag:`-fprint-explicit-foralls` enabled,
- type variables not available for visible type application are printed
- in braces. We can observe this behavior in a GHCi session: ::
-
- > :set -XTypeApplications -fprint-explicit-foralls
- > let myLength1 :: Foldable f => f a -> Int; myLength1 = length
- > :type +v myLength1
- myLength1 :: forall (f :: * -> *) a. Foldable f => f a -> Int
- > let myLength2 = length
- > :type +v myLength2
- myLength2 :: forall {a} {t :: * -> *}. Foldable t => t a -> Int
- > :type +v myLength2 @[]
-
- <interactive>:1:1: error:
- • Cannot apply expression of type ‘t0 a0 -> Int’
- to a visible type argument ‘[]’
- • In the expression: myLength2 @[]
-
- Notice that since ``myLength1`` was defined with an explicit type signature,
- :ghci-cmd:`:type +v` reports that all of its type variables are available
- for type application. On the other hand, ``myLength2`` was not given a type
- signature. As a result, all of its type variables are surrounded with braces,
- and trying to use visible type application with ``myLength2`` fails.
-
- Also note the use of :ghci-cmd:`:type +v` in the GHCi session above instead
- of :ghci-cmd:`:type`. This is because :ghci-cmd:`:type` gives you the type
- that would be inferred for a variable assigned to the expression provided
- (that is, the type of ``x`` in ``let x = <expr>``). As we saw above with
- ``myLength2``, this type will have no variables available to visible type
- application. On the other hand, :ghci-cmd:`:type +v` gives you the actual
- type of the expression provided. To illustrate this: ::
-
- > :type myLength1
- myLength1 :: forall {a} {f :: * -> *}. Foldable f => f a -> Int
- > :type myLength2
- myLength2 :: forall {a} {t :: * -> *}. Foldable t => t a -> Int
-
- Using :ghci-cmd:`:type` might lead one to conclude that none of the type
- variables in ``myLength1``'s type signature are available for type
- application. This isn't true, however! Be sure to use :ghci-cmd:`:type +v`
- if you want the most accurate information with respect to visible type
- application properties.
-
-- Although GHC supports visible *type* applications, it does not yet support
- visible *kind* applications. However, GHC does follow similar rules for
- quantifying variables in kind signatures as it does for quantifying type
- signatures. For instance: ::
-
- type family F (a :: j) (b :: k) :: l
- -- F :: forall j k l. j -> k -> l
-
- In the kind of ``F``, the left-to-right ordering of ``j``, ``k``, and ``l``
- is preserved.
-
- If a family declaration is associated with a class, then class-bound
- variables always come first in the kind of the family. For instance: ::
-
- class C (a :: Type) where
- type T (x :: f a)
- -- T :: forall a f. f a -> Type
-
- Contrast this with the kind of the following top-level family declaration: ::
-
- type family T2 (x :: f a)
- -- T2 :: forall f a. f a -> Type
+The section in this manual on kind polymorphism describes how variables
+in type and class declarations are ordered (:ref:`inferring-variable-order`).
.. _implicit-parameters:
.. extension:: ImplicitParams
:shortdesc: Enable Implicit Parameters.
- Implies :extension:`FlexibleContexts` and :extension:`FlexibleInstances`.
:since: 6.8.1
.. ghc-flag:: -fabstract-refinement-hole-fits
:shortdesc: *default: off.* Toggles whether refinements where one or more
- or more of the holes are abstract are reported.
+ of the holes are abstract are reported.
:type: dynamic
:reverse: -fno-abstract-refinement-hole-fits
:category: verbosity
type or data instance declaration;
see :ref:`type-wildcards-lhs`.
-Anonymous wildcards are also allowed in visible type applications
-(:ref:`visible-type-application`). If you want to specify only the second type
-argument to ``wurble``, then you can say ``wurble @_ @Int`` where the first
-argument is a wildcard.
+Anonymous wildcards are also allowed in visible type applications/ visible kind
+applications (:ref:`visible-type-application`). If you want to specify only the
+second type argument to ``wurble``, then you can say ``wurble @_ @Int`` where
+the first argument is a wildcard.
Standalone ``deriving`` declarations permit the use of a single,
extra-constraints wildcard, like so: ::
``LANGUAGE`` pragma
-------------------
-.. index::
- single: LANGUAGE; pragma
- single: pragma; LANGUAGE
+.. pragma:: LANGUAGE ⟨ext⟩, ⟨ext⟩, ...
+
+ :where: file header
+
+ Enable or disable a set of language extensions.
The ``LANGUAGE`` pragma allows language extensions to be enabled in a
portable way. It is the intention that all Haskell compilers support the
``OPTIONS_GHC`` pragma
----------------------
-.. index::
- single: OPTIONS_GHC
- single: pragma; OPTIONS_GHC
+.. pragma:: OPTIONS_GHC ⟨flags⟩
+
+ :where: file header
The ``OPTIONS_GHC`` pragma is used to specify additional options that
are given to the compiler when compiling this source file. See
``WARNING`` and ``DEPRECATED`` pragmas
--------------------------------------
-.. index::
- single: WARNING
- single: DEPRECATED
+.. pragma:: WARNING
-The ``WARNING`` pragma allows you to attach an arbitrary warning to a
-particular function, class, or type. A ``DEPRECATED`` pragma lets you
-specify that a particular function, class, or type is deprecated. There
-are two ways of using these pragmas.
+ :where: declaration
+
+ The ``WARNING`` pragma allows you to attach an arbitrary warning to a
+ particular function, class, or type.
+
+.. pragma:: DEPRECATED
+
+ :where: declaration
+
+ A ``DEPRECATED`` pragma lets you specify that a particular function, class,
+ or type is deprecated.
+
+There are two ways of using these pragmas.
- You can work on an entire module thus: ::
``MINIMAL`` pragma
------------------
-.. index::
- single: MINIMAL
- single: pragma; MINIMAL
+.. pragma:: MINIMAL ⟨name⟩ | ⟨name⟩ , ...
+
+ :where: in class body
+
+ Define the methods needed for a minimal complete instance of a class.
The ``MINIMAL`` pragma is used to specify the minimal complete definition of
a class, i.e. specify which methods must be implemented by all
``INLINE`` pragma
~~~~~~~~~~~~~~~~~
-.. index::
- single: INLINE
- single: pragma; INLINE
+.. pragma:: INLINE ⟨name⟩
+
+ :where: top-level
+
+ Force GHC to inline a value.
GHC (with :ghc-flag:`-O`, as always) tries to inline (or "unfold")
functions/values that are "small enough," thus avoiding the call
which will optimise better than the corresponding use of ``comp2``.
- It is useful for GHC to optimise the definition of an INLINE function
- ``f`` just like any other non-INLINE function, in case the
+ ``f`` just like any other non-``INLINE`` function, in case the
non-inlined version of ``f`` is ultimately called. But we don't want
to inline the *optimised* version of ``f``; a major reason for ``INLINE``
pragmas is to expose functions in ``f``\'s RHS that have rewrite
usual. For externally-visible functions the inline-RHS (not the
optimised RHS) is recorded in the interface file.
-- An INLINE function is not worker/wrappered by strictness analysis.
+- An ``INLINE`` function is not worker/wrappered by strictness analysis.
It's going to be inlined wholesale instead.
GHC ensures that inlining cannot go on forever: every mutually-recursive
``INLINABLE`` pragma
~~~~~~~~~~~~~~~~~~~~
+.. pragma:: INLINABLE ⟨name⟩
+
+ :where: top-level
+
+ Suggest that the compiler always consider inlining ``name``.
+
An ``{-# INLINABLE f #-}`` pragma on a function ``f`` has the following
behaviour:
~~~~~~~~~~~~~~~~~~~
.. index::
- single: NOINLINE
single: NOTINLINE
-The ``NOINLINE`` pragma does exactly what you'd expect: it stops the
+.. pragma:: NOINLINE ⟨name⟩
+
+ :where: top-level
+
+ Instructs the compiler not to inline a value.
+
+The :pragma:`NOINLINE` pragma does exactly what you'd expect: it stops the
named function from being inlined by the compiler. You shouldn't ever
need to do this, unless you're very cautious about code size.
``CONLIKE`` modifier
~~~~~~~~~~~~~~~~~~~~
-.. index::
- single: CONLIKE
+.. pragma:: CONLINE
-An ``INLINE`` or ``NOINLINE`` pragma may have a ``CONLIKE`` modifier, which affects
-matching in RULEs (only). See :ref:`conlike`.
+ :where: modifies :pragma:`INLINE` or :pragma:`NOINLINE` pragma
+
+ Instructs GHC to consider a value to be especially cheap to inline.
+
+An :pragma:`INLINE` or :pragma:`NOINLINE` pragma may have a :pragma:`CONLIKE` modifier, which affects
+matching in :pragma:`RULE`\s (only). See :ref:`conlike`.
.. _phase-control:
Phase control
~~~~~~~~~~~~~
-Sometimes you want to control exactly when in GHC's pipeline the ``INLINE``
+Sometimes you want to control exactly when in GHC's pipeline the :pragma:`INLINE`
pragma is switched on. Inlining happens only during runs of the
*simplifier*. Each run of the simplifier has a different *phase number*;
the phase number decreases towards zero. If you use
-``-dverbose-core2core`` you'll see the sequence of phase numbers for
-successive runs of the simplifier. In an ``INLINE`` pragma you can
+:ghc-flag:`-dverbose-core2core` you will see the sequence of phase numbers for
+successive runs of the simplifier. In an :pragma:`INLINE` pragma you can
optionally specify a phase number, thus:
- "``INLINE[k] f``" means: do not inline ``f`` until phase ``k``, but
The same information is summarised here:
-::
+.. code-block:: none
-- Before phase 2 Phase 2 and later
{-# INLINE [2] f #-} -- No Yes
function body is small, or it is applied to interesting-looking
arguments etc). Another way to understand the semantics is this:
-- For both ``INLINE`` and ``NOINLINE``, the phase number says when inlining is
- allowed at all.
+- For both :pragma:`INLINE` and :pragma:`NOINLINE`, the phase number says when
+ inlining is allowed at all.
-- The ``INLINE`` pragma has the additional effect of making the function
+- The :pragma:`INLINE` pragma has the additional effect of making the function
body look small, so that when inlining is allowed it is very likely
to happen.
-The same phase-numbering control is available for RULES
+The same phase-numbering control is available for :pragma:`RULE`\s
(:ref:`rewrite-rules`).
.. _line-pragma:
``LINE`` pragma
---------------
-.. index::
- single: LINE; pragma
- single: pragma; LINE
+.. pragma:: LINE ⟨lineno⟩ "⟨file⟩"
+
+ :where: anywhere
+
+ Generated by preprocessors to convey source line numbers of the original
+ source.
This pragma is similar to C's ``#line`` pragma, and is mainly for use in
automatically generated Haskell code. It lets you specify the line
``RULES`` pragma
----------------
-The ``RULES`` pragma lets you specify rewrite rules. It is described in
+The :pragma:`RULES` pragma lets you specify rewrite rules. It is described in
:ref:`rewrite-rules`.
.. _specialize-pragma:
single: pragma, SPECIALIZE
single: overloading, death to
+.. pragma:: SPECIALIZE ⟨name⟩ :: ⟨type⟩
+
+ Ask that GHC specialize a polymorphic value to a particular type.
+
(UK spelling also accepted.) For key overloaded functions, you can
-create extra versions (NB: more code space) specialised to particular
+create extra versions (NB: at the cost of larger code) specialised to particular
types. Thus, if you have an overloaded function:
::
``SPECIALIZE INLINE``
~~~~~~~~~~~~~~~~~~~~~
+.. pragma:: SPECIALIZE INLINE ⟨name⟩ :: ⟨type⟩
+
+ :where: top-level
+
A ``SPECIALIZE`` pragma can optionally be followed with a ``INLINE`` or
``NOINLINE`` pragma, optionally followed by a phase, as described in
:ref:`inline-noinline-pragma`. The ``INLINE`` pragma affects the
a type-based unrolling of the indexing function.
You can add explicit phase control (:ref:`phase-control`) to
-``SPECIALISE INLINE`` pragma, just like on an ``INLINE`` pragma; if you
-do so, the same phase is used for the rewrite rule and the INLINE
-control of the specialised function.
+``SPECIALISE INLINE`` pragma, just like on an :pragma:`INLINE` pragma; if you do
+so, the same phase is used for the rewrite rule and the INLINE control of the
+specialised function.
.. warning:: You can make GHC diverge by using ``SPECIALISE INLINE`` on an
ordinarily-recursive function.
``SPECIALIZE`` for imported functions
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Generally, you can only give a ``SPECIALIZE`` pragma for a function
+Generally, you can only give a :pragma:`SPECIALIZE` pragma for a function
defined in the same module. However if a function ``f`` is given an
-``INLINABLE`` pragma at its definition site, then it can subsequently be
+:pragma:`INLINABLE` pragma at its definition site, then it can subsequently be
specialised by importing modules (see :ref:`inlinable-pragma`). For example ::
module Map( lookup, blah blah ) where
data T = T1 | T2 deriving( Eq, Ord )
{-# SPECIALISE lookup :: [(T,a)] -> T -> Maybe a
-Here, ``lookup`` is declared ``INLINABLE``, but it cannot be specialised
+Here, ``lookup`` is declared :pragma:`INLINABLE`, but it cannot be specialised
for type ``T`` at its definition site, because that type does not exist
yet. Instead a client module can define ``T`` and then specialise
``lookup`` at that type.
Moreover, every module that imports ``Client`` (or imports a module that
imports ``Client``, transitively) will "see", and make use of, the
specialised version of ``lookup``. You don't need to put a
-``SPECIALIZE`` pragma in every module.
+:pragma:`SPECIALIZE` pragma in every module.
-Moreover you often don't even need the ``SPECIALIZE`` pragma in the
+Moreover you often don't even need the :pragma:`SPECIALIZE` pragma in the
first place. When compiling a module ``M``, GHC's optimiser (when given the
:ghc-flag:`-O` flag) automatically considers each top-level overloaded function declared
in ``M``, and specialises it for the different types at which it is called in
-``M``. The optimiser *also* considers each *imported* ``INLINABLE``
+``M``. The optimiser *also* considers each *imported* :pragma:`INLINABLE`
overloaded function, and specialises it for the different types at which
it is called in ``M``. So in our example, it would be enough for ``lookup``
to be called at type ``T``:
------------------------------
.. index::
- single: SPECIALIZE pragma
+ single: instance, specializing
single: overloading, death to
+.. pragma:: SPECIALIZE instance ⟨instance head⟩
+
+ :where: instance body
+
Same idea, except for instance declarations. For example:
::
``UNPACK`` pragma
-----------------
-.. index::
- single: UNPACK
+.. pragma:: UNPACK
+
+ :where: data constructor field
+
+ Instructs the compiler to unpack the contents of a constructor field into
+ the constructor itself.
The ``UNPACK`` indicates to the compiler that it should unpack the
contents of a constructor field into the constructor itself, removing a
effect of adding ``{-# UNPACK #-}`` to every strict constructor field.
.. [1]
- In fact, ``UNPACK`` has no effect without :ghc-flag:`-O`, for technical
+ In fact, :pragma:`UNPACK` has no effect without :ghc-flag:`-O`, for technical
reasons (see :ghc-ticket:`5252`).
.. _nounpack-pragma:
``NOUNPACK`` pragma
-------------------
-.. index::
- single: NOUNPACK
+.. pragma:: NOUNPACK
+
+ :where: top-level
+
+ Instructs the compiler not to unpack a constructor field.
The ``NOUNPACK`` pragma indicates to the compiler that it should not
unpack the contents of a constructor field. Example: ::
``SOURCE`` pragma
-----------------
-.. index::
- single: SOURCE
- single: pragma; SOURCE
+.. pragma:: SOURCE
+
+ :where: after ``import`` statement
+
+ Import a module by ``hs-boot`` file to break a module loop.
The ``{-# SOURCE #-}`` pragma is used only in ``import`` declarations,
to break a module loop. It is described in detail in
``COMPLETE`` pragmas
--------------------
+.. pragma:: COMPLETE
+
+ :where: at top level
+
+ Specify the set of constructors or pattern synonyms which constitute a total
+ match.
+
The ``COMPLETE`` pragma is used to inform the pattern match checker that a
certain set of patterns is complete and that any function which matches
on all the specified patterns is total.
single: INCOHERENT
single: pragma; INCOHERENT
+.. pragma:: OVERLAPPING
+.. pragma:: OVERLAPPABLE
+.. pragma:: OVERLAPS
+.. pragma:: INCOHERENT
+
+ :where: on instance head
+
The pragmas ``OVERLAPPING``, ``OVERLAPPABLE``, ``OVERLAPS``,
``INCOHERENT`` are used to specify the overlap behavior for individual
instances, as described in Section :ref:`instance-overlap`. The pragmas
=============
.. index::
- single: RULES pragma
- single: pragma; RULES
single: rewrite rules
+.. pragma:: RULES "⟨name⟩" forall ⟨binder⟩ ... . ⟨expr⟩ = ⟨expr⟩ ...
+
+ :where: top-level
+
+ Define a rewrite rule to be used to optimize a source program.
+
The programmer can specify rewrite rules as part of the source program
(in a pragma). Here is an example: ::
{-# RULES
- "map/map" forall f g xs. map f (map g xs) = map (f.g) xs
+ "map/map" forall f g xs. map f (map g xs) = map (f.g) xs
#-}
Use the debug flag :ghc-flag:`-ddump-simpl-stats` to see what rules fired. If
From a syntactic point of view:
-- There may be zero or more rules in a ``RULES`` pragma, separated by
+- There may be zero or more rules in a :pragma:`RULES` pragma, separated by
semicolons (which may be generated by the layout rule).
- The layout rule applies in a pragma. Currently no new indentation
the same column as the enclosing definitions. ::
{-# RULES
- "map/map" forall f g xs. map f (map g xs) = map (f.g) xs
- "map/append" forall f xs ys. map f (xs ++ ys) = map f xs ++ map f ys
+ "map/map" forall f g xs. map f (map g xs) = map (f.g) xs
+ "map/append" forall f xs ys. map f (xs ++ ys) = map f xs ++ map f ys
#-}
Furthermore, the closing ``#-}`` should start in a column to the
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``.
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: ::
then C's rules are in force when compiling A.) The situation is very
similar to that for instance declarations.
-- Inside a RULE "``forall``" is treated as a keyword, regardless of any
+- Inside a :pragma:`RULE` "``forall``" is treated as a keyword, regardless of any
other flag settings. Furthermore, inside a RULE, the language
extension :extension:`ScopedTypeVariables` is automatically enabled; see
:ref:`scoped-type-variables`.
-- Like other pragmas, ``RULE`` pragmas are always checked for scope errors,
+- Like other pragmas, :pragma:`RULE` pragmas are always checked for scope errors,
and are typechecked. Typechecking means that the LHS and RHS of a
rule are typechecked, and must have the same type. However, rules are
only *enabled* if the :ghc-flag:`-fenable-rewrite-rules` flag is on (see
g y = y
-Now ``g`` is inlined into ``h``, but ``f``\'s RULE has no chance to fire.
-If instead GHC had first inlined ``g`` into ``h`` then there would have
-been a better chance that ``f``\'s RULE might fire.
+Now ``g`` is inlined into ``h``, but ``f``\'s :pragma:`RULE` has no chance to
+fire. If instead GHC had first inlined ``g`` into ``h`` then there would have
+been a better chance that ``f``\'s :pragma:`RULE` might fire.
-The way to get predictable behaviour is to use a ``NOINLINE`` pragma, or an
-``INLINE[⟨phase⟩]`` pragma, on ``f``, to ensure that it is not inlined until
+The way to get predictable behaviour is to use a :pragma:`NOINLINE` pragma, or an
+INLINE[⟨phase⟩] pragma, on ``f``, to ensure that it is not inlined until
its RULEs have had a chance to fire. The warning flag
:ghc-flag:`-Winline-rule-shadowing` (see :ref:`options-sanity`) warns about
this situation.
to the left of the ``=`` sign) should be considered cheap enough to
duplicate, if such a duplication would make rule fire. (The name
"CONLIKE" is short for "constructor-like", because constructors
-certainly have such a property.) The ``CONLIKE`` pragma is a modifier to
-INLINE/NOINLINE because it really only makes sense to match ``f`` on the
-LHS of a rule if you are sure that ``f`` is not going to be inlined
+certainly have such a property.) The :pragma:`CONLIKE` pragma is a modifier to
+:pragma:`INLINE`/:pragma:`NOINLINE` because it really only makes sense to match
+``f`` on the LHS of a rule if you are sure that ``f`` is not going to be inlined
before the rule has a chance to fire.
.. _rules-class-methods:
{-# INLINE build #-}
build g = g (:) []
- Notice the ``INLINE``! That prevents ``(:)`` from being inlined when
+ Notice the :pragma:`INLINE`! That prevents ``(:)`` from being inlined when
compiling ``PrelBase``, so that an importing module will “see” the
``(:)``, and can match it on the LHS of a rule. ``INLINE`` prevents
any inlining happening in the RHS of the ``INLINE`` thing. I regret
git.haskell.org / ghc.git / blobdiff