diff git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 774805b344c093a4121338e9473f6cb0165e392b..481ff5ffe537d7bf8a7c0886116b6ed75b3fbd86 100644
 a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ 617,3833 +617,3833 @@ follows:
alphaequivalence, so two instances of ``(x, view x > y)`` will not
be coalesced.
.. _patternsynonyms:

Pattern synonyms

+.. _nkpatterns:
.. ghcflag:: XPatternSynonyms
+n+k patterns
+
 :since: 7.8.1
+.. ghcflag:: XNPlusKPatterns
 Allow the definition of pattern synonyms.
+ Enable use of ``n+k`` patterns.
Pattern synonyms are enabled by the flag :ghcflag:`XPatternSynonyms`, which is
required for defining them, but *not* for using them. More information
and examples of view patterns can be found on the
`Wiki page `.
+.. _recursivedonotation:
Pattern synonyms enable giving names to parametrized pattern schemes.
They can also be thought of as abstract constructors that don't have a
bearing on data representation. For example, in a programming language
implementation, we might represent types of the language as follows: ::
+The recursive donotation
+
 data Type = App String [Type]
+.. ghcflag:: XRecursiveDo
Here are some examples of using said representation. Consider a few
types of the ``Type`` universe encoded like this: ::
+ Allow the use of recursive ``do`` notation.
 App ">" [t1, t2]  t1 > t2
 App "Int" []  Int
 App "Maybe" [App "Int" []]  Maybe Int
+The donotation of Haskell 98 does not allow *recursive bindings*, that
+is, the variables bound in a doexpression are visible only in the
+textually following code block. Compare this to a letexpression, where
+bound variables are visible in the entire binding group.
This representation is very generic in that no types are given special
treatment. However, some functions might need to handle some known types
specially, for example the following two functions collect all argument
types of (nested) arrow types, and recognize the ``Int`` type,
respectively: ::
+It turns out that such recursive bindings do indeed make sense for a
+variety of monads, but not all. In particular, recursion in this sense
+requires a fixedpoint operator for the underlying monad, captured by
+the ``mfix`` method of the ``MonadFix`` class, defined in
+``Control.Monad.Fix`` as follows: ::
 collectArgs :: Type > [Type]
 collectArgs (App ">" [t1, t2]) = t1 : collectArgs t2
 collectArgs _ = []
+ class Monad m => MonadFix m where
+ mfix :: (a > m a) > m a
 isInt :: Type > Bool
 isInt (App "Int" []) = True
 isInt _ = False
+Haskell's ``Maybe``, ``[]`` (list), ``ST`` (both strict and lazy
+versions), ``IO``, and many other monads have ``MonadFix`` instances. On
+the negative side, the continuation monad, with the signature
+``(a > r) > r``, does not.
Matching on ``App`` directly is both hard to read and error prone to
write. And the situation is even worse when the matching is nested: ::
+For monads that do belong to the ``MonadFix`` class, GHC provides an
+extended version of the donotation that allows recursive bindings. The
+:ghcflag:`XRecursiveDo` (language pragma: ``RecursiveDo``) provides the
+necessary syntactic support, introducing the keywords ``mdo`` and
+``rec`` for higher and lower levels of the notation respectively. Unlike
+bindings in a ``do`` expression, those introduced by ``mdo`` and ``rec``
+are recursively defined, much like in an ordinary letexpression. Due to
+the new keyword ``mdo``, we also call this notation the *mdonotation*.
 isIntEndo :: Type > Bool
 isIntEndo (App ">" [App "Int" [], App "Int" []]) = True
 isIntEndo _ = False
+Here is a simple (albeit contrived) example:
Pattern synonyms permit abstracting from the representation to expose
matchers that behave in a constructorlike manner with respect to
pattern matching. We can create pattern synonyms for the known types we
care about, without committing the representation to them (note that
these don't have to be defined in the same module as the ``Type`` type): ::
+::
 pattern Arrow t1 t2 = App ">" [t1, t2]
 pattern Int = App "Int" []
 pattern Maybe t = App "Maybe" [t]
+ {# LANGUAGE RecursiveDo #}
+ justOnes = mdo { xs < Just (1:xs)
+ ; return (map negate xs) }
Which enables us to rewrite our functions in a much cleaner style: ::
+or equivalently
 collectArgs :: Type > [Type]
 collectArgs (Arrow t1 t2) = t1 : collectArgs t2
 collectArgs _ = []
+::
 isInt :: Type > Bool
 isInt Int = True
 isInt _ = False
+ {# LANGUAGE RecursiveDo #}
+ justOnes = do { rec { xs < Just (1:xs) }
+ ; return (map negate xs) }
 isIntEndo :: Type > Bool
 isIntEndo (Arrow Int Int) = True
 isIntEndo _ = False
+As you can guess ``justOnes`` will evaluate to ``Just [1,1,1,...``.
In general there are three kinds of pattern synonyms. Unidirectional,
bidirectional and explicitly bidirectional. The examples given so far are
examples of bidirectional pattern synonyms. A bidirectional synonym
behaves the same as an ordinary data constructor. We can use it in a pattern
context to deconstruct values and in an expression context to construct values.
For example, we can construct the value `intEndo` using the pattern synonyms
`Arrow` and `Int` as defined previously. ::
+GHC's implementation the mdonotation closely follows the original
+translation as described in the paper `A recursive do for
+Haskell `__, which
+in turn is based on the work `Value Recursion in Monadic
+Computations `__.
+Furthermore, GHC extends the syntax described in the former paper with a
+lower level syntax flagged by the ``rec`` keyword, as we describe next.
 intEndo :: Type
 intEndo = Arrow Int Int
+Recursive binding groups
+~~~~~~~~~~~~~~~~~~~~~~~~
This example is equivalent to the much more complicated construction if we had
directly used the `Type` constructors. ::
+The flag :ghcflag:`XRecursiveDo` also introduces a new keyword ``rec``, which
+wraps a mutuallyrecursive group of monadic statements inside a ``do``
+expression, producing a single statement. Similar to a ``let`` statement
+inside a ``do``, variables bound in the ``rec`` are visible throughout
+the ``rec`` group, and below it. For example, compare
 intEndo :: Type
 intEndo = App ">" [App "Int" [], App "Int" []]
+::
+ do { a < getChar do { a < getChar
+ ; let { r1 = f a r2 ; rec { r1 < f a r2
+ ; ; r2 = g r1 } ; ; r2 < g r1 }
+ ; return (r1 ++ r2) } ; return (r1 ++ r2) }
Unidirectional synonyms can only be used in a pattern context and are
defined as follows:
+In both cases, ``r1`` and ``r2`` are available both throughout the
+``let`` or ``rec`` block, and in the statements that follow it. The
+difference is that ``let`` is nonmonadic, while ``rec`` is monadic. (In
+Haskell ``let`` is really ``letrec``, of course.)
+The semantics of ``rec`` is fairly straightforward. Whenever GHC finds a
+``rec`` group, it will compute its set of bound variables, and will
+introduce an appropriate call to the underlying monadic valuerecursion
+operator ``mfix``, belonging to the ``MonadFix`` class. Here is an
+example:
::
 pattern Head x < x:xs
+ rec { b < f a c ===> (b,c) < mfix (\ ~(b,c) > do { b < f a c
+ ; c < f b a } ; c < f b a
+ ; return (b,c) })
In this case, ``Head`` ⟨x⟩ cannot be used in expressions, only patterns,
since it wouldn't specify a value for the ⟨xs⟩ on the righthand side. However,
we can define an explicitly bidirectional pattern synonym by separately
specifying how to construct and deconstruct a type. The syntax for
doing this is as follows:
+As usual, the metavariables ``b``, ``c`` etc., can be arbitrary
+patterns. In general, the statement ``rec ss`` is desugared to the
+statement
::
 pattern HeadC x < x:xs where
 HeadC x = [x]
+ vs < mfix (\ ~vs > do { ss; return vs })
We can then use ``HeadC`` in both expression and pattern contexts. In a pattern
context it will match the head of any list with length at least one. In an
expression context it will construct a singleton list.
+where ``vs`` is a tuple of the variables bound by ``ss``.
The table below summarises where each kind of pattern synonym can be used.
+Note in particular that the translation for a ``rec`` block only
+involves wrapping a call to ``mfix``: it performs no other analysis on
+the bindings. The latter is the task for the ``mdo`` notation, which is
+described next.
+++++
 Context  Unidirectional  Bidirectional  Explicitly Bidirectional 
+===============+================+===============+===========================+
 Pattern  Yes  Yes  Yes 
+++++
 Expression  No  Yes (Inferred) Yes (Explicit) 
+++++
+The ``mdo`` notation
+~~~~~~~~~~~~~~~~~~~~
.. _recordpatsyn:
+A ``rec``block tells the compiler where precisely the recursive knot
+should be tied. It turns out that the placement of the recursive knots
+can be rather delicate: in particular, we would like the knots to be
+wrapped around as minimal groups as possible. This process is known as
+*segmentation*, and is described in detail in Section 3.2 of `A
+recursive do for
+Haskell `__.
+Segmentation improves polymorphism and reduces the size of the recursive
+knot. Most importantly, it avoids unnecessary interference caused by a
+fundamental issue with the socalled *rightshrinking* axiom for monadic
+recursion. In brief, most monads of interest (IO, strict state, etc.) do
+*not* have recursion operators that satisfy this axiom, and thus not
+performing segmentation can cause unnecessary interference, changing the
+termination behavior of the resulting translation. (Details can be found
+in Sections 3.1 and 7.2.2 of `Value Recursion in Monadic
+Computations `__.)
Record Pattern Synonyms
~~~~~~~~~~~~~~~~~~~~~~~
+The ``mdo`` notation removes the burden of placing explicit ``rec``
+blocks in the code. Unlike an ordinary ``do`` expression, in which
+variables bound by statements are only in scope for later statements,
+variables bound in an ``mdo`` expression are in scope for all statements
+of the expression. The compiler then automatically identifies minimal
+mutually recursively dependent segments of statements, treating them as
+if the user had wrapped a ``rec`` qualifier around them.
It is also possible to define pattern synonyms which behave just like record
constructors. The syntax for doing this is as follows:
+The definition is syntactic:
::
+ A generator ⟨g⟩ *depends* on a textually following generator ⟨g'⟩, if
 pattern Point :: (Int, Int)
 pattern Point{x, y} = (x, y)
+  ⟨g'⟩ defines a variable that is used by ⟨g⟩, or
The idea is that we can then use ``Point`` just as if we had defined a new
datatype ``MyPoint`` with two fields ``x`` and ``y``.
+  ⟨g'⟩ textually appears between ⟨g⟩ and ⟨g''⟩, where ⟨g⟩ depends on
+ ⟨g''⟩.
::
+ A *segment* of a given ``mdo``expression is a minimal sequence of
+ generators such that no generator of the sequence depends on an
+ outside generator. As a special case, although it is not a generator,
+ the final expression in an ``mdo``expression is considered to form a
+ segment by itself.
 data MyPoint = Point { x :: Int, y :: Int }
+Segments in this sense are related to *stronglyconnected components*
+analysis, with the exception that bindings in a segment cannot be
+reordered and must be contiguous.
Whilst a normal pattern synonym can be used in two ways, there are then seven
ways in which to use ``Point``. Precisely the ways in which a normal record
constructor can be used.
+Here is an example ``mdo``expression, and its translation to ``rec``
+blocks:
======================================= ==================================
Usage Example
======================================= ==================================
As a constructor ``zero = Point 0 0``
As a constructor with record syntax ``zero = Point { x = 0, y = 0}``
In a pattern context ``isZero (Point 0 0) = True``
In a pattern context with record syntax ``isZero (Point { x = 0, y = 0 }``
In a pattern context with field puns ``getX (Point {x}) = x``
In a record update ``(0, 0) { x = 1 } == (1,0)``
Using record selectors ``x (0,0) == 0``
======================================= ==================================
+::
For a unidirectional record pattern synonym we define record selectors but do
not allow record updates or construction.
+ mdo { a < getChar ===> do { a < getChar
+ ; b < f a c ; rec { b < f a c
+ ; c < f b a ; ; c < f b a }
+ ; z < h a b ; z < h a b
+ ; d < g d e ; rec { d < g d e
+ ; e < g a z ; ; e < g a z }
+ ; putChar c } ; putChar c }
The syntax and semantics of pattern synonyms are elaborated in the
following subsections. See the :ghcwiki:`Wiki page ` for more
details.
+Note that a given ``mdo`` expression can cause the creation of multiple
+``rec`` blocks. If there are no recursive dependencies, ``mdo`` will
+introduce no ``rec`` blocks. In this latter case an ``mdo`` expression
+is precisely the same as a ``do`` expression, as one would expect.
Syntax and scoping of pattern synonyms
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In summary, given an ``mdo`` expression, GHC first performs
+segmentation, introducing ``rec`` blocks to wrap over minimal recursive
+groups. Then, each resulting ``rec`` is desugared, using a call to
+``Control.Monad.Fix.mfix`` as described in the previous section. The
+original ``mdo``expression typechecks exactly when the desugared
+version would do so.
A pattern synonym declaration can be either unidirectional,
bidirectional or explicitly bidirectional.
The syntax for unidirectional pattern synonyms is: ::
+Here are some other important points in using the recursivedo notation:
 pattern pat_lhs < pat
+ It is enabled with the flag :ghcflag:`XRecursiveDo`, or the
+ ``LANGUAGE RecursiveDo`` pragma. (The same flag enables both
+ ``mdo``notation, and the use of ``rec`` blocks inside ``do``
+ expressions.)
the syntax for bidirectional pattern synonyms is: ::
+ ``rec`` blocks can also be used inside ``mdo``expressions, which
+ will be treated as a single statement. However, it is good style to
+ either use ``mdo`` or ``rec`` blocks in a single expression.
 pattern pat_lhs = pat
+ If recursive bindings are required for a monad, then that monad must
+ be declared an instance of the ``MonadFix`` class.
and the syntax for explicitly bidirectional pattern synonyms is: ::
+ The following instances of ``MonadFix`` are automatically provided:
+ List, Maybe, IO. Furthermore, the ``Control.Monad.ST`` and
+ ``Control.Monad.ST.Lazy`` modules provide the instances of the
+ ``MonadFix`` class for Haskell's internal state monad (strict and
+ lazy, respectively).
 pattern pat_lhs < pat where
 pat_lhs = expr
+ Like ``let`` and ``where`` bindings, name shadowing is not allowed
+ within an ``mdo``expression or a ``rec``block; that is, all the
+ names bound in a single ``rec`` must be distinct. (GHC will complain
+ if this is not the case.)
We can define either prefix, infix or record pattern synonyms by modifying
the form of `pat_lhs`. The syntax for these is as follows:
+.. _applicativedo:
======= ============================
Prefix ``Name args``
 
Infix ``arg1 `Name` arg2``
 or ``arg1 op arg2``
 
Record ``Name{arg1,arg2,...,argn}``
======= ============================
+Applicative donotation
+
+.. index::
+ single: Applicative donotation
+ single: donotation; Applicative
Pattern synonym declarations can only occur in the top level of a
module. In particular, they are not allowed as local definitions.
+.. ghcflag:: XApplicativeDo
The variables in the lefthand side of the definition are bound by the
pattern on the righthand side. For bidirectional pattern
synonyms, all the variables of the righthand side must also occur on
the lefthand side; also, wildcard patterns and view patterns are not
allowed. For unidirectional and explicitly bidirectional pattern
synonyms, there is no restriction on the righthand side pattern.
+ :since: 8.0.1
Pattern synonyms cannot be defined recursively.
+ Allow use of ``Applicative`` ``do`` notation.
.. _patsynimpexp:
+The language option :ghcflag:`XApplicativeDo` enables an alternative translation for
+the donotation, which uses the operators ``<$>``, ``<*>``, along with ``join``
+as far as possible. There are two main reasons for wanting to do this:
Import and export of pattern synonyms
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+ We can use donotation with types that are an instance of ``Applicative`` and
+ ``Functor``, but not ``Monad``
+ In some monads, using the applicative operators is more efficient than monadic
+ bind. For example, it may enable more parallelism.
The name of the pattern synonym is in the same namespace as proper data
constructors. Like normal data constructors, pattern synonyms can be imported
and exported through association with a type constructor or independently.
+Applicative donotation desugaring preserves the original semantics, provided
+that the ``Applicative`` instance satisfies ``<*> = ap`` and ``pure = return``
+(these are true of all the common monadic types). Thus, you can normally turn on
+:ghcflag:`XApplicativeDo` without fear of breaking your program. There is one pitfall
+to watch out for; see :ref:`applicativedopitfall`.
To export them on their own, in an export or import specification, you must
prefix pattern names with the ``pattern`` keyword, e.g.: ::
+There are no syntactic changes with :ghcflag:`XApplicativeDo`. The only way it shows
+up at the source level is that you can have a ``do`` expression that doesn't
+require a ``Monad`` constraint. For example, in GHCi: ::
 module Example (pattern Zero) where
+ Prelude> :set XApplicativeDo
+ Prelude> :t \m > do { x < m; return (not x) }
+ \m > do { x < m; return (not x) }
+ :: Functor f => f Bool > f Bool
 data MyNum = MkNum Int
+This example only requires ``Functor``, because it is translated into ``(\x >
+not x) <$> m``. A more complex example requires ``Applicative``, ::
 pattern Zero :: MyNum
 pattern Zero = MkNum 0
+ Prelude> :t \m > do { x < m 'a'; y < m 'b'; return (x  y) }
+ \m > do { x < m 'a'; y < m 'b'; return (x  y) }
+ :: Applicative f => (Char > f Bool) > f Bool
Without the ``pattern`` prefix, ``Zero`` would be interpreted as a
type constructor in the export list.
+Here GHC has translated the expression into ::
You may also use the ``pattern`` keyword in an import/export
specification to import or export an ordinary data constructor. For
example: ::
+ (\x y > x  y) <$> m 'a' <*> m 'b'
 import Data.Maybe( pattern Just )
+It is possible to see the actual translation by using :ghcflag:`ddumpds`, but be
+warned, the output is quite verbose.
would bring into scope the data constructor ``Just`` from the ``Maybe``
type, without also bringing the type constructor ``Maybe`` into scope.
+Note that if the expression can't be translated into uses of ``<$>``, ``<*>``
+only, then it will incur a ``Monad`` constraint as usual. This happens when
+there is a dependency on a value produced by an earlier statement in the
+``do``block: ::
To bundle a pattern synonym with a type constructor, we list the pattern
synonym in the export list of a module which exports the type constructor.
For example, to bundle ``Zero`` with ``MyNum`` we could write the following: ::
+ Prelude> :t \m > do { x < m True; y < m x; return (x  y) }
+ \m > do { x < m True; y < m x; return (x  y) }
+ :: Monad m => (Bool > m Bool) > m Bool
 module Example ( MyNum(Zero) ) where
+Here, ``m x`` depends on the value of ``x`` produced by the first statement, so
+the expression cannot be translated using ``<*>``.
If a module was then to import ``MyNum`` from ``Example``, it would also import
the pattern synonym ``Zero``.
+In general, the rule for when a ``do`` statement incurs a ``Monad`` constraint
+is as follows. If the doexpression has the following form: ::
It is also possible to use the special token ``..`` in an export list to mean
all currently bundled constructors. For example, we could write: ::
+ do p1 < E1; ...; pn < En; return E
 module Example ( MyNum(.., Zero) ) where
+where none of the variables defined by ``p1...pn`` are mentioned in ``E1...En``,
+then the expression will only require ``Applicative``. Otherwise, the expression
+will require ``Monad``.
in which case, ``Example`` would export the type constructor ``MyNum`` with
the data constructor ``MkNum`` and also the pattern synonym ``Zero``.
Bundled patterns synoyms are type checked to ensure that they are of the same
type as the type constructor which they are bundled with. A pattern synonym
``P`` can not be bundled with a type constructor ``T`` if ``P``\'s type is visibly
incompatible with ``T``.
+.. _applicativedopitfall:
A module which imports ``MyNum(..)`` from ``Example`` and then reexports
``MyNum(..)`` will also export any pattern synonyms bundled with ``MyNum`` in
``Example``. A more complete specification can be found on the
:ghcwiki:`wiki. `
+Things to watch out for
+~~~~~~~~~~~~~~~~~~~~~~~
Typing of pattern synonyms
~~~~~~~~~~~~~~~~~~~~~~~~~~
+Your code should just work as before when :ghcflag:`XApplicativeDo` is enabled,
+provided you use conventional ``Applicative`` instances. However, if you define
+a ``Functor`` or ``Applicative`` instance using donotation, then it will likely
+get turned into an infinite loop by GHC. For example, if you do this: ::
Given a pattern synonym definition of the form ::
+ instance Functor MyType where
+ fmap f m = do x < m; return (f x)
 pattern P var1 var2 ... varN < pat
+Then applicative desugaring will turn it into ::
it is assigned a *pattern type* of the form ::
+ instance Functor MyType where
+ fmap f m = fmap (\x > f x) m
 pattern P :: CReq => CProv => t1 > t2 > ... > tN > t
+And the program will loop at runtime. Similarly, an ``Applicative`` instance
+like this ::
where ⟨CProv⟩ and ⟨CReq⟩ are type contexts, and ⟨t1⟩, ⟨t2⟩, ..., ⟨tN⟩
and ⟨t⟩ are types. Notice the unusual form of the type, with two
contexts ⟨CProv⟩ and ⟨CReq⟩:
+ instance Applicative MyType where
+ pure = return
+ x <*> y = do f < x; a < y; return (f a)
 ⟨CProv⟩ are the constraints *made available (provided)* by a
 successful pattern match.
+will result in an infinte loop when ``<*>`` is called.
 ⟨CReq⟩ are the constraints *required* to match the pattern.
+Just as you wouldn't define a ``Monad`` instance using the donotation, you
+shouldn't define ``Functor`` or ``Applicative`` instance using donotation (when
+using ``ApplicativeDo``) either. The correct way to define these instances in
+terms of ``Monad`` is to use the ``Monad`` operations directly, e.g. ::
For example, consider ::
+ instance Functor MyType where
+ fmap f m = m >>= return . f
 data T a where
 MkT :: (Show b) => a > b > T a
+ instance Applicative MyType where
+ pure = return
+ (<*>) = ap
 f1 :: (Eq a, Num a) => T a > String
 f1 (MkT 42 x) = show x
 pattern ExNumPat :: (Num a, Eq a) => (Show b) => b > T a
 pattern ExNumPat x = MkT 42 x
+.. _parallellistcomprehensions:
 f2 :: (Eq a, Num a) => T a > String
 f2 (ExNumPat x) = show x
+Parallel List Comprehensions
+
Here ``f1`` does not use pattern synonyms. To match against the numeric
pattern ``42`` *requires* the caller to satisfy the constraints
``(Num a, Eq a)``, so they appear in ``f1``'s type. The call to ``show``
generates a ``(Show b)`` constraint, where ``b`` is an existentially
type variable bound by the pattern match on ``MkT``. But the same
pattern match also *provides* the constraint ``(Show b)`` (see ``MkT``'s
type), and so all is well.
+.. index::
+ single: list comprehensions; parallel
+ single: parallel list comprehensions
Exactly the same reasoning applies to ``ExNumPat``: matching against
``ExNumPat`` *requires* the constraints ``(Num a, Eq a)``, and
*provides* the constraint ``(Show b)``.
+.. ghcflag:: XParallelListComp
Note also the following points
+ Allow parallel list comprehension syntax.
 In the common case where ``Prov`` is empty, ``()``, it can be omitted
 altogether.
+Parallel list comprehensions are a natural extension to list
+comprehensions. List comprehensions can be thought of as a nice syntax
+for writing maps and filters. Parallel comprehensions extend this to
+include the ``zipWith`` family.
 You may specify an explicit *pattern signature*, as we did for
 ``ExNumPat`` above, to specify the type of a pattern, just as you can
 for a function. As usual, the type signature can be less polymorphic
 than the inferred type. For example
+A parallel list comprehension has multiple independent branches of
+qualifier lists, each separated by a ```` symbol. For example, the
+following zips together two lists: ::
 ::
+ [ (x, y)  x < xs  y < ys ]
  Inferred type would be 'a > [a]'
 pattern SinglePair :: (a, a) > [(a, a)]
 pattern SinglePair x = [x]
+The behaviour of parallel list comprehensions follows that of zip, in
+that the resulting list will have the same length as the shortest
+branch.
 The GHCi :ghcicmd:`:info` command shows pattern types in this format.
+We can define parallel list comprehensions by translation to regular
+comprehensions. Here's the basic idea:
 For a bidirectional pattern synonym, a use of the pattern synonym as
 an expression has the type
+Given a parallel comprehension of the form: ::
 ::
+ [ e  p1 < e11, p2 < e12, ...
+  q1 < e21, q2 < e22, ...
+ ...
+ ]
 (CReq, CProv) => t1 > t2 > ... > tN > t
+This will be translated to: ::
 So in the previous example, when used in an expression, ``ExNumPat``
 has type
+ [ e  ((p1,p2), (q1,q2), ...) < zipN [(p1,p2)  p1 < e11, p2 < e12, ...]
+ [(q1,q2)  q1 < e21, q2 < e22, ...]
+ ...
+ ]
 ::
+where ``zipN`` is the appropriate zip for the given number of branches.
 ExNumPat :: (Num a, Eq a, Show b) => b > T t
+.. _generalisedlistcomprehensions:
 Notice that this is a tiny bit more restrictive than the expression
 ``MkT 42 x`` which would not require ``(Eq a)``.
+Generalised (SQLlike) List Comprehensions
+
 Consider these two pattern synonyms: ::
+.. index::
+ single: list comprehensions; generalised
+ single: extended list comprehensions
+ single: group
+ single: SQL
 data S a where
 S1 :: Bool > S Bool
+.. ghcflag:: XTransformListComp
 pattern P1 :: Bool > Maybe Bool
 pattern P1 b = Just b
+ Allow use of generalised list (SQLlike) comprehension syntax. This
+ introduces the ``group``, ``by``, and ``using`` keywords.
 pattern P2 :: () => (b ~ Bool) => Bool > S b
 pattern P2 b = S1 b
+Generalised list comprehensions are a further enhancement to the list
+comprehension syntactic sugar to allow operations such as sorting and
+grouping which are familiar from SQL. They are fully described in the
+paper `Comprehensive comprehensions: comprehensions with "order by" and
+"group by" `__,
+except that the syntax we use differs slightly from the paper.
 f :: Maybe a > String
 f (P1 x) = "no no no"  Typeincorrect
+The extension is enabled with the flag :ghcflag:`XTransformListComp`.
 g :: S a > String
 g (P2 b) = "yes yes yes"  Fine
+Here is an example:
 Pattern ``P1`` can only match against a value of type ``Maybe Bool``,
 so function ``f`` is rejected because the type signature is
 ``Maybe a``. (To see this, imagine expanding the pattern synonym.)
+::
 On the other hand, function ``g`` works fine, because matching
 against ``P2`` (which wraps the GADT ``S``) provides the local
 equality ``(a~Bool)``. If you were to give an explicit pattern
 signature ``P2 :: Bool > S Bool``, then ``P2`` would become less
 polymorphic, and would behave exactly like ``P1`` so that ``g`` would
 then be rejected.
+ employees = [ ("Simon", "MS", 80)
+ , ("Erik", "MS", 100)
+ , ("Phil", "Ed", 40)
+ , ("Gordon", "Ed", 45)
+ , ("Paul", "Yale", 60) ]
 In short, if you want GADTlike behaviour for pattern synonyms, then
 (unlike unlike concrete data constructors like ``S1``) you must write
 its type with explicit provided equalities. For a concrete data
 constructor like ``S1`` you can write its type signature as either
 ``S1 :: Bool > S Bool`` or ``S1 :: (b~Bool) => Bool > S b``; the
 two are equivalent. Not so for pattern synonyms: the two forms are
 different, in order to distinguish the two cases above. (See
 :ghcticket:`9953` for discussion of this choice.)
+ output = [ (the dept, sum salary)
+  (name, dept, salary) < employees
+ , then group by dept using groupWith
+ , then sortWith by (sum salary)
+ , then take 5 ]
Matching of pattern synonyms
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In this example, the list ``output`` would take on the value:
A pattern synonym occurrence in a pattern is evaluated by first matching
against the pattern synonym itself, and then on the argument patterns.
For example, in the following program, ``f`` and ``f'`` are equivalent: ::
+::
 pattern Pair x y < [x, y]
+ [("Yale", 60), ("Ed", 85), ("MS", 180)]
 f (Pair True True) = True
 f _ = False
+There are three new keywords: ``group``, ``by``, and ``using``. (The
+functions ``sortWith`` and ``groupWith`` are not keywords; they are
+ordinary functions that are exported by ``GHC.Exts``.)
 f' [x, y]  True < x, True < y = True
 f' _ = False
+There are five new forms of comprehension qualifier, all introduced by
+the (existing) keyword ``then``:
Note that the strictness of ``f`` differs from that of ``g`` defined
below:
+ ::
.. codeblock:: none
+ then f
 g [True, True] = True
 g _ = False
+ This statement requires that
+ f
+ have the type
+ forall a. [a] > [a]
+ . You can see an example of its use in the motivating example, as
+ this form is used to apply
+ take 5
+ .
+ ::
 *Main> f (False:undefined)
 *** Exception: Prelude.undefined
 *Main> g (False:undefined)
 False
+ then f by e
.. _nkpatterns:
+ This form is similar to the previous one, but allows you to create a
+ function which will be passed as the first argument to f. As a
+ consequence f must have the type
+ ``forall a. (a > t) > [a] > [a]``. As you can see from the type,
+ this function lets f "project out" some information from the elements
+ of the list it is transforming.
n+k patterns

+ An example is shown in the opening example, where ``sortWith`` is
+ supplied with a function that lets it find out the ``sum salary`` for
+ any item in the list comprehension it transforms.
.. ghcflag:: XNPlusKPatterns
+ ::
 Enable use of ``n+k`` patterns.
+ then group by e using f
.. _recursivedonotation:
+ This is the most general of the groupingtype statements. In this
+ form, f is required to have type
+ ``forall a. (a > t) > [a] > [[a]]``. As with the ``then f by e``
+ case above, the first argument is a function supplied to f by the
+ compiler which lets it compute e on every element of the list being
+ transformed. However, unlike the nongrouping case, f additionally
+ partitions the list into a number of sublists: this means that at
+ every point after this statement, binders occurring before it in the
+ comprehension refer to *lists* of possible values, not single values.
+ To help understand this, let's look at an example:
The recursive donotation

+ ::
.. ghcflag:: XRecursiveDo
+  This works similarly to groupWith in GHC.Exts, but doesn't sort its input first
+ groupRuns :: Eq b => (a > b) > [a] > [[a]]
+ groupRuns f = groupBy (\x y > f x == f y)
 Allow the use of recursive ``do`` notation.
+ output = [ (the x, y)
+  x < ([1..3] ++ [1..2])
+ , y < [4..6]
+ , then group by x using groupRuns ]
The donotation of Haskell 98 does not allow *recursive bindings*, that
is, the variables bound in a doexpression are visible only in the
textually following code block. Compare this to a letexpression, where
bound variables are visible in the entire binding group.
+ This results in the variable ``output`` taking on the value below:
It turns out that such recursive bindings do indeed make sense for a
variety of monads, but not all. In particular, recursion in this sense
requires a fixedpoint operator for the underlying monad, captured by
the ``mfix`` method of the ``MonadFix`` class, defined in
``Control.Monad.Fix`` as follows: ::
+ ::
 class Monad m => MonadFix m where
 mfix :: (a > m a) > m a
+ [(1, [4, 5, 6]), (2, [4, 5, 6]), (3, [4, 5, 6]), (1, [4, 5, 6]), (2, [4, 5, 6])]
Haskell's ``Maybe``, ``[]`` (list), ``ST`` (both strict and lazy
versions), ``IO``, and many other monads have ``MonadFix`` instances. On
the negative side, the continuation monad, with the signature
``(a > r) > r``, does not.
+ Note that we have used the ``the`` function to change the type of x
+ from a list to its original numeric type. The variable y, in
+ contrast, is left unchanged from the list form introduced by the
+ grouping.
For monads that do belong to the ``MonadFix`` class, GHC provides an
extended version of the donotation that allows recursive bindings. The
:ghcflag:`XRecursiveDo` (language pragma: ``RecursiveDo``) provides the
necessary syntactic support, introducing the keywords ``mdo`` and
``rec`` for higher and lower levels of the notation respectively. Unlike
bindings in a ``do`` expression, those introduced by ``mdo`` and ``rec``
are recursively defined, much like in an ordinary letexpression. Due to
the new keyword ``mdo``, we also call this notation the *mdonotation*.
+ ::
Here is a simple (albeit contrived) example:
+ then group using f
::
+ With this form of the group statement, f is required to simply have
+ the type ``forall a. [a] > [[a]]``, which will be used to group up
+ the comprehension so far directly. An example of this form is as
+ follows:
 {# LANGUAGE RecursiveDo #}
 justOnes = mdo { xs < Just (1:xs)
 ; return (map negate xs) }
+ ::
or equivalently
+ output = [ x
+  y < [1..5]
+ , x < "hello"
+ , then group using inits]
::
+ This will yield a list containing every prefix of the word "hello"
+ written out 5 times:
 {# LANGUAGE RecursiveDo #}
 justOnes = do { rec { xs < Just (1:xs) }
 ; return (map negate xs) }
+ ::
As you can guess ``justOnes`` will evaluate to ``Just [1,1,1,...``.
+ ["","h","he","hel","hell","hello","helloh","hellohe","hellohel","hellohell","hellohello","hellohelloh",...]
GHC's implementation the mdonotation closely follows the original
translation as described in the paper `A recursive do for
Haskell `__, which
in turn is based on the work `Value Recursion in Monadic
Computations `__.
Furthermore, GHC extends the syntax described in the former paper with a
lower level syntax flagged by the ``rec`` keyword, as we describe next.
+.. _monadcomprehensions:
Recursive binding groups
~~~~~~~~~~~~~~~~~~~~~~~~
+Monad comprehensions
+
The flag :ghcflag:`XRecursiveDo` also introduces a new keyword ``rec``, which
wraps a mutuallyrecursive group of monadic statements inside a ``do``
expression, producing a single statement. Similar to a ``let`` statement
inside a ``do``, variables bound in the ``rec`` are visible throughout
the ``rec`` group, and below it. For example, compare
+.. index::
+ single: monad comprehensions
::
+Monad comprehensions generalise the list comprehension notation,
+including parallel comprehensions (:ref:`parallellistcomprehensions`)
+and transform comprehensions (:ref:`generalisedlistcomprehensions`) to
+work for any monad.
 do { a < getChar do { a < getChar
 ; let { r1 = f a r2 ; rec { r1 < f a r2
 ; ; r2 = g r1 } ; ; r2 < g r1 }
 ; return (r1 ++ r2) } ; return (r1 ++ r2) }
+Monad comprehensions support:
In both cases, ``r1`` and ``r2`` are available both throughout the
``let`` or ``rec`` block, and in the statements that follow it. The
difference is that ``let`` is nonmonadic, while ``rec`` is monadic. (In
Haskell ``let`` is really ``letrec``, of course.)
+ Bindings: ::
The semantics of ``rec`` is fairly straightforward. Whenever GHC finds a
``rec`` group, it will compute its set of bound variables, and will
introduce an appropriate call to the underlying monadic valuerecursion
operator ``mfix``, belonging to the ``MonadFix`` class. Here is an
example:
+ [ x + y  x < Just 1, y < Just 2 ]
::
+ Bindings are translated with the ``(>>=)`` and ``return`` functions
+ to the usual donotation: ::
 rec { b < f a c ===> (b,c) < mfix (\ ~(b,c) > do { b < f a c
 ; c < f b a } ; c < f b a
 ; return (b,c) })
+ do x < Just 1
+ y < Just 2
+ return (x+y)
As usual, the metavariables ``b``, ``c`` etc., can be arbitrary
patterns. In general, the statement ``rec ss`` is desugared to the
statement
+ Guards: ::
::
+ [ x  x < [1..10], x <= 5 ]
 vs < mfix (\ ~vs > do { ss; return vs })
+ Guards are translated with the ``guard`` function, which requires a
+ ``MonadPlus`` instance: ::
where ``vs`` is a tuple of the variables bound by ``ss``.
+ do x < [1..10]
+ guard (x <= 5)
+ return x
Note in particular that the translation for a ``rec`` block only
involves wrapping a call to ``mfix``: it performs no other analysis on
the bindings. The latter is the task for the ``mdo`` notation, which is
described next.

The ``mdo`` notation
~~~~~~~~~~~~~~~~~~~~

A ``rec``block tells the compiler where precisely the recursive knot
should be tied. It turns out that the placement of the recursive knots
can be rather delicate: in particular, we would like the knots to be
wrapped around as minimal groups as possible. This process is known as
*segmentation*, and is described in detail in Section 3.2 of `A
recursive do for
Haskell `__.
Segmentation improves polymorphism and reduces the size of the recursive
knot. Most importantly, it avoids unnecessary interference caused by a
fundamental issue with the socalled *rightshrinking* axiom for monadic
recursion. In brief, most monads of interest (IO, strict state, etc.) do
*not* have recursion operators that satisfy this axiom, and thus not
performing segmentation can cause unnecessary interference, changing the
termination behavior of the resulting translation. (Details can be found
in Sections 3.1 and 7.2.2 of `Value Recursion in Monadic
Computations `__.)

The ``mdo`` notation removes the burden of placing explicit ``rec``
blocks in the code. Unlike an ordinary ``do`` expression, in which
variables bound by statements are only in scope for later statements,
variables bound in an ``mdo`` expression are in scope for all statements
of the expression. The compiler then automatically identifies minimal
mutually recursively dependent segments of statements, treating them as
if the user had wrapped a ``rec`` qualifier around them.

The definition is syntactic:

 A generator ⟨g⟩ *depends* on a textually following generator ⟨g'⟩, if

  ⟨g'⟩ defines a variable that is used by ⟨g⟩, or

  ⟨g'⟩ textually appears between ⟨g⟩ and ⟨g''⟩, where ⟨g⟩ depends on
 ⟨g''⟩.
+ Transform statements (as with :ghcflag:`XTransformListComp`): ::
 A *segment* of a given ``mdo``expression is a minimal sequence of
 generators such that no generator of the sequence depends on an
 outside generator. As a special case, although it is not a generator,
 the final expression in an ``mdo``expression is considered to form a
 segment by itself.
+ [ x+y  x < [1..10], y < [1..x], then take 2 ]
Segments in this sense are related to *stronglyconnected components*
analysis, with the exception that bindings in a segment cannot be
reordered and must be contiguous.
+ This translates to: ::
Here is an example ``mdo``expression, and its translation to ``rec``
blocks:
+ do (x,y) < take 2 (do x < [1..10]
+ y < [1..x]
+ return (x,y))
+ return (x+y)
::
+ Group statements (as with :ghcflag:`XTransformListComp`):
 mdo { a < getChar ===> do { a < getChar
 ; b < f a c ; rec { b < f a c
 ; c < f b a ; ; c < f b a }
 ; z < h a b ; z < h a b
 ; d < g d e ; rec { d < g d e
 ; e < g a z ; ; e < g a z }
 ; putChar c } ; putChar c }
+ ::
Note that a given ``mdo`` expression can cause the creation of multiple
``rec`` blocks. If there are no recursive dependencies, ``mdo`` will
introduce no ``rec`` blocks. In this latter case an ``mdo`` expression
is precisely the same as a ``do`` expression, as one would expect.
+ [ x  x < [1,1,2,2,3], then group by x using GHC.Exts.groupWith ]
+ [ x  x < [1,1,2,2,3], then group using myGroup ]
In summary, given an ``mdo`` expression, GHC first performs
segmentation, introducing ``rec`` blocks to wrap over minimal recursive
groups. Then, each resulting ``rec`` is desugared, using a call to
``Control.Monad.Fix.mfix`` as described in the previous section. The
original ``mdo``expression typechecks exactly when the desugared
version would do so.
+ Parallel statements (as with :ghcflag:`XParallelListComp`):
Here are some other important points in using the recursivedo notation:
+ ::
 It is enabled with the flag :ghcflag:`XRecursiveDo`, or the
 ``LANGUAGE RecursiveDo`` pragma. (The same flag enables both
 ``mdo``notation, and the use of ``rec`` blocks inside ``do``
 expressions.)
+ [ (x+y)  x < [1..10]
+  y < [11..20]
+ ]
 ``rec`` blocks can also be used inside ``mdo``expressions, which
 will be treated as a single statement. However, it is good style to
 either use ``mdo`` or ``rec`` blocks in a single expression.
+ Parallel statements are translated using the ``mzip`` function, which
+ requires a ``MonadZip`` instance defined in
+ :baseref:`Control.Monad.Zip `:
 If recursive bindings are required for a monad, then that monad must
 be declared an instance of the ``MonadFix`` class.
+ ::
 The following instances of ``MonadFix`` are automatically provided:
 List, Maybe, IO. Furthermore, the ``Control.Monad.ST`` and
 ``Control.Monad.ST.Lazy`` modules provide the instances of the
 ``MonadFix`` class for Haskell's internal state monad (strict and
 lazy, respectively).
+ do (x,y) < mzip (do x < [1..10]
+ return x)
+ (do y < [11..20]
+ return y)
+ return (x+y)
 Like ``let`` and ``where`` bindings, name shadowing is not allowed
 within an ``mdo``expression or a ``rec``block; that is, all the
 names bound in a single ``rec`` must be distinct. (GHC will complain
 if this is not the case.)
+All these features are enabled by default if the ``MonadComprehensions``
+extension is enabled. The types and more detailed examples on how to use
+comprehensions are explained in the previous chapters
+:ref:`generalisedlistcomprehensions` and
+:ref:`parallellistcomprehensions`. In general you just have to replace
+the type ``[a]`` with the type ``Monad m => m a`` for monad
+comprehensions.
.. _applicativedo:
+.. note::
+ Even though most of these examples are using the list monad, monad
+ comprehensions work for any monad. The ``base`` package offers all
+ necessary instances for lists, which make ``MonadComprehensions``
+ backward compatible to builtin, transform and parallel list
+ comprehensions.
Applicative donotation

+More formally, the desugaring is as follows. We write ``D[ e  Q]`` to
+mean the desugaring of the monad comprehension ``[ e  Q]``:
.. index::
 single: Applicative donotation
 single: donotation; Applicative
+::
.. ghcflag:: XApplicativeDo
+ Expressions: e
+ Declarations: d
+ Lists of qualifiers: Q,R,S
 :since: 8.0.1
+  Basic forms
+ D[ e  ] = return e
+ D[ e  p < e, Q ] = e >>= \p > D[ e  Q ]
+ D[ e  e, Q ] = guard e >> \p > D[ e  Q ]
+ D[ e  let d, Q ] = let d in D[ e  Q ]
 Allow use of ``Applicative`` ``do`` notation.
+  Parallel comprehensions (iterate for multiple parallel branches)
+ D[ e  (Q  R), S ] = mzip D[ Qv  Q ] D[ Rv  R ] >>= \(Qv,Rv) > D[ e  S ]
The language option :ghcflag:`XApplicativeDo` enables an alternative translation for
the donotation, which uses the operators ``<$>``, ``<*>``, along with ``join``
as far as possible. There are two main reasons for wanting to do this:
+  Transform comprehensions
+ D[ e  Q then f, R ] = f D[ Qv  Q ] >>= \Qv > D[ e  R ]
 We can use donotation with types that are an instance of ``Applicative`` and
 ``Functor``, but not ``Monad``
 In some monads, using the applicative operators is more efficient than monadic
 bind. For example, it may enable more parallelism.
+ D[ e  Q then f by b, R ] = f (\Qv > b) D[ Qv  Q ] >>= \Qv > D[ e  R ]
Applicative donotation desugaring preserves the original semantics, provided
that the ``Applicative`` instance satisfies ``<*> = ap`` and ``pure = return``
(these are true of all the common monadic types). Thus, you can normally turn on
:ghcflag:`XApplicativeDo` without fear of breaking your program. There is one pitfall
to watch out for; see :ref:`applicativedopitfall`.
+ D[ e  Q then group using f, R ] = f D[ Qv  Q ] >>= \ys >
+ case (fmap selQv1 ys, ..., fmap selQvn ys) of
+ Qv > D[ e  R ]
There are no syntactic changes with :ghcflag:`XApplicativeDo`. The only way it shows
up at the source level is that you can have a ``do`` expression that doesn't
require a ``Monad`` constraint. For example, in GHCi: ::
+ D[ e  Q then group by b using f, R ] = f (\Qv > b) D[ Qv  Q ] >>= \ys >
+ case (fmap selQv1 ys, ..., fmap selQvn ys) of
+ Qv > D[ e  R ]
 Prelude> :set XApplicativeDo
 Prelude> :t \m > do { x < m; return (not x) }
 \m > do { x < m; return (not x) }
 :: Functor f => f Bool > f Bool
+ where Qv is the tuple of variables bound by Q (and used subsequently)
+ selQvi is a selector mapping Qv to the ith component of Qv
This example only requires ``Functor``, because it is translated into ``(\x >
not x) <$> m``. A more complex example requires ``Applicative``, ::
+ Operator Standard binding Expected type
+ 
+ return GHC.Base t1 > m t2
+ (>>=) GHC.Base m1 t1 > (t2 > m2 t3) > m3 t3
+ (>>) GHC.Base m1 t1 > m2 t2 > m3 t3
+ guard Control.Monad t1 > m t2
+ fmap GHC.Base forall a b. (a>b) > n a > n b
+ mzip Control.Monad.Zip forall a b. m a > m b > m (a,b)
 Prelude> :t \m > do { x < m 'a'; y < m 'b'; return (x  y) }
 \m > do { x < m 'a'; y < m 'b'; return (x  y) }
 :: Applicative f => (Char > f Bool) > f Bool
+The comprehension should typecheck when its desugaring would typecheck,
+except that (as discussed in :ref:`generalisedlistcomprehensions`) in the
+"then ``f``" and "then group using ``f``" clauses, when the "by ``b``" qualifier
+is omitted, argument ``f`` should have a polymorphic type. In particular, "then
+``Data.List.sort``" and "then group using ``Data.List.group``" are
+insufficiently polymorphic.
Here GHC has translated the expression into ::
+Monad comprehensions support rebindable syntax
+(:ref:`rebindablesyntax`). Without rebindable syntax, the operators
+from the "standard binding" module are used; with rebindable syntax, the
+operators are looked up in the current lexical scope. For example,
+parallel comprehensions will be typechecked and desugared using whatever
+"``mzip``" is in scope.
 (\x y > x  y) <$> m 'a' <*> m 'b'
+The rebindable operators must have the "Expected type" given in the
+table above. These types are surprisingly general. For example, you can
+use a bind operator with the type
It is possible to see the actual translation by using :ghcflag:`ddumpds`, but be
warned, the output is quite verbose.
+::
Note that if the expression can't be translated into uses of ``<$>``, ``<*>``
only, then it will incur a ``Monad`` constraint as usual. This happens when
there is a dependency on a value produced by an earlier statement in the
``do``block: ::
+ (>>=) :: T x y a > (a > T y z b) > T x z b
 Prelude> :t \m > do { x < m True; y < m x; return (x  y) }
 \m > do { x < m True; y < m x; return (x  y) }
 :: Monad m => (Bool > m Bool) > m Bool
+In the case of transform comprehensions, notice that the groups are
+parameterised over some arbitrary type ``n`` (provided it has an
+``fmap``, as well as the comprehension being over an arbitrary monad.
Here, ``m x`` depends on the value of ``x`` produced by the first statement, so
the expression cannot be translated using ``<*>``.
+.. _monadfaildesugaring:
In general, the rule for when a ``do`` statement incurs a ``Monad`` constraint
is as follows. If the doexpression has the following form: ::
+New monadic failure desugaring mechanism
+
 do p1 < E1; ...; pn < En; return E
+.. ghcflag:: XMonadFailDesugaring
where none of the variables defined by ``p1...pn`` are mentioned in ``E1...En``,
then the expression will only require ``Applicative``. Otherwise, the expression
will require ``Monad``.
+ :since: 8.0.1
+ Use the ``MonadFail.fail`` instead of the legacy ``Monad.fail`` function
+ when desugaring refutable patterns in ``do`` blocks.
.. _applicativedopitfall:
+The ``XMonadFailDesugaring`` extension switches the desugaring of
+``do``blocks to use ``MonadFail.fail`` instead of ``Monad.fail``. This will
+eventually be the default behaviour in a future GHC release, under the
+`MonadFail Proposal (MFP)
+`__.
Things to watch out for
~~~~~~~~~~~~~~~~~~~~~~~
+This extension is temporary, and will be deprecated in a future release. It is
+included so that library authors have a hard check for whether their code
+will work with future GHC versions.
Your code should just work as before when :ghcflag:`XApplicativeDo` is enabled,
provided you use conventional ``Applicative`` instances. However, if you define
a ``Functor`` or ``Applicative`` instance using donotation, then it will likely
get turned into an infinite loop by GHC. For example, if you do this: ::
+.. _rebindablesyntax:
 instance Functor MyType where
 fmap f m = do x < m; return (f x)
+Rebindable syntax and the implicit Prelude import
+
Then applicative desugaring will turn it into ::
+.. ghcflag:: XNoImplicitPrelude
 instance Functor MyType where
 fmap f m = fmap (\x > f x) m
+ Don't import ``Prelude`` by default.
And the program will loop at runtime. Similarly, an ``Applicative`` instance
like this ::
+GHC normally imports ``Prelude.hi`` files for
+you. If you'd rather it didn't, then give it a ``XNoImplicitPrelude``
+option. The idea is that you can then import a Prelude of your own. (But
+don't call it ``Prelude``; the Haskell module namespace is flat, and you
+must not conflict with any Prelude module.)
 instance Applicative MyType where
 pure = return
 x <*> y = do f < x; a < y; return (f a)
+.. ghcflag:: XRebindableSyntax
will result in an infinte loop when ``<*>`` is called.
+ :implies: :ghcflag:`XNoImplicitPrelude`
+ :since: 7.0.1
Just as you wouldn't define a ``Monad`` instance using the donotation, you
shouldn't define ``Functor`` or ``Applicative`` instance using donotation (when
using ``ApplicativeDo``) either. The correct way to define these instances in
terms of ``Monad`` is to use the ``Monad`` operations directly, e.g. ::
+ Enable rebinding of a variety of usuallybuiltin operations.
 instance Functor MyType where
 fmap f m = m >>= return . f
+Suppose you are importing a Prelude of your own in order to define your
+own numeric class hierarchy. It completely defeats that purpose if the
+literal "1" means "``Prelude.fromInteger 1``", which is what the Haskell
+Report specifies. So the :ghcflag:`XRebindableSyntax` flag causes the
+following pieces of builtin syntax to refer to *whatever is in scope*,
+not the Prelude versions:
 instance Applicative MyType where
 pure = return
 (<*>) = ap
+ 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
+ translation is ``fromRational (3.68::Rational)``.
.. _parallellistcomprehensions:
+ The equality test in an overloaded numeric pattern uses whatever
+ ``(==)`` is in scope.
Parallel List Comprehensions

+ The subtraction operation, and the greaterthanorequal test, in
+ ``n+k`` patterns use whatever ``()`` and ``(>=)`` are in scope.
.. index::
 single: list comprehensions; parallel
 single: parallel list comprehensions
+ Negation (e.g. "`` (f x)``") means "``negate (f x)``", both in
+ numeric patterns, and expressions.
.. ghcflag:: XParallelListComp
+ Conditionals (e.g. "``if`` e1 ``then`` e2 ``else`` e3") means
+ "``ifThenElse`` e1 e2 e3". However ``case`` expressions are
+ unaffected.
 Allow parallel list comprehension syntax.
+ "Do" notation is translated using whatever functions ``(>>=)``,
+ ``(>>)``, and ``fail``, are in scope (not the Prelude versions). List
+ comprehensions, ``mdo`` (:ref:`recursivedonotation`), and parallel
+ array comprehensions, are unaffected.
Parallel list comprehensions are a natural extension to list
comprehensions. List comprehensions can be thought of as a nice syntax
for writing maps and filters. Parallel comprehensions extend this to
include the ``zipWith`` family.
+ Arrow notation (see :ref:`arrownotation`) uses whatever ``arr``,
+ ``(>>>)``, ``first``, ``app``, ``()`` and ``loop`` functions are
+ in scope. But unlike the other constructs, the types of these
+ functions must match the Prelude types very closely. Details are in
+ flux; if you want to use this, ask!
A parallel list comprehension has multiple independent branches of
qualifier lists, each separated by a ```` symbol. For example, the
following zips together two lists: ::
+:ghcflag:`XRebindableSyntax` implies :ghcflag:`XNoImplicitPrelude`.
 [ (x, y)  x < xs  y < ys ]
+In all cases (apart from arrow notation), the static semantics should be
+that of the desugared form, even if that is a little unexpected. For
+example, the static semantics of the literal ``368`` is exactly that of
+``fromInteger (368::Integer)``; it's fine for ``fromInteger`` to have
+any of the types: ::
The behaviour of parallel list comprehensions follows that of zip, in
that the resulting list will have the same length as the shortest
branch.
+ fromInteger :: Integer > Integer
+ fromInteger :: forall a. Foo a => Integer > a
+ fromInteger :: Num a => a > Integer
+ fromInteger :: Integer > Bool > Bool
We can define parallel list comprehensions by translation to regular
comprehensions. Here's the basic idea:
+Be warned: this is an experimental facility, with fewer checks than
+usual. Use ``dcorelint`` to typecheck the desugared program. If Core
+Lint is happy you should be all right.
Given a parallel comprehension of the form: ::
+.. _postfixoperators:
 [ e  p1 < e11, p2 < e12, ...
  q1 < e21, q2 < e22, ...
 ...
 ]
+Postfix operators
+
This will be translated to: ::
+.. ghcflag:: XPostfixOperators
 [ e  ((p1,p2), (q1,q2), ...) < zipN [(p1,p2)  p1 < e11, p2 < e12, ...]
 [(q1,q2)  q1 < e21, q2 < e22, ...]
 ...
 ]
+ Allow the use of postfix operators
where ``zipN`` is the appropriate zip for the given number of branches.
+The :ghcflag:`XPostfixOperators` flag enables a small extension to the syntax
+of left operator sections, which allows you to define postfix operators.
+The extension is this: the left section ::
.. _generalisedlistcomprehensions:
+ (e !)
Generalised (SQLlike) List Comprehensions

+is equivalent (from the point of view of both type checking and
+execution) to the expression ::
.. index::
 single: list comprehensions; generalised
 single: extended list comprehensions
 single: group
 single: SQL
+ ((!) e)
.. ghcflag:: XTransformListComp
+(for any expression ``e`` and operator ``(!)``. The strict Haskell 98
+interpretation is that the section is equivalent to ::
 Allow use of generalised list (SQLlike) comprehension syntax. This
 introduces the ``group``, ``by``, and ``using`` keywords.
+ (\y > (!) e y)
Generalised list comprehensions are a further enhancement to the list
comprehension syntactic sugar to allow operations such as sorting and
grouping which are familiar from SQL. They are fully described in the
paper `Comprehensive comprehensions: comprehensions with "order by" and
"group by" `__,
except that the syntax we use differs slightly from the paper.
+That is, the operator must be a function of two arguments. GHC allows it
+to take only one argument, and that in turn allows you to write the
+function postfix.
The extension is enabled with the flag :ghcflag:`XTransformListComp`.
+The extension does not extend to the lefthand side of function
+definitions; you must define such a function in prefix form.
Here is an example:
+.. _tuplesections:
::
+Tuple sections
+
 employees = [ ("Simon", "MS", 80)
 , ("Erik", "MS", 100)
 , ("Phil", "Ed", 40)
 , ("Gordon", "Ed", 45)
 , ("Paul", "Yale", 60) ]
+.. ghcflag:: XTupleSections
 output = [ (the dept, sum salary)
  (name, dept, salary) < employees
 , then group by dept using groupWith
 , then sortWith by (sum salary)
 , then take 5 ]
+ Allow the use of tuple section syntax
In this example, the list ``output`` would take on the value:
+The :ghcflag:`XTupleSections` flag enables Pythonstyle partially applied
+tuple constructors. For example, the following program ::
::
+ (, True)
 [("Yale", 60), ("Ed", 85), ("MS", 180)]
+is considered to be an alternative notation for the more unwieldy
+alternative ::
There are three new keywords: ``group``, ``by``, and ``using``. (The
functions ``sortWith`` and ``groupWith`` are not keywords; they are
ordinary functions that are exported by ``GHC.Exts``.)
+ \x > (x, True)
There are five new forms of comprehension qualifier, all introduced by
the (existing) keyword ``then``:
+You can omit any combination of arguments to the tuple, as in the
+following ::
 ::
+ (, "I", , , "Love", , 1337)
 then f
+which translates to ::
 This statement requires that
 f
 have the type
 forall a. [a] > [a]
 . You can see an example of its use in the motivating example, as
 this form is used to apply
 take 5
 .
 ::
+ \a b c d > (a, "I", b, c, "Love", d, 1337)
 then f by e
+If you have `unboxed tuples <#unboxedtuples>`__ enabled, tuple sections
+will also be available for them, like so ::
 This form is similar to the previous one, but allows you to create a
 function which will be passed as the first argument to f. As a
 consequence f must have the type
 ``forall a. (a > t) > [a] > [a]``. As you can see from the type,
 this function lets f "project out" some information from the elements
 of the list it is transforming.
+ (# , True #)
 An example is shown in the opening example, where ``sortWith`` is
 supplied with a function that lets it find out the ``sum salary`` for
 any item in the list comprehension it transforms.
+Because there is no unboxed unit tuple, the following expression ::
 ::
+ (# #)
 then group by e using f
+continues to stand for the unboxed singleton tuple data constructor.
 This is the most general of the groupingtype statements. In this
 form, f is required to have type
 ``forall a. (a > t) > [a] > [[a]]``. As with the ``then f by e``
 case above, the first argument is a function supplied to f by the
 compiler which lets it compute e on every element of the list being
 transformed. However, unlike the nongrouping case, f additionally
 partitions the list into a number of sublists: this means that at
 every point after this statement, binders occurring before it in the
 comprehension refer to *lists* of possible values, not single values.
 To help understand this, let's look at an example:
+.. _lambdacase:
 ::
+Lambdacase
+
  This works similarly to groupWith in GHC.Exts, but doesn't sort its input first
 groupRuns :: Eq b => (a > b) > [a] > [[a]]
 groupRuns f = groupBy (\x y > f x == f y)
+.. ghcflag:: XLambdaCase
 output = [ (the x, y)
  x < ([1..3] ++ [1..2])
 , y < [4..6]
 , then group by x using groupRuns ]
+ :since: 7.6.1
 This results in the variable ``output`` taking on the value below:
+ Allow the use of lambdacase syntax.
 ::
+The :ghcflag:`XLambdaCase` flag enables expressions of the form ::
 [(1, [4, 5, 6]), (2, [4, 5, 6]), (3, [4, 5, 6]), (1, [4, 5, 6]), (2, [4, 5, 6])]
+ \case { p1 > e1; ...; pN > eN }
 Note that we have used the ``the`` function to change the type of x
 from a list to its original numeric type. The variable y, in
 contrast, is left unchanged from the list form introduced by the
 grouping.
+which is equivalent to ::
 ::
+ \freshName > case freshName of { p1 > e1; ...; pN > eN }
 then group using f
+Note that ``\case`` starts a layout, so you can write ::
 With this form of the group statement, f is required to simply have
 the type ``forall a. [a] > [[a]]``, which will be used to group up
 the comprehension so far directly. An example of this form is as
 follows:
+ \case
+ p1 > e1
+ ...
+ pN > eN
 ::
+.. _emptycase:
 output = [ x
  y < [1..5]
 , x < "hello"
 , then group using inits]
+Empty case alternatives
+
 This will yield a list containing every prefix of the word "hello"
 written out 5 times:
+.. ghcflag:: XEmptyCase
 ::
+ :since: 7.8.1
 ["","h","he","hel","hell","hello","helloh","hellohe","hellohel","hellohell","hellohello","hellohelloh",...]
+ Allow empty case expressions.
.. _monadcomprehensions:
+The :ghcflag:`XEmptyCase` flag enables case expressions, or lambdacase
+expressions, that have no alternatives, thus: ::
Monad comprehensions

+ case e of { }  No alternatives
.. index::
 single: monad comprehensions
+or ::
Monad comprehensions generalise the list comprehension notation,
including parallel comprehensions (:ref:`parallellistcomprehensions`)
and transform comprehensions (:ref:`generalisedlistcomprehensions`) to
work for any monad.
+ \case { }  XLambdaCase is also required
Monad comprehensions support:
+This can be useful when you know that the expression being scrutinised
+has no nonbottom values. For example:
 Bindings: ::
+::
 [ x + y  x < Just 1, y < Just 2 ]
+ data Void
+ f :: Void > Int
+ f x = case x of { }
 Bindings are translated with the ``(>>=)`` and ``return`` functions
 to the usual donotation: ::
+With dependentlytyped features it is more useful (see :ghcticket:`2431``). For
+example, consider these two candidate definitions of ``absurd``:
 do x < Just 1
 y < Just 2
 return (x+y)
+::
 Guards: ::
+ data a :==: b where
+ Refl :: a :==: a
 [ x  x < [1..10], x <= 5 ]
+ absurd :: True :~: False > a
+ absurd x = error "absurd"  (A)
+ absurd x = case x of {}  (B)
 Guards are translated with the ``guard`` function, which requires a
 ``MonadPlus`` instance: ::
+We much prefer (B). Why? Because GHC can figure out that
+``(True :~: False)`` is an empty type. So (B) has no partiality and GHC
+should be able to compile with :ghcflag:`Wincompletepatterns`. (Though
+the pattern match checking is not yet clever enough to do that.) On the
+other hand (A) looks dangerous, and GHC doesn't check to make sure that,
+in fact, the function can never get called.
 do x < [1..10]
 guard (x <= 5)
 return x
+.. _multiwayif:
 Transform statements (as with :ghcflag:`XTransformListComp`): ::
+Multiway ifexpressions
+
 [ x+y  x < [1..10], y < [1..x], then take 2 ]
+.. ghcflag:: XMultiWayIf
 This translates to: ::
+ :since: 7.6.1
 do (x,y) < take 2 (do x < [1..10]
 y < [1..x]
 return (x,y))
 return (x+y)
+ Allow the use of multiway``if`` syntax.
 Group statements (as with :ghcflag:`XTransformListComp`):
+With :ghcflag:`XMultiWayIf` flag GHC accepts conditional expressions with
+multiple branches: ::
 ::
+ if  guard1 > expr1
+  ...
+  guardN > exprN
 [ x  x < [1,1,2,2,3], then group by x using GHC.Exts.groupWith ]
 [ x  x < [1,1,2,2,3], then group using myGroup ]
+which is roughly equivalent to ::
 Parallel statements (as with :ghcflag:`XParallelListComp`):
+ case () of
+ _  guard1 > expr1
+ ...
+ _  guardN > exprN
 ::
+Multiway if expressions introduce a new layout context. So the example
+above is equivalent to: ::
 [ (x+y)  x < [1..10]
  y < [11..20]
 ]
+ if {  guard1 > expr1
+ ;  ...
+ ;  guardN > exprN
+ }
 Parallel statements are translated using the ``mzip`` function, which
 requires a ``MonadZip`` instance defined in
 :baseref:`Control.Monad.Zip `:
+The following behaves as expected: ::
 ::
+ if  guard1 > if  guard2 > expr2
+  guard3 > expr3
+  guard4 > expr4
 do (x,y) < mzip (do x < [1..10]
 return x)
 (do y < [11..20]
 return y)
 return (x+y)
+because layout translates it as ::
All these features are enabled by default if the ``MonadComprehensions``
extension is enabled. The types and more detailed examples on how to use
comprehensions are explained in the previous chapters
:ref:`generalisedlistcomprehensions` and
:ref:`parallellistcomprehensions`. In general you just have to replace
the type ``[a]`` with the type ``Monad m => m a`` for monad
comprehensions.
+ if {  guard1 > if {  guard2 > expr2
+ ;  guard3 > expr3
+ }
+ ;  guard4 > expr4
+ }
.. note::
 Even though most of these examples are using the list monad, monad
 comprehensions work for any monad. The ``base`` package offers all
 necessary instances for lists, which make ``MonadComprehensions``
 backward compatible to builtin, transform and parallel list
 comprehensions.
+Layout with multiway if works in the same way as other layout contexts,
+except that the semicolons between guards in a multiway if are
+optional. So it is not necessary to line up all the guards at the same
+column; this is consistent with the way guards work in function
+definitions and case expressions.
More formally, the desugaring is as follows. We write ``D[ e  Q]`` to
mean the desugaring of the monad comprehension ``[ e  Q]``:
+.. _localfixitydeclarations:
::
+Local Fixity Declarations
+
 Expressions: e
 Declarations: d
 Lists of qualifiers: Q,R,S
+A careful reading of the Haskell 98 Report reveals that fixity
+declarations (``infix``, ``infixl``, and ``infixr``) are permitted to
+appear inside local bindings such those introduced by ``let`` and
+``where``. However, the Haskell Report does not specify the semantics of
+such bindings very precisely.
  Basic forms
 D[ e  ] = return e
 D[ e  p < e, Q ] = e >>= \p > D[ e  Q ]
 D[ e  e, Q ] = guard e >> \p > D[ e  Q ]
 D[ e  let d, Q ] = let d in D[ e  Q ]
+In GHC, a fixity declaration may accompany a local binding: ::
  Parallel comprehensions (iterate for multiple parallel branches)
 D[ e  (Q  R), S ] = mzip D[ Qv  Q ] D[ Rv  R ] >>= \(Qv,Rv) > D[ e  S ]
+ let f = ...
+ infixr 3 `f`
+ in
+ ...
  Transform comprehensions
 D[ e  Q then f, R ] = f D[ Qv  Q ] >>= \Qv > D[ e  R ]
+and the fixity declaration applies wherever the binding is in scope. For
+example, in a ``let``, it applies in the righthand sides of other
+``let``bindings and the body of the ``let``\ C. Or, in recursive ``do``
+expressions (:ref:`recursivedonotation`), the local fixity
+declarations of a ``let`` statement scope over other statements in the
+group, just as the bound name does.
 D[ e  Q then f by b, R ] = f (\Qv > b) D[ Qv  Q ] >>= \Qv > D[ e  R ]
+Moreover, a local fixity declaration *must* accompany a local binding
+of that name: it is not possible to revise the fixity of name bound
+elsewhere, as in ::
 D[ e  Q then group using f, R ] = f D[ Qv  Q ] >>= \ys >
 case (fmap selQv1 ys, ..., fmap selQvn ys) of
 Qv > D[ e  R ]
+ let infixr 9 $ in ...
 D[ e  Q then group by b using f, R ] = f (\Qv > b) D[ Qv  Q ] >>= \ys >
 case (fmap selQv1 ys, ..., fmap selQvn ys) of
 Qv > D[ e  R ]
+Because local fixity declarations are technically Haskell 98, no flag is
+necessary to enable them.
 where Qv is the tuple of variables bound by Q (and used subsequently)
 selQvi is a selector mapping Qv to the ith component of Qv
+.. _packageimports:
 Operator Standard binding Expected type
 
 return GHC.Base t1 > m t2
 (>>=) GHC.Base m1 t1 > (t2 > m2 t3) > m3 t3
 (>>) GHC.Base m1 t1 > m2 t2 > m3 t3
 guard Control.Monad t1 > m t2
 fmap GHC.Base forall a b. (a>b) > n a > n b
 mzip Control.Monad.Zip forall a b. m a > m b > m (a,b)
+Import and export extensions
+
The comprehension should typecheck when its desugaring would typecheck,
except that (as discussed in :ref:`generalisedlistcomprehensions`) in the
"then ``f``" and "then group using ``f``" clauses, when the "by ``b``" qualifier
is omitted, argument ``f`` should have a polymorphic type. In particular, "then
``Data.List.sort``" and "then group using ``Data.List.group``" are
insufficiently polymorphic.
+Hiding things the imported module doesn't export
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Monad comprehensions support rebindable syntax
(:ref:`rebindablesyntax`). Without rebindable syntax, the operators
from the "standard binding" module are used; with rebindable syntax, the
operators are looked up in the current lexical scope. For example,
parallel comprehensions will be typechecked and desugared using whatever
"``mzip``" is in scope.
+Technically in Haskell 2010 this is illegal: ::
The rebindable operators must have the "Expected type" given in the
table above. These types are surprisingly general. For example, you can
use a bind operator with the type
+ module A( f ) where
+ f = True
::
+ module B where
+ import A hiding( g )  A does not export g
+ g = f
 (>>=) :: T x y a > (a > T y z b) > T x z b
+The ``import A hiding( g )`` in module ``B`` is technically an error
+(`Haskell Report,
+5.3.1 `__)
+because ``A`` does not export ``g``. However GHC allows it, in the
+interests of supporting backward compatibility; for example, a newer
+version of ``A`` might export ``g``, and you want ``B`` to work in
+either case.
In the case of transform comprehensions, notice that the groups are
parameterised over some arbitrary type ``n`` (provided it has an
``fmap``, as well as the comprehension being over an arbitrary monad.
+The warning :ghcflag:`Wdodgyimports`, which is off by default but included
+with :ghcflag:`W`, warns if you hide something that the imported module does
+not export.
.. _monadfaildesugaring:
+.. _packagequalifiedimports:
New monadic failure desugaring mechanism

+Packagequalified imports
+~~~~~~~~~~~~~~~~~~~~~~~~~
.. ghcflag:: XMonadFailDesugaring
+.. ghcflag:: XPackageImports
 :since: 8.0.1
+ Allow the use of packagequalified ``import`` syntax.
 Use the ``MonadFail.fail`` instead of the legacy ``Monad.fail`` function
 when desugaring refutable patterns in ``do`` blocks.
+With the :ghcflag:`XPackageImports` flag, GHC allows import declarations to be
+qualified by the package name that the module is intended to be imported
+from. For example: ::
The ``XMonadFailDesugaring`` extension switches the desugaring of
``do``blocks to use ``MonadFail.fail`` instead of ``Monad.fail``. This will
eventually be the default behaviour in a future GHC release, under the
`MonadFail Proposal (MFP)
`__.
+ import "network" Network.Socket
This extension is temporary, and will be deprecated in a future release. It is
included so that library authors have a hard check for whether their code
will work with future GHC versions.
+would import the module ``Network.Socket`` from the package ``network``
+(any version). This may be used to disambiguate an import when the same
+module is available from multiple packages, or is present in both the
+current package being built and an external package.
.. _rebindablesyntax:
+The special package name ``this`` can be used to refer to the current
+package being built.
Rebindable syntax and the implicit Prelude import

+.. note::
+ You probably don't need to use this feature, it was added mainly so that we
+ can build backwardscompatible versions of packages when APIs change. It can
+ lead to fragile dependencies in the common case: modules occasionally move
+ from one package to another, rendering any packagequalified imports broken.
+ See also :ref:`packagethinningandrenaming` for an alternative way of
+ disambiguating between module names.
.. ghcflag:: XNoImplicitPrelude
+.. _safeimportsext:
 Don't import ``Prelude`` by default.
+Safe imports
+~~~~~~~~~~~~
GHC normally imports ``Prelude.hi`` files for
you. If you'd rather it didn't, then give it a ``XNoImplicitPrelude``
option. The idea is that you can then import a Prelude of your own. (But
don't call it ``Prelude``; the Haskell module namespace is flat, and you
must not conflict with any Prelude module.)
+.. ghcflag:: XSafe
+ XTrustworthy
+ XUnsafe
+ :noindex:
.. ghcflag:: XRebindableSyntax
+ Declare the Safe Haskell state of the current module.
 :implies: :ghcflag:`XNoImplicitPrelude`
 :since: 7.0.1
+With the :ghcflag:`XSafe`, :ghcflag:`XTrustworthy` and :ghcflag:`XUnsafe`
+language flags, GHC extends the import declaration syntax to take an optional
+``safe`` keyword after the ``import`` keyword. This feature is part of the Safe
+Haskell GHC extension. For example: ::
 Enable rebinding of a variety of usuallybuiltin operations.
+ import safe qualified Network.Socket as NS
Suppose you are importing a Prelude of your own in order to define your
own numeric class hierarchy. It completely defeats that purpose if the
literal "1" means "``Prelude.fromInteger 1``", which is what the Haskell
Report specifies. So the :ghcflag:`XRebindableSyntax` flag causes the
following pieces of builtin syntax to refer to *whatever is in scope*,
not the Prelude versions:
+would import the module ``Network.Socket`` with compilation only
+succeeding if ``Network.Socket`` can be safely imported. For a description of
+when a import is considered safe see :ref:`safehaskell`.
 An integer literal ``368`` means "``fromInteger (368::Integer)``",
 rather than "``Prelude.fromInteger (368::Integer)``".
+.. _explicitnamespaces:
 Fractional literals are handed in just the same way, except that the
 translation is ``fromRational (3.68::Rational)``.
+Explicit namespaces in import/export
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The equality test in an overloaded numeric pattern uses whatever
 ``(==)`` is in scope.
+.. ghcflag:: XExplicitNamespaces
 The subtraction operation, and the greaterthanorequal test, in
 ``n+k`` patterns use whatever ``()`` and ``(>=)`` are in scope.
+ :since: 7.6.1
 Negation (e.g. "`` (f x)``") means "``negate (f x)``", both in
 numeric patterns, and expressions.
+ Enable use of explicit namespaces in module export lists.
 Conditionals (e.g. "``if`` e1 ``then`` e2 ``else`` e3") means
 "``ifThenElse`` e1 e2 e3". However ``case`` expressions are
 unaffected.
+In an import or export list, such as ::
 "Do" notation is translated using whatever functions ``(>>=)``,
 ``(>>)``, and ``fail``, are in scope (not the Prelude versions). List
 comprehensions, ``mdo`` (:ref:`recursivedonotation`), and parallel
 array comprehensions, are unaffected.
+ module M( f, (++) ) where ...
+ import N( f, (++) )
+ ...
 Arrow notation (see :ref:`arrownotation`) uses whatever ``arr``,
 ``(>>>)``, ``first``, ``app``, ``()`` and ``loop`` functions are
 in scope. But unlike the other constructs, the types of these
 functions must match the Prelude types very closely. Details are in
 flux; if you want to use this, ask!
+the entities ``f`` and ``(++)`` are *values*. However, with type
+operators (:ref:`typeoperators`) it becomes possible to declare
+``(++)`` as a *type constructor*. In that case, how would you export or
+import it?
:ghcflag:`XRebindableSyntax` implies :ghcflag:`XNoImplicitPrelude`.
+The :ghcflag:`XExplicitNamespaces` extension allows you to prefix the name of
+a type constructor in an import or export list with "``type``" to
+disambiguate this case, thus: ::
In all cases (apart from arrow notation), the static semantics should be
that of the desugared form, even if that is a little unexpected. For
example, the static semantics of the literal ``368`` is exactly that of
``fromInteger (368::Integer)``; it's fine for ``fromInteger`` to have
any of the types: ::
+ module M( f, type (++) ) where ...
+ import N( f, type (++) )
+ ...
+ module N( f, type (++) ) where
+ data family a ++ b = L a  R b
 fromInteger :: Integer > Integer
 fromInteger :: forall a. Foo a => Integer > a
 fromInteger :: Num a => a > Integer
 fromInteger :: Integer > Bool > Bool
+The extension :ghcflag:`XExplicitNamespaces` is implied by
+:ghcflag:`XTypeOperators` and (for some reason) by :ghcflag:`XTypeFamilies`.
Be warned: this is an experimental facility, with fewer checks than
usual. Use ``dcorelint`` to typecheck the desugared program. If Core
Lint is happy you should be all right.
+In addition, with :ghcflag:`XPatternSynonyms` you can prefix the name of a
+data constructor in an import or export list with the keyword
+``pattern``, to allow the import or export of a data constructor without
+its parent type constructor (see :ref:`patsynimpexp`).
.. _postfixoperators:
+.. _visibletypeapplication:
Postfix operators

+Visible type application
+~~~~~~~~~~~~~~~~~~~~~~~~
.. ghcflag:: XPostfixOperators
+.. ghcflag:: XTypeApplications
 Allow the use of postfix operators
+ :implies: :ghcflag:`XAllowAmbiguousTypes`
+ :since: 8.0.1
The :ghcflag:`XPostfixOperators` flag enables a small extension to the syntax
of left operator sections, which allows you to define postfix operators.
The extension is this: the left section ::
+ Allow the use of type application syntax.
 (e !)
+The :ghcflag:`XTypeApplications` extension allows you to use
+*visible type application* in expressions. Here is an
+example: ``show (read @Int "5")``. The ``@Int``
+is the visible type application; it specifies the value of the type variable
+in ``read``'s type.
is equivalent (from the point of view of both type checking and
execution) to the expression ::
+A visible type application is preceded with an ``@``
+sign. (To disambiguate the syntax, the ``@`` must be
+preceded with a nonidentifier letter, usually a space. For example,
+``read@Int 5`` would not parse.) It can be used whenever
+the full polymorphic type of the function is known. If the function
+is an identifier (the common case), its type is considered known only when
+the identifier has been given a type signature. If the identifier does
+not have a type signature, visible type application cannot be used.
 ((!) e)
+Here are the details:
(for any expression ``e`` and operator ``(!)``. The strict Haskell 98
interpretation is that the section is equivalent to ::
+ If an identifier's type signature does not include an
+ explicit ``forall``, the type variable arguments appear
+ in the lefttoright 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``.
 (\y > (!) e y)
+ If any of the variables depend on other variables (that is, if some
+ of the variables are *kind* variables), the variables are reordered
+ so that kind variables come before type variables, preserving the
+ lefttoright order as much as possible. That is, GHC performs a
+ stable topological sort on the variables.
That is, the operator must be a function of two arguments. GHC allows it
to take only one argument, and that in turn allows you to write the
function postfix.
+ For example: if we have ``bar :: Proxy (a :: (j, k)) > b``, then
+ the variables are ordered ``j``, ``k``, ``a``, ``b``.
The extension does not extend to the lefthand side of function
definitions; you must define such a function in prefix form.
+ Class methods' type arguments include the class type
+ variables, followed by any variables an individual method is polymorphic
+ in. So, ``class Monad m where return :: a > m a`` means
+ that ``return``'s type arguments are ``m, a``.
.. _tuplesections:
+ With the :ghcflag:`XRankNTypes` extension
+ (:ref:`universalquantification`), it is possible to declare
+ type arguments somewhere other than the beginning of a type. For example,
+ we can have ``pair :: forall a. a > forall b. b > (a, b)``
+ and then say ``pair @Bool True @Char`` which would have
+ type ``Char > (Bool, Char)``.
Tuple sections

+ Partial type signatures (:ref:`partialtypesignatures`)
+ work nicely with visible type
+ 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 :ghcflag:`XPartialTypeSignatures` and your
+ code will not generate a warning informing you of the omitted type.
.. ghcflag:: XTupleSections
+.. _syntaxstolen:
 Allow the use of tuple section syntax
+Summary of stolen syntax
+
+
+Turning on an option that enables special syntax *might* cause working
+Haskell 98 code to fail to compile, perhaps because it uses a variable
+name which has become a reserved word. This section lists the syntax
+that is "stolen" by language extensions. We use notation and nonterminal
+names from the Haskell 98 lexical syntax (see the Haskell 98 Report). We
+only list syntax changes here that might affect existing working
+programs (i.e. "stolen" syntax). Many of these extensions will also
+enable new contextfree syntax, but in all cases programs written to use
+the new syntax would not be compilable without the option enabled.
The :ghcflag:`XTupleSections` flag enables Pythonstyle partially applied
tuple constructors. For example, the following program ::
+There are two classes of special syntax:
 (, True)
+ New reserved words and symbols: character sequences which are no
+ longer available for use as identifiers in the program.
is considered to be an alternative notation for the more unwieldy
alternative ::
+ Other special syntax: sequences of characters that have a different
+ meaning when this particular option is turned on.
 \x > (x, True)
+The following syntax is stolen:
You can omit any combination of arguments to the tuple, as in the
following ::
+``forall``
+ .. index::
+ single: forall
 (, "I", , , "Love", , 1337)
+ Stolen (in types) by: :ghcflag:`XExplicitForAll`, and hence by
+ :ghcflag:`XScopedTypeVariables`, :ghcflag:`XLiberalTypeSynonyms`,
+ :ghcflag:`XRankNTypes`, :ghcflag:`XExistentialQuantification`
which translates to ::
+``mdo``
+ .. index::
+ single: mdo
 \a b c d > (a, "I", b, c, "Love", d, 1337)
+ Stolen by: :ghcflag:`XRecursiveDo`
If you have `unboxed tuples <#unboxedtuples>`__ enabled, tuple sections
will also be available for them, like so ::
+``foreign``
+ .. index::
+ single: foreign
 (# , True #)
+ Stolen by: :ghcflag:`XForeignFunctionInterface`
Because there is no unboxed unit tuple, the following expression ::
+``rec``, ``proc``, ``<``, ``>``, ``<<``, ``>>``, ``(``, ``)``
+ .. index::
+ single: proc
 (# #)
+ Stolen by: :ghcflag:`XArrows`
continues to stand for the unboxed singleton tuple data constructor.
+``?varid``
+ .. index::
+ single: implicit parameters
.. _lambdacase:
+ Stolen by: :ghcflag:`XImplicitParams`
Lambdacase

+``[``, ``[e``, ``[p``, ``[d``, ``[t``, ``$(``, ``$$(``, ``[``, ``[e``, ``$varid``, ``$$varid``
+ .. index::
+ single: Template Haskell
.. ghcflag:: XLambdaCase
+ Stolen by: :ghcflag:`XTemplateHaskell`
 :since: 7.6.1
+``[varid``
+ .. index::
+ single: quasiquotation
 Allow the use of lambdacase syntax.
+ Stolen by: :ghcflag:`XQuasiQuotes`
The :ghcflag:`XLambdaCase` flag enables expressions of the form ::
+⟨varid⟩, ``#``\ ⟨char⟩, ``#``, ⟨string⟩, ``#``, ⟨integer⟩, ``#``, ⟨float⟩, ``#``, ⟨float⟩, ``##``
+ Stolen by: :ghcflag:`XMagicHash`
 \case { p1 > e1; ...; pN > eN }
+``(#``, ``#)``
+ Stolen by: :ghcflag:`XUnboxedTuples`
which is equivalent to ::
+⟨varid⟩, ``!``, ⟨varid⟩
+ Stolen by: :ghcflag:`XBangPatterns`
 \freshName > case freshName of { p1 > e1; ...; pN > eN }
+``pattern``
+ Stolen by: :ghcflag:`XPatternSynonyms`
Note that ``\case`` starts a layout, so you can write ::
+.. _datatypeextensions:
 \case
 p1 > e1
 ...
 pN > eN
+Extensions to data types and type synonyms
+==========================================
.. _emptycase:
+.. _nullarytypes:
Empty case alternatives

+Data types with no constructors
+
.. ghcflag:: XEmptyCase
+.. ghcflag:: XEmptyDataDecls
 :since: 7.8.1
+ Allow definition of empty ``data`` types.
 Allow empty case expressions.
+With the :ghcflag:`XEmptyDataDecls` flag (or equivalent ``LANGUAGE`` pragma), GHC
+lets you declare a data type with no constructors. For example: ::
The :ghcflag:`XEmptyCase` flag enables case expressions, or lambdacase
expressions, that have no alternatives, thus: ::
+ data S  S :: *
+ data T a  T :: * > *
 case e of { }  No alternatives
+Syntactically, the declaration lacks the "= constrs" part. The type can
+be parameterised over types of any kind, but if the kind is not ``*``
+then an explicit kind annotation must be used (see :ref:`kinding`).
or ::
+Such data types have only one value, namely bottom. Nevertheless, they
+can be useful when defining "phantom types".
 \case { }  XLambdaCase is also required
+.. _datatypecontexts:
This can be useful when you know that the expression being scrutinised
has no nonbottom values. For example:
+Data type contexts
+
::
+.. ghcflag:: XDatatypeContexts
 data Void
 f :: Void > Int
 f x = case x of { }
+ :since: 7.0.1
With dependentlytyped features it is more useful (see :ghcticket:`2431``). For
example, consider these two candidate definitions of ``absurd``:
+ Allow contexts on ``data`` types.
::
+Haskell allows datatypes to be given contexts, e.g. ::
 data a :==: b where
 Refl :: a :==: a
+ data Eq a => Set a = NilSet  ConsSet a (Set a)
 absurd :: True :~: False > a
 absurd x = error "absurd"  (A)
 absurd x = case x of {}  (B)
+give constructors with types: ::
We much prefer (B). Why? Because GHC can figure out that
``(True :~: False)`` is an empty type. So (B) has no partiality and GHC
should be able to compile with :ghcflag:`Wincompletepatterns`. (Though
the pattern match checking is not yet clever enough to do that.) On the
other hand (A) looks dangerous, and GHC doesn't check to make sure that,
in fact, the function can never get called.
+ NilSet :: Set a
+ ConsSet :: Eq a => a > Set a > Set a
.. _multiwayif:
+This is widely considered a misfeature, and is going to be removed from
+the language. In GHC, it is controlled by the deprecated extension
+``DatatypeContexts``.
Multiway ifexpressions

+.. _infixtycons:
.. ghcflag:: XMultiWayIf
+Infix type constructors, classes, and type variables
+
 :since: 7.6.1
+GHC allows type constructors, classes, and type variables to be
+operators, and to be written infix, very much like expressions. More
+specifically:
 Allow the use of multiway``if`` syntax.
+ A type constructor or class can be any nonreserved operator.
+ Symbols used in types are always like capitalized identifiers; they
+ are never variables. Note that this is different from the lexical
+ syntax of data constructors, which are required to begin with a
+ ``:``.
With :ghcflag:`XMultiWayIf` flag GHC accepts conditional expressions with
multiple branches: ::
+ Data type and typesynonym declarations can be written infix,
+ parenthesised if you want further arguments. E.g. ::
 if  guard1 > expr1
  ...
  guardN > exprN
+ data a :*: b = Foo a b
+ type a :+: b = Either a b
+ class a :=: b where ...
which is roughly equivalent to ::
+ data (a :**: b) x = Baz a b x
+ type (a :++: b) y = Either (a,b) y
 case () of
 _  guard1 > expr1
 ...
 _  guardN > exprN
+ Types, and class constraints, can be written infix. For example ::
Multiway if expressions introduce a new layout context. So the example
above is equivalent to: ::
+ x :: Int :*: Bool
+ f :: (a :=: b) => a > b
 if {  guard1 > expr1
 ;  ...
 ;  guardN > exprN
 }
+ Backquotes work as for expressions, both for type constructors and
+ type variables; e.g. ``Int `Either` Bool``, or ``Int `a` Bool``.
+ Similarly, parentheses work the same; e.g. ``(:*:) Int Bool``.
The following behaves as expected: ::
+ Fixities may be declared for type constructors, or classes, just as
+ for data constructors. However, one cannot distinguish between the
+ two in a fixity declaration; a fixity declaration sets the fixity for
+ a data constructor and the corresponding type constructor. For
+ example: ::
 if  guard1 > if  guard2 > expr2
  guard3 > expr3
  guard4 > expr4
+ infixl 7 T, :*:
because layout translates it as ::
+ sets the fixity for both type constructor ``T`` and data constructor
+ ``T``, and similarly for ``:*:``. ``Int `a` Bool``.
 if {  guard1 > if {  guard2 > expr2
 ;  guard3 > expr3
 }
 ;  guard4 > expr4
 }
+ Function arrow is ``infixr`` with fixity 0 (this might change; it's
+ not clear what it should be).
Layout with multiway if works in the same way as other layout contexts,
except that the semicolons between guards in a multiway if are
optional. So it is not necessary to line up all the guards at the same
column; this is consistent with the way guards work in function
definitions and case expressions.
+.. _typeoperators:
.. _localfixitydeclarations:
+Type operators
+
Local Fixity Declarations

+.. ghcflag:: XTypeOperators
A careful reading of the Haskell 98 Report reveals that fixity
declarations (``infix``, ``infixl``, and ``infixr``) are permitted to
appear inside local bindings such those introduced by ``let`` and
``where``. However, the Haskell Report does not specify the semantics of
such bindings very precisely.
+ :implies: :ghcflag:`XExplicitNamespaces`
In GHC, a fixity declaration may accompany a local binding: ::
+ Allow the use and definition of types with operator names.
 let f = ...
 infixr 3 `f`
 in
 ...
+In types, an operator symbol like ``(+)`` is normally treated as a type
+*variable*, just like ``a``. Thus in Haskell 98 you can say
and the fixity declaration applies wherever the binding is in scope. For
example, in a ``let``, it applies in the righthand sides of other
``let``bindings and the body of the ``let``\ C. Or, in recursive ``do``
expressions (:ref:`recursivedonotation`), the local fixity
declarations of a ``let`` statement scope over other statements in the
group, just as the bound name does.
+::
Moreover, a local fixity declaration *must* accompany a local binding
of that name: it is not possible to revise the fixity of name bound
elsewhere, as in ::
+ type T (+) = ((+), (+))
+  Just like: type T a = (a,a)
 let infixr 9 $ in ...
+ f :: T Int > Int
+ f (x,y)= x
Because local fixity declarations are technically Haskell 98, no flag is
necessary to enable them.
+As you can see, using operators in this way is not very useful, and
+Haskell 98 does not even allow you to write them infix.
.. _packageimports:
+The language :ghcflag:`XTypeOperators` changes this behaviour:
Import and export extensions

+ Operator symbols become type *constructors* rather than type
+ *variables*.
Hiding things the imported module doesn't export
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+ Operator symbols in types can be written infix, both in definitions
+ and uses. For example: ::
Technically in Haskell 2010 this is illegal: ::
+ data a + b = Plus a b
+ type Foo = Int + Bool
 module A( f ) where
 f = True
+ There is now some potential ambiguity in import and export lists; for
+ example if you write ``import M( (+) )`` do you mean the *function*
+ ``(+)`` or the *type constructor* ``(+)``? The default is the former,
+ but with :ghcflag:`XExplicitNamespaces` (which is implied by
+ :ghcflag:`XTypeOperators`) GHC allows you to specify the latter by
+ preceding it with the keyword ``type``, thus: ::
 module B where
 import A hiding( g )  A does not export g
 g = f
+ import M( type (+) )
The ``import A hiding( g )`` in module ``B`` is technically an error
(`Haskell Report,
5.3.1 `__)
because ``A`` does not export ``g``. However GHC allows it, in the
interests of supporting backward compatibility; for example, a newer
version of ``A`` might export ``g``, and you want ``B`` to work in
either case.
+ See :ref:`explicitnamespaces`.
The warning :ghcflag:`Wdodgyimports`, which is off by default but included
with :ghcflag:`W`, warns if you hide something that the imported module does
not export.
+ The fixity of a type operator may be set using the usual fixity
+ declarations but, as in :ref:`infixtycons`, the function and type
+ constructor share a single fixity.
.. _packagequalifiedimports:
+.. _typesynonyms:
Packagequalified imports
~~~~~~~~~~~~~~~~~~~~~~~~~
+Liberalised type synonyms
+
.. ghcflag:: XPackageImports
+.. ghcflag:: XLiberalTypeSynonyms
 Allow the use of packagequalified ``import`` syntax.
+ :implies: :ghcflag:`XExplicitForAll`
With the :ghcflag:`XPackageImports` flag, GHC allows import declarations to be
qualified by the package name that the module is intended to be imported
from. For example: ::
+ Relax many of the Haskell 98 rules on type synonym definitions.
 import "network" Network.Socket
+Type synonyms are like macros at the type level, but Haskell 98 imposes
+many rules on individual synonym declarations. With the
+:ghcflag:`XLiberalTypeSynonyms` extension, GHC does validity checking on types
+*only after expanding type synonyms*. That means that GHC can be very
+much more liberal about type synonyms than Haskell 98.
would import the module ``Network.Socket`` from the package ``network``
(any version). This may be used to disambiguate an import when the same
module is available from multiple packages, or is present in both the
current package being built and an external package.
+ You can write a ``forall`` (including overloading) in a type synonym,
+ thus: ::
The special package name ``this`` can be used to refer to the current
package being built.
+ type Discard a = forall b. Show b => a > b > (a, String)
.. note::
 You probably don't need to use this feature, it was added mainly so that we
 can build backwardscompatible versions of packages when APIs change. It can
 lead to fragile dependencies in the common case: modules occasionally move
 from one package to another, rendering any packagequalified imports broken.
 See also :ref:`packagethinningandrenaming` for an alternative way of
 disambiguating between module names.
+ f :: Discard a
+ f x y = (x, show y)
.. _safeimportsext:
+ g :: Discard Int > (Int,String)  A rank2 type
+ g f = f 3 True
Safe imports
~~~~~~~~~~~~
+ If you also use :ghcflag:`XUnboxedTuples`, you can write an unboxed tuple
+ in a type synonym: ::
.. ghcflag:: XSafe
 XTrustworthy
 XUnsafe
 :noindex:
+ type Pr = (# Int, Int #)
 Declare the Safe Haskell state of the current module.
+ h :: Int > Pr
+ h x = (# x, x #)
With the :ghcflag:`XSafe`, :ghcflag:`XTrustworthy` and :ghcflag:`XUnsafe`
language flags, GHC extends the import declaration syntax to take an optional
``safe`` keyword after the ``import`` keyword. This feature is part of the Safe
Haskell GHC extension. For example: ::
+ You can apply a type synonym to a forall type: ::
 import safe qualified Network.Socket as NS
+ type Foo a = a > a > Bool
would import the module ``Network.Socket`` with compilation only
succeeding if ``Network.Socket`` can be safely imported. For a description of
when a import is considered safe see :ref:`safehaskell`.
+ f :: Foo (forall b. b>b)
.. _explicitnamespaces:
+ After expanding the synonym, ``f`` has the legal (in GHC) type: ::
Explicit namespaces in import/export
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+ f :: (forall b. b>b) > (forall b. b>b) > Bool
.. ghcflag:: XExplicitNamespaces
+ You can apply a type synonym to a partially applied type synonym: ::
 :since: 7.6.1
+ type Generic i o = forall x. i x > o x
+ type Id x = x
 Enable use of explicit namespaces in module export lists.
+ foo :: Generic Id []
In an import or export list, such as ::
+ After expanding the synonym, ``foo`` has the legal (in GHC) type: ::
 module M( f, (++) ) where ...
 import N( f, (++) )
 ...
+ foo :: forall x. x > [x]
the entities ``f`` and ``(++)`` are *values*. However, with type
operators (:ref:`typeoperators`) it becomes possible to declare
``(++)`` as a *type constructor*. In that case, how would you export or
import it?
+GHC currently does kind checking before expanding synonyms (though even
+that could be changed)..
The :ghcflag:`XExplicitNamespaces` extension allows you to prefix the name of
a type constructor in an import or export list with "``type``" to
disambiguate this case, thus: ::
+After expanding type synonyms, GHC does validity checking on types,
+looking for the following malformedness which isn't detected simply by
+kind checking:
 module M( f, type (++) ) where ...
 import N( f, type (++) )
 ...
 module N( f, type (++) ) where
 data family a ++ b = L a  R b
+ Type constructor applied to a type involving foralls (if
+ :ghcflag:`XImpredicativeTypes` is off)
The extension :ghcflag:`XExplicitNamespaces` is implied by
:ghcflag:`XTypeOperators` and (for some reason) by :ghcflag:`XTypeFamilies`.
+ Partiallyapplied type synonym.
In addition, with :ghcflag:`XPatternSynonyms` you can prefix the name of a
data constructor in an import or export list with the keyword
``pattern``, to allow the import or export of a data constructor without
its parent type constructor (see :ref:`patsynimpexp`).
+So, for example, this will be rejected: ::
.. _visibletypeapplication:
+ type Pr = forall a. a
Visible type application
~~~~~~~~~~~~~~~~~~~~~~~~
+ h :: [Pr]
+ h = ...
.. ghcflag:: XTypeApplications
+because GHC does not allow type constructors applied to forall types.
 :implies: :ghcflag:`XAllowAmbiguousTypes`
 :since: 8.0.1
+.. _existentialquantification:
 Allow the use of type application syntax.
+Existentially quantified data constructors
+
The :ghcflag:`XTypeApplications` extension allows you to use
*visible type application* in expressions. Here is an
example: ``show (read @Int "5")``. The ``@Int``
is the visible type application; it specifies the value of the type variable
in ``read``'s type.
+.. ghcflag:: XExistentialQuantification
A visible type application is preceded with an ``@``
sign. (To disambiguate the syntax, the ``@`` must be
preceded with a nonidentifier letter, usually a space. For example,
``read@Int 5`` would not parse.) It can be used whenever
the full polymorphic type of the function is known. If the function
is an identifier (the common case), its type is considered known only when
the identifier has been given a type signature. If the identifier does
not have a type signature, visible type application cannot be used.
+ :implies: :ghcflag:`XExplicitForAll`
Here are the details:
+ Allow existentially quantified type variables in types.
 If an identifier's type signature does not include an
 explicit ``forall``, the type variable arguments appear
 in the lefttoright 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``.
+The idea of using existential quantification in data type declarations
+was suggested by Perry, and implemented in Hope+ (Nigel Perry, *The
+Implementation of Practical Functional Programming Languages*, PhD
+Thesis, University of London, 1991). It was later formalised by Laufer
+and Odersky (*Polymorphic type inference and abstract data types*,
+TOPLAS, 16(5), pp. 14111430, 1994). It's been in Lennart Augustsson's
+``hbc`` Haskell compiler for several years, and proved very useful.
+Here's the idea. Consider the declaration: ::
 If any of the variables depend on other variables (that is, if some
 of the variables are *kind* variables), the variables are reordered
 so that kind variables come before type variables, preserving the
 lefttoright order as much as possible. That is, GHC performs a
 stable topological sort on the variables.
+ data Foo = forall a. MkFoo a (a > Bool)
+  Nil
 For example: if we have ``bar :: Proxy (a :: (j, k)) > b``, then
 the variables are ordered ``j``, ``k``, ``a``, ``b``.
+The data type ``Foo`` has two constructors with types: ::
 Class methods' type arguments include the class type
 variables, followed by any variables an individual method is polymorphic
 in. So, ``class Monad m where return :: a > m a`` means
 that ``return``'s type arguments are ``m, a``.
+ MkFoo :: forall a. a > (a > Bool) > Foo
+ Nil :: Foo
 With the :ghcflag:`XRankNTypes` extension
 (:ref:`universalquantification`), it is possible to declare
 type arguments somewhere other than the beginning of a type. For example,
 we can have ``pair :: forall a. a > forall b. b > (a, b)``
 and then say ``pair @Bool True @Char`` which would have
 type ``Char > (Bool, Char)``.
+Notice that the type variable ``a`` in the type of ``MkFoo`` does not
+appear in the data type itself, which is plain ``Foo``. For example, the
+following expression is fine: ::
 Partial type signatures (:ref:`partialtypesignatures`)
 work nicely with visible type
 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 :ghcflag:`XPartialTypeSignatures` and your
 code will not generate a warning informing you of the omitted type.
+ [MkFoo 3 even, MkFoo 'c' isUpper] :: [Foo]
.. _syntaxstolen:
+Here, ``(MkFoo 3 even)`` packages an integer with a function ``even``
+that maps an integer to ``Bool``; and ``MkFoo 'c'
+isUpper`` packages a character with a compatible function. These two
+things are each of type ``Foo`` and can be put in a list.
Summary of stolen syntax

+What can we do with a value of type ``Foo``? In particular, what
+happens when we patternmatch on ``MkFoo``? ::
Turning on an option that enables special syntax *might* cause working
Haskell 98 code to fail to compile, perhaps because it uses a variable
name which has become a reserved word. This section lists the syntax
that is "stolen" by language extensions. We use notation and nonterminal
names from the Haskell 98 lexical syntax (see the Haskell 98 Report). We
only list syntax changes here that might affect existing working
programs (i.e. "stolen" syntax). Many of these extensions will also
enable new contextfree syntax, but in all cases programs written to use
the new syntax would not be compilable without the option enabled.
+ f (MkFoo val fn) = ???
There are two classes of special syntax:
+Since all we know about ``val`` and ``fn`` is that they are compatible,
+the only (useful) thing we can do with them is to apply ``fn`` to
+``val`` to get a boolean. For example: ::
 New reserved words and symbols: character sequences which are no
 longer available for use as identifiers in the program.
+ f :: Foo > Bool
+ f (MkFoo val fn) = fn val
 Other special syntax: sequences of characters that have a different
 meaning when this particular option is turned on.
+What this allows us to do is to package heterogeneous values together
+with a bunch of functions that manipulate them, and then treat that
+collection of packages in a uniform manner. You can express quite a bit
+of objectorientedlike programming this way.
The following syntax is stolen:
+.. _existential:
``forall``
 .. index::
 single: forall
+Why existential?
+~~~~~~~~~~~~~~~~
 Stolen (in types) by: :ghcflag:`XExplicitForAll`, and hence by
 :ghcflag:`XScopedTypeVariables`, :ghcflag:`XLiberalTypeSynonyms`,
 :ghcflag:`XRankNTypes`, :ghcflag:`XExistentialQuantification`
+What has this to do with *existential* quantification? Simply that
+``MkFoo`` has the (nearly) isomorphic type ::
``mdo``
 .. index::
 single: mdo
+ MkFoo :: (exists a . (a, a > Bool)) > Foo
 Stolen by: :ghcflag:`XRecursiveDo`
+But Haskell programmers can safely think of the ordinary *universally*
+quantified type given above, thereby avoiding adding a new existential
+quantification construct.
``foreign``
 .. index::
 single: foreign
+.. _existentialwithcontext:
 Stolen by: :ghcflag:`XForeignFunctionInterface`
+Existentials and type classes
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
``rec``, ``proc``, ``<``, ``>``, ``<<``, ``>>``, ``(``, ``)``
 .. index::
 single: proc
+An easy extension is to allow arbitrary contexts before the constructor.
+For example: ::
 Stolen by: :ghcflag:`XArrows`
+ data Baz = forall a. Eq a => Baz1 a a
+  forall b. Show b => Baz2 b (b > b)
``?varid``
 .. index::
 single: implicit parameters
+The two constructors have the types you'd expect: ::
 Stolen by: :ghcflag:`XImplicitParams`
+ Baz1 :: forall a. Eq a => a > a > Baz
+ Baz2 :: forall b. Show b => b > (b > b) > Baz
``[``, ``[e``, ``[p``, ``[d``, ``[t``, ``$(``, ``$$(``, ``[``, ``[e``, ``$varid``, ``$$varid``
 .. index::
 single: Template Haskell
+But when pattern matching on ``Baz1`` the matched values can be compared
+for equality, and when pattern matching on ``Baz2`` the first matched
+value can be converted to a string (as well as applying the function to
+it). So this program is legal: ::
 Stolen by: :ghcflag:`XTemplateHaskell`
+ f :: Baz > String
+ f (Baz1 p q)  p == q = "Yes"
+  otherwise = "No"
+ f (Baz2 v fn) = show (fn v)
``[varid``
 .. index::
 single: quasiquotation
+Operationally, in a dictionarypassing implementation, the constructors
+``Baz1`` and ``Baz2`` must store the dictionaries for ``Eq`` and
+``Show`` respectively, and extract it on pattern matching.
 Stolen by: :ghcflag:`XQuasiQuotes`
+.. _existentialrecords:
⟨varid⟩, ``#``\ ⟨char⟩, ``#``, ⟨string⟩, ``#``, ⟨integer⟩, ``#``, ⟨float⟩, ``#``, ⟨float⟩, ``##``
 Stolen by: :ghcflag:`XMagicHash`
+Record Constructors
+~~~~~~~~~~~~~~~~~~~
``(#``, ``#)``
 Stolen by: :ghcflag:`XUnboxedTuples`
+GHC allows existentials to be used with records syntax as well. For
+example: ::
⟨varid⟩, ``!``, ⟨varid⟩
 Stolen by: :ghcflag:`XBangPatterns`
+ data Counter a = forall self. NewCounter
+ { _this :: self
+ , _inc :: self > self
+ , _display :: self > IO ()
+ , tag :: a
+ }
``pattern``
 Stolen by: :ghcflag:`XPatternSynonyms`
+Here ``tag`` is a public field, with a welltyped selector function
+``tag :: Counter a > a``. The ``self`` type is hidden from the outside;
+any attempt to apply ``_this``, ``_inc`` or ``_display`` as functions
+will raise a compiletime error. In other words, *GHC defines a record
+selector function only for fields whose type does not mention the
+existentiallyquantified variables*. (This example used an underscore in
+the fields for which record selectors will not be defined, but that is
+only programming style; GHC ignores them.)
.. _datatypeextensions:
+To make use of these hidden fields, we need to create some helper
+functions: ::
Extensions to data types and type synonyms
==========================================
+ inc :: Counter a > Counter a
+ inc (NewCounter x i d t) = NewCounter
+ { _this = i x, _inc = i, _display = d, tag = t }
.. _nullarytypes:
+ display :: Counter a > IO ()
+ display NewCounter{ _this = x, _display = d } = d x
Data types with no constructors

+Now we can define counters with different underlying implementations: ::
.. ghcflag:: XEmptyDataDecls
+ counterA :: Counter String
+ counterA = NewCounter
+ { _this = 0, _inc = (1+), _display = print, tag = "A" }
 Allow definition of empty ``data`` types.
+ counterB :: Counter String
+ counterB = NewCounter
+ { _this = "", _inc = ('#':), _display = putStrLn, tag = "B" }
With the :ghcflag:`XEmptyDataDecls` flag (or equivalent ``LANGUAGE`` pragma), GHC
lets you declare a data type with no constructors. For example: ::
+ main = do
+ display (inc counterA)  prints "1"
+ display (inc (inc counterB))  prints "##"
 data S  S :: *
 data T a  T :: * > *
+Record update syntax is supported for existentials (and GADTs): ::
Syntactically, the declaration lacks the "= constrs" part. The type can
be parameterised over types of any kind, but if the kind is not ``*``
then an explicit kind annotation must be used (see :ref:`kinding`).
+ setTag :: Counter a > a > Counter a
+ setTag obj t = obj{ tag = t }
Such data types have only one value, namely bottom. Nevertheless, they
can be useful when defining "phantom types".
+The rule for record update is this:
.. _datatypecontexts:
+ the types of the updated fields may mention only the universallyquantified
+ type variables of the data constructor. For GADTs, the field may mention
+ only types that appear as a simple typevariable argument in the
+ constructor's result type.
Data type contexts

+For example: ::
.. ghcflag:: XDatatypeContexts
+ data T a b where { T1 { f1::a, f2::b, f3::(b,c) } :: T a b }  c is existential
+ upd1 t x = t { f1=x }  OK: upd1 :: T a b > a' > T a' b
+ upd2 t x = t { f3=x }  BAD (f3's type mentions c, which is
+  existentially quantified)
 :since: 7.0.1
+ data G a b where { G1 { g1::a, g2::c } :: G a [c] }
+ upd3 g x = g { g1=x }  OK: upd3 :: G a b > c > G c b
+ upd4 g x = g { g2=x }  BAD (f2's type mentions c, which is not a simple
+  typevariable argument in G1's result type)
 Allow contexts on ``data`` types.
+Restrictions
+~~~~~~~~~~~~
Haskell allows datatypes to be given contexts, e.g. ::
+There are several restrictions on the ways in which existentiallyquantified
+constructors can be used.
 data Eq a => Set a = NilSet  ConsSet a (Set a)
+ When pattern matching, each pattern match introduces a new, distinct,
+ type for each existential type variable. These types cannot be
+ unified with any other type, nor can they escape from the scope of
+ the pattern match. For example, these fragments are incorrect: ::
give constructors with types: ::
+ f1 (MkFoo a f) = a
 NilSet :: Set a
 ConsSet :: Eq a => a > Set a > Set a
+ Here, the type bound by ``MkFoo`` "escapes", because ``a`` is the
+ result of ``f1``. One way to see why this is wrong is to ask what
+ type ``f1`` has: ::
This is widely considered a misfeature, and is going to be removed from
the language. In GHC, it is controlled by the deprecated extension
``DatatypeContexts``.
+ f1 :: Foo > a  Weird!
.. _infixtycons:
+ What is this "``a``" in the result type? Clearly we don't mean this: ::
Infix type constructors, classes, and type variables

+ f1 :: forall a. Foo > a  Wrong!
GHC allows type constructors, classes, and type variables to be
operators, and to be written infix, very much like expressions. More
specifically:
+ The original program is just plain wrong. Here's another sort of
+ error ::
 A type constructor or class can be any nonreserved operator.
 Symbols used in types are always like capitalized identifiers; they
 are never variables. Note that this is different from the lexical
 syntax of data constructors, which are required to begin with a
 ``:``.
+ f2 (Baz1 a b) (Baz1 p q) = a==q
 Data type and typesynonym declarations can be written infix,
 parenthesised if you want further arguments. E.g. ::
+ It's ok to say ``a==b`` or ``p==q``, but ``a==q`` is wrong because it
+ equates the two distinct types arising from the two ``Baz1``
+ constructors.
 data a :*: b = Foo a b
 type a :+: b = Either a b
 class a :=: b where ...
+ You can't patternmatch on an existentially quantified constructor in
+ a ``let`` or ``where`` group of bindings. So this is illegal: ::
 data (a :**: b) x = Baz a b x
 type (a :++: b) y = Either (a,b) y
+ f3 x = a==b where { Baz1 a b = x }
 Types, and class constraints, can be written infix. For example ::
+ Instead, use a ``case`` expression: ::
 x :: Int :*: Bool
 f :: (a :=: b) => a > b
+ f3 x = case x of Baz1 a b > a==b
 Backquotes work as for expressions, both for type constructors and
 type variables; e.g. ``Int `Either` Bool``, or ``Int `a` Bool``.
 Similarly, parentheses work the same; e.g. ``(:*:) Int Bool``.
+ In general, you can only patternmatch on an existentiallyquantified
+ constructor in a ``case`` expression or in the patterns of a function
+ definition. The reason for this restriction is really an
+ implementation one. Typechecking binding groups is already a
+ nightmare without existentials complicating the picture. Also an
+ existential pattern binding at the top level of a module doesn't make
+ sense, because it's not clear how to prevent the
+ existentiallyquantified type "escaping". So for now, there's a
+ simpletostate restriction. We'll see how annoying it is.
 Fixities may be declared for type constructors, or classes, just as
 for data constructors. However, one cannot distinguish between the
 two in a fixity declaration; a fixity declaration sets the fixity for
 a data constructor and the corresponding type constructor. For
 example: ::
+ You can't use existential quantification for ``newtype``
+ declarations. So this is illegal: ::
 infixl 7 T, :*:
+ newtype T = forall a. Ord a => MkT a
 sets the fixity for both type constructor ``T`` and data constructor
 ``T``, and similarly for ``:*:``. ``Int `a` Bool``.
+ Reason: a value of type ``T`` must be represented as a pair of a
+ dictionary for ``Ord t`` and a value of type ``t``. That contradicts
+ the idea that ``newtype`` should have no concrete representation. You
+ can get just the same efficiency and effect by using ``data`` instead
+ of ``newtype``. If there is no overloading involved, then there is
+ more of a case for allowing an existentiallyquantified ``newtype``,
+ because the ``data`` version does carry an implementation cost, but
+ singlefield existentially quantified constructors aren't much use.
+ So the simple restriction (no existential stuff on ``newtype``)
+ stands, unless there are convincing reasons to change it.
 Function arrow is ``infixr`` with fixity 0 (this might change; it's
 not clear what it should be).
+ You can't use ``deriving`` to define instances of a data type with
+ existentially quantified data constructors. Reason: in most cases it
+ would not make sense. For example:; ::
.. _typeoperators:
+ data T = forall a. MkT [a] deriving( Eq )
Type operators

+ To derive ``Eq`` in the standard way we would need to have equality
+ between the single component of two ``MkT`` constructors: ::
.. ghcflag:: XTypeOperators
+ instance Eq T where
+ (MkT a) == (MkT b) = ???
 :implies: :ghcflag:`XExplicitNamespaces`
+ But ``a`` and ``b`` have distinct types, and so can't be compared.
+ It's just about possible to imagine examples in which the derived
+ instance would make sense, but it seems altogether simpler simply to
+ prohibit such declarations. Define your own instances!
 Allow the use and definition of types with operator names.
+.. _gadtstyle:
In types, an operator symbol like ``(+)`` is normally treated as a type
*variable*, just like ``a``. Thus in Haskell 98 you can say
+Declaring data types with explicit constructor signatures
+
::
+.. ghcflag:: XGADTSyntax
 type T (+) = ((+), (+))
  Just like: type T a = (a,a)
+ Allow the use of GADT syntax in data type definitions (but not GADTs
+ themselves; for this see :ghcflag:`XGADTs`)
 f :: T Int > Int
 f (x,y)= x
+When the ``GADTSyntax`` extension is enabled, GHC allows you to declare
+an algebraic data type by giving the type signatures of constructors
+explicitly. For example: ::
As you can see, using operators in this way is not very useful, and
Haskell 98 does not even allow you to write them infix.
+ data Maybe a where
+ Nothing :: Maybe a
+ Just :: a > Maybe a
The language :ghcflag:`XTypeOperators` changes this behaviour:
+The form is called a "GADTstyle declaration" because Generalised
+Algebraic Data Types, described in :ref:`gadt`, can only be declared
+using this form.
 Operator symbols become type *constructors* rather than type
 *variables*.
+Notice that GADTstyle syntax generalises existential types
+(:ref:`existentialquantification`). For example, these two declarations
+are equivalent: ::
 Operator symbols in types can be written infix, both in definitions
 and uses. For example: ::
+ data Foo = forall a. MkFoo a (a > Bool)
+ data Foo' where { MKFoo :: a > (a>Bool) > Foo' }
 data a + b = Plus a b
 type Foo = Int + Bool
+Any data type that can be declared in standard Haskell 98 syntax can
+also be declared using GADTstyle syntax. The choice is largely
+stylistic, but GADTstyle declarations differ in one important respect:
+they treat class constraints on the data constructors differently.
+Specifically, if the constructor is given a typeclass context, that
+context is made available by pattern matching. For example: ::
 There is now some potential ambiguity in import and export lists; for
 example if you write ``import M( (+) )`` do you mean the *function*
 ``(+)`` or the *type constructor* ``(+)``? The default is the former,
 but with :ghcflag:`XExplicitNamespaces` (which is implied by
 :ghcflag:`XTypeOperators`) GHC allows you to specify the latter by
 preceding it with the keyword ``type``, thus: ::
+ data Set a where
+ MkSet :: Eq a => [a] > Set a
 import M( type (+) )
+ makeSet :: Eq a => [a] > Set a
+ makeSet xs = MkSet (nub xs)
 See :ref:`explicitnamespaces`.
+ insert :: a > Set a > Set a
+ insert a (MkSet as)  a `elem` as = MkSet as
+  otherwise = MkSet (a:as)
 The fixity of a type operator may be set using the usual fixity
 declarations but, as in :ref:`infixtycons`, the function and type
 constructor share a single fixity.
+A use of ``MkSet`` as a constructor (e.g. in the definition of
+``makeSet``) gives rise to a ``(Eq a)`` constraint, as you would expect.
+The new feature is that patternmatching on ``MkSet`` (as in the
+definition of ``insert``) makes *available* an ``(Eq a)`` context. In
+implementation terms, the ``MkSet`` constructor has a hidden field that
+stores the ``(Eq a)`` dictionary that is passed to ``MkSet``; so when
+patternmatching that dictionary becomes available for the righthand
+side of the match. In the example, the equality dictionary is used to
+satisfy the equality constraint generated by the call to ``elem``, so
+that the type of ``insert`` itself has no ``Eq`` constraint.
.. _typesynonyms:
+For example, one possible application is to reify dictionaries: ::
Liberalised type synonyms

+ data NumInst a where
+ MkNumInst :: Num a => NumInst a
.. ghcflag:: XLiberalTypeSynonyms
+ intInst :: NumInst Int
+ intInst = MkNumInst
 :implies: :ghcflag:`XExplicitForAll`
+ plus :: NumInst a > a > a > a
+ plus MkNumInst p q = p + q
 Relax many of the Haskell 98 rules on type synonym definitions.
+Here, a value of type ``NumInst a`` is equivalent to an explicit
+``(Num a)`` dictionary.
Type synonyms are like macros at the type level, but Haskell 98 imposes
many rules on individual synonym declarations. With the
:ghcflag:`XLiberalTypeSynonyms` extension, GHC does validity checking on types
*only after expanding type synonyms*. That means that GHC can be very
much more liberal about type synonyms than Haskell 98.
+All this applies to constructors declared using the syntax of
+:ref:`existentialwithcontext`. For example, the ``NumInst`` data type
+above could equivalently be declared like this: ::
 You can write a ``forall`` (including overloading) in a type synonym,
 thus: ::
+ data NumInst a
+ = Num a => MkNumInst (NumInst a)
 type Discard a = forall b. Show b => a > b > (a, String)
+Notice that, unlike the situation when declaring an existential, there
+is no ``forall``, because the ``Num`` constrains the data type's
+universally quantified type variable ``a``. A constructor may have both
+universal and existential type variables: for example, the following two
+declarations are equivalent: ::
 f :: Discard a
 f x y = (x, show y)
+ data T1 a
+ = forall b. (Num a, Eq b) => MkT1 a b
+ data T2 a where
+ MkT2 :: (Num a, Eq b) => a > b > T2 a
 g :: Discard Int > (Int,String)  A rank2 type
 g f = f 3 True
+All this behaviour contrasts with Haskell 98's peculiar treatment of
+contexts on a data type declaration (Section 4.2.1 of the Haskell 98
+Report). In Haskell 98 the definition ::
 If you also use :ghcflag:`XUnboxedTuples`, you can write an unboxed tuple
 in a type synonym: ::
+ data Eq a => Set' a = MkSet' [a]
 type Pr = (# Int, Int #)
+gives ``MkSet'`` the same type as ``MkSet`` above. But instead of
+*making available* an ``(Eq a)`` constraint, patternmatching on
+``MkSet'`` *requires* an ``(Eq a)`` constraint! GHC faithfully
+implements this behaviour, odd though it is. But for GADTstyle
+declarations, GHC's behaviour is much more useful, as well as much more
+intuitive.
 h :: Int > Pr
 h x = (# x, x #)
+The rest of this section gives further details about GADTstyle data
+type declarations.
 You can apply a type synonym to a forall type: ::
+ The result type of each data constructor must begin with the type
+ constructor being defined. If the result type of all constructors has
+ the form ``T a1 ... an``, where ``a1 ... an`` are distinct type
+ variables, then the data type is *ordinary*; otherwise is a
+ *generalised* data type (:ref:`gadt`).
 type Foo a = a > a > Bool
+ As with other type signatures, you can give a single signature for
+ several data constructors. In this example we give a single signature
+ for ``T1`` and ``T2``: ::
 f :: Foo (forall b. b>b)
+ data T a where
+ T1,T2 :: a > T a
+ T3 :: T a
 After expanding the synonym, ``f`` has the legal (in GHC) type: ::
+ The type signature of each constructor is independent, and is
+ implicitly universally quantified as usual. In particular, the type
+ variable(s) in the "``data T a where``" header have no scope, and
+ different constructors may have different universallyquantified type
+ variables: ::
 f :: (forall b. b>b) > (forall b. b>b) > Bool
+ data T a where  The 'a' has no scope
+ T1,T2 :: b > T b  Means forall b. b > T b
+ T3 :: T a  Means forall a. T a
 You can apply a type synonym to a partially applied type synonym: ::
+ A constructor signature may mention type class constraints, which can
+ differ for different constructors. For example, this is fine: ::
 type Generic i o = forall x. i x > o x
 type Id x = x
+ data T a where
+ T1 :: Eq b => b > b > T b
+ T2 :: (Show c, Ix c) => c > [c] > T c
 foo :: Generic Id []
+ When pattern matching, these constraints are made available to
+ discharge constraints in the body of the match. For example: ::
 After expanding the synonym, ``foo`` has the legal (in GHC) type: ::
+ f :: T a > String
+ f (T1 x y)  x==y = "yes"
+  otherwise = "no"
+ f (T2 a b) = show a
 foo :: forall x. x > [x]
+ Note that ``f`` is not overloaded; the ``Eq`` constraint arising from
+ the use of ``==`` is discharged by the pattern match on ``T1`` and
+ similarly the ``Show`` constraint arising from the use of ``show``.
GHC currently does kind checking before expanding synonyms (though even
that could be changed)..
+ Unlike a Haskell98style data type declaration, the type variable(s)
+ in the "``data Set a where``" header have no scope. Indeed, one can
+ write a kind signature instead: ::
After expanding type synonyms, GHC does validity checking on types,
looking for the following malformedness which isn't detected simply by
kind checking:
+ data Set :: * > * where ...
 Type constructor applied to a type involving foralls (if
 :ghcflag:`XImpredicativeTypes` is off)
+ or even a mixture of the two: ::
 Partiallyapplied type synonym.
+ data Bar a :: (* > *) > * where ...
So, for example, this will be rejected: ::
+ The type variables (if given) may be explicitly kinded, so we could
+ also write the header for ``Foo`` like this: ::
 type Pr = forall a. a
+ data Bar a (b :: * > *) where ...
 h :: [Pr]
 h = ...
+ You can use strictness annotations, in the obvious places in the
+ constructor type: ::
because GHC does not allow type constructors applied to forall types.
+ data Term a where
+ Lit :: !Int > Term Int
+ If :: Term Bool > !(Term a) > !(Term a) > Term a
+ Pair :: Term a > Term b > Term (a,b)
.. _existentialquantification:
+ You can use a ``deriving`` clause on a GADTstyle data type
+ declaration. For example, these two declarations are equivalent ::
Existentially quantified data constructors

+ data Maybe1 a where {
+ Nothing1 :: Maybe1 a ;
+ Just1 :: a > Maybe1 a
+ } deriving( Eq, Ord )
.. ghcflag:: XExistentialQuantification
+ data Maybe2 a = Nothing2  Just2 a
+ deriving( Eq, Ord )
 :implies: :ghcflag:`XExplicitForAll`
+ The type signature may have quantified type variables that do not
+ appear in the result type: ::
 Allow existentially quantified type variables in types.
+ data Foo where
+ MkFoo :: a > (a>Bool) > Foo
+ Nil :: Foo
The idea of using existential quantification in data type declarations
was suggested by Perry, and implemented in Hope+ (Nigel Perry, *The
Implementation of Practical Functional Programming Languages*, PhD
Thesis, University of London, 1991). It was later formalised by Laufer
and Odersky (*Polymorphic type inference and abstract data types*,
TOPLAS, 16(5), pp. 14111430, 1994). It's been in Lennart Augustsson's
``hbc`` Haskell compiler for several years, and proved very useful.
Here's the idea. Consider the declaration: ::
+ Here the type variable ``a`` does not appear in the result type of
+ either constructor. Although it is universally quantified in the type
+ of the constructor, such a type variable is often called
+ "existential". Indeed, the above declaration declares precisely the
+ same type as the ``data Foo`` in :ref:`existentialquantification`.
 data Foo = forall a. MkFoo a (a > Bool)
  Nil
+ The type may contain a class context too, of course: ::
The data type ``Foo`` has two constructors with types: ::
+ data Showable where
+ MkShowable :: Show a => a > Showable
 MkFoo :: forall a. a > (a > Bool) > Foo
 Nil :: Foo
+ You can use record syntax on a GADTstyle data type declaration: ::
Notice that the type variable ``a`` in the type of ``MkFoo`` does not
appear in the data type itself, which is plain ``Foo``. For example, the
following expression is fine: ::
+ data Person where
+ Adult :: { name :: String, children :: [Person] } > Person
+ Child :: Show a => { name :: !String, funny :: a } > Person
 [MkFoo 3 even, MkFoo 'c' isUpper] :: [Foo]
+ As usual, for every constructor that has a field ``f``, the type of
+ field ``f`` must be the same (modulo alpha conversion). The ``Child``
+ constructor above shows that the signature may have a context,
+ existentiallyquantified variables, and strictness annotations, just
+ as in the nonrecord case. (NB: the "type" that follows the
+ doublecolon is not really a type, because of the record syntax and
+ strictness annotations. A "type" of this form can appear only in a
+ constructor signature.)
Here, ``(MkFoo 3 even)`` packages an integer with a function ``even``
that maps an integer to ``Bool``; and ``MkFoo 'c'
isUpper`` packages a character with a compatible function. These two
things are each of type ``Foo`` and can be put in a list.
+ Record updates are allowed with GADTstyle declarations, only fields
+ that have the following property: the type of the field mentions no
+ existential type variables.
What can we do with a value of type ``Foo``? In particular, what
happens when we patternmatch on ``MkFoo``? ::
+ As in the case of existentials declared using the Haskell98like
+ record syntax (:ref:`existentialrecords`), recordselector functions
+ are generated only for those fields that have welltyped selectors.
+ Here is the example of that section, in GADTstyle syntax: ::
 f (MkFoo val fn) = ???
+ data Counter a where
+ NewCounter :: { _this :: self
+ , _inc :: self > self
+ , _display :: self > IO ()
+ , tag :: a
+ } > Counter a
Since all we know about ``val`` and ``fn`` is that they are compatible,
the only (useful) thing we can do with them is to apply ``fn`` to
``val`` to get a boolean. For example: ::
+ As before, only one selector function is generated here, that for
+ ``tag``. Nevertheless, you can still use all the field names in
+ pattern matching and record construction.
 f :: Foo > Bool
 f (MkFoo val fn) = fn val
+ In a GADTstyle data type declaration there is no obvious way to
+ specify that a data constructor should be infix, which makes a
+ difference if you derive ``Show`` for the type. (Data constructors
+ declared infix are displayed infix by the derived ``show``.) So GHC
+ implements the following design: a data constructor declared in a
+ GADTstyle data type declaration is displayed infix by ``Show`` iff
+ (a) it is an operator symbol, (b) it has two arguments, (c) it has a
+ programmersupplied fixity declaration. For example
What this allows us to do is to package heterogeneous values together
with a bunch of functions that manipulate them, and then treat that
collection of packages in a uniform manner. You can express quite a bit
of objectorientedlike programming this way.
+ ::
.. _existential:
+ infix 6 (::)
+ data T a where
+ (::) :: Int > Bool > T Int
Why existential?
~~~~~~~~~~~~~~~~
+.. _gadt:
What has this to do with *existential* quantification? Simply that
``MkFoo`` has the (nearly) isomorphic type ::
+Generalised Algebraic Data Types (GADTs)
+
 MkFoo :: (exists a . (a, a > Bool)) > Foo
+.. ghcflag:: XGADTs
But Haskell programmers can safely think of the ordinary *universally*
quantified type given above, thereby avoiding adding a new existential
quantification construct.
+ :implies: :ghcflag:`XMonoLocalBinds`, :ghcflag:`XGADTSyntax`
.. _existentialwithcontext:
+ Allow use of Generalised Algebraic Data Types (GADTs).
Existentials and type classes
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Generalised Algebraic Data Types generalise ordinary algebraic data
+types by allowing constructors to have richer return types. Here is an
+example: ::
An easy extension is to allow arbitrary contexts before the constructor.
For example: ::
+ data Term a where
+ Lit :: Int > Term Int
+ Succ :: Term Int > Term Int
+ IsZero :: Term Int > Term Bool
+ If :: Term Bool > Term a > Term a > Term a
+ Pair :: Term a > Term b > Term (a,b)
 data Baz = forall a. Eq a => Baz1 a a
  forall b. Show b => Baz2 b (b > b)
+Notice that the return type of the constructors is not always
+``Term a``, as is the case with ordinary data types. This generality
+allows us to write a welltyped ``eval`` function for these ``Terms``: ::
The two constructors have the types you'd expect: ::
+ eval :: Term a > a
+ eval (Lit i) = i
+ eval (Succ t) = 1 + eval t
+ eval (IsZero t) = eval t == 0
+ eval (If b e1 e2) = if eval b then eval e1 else eval e2
+ eval (Pair e1 e2) = (eval e1, eval e2)
 Baz1 :: forall a. Eq a => a > a > Baz
 Baz2 :: forall b. Show b => b > (b > b) > Baz
+The key point about GADTs is that *pattern matching causes type
+refinement*. For example, in the right hand side of the equation ::
But when pattern matching on ``Baz1`` the matched values can be compared
for equality, and when pattern matching on ``Baz2`` the first matched
value can be converted to a string (as well as applying the function to
it). So this program is legal: ::
+ eval :: Term a > a
+ eval (Lit i) = ...
 f :: Baz > String
 f (Baz1 p q)  p == q = "Yes"
  otherwise = "No"
 f (Baz2 v fn) = show (fn v)
+the type ``a`` is refined to ``Int``. That's the whole point! A precise
+specification of the type rules is beyond what this user manual aspires
+to, but the design closely follows that described in the paper `Simple
+unificationbased type inference for
+GADTs `__, (ICFP
+2006). The general principle is this: *type refinement is only carried
+out based on usersupplied type annotations*. So if no type signature is
+supplied for ``eval``, no type refinement happens, and lots of obscure
+error messages will occur. However, the refinement is quite general. For
+example, if we had: ::
Operationally, in a dictionarypassing implementation, the constructors
``Baz1`` and ``Baz2`` must store the dictionaries for ``Eq`` and
``Show`` respectively, and extract it on pattern matching.
+ eval :: Term a > a > a
+ eval (Lit i) j = i+j
.. _existentialrecords:
+the pattern match causes the type ``a`` to be refined to ``Int``
+(because of the type of the constructor ``Lit``), and that refinement
+also applies to the type of ``j``, and the result type of the ``case``
+expression. Hence the addition ``i+j`` is legal.
Record Constructors
~~~~~~~~~~~~~~~~~~~
+These and many other examples are given in papers by Hongwei Xi, and Tim
+Sheard. There is a longer introduction `on the
+wiki `__, and Ralf Hinze's `Fun
+with phantom
+types `__ also
+has a number of examples. Note that papers may use different notation to
+that implemented in GHC.
GHC allows existentials to be used with records syntax as well. For
example: ::
+The rest of this section outlines the extensions to GHC that support
+GADTs. The extension is enabled with :ghcflag:`XGADTs`. The :ghcflag:`XGADTs` flag
+also sets :ghcflag:`XGADTSyntax` and :ghcflag:`XMonoLocalBinds`.
 data Counter a = forall self. NewCounter
 { _this :: self
 , _inc :: self > self
 , _display :: self > IO ()
 , tag :: a
 }
+ A GADT can only be declared using GADTstyle syntax
+ (:ref:`gadtstyle`); the old Haskell 98 syntax for data declarations
+ always declares an ordinary data type. The result type of each
+ constructor must begin with the type constructor being defined, but
+ for a GADT the arguments to the type constructor can be arbitrary
+ monotypes. For example, in the ``Term`` data type above, the type of
+ each constructor must end with ``Term ty``, but the ``ty`` need not
+ be a type variable (e.g. the ``Lit`` constructor).
Here ``tag`` is a public field, with a welltyped selector function
``tag :: Counter a > a``. The ``self`` type is hidden from the outside;
any attempt to apply ``_this``, ``_inc`` or ``_display`` as functions
will raise a compiletime error. In other words, *GHC defines a record
selector function only for fields whose type does not mention the
existentiallyquantified variables*. (This example used an underscore in
the fields for which record selectors will not be defined, but that is
only programming style; GHC ignores them.)
+ It is permitted to declare an ordinary algebraic data type using
+ GADTstyle syntax. What makes a GADT into a GADT is not the syntax,
+ but rather the presence of data constructors whose result type is not
+ just ``T a b``.
To make use of these hidden fields, we need to create some helper
functions: ::
+ You cannot use a ``deriving`` clause for a GADT; only for an ordinary
+ data type.
 inc :: Counter a > Counter a
 inc (NewCounter x i d t) = NewCounter
 { _this = i x, _inc = i, _display = d, tag = t }
+ As mentioned in :ref:`gadtstyle`, record syntax is supported. For
+ example:
 display :: Counter a > IO ()
 display NewCounter{ _this = x, _display = d } = d x
+ ::
Now we can define counters with different underlying implementations: ::
+ data Term a where
+ Lit :: { val :: Int } > Term Int
+ Succ :: { num :: Term Int } > Term Int
+ Pred :: { num :: Term Int } > Term Int
+ IsZero :: { arg :: Term Int } > Term Bool
+ Pair :: { arg1 :: Term a
+ , arg2 :: Term b
+ } > Term (a,b)
+ If :: { cnd :: Term Bool
+ , tru :: Term a
+ , fls :: Term a
+ } > Term a
 counterA :: Counter String
 counterA = NewCounter
 { _this = 0, _inc = (1+), _display = print, tag = "A" }
+ However, for GADTs there is the following additional constraint:
+ every constructor that has a field ``f`` must have the same result
+ type (modulo alpha conversion) Hence, in the above example, we cannot
+ merge the ``num`` and ``arg`` fields above into a single name.
+ Although their field types are both ``Term Int``, their selector
+ functions actually have different types:
 counterB :: Counter String
 counterB = NewCounter
 { _this = "", _inc = ('#':), _display = putStrLn, tag = "B" }
+ ::
 main = do
 display (inc counterA)  prints "1"
 display (inc (inc counterB))  prints "##"
+ num :: Term Int > Term Int
+ arg :: Term Bool > Term Int
Record update syntax is supported for existentials (and GADTs): ::
+ When patternmatching against data constructors drawn from a GADT,
+ for example in a ``case`` expression, the following rules apply:
 setTag :: Counter a > a > Counter a
 setTag obj t = obj{ tag = t }
+  The type of the scrutinee must be rigid.
The rule for record update is this:
+  The type of the entire ``case`` expression must be rigid.
 the types of the updated fields may mention only the universallyquantified
 type variables of the data constructor. For GADTs, the field may mention
 only types that appear as a simple typevariable argument in the
 constructor's result type.
+  The type of any free variable mentioned in any of the ``case``
+ alternatives must be rigid.
For example: ::
+ A type is "rigid" if it is completely known to the compiler at its
+ binding site. The easiest way to ensure that a variable a rigid type
+ is to give it a type signature. For more precise details see `Simple
+ unificationbased type inference for
+ GADTs `__. The
+ criteria implemented by GHC are given in the Appendix.
 data T a b where { T1 { f1::a, f2::b, f3::(b,c) } :: T a b }  c is existential
 upd1 t x = t { f1=x }  OK: upd1 :: T a b > a' > T a' b
 upd2 t x = t { f3=x }  BAD (f3's type mentions c, which is
  existentially quantified)
+.. _recordsystemextensions:
 data G a b where { G1 { g1::a, g2::c } :: G a [c] }
 upd3 g x = g { g1=x }  OK: upd3 :: G a b > c > G c b
 upd4 g x = g { g2=x }  BAD (f2's type mentions c, which is not a simple
  typevariable argument in G1's result type)
+Extensions to the record system
+===============================
Restrictions
~~~~~~~~~~~~
+.. _traditionalrecordsyntax:
There are several restrictions on the ways in which existentiallyquantified
constructors can be used.
+Traditional record syntax
+
 When pattern matching, each pattern match introduces a new, distinct,
 type for each existential type variable. These types cannot be
 unified with any other type, nor can they escape from the scope of
 the pattern match. For example, these fragments are incorrect: ::
+.. ghcflag:: XNoTraditionalRecordSyntax
 f1 (MkFoo a f) = a
+ :since: 7.4.1
 Here, the type bound by ``MkFoo`` "escapes", because ``a`` is the
 result of ``f1``. One way to see why this is wrong is to ask what
 type ``f1`` has: ::
+ Disallow use of record syntax.
 f1 :: Foo > a  Weird!
+Traditional record syntax, such as ``C {f = x}``, is enabled by default.
+To disable it, you can use the :ghcflag:`XNoTraditionalRecordSyntax` flag.
 What is this "``a``" in the result type? Clearly we don't mean this: ::
+.. _disambiguatefields:
 f1 :: forall a. Foo > a  Wrong!
+Record field disambiguation
+
+
+.. ghcflag:: XDisambiguateRecordFields
 The original program is just plain wrong. Here's another sort of
 error ::
+ Allow the compiler to automatically choose between identicallynamed
+ record selectors based on type (if the choice is unambiguous).
 f2 (Baz1 a b) (Baz1 p q) = a==q
+In record construction and record pattern matching it is entirely
+unambiguous which field is referred to, even if there are two different
+data types in scope with a common field name. For example:
 It's ok to say ``a==b`` or ``p==q``, but ``a==q`` is wrong because it
 equates the two distinct types arising from the two ``Baz1``
 constructors.
+::
 You can't patternmatch on an existentially quantified constructor in
 a ``let`` or ``where`` group of bindings. So this is illegal: ::
+ module M where
+ data S = MkS { x :: Int, y :: Bool }
 f3 x = a==b where { Baz1 a b = x }
+ module Foo where
+ import M
 Instead, use a ``case`` expression: ::
+ data T = MkT { x :: Int }
 f3 x = case x of Baz1 a b > a==b
+ ok1 (MkS { x = n }) = n+1  Unambiguous
+ ok2 n = MkT { x = n+1 }  Unambiguous
 In general, you can only patternmatch on an existentiallyquantified
 constructor in a ``case`` expression or in the patterns of a function
 definition. The reason for this restriction is really an
 implementation one. Typechecking binding groups is already a
 nightmare without existentials complicating the picture. Also an
 existential pattern binding at the top level of a module doesn't make
 sense, because it's not clear how to prevent the
 existentiallyquantified type "escaping". So for now, there's a
 simpletostate restriction. We'll see how annoying it is.
+ bad1 k = k { x = 3 }  Ambiguous
+ bad2 k = x k  Ambiguous
 You can't use existential quantification for ``newtype``
 declarations. So this is illegal: ::
+Even though there are two ``x``'s in scope, it is clear that the ``x``
+in the pattern in the definition of ``ok1`` can only mean the field
+``x`` from type ``S``. Similarly for the function ``ok2``. However, in
+the record update in ``bad1`` and the record selection in ``bad2`` it is
+not clear which of the two types is intended.
 newtype T = forall a. Ord a => MkT a
+Haskell 98 regards all four as ambiguous, but with the
+:ghcflag:`XDisambiguateRecordFields` flag, GHC will accept the former two. The
+rules are precisely the same as those for instance declarations in
+Haskell 98, where the method names on the lefthand side of the method
+bindings in an instance declaration refer unambiguously to the method of
+that class (provided they are in scope at all), even if there are other
+variables in scope with the same name. This reduces the clutter of
+qualified names when you import two records from different modules that
+use the same field name.
 Reason: a value of type ``T`` must be represented as a pair of a
 dictionary for ``Ord t`` and a value of type ``t``. That contradicts
 the idea that ``newtype`` should have no concrete representation. You
 can get just the same efficiency and effect by using ``data`` instead
 of ``newtype``. If there is no overloading involved, then there is
 more of a case for allowing an existentiallyquantified ``newtype``,
 because the ``data`` version does carry an implementation cost, but
 singlefield existentially quantified constructors aren't much use.
 So the simple restriction (no existential stuff on ``newtype``)
 stands, unless there are convincing reasons to change it.
+Some details:
 You can't use ``deriving`` to define instances of a data type with
 existentially quantified data constructors. Reason: in most cases it
 would not make sense. For example:; ::
+ Field disambiguation can be combined with punning (see
+ :ref:`recordpuns`). For example: ::
 data T = forall a. MkT [a] deriving( Eq )
+ module Foo where
+ import M
+ x=True
+ ok3 (MkS { x }) = x+1  Uses both disambiguation and punning
 To derive ``Eq`` in the standard way we would need to have equality
 between the single component of two ``MkT`` constructors: ::
+ With :ghcflag:`XDisambiguateRecordFields` you can use *unqualified* field
+ names even if the corresponding selector is only in scope *qualified*
+ For example, assuming the same module ``M`` as in our earlier
+ example, this is legal: ::
 instance Eq T where
 (MkT a) == (MkT b) = ???
+ module Foo where
+ import qualified M  Note qualified
 But ``a`` and ``b`` have distinct types, and so can't be compared.
 It's just about possible to imagine examples in which the derived
 instance would make sense, but it seems altogether simpler simply to
 prohibit such declarations. Define your own instances!
+ ok4 (M.MkS { x = n }) = n+1  Unambiguous
.. _gadtstyle:
+ Since the constructor ``MkS`` is only in scope qualified, you must
+ name it ``M.MkS``, but the field ``x`` does not need to be qualified
+ even though ``M.x`` is in scope but ``x`` is not (In effect, it is
+ qualified by the constructor).
Declaring data types with explicit constructor signatures

+.. _duplicaterecordfields:
.. ghcflag:: XGADTSyntax
+Duplicate record fields
+
 Allow the use of GADT syntax in data type definitions (but not GADTs
 themselves; for this see :ghcflag:`XGADTs`)
+.. ghcflag:: XDuplicateRecordFields
When the ``GADTSyntax`` extension is enabled, GHC allows you to declare
an algebraic data type by giving the type signatures of constructors
explicitly. For example: ::
+ :implies: :ghcflag:`XDisambiguateRecordFields`
+ :since: 8.0.1
 data Maybe a where
 Nothing :: Maybe a
 Just :: a > Maybe a
+ Allow definition of record types with identicallynamed fields.
The form is called a "GADTstyle declaration" because Generalised
Algebraic Data Types, described in :ref:`gadt`, can only be declared
using this form.
+Going beyond :ghcflag:`XDisambiguateRecordFields` (see :ref:`disambiguatefields`),
+the :ghcflag:`XDuplicateRecordFields` extension allows multiple datatypes to be
+declared using the same field names in a single module. For example, it allows
+this: ::
Notice that GADTstyle syntax generalises existential types
(:ref:`existentialquantification`). For example, these two declarations
are equivalent: ::
+ module M where
+ data S = MkS { x :: Int }
+ data T = MkT { x :: Bool }
 data Foo = forall a. MkFoo a (a > Bool)
 data Foo' where { MKFoo :: a > (a>Bool) > Foo' }
+Uses of fields that are always unambiguous because they mention the constructor,
+including construction and patternmatching, may freely use duplicated field
+names. For example, the following are permitted (just as with
+:ghcflag:`XDisambiguateRecordFields`): ::
Any data type that can be declared in standard Haskell 98 syntax can
also be declared using GADTstyle syntax. The choice is largely
stylistic, but GADTstyle declarations differ in one important respect:
they treat class constraints on the data constructors differently.
Specifically, if the constructor is given a typeclass context, that
context is made available by pattern matching. For example: ::
+ s = MkS { x = 3 }
 data Set a where
 MkSet :: Eq a => [a] > Set a
+ f (MkT { x = b }) = b
 makeSet :: Eq a => [a] > Set a
 makeSet xs = MkSet (nub xs)
+Field names used as selector functions or in record updates must be unambiguous,
+either because there is only one such field in scope, or because a type
+signature is supplied, as described in the following sections.
 insert :: a > Set a > Set a
 insert a (MkSet as)  a `elem` as = MkSet as
  otherwise = MkSet (a:as)
+Selector functions
+~~~~~~~~~~~~~~~~~~
A use of ``MkSet`` as a constructor (e.g. in the definition of
``makeSet``) gives rise to a ``(Eq a)`` constraint, as you would expect.
The new feature is that patternmatching on ``MkSet`` (as in the
definition of ``insert``) makes *available* an ``(Eq a)`` context. In
implementation terms, the ``MkSet`` constructor has a hidden field that
stores the ``(Eq a)`` dictionary that is passed to ``MkSet``; so when
patternmatching that dictionary becomes available for the righthand
side of the match. In the example, the equality dictionary is used to
satisfy the equality constraint generated by the call to ``elem``, so
that the type of ``insert`` itself has no ``Eq`` constraint.
+Fields may be used as selector functions only if they are unambiguous, so this
+is still not allowed if both ``S(x)`` and ``T(x)`` are in scope: ::
For example, one possible application is to reify dictionaries: ::
+ bad r = x r
 data NumInst a where
 MkNumInst :: Num a => NumInst a
+An ambiguous selector may be disambiguated by the type being "pushed down" to
+the occurrence of the selector (see :ref:`higherranktypeinference` for more
+details on what "pushed down" means). For example, the following are permitted: ::
 intInst :: NumInst Int
 intInst = MkNumInst
+ ok1 = x :: S > Int
 plus :: NumInst a > a > a > a
 plus MkNumInst p q = p + q
+ ok2 :: S > Int
+ ok2 = x
Here, a value of type ``NumInst a`` is equivalent to an explicit
``(Num a)`` dictionary.
+ ok3 = k x  assuming we already have k :: (S > Int) > _
All this applies to constructors declared using the syntax of
:ref:`existentialwithcontext`. For example, the ``NumInst`` data type
above could equivalently be declared like this: ::
+In addition, the datatype that is meant may be given as a type signature on the
+argument to the selector: ::
 data NumInst a
 = Num a => MkNumInst (NumInst a)
+ ok4 s = x (s :: S)
Notice that, unlike the situation when declaring an existential, there
is no ``forall``, because the ``Num`` constrains the data type's
universally quantified type variable ``a``. A constructor may have both
universal and existential type variables: for example, the following two
declarations are equivalent: ::
+However, we do not infer the type of the argument to determine the datatype, or
+have any way of deferring the choice to the constraint solver. Thus the
+following is ambiguous: ::
 data T1 a
 = forall b. (Num a, Eq b) => MkT1 a b
 data T2 a where
 MkT2 :: (Num a, Eq b) => a > b > T2 a
+ bad :: S > Int
+ bad s = x s
All this behaviour contrasts with Haskell 98's peculiar treatment of
contexts on a data type declaration (Section 4.2.1 of the Haskell 98
Report). In Haskell 98 the definition ::
+Even though a field label is duplicated in its defining module, it may be
+possible to use the selector unambiguously elsewhere. For example, another
+module could import ``S(x)`` but not ``T(x)``, and then use ``x`` unambiguously.
 data Eq a => Set' a = MkSet' [a]
+Record updates
+~~~~~~~~~~~~~~
gives ``MkSet'`` the same type as ``MkSet`` above. But instead of
*making available* an ``(Eq a)`` constraint, patternmatching on
``MkSet'`` *requires* an ``(Eq a)`` constraint! GHC faithfully
implements this behaviour, odd though it is. But for GADTstyle
declarations, GHC's behaviour is much more useful, as well as much more
intuitive.
+In a record update such as ``e { x = 1 }``, if there are multiple ``x`` fields
+in scope, then the type of the context must fix which record datatype is
+intended, or a type annotation must be supplied. Consider the following
+definitions: ::
The rest of this section gives further details about GADTstyle data
type declarations.
+ data S = MkS { foo :: Int }
+ data T = MkT { foo :: Int, bar :: Int }
+ data U = MkU { bar :: Int, baz :: Int }
 The result type of each data constructor must begin with the type
 constructor being defined. If the result type of all constructors has
 the form ``T a1 ... an``, where ``a1 ... an`` are distinct type
 variables, then the data type is *ordinary*; otherwise is a
 *generalised* data type (:ref:`gadt`).
+Without :ghcflag:`XDuplicateRecordFields`, an update mentioning ``foo`` will always be
+ambiguous if all these definitions were in scope. When the extension is enabled,
+there are several options for disambiguating updates:
 As with other type signatures, you can give a single signature for
 several data constructors. In this example we give a single signature
 for ``T1`` and ``T2``: ::
+ Check for types that have all the fields being updated. For example: ::
 data T a where
 T1,T2 :: a > T a
 T3 :: T a
+ f x = x { foo = 3, bar = 2 }
 The type signature of each constructor is independent, and is
 implicitly universally quantified as usual. In particular, the type
 variable(s) in the "``data T a where``" header have no scope, and
 different constructors may have different universallyquantified type
 variables: ::
+ Here ``f`` must be updating ``T`` because neither ``S`` nor ``U`` have both
+ fields.
 data T a where  The 'a' has no scope
 T1,T2 :: b > T b  Means forall b. b > T b
 T3 :: T a  Means forall a. T a
+ Use the type being pushed in to the record update, as in the following: ::
 A constructor signature may mention type class constraints, which can
 differ for different constructors. For example, this is fine: ::
+ g1 :: T > T
+ g1 x = x { foo = 3 }
 data T a where
 T1 :: Eq b => b > b > T b
 T2 :: (Show c, Ix c) => c > [c] > T c
+ g2 x = x { foo = 3 } :: T
 When pattern matching, these constraints are made available to
 discharge constraints in the body of the match. For example: ::
+ g3 = k (x { foo = 3 })  assuming we already have k :: T > _
 f :: T a > String
 f (T1 x y)  x==y = "yes"
  otherwise = "no"
 f (T2 a b) = show a
+ Use an explicit type signature on the record expression, as in: ::
 Note that ``f`` is not overloaded; the ``Eq`` constraint arising from
 the use of ``==`` is discharged by the pattern match on ``T1`` and
 similarly the ``Show`` constraint arising from the use of ``show``.
+ h x = (x :: T) { foo = 3 }
 Unlike a Haskell98style data type declaration, the type variable(s)
 in the "``data Set a where``" header have no scope. Indeed, one can
 write a kind signature instead: ::
+The type of the expression being updated will not be inferred, and no
+constraintsolving will be performed, so the following will be rejected as
+ambiguous: ::
 data Set :: * > * where ...
+ let x :: T
+ x = blah
+ in x { foo = 3 }
 or even a mixture of the two: ::
+ \x > [x { foo = 3 }, blah :: T ]
 data Bar a :: (* > *) > * where ...
+ \ (x :: T) > x { foo = 3 }
 The type variables (if given) may be explicitly kinded, so we could
 also write the header for ``Foo`` like this: ::
+Import and export of record fields
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 data Bar a (b :: * > *) where ...
+When :ghcflag:`XDuplicateRecordFields` is enabled, an ambiguous field must be exported
+as part of its datatype, rather than at the top level. For example, the
+following is legal: ::
 You can use strictness annotations, in the obvious places in the
 constructor type: ::
+ module M (S(x), T(..)) where
+ data S = MkS { x :: Int }
+ data T = MkT { x :: Bool }
 data Term a where
 Lit :: !Int > Term Int
 If :: Term Bool > !(Term a) > !(Term a) > Term a
 Pair :: Term a > Term b > Term (a,b)
+However, this would not be permitted, because ``x`` is ambiguous: ::
 You can use a ``deriving`` clause on a GADTstyle data type
 declaration. For example, these two declarations are equivalent ::
+ module M (x) where ...
 data Maybe1 a where {
 Nothing1 :: Maybe1 a ;
 Just1 :: a > Maybe1 a
 } deriving( Eq, Ord )
+Similar restrictions apply on import.
 data Maybe2 a = Nothing2  Just2 a
 deriving( Eq, Ord )
+.. _recordpuns:
 The type signature may have quantified type variables that do not
 appear in the result type: ::
+Record puns
+
 data Foo where
 MkFoo :: a > (a>Bool) > Foo
 Nil :: Foo
+.. ghcflag:: XNamedFieldPuns
 Here the type variable ``a`` does not appear in the result type of
 either constructor. Although it is universally quantified in the type
 of the constructor, such a type variable is often called
 "existential". Indeed, the above declaration declares precisely the
 same type as the ``data Foo`` in :ref:`existentialquantification`.
+ Allow use of record puns.
 The type may contain a class context too, of course: ::
+Record puns are enabled by the flag :ghcflag:`XNamedFieldPuns`.
 data Showable where
 MkShowable :: Show a => a > Showable
+When using records, it is common to write a pattern that binds a
+variable with the same name as a record field, such as: ::
 You can use record syntax on a GADTstyle data type declaration: ::
+ data C = C {a :: Int}
+ f (C {a = a}) = a
 data Person where
 Adult :: { name :: String, children :: [Person] } > Person
 Child :: Show a => { name :: !String, funny :: a } > Person
+Record punning permits the variable name to be elided, so one can simply
+write ::
 As usual, for every constructor that has a field ``f``, the type of
 field ``f`` must be the same (modulo alpha conversion). The ``Child``
 constructor above shows that the signature may have a context,
 existentiallyquantified variables, and strictness annotations, just
 as in the nonrecord case. (NB: the "type" that follows the
 doublecolon is not really a type, because of the record syntax and
 strictness annotations. A "type" of this form can appear only in a
 constructor signature.)
+ f (C {a}) = a
 Record updates are allowed with GADTstyle declarations, only fields
 that have the following property: the type of the field mentions no
 existential type variables.
+to mean the same pattern as above. That is, in a record pattern, the
+pattern ``a`` expands into the pattern ``a = a`` for the same name
+``a``.
 As in the case of existentials declared using the Haskell98like
 record syntax (:ref:`existentialrecords`), recordselector functions
 are generated only for those fields that have welltyped selectors.
 Here is the example of that section, in GADTstyle syntax: ::
+Note that:
 data Counter a where
 NewCounter :: { _this :: self
 , _inc :: self > self
 , _display :: self > IO ()
 , tag :: a
 } > Counter a
+ Record punning can also be used in an expression, writing, for
+ example, ::
 As before, only one selector function is generated here, that for
 ``tag``. Nevertheless, you can still use all the field names in
 pattern matching and record construction.
+ let a = 1 in C {a}
 In a GADTstyle data type declaration there is no obvious way to
 specify that a data constructor should be infix, which makes a
 difference if you derive ``Show`` for the type. (Data constructors
 declared infix are displayed infix by the derived ``show``.) So GHC
 implements the following design: a data constructor declared in a
 GADTstyle data type declaration is displayed infix by ``Show`` iff
 (a) it is an operator symbol, (b) it has two arguments, (c) it has a
 programmersupplied fixity declaration. For example
+ instead of ::
 ::
+ let a = 1 in C {a = a}
 infix 6 (::)
 data T a where
 (::) :: Int > Bool > T Int
+ The expansion is purely syntactic, so the expanded righthand side
+ expression refers to the nearest enclosing variable that is spelled
+ the same as the field name.
.. _gadt:
+ Puns and other patterns can be mixed in the same record: ::
Generalised Algebraic Data Types (GADTs)

+ data C = C {a :: Int, b :: Int}
+ f (C {a, b = 4}) = a
.. ghcflag:: XGADTs
+ Puns can be used wherever record patterns occur (e.g. in ``let``
+ bindings or at the toplevel).
 :implies: :ghcflag:`XMonoLocalBinds`, :ghcflag:`XGADTSyntax`
+ A pun on a qualified field name is expanded by stripping off the
+ module qualifier. For example: ::
 Allow use of Generalised Algebraic Data Types (GADTs).
+ f (C {M.a}) = a
Generalised Algebraic Data Types generalise ordinary algebraic data
types by allowing constructors to have richer return types. Here is an
example: ::
+ means ::
 data Term a where
 Lit :: Int > Term Int
 Succ :: Term Int > Term Int
 IsZero :: Term Int > Term Bool
 If :: Term Bool > Term a > Term a > Term a
 Pair :: Term a > Term b > Term (a,b)
+ f (M.C {M.a = a}) = a
Notice that the return type of the constructors is not always
``Term a``, as is the case with ordinary data types. This generality
allows us to write a welltyped ``eval`` function for these ``Terms``: ::
+ (This is useful if the field selector ``a`` for constructor ``M.C``
+ is only in scope in qualified form.)
 eval :: Term a > a
 eval (Lit i) = i
 eval (Succ t) = 1 + eval t
 eval (IsZero t) = eval t == 0
 eval (If b e1 e2) = if eval b then eval e1 else eval e2
 eval (Pair e1 e2) = (eval e1, eval e2)
+.. _recordwildcards:
The key point about GADTs is that *pattern matching causes type
refinement*. For example, in the right hand side of the equation ::
+Record wildcards
+
 eval :: Term a > a
 eval (Lit i) = ...
+.. ghcflag:: XRecordWildCards
the type ``a`` is refined to ``Int``. That's the whole point! A precise
specification of the type rules is beyond what this user manual aspires
to, but the design closely follows that described in the paper `Simple
unificationbased type inference for
GADTs `__, (ICFP
2006). The general principle is this: *type refinement is only carried
out based on usersupplied type annotations*. So if no type signature is
supplied for ``eval``, no type refinement happens, and lots of obscure
error messages will occur. However, the refinement is quite general. For
example, if we had: ::
+ :implies: :ghcflag:`XDisambiguateRecordFields`.
 eval :: Term a > a > a
 eval (Lit i) j = i+j
+ Allow the use of wildcards in record construction and pattern matching.
the pattern match causes the type ``a`` to be refined to ``Int``
(because of the type of the constructor ``Lit``), and that refinement
also applies to the type of ``j``, and the result type of the ``case``
expression. Hence the addition ``i+j`` is legal.
+Record wildcards are enabled by the flag :ghcflag:`XRecordWildCards`. This
+flag implies :ghcflag:`XDisambiguateRecordFields`.
These and many other examples are given in papers by Hongwei Xi, and Tim
Sheard. There is a longer introduction `on the
wiki `__, and Ralf Hinze's `Fun
with phantom
types `__ also
has a number of examples. Note that papers may use different notation to
that implemented in GHC.
+For records with many fields, it can be tiresome to write out each field
+individually in a record pattern, as in ::
The rest of this section outlines the extensions to GHC that support
GADTs. The extension is enabled with :ghcflag:`XGADTs`. The :ghcflag:`XGADTs` flag
also sets :ghcflag:`XGADTSyntax` and :ghcflag:`XMonoLocalBinds`.
+ data C = C {a :: Int, b :: Int, c :: Int, d :: Int}
+ f (C {a = 1, b = b, c = c, d = d}) = b + c + d
 A GADT can only be declared using GADTstyle syntax
 (:ref:`gadtstyle`); the old Haskell 98 syntax for data declarations
 always declares an ordinary data type. The result type of each
 constructor must begin with the type constructor being defined, but
 for a GADT the arguments to the type constructor can be arbitrary
 monotypes. For example, in the ``Term`` data type above, the type of
 each constructor must end with ``Term ty``, but the ``ty`` need not
 be a type variable (e.g. the ``Lit`` constructor).
+Record wildcard syntax permits a "``..``" in a record pattern, where
+each elided field ``f`` is replaced by the pattern ``f = f``. For
+example, the above pattern can be written as ::
 It is permitted to declare an ordinary algebraic data type using
 GADTstyle syntax. What makes a GADT into a GADT is not the syntax,
 but rather the presence of data constructors whose result type is not
 just ``T a b``.
+ f (C {a = 1, ..}) = b + c + d
 You cannot use a ``deriving`` clause for a GADT; only for an ordinary
 data type.
+More details:
 As mentioned in :ref:`gadtstyle`, record syntax is supported. For
 example:
+ Record wildcards in patterns can be mixed with other patterns,
+ including puns (:ref:`recordpuns`); for example, in a pattern
+ ``(C {a = 1, b, ..})``. Additionally, record wildcards can be used
+ wherever record patterns occur, including in ``let`` bindings and at
+ the toplevel. For example, the toplevel binding ::
 ::
+ C {a = 1, ..} = e
 data Term a where
 Lit :: { val :: Int } > Term Int
 Succ :: { num :: Term Int } > Term Int
 Pred :: { num :: Term Int } > Term Int
 IsZero :: { arg :: Term Int } > Term Bool
 Pair :: { arg1 :: Term a
 , arg2 :: Term b
 } > Term (a,b)
 If :: { cnd :: Term Bool
 , tru :: Term a
 , fls :: Term a
 } > Term a
+ defines ``b``, ``c``, and ``d``.
 However, for GADTs there is the following additional constraint:
 every constructor that has a field ``f`` must have the same result
 type (modulo alpha conversion) Hence, in the above example, we cannot
 merge the ``num`` and ``arg`` fields above into a single name.
 Although their field types are both ``Term Int``, their selector
 functions actually have different types:
+ Record wildcards can also be used in an expression, when constructing
+ a record. For example, ::
 ::
+ let {a = 1; b = 2; c = 3; d = 4} in C {..}
 num :: Term Int > Term Int
 arg :: Term Bool > Term Int
+ in place of ::
 When patternmatching against data constructors drawn from a GADT,
 for example in a ``case`` expression, the following rules apply:
+ let {a = 1; b = 2; c = 3; d = 4} in C {a=a, b=b, c=c, d=d}
  The type of the scrutinee must be rigid.
+ The expansion is purely syntactic, so the record wildcard expression
+ refers to the nearest enclosing variables that are spelled the same
+ as the omitted field names.
  The type of the entire ``case`` expression must be rigid.
+ Record wildcards may *not* be used in record *updates*. For example
+ this is illegal: ::
  The type of any free variable mentioned in any of the ``case``
 alternatives must be rigid.
+ f r = r { x = 3, .. }
 A type is "rigid" if it is completely known to the compiler at its
 binding site. The easiest way to ensure that a variable a rigid type
 is to give it a type signature. For more precise details see `Simple
 unificationbased type inference for
 GADTs `__. The
 criteria implemented by GHC are given in the Appendix.
+ For both pattern and expression wildcards, the "``..``" expands to
+ the missing *inscope* record fields. Specifically the expansion of
+ "``C {..}``" includes ``f`` if and only if:
.. _recordsystemextensions:
+  ``f`` is a record field of constructor ``C``.
Extensions to the record system
===============================
+  The record field ``f`` is in scope somehow (either qualified or
+ unqualified).
.. _traditionalrecordsyntax:
+  In the case of expressions (but not patterns), the variable ``f``
+ is in scope unqualified, apart from the binding of the record
+ selector itself.
Traditional record syntax

+ These rules restrict record wildcards to the situations in which the
+ user could have written the expanded version. For example ::
.. ghcflag:: XNoTraditionalRecordSyntax
+ module M where
+ data R = R { a,b,c :: Int }
+ module X where
+ import M( R(a,c) )
+ f b = R { .. }
 :since: 7.4.1
+ The ``R{..}`` expands to ``R{M.a=a}``, omitting ``b`` since the
+ record field is not in scope, and omitting ``c`` since the variable
+ ``c`` is not in scope (apart from the binding of the record selector
+ ``c``, of course).
 Disallow use of record syntax.
+ Record wildcards cannot be used (a) in a record update construct, and
+ (b) for data constructors that are not declared with record fields.
+ For example: ::
Traditional record syntax, such as ``C {f = x}``, is enabled by default.
To disable it, you can use the :ghcflag:`XNoTraditionalRecordSyntax` flag.
+ f x = x { v=True, .. }  Illegal (a)
.. _disambiguatefields:
+ data T = MkT Int Bool
+ g = MkT { .. }  Illegal (b)
+ h (MkT { .. }) = True  Illegal (b)
Record field disambiguation

+.. _deriving:
.. ghcflag:: XDisambiguateRecordFields
+Extensions to the "deriving" mechanism
+======================================
 Allow the compiler to automatically choose between identicallynamed
 record selectors based on type (if the choice is unambiguous).
+.. _derivinginferred:
In record construction and record pattern matching it is entirely
unambiguous which field is referred to, even if there are two different
data types in scope with a common field name. For example:
+Inferred context for deriving clauses
+
::
+The Haskell Report is vague about exactly when a ``deriving`` clause is
+legal. For example: ::
 module M where
 data S = MkS { x :: Int, y :: Bool }
+ data T0 f a = MkT0 a deriving( Eq )
+ data T1 f a = MkT1 (f a) deriving( Eq )
+ data T2 f a = MkT2 (f (f a)) deriving( Eq )
 module Foo where
 import M
+The natural generated ``Eq`` code would result in these instance
+declarations: ::
 data T = MkT { x :: Int }
+ instance Eq a => Eq (T0 f a) where ...
+ instance Eq (f a) => Eq (T1 f a) where ...
+ instance Eq (f (f a)) => Eq (T2 f a) where ...
 ok1 (MkS { x = n }) = n+1  Unambiguous
 ok2 n = MkT { x = n+1 }  Unambiguous
+The first of these is obviously fine. The second is still fine, although
+less obviously. The third is not Haskell 98, and risks losing
+termination of instances.
 bad1 k = k { x = 3 }  Ambiguous
 bad2 k = x k  Ambiguous
+GHC takes a conservative position: it accepts the first two, but not the
+third. The rule is this: each constraint in the inferred instance
+context must consist only of type variables, with no repetitions.
Even though there are two ``x``'s in scope, it is clear that the ``x``
in the pattern in the definition of ``ok1`` can only mean the field
``x`` from type ``S``. Similarly for the function ``ok2``. However, in
the record update in ``bad1`` and the record selection in ``bad2`` it is
not clear which of the two types is intended.
+This rule is applied regardless of flags. If you want a more exotic
+context, you can write it yourself, using the `standalone deriving
+mechanism <#standalonederiving>`__.
Haskell 98 regards all four as ambiguous, but with the
:ghcflag:`XDisambiguateRecordFields` flag, GHC will accept the former two. The
rules are precisely the same as those for instance declarations in
Haskell 98, where the method names on the lefthand side of the method
bindings in an instance declaration refer unambiguously to the method of
that class (provided they are in scope at all), even if there are other
variables in scope with the same name. This reduces the clutter of
qualified names when you import two records from different modules that
use the same field name.
+.. _standalonederiving:
Some details:
+Standalone deriving declarations
+
 Field disambiguation can be combined with punning (see
 :ref:`recordpuns`). For example: ::
+.. ghcflag:: XStandaloneDeriving
 module Foo where
 import M
 x=True
 ok3 (MkS { x }) = x+1  Uses both disambiguation and punning
+ Allow the use of standalone ``deriving`` declarations.
 With :ghcflag:`XDisambiguateRecordFields` you can use *unqualified* field
 names even if the corresponding selector is only in scope *qualified*
 For example, assuming the same module ``M`` as in our earlier
 example, this is legal: ::
+GHC allows standalone ``deriving`` declarations, enabled by
+:ghcflag:`XStandaloneDeriving`: ::
 module Foo where
 import qualified M  Note qualified
+ data Foo a = Bar a  Baz String
 ok4 (M.MkS { x = n }) = n+1  Unambiguous
+ deriving instance Eq a => Eq (Foo a)
 Since the constructor ``MkS`` is only in scope qualified, you must
 name it ``M.MkS``, but the field ``x`` does not need to be qualified
 even though ``M.x`` is in scope but ``x`` is not (In effect, it is
 qualified by the constructor).
+The syntax is identical to that of an ordinary instance declaration
+apart from (a) the keyword ``deriving``, and (b) the absence of the
+``where`` part.
.. _duplicaterecordfields:
+However, standalone deriving differs from a ``deriving`` clause in a
+number of important ways:
Duplicate record fields

+ The standalone deriving declaration does not need to be in the same
+ module as the data type declaration. (But be aware of the dangers of
+ orphan instances (:ref:`orphanmodules`).
.. ghcflag:: XDuplicateRecordFields
+ You must supply an explicit context (in the example the context is
+ ``(Eq a)``), exactly as you would in an ordinary instance
+ declaration. (In contrast, in a ``deriving`` clause attached to a
+ data type declaration, the context is inferred.)
 :implies: :ghcflag:`XDisambiguateRecordFields`
 :since: 8.0.1
+ Unlike a ``deriving`` declaration attached to a ``data`` declaration,
+ the instance can be more specific than the data type (assuming you
+ also use :ghcflag:`XFlexibleInstances`, :ref:`instancerules`). Consider
+ for example ::
 Allow definition of record types with identicallynamed fields.
+ data Foo a = Bar a  Baz String
Going beyond :ghcflag:`XDisambiguateRecordFields` (see :ref:`disambiguatefields`),
the :ghcflag:`XDuplicateRecordFields` extension allows multiple datatypes to be
declared using the same field names in a single module. For example, it allows
this: ::
+ deriving instance Eq a => Eq (Foo [a])
+ deriving instance Eq a => Eq (Foo (Maybe a))
 module M where
 data S = MkS { x :: Int }
 data T = MkT { x :: Bool }
+ This will generate a derived instance for ``(Foo [a])`` and
+ ``(Foo (Maybe a))``, but other types such as ``(Foo (Int,Bool))``
+ will not be an instance of ``Eq``.
Uses of fields that are always unambiguous because they mention the constructor,
including construction and patternmatching, may freely use duplicated field
names. For example, the following are permitted (just as with
:ghcflag:`XDisambiguateRecordFields`): ::
+ Unlike a ``deriving`` declaration attached to a ``data`` declaration,
+ GHC does not restrict the form of the data type. Instead, GHC simply
+ generates the appropriate boilerplate code for the specified class,
+ and typechecks it. If there is a type error, it is your problem. (GHC
+ will show you the offending code if it has a type error.)
 s = MkS { x = 3 }
+ The merit of this is that you can derive instances for GADTs and
+ other exotic data types, providing only that the boilerplate code
+ does indeed typecheck. For example: ::
 f (MkT { x = b }) = b
+ data T a where
+ T1 :: T Int
+ T2 :: T Bool
Field names used as selector functions or in record updates must be unambiguous,
either because there is only one such field in scope, or because a type
signature is supplied, as described in the following sections.
+ deriving instance Show (T a)
Selector functions
~~~~~~~~~~~~~~~~~~
+ In this example, you cannot say ``... deriving( Show )`` on the data
+ type declaration for ``T``, because ``T`` is a GADT, but you *can*
+ generate the instance declaration using standalone deriving.
Fields may be used as selector functions only if they are unambiguous, so this
is still not allowed if both ``S(x)`` and ``T(x)`` are in scope: ::
+ The downside is that, if the boilerplate code fails to typecheck,
+ you will get an error message about that code, which you did not
+ write. Whereas, with a ``deriving`` clause the sideconditions are
+ necessarily more conservative, but any error message may be more
+ comprehensible.
 bad r = x r
+In other ways, however, a standalone deriving obeys the same rules as
+ordinary deriving:
An ambiguous selector may be disambiguated by the type being "pushed down" to
the occurrence of the selector (see :ref:`higherranktypeinference` for more
details on what "pushed down" means). For example, the following are permitted: ::
+ A ``deriving instance`` declaration must obey the same rules
+ concerning form and termination as ordinary instance declarations,
+ controlled by the same flags; see :ref:`instancedecls`.
 ok1 = x :: S > Int
+ The standalone syntax is generalised for newtypes in exactly the
+ same way that ordinary ``deriving`` clauses are generalised
+ (:ref:`newtypederiving`). For example: ::
 ok2 :: S > Int
 ok2 = x
+ newtype Foo a = MkFoo (State Int a)
 ok3 = k x  assuming we already have k :: (S > Int) > _
+ deriving instance MonadState Int Foo
In addition, the datatype that is meant may be given as a type signature on the
argument to the selector: ::
+ GHC always treats the *last* parameter of the instance (``Foo`` in
+ this example) as the type whose instance is being derived.
 ok4 s = x (s :: S)
+.. _derivingextra:
However, we do not infer the type of the argument to determine the datatype, or
have any way of deferring the choice to the constraint solver. Thus the
following is ambiguous: ::
+Deriving instances of extra classes (``Data``, etc.)
+
+
+.. ghcflag:: XDeriveGeneric
+
+ Allow automatic deriving of instances for the ``Generic`` typeclass.
 bad :: S > Int
 bad s = x s
+.. ghcflag:: XDeriveFunctor
Even though a field label is duplicated in its defining module, it may be
possible to use the selector unambiguously elsewhere. For example, another
module could import ``S(x)`` but not ``T(x)``, and then use ``x`` unambiguously.
+ Allow automatic deriving of instances for the ``Functor`` typeclass.
Record updates
~~~~~~~~~~~~~~
+.. ghcflag:: XDeriveFoldable
In a record update such as ``e { x = 1 }``, if there are multiple ``x`` fields
in scope, then the type of the context must fix which record datatype is
intended, or a type annotation must be supplied. Consider the following
definitions: ::
+ Allow automatic deriving of instances for the ``Foldable`` typeclass.
 data S = MkS { foo :: Int }
 data T = MkT { foo :: Int, bar :: Int }
 data U = MkU { bar :: Int, baz :: Int }
+.. ghcflag:: XDeriveTraversable
Without :ghcflag:`XDuplicateRecordFields`, an update mentioning ``foo`` will always be
ambiguous if all these definitions were in scope. When the extension is enabled,
there are several options for disambiguating updates:
+ :implies: :ghcflag:`XDeriveFoldable`, :ghcflag:`XDeriveFunctor`
 Check for types that have all the fields being updated. For example: ::
+ Allow automatic deriving of instances for the ``Traversable`` typeclass.
 f x = x { foo = 3, bar = 2 }
+Haskell 98 allows the programmer to add "``deriving( Eq, Ord )``" to a
+data type declaration, to generate a standard instance declaration for
+classes specified in the ``deriving`` clause. In Haskell 98, the only
+classes that may appear in the ``deriving`` clause are the standard
+classes ``Eq``, ``Ord``, ``Enum``, ``Ix``, ``Bounded``, ``Read``, and
+``Show``.
 Here ``f`` must be updating ``T`` because neither ``S`` nor ``U`` have both
 fields.
+GHC extends this list with several more classes that may be
+automatically derived:
 Use the type being pushed in to the record update, as in the following: ::
+ With :ghcflag:`XDeriveGeneric`, you can derive instances of the classes
+ ``Generic`` and ``Generic1``, defined in ``GHC.Generics``. You can
+ use these to define generic functions, as described in
+ :ref:`genericprogramming`.
 g1 :: T > T
 g1 x = x { foo = 3 }
+ With :ghcflag:`XDeriveFunctor`, you can derive instances of the class
+ ``Functor``, defined in ``GHC.Base``. See :ref:`derivingfunctor`.
 g2 x = x { foo = 3 } :: T
+ With :ghcflag:`XDeriveDataTypeable`, you can derive instances of the class
+ ``Data``, defined in ``Data.Data``. See :ref:`derivingtypeable` for
+ deriving ``Typeable``.
 g3 = k (x { foo = 3 })  assuming we already have k :: T > _
+ With :ghcflag:`XDeriveFoldable`, you can derive instances of the class
+ ``Foldable``, defined in ``Data.Foldable``. See
+ :ref:`derivingfoldable`.
 Use an explicit type signature on the record expression, as in: ::
+ With :ghcflag:`XDeriveTraversable`, you can derive instances of the class
+ ``Traversable``, defined in ``Data.Traversable``. Since the
+ ``Traversable`` instance dictates the instances of ``Functor`` and
+ ``Foldable``, you'll probably want to derive them too, so
+ :ghcflag:`XDeriveTraversable` implies :ghcflag:`XDeriveFunctor` and
+ :ghcflag:`XDeriveFoldable`. See :ref:`derivingtraversable`.
 h x = (x :: T) { foo = 3 }
+ With :ghcflag:`XDeriveLift`, you can derive instances of the class ``Lift``,
+ defined in the ``Language.Haskell.TH.Syntax`` module of the
+ ``templatehaskell`` package. See :ref:`derivinglift`.
The type of the expression being updated will not be inferred, and no
constraintsolving will be performed, so the following will be rejected as
ambiguous: ::
+You can also use a standalone deriving declaration instead (see
+:ref:`standalonederiving`).
 let x :: T
 x = blah
 in x { foo = 3 }
+In each case the appropriate class must be in scope before it can be
+mentioned in the ``deriving`` clause.
 \x > [x { foo = 3 }, blah :: T ]
+.. _derivingfunctor:
 \ (x :: T) > x { foo = 3 }
+Deriving ``Functor`` instances
+
Import and export of record fields
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+With :ghcflag:`XDeriveFunctor`, one can derive ``Functor`` instances for data types
+of kind ``* > *``. For example, this declaration::
When :ghcflag:`XDuplicateRecordFields` is enabled, an ambiguous field must be exported
as part of its datatype, rather than at the top level. For example, the
following is legal: ::
+ data Example a = Ex a Char (Example a) (Example Char)
+ deriving Functor
 module M (S(x), T(..)) where
 data S = MkS { x :: Int }
 data T = MkT { x :: Bool }
+would generate the following instance: ::
However, this would not be permitted, because ``x`` is ambiguous: ::
+ instance Functor Example where
+ fmap f (Ex a1 a2 a3 a4) = Ex (f a1) a2 (fmap f a3) a4
 module M (x) where ...
+The basic algorithm for :ghcflag:`XDeriveFunctor` walks the arguments of each
+constructor of a data type, applying a mapping function depending on the type
+of each argument. If a plain type variable is found that is syntactically
+equivalent to the last type parameter of the data type (``a`` in the above
+example), then we apply the function ``f`` directly to it. If a type is
+encountered that is not syntactically equivalent to the last type parameter
+*but does mention* the last type parameter somewhere in it, then a recursive
+call to ``fmap`` is made. If a type is found which doesn't mention the last
+type paramter at all, then it is left alone.
Similar restrictions apply on import.
+The second of those cases, in which a type is unequal to the type parameter but
+does contain the type parameter, can be surprisingly tricky. For example, the
+following example compiles::
.. _recordpuns:
+ newtype Right a = Right (Either Int a) deriving Functor
Record puns

+Modifying the code slightly, however, produces code which will not compile::
.. ghcflag:: XNamedFieldPuns
+ newtype Wrong a = Wrong (Either a Int) deriving Functor
 Allow use of record puns.
+The difference involves the placement of the last type parameter, ``a``. In the
+``Right`` case, ``a`` occurs within the type ``Either Int a``, and moreover, it
+appears as the last type argument of ``Either``. In the ``Wrong`` case,
+however, ``a`` is not the last type argument to ``Either``; rather, ``Int`` is.
Record puns are enabled by the flag :ghcflag:`XNamedFieldPuns`.
+This distinction is important because of the way :ghcflag:`XDeriveFunctor` works. The
+derived ``Functor Right`` instance would be::
When using records, it is common to write a pattern that binds a
variable with the same name as a record field, such as: ::
+ instance Functor Right where
+ fmap f (Right a) = Right (fmap f a)
 data C = C {a :: Int}
 f (C {a = a}) = a
+Given a value of type ``Right a``, GHC must produce a value of type
+``Right b``. Since the argument to the ``Right`` constructor has type
+``Either Int a``, the code recursively calls ``fmap`` on it to produce a value
+of type ``Either Int b``, which is used in turn to construct a final value of
+type ``Right b``.
Record punning permits the variable name to be elided, so one can simply
write ::
+The generated code for the ``Functor Wrong`` instance would look exactly the
+same, except with ``Wrong`` replacing every occurrence of ``Right``. The
+problem is now that ``fmap`` is being applied recursively to a value of type
+``Either a Int``. This cannot possibly produce a value of type
+``Either b Int``, as ``fmap`` can only change the last type parameter! This
+causes the generated code to be illtyped.
 f (C {a}) = a
+As a general rule, if a data type has a derived ``Functor`` instance and its
+last type parameter occurs on the righthand side of the data declaration, then
+either it must (1) occur bare (e.g., ``newtype Id a = a``), or (2) occur as the
+last argument of a type constructor (as in ``Right`` above).
to mean the same pattern as above. That is, in a record pattern, the
pattern ``a`` expands into the pattern ``a = a`` for the same name
``a``.
+There are two exceptions to this rule:
Note that:
+#. Tuple types. When a nonunit tuple is used on the righthand side of a data
+ declaration, :ghcflag:`XDeriveFunctor` treats it as a product of distinct types.
+ In other words, the following code::
 Record punning can also be used in an expression, writing, for
 example, ::
+ newtype Triple a = Triple (a, Int, [a]) deriving Functor
 let a = 1 in C {a}
+ Would result in a generated ``Functor`` instance like so::
 instead of ::
+ instance Functor Triple where
+ fmap f (Triple a) =
+ Triple (case a of
+ (a1, a2, a3) > (f a1, a2, fmap f a3))
 let a = 1 in C {a = a}
+ That is, :ghcflag:`XDeriveFunctor` patternmatches its way into tuples and maps
+ over each type that constitutes the tuple. The generated code is
+ reminiscient of what would be generated from
+ ``data Triple a = Triple a Int [a]``, except with extra machinery to handle
+ the tuple.
 The expansion is purely syntactic, so the expanded righthand side
 expression refers to the nearest enclosing variable that is spelled
 the same as the field name.
+#. Function types. The last type parameter can appear anywhere in a function
+ type as long as it occurs in a *covariant* position. To illustrate what this
+ means, consider the following three examples::
 Puns and other patterns can be mixed in the same record: ::
+ newtype CovFun1 a = CovFun1 (Int > a) deriving Functor
+ newtype CovFun2 a = CovFun2 ((a > Int) > a) deriving Functor
+ newtype CovFun3 a = CovFun3 (((Int > a) > Int) > a) deriving Functor
 data C = C {a :: Int, b :: Int}
 f (C {a, b = 4}) = a
+ All three of these examples would compile without issue. On the other hand::
 Puns can be used wherever record patterns occur (e.g. in ``let``
 bindings or at the toplevel).
+ newtype ContraFun1 a = ContraFun1 (a > Int) deriving Functor
+ newtype ContraFun2 a = ContraFun2 ((Int > a) > Int) deriving Functor
+ newtype ContraFun3 a = ContraFun3 (((a > Int) > a) > Int) deriving Functor
 A pun on a qualified field name is expanded by stripping off the
 module qualifier. For example: ::
+ While these examples look similar, none of them would successfully compile.
+ This is because all occurrences of the last type parameter ``a`` occur in *contravariant* positions, not covariant ones.
 f (C {M.a}) = a
+ Intuitively, a covariant type is *produced*, and a contravariant type is
+ *consumed*. Most types in Haskell are covariant, but the function type is
+ special in that the lefthand side of a function arrow reverses variance. If
+ a function type ``a > b`` appears in a covariant position (e.g.,
+ ``CovFun1`` above), then ``a`` is in a contravariant position and ``b`` is
+ in a covariant position. Similarly, if ``a > b`` appears in a contravariant
+ position (e.g., ``CovFun2`` above), then ``a`` is in ``a`` covariant
+ position and ``b`` is in a contravariant position.
 means ::
+ To see why a data type with a contravariant occurrence of its last type
+ parameter cannot have a derived ``Functor`` instance, let's suppose that a
+ ``Functor ContraFun1`` instance exists. The implementation would look
+ something like this::
 f (M.C {M.a = a}) = a
+ instance Functor ContraFun1 where
+ fmap f (ContraFun g) = ContraFun (\x > _)
 (This is useful if the field selector ``a`` for constructor ``M.C``
 is only in scope in qualified form.)
+ We have ``f :: a > b``, ``g :: a > Int``, and ``x :: b``. Using these, we
+ must somehow fill in the hole (denoted with an underscore) with a value of
+ type ``Int``. What are our options?
.. _recordwildcards:
+ We could try applying ``g`` to ``x``. This won't work though, as ``g``
+ expects an argument of type ``a``, and ``x :: b``. Even worse, we can't turn
+ ``x`` into something of type ``a``, since ``f`` also needs an argument of
+ type ``a``! In short, there's no good way to make this work.
Record wildcards

+ On the other hand, a derived ``Functor`` instances for the ``CovFun``\ s are
+ within the realm of possibility::
.. ghcflag:: XRecordWildCards
+ instance Functor CovFun1 where
+ fmap f (CovFun1 g) = CovFun1 (\x > f (g x))
 :implies: :ghcflag:`XDisambiguateRecordFields`.
+ instance Functor CovFun2 where
+ fmap f (CovFun2 g) = CovFun2 (\h > f (g (\x > h (f x))))
 Allow the use of wildcards in record construction and pattern matching.
+ instance Functor CovFun3 where
+ fmap f (CovFun3 g) = CovFun3 (\h > f (g (\k > h (\x > f (k x)))))
Record wildcards are enabled by the flag :ghcflag:`XRecordWildCards`. This
flag implies :ghcflag:`XDisambiguateRecordFields`.
+There are some other scenarios in which a derived ``Functor`` instance will
+fail to compile:
For records with many fields, it can be tiresome to write out each field
individually in a record pattern, as in ::
+#. A data type has no type parameters (e.g., ``data Nothing = Nothing``).
 data C = C {a :: Int, b :: Int, c :: Int, d :: Int}
 f (C {a = 1, b = b, c = c, d = d}) = b + c + d
+#. A data type's last type variable is used in a :ghcflag:`XDatatypeContexts`
+ constraint (e.g., ``data Ord a => O a = O a``).
Record wildcard syntax permits a "``..``" in a record pattern, where
each elided field ``f`` is replaced by the pattern ``f = f``. For
example, the above pattern can be written as ::
+#. A data type's last type variable is used in an
+ :ghcflag:`XExistentialQuantification` constraint, or is refined in a GADT. For
+ example, ::
+
+ data T a b where
+ T4 :: Ord b => b > T a b
+ T5 :: b > T b b
+ T6 :: T a (b,b)
 f (C {a = 1, ..}) = b + c + d
+ deriving instance Functor (T a)
More details:
+ would not compile successfully due to the way in which ``b`` is constrained.
 Record wildcards in patterns can be mixed with other patterns,
 including puns (:ref:`recordpuns`); for example, in a pattern
 ``(C {a = 1, b, ..})``. Additionally, record wildcards can be used
 wherever record patterns occur, including in ``let`` bindings and at
 the toplevel. For example, the toplevel binding ::
+.. _derivingfoldable:
 C {a = 1, ..} = e
+Deriving ``Foldable`` instances
+
 defines ``b``, ``c``, and ``d``.
+With :ghcflag:`XDeriveFoldable`, one can derive ``Foldable`` instances for data types
+of kind ``* > *``. For example, this declaration::
 Record wildcards can also be used in an expression, when constructing
 a record. For example, ::
+ data Example a = Ex a Char (Example a) (Example Char)
+ deriving Foldable
 let {a = 1; b = 2; c = 3; d = 4} in C {..}
+would generate the following instance::
 in place of ::
+ instance Foldable Example where
+ foldr f z (Ex a1 a2 a3 a4) = f a1 (foldr f z a3)
+ foldMap f (Ex a1 a2 a3 a4) = mappend (f a1) (foldMap f a3)
 let {a = 1; b = 2; c = 3; d = 4} in C {a=a, b=b, c=c, d=d}
+The algorithm for :ghcflag:`XDeriveFoldable` is adapted from the :ghcflag:`XDeriveFunctor`
+algorithm, but it generates definitions for ``foldMap`` and ``foldr`` instead
+of ``fmap``. Here are the differences between the generated code in each
+extension:
 The expansion is purely syntactic, so the record wildcard expression
 refers to the nearest enclosing variables that are spelled the same
 as the omitted field names.
+#. When a bare type variable ``a`` is encountered, :ghcflag:`XDeriveFunctor` would
+ generate ``f a`` for an ``fmap`` definition. :ghcflag:`XDeriveFoldable` would
+ generate ``f a z`` for ``foldr``, and ``f a`` for ``foldMap``.
 Record wildcards may *not* be used in record *updates*. For example
 this is illegal: ::
+#. When a type that is not syntactically equivalent to ``a``, but which does
+ contain ``a``, is encountered, :ghcflag:`XDeriveFunctor` recursively calls
+ ``fmap`` on it. Similarly, :ghcflag:`XDeriveFoldable` would recursively call
+ ``foldr`` and ``foldMap``.
 f r = r { x = 3, .. }
+#. When a type that does not mention ``a`` is encountered, :ghcflag:`XDeriveFunctor`
+ leaves it alone. On the other hand, :ghcflag:`XDeriveFoldable` would generate
+ ``z`` (the state value) for ``foldr`` and ``mempty`` for ``foldMap``.
 For both pattern and expression wildcards, the "``..``" expands to
 the missing *inscope* record fields. Specifically the expansion of
 "``C {..}``" includes ``f`` if and only if:
+#. :ghcflag:`XDeriveFunctor` puts everything back together again at the end by
+ invoking the constructor. :ghcflag:`XDeriveFoldable`, however, builds up a value
+ of some type. For ``foldr``, this is accomplished by chaining applications
+ of ``f`` and recursive ``foldr`` calls on the state value ``z``. For
+ ``foldMap``, this happens by combining all values with ``mappend``.
  ``f`` is a record field of constructor ``C``.
+There are some other differences regarding what data types can have derived
+``Foldable`` instances:
  The record field ``f`` is in scope somehow (either qualified or
 unqualified).
+#. Data types containing function types on the righthand side cannot have
+ derived ``Foldable`` instances.
  In the case of expressions (but not patterns), the variable ``f``
 is in scope unqualified, apart from the binding of the record
 selector itself.
+#. ``Foldable`` instances can be derived for data types in which the last type
+ parameter is existentially constrained or refined in a GADT. For example,
+ this data type::
 These rules restrict record wildcards to the situations in which the
 user could have written the expanded version. For example ::
+ data E a where
+ E1 :: (a ~ Int) => a > E a
+ E2 :: Int > E Int
+ E3 :: (a ~ Int) => a > E Int
+ E4 :: (a ~ Int) => Int > E a
 module M where
 data R = R { a,b,c :: Int }
 module X where
 import M( R(a,c) )
 f b = R { .. }
+ deriving instance Foldable E
 The ``R{..}`` expands to ``R{M.a=a}``, omitting ``b`` since the
 record field is not in scope, and omitting ``c`` since the variable
 ``c`` is not in scope (apart from the binding of the record selector
 ``c``, of course).
+ would have the following generated ``Foldable`` instance::
 Record wildcards cannot be used (a) in a record update construct, and
 (b) for data constructors that are not declared with record fields.
 For example: ::
+ instance Foldable E where
+ foldr f z (E1 e) = f e z
+ foldr f z (E2 e) = z
+ foldr f z (E3 e) = z
+ foldr f z (E4 e) = z
 f x = x { v=True, .. }  Illegal (a)
+ foldMap f (E1 e) = f e
+ foldMap f (E2 e) = mempty
+ foldMap f (E3 e) = mempty
+ foldMap f (E4 e) = mempty
 data T = MkT Int Bool
 g = MkT { .. }  Illegal (b)
 h (MkT { .. }) = True  Illegal (b)
+ Notice how every constructor of ``E`` utilizes some sort of existential
+ quantification, but only the argument of ``E1`` is actually "folded over".
+ This is because we make a deliberate choice to only fold over universally
+ polymorphic types that are syntactically equivalent to the last type
+ parameter. In particular:
.. _deriving:
+  We don't fold over the arguments of ``E1`` or ``E4`` beacause even though
+ ``(a ~ Int)``, ``Int`` is not syntactically equivalent to ``a``.
Extensions to the "deriving" mechanism
======================================
+  We don't fold over the argument of ``E3`` because ``a`` is not universally
+ polymorphic. The ``a`` in ``E3`` is (implicitly) existentially quantified,
+ so it is not the same as the last type parameter of ``E``.
.. _derivinginferred:
+.. _derivingtraversable:
Inferred context for deriving clauses

+Deriving ``Traversable`` instances
+
The Haskell Report is vague about exactly when a ``deriving`` clause is
legal. For example: ::
+With :ghcflag:`XDeriveTraversable`, one can derive ``Traversable`` instances for data
+types of kind ``* > *``. For example, this declaration::
 data T0 f a = MkT0 a deriving( Eq )
 data T1 f a = MkT1 (f a) deriving( Eq )
 data T2 f a = MkT2 (f (f a)) deriving( Eq )
+ data Example a = Ex a Char (Example a) (Example Char)
+ deriving (Functor, Foldable, Traversable)
The natural generated ``Eq`` code would result in these instance
declarations: ::
+would generate the following ``Traversable`` instance::
 instance Eq a => Eq (T0 f a) where ...
 instance Eq (f a) => Eq (T1 f a) where ...
 instance Eq (f (f a)) => Eq (T2 f a) where ...
+ instance Traversable Example where
+ traverse f (Ex a1 a2 a3 a4)
+ = fmap Ex (f a1) <*> traverse f a3
The first of these is obviously fine. The second is still fine, although
less obviously. The third is not Haskell 98, and risks losing
termination of instances.
+The algorithm for :ghcflag:`XDeriveTraversable` is adapted from the
+:ghcflag:`XDeriveFunctor` algorithm, but it generates a definition for ``traverse``
+instead of ``fmap``. Here are the differences between the generated code in
+each extension:
GHC takes a conservative position: it accepts the first two, but not the
third. The rule is this: each constraint in the inferred instance
context must consist only of type variables, with no repetitions.
+#. When a bare type variable ``a`` is encountered, both :ghcflag:`XDeriveFunctor` and
+ :ghcflag:`XDeriveTraversable` would generate ``f a`` for an ``fmap`` and
+ ``traverse`` definition, respectively.
This rule is applied regardless of flags. If you want a more exotic
context, you can write it yourself, using the `standalone deriving
mechanism <#standalonederiving>`__.
+#. When a type that is not syntactically equivalent to ``a``, but which does
+ contain ``a``, is encountered, :ghcflag:`XDeriveFunctor` recursively calls
+ ``fmap`` on it. Similarly, :ghcflag:`XDeriveTraversable` would recursively call
+ ``traverse``.
.. _standalonederiving:
+#. When a type that does not mention ``a`` is encountered, :ghcflag:`XDeriveFunctor`
+ leaves it alone. On the other hand, :ghcflag:`XDeriveTraversable` would call
+ ``pure`` on the value of that type.
Standalone deriving declarations

+#. :ghcflag:`XDeriveFunctor` puts everything back together again at the end by
+ invoking the constructor. :ghcflag:`XDeriveTraversable` does something similar,
+ but it works in an ``Applicative`` context by chaining everything together
+ with ``(<*>)``.
.. ghcflag:: XStandaloneDeriving
+Unlike :ghcflag:`XDeriveFunctor`, :ghcflag:`XDeriveTraversable` cannot be used on data
+types containing a function type on the righthand side.
 Allow the use of standalone ``deriving`` declarations.
+For a full specification of the algorithms used in :ghcflag:`XDeriveFunctor`,
+:ghcflag:`XDeriveFoldable`, and :ghcflag:`XDeriveTraversable`, see
+:ghcwiki:`this wiki page `.
GHC allows standalone ``deriving`` declarations, enabled by
:ghcflag:`XStandaloneDeriving`: ::
+.. _derivingtypeable:
 data Foo a = Bar a  Baz String
+Deriving ``Typeable`` instances
+
 deriving instance Eq a => Eq (Foo a)
+.. ghcflag:: XDeriveDataTypeable
The syntax is identical to that of an ordinary instance declaration
apart from (a) the keyword ``deriving``, and (b) the absence of the
``where`` part.
+ Enable automatic deriving of instances for the ``Typeable`` typeclass
However, standalone deriving differs from a ``deriving`` clause in a
number of important ways:
+The class ``Typeable`` is very special:
 The standalone deriving declaration does not need to be in the same
 module as the data type declaration. (But be aware of the dangers of
 orphan instances (:ref:`orphanmodules`).
+ ``Typeable`` is kindpolymorphic (see :ref:`kindpolymorphism`).
 You must supply an explicit context (in the example the context is
 ``(Eq a)``), exactly as you would in an ordinary instance
 declaration. (In contrast, in a ``deriving`` clause attached to a
 data type declaration, the context is inferred.)
+ GHC has a custom solver for discharging constraints that involve
+ class ``Typeable``, and handwritten instances are forbidden. This
+ ensures that the programmer cannot subvert the type system by writing
+ bogus instances.
 Unlike a ``deriving`` declaration attached to a ``data`` declaration,
 the instance can be more specific than the data type (assuming you
 also use :ghcflag:`XFlexibleInstances`, :ref:`instancerules`). Consider
 for example ::
+ Derived instances of ``Typeable`` are ignored, and may be reported as
+ an error in a later version of the compiler.
 data Foo a = Bar a  Baz String
+ The rules for solving \`Typeable\` constraints are as follows:
 deriving instance Eq a => Eq (Foo [a])
 deriving instance Eq a => Eq (Foo (Maybe a))
+  A concrete type constructor applied to some types. ::
 This will generate a derived instance for ``(Foo [a])`` and
 ``(Foo (Maybe a))``, but other types such as ``(Foo (Int,Bool))``
 will not be an instance of ``Eq``.
+ instance (Typeable t1, .., Typeable t_n) =>
+ Typeable (T t1 .. t_n)
 Unlike a ``deriving`` declaration attached to a ``data`` declaration,
 GHC does not restrict the form of the data type. Instead, GHC simply
 generates the appropriate boilerplate code for the specified class,
 and typechecks it. If there is a type error, it is your problem. (GHC
 will show you the offending code if it has a type error.)
+ This rule works for any concrete type constructor, including type
+ constructors with polymorphic kinds. The only restriction is that
+ if the type constructor has a polymorphic kind, then it has to be
+ applied to all of its kinds parameters, and these kinds need to be
+ concrete (i.e., they cannot mention kind variables).
 The merit of this is that you can derive instances for GADTs and
 other exotic data types, providing only that the boilerplate code
 does indeed typecheck. For example: ::
+  ::
 data T a where
 T1 :: T Int
 T2 :: T Bool
+ A type variable applied to some types.
+ instance (Typeable f, Typeable t1, .., Typeable t_n) =>
+ Typeable (f t1 .. t_n)
 deriving instance Show (T a)
+  ::
 In this example, you cannot say ``... deriving( Show )`` on the data
 type declaration for ``T``, because ``T`` is a GADT, but you *can*
 generate the instance declaration using standalone deriving.
+ A concrete type literal.
+ instance Typeable 0  Type natural literals
+ instance Typeable "Hello"  Typelevel symbols
 The downside is that, if the boilerplate code fails to typecheck,
 you will get an error message about that code, which you did not
 write. Whereas, with a ``deriving`` clause the sideconditions are
 necessarily more conservative, but any error message may be more
 comprehensible.
+.. _derivinglift:
+
+Deriving ``Lift`` instances
+
In other ways, however, a standalone deriving obeys the same rules as
ordinary deriving:
+.. ghcflag:: XDeriveLift
 A ``deriving instance`` declaration must obey the same rules
 concerning form and termination as ordinary instance declarations,
 controlled by the same flags; see :ref:`instancedecls`.
+ :since: 8.0.1
 The standalone syntax is generalised for newtypes in exactly the
 same way that ordinary ``deriving`` clauses are generalised
 (:ref:`newtypederiving`). For example: ::
+ Enable automatic deriving of instances for the ``Lift`` typeclass for
+ Template Haskell.
 newtype Foo a = MkFoo (State Int a)
+The class ``Lift``, unlike other derivable classes, lives in
+``templatehaskell`` instead of ``base``. Having a data type be an instance of
+``Lift`` permits its values to be promoted to Template Haskell expressions (of
+type ``ExpQ``), which can then be spliced into Haskell source code.
 deriving instance MonadState Int Foo
+Here is an example of how one can derive ``Lift``:
 GHC always treats the *last* parameter of the instance (``Foo`` in
 this example) as the type whose instance is being derived.
+::
.. _derivingextra:
+ {# LANGUAGE DeriveLift #}
+ module Bar where
Deriving instances of extra classes (``Data``, etc.)

+ import Language.Haskell.TH.Syntax
.. ghcflag:: XDeriveGeneric
+ data Foo a = Foo a  a :^: a deriving Lift
 Allow automatic deriving of instances for the ``Generic`` typeclass.
+ {
+ instance (Lift a) => Lift (Foo a) where
+ lift (Foo a)
+ = appE
+ (conE
+ (mkNameG_d "packagename" "Bar" "Foo"))
+ (lift a)
+ lift (u :^: v)
+ = infixApp
+ (lift u)
+ (conE
+ (mkNameG_d "packagename" "Bar" ":^:"))
+ (lift v)
+ }
.. ghcflag:: XDeriveFunctor
+ 
+ {# LANGUAGE TemplateHaskell #}
+ module Baz where
 Allow automatic deriving of instances for the ``Functor`` typeclass.
+ import Bar
+ import Language.Haskell.TH.Lift
.. ghcflag:: XDeriveFoldable
+ foo :: Foo String
+ foo = $(lift $ Foo "foo")
 Allow automatic deriving of instances for the ``Foldable`` typeclass.
+ fooExp :: Lift a => Foo a > Q Exp
+ fooExp f = [ f ]
.. ghcflag:: XDeriveTraversable
+:ghcflag:`XDeriveLift` also works for certain unboxed types (``Addr#``, ``Char#``,
+``Double#``, ``Float#``, ``Int#``, and ``Word#``):
 :implies: :ghcflag:`XDeriveFoldable`, :ghcflag:`XDeriveFunctor`
+::
 Allow automatic deriving of instances for the ``Traversable`` typeclass.
+ {# LANGUAGE DeriveLift, MagicHash #}
+ module Unboxed where
Haskell 98 allows the programmer to add "``deriving( Eq, Ord )``" to a
data type declaration, to generate a standard instance declaration for
classes specified in the ``deriving`` clause. In Haskell 98, the only
classes that may appear in the ``deriving`` clause are the standard
classes ``Eq``, ``Ord``, ``Enum``, ``Ix``, ``Bounded``, ``Read``, and
``Show``.
+ import GHC.Exts
+ import Language.Haskell.TH.Syntax
GHC extends this list with several more classes that may be
automatically derived:
+ data IntHash = IntHash Int# deriving Lift
 With :ghcflag:`XDeriveGeneric`, you can derive instances of the classes
 ``Generic`` and ``Generic1``, defined in ``GHC.Generics``. You can
 use these to define generic functions, as described in
 :ref:`genericprogramming`.
+ {
+ instance Lift IntHash where
+ lift (IntHash i)
+ = appE
+ (conE
+ (mkNameG_d "packagename" "Unboxed" "IntHash"))
+ (litE
+ (intPrimL (toInteger (I# i))))
+ }
 With :ghcflag:`XDeriveFunctor`, you can derive instances of the class
 ``Functor``, defined in ``GHC.Base``. See :ref:`derivingfunctor`.
 With :ghcflag:`XDeriveDataTypeable`, you can derive instances of the class
 ``Data``, defined in ``Data.Data``. See :ref:`derivingtypeable` for
 deriving ``Typeable``.
+.. _newtypederiving:
 With :ghcflag:`XDeriveFoldable`, you can derive instances of the class
 ``Foldable``, defined in ``Data.Foldable``. See
 :ref:`derivingfoldable`.
+Generalised derived instances for newtypes
+
 With :ghcflag:`XDeriveTraversable`, you can derive instances of the class
 ``Traversable``, defined in ``Data.Traversable``. Since the
 ``Traversable`` instance dictates the instances of ``Functor`` and
 ``Foldable``, you'll probably want to derive them too, so
 :ghcflag:`XDeriveTraversable` implies :ghcflag:`XDeriveFunctor` and
 :ghcflag:`XDeriveFoldable`. See :ref:`derivingtraversable`.
+.. ghcflag:: XGeneralisedNewtypeDeriving
+ XGeneralizedNewtypeDeriving
 With :ghcflag:`XDeriveLift`, you can derive instances of the class ``Lift``,
 defined in the ``Language.Haskell.TH.Syntax`` module of the
 ``templatehaskell`` package. See :ref:`derivinglift`.
+ Enable GHC's cunning generalised deriving mechanism for ``newtype``\s
You can also use a standalone deriving declaration instead (see
:ref:`standalonederiving`).
+When you define an abstract type using ``newtype``, you may want the new
+type to inherit some instances from its representation. In Haskell 98,
+you can inherit instances of ``Eq``, ``Ord``, ``Enum`` and ``Bounded``
+by deriving them, but for any other classes you have to write an
+explicit instance declaration. For example, if you define ::
In each case the appropriate class must be in scope before it can be
mentioned in the ``deriving`` clause.
+ newtype Dollars = Dollars Int
.. _derivingfunctor:
+and you want to use arithmetic on ``Dollars``, you have to explicitly
+define an instance of ``Num``: ::
Deriving ``Functor`` instances

+ instance Num Dollars where
+ Dollars a + Dollars b = Dollars (a+b)
+ ...
With :ghcflag:`XDeriveFunctor`, one can derive ``Functor`` instances for data types
of kind ``* > *``. For example, this declaration::
+All the instance does is apply and remove the ``newtype`` constructor.
+It is particularly galling that, since the constructor doesn't appear at
+runtime, this instance declaration defines a dictionary which is
+*wholly equivalent* to the ``Int`` dictionary, only slower!
 data Example a = Ex a Char (Example a) (Example Char)
 deriving Functor
+.. _generalizednewtypederiving:
would generate the following instance: ::
+Generalising the deriving clause
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 instance Functor Example where
 fmap f (Ex a1 a2 a3 a4) = Ex (f a1) a2 (fmap f a3) a4
+GHC now permits such instances to be derived instead, using the flag
+:ghcflag:`XGeneralizedNewtypeDeriving`, so one can write ::
The basic algorithm for :ghcflag:`XDeriveFunctor` walks the arguments of each
constructor of a data type, applying a mapping function depending on the type
of each argument. If a plain type variable is found that is syntactically
equivalent to the last type parameter of the data type (``a`` in the above
example), then we apply the function ``f`` directly to it. If a type is
encountered that is not syntactically equivalent to the last type parameter
*but does mention* the last type parameter somewhere in it, then a recursive
call to ``fmap`` is made. If a type is found which doesn't mention the last
type paramter at all, then it is left alone.
+ newtype Dollars = Dollars Int deriving (Eq,Show,Num)
The second of those cases, in which a type is unequal to the type parameter but
does contain the type parameter, can be surprisingly tricky. For example, the
following example compiles::
+and the implementation uses the *same* ``Num`` dictionary for
+``Dollars`` as for ``Int``. Notionally, the compiler derives an instance
+declaration of the form ::
 newtype Right a = Right (Either Int a) deriving Functor
+ instance Num Int => Num Dollars
Modifying the code slightly, however, produces code which will not compile::
+which just adds or removes the ``newtype`` constructor according to the
+type.
 newtype Wrong a = Wrong (Either a Int) deriving Functor
+We can also derive instances of constructor classes in a similar way.
+For example, suppose we have implemented state and failure monad
+transformers, such that ::
The difference involves the placement of the last type parameter, ``a``. In the
``Right`` case, ``a`` occurs within the type ``Either Int a``, and moreover, it
appears as the last type argument of ``Either``. In the ``Wrong`` case,
however, ``a`` is not the last type argument to ``Either``; rather, ``Int`` is.
+ instance Monad m => Monad (State s m)
+ instance Monad m => Monad (Failure m)
This distinction is important because of the way :ghcflag:`XDeriveFunctor` works. The
derived ``Functor Right`` instance would be::
+In Haskell 98, we can define a parsing monad by ::
 instance Functor Right where
 fmap f (Right a) = Right (fmap f a)
+ type Parser tok m a = State [tok] (Failure m) a
Given a value of type ``Right a``, GHC must produce a value of type
``Right b``. Since the argument to the ``Right`` constructor has type
``Either Int a``, the code recursively calls ``fmap`` on it to produce a value
of type ``Either Int b``, which is used in turn to construct a final value of
type ``Right b``.
+which is automatically a monad thanks to the instance declarations
+above. With the extension, we can make the parser type abstract, without
+needing to write an instance of class ``Monad``, via ::
The generated code for the ``Functor Wrong`` instance would look exactly the
same, except with ``Wrong`` replacing every occurrence of ``Right``. The
problem is now that ``fmap`` is being applied recursively to a value of type
``Either a Int``. This cannot possibly produce a value of type
``Either b Int``, as ``fmap`` can only change the last type parameter! This
causes the generated code to be illtyped.
+ newtype Parser tok m a = Parser (State [tok] (Failure m) a)
+ deriving Monad
As a general rule, if a data type has a derived ``Functor`` instance and its
last type parameter occurs on the righthand side of the data declaration, then
either it must (1) occur bare (e.g., ``newtype Id a = a``), or (2) occur as the
last argument of a type constructor (as in ``Right`` above).
+In this case the derived instance declaration is of the form ::
There are two exceptions to this rule:
+ instance Monad (State [tok] (Failure m)) => Monad (Parser tok m)
#. Tuple types. When a nonunit tuple is used on the righthand side of a data
 declaration, :ghcflag:`XDeriveFunctor` treats it as a product of distinct types.
 In other words, the following code::
+Notice that, since ``Monad`` is a constructor class, the instance is a
+*partial application* of the new type, not the entire left hand side. We
+can imagine that the type declaration is "etaconverted" to generate the
+context of the instance declaration.
 newtype Triple a = Triple (a, Int, [a]) deriving Functor
+We can even derive instances of multiparameter classes, provided the
+newtype is the last class parameter. In this case, a "partial
+application" of the class appears in the ``deriving`` clause. For
+example, given the class ::
 Would result in a generated ``Functor`` instance like so::
+ class StateMonad s m  m > s where ...
+ instance Monad m => StateMonad s (State s m) where ...
 instance Functor Triple where
 fmap f (Triple a) =
 Triple (case a of
 (a1, a2, a3) > (f a1, a2, fmap f a3))
+then we can derive an instance of ``StateMonad`` for ``Parser`` by ::
 That is, :ghcflag:`XDeriveFunctor` patternmatches its way into tuples and maps
 over each type that constitutes the tuple. The generated code is
 reminiscient of what would be generated from
 ``data Triple a = Triple a Int [a]``, except with extra machinery to handle
 the tuple.
+ newtype Parser tok m a = Parser (State [tok] (Failure m) a)
+ deriving (Monad, StateMonad [tok])
#. Function types. The last type parameter can appear anywhere in a function
 type as long as it occurs in a *covariant* position. To illustrate what this
 means, consider the following three examples::
+The derived instance is obtained by completing the application of the
+class to the new type: ::
 newtype CovFun1 a = CovFun1 (Int > a) deriving Functor
 newtype CovFun2 a = CovFun2 ((a > Int) > a) deriving Functor
 newtype CovFun3 a = CovFun3 (((Int > a) > Int) > a) deriving Functor
+ instance StateMonad [tok] (State [tok] (Failure m)) =>
+ StateMonad [tok] (Parser tok m)
 All three of these examples would compile without issue. On the other hand::
+As a result of this extension, all derived instances in newtype
+declarations are treated uniformly (and implemented just by reusing the
+dictionary for the representation type), *except* ``Show`` and ``Read``,
+which really behave differently for the newtype and its representation.
 newtype ContraFun1 a = ContraFun1 (a > Int) deriving Functor
 newtype ContraFun2 a = ContraFun2 ((Int > a) > Int) deriving Functor
 newtype ContraFun3 a = ContraFun3 (((a > Int) > a) > Int) deriving Functor
+A more precise specification
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+A derived instance is derived only for declarations of these forms
+(after expansion of any type synonyms) ::
 While these examples look similar, none of them would successfully compile.
 This is because all occurrences of the last type parameter ``a`` occur in *contravariant* positions, not covariant ones.
+ newtype T v1..vn = MkT (t vk+1..vn) deriving (C t1..tj)
+ newtype instance T s1..sk vk+1..vn = MkT (t vk+1..vn) deriving (C t1..tj)
 Intuitively, a covariant type is *produced*, and a contravariant type is
 *consumed*. Most types in Haskell are covariant, but the function type is
 special in that the lefthand side of a function arrow reverses variance. If
 a function type ``a > b`` appears in a covariant position (e.g.,
 ``CovFun1`` above), then ``a`` is in a contravariant position and ``b`` is
 in a covariant position. Similarly, if ``a > b`` appears in a contravariant
 position (e.g., ``CovFun2`` above), then ``a`` is in ``a`` covariant
 position and ``b`` is in a contravariant position.
+where
 To see why a data type with a contravariant occurrence of its last type
 parameter cannot have a derived ``Functor`` instance, let's suppose that a
 ``Functor ContraFun1`` instance exists. The implementation would look
 something like this::
+ ``v1..vn`` are type variables, and ``t``, ``s1..sk``, ``t1..tj`` are
+ types.
 instance Functor ContraFun1 where
 fmap f (ContraFun g) = ContraFun (\x > _)
+ The ``(C t1..tj)`` is a partial applications of the class ``C``,
+ where the arity of ``C`` is exactly ``j+1``. That is, ``C`` lacks
+ exactly one type argument.
 We have ``f :: a > b``, ``g :: a > Int``, and ``x :: b``. Using these, we
 must somehow fill in the hole (denoted with an underscore) with a value of
 type ``Int``. What are our options?
+ ``k`` is chosen so that ``C t1..tj (T v1...vk)`` is wellkinded. (Or,
+ in the case of a ``data instance``, so that ``C t1..tj (T s1..sk)``
+ is well kinded.)
 We could try applying ``g`` to ``x``. This won't work though, as ``g``
 expects an argument of type ``a``, and ``x :: b``. Even worse, we can't turn
 ``x`` into something of type ``a``, since ``f`` also needs an argument of
 type ``a``! In short, there's no good way to make this work.
+ The type ``t`` is an arbitrary type.
 On the other hand, a derived ``Functor`` instances for the ``CovFun``\ s are
 within the realm of possibility::
+ The type variables ``vk+1...vn`` do not occur in the types ``t``,
+ ``s1..sk``, or ``t1..tj``.
 instance Functor CovFun1 where
 fmap f (CovFun1 g) = CovFun1 (\x > f (g x))
+ ``C`` is not ``Read``, ``Show``, ``Typeable``, or ``Data``. These
+ classes should not "look through" the type or its constructor. You
+ can still derive these classes for a newtype, but it happens in the
+ usual way, not via this new mechanism.
 instance Functor CovFun2 where
 fmap f (CovFun2 g) = CovFun2 (\h > f (g (\x > h (f x))))
+ It is safe to coerce each of the methods of ``C``. That is, the
+ missing last argument to ``C`` is not used at a nominal role in any
+ of the ``C``'s methods. (See :ref:`roles`.)
 instance Functor CovFun3 where
 fmap f (CovFun3 g) = CovFun3 (\h > f (g (\k > h (\x > f (k x)))))
+Then the derived instance declaration is of the form ::
There are some other scenarios in which a derived ``Functor`` instance will
fail to compile:
+ instance C t1..tj t => C t1..tj (T v1...vk)
#. A data type has no type parameters (e.g., ``data Nothing = Nothing``).
+As an example which does *not* work, consider ::
#. A data type's last type variable is used in a :ghcflag:`XDatatypeContexts`
 constraint (e.g., ``data Ord a => O a = O a``).
+ newtype NonMonad m s = NonMonad (State s m s) deriving Monad
#. A data type's last type variable is used in an
 :ghcflag:`XExistentialQuantification` constraint, or is refined in a GADT. For
 example, ::
+Here we cannot derive the instance ::
 data T a b where
 T4 :: Ord b => b > T a b
 T5 :: b > T b b
 T6 :: T a (b,b)
+ instance Monad (State s m) => Monad (NonMonad m)
 deriving instance Functor (T a)
+because the type variable ``s`` occurs in ``State s m``, and so cannot
+be "etaconverted" away. It is a good thing that this ``deriving``
+clause is rejected, because ``NonMonad m`` is not, in fact, a monad 
+for the same reason. Try defining ``>>=`` with the correct type: you
+won't be able to.
 would not compile successfully due to the way in which ``b`` is constrained.
+Notice also that the *order* of class parameters becomes important,
+since we can only derive instances for the last one. If the
+``StateMonad`` class above were instead defined as ::
.. _derivingfoldable:
+ class StateMonad m s  m > s where ...
Deriving ``Foldable`` instances

+then we would not have been able to derive an instance for the
+``Parser`` type above. We hypothesise that multiparameter classes
+usually have one "main" parameter for which deriving new instances is
+most interesting.
With :ghcflag:`XDeriveFoldable`, one can derive ``Foldable`` instances for data types
of kind ``* > *``. For example, this declaration::
+Lastly, all of this applies only for classes other than ``Read``,
+``Show``, ``Typeable``, and ``Data``, for which the builtin derivation
+applies (section 4.3.3. of the Haskell Report). (For the standard
+classes ``Eq``, ``Ord``, ``Ix``, and ``Bounded`` it is immaterial
+whether the standard method is used or the one described here.)
 data Example a = Ex a Char (Example a) (Example Char)
 deriving Foldable
+.. _deriveanyclass:
would generate the following instance::
+Deriving any other class
+
 instance Foldable Example where
 foldr f z (Ex a1 a2 a3 a4) = f a1 (foldr f z a3)
 foldMap f (Ex a1 a2 a3 a4) = mappend (f a1) (foldMap f a3)
+.. ghcflag:: XDeriveAnyClass
The algorithm for :ghcflag:`XDeriveFoldable` is adapted from the :ghcflag:`XDeriveFunctor`
algorithm, but it generates definitions for ``foldMap`` and ``foldr`` instead
of ``fmap``. Here are the differences between the generated code in each
extension:
+ :since: 7.10.1
#. When a bare type variable ``a`` is encountered, :ghcflag:`XDeriveFunctor` would
 generate ``f a`` for an ``fmap`` definition. :ghcflag:`XDeriveFoldable` would
 generate ``f a z`` for ``foldr``, and ``f a`` for ``foldMap``.
+ Allow use of any typeclass in ``deriving`` clauses.
#. When a type that is not syntactically equivalent to ``a``, but which does
 contain ``a``, is encountered, :ghcflag:`XDeriveFunctor` recursively calls
 ``fmap`` on it. Similarly, :ghcflag:`XDeriveFoldable` would recursively call
 ``foldr`` and ``foldMap``.
+With :ghcflag:`XDeriveAnyClass` you can derive any other class. The compiler
+will simply generate an instance declaration with no explicitlydefined
+methods.
+This is
+mostly useful in classes whose `minimal set <#minimalpragma>`__ is
+empty, and especially when writing
+`generic functions <#genericprogramming>`__.
#. When a type that does not mention ``a`` is encountered, :ghcflag:`XDeriveFunctor`
 leaves it alone. On the other hand, :ghcflag:`XDeriveFoldable` would generate
 ``z`` (the state value) for ``foldr`` and ``mempty`` for ``foldMap``.
+As an example, consider a simple prettyprinter class ``SPretty``, which outputs
+pretty strings: ::
#. :ghcflag:`XDeriveFunctor` puts everything back together again at the end by
 invoking the constructor. :ghcflag:`XDeriveFoldable`, however, builds up a value
 of some type. For ``foldr``, this is accomplished by chaining applications
 of ``f`` and recursive ``foldr`` calls on the state value ``z``. For
 ``foldMap``, this happens by combining all values with ``mappend``.
+ {# LANGUAGE DefaultSignatures, DeriveAnyClass #}
There are some other differences regarding what data types can have derived
``Foldable`` instances:
+ class SPretty a where
+ sPpr :: a > String
+ default sPpr :: Show a => a > String
+ sPpr = show
#. Data types containing function types on the righthand side cannot have
 derived ``Foldable`` instances.
+If a user does not provide a manual implementation for ``sPpr``, then it will
+default to ``show``. Now we can leverage the :ghcflag:`XDeriveAnyClass` extension to
+easily implement a ``SPretty`` instance for a new data type: ::
#. ``Foldable`` instances can be derived for data types in which the last type
 parameter is existentially constrained or refined in a GADT. For example,
 this data type::
+ data Foo = Foo deriving (Show, SPretty)
 data E a where
 E1 :: (a ~ Int) => a > E a
 E2 :: Int > E Int
 E3 :: (a ~ Int) => a > E Int
 E4 :: (a ~ Int) => Int > E a
+The above code is equivalent to: ::
 deriving instance Foldable E
+ data Foo = Foo deriving Show
+ instance SPretty Foo
 would have the following generated ``Foldable`` instance::
+That is, an ``SPretty Foo`` instance will be created with empty implementations
+for all methods. Since we are using :ghcflag:`XDefaultSignatures` in this example, a
+default implementation of ``sPpr`` is filled in automatically.
 instance Foldable E where
 foldr f z (E1 e) = f e z
 foldr f z (E2 e) = z
 foldr f z (E3 e) = z
 foldr f z (E4 e) = z
+Note the following details
 foldMap f (E1 e) = f e
 foldMap f (E2 e) = mempty
 foldMap f (E3 e) = mempty
 foldMap f (E4 e) = mempty
+ In case you try to derive some
+ class on a newtype, and :ghcflag:`XGeneralizedNewtypeDeriving` is also on,
+ :ghcflag:`XDeriveAnyClass` takes precedence.
 Notice how every constructor of ``E`` utilizes some sort of existential
 quantification, but only the argument of ``E1`` is actually "folded over".
 This is because we make a deliberate choice to only fold over universally
 polymorphic types that are syntactically equivalent to the last type
 parameter. In particular:
+ :ghcflag:`XDeriveAnyClass` is allowed only when the last argument of the class
+ has kind ``*`` or ``(* > *)``. So this is not allowed: ::
  We don't fold over the arguments of ``E1`` or ``E4`` beacause even though
 ``(a ~ Int)``, ``Int`` is not syntactically equivalent to ``a``.
+ data T a b = MkT a b deriving( Bifunctor )
  We don't fold over the argument of ``E3`` because ``a`` is not universally
 polymorphic. The ``a`` in ``E3`` is (implicitly) existentially quantified,
 so it is not the same as the last type parameter of ``E``.
+ because the last argument of ``Bifunctor :: (* > * > *) > Constraint``
+ has the wrong kind.
.. _derivingtraversable:
+ The instance context will be generated according to the same rules
+ used when deriving ``Eq`` (if the kind of the type is ``*``), or
+ the rules for ``Functor`` (if the kind of the type is ``(* > *)``).
+ For example ::
Deriving ``Traversable`` instances

+ instance C a => C (a,b) where ...
With :ghcflag:`XDeriveTraversable`, one can derive ``Traversable`` instances for data
types of kind ``* > *``. For example, this declaration::
+ data T a b = MkT a (a,b) deriving( C )
 data Example a = Ex a Char (Example a) (Example Char)
 deriving (Functor, Foldable, Traversable)
+ The ``deriving`` clause will generate ::
would generate the following ``Traversable`` instance::
+ instance C a => C (T a b) where {}
 instance Traversable Example where
 traverse f (Ex a1 a2 a3 a4)
 = fmap Ex (f a1) <*> traverse f a3
+ The constraints `C a` and `C (a,b)` are generated from the data
+ constructor arguments, but the latter simplifies to `C a`.
The algorithm for :ghcflag:`XDeriveTraversable` is adapted from the
:ghcflag:`XDeriveFunctor` algorithm, but it generates a definition for ``traverse``
instead of ``fmap``. Here are the differences between the generated code in
each extension:
+ :ghcflag:`XDeriveAnyClass` can be used with partially applied classes,
+ such as ::
#. When a bare type variable ``a`` is encountered, both :ghcflag:`XDeriveFunctor` and
 :ghcflag:`XDeriveTraversable` would generate ``f a`` for an ``fmap`` and
 ``traverse`` definition, respectively.
+ data T a = MKT a deriving( D Int )
#. When a type that is not syntactically equivalent to ``a``, but which does
 contain ``a``, is encountered, :ghcflag:`XDeriveFunctor` recursively calls
 ``fmap`` on it. Similarly, :ghcflag:`XDeriveTraversable` would recursively call
 ``traverse``.
+ which generates ::
#. When a type that does not mention ``a`` is encountered, :ghcflag:`XDeriveFunctor`
 leaves it alone. On the other hand, :ghcflag:`XDeriveTraversable` would call
 ``pure`` on the value of that type.
+ instance D Int a => D Int (T a) where {}
#. :ghcflag:`XDeriveFunctor` puts everything back together again at the end by
 invoking the constructor. :ghcflag:`XDeriveTraversable` does something similar,
 but it works in an ``Applicative`` context by chaining everything together
 with ``(<*>)``.
+ :ghcflag:`XDeriveAnyClass` can be used to fill in default instances for
+ associated type families: ::
Unlike :ghcflag:`XDeriveFunctor`, :ghcflag:`XDeriveTraversable` cannot be used on data
types containing a function type on the righthand side.
+ {# LANGUAGE DeriveAnyClass, TypeFamilies #}
For a full specification of the algorithms used in :ghcflag:`XDeriveFunctor`,
:ghcflag:`XDeriveFoldable`, and :ghcflag:`XDeriveTraversable`, see
:ghcwiki:`this wiki page `.
+ class Sizable a where
+ type Size a
+ type Size a = Int
.. _derivingtypeable:
+ data Bar = Bar deriving Sizable
Deriving ``Typeable`` instances

+ doubleBarSize :: Size Bar > Size Bar
+ doubleBarSize s = 2*s
.. ghcflag:: XDeriveDataTypeable
+ The ``deriving( Sizable )`` is equivalent to saying ::
 Enable automatic deriving of instances for the ``Typeable`` typeclass
+ instance Sizeable Bar where {}
The class ``Typeable`` is very special:
+ and then the normal rules for filling in associated types from the
+ default will apply, making ``Size Bar`` equal to ``Int``.
 ``Typeable`` is kindpolymorphic (see :ref:`kindpolymorphism`).
+.. _patternsynonyms:
 GHC has a custom solver for discharging constraints that involve
 class ``Typeable``, and handwritten instances are forbidden. This
 ensures that the programmer cannot subvert the type system by writing
 bogus instances.
+Pattern synonyms
+================
 Derived instances of ``Typeable`` are ignored, and may be reported as
 an error in a later version of the compiler.
+.. ghcflag:: XPatternSynonyms
 The rules for solving \`Typeable\` constraints are as follows:
+ :since: 7.8.1
  A concrete type constructor applied to some types. ::
+ Allow the definition of pattern synonyms.
 instance (Typeable t1, .., Typeable t_n) =>
 Typeable (T t1 .. t_n)
+Pattern synonyms are enabled by the flag :ghcflag:`XPatternSynonyms`, which is
+required for defining them, but *not* for using them. More information
+and examples of view patterns can be found on the
+`Wiki page `.
 This rule works for any concrete type constructor, including type
 constructors with polymorphic kinds. The only restriction is that
 if the type constructor has a polymorphic kind, then it has to be
 applied to all of its kinds parameters, and these kinds need to be
 concrete (i.e., they cannot mention kind variables).
+Pattern synonyms enable giving names to parametrized pattern schemes.
+They can also be thought of as abstract constructors that don't have a
+bearing on data representation. For example, in a programming language
+implementation, we might represent types of the language as follows: ::
  ::
+ data Type = App String [Type]
 A type variable applied to some types.
 instance (Typeable f, Typeable t1, .., Typeable t_n) =>
 Typeable (f t1 .. t_n)
+Here are some examples of using said representation. Consider a few
+types of the ``Type`` universe encoded like this: ::
  ::
+ App ">" [t1, t2]  t1 > t2
+ App "Int" []  Int
+ App "Maybe" [App "Int" []]  Maybe Int
 A concrete type literal.
 instance Typeable 0  Type natural literals
 instance Typeable "Hello"  Typelevel symbols
+This representation is very generic in that no types are given special
+treatment. However, some functions might need to handle some known types
+specially, for example the following two functions collect all argument
+types of (nested) arrow types, and recognize the ``Int`` type,
+respectively: ::
.. _derivinglift:
+ collectArgs :: Type > [Type]
+ collectArgs (App ">" [t1, t2]) = t1 : collectArgs t2
+ collectArgs _ = []
Deriving ``Lift`` instances

+ isInt :: Type > Bool
+ isInt (App "Int" []) = True
+ isInt _ = False
.. ghcflag:: XDeriveLift
+Matching on ``App`` directly is both hard to read and error prone to
+write. And the situation is even worse when the matching is nested: ::
 :since: 8.0.1
+ isIntEndo :: Type > Bool
+ isIntEndo (App ">" [App "Int" [], App "Int" []]) = True
+ isIntEndo _ = False
 Enable automatic deriving of instances for the ``Lift`` typeclass for
 Template Haskell.
+Pattern synonyms permit abstracting from the representation to expose
+matchers that behave in a constructorlike manner with respect to
+pattern matching. We can create pattern synonyms for the known types we
+care about, without committing the representation to them (note that
+these don't have to be defined in the same module as the ``Type`` type): ::
The class ``Lift``, unlike other derivable classes, lives in
``templatehaskell`` instead of ``base``. Having a data type be an instance of
``Lift`` permits its values to be promoted to Template Haskell expressions (of
type ``ExpQ``), which can then be spliced into Haskell source code.
+ pattern Arrow t1 t2 = App ">" [t1, t2]
+ pattern Int = App "Int" []
+ pattern Maybe t = App "Maybe" [t]
Here is an example of how one can derive ``Lift``:
+Which enables us to rewrite our functions in a much cleaner style: ::
::
+ collectArgs :: Type > [Type]
+ collectArgs (Arrow t1 t2) = t1 : collectArgs t2
+ collectArgs _ = []
 {# LANGUAGE DeriveLift #}
 module Bar where
+ isInt :: Type > Bool
+ isInt Int = True
+ isInt _ = False
 import Language.Haskell.TH.Syntax
+ isIntEndo :: Type > Bool
+ isIntEndo (Arrow Int Int) = True
+ isIntEndo _ = False
 data Foo a = Foo a  a :^: a deriving Lift
+In general there are three kinds of pattern synonyms. Unidirectional,
+bidirectional and explicitly bidirectional. The examples given so far are
+examples of bidirectional pattern synonyms. A bidirectional synonym
+behaves the same as an ordinary data constructor. We can use it in a pattern
+context to deconstruct values and in an expression context to construct values.
+For example, we can construct the value `intEndo` using the pattern synonyms
+`Arrow` and `Int` as defined previously. ::
 {
 instance (Lift a) => Lift (Foo a) where
 lift (Foo a)
 = appE
 (conE
 (mkNameG_d "packagename" "Bar" "Foo"))
 (lift a)
 lift (u :^: v)
 = infixApp
 (lift u)
 (conE
 (mkNameG_d "packagename" "Bar" ":^:"))
 (lift v)
 }
+ intEndo :: Type
+ intEndo = Arrow Int Int
 
 {# LANGUAGE TemplateHaskell #}
 module Baz where
+This example is equivalent to the much more complicated construction if we had
+directly used the `Type` constructors. ::
 import Bar
 import Language.Haskell.TH.Lift
+ intEndo :: Type
+ intEndo = App ">" [App "Int" [], App "Int" []]
 foo :: Foo String
 foo = $(lift $ Foo "foo")
 fooExp :: Lift a => Foo a > Q Exp
 fooExp f = [ f ]
+Unidirectional synonyms can only be used in a pattern context and are
+defined as follows:
:ghcflag:`XDeriveLift` also works for certain unboxed types (``Addr#``, ``Char#``,
``Double#``, ``Float#``, ``Int#``, and ``Word#``):
::
 {# LANGUAGE DeriveLift, MagicHash #}
 module Unboxed where
+ pattern Head x < x:xs
 import GHC.Exts
 import Language.Haskell.TH.Syntax
+In this case, ``Head`` ⟨x⟩ cannot be used in expressions, only patterns,
+since it wouldn't specify a value for the ⟨xs⟩ on the righthand side. However,
+we can define an explicitly bidirectional pattern synonym by separately
+specifying how to construct and deconstruct a type. The syntax for
+doing this is as follows:
 data IntHash = IntHash Int# deriving Lift
+::
 {
 instance Lift IntHash where
 lift (IntHash i)
 = appE
 (conE
 (mkNameG_d "packagename" "Unboxed" "IntHash"))
 (litE
 (intPrimL (toInteger (I# i))))
 }
+ pattern HeadC x < x:xs where
+ HeadC x = [x]
+We can then use ``HeadC`` in both expression and pattern contexts. In a pattern
+context it will match the head of any list with length at least one. In an
+expression context it will construct a singleton list.
.. _newtypederiving:
+The table below summarises where each kind of pattern synonym can be used.
Generalised derived instances for newtypes

++++++
+ Context  Unidirectional  Bidirectional  Explicitly Bidirectional 
++===============+================+===============+===========================+
+ Pattern  Yes  Yes  Yes 
++++++
+ Expression  No  Yes (Inferred) Yes (Explicit) 
++++++
.. ghcflag:: XGeneralisedNewtypeDeriving
 XGeneralizedNewtypeDeriving
+.. _recordpatsyn:
 Enable GHC's cunning generalised deriving mechanism for ``newtype``\s
+Record Pattern Synonyms
+
When you define an abstract type using ``newtype``, you may want the new
type to inherit some instances from its representation. In Haskell 98,
you can inherit instances of ``Eq``, ``Ord``, ``Enum`` and ``Bounded``
by deriving them, but for any other classes you have to write an
explicit instance declaration. For example, if you define ::
+It is also possible to define pattern synonyms which behave just like record
+constructors. The syntax for doing this is as follows:
 newtype Dollars = Dollars Int
+::
and you want to use arithmetic on ``Dollars``, you have to explicitly
define an instance of ``Num``: ::
+ pattern Point :: (Int, Int)
+ pattern Point{x, y} = (x, y)
 instance Num Dollars where
 Dollars a + Dollars b = Dollars (a+b)
 ...
+The idea is that we can then use ``Point`` just as if we had defined a new
+datatype ``MyPoint`` with two fields ``x`` and ``y``.
All the instance does is apply and remove the ``newtype`` constructor.
It is particularly galling that, since the constructor doesn't appear at
runtime, this instance declaration defines a dictionary which is
*wholly equivalent* to the ``Int`` dictionary, only slower!
+::
.. _generalizednewtypederiving:
+ data MyPoint = Point { x :: Int, y :: Int }
Generalising the deriving clause
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Whilst a normal pattern synonym can be used in two ways, there are then seven
+ways in which to use ``Point``. Precisely the ways in which a normal record
+constructor can be used.
GHC now permits such instances to be derived instead, using the flag
:ghcflag:`XGeneralizedNewtypeDeriving`, so one can write ::
+======================================= ==================================
+Usage Example
+======================================= ==================================
+As a constructor ``zero = Point 0 0``
+As a constructor with record syntax ``zero = Point { x = 0, y = 0}``
+In a pattern context ``isZero (Point 0 0) = True``
+In a pattern context with record syntax ``isZero (Point { x = 0, y = 0 }``
+In a pattern context with field puns ``getX (Point {x}) = x``
+In a record update ``(0, 0) { x = 1 } == (1,0)``
+Using record selectors ``x (0,0) == 0``
+======================================= ==================================
 newtype Dollars = Dollars Int deriving (Eq,Show,Num)
+For a unidirectional record pattern synonym we define record selectors but do
+not allow record updates or construction.
and the implementation uses the *same* ``Num`` dictionary for
``Dollars`` as for ``Int``. Notionally, the compiler derives an instance
declaration of the form ::
+The syntax and semantics of pattern synonyms are elaborated in the
+following subsections. See the :ghcwiki:`Wiki page ` for more
+details.
 instance Num Int => Num Dollars
+Syntax and scoping of pattern synonyms
+
which just adds or removes the ``newtype`` constructor according to the
type.
+A pattern synonym declaration can be either unidirectional,
+bidirectional or explicitly bidirectional.
+The syntax for unidirectional pattern synonyms is: ::
We can also derive instances of constructor classes in a similar way.
For example, suppose we have implemented state and failure monad
transformers, such that ::
+ pattern pat_lhs < pat
 instance Monad m => Monad (State s m)
 instance Monad m => Monad (Failure m)
+the syntax for bidirectional pattern synonyms is: ::
In Haskell 98, we can define a parsing monad by ::
+ pattern pat_lhs = pat
 type Parser tok m a = State [tok] (Failure m) a
+and the syntax for explicitly bidirectional pattern synonyms is: ::
+
+ pattern pat_lhs < pat where
+ pat_lhs = expr
which is automatically a monad thanks to the instance declarations
above. With the extension, we can make the parser type abstract, without
needing to write an instance of class ``Monad``, via ::
+We can define either prefix, infix or record pattern synonyms by modifying
+the form of `pat_lhs`. The syntax for these is as follows:
 newtype Parser tok m a = Parser (State [tok] (Failure m) a)
 deriving Monad
+======= ============================
+Prefix ``Name args``
+ 
+Infix ``arg1 `Name` arg2``
+ or ``arg1 op arg2``
+ 
+Record ``Name{arg1,arg2,...,argn}``
+======= ============================
In this case the derived instance declaration is of the form ::
 instance Monad (State [tok] (Failure m)) => Monad (Parser tok m)
+Pattern synonym declarations can only occur in the top level of a
+module. In particular, they are not allowed as local definitions.
Notice that, since ``Monad`` is a constructor class, the instance is a
*partial application* of the new type, not the entire left hand side. We
can imagine that the type declaration is "etaconverted" to generate the
context of the instance declaration.
+The variables in the lefthand side of the definition are bound by the
+pattern on the righthand side. For bidirectional pattern
+synonyms, all the variables of the righthand side must also occur on
+the lefthand side; also, wildcard patterns and view patterns are not
+allowed. For unidirectional and explicitly bidirectional pattern
+synonyms, there is no restriction on the righthand side pattern.
We can even derive instances of multiparameter classes, provided the
newtype is the last class parameter. In this case, a "partial
application" of the class appears in the ``deriving`` clause. For
example, given the class ::
+Pattern synonyms cannot be defined recursively.
 class StateMonad s m  m > s where ...
 instance Monad m => StateMonad s (State s m) where ...
+.. _patsynimpexp:
then we can derive an instance of ``StateMonad`` for ``Parser`` by ::
+Import and export of pattern synonyms
+
 newtype Parser tok m a = Parser (State [tok] (Failure m) a)
 deriving (Monad, StateMonad [tok])
+The name of the pattern synonym is in the same namespace as proper data
+constructors. Like normal data constructors, pattern synonyms can be imported
+and exported through association with a type constructor or independently.
The derived instance is obtained by completing the application of the
class to the new type: ::
+To export them on their own, in an export or import specification, you must
+prefix pattern names with the ``pattern`` keyword, e.g.: ::
 instance StateMonad [tok] (State [tok] (Failure m)) =>
 StateMonad [tok] (Parser tok m)
+ module Example (pattern Zero) where
As a result of this extension, all derived instances in newtype
declarations are treated uniformly (and implemented just by reusing the
dictionary for the representation type), *except* ``Show`` and ``Read``,
which really behave differently for the newtype and its representation.
+ data MyNum = MkNum Int
A more precise specification
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+ pattern Zero :: MyNum
+ pattern Zero = MkNum 0
A derived instance is derived only for declarations of these forms
(after expansion of any type synonyms) ::
+Without the ``pattern`` prefix, ``Zero`` would be interpreted as a
+type constructor in the export list.
 newtype T v1..vn = MkT (t vk+1..vn) deriving (C t1..tj)
 newtype instance T s1..sk vk+1..vn = MkT (t vk+1..vn) deriving (C t1..tj)
+You may also use the ``pattern`` keyword in an import/export
+specification to import or export an ordinary data constructor. For
+example: ::
where
+ import Data.Maybe( pattern Just )
 ``v1..vn`` are type variables, and ``t``, ``s1..sk``, ``t1..tj`` are
 types.
+would bring into scope the data constructor ``Just`` from the ``Maybe``
+type, without also bringing the type constructor ``Maybe`` into scope.
 The ``(C t1..tj)`` is a partial applications of the class ``C``,
 where the arity of ``C`` is exactly ``j+1``. That is, ``C`` lacks
 exactly one type argument.
+To bundle a pattern synonym with a type constructor, we list the pattern
+synonym in the export list of a module which exports the type constructor.
+For example, to bundle ``Zero`` with ``MyNum`` we could write the following: ::
 ``k`` is chosen so that ``C t1..tj (T v1...vk)`` is wellkinded. (Or,
 in the case of a ``data instance``, so that ``C t1..tj (T s1..sk)``
 is well kinded.)
+ module Example ( MyNum(Zero) ) where
 The type ``t`` is an arbitrary type.
+If a module was then to import ``MyNum`` from ``Example``, it would also import
+the pattern synonym ``Zero``.
 The type variables ``vk+1...vn`` do not occur in the types ``t``,
 ``s1..sk``, or ``t1..tj``.
+It is also possible to use the special token ``..`` in an export list to mean
+all currently bundled constructors. For example, we could write: ::
 ``C`` is not ``Read``, ``Show``, ``Typeable``, or ``Data``. These
 classes should not "look through" the type or its constructor. You
 can still derive these classes for a newtype, but it happens in the
 usual way, not via this new mechanism.
+ module Example ( MyNum(.., Zero) ) where
 It is safe to coerce each of the methods of ``C``. That is, the
 missing last argument to ``C`` is not used at a nominal role in any
 of the ``C``'s methods. (See :ref:`roles`.)
+in which case, ``Example`` would export the type constructor ``MyNum`` with
+the data constructor ``MkNum`` and also the pattern synonym ``Zero``.
Then the derived instance declaration is of the form ::
+Bundled patterns synoyms are type checked to ensure that they are of the same
+type as the type constructor which they are bundled with. A pattern synonym
+``P`` can not be bundled with a type constructor ``T`` if ``P``\'s type is visibly
+incompatible with ``T``.
 instance C t1..tj t => C t1..tj (T v1...vk)
+A module which imports ``MyNum(..)`` from ``Example`` and then reexports
+``MyNum(..)`` will also export any pattern synonyms bundled with ``MyNum`` in
+``Example``. A more complete specification can be found on the
+:ghcwiki:`wiki. `
As an example which does *not* work, consider ::
+Typing of pattern synonyms
+
 newtype NonMonad m s = NonMonad (State s m s) deriving Monad
+Given a pattern synonym definition of the form ::
Here we cannot derive the instance ::
+ pattern P var1 var2 ... varN < pat
 instance Monad (State s m) => Monad (NonMonad m)
+it is assigned a *pattern type* of the form ::
because the type variable ``s`` occurs in ``State s m``, and so cannot
be "etaconverted" away. It is a good thing that this ``deriving``
clause is rejected, because ``NonMonad m`` is not, in fact, a monad 
for the same reason. Try defining ``>>=`` with the correct type: you
won't be able to.
+ pattern P :: CReq => CProv => t1 > t2 > ... > tN > t
Notice also that the *order* of class parameters becomes important,
since we can only derive instances for the last one. If the
``StateMonad`` class above were instead defined as ::
+where ⟨CProv⟩ and ⟨CReq⟩ are type contexts, and ⟨t1⟩, ⟨t2⟩, ..., ⟨tN⟩
+and ⟨t⟩ are types. Notice the unusual form of the type, with two
+contexts ⟨CProv⟩ and ⟨CReq⟩:
 class StateMonad m s  m > s where ...
+ ⟨CProv⟩ are the constraints *made available (provided)* by a
+ successful pattern match.
then we would not have been able to derive an instance for the
``Parser`` type above. We hypothesise that multiparameter classes
usually have one "main" parameter for which deriving new instances is
most interesting.
+ ⟨CReq⟩ are the constraints *required* to match the pattern.
Lastly, all of this applies only for classes other than ``Read``,
``Show``, ``Typeable``, and ``Data``, for which the builtin derivation
applies (section 4.3.3. of the Haskell Report). (For the standard
classes ``Eq``, ``Ord``, ``Ix``, and ``Bounded`` it is immaterial
whether the standard method is used or the one described here.)
+For example, consider ::
.. _deriveanyclass:
+ data T a where
+ MkT :: (Show b) => a > b > T a
Deriving any other class

+ f1 :: (Eq a, Num a) => T a > String
+ f1 (MkT 42 x) = show x
.. ghcflag:: XDeriveAnyClass
+ pattern ExNumPat :: (Num a, Eq a) => (Show b) => b > T a
+ pattern ExNumPat x = MkT 42 x
 :since: 7.10.1
+ f2 :: (Eq a, Num a) => T a > String
+ f2 (ExNumPat x) = show x
 Allow use of any typeclass in ``deriving`` clauses.
+Here ``f1`` does not use pattern synonyms. To match against the numeric
+pattern ``42`` *requires* the caller to satisfy the constraints
+``(Num a, Eq a)``, so they appear in ``f1``'s type. The call to ``show``
+generates a ``(Show b)`` constraint, where ``b`` is an existentially
+type variable bound by the pattern match on ``MkT``. But the same
+pattern match also *provides* the constraint ``(Show b)`` (see ``MkT``'s
+type), and so all is well.
With :ghcflag:`XDeriveAnyClass` you can derive any other class. The compiler
will simply generate an instance declaration with no explicitlydefined
methods.
This is
mostly useful in classes whose `minimal set <#minimalpragma>`__ is
empty, and especially when writing
`generic functions <#genericprogramming>`__.
+Exactly the same reasoning applies to ``ExNumPat``: matching against
+``ExNumPat`` *requires* the constraints ``(Num a, Eq a)``, and
+*provides* the constraint ``(Show b)``.
As an example, consider a simple prettyprinter class ``SPretty``, which outputs
pretty strings: ::
+Note also the following points
 {# LANGUAGE DefaultSignatures, DeriveAnyClass #}
+ In the common case where ``Prov`` is empty, ``()``, it can be omitted
+ altogether.
 class SPretty a where
 sPpr :: a > String
 default sPpr :: Show a => a > String
 sPpr = show
+ You may specify an explicit *pattern signature*, as we did for
+ ``ExNumPat`` above, to specify the type of a pattern, just as you can
+ for a function. As usual, the type signature can be less polymorphic
+ than the inferred type. For example
If a user does not provide a manual implementation for ``sPpr``, then it will
default to ``show``. Now we can leverage the :ghcflag:`XDeriveAnyClass` extension to
easily implement a ``SPretty`` instance for a new data type: ::
+ ::
 data Foo = Foo deriving (Show, SPretty)
+  Inferred type would be 'a > [a]'
+ pattern SinglePair :: (a, a) > [(a, a)]
+ pattern SinglePair x = [x]
The above code is equivalent to: ::
+ The GHCi :ghcicmd:`:info` command shows pattern types in this format.
 data Foo = Foo deriving Show
 instance SPretty Foo
+ For a bidirectional pattern synonym, a use of the pattern synonym as
+ an expression has the type
That is, an ``SPretty Foo`` instance will be created with empty implementations
for all methods. Since we are using :ghcflag:`XDefaultSignatures` in this example, a
default implementation of ``sPpr`` is filled in automatically.
+ ::
Note the following details
+ (CReq, CProv) => t1 > t2 > ... > tN > t
 In case you try to derive some
 class on a newtype, and :ghcflag:`XGeneralizedNewtypeDeriving` is also on,
 :ghcflag:`XDeriveAnyClass` takes precedence.
+ So in the previous example, when used in an expression, ``ExNumPat``
+ has type
 :ghcflag:`XDeriveAnyClass` is allowed only when the last argument of the class
 has kind ``*`` or ``(* > *)``. So this is not allowed: ::
+ ::
 data T a b = MkT a b deriving( Bifunctor )
+ ExNumPat :: (Num a, Eq a, Show b) => b > T t
 because the last argument of ``Bifunctor :: (* > * > *) > Constraint``
 has the wrong kind.
+ Notice that this is a tiny bit more restrictive than the expression
+ ``MkT 42 x`` which would not require ``(Eq a)``.
 The instance context will be generated according to the same rules
 used when deriving ``Eq`` (if the kind of the type is ``*``), or
 the rules for ``Functor`` (if the kind of the type is ``(* > *)``).
 For example ::
+ Consider these two pattern synonyms: ::
 instance C a => C (a,b) where ...
+ data S a where
+ S1 :: Bool > S Bool
 data T a b = MkT a (a,b) deriving( C )
+ pattern P1 :: Bool > Maybe Bool
+ pattern P1 b = Just b
 The ``deriving`` clause will generate ::
+ pattern P2 :: () => (b ~ Bool) => Bool > S b
+ pattern P2 b = S1 b
 instance C a => C (T a b) where {}
+ f :: Maybe a > String
+ f (P1 x) = "no no no"  Typeincorrect
 The constraints `C a` and `C (a,b)` are generated from the data
 constructor arguments, but the latter simplifies to `C a`.
+ g :: S a > String
+ g (P2 b) = "yes yes yes"  Fine
 :ghcflag:`XDeriveAnyClass` can be used with partially applied classes,
 such as ::
+ Pattern ``P1`` can only match against a value of type ``Maybe Bool``,
+ so function ``f`` is rejected because the type signature is
+ ``Maybe a``. (To see this, imagine expanding the pattern synonym.)
 data T a = MKT a deriving( D Int )
+ On the other hand, function ``g`` works fine, because matching
+ against ``P2`` (which wraps the GADT ``S``) provides the local
+ equality ``(a~Bool)``. If you were to give an explicit pattern
+ signature ``P2 :: Bool > S Bool``, then ``P2`` would become less
+ polymorphic, and would behave exactly like ``P1`` so that ``g`` would
+ then be rejected.
 which generates ::
+ In short, if you want GADTlike behaviour for pattern synonyms, then
+ (unlike unlike concrete data constructors like ``S1``) you must write
+ its type with explicit provided equalities. For a concrete data
+ constructor like ``S1`` you can write its type signature as either
+ ``S1 :: Bool > S Bool`` or ``S1 :: (b~Bool) => Bool > S b``; the
+ two are equivalent. Not so for pattern synonyms: the two forms are
+ different, in order to distinguish the two cases above. (See
+ :ghcticket:`9953` for discussion of this choice.)
 instance D Int a => D Int (T a) where {}
+Matching of pattern synonyms
+
 :ghcflag:`XDeriveAnyClass` can be used to fill in default instances for
 associated type families: ::
+A pattern synonym occurrence in a pattern is evaluated by first matching
+against the pattern synonym itself, and then on the argument patterns.
+For example, in the following program, ``f`` and ``f'`` are equivalent: ::
 {# LANGUAGE DeriveAnyClass, TypeFamilies #}
+ pattern Pair x y < [x, y]
 class Sizable a where
 type Size a
 type Size a = Int
+ f (Pair True True) = True
+ f _ = False
 data Bar = Bar deriving Sizable
+ f' [x, y]  True < x, True < y = True
+ f' _ = False
 doubleBarSize :: Size Bar > Size Bar
 doubleBarSize s = 2*s
+Note that the strictness of ``f`` differs from that of ``g`` defined
+below:
 The ``deriving( Sizable )`` is equivalent to saying ::
+.. codeblock:: none
 instance Sizeable Bar where {}
+ g [True, True] = True
+ g _ = False
 and then the normal rules for filling in associated types from the
 default will apply, making ``Size Bar`` equal to ``Int``.
+ *Main> f (False:undefined)
+ *** Exception: Prelude.undefined
+ *Main> g (False:undefined)
+ False
.. _typeclassextensions:
@@ 7544,10 +7544,13 @@ the type level:
GHC.TypeLits> natVal (lg (Proxy :: Proxy 2) (Proxy :: Proxy 8))
3
+Constraints in types
+====================
+
.. _equalityconstraints:
Equality constraints
====================
+
A type context can include equality constraints of the form ``t1 ~ t2``,
which denote that the types ``t1`` and ``t2`` need to be the same. In
@@ 7597,7 +7600,7 @@ the paper
.. _constraintkind:
The ``Constraint`` kind
=======================
+
.. ghcflag:: XConstraintKinds
@@ 7673,10 +7676,10 @@ contexts and superclasses, but to do so you must use
:ghcflag:`XUndecidableInstances` to signal that you don't mind if the type
checker fails to terminate.
.. _othertypeextensions:
+.. _extensionstotypesignatures:
Other type system extensions
============================
+Extensions to type signatures
+=============================
.. _explicitforalls:
@@ 7698,18 +7701,26 @@ means this: ::
g :: forall b. (b > b)
The two are treated identically.
+The two are treated identically, except that the latter may bring type variables
+into scope (see :ref:`scopedtypevariables`).
+
+Notes:
+
+ With :ghcflag:`XExplicitForAll`, ``forall`` becomes a keyword; you can't use ``forall`` as a
+ type variable any more!
Of course ``forall`` becomes a keyword; you can't use ``forall`` as a
type variable any more!
+ As well in type signatures, you can also use an explicit ``forall``
+ in an instance declaration: ::
If the :ghcflag:`Wunusedforalls` flag is enabled, a warning will be emitted
when you write a type variable in an explicit ``forall`` statement that is
otherwise unused. For instance: ::
+ instance forall a. Eq a => Eq [a] where ...
+
+ If the :ghcflag:`Wunusedforalls` flag is enabled, a warning will be emitted
+ when you write a type variable in an explicit ``forall`` statement that is
+ otherwise unused. For instance: ::
g :: forall a b. (b > b)
would warn about the unused type variable `a`.
+ would warn about the unused type variable `a`.
.. _flexiblecontexts:
@@ 7763,283 +7774,83 @@ dependencies: ::
The ``Int`` may well fix ``b`` at the call site, so that signature
should not be rejected. Moreover, the dependencies might be hidden.
Consider ::

 class X a b where ...
 class D a b  a > b where ...
 instance D a b => X [a] b where...
 h :: X a b => a > a

Here ``h``\'s type looks ambiguous in ``b``, but here's a legal call: ::

 ...(h [True])...

That gives rise to a ``(X [Bool] beta)`` constraint, and using the
instance means we need ``(D Bool beta)`` and that fixes ``beta`` via
``D``\'s fundep!

Behind all these special cases there is a simple guiding principle.
Consider ::

 f :: type
 f = ...blah...

 g :: type
 g = f

You would think that the definition of ``g`` would surely typecheck!
After all ``f`` has exactly the same type, and ``g=f``. But in fact
``f``\'s type is instantiated and the instantiated constraints are solved
against the constraints bound by ``g``\ 's signature. So, in the case an
ambiguous type, solving will fail. For example, consider the earlier
definition ``f :: C a => Int``: ::

 f :: C a => Int
 f = ...blah...

 g :: C a => Int
 g = f

In ``g``\'s definition, we'll instantiate to ``(C alpha)`` and try to
deduce ``(C alpha)`` from ``(C a)``, and fail.

So in fact we use this as our *definition* of ambiguity: a type ``ty``
is ambiguous if and only if ``((undefined :: ty) :: ty)`` would fail to
typecheck. We use a very similar test for *inferred* types, to ensure
that they too are unambiguous.

*Switching off the ambiguity check.* Even if a function is has an
ambiguous type according the "guiding principle", it is possible that
the function is callable. For example: ::

 class D a b where ...
 instance D Bool b where ...

 strange :: D a b => a > a
 strange = ...blah...

 foo = strange True

Here ``strange``\'s type is ambiguous, but the call in ``foo`` is OK
because it gives rise to a constraint ``(D Bool beta)``, which is
soluble by the ``(D Bool b)`` instance. So the language extension
:ghcflag:`XAllowAmbiguousTypes` allows you to switch off the ambiguity check.
But even with ambiguity checking switched off, GHC will complain about a
function that can *never* be called, such as this one: ::

 f :: (Int ~ Bool) => a > a

.. note::
 *A historical note.* GHC used to impose some more restrictive and less
 principled conditions on type signatures. For type
 ``forall tv1..tvn (c1, ...,cn) => type`` GHC used to require

 a. that each universally quantified type variable ``tvi`` must be "reachable"
 from ``type``, and

 b. that every constraint ``ci`` mentions at least one of the universally
 quantified type variables ``tvi``. These adhoc restrictions are
 completely subsumed by the new ambiguity check.

.. _implicitparameters:

Implicit parameters


.. ghcflag:: XImplicitParams

 Allow definition of functions expecting implicit parameters.

Implicit parameters are implemented as described in [Lewis2000]_ and enabled
with the option :ghcflag:`XImplicitParams`. (Most of the following, still rather
incomplete, documentation is due to Jeff Lewis.)

.. [Lewis2000]
 "Implicit parameters: dynamic scoping with static types",
 J Lewis, MB Shields, E Meijer, J Launchbury,
 *27th ACM Symposium on Principles of Programming Languages (POPL'00)*,
 Boston, Jan 2000.

A variable is called *dynamically bound* when it is bound by the calling
context of a function and *statically bound* when bound by the callee's
context. In Haskell, all variables are statically bound. Dynamic binding
of variables is a notion that goes back to Lisp, but was later discarded
in more modern incarnations, such as Scheme. Dynamic binding can be very
confusing in an untyped language, and unfortunately, typed languages, in
particular HindleyMilner typed languages like Haskell, only support
static scoping of variables.

However, by a simple extension to the type class system of Haskell, we
can support dynamic binding. Basically, we express the use of a
dynamically bound variable as a constraint on the type. These
constraints lead to types of the form ``(?x::t') => t``, which says
"this function uses a dynamicallybound variable ``?x`` of type ``t'``".
For example, the following expresses the type of a sort function,
implicitly parameterised by a comparison function named ``cmp``. ::

 sort :: (?cmp :: a > a > Bool) => [a] > [a]

The dynamic binding constraints are just a new form of predicate in the
type class system.

An implicit parameter occurs in an expression using the special form
``?x``, where ``x`` is any valid identifier (e.g. ``ord ?x`` is a valid
expression). Use of this construct also introduces a new dynamicbinding
constraint in the type of the expression. For example, the following
definition shows how we can define an implicitly parameterised sort
function in terms of an explicitly parameterised ``sortBy`` function: ::

 sortBy :: (a > a > Bool) > [a] > [a]

 sort :: (?cmp :: a > a > Bool) => [a] > [a]
 sort = sortBy ?cmp

Implicitparameter type constraints
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Dynamic binding constraints behave just like other type class
constraints in that they are automatically propagated. Thus, when a
function is used, its implicit parameters are inherited by the function
that called it. For example, our ``sort`` function might be used to pick
out the least value in a list: ::

 least :: (?cmp :: a > a > Bool) => [a] > a
 least xs = head (sort xs)

Without lifting a finger, the ``?cmp`` parameter is propagated to become
a parameter of ``least`` as well. With explicit parameters, the default
is that parameters must always be explicit propagated. With implicit
parameters, the default is to always propagate them.

An implicitparameter type constraint differs from other type class
constraints in the following way: All uses of a particular implicit
parameter must have the same type. This means that the type of
``(?x, ?x)`` is ``(?x::a) => (a,a)``, and not
``(?x::a, ?x::b) => (a, b)``, as would be the case for type class
constraints.

You can't have an implicit parameter in the context of a class or
instance declaration. For example, both these declarations are illegal: ::

 class (?x::Int) => C a where ...
 instance (?x::a) => Foo [a] where ...

Reason: exactly which implicit parameter you pick up depends on exactly
where you invoke a function. But the "invocation" of instance
declarations is done behind the scenes by the compiler, so it's hard to
figure out exactly where it is done. Easiest thing is to outlaw the
offending types.

Implicitparameter constraints do not cause ambiguity. For example,
consider: ::

 f :: (?x :: [a]) => Int > Int
 f n = n + length ?x

 g :: (Read a, Show a) => String > String
 g s = show (read s)

Here, ``g`` has an ambiguous type, and is rejected, but ``f`` is fine.
The binding for ``?x`` at ``f``\ 's call site is quite unambiguous, and
fixes the type ``a``.

Implicitparameter bindings
~~~~~~~~~~~~~~~~~~~~~~~~~~~

An implicit parameter is *bound* using the standard ``let`` or ``where``
binding forms. For example, we define the ``min`` function by binding
``cmp``. ::

 min :: Ord a => [a] > a
 min = let ?cmp = (<=) in least

A group of implicitparameter bindings may occur anywhere a normal group
of Haskell bindings can occur, except at top level. That is, they can
occur in a ``let`` (including in a list comprehension, or donotation,
or pattern guards), or a ``where`` clause. Note the following points:

 An implicitparameter binding group must be a collection of simple
 bindings to implicitstyle variables (no functionstyle bindings, and
 no type signatures); these bindings are neither polymorphic or
 recursive.
+Consider ::
 You may not mix implicitparameter bindings with ordinary bindings in
 a single ``let`` expression; use two nested ``let``\ s instead. (In
 the case of ``where`` you are stuck, since you can't nest ``where``
 clauses.)
+ class X a b where ...
+ class D a b  a > b where ...
+ instance D a b => X [a] b where...
+ h :: X a b => a > a
 You may put multiple implicitparameter bindings in a single binding
 group; but they are *not* treated as a mutually recursive group (as
 ordinary ``let`` bindings are). Instead they are treated as a
 nonrecursive group, simultaneously binding all the implicit
 parameter. The bindings are not nested, and may be reordered without
 changing the meaning of the program. For example, consider: ::
+Here ``h``\'s type looks ambiguous in ``b``, but here's a legal call: ::
 f t = let { ?x = t; ?y = ?x+(1::Int) } in ?x + ?y
+ ...(h [True])...
 The use of ``?x`` in the binding for ``?y`` does not "see" the
 binding for ``?x``, so the type of ``f`` is ::
+That gives rise to a ``(X [Bool] beta)`` constraint, and using the
+instance means we need ``(D Bool beta)`` and that fixes ``beta`` via
+``D``\'s fundep!
 f :: (?x::Int) => Int > Int
+Behind all these special cases there is a simple guiding principle.
+Consider ::
Implicit parameters and polymorphic recursion
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+ f :: type
+ f = ...blah...
Consider these two definitions: ::
+ g :: type
+ g = f
 len1 :: [a] > Int
 len1 xs = let ?acc = 0 in len_acc1 xs
+You would think that the definition of ``g`` would surely typecheck!
+After all ``f`` has exactly the same type, and ``g=f``. But in fact
+``f``\'s type is instantiated and the instantiated constraints are solved
+against the constraints bound by ``g``\ 's signature. So, in the case an
+ambiguous type, solving will fail. For example, consider the earlier
+definition ``f :: C a => Int``: ::
 len_acc1 [] = ?acc
 len_acc1 (x:xs) = let ?acc = ?acc + (1::Int) in len_acc1 xs
+ f :: C a => Int
+ f = ...blah...
 
+ g :: C a => Int
+ g = f
 len2 :: [a] > Int
 len2 xs = let ?acc = 0 in len_acc2 xs
+In ``g``\'s definition, we'll instantiate to ``(C alpha)`` and try to
+deduce ``(C alpha)`` from ``(C a)``, and fail.
 len_acc2 :: (?acc :: Int) => [a] > Int
 len_acc2 [] = ?acc
 len_acc2 (x:xs) = let ?acc = ?acc + (1::Int) in len_acc2 xs
+So in fact we use this as our *definition* of ambiguity: a type ``ty``
+is ambiguous if and only if ``((undefined :: ty) :: ty)`` would fail to
+typecheck. We use a very similar test for *inferred* types, to ensure
+that they too are unambiguous.
The only difference between the two groups is that in the second group
``len_acc`` is given a type signature. In the former case, ``len_acc1``
is monomorphic in its own righthand side, so the implicit parameter
``?acc`` is not passed to the recursive call. In the latter case,
because ``len_acc2`` has a type signature, the recursive call is made to
the *polymorphic* version, which takes ``?acc`` as an implicit
parameter. So we get the following results in GHCi:
+*Switching off the ambiguity check.* Even if a function is has an
+ambiguous type according the "guiding principle", it is possible that
+the function is callable. For example: ::
.. codeblock:: none
+ class D a b where ...
+ instance D Bool b where ...
 Prog> len1 "hello"
 0
 Prog> len2 "hello"
 5
+ strange :: D a b => a > a
+ strange = ...blah...
Adding a type signature dramatically changes the result! This is a
rather counterintuitive phenomenon, worth watching out for.
+ foo = strange True
Implicit parameters and monomorphism
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Here ``strange``\'s type is ambiguous, but the call in ``foo`` is OK
+because it gives rise to a constraint ``(D Bool beta)``, which is
+soluble by the ``(D Bool b)`` instance. So the language extension
+:ghcflag:`XAllowAmbiguousTypes` allows you to switch off the ambiguity check.
+But even with ambiguity checking switched off, GHC will complain about a
+function that can *never* be called, such as this one: ::
GHC applies the dreaded Monomorphism Restriction (section 4.5.5 of the
Haskell Report) to implicit parameters. For example, consider: ::
+ f :: (Int ~ Bool) => a > a
 f :: Int > Int
 f v = let ?x = 0 in
 let y = ?x + v in
 let ?x = 5 in
 y
+.. note::
+ *A historical note.* GHC used to impose some more restrictive and less
+ principled conditions on type signatures. For type
+ ``forall tv1..tvn (c1, ...,cn) => type`` GHC used to require
Since the binding for ``y`` falls under the Monomorphism Restriction it
is not generalised, so the type of ``y`` is simply ``Int``, not
``(?x::Int) => Int``. Hence, ``(f 9)`` returns result ``9``. If you add
a type signature for ``y``, then ``y`` will get type
``(?x::Int) => Int``, so the occurrence of ``y`` in the body of the
``let`` will see the inner binding of ``?x``, so ``(f 9)`` will return
``14``.
+ a. that each universally quantified type variable ``tvi`` must be "reachable"
+ from ``type``, and
+ b. that every constraint ``ci`` mentions at least one of the universally
+ quantified type variables ``tvi``. These adhoc restrictions are
+ completely subsumed by the new ambiguity check.
.. _kinding:
@@ 8079,702 +7890,903 @@ This flag enables kind signatures in the following places:
 ``class`` declarations: ::
 class (Eq a) => C (f :: * > *) a where ...
+ class (Eq a) => C (f :: * > *) a where ...
+
+ ``forall``\'s in type signatures: ::
+
+ f :: forall (cxt :: * > *). Set cxt Int
+
+The parentheses are required. Some of the spaces are required too, to
+separate the lexemes. If you write ``(f::*>*)`` you will get a parse
+error, because ``::*>*`` is a single lexeme in Haskell.
+
+As part of the same extension, you can put kind annotations in types as
+well. Thus: ::
+
+ f :: (Int :: *) > Int
+ g :: forall a. a > (a :: *)
+
+The syntax is
+
+.. codeblock:: none
+
+ atype ::= '(' ctype '::' kind ')
+
+The parentheses are required.
+
+.. _universalquantification:
+
+.. _scopedtypevariables:
+
+Lexically scoped type variables
+===============================
+
+.. ghcflag:: XScopedTypeVariables
+
+ :implies: :ghcflag:`XRelaxedPolyRec`
+ :implies: :ghcflag:`XExplicitForAll`
+
+ Enable lexical scoping of type variables explicitly introduced with
+ ``forall``.
+
+GHC supports *lexically scoped type variables*, without which some type
+signatures are simply impossible to write. For example: ::
+
+ f :: forall a. [a] > [a]
+ f xs = ys ++ ys
+ where
+ ys :: [a]
+ ys = reverse xs
+
+The type signature for ``f`` brings the type variable ``a`` into scope,
+because of the explicit ``forall`` (:ref:`decltypesigs`). The type
+variables bound by a ``forall`` scope over the entire definition of the
+accompanying value declaration. In this example, the type variable ``a``
+scopes over the whole definition of ``f``, including over the type
+signature for ``ys``. In Haskell 98 it is not possible to declare a type
+for ``ys``; a major benefit of scoped type variables is that it becomes
+possible to do so.
+
+Lexicallyscoped type variables are enabled by
+:ghcflag:`XScopedTypeVariables`. This flag implies :ghcflag:`XRelaxedPolyRec`.
+
+Overview
+
+
+The design follows the following principles
+
+ A scoped type variable stands for a type *variable*, and not for a
+ *type*. (This is a change from GHC's earlier design.)
+
+ Furthermore, distinct lexical type variables stand for distinct type
+ variables. This means that every programmerwritten type signature
+ (including one that contains free scoped type variables) denotes a
+ *rigid* type; that is, the type is fully known to the type checker,
+ and no inference is involved.
+
+ Lexical type variables may be alpharenamed freely, without changing
+ the program.
+
+A *lexically scoped type variable* can be bound by:
+
+ A declaration type signature (:ref:`decltypesigs`)
+
+ An expression type signature (:ref:`exptypesigs`)
+
+ A pattern type signature (:ref:`patterntypesigs`)
+
+ Class and instance declarations (:ref:`clsinstscopedtyvars`)
+
+In Haskell, a programmerwritten type signature is implicitly quantified
+over its free type variables (`Section
+4.1.2 `__ of
+the Haskell Report). Lexically scoped type variables affect this
+implicit quantification rules as follows: any type variable that is in
+scope is *not* universally quantified. For example, if type variable
+``a`` is in scope, then ::
+
+ (e :: a > a) means (e :: a > a)
+ (e :: b > b) means (e :: forall b. b>b)
+ (e :: a > b) means (e :: forall b. a>b)
+
+.. _decltypesigs:
+
+Declaration type signatures
+
+
+A declaration type signature that has *explicit* quantification (using
+``forall``) brings into scope the explicitlyquantified type variables,
+in the definition of the named function. For example: ::
+
+ f :: forall a. [a] > [a]
+ f (x:xs) = xs ++ [ x :: a ]
+
+The "``forall a``" brings "``a``" into scope in the definition of
+"``f``".
+
+This only happens if:
+
+ The quantification in ``f``\'s type signature is explicit. For
+ example: ::
+
+ g :: [a] > [a]
+ g (x:xs) = xs ++ [ x :: a ]
+
+ This program will be rejected, because "``a``" does not scope over
+ the definition of "``g``", so "``x::a``" means "``x::forall a. a``"
+ by Haskell's usual implicit quantification rules.
+
+ The signature gives a type for a function binding or a bare variable
+ binding, not a pattern binding. For example: ::
+
+ f1 :: forall a. [a] > [a]
+ f1 (x:xs) = xs ++ [ x :: a ]  OK
+
+ f2 :: forall a. [a] > [a]
+ f2 = \(x:xs) > xs ++ [ x :: a ]  OK
+
+ f3 :: forall a. [a] > [a]
+ Just f3 = Just (\(x:xs) > xs ++ [ x :: a ])  Not OK!
+
+ The binding for ``f3`` is a pattern binding, and so its type
+ signature does not bring ``a`` into scope. However ``f1`` is a
+ function binding, and ``f2`` binds a bare variable; in both cases the
+ type signature brings ``a`` into scope.
+
+.. _exptypesigs:
+
+Expression type signatures
+
 ``forall``\'s in type signatures: ::
+An expression type signature that has *explicit* quantification (using
+``forall``) brings into scope the explicitlyquantified type variables,
+in the annotated expression. For example: ::
 f :: forall (cxt :: * > *). Set cxt Int
+ f = runST ( (op >>= \(x :: STRef s Int) > g x) :: forall s. ST s Bool )
The parentheses are required. Some of the spaces are required too, to
separate the lexemes. If you write ``(f::*>*)`` you will get a parse
error, because ``::*>*`` is a single lexeme in Haskell.
+Here, the type signature ``forall s. ST s Bool`` brings the type
+variable ``s`` into scope, in the annotated expression
+``(op >>= \(x :: STRef s Int) > g x)``.
As part of the same extension, you can put kind annotations in types as
well. Thus: ::
+.. _patterntypesigs:
 f :: (Int :: *) > Int
 g :: forall a. a > (a :: *)
+Pattern type signatures
+
The syntax is
+A type signature may occur in any pattern; this is a *pattern type
+signature*. For example: ::
.. codeblock:: none
+  f and g assume that 'a' is already in scope
+ f = \(x::Int, y::a) > x
 atype ::= '(' ctype '::' kind ')
+ g (x::a) = x
The parentheses are required.
+ h ((x,y) :: (Int,Bool)) = (y,x)
.. _universalquantification:
+In the case where all the type variables in the pattern type signature
+are already in scope (i.e. bound by the enclosing context), matters are
+simple: the signature simply constrains the type of the pattern in the
+obvious way.
Arbitraryrank polymorphism

+Unlike expression and declaration type signatures, pattern type
+signatures are not implicitly generalised. The pattern in a *pattern
+binding* may only mention type variables that are already in scope. For
+example: ::
.. ghcflag:: XRankNTypes
+ f :: forall a. [a] > (Int, [a])
+ f xs = (n, zs)
+ where
+ (ys::[a], n) = (reverse xs, length xs)  OK
+ zs::[a] = xs ++ ys  OK
+ Just (v::b) = ...  Not OK; b is not in scope
 :implies: :ghcflag:`XExplicitForAll`
+Here, the pattern signatures for ``ys`` and ``zs`` are fine, but the one
+for ``v`` is not because ``b`` is not in scope.
 Allow types of arbitrary rank.
+However, in all patterns *other* than pattern bindings, a pattern type
+signature may mention a type variable that is not in scope; in this
+case, *the signature brings that type variable into scope*. This is
+particularly important for existential data constructors. For example: ::
.. ghcflag:: XRank2Types
+ data T = forall a. MkT [a]
 A deprecated alias of :ghcflag:`XRankNTypes`.
+ k :: T > T
+ k (MkT [t::a]) =
+ MkT t3
+ where
+ t3::[a] = [t,t,t]
GHC's type system supports *arbitraryrank* explicit universal
quantification in types. For example, all the following types are legal: ::
+Here, the pattern type signature ``(t::a)`` mentions a lexical type
+variable that is not already in scope. Indeed, it *cannot* already be in
+scope, because it is bound by the pattern match. GHC's rule is that in
+this situation (and only then), a pattern type signature can mention a
+type variable that is not already in scope; the effect is to bring it
+into scope, standing for the existentiallybound type variable.
 f1 :: forall a b. a > b > a
 g1 :: forall a b. (Ord a, Eq b) => a > b > a
+When a pattern type signature binds a type variable in this way, GHC
+insists that the type variable is bound to a *rigid*, or fullyknown,
+type variable. This means that any userwritten type signature always
+stands for a completely known type.
 f2 :: (forall a. a>a) > Int > Int
 g2 :: (forall a. Eq a => [a] > a > Bool) > Int > Int
+If all this seems a little odd, we think so too. But we must have *some*
+way to bring such type variables into scope, else we could not name
+existentiallybound type variables in subsequent type signatures.
 f3 :: ((forall a. a>a) > Int) > Bool > Bool
+This is (now) the *only* situation in which a pattern type signature is
+allowed to mention a lexical variable that is not already in scope. For
+example, both ``f`` and ``g`` would be illegal if ``a`` was not already
+in scope.
 f4 :: Int > (forall a. a > a)
+.. _clsinstscopedtyvars:
Here, ``f1`` and ``g1`` are rank1 types, and can be written in standard
Haskell (e.g. ``f1 :: a>b>a``). The ``forall`` makes explicit the
universal quantification that is implicitly added by Haskell.
+Class and instance declarations
+
The functions ``f2`` and ``g2`` have rank2 types; the ``forall`` is on
the left of a function arrow. As ``g2`` shows, the polymorphic type on
the left of the function arrow can be overloaded.
+The type variables in the head of a ``class`` or ``instance``
+declaration scope over the methods defined in the ``where`` part. You do
+not even need an explicit ``forall`` (although you are allowed an explicit
+``forall`` in an ``instance`` declaration; see :ref:`explicitforalls`).
+For example: ::
The function ``f3`` has a rank3 type; it has rank2 types on the left
of a function arrow.
+ class C a where
+ op :: [a] > a
The language option :ghcflag:`XRankNTypes` (which implies
:ghcflag:`XExplicitForAll`) enables higherrank
types. That is, you can nest ``forall``\ s arbitrarily deep in function
arrows. For example, a foralltype (also called a "type scheme"),
including a typeclass context, is legal:
+ op xs = let ys::[a]
+ ys = reverse xs
+ in
+ head ys
 On the left or right (see ``f4``, for example) of a function arrow
+ instance C b => C [b] where
+ op xs = reverse (head (xs :: [[b]]))
 As the argument of a constructor, or type of a field, in a data type
 declaration. For example, any of the ``f1, f2, f3, g1, g2`` above would
 be valid field type signatures.
+Bindings and generalisation
+===========================
 As the type of an implicit parameter
+.. _monomorphism:
 In a pattern type signature (see :ref:`scopedtypevariables`)
+Switching off the dreaded Monomorphism Restriction
+
The :ghcflag:`XRankNTypes` option is also required for any type with a
``forall`` or context to the right of an arrow (e.g.
``f :: Int > forall a. a>a``, or ``g :: Int > Ord a => a > a``).
Such types are technically rank 1, but are clearly not Haskell98, and
an extra flag did not seem worth the bother.
+.. ghcflag:: XNoMonomorphismRestriction
In particular, in ``data`` and ``newtype`` declarations the constructor
arguments may be polymorphic types of any rank; see examples in
:ref:`univ`. Note that the declared types are nevertheless always
monomorphic. This is important because by default GHC will not
instantiate type variables to a polymorphic type
(:ref:`impredicativepolymorphism`).
+ :default: on
The obsolete language options :ghcflag:`XPolymorphicComponents` and
:ghcflag:`XRank2Types` are synonyms for :ghcflag:`XRankNTypes`. They used to
specify finer distinctions that GHC no longer makes. (They should really elicit
a deprecation warning, but they don't, purely to avoid the need to library
authors to change their old flags specifications.)
+ Prevents the compiler from applying the monomorphism restriction to
+ bindings lacking explicit type signatures.
.. _univ:
+Haskell's monomorphism restriction (see `Section
+4.5.5 `__ of
+the Haskell Report) can be completely switched off by
+:ghcflag:`XNoMonomorphismRestriction`. Since GHC 7.8.1, the monomorphism
+restriction is switched off by default in GHCi's interactive options
+(see :ref:`ghciinteractiveoptions`).
Examples
~~~~~~~~
+.. _typingbinds:
These are examples of ``data`` and ``newtype`` declarations whose data
constructors have polymorphic argument types: ::
+Generalised typing of mutually recursive bindings
+
 data T a = T1 (forall b. b > b > b) a
+.. ghcflag:: XRelaxedPolyRec
 data MonadT m = MkMonad { return :: forall a. a > m a,
 bind :: forall a b. m a > (a > m b) > m b
 }
+ Allow the typechecker to ignore references to bindings with
+ explicit type signatures.
 newtype Swizzle = MkSwizzle (forall a. Ord a => [a] > [a])
+The Haskell Report specifies that a group of bindings (at top level, or
+in a ``let`` or ``where``) should be sorted into stronglyconnected
+components, and then typechecked in dependency order
+(`Haskell Report, Section
+4.5.1 `__). As
+each group is typechecked, any binders of the group that have an
+explicit type signature are put in the type environment with the
+specified polymorphic type, and all others are monomorphic until the
+group is generalised (`Haskell Report, Section
+4.5.2 `__).
The constructors have rank2 types: ::
+Following a suggestion of Mark Jones, in his paper `Typing Haskell in
+Haskell `__, GHC implements a
+more general scheme. If :ghcflag:`XRelaxedPolyRec` is specified: *the
+dependency analysis ignores references to variables that have an
+explicit type signature*. As a result of this refined dependency
+analysis, the dependency groups are smaller, and more bindings will
+typecheck. For example, consider: ::
 T1 :: forall a. (forall b. b > b > b) > a > T a
+ f :: Eq a => a > Bool
+ f x = (x == x)  g True  g "Yes"
 MkMonad :: forall m. (forall a. a > m a)
 > (forall a b. m a > (a > m b) > m b)
 > MonadT m
+ g y = (y <= y)  f True
 MkSwizzle :: (forall a. Ord a => [a] > [a]) > Swizzle
+This is rejected by Haskell 98, but under Jones's scheme the definition
+for ``g`` is typechecked first, separately from that for ``f``, because
+the reference to ``f`` in ``g``\'s right hand side is ignored by the
+dependency analysis. Then ``g``\'s type is generalised, to get ::
In earlier versions of GHC, it was possible to omit the ``forall`` in
the type of the constructor if there was an explicit context. For
example: ::
+ g :: Ord a => a > Bool
 newtype Swizzle' = MkSwizzle' (Ord a => [a] > [a])
+Now, the definition for ``f`` is typechecked, with this type for ``g``
+in the type environment.
As of GHC 7.10, this is deprecated. The
:ghcflag:`Wcontextquantification` flag detects this situation and issues
a warning. In GHC 8.0 this flag was deprecated and declarations such as
``MkSwizzle'`` will cause an outofscope error.
+The same refined dependency analysis also allows the type signatures of
+mutuallyrecursive functions to have different contexts, something that
+is illegal in Haskell 98 (Section 4.5.2, last sentence). With
+:ghcflag:`XRelaxedPolyRec` GHC only insists that the type signatures of a
+*refined* group have identical type signatures; in practice this means
+that only variables bound by the same pattern binding must have the same
+context. For example, this is fine: ::
As for type signatures, implicit quantification happens for
nonoverloaded types too. So if you write this: ::
+ f :: Eq a => a > Bool
+ f x = (x == x)  g True
 f :: (a > a) > a
+ g :: Ord a => a > Bool
+ g y = (y <= y)  f True
it's just as if you had written this: ::
+.. _monolocalbinds:
 f :: forall a. (a > a) > a
+Letgeneralisation
+
That is, since the type variable ``a`` isn't in scope, it's implicitly
universally quantified.
+.. ghcflag:: XMonoLocalBinds
You construct values of types ``T1, MonadT, Swizzle`` by applying the
constructor to suitable values, just as usual. For example, ::
+ Infer less polymorphic types for local bindings by default.
 a1 :: T Int
 a1 = T1 (\xy>x) 3
+An MLstyle language usually generalises the type of any ``let``\bound or
+``where``\bound variable, so that it is as polymorphic as possible. With the
+flag :ghcflag:`XMonoLocalBinds` GHC implements a slightly more conservative
+policy, using the following rules:
 a2, a3 :: Swizzle
 a2 = MkSwizzle sort
 a3 = MkSwizzle reverse
+ A variable is *closed* if and only if
 a4 :: MonadT Maybe
 a4 = let r x = Just x
 b m k = case m of
 Just y > k y
 Nothing > Nothing
 in
 MkMonad r b
+  the variable is letbound
 mkTs :: (forall b. b > b > b) > a > [T a]
 mkTs f x y = [T1 f x, T1 f y]
+  one of the following holds:
The type of the argument can, as usual, be more general than the type
required, as ``(MkSwizzle reverse)`` shows. (``reverse`` does not need
the ``Ord`` constraint.)
+  the variable has an explicit type signature that has no free
+ type variables, or
When you use pattern matching, the bound variables may now have
polymorphic types. For example: ::
+  its binding group is fully generalised (see next bullet)
 f :: T a > a > (a, Char)
 f (T1 w k) x = (w k x, w 'c' 'd')
+ A binding group is *fully generalised* if and only if
 g :: (Ord a, Ord b) => Swizzle > [a] > (a > b) > [b]
 g (MkSwizzle s) xs f = s (map f (s xs))
+  each of its free variables is either imported or closed, and
 h :: MonadT m > [m a] > m [a]
 h m [] = return m []
 h m (x:xs) = bind m x $ \y >
 bind m (h m xs) $ \ys >
 return m (y:ys)
+  the binding is not affected by the monomorphism restriction
+ (`Haskell Report, Section
+ 4.5.5 `__)
In the function ``h`` we use the record selectors ``return`` and
``bind`` to extract the polymorphic bind and return functions from the
``MonadT`` data structure, rather than using pattern matching.
+For example, consider ::
+ f x = x + 1
+ g x = let h y = f y * 2
+ k z = z+x
+ in h x + k x
.. _higherranktypeinference:
+Here ``f`` is generalised because it has no free variables; and its
+binding group is unaffected by the monomorphism restriction; and hence
+``f`` is closed. The same reasoning applies to ``g``, except that it has
+one closed free variable, namely ``f``. Similarly ``h`` is closed, *even
+though it is not bound at top level*, because its only free variable
+``f`` is closed. But ``k`` is not closed, because it mentions ``x``
+which is not closed (because it is not letbound).
Type inference
~~~~~~~~~~~~~~
+Notice that a toplevel binding that is affected by the monomorphism
+restriction is not closed, and hence may in turn prevent generalisation
+of bindings that mention it.
In general, type inference for arbitraryrank types is undecidable. GHC
uses an algorithm proposed by Odersky and Laufer ("Putting type
annotations to work", POPL'96) to get a decidable algorithm by requiring
some help from the programmer. We do not yet have a formal specification
of "some help" but the rule is this:
+The rationale for this more conservative strategy is given in `the
+papers `__
+"Let should not be generalised" and "Modular type inference with local
+assumptions", and a related `blog post `__.
 For a lambdabound or casebound variable, x, either the programmer
 provides an explicit polymorphic type for x, or GHC's type inference
 will assume that x's type has no foralls in it.
+The flag :ghcflag:`XMonoLocalBinds` is implied by :ghcflag:`XTypeFamilies`
+and :ghcflag:`XGADTs`. You can switch it off again with
+:ghcflag:`XNoMonoLocalBinds <XMonoLocalBinds>` but type inference becomes
+less predicatable if you do so. (Read the papers!)
What does it mean to "provide" an explicit type for x? You can do that
by giving a type signature for x directly, using a pattern type
signature (:ref:`scopedtypevariables`), thus: ::
+.. _implicitparameters:
 \ f :: (forall a. a>a) > (f True, f 'c')
+Implicit parameters
+===================
Alternatively, you can give a type signature to the enclosing context,
which GHC can "push down" to find the type for the variable: ::
+.. ghcflag:: XImplicitParams
 (\ f > (f True, f 'c')) :: (forall a. a>a) > (Bool,Char)
+ Allow definition of functions expecting implicit parameters.
Here the type signature on the expression can be pushed inwards to give
a type signature for f. Similarly, and more commonly, one can give a
type signature for the function itself: ::
+Implicit parameters are implemented as described in [Lewis2000]_ and enabled
+with the option :ghcflag:`XImplicitParams`. (Most of the following, still rather
+incomplete, documentation is due to Jeff Lewis.)
 h :: (forall a. a>a) > (Bool,Char)
 h f = (f True, f 'c')
+.. [Lewis2000]
+ "Implicit parameters: dynamic scoping with static types",
+ J Lewis, MB Shields, E Meijer, J Launchbury,
+ *27th ACM Symposium on Principles of Programming Languages (POPL'00)*,
+ Boston, Jan 2000.
You don't need to give a type signature if the lambda bound variable is
a constructor argument. Here is an example we saw earlier: ::
+A variable is called *dynamically bound* when it is bound by the calling
+context of a function and *statically bound* when bound by the callee's
+context. In Haskell, all variables are statically bound. Dynamic binding
+of variables is a notion that goes back to Lisp, but was later discarded
+in more modern incarnations, such as Scheme. Dynamic binding can be very
+confusing in an untyped language, and unfortunately, typed languages, in
+particular HindleyMilner typed languages like Haskell, only support
+static scoping of variables.
 f :: T a > a > (a, Char)
 f (T1 w k) x = (w k x, w 'c' 'd')
+However, by a simple extension to the type class system of Haskell, we
+can support dynamic binding. Basically, we express the use of a
+dynamically bound variable as a constraint on the type. These
+constraints lead to types of the form ``(?x::t') => t``, which says
+"this function uses a dynamicallybound variable ``?x`` of type ``t'``".
+For example, the following expresses the type of a sort function,
+implicitly parameterised by a comparison function named ``cmp``. ::
Here we do not need to give a type signature to ``w``, because it is an
argument of constructor ``T1`` and that tells GHC all it needs to know.
+ sort :: (?cmp :: a > a > Bool) => [a] > [a]
+The dynamic binding constraints are just a new form of predicate in the
+type class system.
.. _implicitquant:
+An implicit parameter occurs in an expression using the special form
+``?x``, where ``x`` is any valid identifier (e.g. ``ord ?x`` is a valid
+expression). Use of this construct also introduces a new dynamicbinding
+constraint in the type of the expression. For example, the following
+definition shows how we can define an implicitly parameterised sort
+function in terms of an explicitly parameterised ``sortBy`` function: ::
Implicit quantification
~~~~~~~~~~~~~~~~~~~~~~~
+ sortBy :: (a > a > Bool) > [a] > [a]
GHC performs implicit quantification as follows. At the top level
(only) of userwritten types, if and only if there is no explicit
``forall``, GHC finds all the type variables mentioned in the type that
are not already in scope, and universally quantifies them. For example,
the following pairs are equivalent: ::
+ sort :: (?cmp :: a > a > Bool) => [a] > [a]
+ sort = sortBy ?cmp
 f :: a > a
 f :: forall a. a > a
+Implicitparameter type constraints
+
 g (x::a) = let
 h :: a > b > b
 h x y = y
 in ...
 g (x::a) = let
 h :: forall b. a > b > b
 h x y = y
 in ...
+Dynamic binding constraints behave just like other type class
+constraints in that they are automatically propagated. Thus, when a
+function is used, its implicit parameters are inherited by the function
+that called it. For example, our ``sort`` function might be used to pick
+out the least value in a list: ::
Notice that GHC does *not* find the innermost possible quantification
point. For example: ::
+ least :: (?cmp :: a > a > Bool) => [a] > a
+ least xs = head (sort xs)
 f :: (a > a) > Int
  MEANS
 f :: forall a. (a > a) > Int
  NOT
 f :: (forall a. a > a) > Int
+Without lifting a finger, the ``?cmp`` parameter is propagated to become
+a parameter of ``least`` as well. With explicit parameters, the default
+is that parameters must always be explicit propagated. With implicit
+parameters, the default is to always propagate them.
+An implicitparameter type constraint differs from other type class
+constraints in the following way: All uses of a particular implicit
+parameter must have the same type. This means that the type of
+``(?x, ?x)`` is ``(?x::a) => (a,a)``, and not
+``(?x::a, ?x::b) => (a, b)``, as would be the case for type class
+constraints.
 g :: (Ord a => a > a) > Int
  MEANS the illegal type
 g :: forall a. (Ord a => a > a) > Int
  NOT
 g :: (forall a. Ord a => a > a) > Int
+You can't have an implicit parameter in the context of a class or
+instance declaration. For example, both these declarations are illegal: ::
The latter produces an illegal type, which you might think is silly, but
at least the rule is simple. If you want the latter type, you can write
your ``forall``\s explicitly. Indeed, doing so is strongly advised for
rank2 types.
+ class (?x::Int) => C a where ...
+ instance (?x::a) => Foo [a] where ...
.. _impredicativepolymorphism:
+Reason: exactly which implicit parameter you pick up depends on exactly
+where you invoke a function. But the "invocation" of instance
+declarations is done behind the scenes by the compiler, so it's hard to
+figure out exactly where it is done. Easiest thing is to outlaw the
+offending types.
Impredicative polymorphism

+Implicitparameter constraints do not cause ambiguity. For example,
+consider: ::
.. ghcflag:: XImpredicativeTypes
+ f :: (?x :: [a]) => Int > Int
+ f n = n + length ?x
 :implies: :ghcflag:`RankNTypes`
+ g :: (Read a, Show a) => String > String
+ g s = show (read s)
 Allow impredicative polymorphic types.
+Here, ``g`` has an ambiguous type, and is rejected, but ``f`` is fine.
+The binding for ``?x`` at ``f``\ 's call site is quite unambiguous, and
+fixes the type ``a``.
In general, GHC will only instantiate a polymorphic function at a
monomorphic type (one with no foralls). For example, ::
+Implicitparameter bindings
+
 runST :: (forall s. ST s a) > a
 id :: forall b. b > b
+An implicit parameter is *bound* using the standard ``let`` or ``where``
+binding forms. For example, we define the ``min`` function by binding
+``cmp``. ::
 foo = id runST  Rejected
+ min :: Ord a => [a] > a
+ min = let ?cmp = (<=) in least
The definition of ``foo`` is rejected because one would have to
instantiate ``id``\'s type with ``b := (forall s. ST s a) > a``, and
that is not allowed. Instantiating polymorphic type variables with
polymorphic types is called *impredicative polymorphism*.
+A group of implicitparameter bindings may occur anywhere a normal group
+of Haskell bindings can occur, except at top level. That is, they can
+occur in a ``let`` (including in a list comprehension, or donotation,
+or pattern guards), or a ``where`` clause. Note the following points:
GHC has extremely flaky support for *impredicative polymorphism*,
enabled with :ghcflag:`XImpredicativeTypes`. If it worked, this would mean
that you *could* call a polymorphic function at a polymorphic type, and
parameterise data structures over polymorphic types. For example: ::
+ An implicitparameter binding group must be a collection of simple
+ bindings to implicitstyle variables (no functionstyle bindings, and
+ no type signatures); these bindings are neither polymorphic or
+ recursive.
 f :: Maybe (forall a. [a] > [a]) > Maybe ([Int], [Char])
 f (Just g) = Just (g [3], g "hello")
 f Nothing = Nothing
+ You may not mix implicitparameter bindings with ordinary bindings in
+ a single ``let`` expression; use two nested ``let``\ s instead. (In
+ the case of ``where`` you are stuck, since you can't nest ``where``
+ clauses.)
Notice here that the ``Maybe`` type is parameterised by the
*polymorphic* type ``(forall a. [a] > [a])``. However *the extension
should be considered highly experimental, and certainly unsupported*.
You are welcome to try it, but please don't rely on it working
consistently, or working the same in subsequent releases. See
:ghcwiki:`this wiki page ` for more details.
+ You may put multiple implicitparameter bindings in a single binding
+ group; but they are *not* treated as a mutually recursive group (as
+ ordinary ``let`` bindings are). Instead they are treated as a
+ nonrecursive group, simultaneously binding all the implicit
+ parameter. The bindings are not nested, and may be reordered without
+ changing the meaning of the program. For example, consider: ::
If you want impredicative polymorphism, the main workaround is to use a
newtype wrapper. The ``id runST`` example can be written using theis
workaround like this: ::
+ f t = let { ?x = t; ?y = ?x+(1::Int) } in ?x + ?y
 runST :: (forall s. ST s a) > a
 id :: forall b. b > b
+ The use of ``?x`` in the binding for ``?y`` does not "see" the
+ binding for ``?x``, so the type of ``f`` is ::
 nwetype Wrap a = Wrap { unWrap :: (forall s. ST s a) > a }
+ f :: (?x::Int) => Int > Int
 foo :: (forall s. ST s a) > a
 foo = unWrap (id (Wrap runST))
  Here id is called at monomorphic type (Wrap a)
+Implicit parameters and polymorphic recursion
+
.. _scopedtypevariables:
+Consider these two definitions: ::
Lexically scoped type variables

+ len1 :: [a] > Int
+ len1 xs = let ?acc = 0 in len_acc1 xs
.. ghcflag:: XScopedTypeVariables
+ len_acc1 [] = ?acc
+ len_acc1 (x:xs) = let ?acc = ?acc + (1::Int) in len_acc1 xs
 :implies: :ghcflag:`XRelaxedPolyRec`
 :implies: :ghcflag:`XExplicitForAll`
+ 
 Enable lexical scoping of type variables explicitly introduced with
 ``forall``.
+ len2 :: [a] > Int
+ len2 xs = let ?acc = 0 in len_acc2 xs
GHC supports *lexically scoped type variables*, without which some type
signatures are simply impossible to write. For example: ::
+ len_acc2 :: (?acc :: Int) => [a] > Int
+ len_acc2 [] = ?acc
+ len_acc2 (x:xs) = let ?acc = ?acc + (1::Int) in len_acc2 xs
 f :: forall a. [a] > [a]
 f xs = ys ++ ys
 where
 ys :: [a]
 ys = reverse xs
+The only difference between the two groups is that in the second group
+``len_acc`` is given a type signature. In the former case, ``len_acc1``
+is monomorphic in its own righthand side, so the implicit parameter
+``?acc`` is not passed to the recursive call. In the latter case,
+because ``len_acc2`` has a type signature, the recursive call is made to
+the *polymorphic* version, which takes ``?acc`` as an implicit
+parameter. So we get the following results in GHCi:
The type signature for ``f`` brings the type variable ``a`` into scope,
because of the explicit ``forall`` (:ref:`decltypesigs`). The type
variables bound by a ``forall`` scope over the entire definition of the
accompanying value declaration. In this example, the type variable ``a``
scopes over the whole definition of ``f``, including over the type
signature for ``ys``. In Haskell 98 it is not possible to declare a type
for ``ys``; a major benefit of scoped type variables is that it becomes
possible to do so.
+.. codeblock:: none
Lexicallyscoped type variables are enabled by
:ghcflag:`XScopedTypeVariables`. This flag implies :ghcflag:`XRelaxedPolyRec`.
+ Prog> len1 "hello"
+ 0
+ Prog> len2 "hello"
+ 5
Overview
~~~~~~~~
+Adding a type signature dramatically changes the result! This is a
+rather counterintuitive phenomenon, worth watching out for.
The design follows the following principles
+Implicit parameters and monomorphism
+
 A scoped type variable stands for a type *variable*, and not for a
 *type*. (This is a change from GHC's earlier design.)
+GHC applies the dreaded Monomorphism Restriction (section 4.5.5 of the
+Haskell Report) to implicit parameters. For example, consider: ::
 Furthermore, distinct lexical type variables stand for distinct type
 variables. This means that every programmerwritten type signature
 (including one that contains free scoped type variables) denotes a
 *rigid* type; that is, the type is fully known to the type checker,
 and no inference is involved.
+ f :: Int > Int
+ f v = let ?x = 0 in
+ let y = ?x + v in
+ let ?x = 5 in
+ y
 Lexical type variables may be alpharenamed freely, without changing
 the program.
+Since the binding for ``y`` falls under the Monomorphism Restriction it
+is not generalised, so the type of ``y`` is simply ``Int``, not
+``(?x::Int) => Int``. Hence, ``(f 9)`` returns result ``9``. If you add
+a type signature for ``y``, then ``y`` will get type
+``(?x::Int) => Int``, so the occurrence of ``y`` in the body of the
+``let`` will see the inner binding of ``?x``, so ``(f 9)`` will return
+``14``.
A *lexically scoped type variable* can be bound by:
+Arbitraryrank polymorphism
+===========================
 A declaration type signature (:ref:`decltypesigs`)
+.. ghcflag:: XRankNTypes
 An expression type signature (:ref:`exptypesigs`)
 A pattern type signature (:ref:`patterntypesigs`)
+ :implies: :ghcflag:`XExplicitForAll`
 Class and instance declarations (:ref:`clsinstscopedtyvars`)
+ Allow types of arbitrary rank.
In Haskell, a programmerwritten type signature is implicitly quantified
over its free type variables (`Section
4.1.2 `__ of
the Haskell Report). Lexically scoped type variables affect this
implicit quantification rules as follows: any type variable that is in
scope is *not* universally quantified. For example, if type variable
``a`` is in scope, then ::
+.. ghcflag:: XRank2Types
 (e :: a > a) means (e :: a > a)
 (e :: b > b) means (e :: forall b. b>b)
 (e :: a > b) means (e :: forall b. a>b)
+ A deprecated alias of :ghcflag:`XRankNTypes`.
.. _decltypesigs:
+GHC's type system supports *arbitraryrank* explicit universal
+quantification in types. For example, all the following types are legal: ::
Declaration type signatures
~~~~~~~~~~~~~~~~~~~~~~~~~~~
+ f1 :: forall a b. a > b > a
+ g1 :: forall a b. (Ord a, Eq b) => a > b > a
A declaration type signature that has *explicit* quantification (using
``forall``) brings into scope the explicitlyquantified type variables,
in the definition of the named function. For example: ::
+ f2 :: (forall a. a>a) > Int > Int
+ g2 :: (forall a. Eq a => [a] > a > Bool) > Int > Int
 f :: forall a. [a] > [a]
 f (x:xs) = xs ++ [ x :: a ]
+ f3 :: ((forall a. a>a) > Int) > Bool > Bool
The "``forall a``" brings "``a``" into scope in the definition of
"``f``".
+ f4 :: Int > (forall a. a > a)
This only happens if:
+Here, ``f1`` and ``g1`` are rank1 types, and can be written in standard
+Haskell (e.g. ``f1 :: a>b>a``). The ``forall`` makes explicit the
+universal quantification that is implicitly added by Haskell.
 The quantification in ``f``\'s type signature is explicit. For
 example: ::
+The functions ``f2`` and ``g2`` have rank2 types; the ``forall`` is on
+the left of a function arrow. As ``g2`` shows, the polymorphic type on
+the left of the function arrow can be overloaded.
 g :: [a] > [a]
 g (x:xs) = xs ++ [ x :: a ]
+The function ``f3`` has a rank3 type; it has rank2 types on the left
+of a function arrow.
 This program will be rejected, because "``a``" does not scope over
 the definition of "``g``", so "``x::a``" means "``x::forall a. a``"
 by Haskell's usual implicit quantification rules.
+The language option :ghcflag:`XRankNTypes` (which implies
+:ghcflag:`XExplicitForAll`) enables higherrank
+types. That is, you can nest ``forall``\ s arbitrarily deep in function
+arrows. For example, a foralltype (also called a "type scheme"),
+including a typeclass context, is legal:
 The signature gives a type for a function binding or a bare variable
 binding, not a pattern binding. For example: ::
+ On the left or right (see ``f4``, for example) of a function arrow
 f1 :: forall a. [a] > [a]
 f1 (x:xs) = xs ++ [ x :: a ]  OK
+ As the argument of a constructor, or type of a field, in a data type
+ declaration. For example, any of the ``f1, f2, f3, g1, g2`` above would
+ be valid field type signatures.
 f2 :: forall a. [a] > [a]
 f2 = \(x:xs) > xs ++ [ x :: a ]  OK
+ As the type of an implicit parameter
 f3 :: forall a. [a] > [a]
 Just f3 = Just (\(x:xs) > xs ++ [ x :: a ])  Not OK!
+ In a pattern type signature (see :ref:`scopedtypevariables`)
 The binding for ``f3`` is a pattern binding, and so its type
 signature does not bring ``a`` into scope. However ``f1`` is a
 function binding, and ``f2`` binds a bare variable; in both cases the
 type signature brings ``a`` into scope.
+The :ghcflag:`XRankNTypes` option is also required for any type with a
+``forall`` or context to the right of an arrow (e.g.
+``f :: Int > forall a. a>a``, or ``g :: Int > Ord a => a > a``).
+Such types are technically rank 1, but are clearly not Haskell98, and
+an extra flag did not seem worth the bother.
.. _exptypesigs:
+In particular, in ``data`` and ``newtype`` declarations the constructor
+arguments may be polymorphic types of any rank; see examples in
+:ref:`univ`. Note that the declared types are nevertheless always
+monomorphic. This is important because by default GHC will not
+instantiate type variables to a polymorphic type
+(:ref:`impredicativepolymorphism`).
Expression type signatures
~~~~~~~~~~~~~~~~~~~~~~~~~~
+The obsolete language options :ghcflag:`XPolymorphicComponents` and
+:ghcflag:`XRank2Types` are synonyms for :ghcflag:`XRankNTypes`. They used to
+specify finer distinctions that GHC no longer makes. (They should really elicit
+a deprecation warning, but they don't, purely to avoid the need to library
+authors to change their old flags specifications.)
An expression type signature that has *explicit* quantification (using
``forall``) brings into scope the explicitlyquantified type variables,
in the annotated expression. For example: ::
+.. _univ:
 f = runST ( (op >>= \(x :: STRef s Int) > g x) :: forall s. ST s Bool )
+Examples
+
Here, the type signature ``forall s. ST s Bool`` brings the type
variable ``s`` into scope, in the annotated expression
``(op >>= \(x :: STRef s Int) > g x)``.
+These are examples of ``data`` and ``newtype`` declarations whose data
+constructors have polymorphic argument types: ::
.. _patterntypesigs:
+ data T a = T1 (forall b. b > b > b) a
Pattern type signatures
~~~~~~~~~~~~~~~~~~~~~~~
+ data MonadT m = MkMonad { return :: forall a. a > m a,
+ bind :: forall a b. m a > (a > m b) > m b
+ }
A type signature may occur in any pattern; this is a *pattern type
signature*. For example: ::
+ newtype Swizzle = MkSwizzle (forall a. Ord a => [a] > [a])
  f and g assume that 'a' is already in scope
 f = \(x::Int, y::a) > x
+The constructors have rank2 types: ::
 g (x::a) = x
+ T1 :: forall a. (forall b. b > b > b) > a > T a
 h ((x,y) :: (Int,Bool)) = (y,x)
+ MkMonad :: forall m. (forall a. a > m a)
+ > (forall a b. m a > (a > m b) > m b)
+ > MonadT m
In the case where all the type variables in the pattern type signature
are already in scope (i.e. bound by the enclosing context), matters are
simple: the signature simply constrains the type of the pattern in the
obvious way.
+ MkSwizzle :: (forall a. Ord a => [a] > [a]) > Swizzle
Unlike expression and declaration type signatures, pattern type
signatures are not implicitly generalised. The pattern in a *pattern
binding* may only mention type variables that are already in scope. For
+In earlier versions of GHC, it was possible to omit the ``forall`` in
+the type of the constructor if there was an explicit context. For
example: ::
 f :: forall a. [a] > (Int, [a])
 f xs = (n, zs)
 where
 (ys::[a], n) = (reverse xs, length xs)  OK
 zs::[a] = xs ++ ys  OK
+ newtype Swizzle' = MkSwizzle' (Ord a => [a] > [a])
 Just (v::b) = ...  Not OK; b is not in scope
+As of GHC 7.10, this is deprecated. The
+:ghcflag:`Wcontextquantification` flag detects this situation and issues
+a warning. In GHC 8.0 this flag was deprecated and declarations such as
+``MkSwizzle'`` will cause an outofscope error.
Here, the pattern signatures for ``ys`` and ``zs`` are fine, but the one
for ``v`` is not because ``b`` is not in scope.
+As for type signatures, implicit quantification happens for
+nonoverloaded types too. So if you write this: ::
However, in all patterns *other* than pattern bindings, a pattern type
signature may mention a type variable that is not in scope; in this
case, *the signature brings that type variable into scope*. This is
particularly important for existential data constructors. For example: ::
+ f :: (a > a) > a
 data T = forall a. MkT [a]
+it's just as if you had written this: ::
 k :: T > T
 k (MkT [t::a]) =
 MkT t3
 where
 t3::[a] = [t,t,t]
+ f :: forall a. (a > a) > a
Here, the pattern type signature ``(t::a)`` mentions a lexical type
variable that is not already in scope. Indeed, it *cannot* already be in
scope, because it is bound by the pattern match. GHC's rule is that in
this situation (and only then), a pattern type signature can mention a
type variable that is not already in scope; the effect is to bring it
into scope, standing for the existentiallybound type variable.
+That is, since the type variable ``a`` isn't in scope, it's implicitly
+universally quantified.
+
+You construct values of types ``T1, MonadT, Swizzle`` by applying the
+constructor to suitable values, just as usual. For example, ::
When a pattern type signature binds a type variable in this way, GHC
insists that the type variable is bound to a *rigid*, or fullyknown,
type variable. This means that any userwritten type signature always
stands for a completely known type.
+ a1 :: T Int
+ a1 = T1 (\xy>x) 3
If all this seems a little odd, we think so too. But we must have *some*
way to bring such type variables into scope, else we could not name
existentiallybound type variables in subsequent type signatures.
+ a2, a3 :: Swizzle
+ a2 = MkSwizzle sort
+ a3 = MkSwizzle reverse
This is (now) the *only* situation in which a pattern type signature is
allowed to mention a lexical variable that is not already in scope. For
example, both ``f`` and ``g`` would be illegal if ``a`` was not already
in scope.
+ a4 :: MonadT Maybe
+ a4 = let r x = Just x
+ b m k = case m of
+ Just y > k y
+ Nothing > Nothing
+ in
+ MkMonad r b
.. _clsinstscopedtyvars:
+ mkTs :: (forall b. b > b > b) > a > [T a]
+ mkTs f x y = [T1 f x, T1 f y]
Class and instance declarations
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The type of the argument can, as usual, be more general than the type
+required, as ``(MkSwizzle reverse)`` shows. (``reverse`` does not need
+the ``Ord`` constraint.)
The type variables in the head of a ``class`` or ``instance``
declaration scope over the methods defined in the ``where`` part. You do
not even need an explicit ``forall``. For example: ::
+When you use pattern matching, the bound variables may now have
+polymorphic types. For example: ::
 class C a where
 op :: [a] > a
+ f :: T a > a > (a, Char)
+ f (T1 w k) x = (w k x, w 'c' 'd')
 op xs = let ys::[a]
 ys = reverse xs
 in
 head ys
+ g :: (Ord a, Ord b) => Swizzle > [a] > (a > b) > [b]
+ g (MkSwizzle s) xs f = s (map f (s xs))
 instance C b => C [b] where
 op xs = reverse (head (xs :: [[b]]))
+ h :: MonadT m > [m a] > m [a]
+ h m [] = return m []
+ h m (x:xs) = bind m x $ \y >
+ bind m (h m xs) $ \ys >
+ return m (y:ys)
Bindings and generalisation

+In the function ``h`` we use the record selectors ``return`` and
+``bind`` to extract the polymorphic bind and return functions from the
+``MonadT`` data structure, rather than using pattern matching.
.. _monomorphism:
Switching off the dreaded Monomorphism Restriction
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+.. _higherranktypeinference:
.. ghcflag:: XNoMonomorphismRestriction
+Type inference
+
 :default: on
+In general, type inference for arbitraryrank types is undecidable. GHC
+uses an algorithm proposed by Odersky and Laufer ("Putting type
+annotations to work", POPL'96) to get a decidable algorithm by requiring
+some help from the programmer. We do not yet have a formal specification
+of "some help" but the rule is this:
 Prevents the compiler from applying the monomorphism restriction to
 bindings lacking explicit type signatures.
+ For a lambdabound or casebound variable, x, either the programmer
+ provides an explicit polymorphic type for x, or GHC's type inference
+ will assume that x's type has no foralls in it.
Haskell's monomorphism restriction (see `Section
4.5.5 `__ of
the Haskell Report) can be completely switched off by
:ghcflag:`XNoMonomorphismRestriction`. Since GHC 7.8.1, the monomorphism
restriction is switched off by default in GHCi's interactive options
(see :ref:`ghciinteractiveoptions`).
+What does it mean to "provide" an explicit type for x? You can do that
+by giving a type signature for x directly, using a pattern type
+signature (:ref:`scopedtypevariables`), thus: ::
.. _typingbinds:
+ \ f :: (forall a. a>a) > (f True, f 'c')
Generalised typing of mutually recursive bindings
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Alternatively, you can give a type signature to the enclosing context,
+which GHC can "push down" to find the type for the variable: ::
.. ghcflag:: XRelaxedPolyRec
+ (\ f > (f True, f 'c')) :: (forall a. a>a) > (Bool,Char)
 Allow the typechecker to ignore references to bindings with
 explicit type signatures.
+Here the type signature on the expression can be pushed inwards to give
+a type signature for f. Similarly, and more commonly, one can give a
+type signature for the function itself: ::
The Haskell Report specifies that a group of bindings (at top level, or
in a ``let`` or ``where``) should be sorted into stronglyconnected
components, and then typechecked in dependency order
(`Haskell Report, Section
4.5.1 `__). As
each group is typechecked, any binders of the group that have an
explicit type signature are put in the type environment with the
specified polymorphic type, and all others are monomorphic until the
group is generalised (`Haskell Report, Section
4.5.2 `__).
+ h :: (forall a. a>a) > (Bool,Char)
+ h f = (f True, f 'c')
Following a suggestion of Mark Jones, in his paper `Typing Haskell in
Haskell `__, GHC implements a
more general scheme. If :ghcflag:`XRelaxedPolyRec` is specified: *the
dependency analysis ignores references to variables that have an
explicit type signature*. As a result of this refined dependency
analysis, the dependency groups are smaller, and more bindings will
typecheck. For example, consider: ::
+You don't need to give a type signature if the lambda bound variable is
+a constructor argument. Here is an example we saw earlier: ::
 f :: Eq a => a > Bool
 f x = (x == x)  g True  g "Yes"
+ f :: T a > a > (a, Char)
+ f (T1 w k) x = (w k x, w 'c' 'd')
 g y = (y <= y)  f True
+Here we do not need to give a type signature to ``w``, because it is an
+argument of constructor ``T1`` and that tells GHC all it needs to know.
This is rejected by Haskell 98, but under Jones's scheme the definition
for ``g`` is typechecked first, separately from that for ``f``, because
the reference to ``f`` in ``g``\'s right hand side is ignored by the
dependency analysis. Then ``g``\'s type is generalised, to get ::
 g :: Ord a => a > Bool
+.. _implicitquant:
Now, the definition for ``f`` is typechecked, with this type for ``g``
in the type environment.
+Implicit quantification
+
The same refined dependency analysis also allows the type signatures of
mutuallyrecursive functions to have different contexts, something that
is illegal in Haskell 98 (Section 4.5.2, last sentence). With
:ghcflag:`XRelaxedPolyRec` GHC only insists that the type signatures of a
*refined* group have identical type signatures; in practice this means
that only variables bound by the same pattern binding must have the same
context. For example, this is fine: ::
+GHC performs implicit quantification as follows. At the top level
+(only) of userwritten types, if and only if there is no explicit
+``forall``, GHC finds all the type variables mentioned in the type that
+are not already in scope, and universally quantifies them. For example,
+the following pairs are equivalent: ::
 f :: Eq a => a > Bool
 f x = (x == x)  g True
+ f :: a > a
+ f :: forall a. a > a
 g :: Ord a => a > Bool
 g y = (y <= y)  f True
+ g (x::a) = let
+ h :: a > b > b
+ h x y = y
+ in ...
+ g (x::a) = let
+ h :: forall b. a > b > b
+ h x y = y
+ in ...
.. _monolocalbinds:
+Notice that GHC does *not* find the innermost possible quantification
+point. For example: ::
Letgeneralisation
~~~~~~~~~~~~~~~~~~
+ f :: (a > a) > Int
+  MEANS
+ f :: forall a. (a > a) > Int
+  NOT
+ f :: (forall a. a > a) > Int
.. ghcflag:: XMonoLocalBinds
 Infer less polymorphic types for local bindings by default.
+ g :: (Ord a => a > a) > Int
+  MEANS the illegal type
+ g :: forall a. (Ord a => a > a) > Int
+  NOT
+ g :: (forall a. Ord a => a > a) > Int
An MLstyle language usually generalises the type of any ``let``\bound or
``where``\bound variable, so that it is as polymorphic as possible. With the
flag :ghcflag:`XMonoLocalBinds` GHC implements a slightly more conservative
policy, using the following rules:
+The latter produces an illegal type, which you might think is silly, but
+at least the rule is simple. If you want the latter type, you can write
+your ``forall``\s explicitly. Indeed, doing so is strongly advised for
+rank2 types.
 A variable is *closed* if and only if
+.. _impredicativepolymorphism:
  the variable is letbound
+Impredicative polymorphism
+==========================
  one of the following holds:
+.. ghcflag:: XImpredicativeTypes
  the variable has an explicit type signature that has no free
 type variables, or
+ :implies: :ghcflag:`RankNTypes`
  its binding group is fully generalised (see next bullet)
+ Allow impredicative polymorphic types.
 A binding group is *fully generalised* if and only if
+In general, GHC will only instantiate a polymorphic function at a
+monomorphic type (one with no foralls). For example, ::
  each of its free variables is either imported or closed, and
+ runST :: (forall s. ST s a) > a
+ id :: forall b. b > b
  the binding is not affected by the monomorphism restriction
 (`Haskell Report, Section
 4.5.5 `__)
+ foo = id runST  Rejected
For example, consider ::
+The definition of ``foo`` is rejected because one would have to
+instantiate ``id``\'s type with ``b := (forall s. ST s a) > a``, and
+that is not allowed. Instantiating polymorphic type variables with
+polymorphic types is called *impredicative polymorphism*.
 f x = x + 1
 g x = let h y = f y * 2
 k z = z+x
 in h x + k x
+GHC has extremely flaky support for *impredicative polymorphism*,
+enabled with :ghcflag:`XImpredicativeTypes`. If it worked, this would mean
+that you *could* call a polymorphic function at a polymorphic type, and
+parameterise data structures over polymorphic types. For example: ::
Here ``f`` is generalised because it has no free variables; and its
binding group is unaffected by the monomorphism restriction; and hence
``f`` is closed. The same reasoning applies to ``g``, except that it has
one closed free variable, namely ``f``. Similarly ``h`` is closed, *even
though it is not bound at top level*, because its only free variable
``f`` is closed. But ``k`` is not closed, because it mentions ``x``
which is not closed (because it is not letbound).
+ f :: Maybe (forall a. [a] > [a]) > Maybe ([Int], [Char])
+ f (Just g) = Just (g [3], g "hello")
+ f Nothing = Nothing
Notice that a toplevel binding that is affected by the monomorphism
restriction is not closed, and hence may in turn prevent generalisation
of bindings that mention it.
+Notice here that the ``Maybe`` type is parameterised by the
+*polymorphic* type ``(forall a. [a] > [a])``. However *the extension
+should be considered highly experimental, and certainly unsupported*.
+You are welcome to try it, but please don't rely on it working
+consistently, or working the same in subsequent releases. See
+:ghcwiki:`this wiki page ` for more details.
The rationale for this more conservative strategy is given in `the
papers `__
"Let should not be generalised" and "Modular type inference with local
assumptions", and a related `blog post `__.
+If you want impredicative polymorphism, the main workaround is to use a
+newtype wrapper. The ``id runST`` example can be written using theis
+workaround like this: ::
The flag :ghcflag:`XMonoLocalBinds` is implied by :ghcflag:`XTypeFamilies`
and :ghcflag:`XGADTs`. You can switch it off again with
:ghcflag:`XNoMonoLocalBinds <XMonoLocalBinds>` but type inference becomes
less predicatable if you do so. (Read the papers!)
+ runST :: (forall s. ST s a) > a
+ id :: forall b. b > b
+
+ nwetype Wrap a = Wrap { unWrap :: (forall s. ST s a) > a }
+
+ foo :: (forall s. ST s a) > a
+ foo = unWrap (id (Wrap runST))
+  Here id is called at monomorphic type (Wrap a)
.. _typedholes: