User documentation for DuplicateRecordFields
authorAdam Gundry <adam@well-typed.com>
Wed, 25 Nov 2015 23:28:32 +0000 (00:28 +0100)
committerBen Gamari <ben@smart-cactus.org>
Wed, 25 Nov 2015 23:28:33 +0000 (00:28 +0100)
This is a first draft of the user manual documentation for
DuplicateRecordFields. Feedback welcome. I've intentionally made this a
minimal change, but I wonder if it might make sense to pull out all the
subsections on record system extensions ("Traditional record syntax",
and "Record field disambiguation" through to "Record wildcards") into a
new section? That is, is it worth breaking down the rather monolithic
"Syntactic extensions" section?

Test Plan: n/a

Reviewers: simonpj, bgamari, austin

Reviewed By: bgamari, austin

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D1522

docs/users_guide/glasgow_exts.rst

index 725ed2b..424d4b6 100644 (file)
@@ -1107,17 +1107,6 @@ n+k patterns
 ``n+k`` pattern support is disabled by default. To enable it, you can
 use the ``-XNPlusKPatterns`` flag.
 
-.. _traditional-record-syntax:
-
-Traditional record syntax
--------------------------
-
-.. index::
-   single: -XNoTraditionalRecordSyntax
-
-Traditional record syntax, such as ``C {f = x}``, is enabled by default.
-To disable it, you can use the ``-XNoTraditionalRecordSyntax`` flag.
-
 .. _recursive-do-notation:
 
 The recursive do-notation
@@ -2101,250 +2090,6 @@ 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.
 
-.. _disambiguate-fields:
-
-Record field disambiguation
----------------------------
-
-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:
-
-::
-
-    module M where
-      data S = MkS { x :: Int, y :: Bool }
-
-    module Foo where
-      import M
-
-      data T = MkT { x :: Int }
-
-      ok1 (MkS { x = n }) = n+1   -- Unambiguous
-      ok2 n = MkT { x = n+1 }     -- Unambiguous
-
-      bad1 k = k { x = 3 }  -- Ambiguous
-      bad2 k = x k          -- Ambiguous
-
-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.
-
-Haskell 98 regards all four as ambiguous, but with the
-``-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 left-hand 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.
-
-Some details:
-
--  Field disambiguation can be combined with punning (see
-   :ref:`record-puns`). For example:
-
-   ::
-
-       module Foo where
-         import M
-         x=True
-         ok3 (MkS { x }) = x+1   -- Uses both disambiguation and punning
-
--  With ``-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:
-
-   ::
-
-       module Foo where
-         import qualified M    -- Note qualified
-
-         ok4 (M.MkS { x = n }) = n+1   -- Unambiguous
-
-   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).
-
-.. _record-puns:
-
-Record puns
------------
-
-Record puns are enabled by the flag ``-XNamedFieldPuns``.
-
-When using records, it is common to write a pattern that binds a
-variable with the same name as a record field, such as:
-
-::
-
-    data C = C {a :: Int}
-    f (C {a = a}) = a
-
-Record punning permits the variable name to be elided, so one can simply
-write
-
-::
-
-    f (C {a}) = a
-
-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``.
-
-Note that:
-
--  Record punning can also be used in an expression, writing, for
-   example,
-
-   ::
-
-       let a = 1 in C {a}
-
-   instead of
-
-   ::
-
-       let a = 1 in C {a = a}
-
-   The expansion is purely syntactic, so the expanded right-hand side
-   expression refers to the nearest enclosing variable that is spelled
-   the same as the field name.
-
--  Puns and other patterns can be mixed in the same record:
-
-   ::
-
-       data C = C {a :: Int, b :: Int}
-       f (C {a, b = 4}) = a
-
--  Puns can be used wherever record patterns occur (e.g. in ``let``
-   bindings or at the top-level).
-
--  A pun on a qualified field name is expanded by stripping off the
-   module qualifier. For example:
-
-   ::
-
-       f (C {M.a}) = a
-
-   means
-
-   ::
-
-       f (M.C {M.a = a}) = a
-
-   (This is useful if the field selector ``a`` for constructor ``M.C``
-   is only in scope in qualified form.)
-
-.. _record-wildcards:
-
-Record wildcards
-----------------
-
-Record wildcards are enabled by the flag ``-XRecordWildCards``. This
-flag implies ``-XDisambiguateRecordFields``.
-
-For records with many fields, it can be tiresome to write out each field
-individually in a record pattern, as in
-
-::
-
-    data C = C {a :: Int, b :: Int, c :: Int, d :: Int}
-    f (C {a = 1, b = b, c = c, d = d}) = b + c + d
-
-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
-
-::
-
-    f (C {a = 1, ..}) = b + c + d
-
-More details:
-
--  Record wildcards in patterns can be mixed with other patterns,
-   including puns (:ref:`record-puns`); 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 top-level. For example, the top-level binding
-
-   ::
-
-       C {a = 1, ..} = e
-
-   defines ``b``, ``c``, and ``d``.
-
--  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 {..}
-
-   in place of
-
-   ::
-
-       let {a = 1; b = 2; c = 3; d = 4} in C {a=a, b=b, c=c, d=d}
-
-   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.
-
--  Record wildcards may *not* be used in record *updates*. For example
-   this is illegal:
-
-   ::
-
-       f r = r { x = 3, .. }
-
--  For both pattern and expression wildcards, the "``..``" expands to
-   the missing *in-scope* record fields. Specifically the expansion of
-   "``C {..}``" includes ``f`` if and only if:
-
-   -  ``f`` is a record field of constructor ``C``.
-
-   -  The record field ``f`` is in scope somehow (either qualified or
-      unqualified).
-
-   -  In the case of expressions (but not patterns), the variable ``f``
-      is in scope unqualified, apart from the binding of the record
-      selector itself.
-
-   These rules restrict record wildcards to the situations in which the
-   user could have written the expanded version. For example
-
-   ::
-
-       module M where
-         data R = R { a,b,c :: Int }
-       module X where
-         import M( R(a,c) )
-         f b = R { .. }
-
-   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).
-
--  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:
-
-   ::
-
-       f x = x { v=True, .. }   -- Illegal (a)
-
-       data T = MkT Int Bool
-       g = MkT { .. }           -- Illegal (b)
-       h (MkT { .. }) = True    -- Illegal (b)
-
 .. _local-fixity-declarations:
 
 Local Fixity Declarations
@@ -3308,230 +3053,643 @@ type declarations.
              If     :: Term Bool -> !(Term a) -> !(Term a) -> Term a
              Pair   :: Term a -> Term b -> Term (a,b)
 
--  You can use a ``deriving`` clause on a GADT-style data type
-   declaration. For example, these two declarations are equivalent
+-  You can use a ``deriving`` clause on a GADT-style data type
+   declaration. For example, these two declarations are equivalent
+
+   ::
+
+         data Maybe1 a where {
+             Nothing1 :: Maybe1 a ;
+             Just1    :: a -> Maybe1 a
+           } deriving( Eq, Ord )
+
+         data Maybe2 a = Nothing2 | Just2 a
+              deriving( Eq, Ord )
+
+-  The type signature may have quantified type variables that do not
+   appear in the result type:
+
+   ::
+
+         data Foo where
+            MkFoo :: a -> (a->Bool) -> Foo
+            Nil   :: Foo
+
+   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:`existential-quantification`.
+
+   The type may contain a class context too, of course:
+
+   ::
+
+         data Showable where
+           MkShowable :: Show a => a -> Showable
+
+-  You can use record syntax on a GADT-style data type declaration:
+
+   ::
+
+         data Person where
+             Adult :: { name :: String, children :: [Person] } -> Person
+             Child :: Show a => { name :: !String, funny :: a } -> Person
+
+   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,
+   existentially-quantified variables, and strictness annotations, just
+   as in the non-record case. (NB: the "type" that follows the
+   double-colon 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.)
+
+-  Record updates are allowed with GADT-style declarations, only fields
+   that have the following property: the type of the field mentions no
+   existential type variables.
+
+-  As in the case of existentials declared using the Haskell-98-like
+   record syntax (:ref:`existential-records`), record-selector functions
+   are generated only for those fields that have well-typed selectors.
+   Here is the example of that section, in GADT-style syntax:
+
+   ::
+
+       data Counter a where
+           NewCounter :: { _this    :: self
+                         , _inc     :: self -> self
+                         , _display :: self -> IO ()
+                         , tag      :: a
+                         } -> Counter a
+
+   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.
+
+-  In a GADT-style 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
+   GADT-style data type declaration is displayed infix by ``Show`` iff
+   (a) it is an operator symbol, (b) it has two arguments, (c) it has a
+   programmer-supplied fixity declaration. For example
+
+   ::
+
+          infix 6 (:--:)
+          data T a where
+            (:--:) :: Int -> Bool -> T Int
+
+.. _gadt:
+
+Generalised Algebraic Data Types (GADTs)
+----------------------------------------
+
+Generalised Algebraic Data Types generalise ordinary algebraic data
+types by allowing constructors to have richer return types. Here is an
+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)
+
+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 well-typed ``eval`` function for these ``Terms``:
+
+::
+
+      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)
+
+The key point about GADTs is that *pattern matching causes type
+refinement*. For example, in the right hand side of the equation
+
+::
+
+      eval :: Term a -> a
+      eval (Lit i) =  ...
+
+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
+unification-based type inference for
+GADTs <http://research.microsoft.com/%7Esimonpj/papers/gadt/>`__, (ICFP
+2006). The general principle is this: *type refinement is only carried
+out based on user-supplied 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:
+
+::
+
+      eval :: Term a -> a -> a
+      eval (Lit i) j =  i+j
+
+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.
+
+These and many other examples are given in papers by Hongwei Xi, and Tim
+Sheard. There is a longer introduction `on the
+wiki <http://www.haskell.org/haskellwiki/GADT>`__, and Ralf Hinze's `Fun
+with phantom
+types <http://www.cs.ox.ac.uk/ralf.hinze/publications/With.pdf>`__ also
+has a number of examples. Note that papers may use different notation to
+that implemented in GHC.
+
+The rest of this section outlines the extensions to GHC that support
+GADTs. The extension is enabled with ``-XGADTs``. The ``-XGADTs`` flag
+also sets ``-XGADTSyntax`` and ``-XMonoLocalBinds``.
+
+-  A GADT can only be declared using GADT-style syntax
+   (:ref:`gadt-style`); 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).
+
+-  It is permitted to declare an ordinary algebraic data type using
+   GADT-style 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``.
+
+-  You cannot use a ``deriving`` clause for a GADT; only for an ordinary
+   data type.
+
+-  As mentioned in :ref:`gadt-style`, record syntax is supported. For
+   example:
+
+   ::
+
+         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
+
+   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:
+
+   ::
+
+         num :: Term Int -> Term Int
+         arg :: Term Bool -> Term Int
+
+-  When pattern-matching against data constructors drawn from a GADT,
+   for example in a ``case`` expression, the following rules apply:
+
+   -  The type of the scrutinee must be rigid.
+
+   -  The type of the entire ``case`` expression must be rigid.
+
+   -  The type of any free variable mentioned in any of the ``case``
+      alternatives must be rigid.
+
+   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
+   unification-based type inference for
+   GADTs <http://research.microsoft.com/%7Esimonpj/papers/gadt>`__. The
+   criteria implemented by GHC are given in the Appendix.
+
+.. _record-system-extensions:
+
+Extensions to the record system
+===============================
+
+.. _traditional-record-syntax:
+
+Traditional record syntax
+-------------------------
+
+.. index::
+   single: -XNoTraditionalRecordSyntax
+
+Traditional record syntax, such as ``C {f = x}``, is enabled by default.
+To disable it, you can use the ``-XNoTraditionalRecordSyntax`` flag.
+
+.. _disambiguate-fields:
+
+Record field disambiguation
+---------------------------
+
+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:
+
+::
+
+    module M where
+      data S = MkS { x :: Int, y :: Bool }
+
+    module Foo where
+      import M
+
+      data T = MkT { x :: Int }
+
+      ok1 (MkS { x = n }) = n+1   -- Unambiguous
+      ok2 n = MkT { x = n+1 }     -- Unambiguous
+
+      bad1 k = k { x = 3 }  -- Ambiguous
+      bad2 k = x k          -- Ambiguous
+
+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.
+
+Haskell 98 regards all four as ambiguous, but with the
+``-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 left-hand 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.
+
+Some details:
+
+-  Field disambiguation can be combined with punning (see
+   :ref:`record-puns`). For example:
+
+   ::
+
+       module Foo where
+         import M
+         x=True
+         ok3 (MkS { x }) = x+1   -- Uses both disambiguation and punning
+
+-  With ``-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:
+
+   ::
+
+       module Foo where
+         import qualified M    -- Note qualified
+
+         ok4 (M.MkS { x = n }) = n+1   -- Unambiguous
+
+   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).
+
+.. _duplicate-record-fields:
+
+Duplicate record fields
+-----------------------
+
+Going beyond ``-XDisambiguateRecordFields`` (see :ref:`disambiguate-fields`),
+the ``-XDuplicateRecordFields`` extension allows multiple datatypes to be
+declared using the same field names in a single module. For example, it allows
+this:
+
+::
+
+    module M where
+      data S = MkS { x :: Int }
+      data T = MkT { x :: Bool }
+
+Uses of fields that are always unambiguous because they mention the constructor,
+including construction and pattern-matching, may freely use duplicated field
+names. For example, the following are permitted (just as with
+``-XDisambiguateRecordFields``):
+
+::
+
+    s = MkS { x = 3 }
+
+    f (MkT { x = b }) = b
+
+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.
+
+Selector functions
+~~~~~~~~~~~~~~~~~~
+
+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:
+
+::
+
+    bad r = x r
+
+An ambiguous selector may be disambiguated by the type being "pushed down" to
+the occurrence of the selector (see :ref:`higher-rank-type-inference` for more
+details on what "pushed down" means). For example, the following are permitted:
+
+::
+
+    ok1 = x :: S -> Int
+
+    ok2 :: S -> Int
+    ok2 = x
+
+    ok3 = k x -- assuming we already have k :: (S -> Int) -> _
+
+In addition, the datatype that is meant may be given as a type signature on the
+argument to the selector:
+
+::
+
+    ok4 s = x (s :: S)
+
+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:
+
+::
+
+    bad :: S -> Int
+    bad s = x s
+
+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.
+
+Record updates
+~~~~~~~~~~~~~~
+
+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:
+
+::
+
+    data S = MkS { foo :: Int }
+    data T = MkT { foo :: Int, bar :: Int }
+    data U = MkU { bar :: Int, baz :: Int }
+
+Without ``-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:
+
+- Check for types that have all the fields being updated. For example:
+
+  ::
+
+      f x = x { foo = 3, bar = 2 }
+
+  Here ``f`` must be updating ``T`` because neither ``S`` nor ``U`` have both
+  fields.
+
+- Use the type being pushed in to the record update, as in the following:
+
+  ::
+
+      g1 :: T -> T
+      g1 x = x { foo = 3 }
+
+      g2 x = x { foo = 3 } :: T
+
+      g3 = k (x { foo = 3 }) -- assuming we already have k :: T -> _
+
+- Use an explicit type signature on the record expression, as in:
+
+  ::
+
+      h x = (x :: T) { foo = 3 }
+
+The type of the expression being updated will not be inferred, and no
+constraint-solving will be performed, so the following will be rejected as
+ambiguous:
+
+::
+
+    let x :: T
+        x = blah
+    in x { foo = 3 }
+
+    \x -> [x { foo = 3 },  blah :: T ]
+
+    \ (x :: T) -> x { foo = 3 }
+
+Import and export of record fields
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+When ``-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:
+
+::
+
+    module M (S(x), T(..)) where
+      data S = MkS { x :: Int }
+      data T = MkT { x :: Bool }
+
+However, this would not be permitted, because ``x`` is ambiguous:
+
+::
+
+    module M (x) where ...
+
+Similar restrictions apply on import.
+
+.. _record-puns:
+
+Record puns
+-----------
+
+Record puns are enabled by the flag ``-XNamedFieldPuns``.
+
+When using records, it is common to write a pattern that binds a
+variable with the same name as a record field, such as:
+
+::
+
+    data C = C {a :: Int}
+    f (C {a = a}) = a
+
+Record punning permits the variable name to be elided, so one can simply
+write
+
+::
+
+    f (C {a}) = a
+
+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``.
+
+Note that:
+
+-  Record punning can also be used in an expression, writing, for
+   example,
 
    ::
 
-         data Maybe1 a where {
-             Nothing1 :: Maybe1 a ;
-             Just1    :: a -> Maybe1 a
-           } deriving( Eq, Ord )
-
-         data Maybe2 a = Nothing2 | Just2 a
-              deriving( Eq, Ord )
+       let a = 1 in C {a}
 
--  The type signature may have quantified type variables that do not
-   appear in the result type:
+   instead of
 
    ::
 
-         data Foo where
-            MkFoo :: a -> (a->Bool) -> Foo
-            Nil   :: Foo
+       let a = 1 in C {a = a}
 
-   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:`existential-quantification`.
+   The expansion is purely syntactic, so the expanded right-hand side
+   expression refers to the nearest enclosing variable that is spelled
+   the same as the field name.
 
-   The type may contain a class context too, of course:
+-  Puns and other patterns can be mixed in the same record:
 
    ::
 
-         data Showable where
-           MkShowable :: Show a => a -> Showable
-
--  You can use record syntax on a GADT-style data type declaration:
+       data C = C {a :: Int, b :: Int}
+       f (C {a, b = 4}) = a
 
-   ::
+-  Puns can be used wherever record patterns occur (e.g. in ``let``
+   bindings or at the top-level).
 
-         data Person where
-             Adult :: { name :: String, children :: [Person] } -> Person
-             Child :: Show a => { name :: !String, funny :: a } -> Person
+-  A pun on a qualified field name is expanded by stripping off the
+   module qualifier. For example:
 
-   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,
-   existentially-quantified variables, and strictness annotations, just
-   as in the non-record case. (NB: the "type" that follows the
-   double-colon 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.)
+   ::
 
--  Record updates are allowed with GADT-style declarations, only fields
-   that have the following property: the type of the field mentions no
-   existential type variables.
+       f (C {M.a}) = a
 
--  As in the case of existentials declared using the Haskell-98-like
-   record syntax (:ref:`existential-records`), record-selector functions
-   are generated only for those fields that have well-typed selectors.
-   Here is the example of that section, in GADT-style syntax:
+   means
 
    ::
 
-       data Counter a where
-           NewCounter :: { _this    :: self
-                         , _inc     :: self -> self
-                         , _display :: self -> IO ()
-                         , tag      :: a
-                         } -> Counter a
-
-   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.
-
--  In a GADT-style 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
-   GADT-style data type declaration is displayed infix by ``Show`` iff
-   (a) it is an operator symbol, (b) it has two arguments, (c) it has a
-   programmer-supplied fixity declaration. For example
+       f (M.C {M.a = a}) = a
 
-   ::
+   (This is useful if the field selector ``a`` for constructor ``M.C``
+   is only in scope in qualified form.)
 
-          infix 6 (:--:)
-          data T a where
-            (:--:) :: Int -> Bool -> T Int
+.. _record-wildcards:
 
-.. _gadt:
+Record wildcards
+----------------
 
-Generalised Algebraic Data Types (GADTs)
-----------------------------------------
+Record wildcards are enabled by the flag ``-XRecordWildCards``. This
+flag implies ``-XDisambiguateRecordFields``.
 
-Generalised Algebraic Data Types generalise ordinary algebraic data
-types by allowing constructors to have richer return types. Here is an
-example:
+For records with many fields, it can be tiresome to write out each field
+individually in a record pattern, as in
 
 ::
 
-      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 C = C {a :: Int, b :: Int, c :: Int, d :: Int}
+    f (C {a = 1, b = b, c = c, d = d}) = b + c + d
 
-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 well-typed ``eval`` function for these ``Terms``:
+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
 
 ::
 
-      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)
+    f (C {a = 1, ..}) = b + c + d
 
-The key point about GADTs is that *pattern matching causes type
-refinement*. For example, in the right hand side of the equation
+More details:
 
-::
+-  Record wildcards in patterns can be mixed with other patterns,
+   including puns (:ref:`record-puns`); 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 top-level. For example, the top-level binding
 
-      eval :: Term a -> a
-      eval (Lit i) =  ...
+   ::
 
-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
-unification-based type inference for
-GADTs <http://research.microsoft.com/%7Esimonpj/papers/gadt/>`__, (ICFP
-2006). The general principle is this: *type refinement is only carried
-out based on user-supplied 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:
+       C {a = 1, ..} = e
 
-::
+   defines ``b``, ``c``, and ``d``.
 
-      eval :: Term a -> a -> a
-      eval (Lit i) j =  i+j
+-  Record wildcards can also be used in an expression, when constructing
+   a record. For example,
 
-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.
+   ::
 
-These and many other examples are given in papers by Hongwei Xi, and Tim
-Sheard. There is a longer introduction `on the
-wiki <http://www.haskell.org/haskellwiki/GADT>`__, and Ralf Hinze's `Fun
-with phantom
-types <http://www.cs.ox.ac.uk/ralf.hinze/publications/With.pdf>`__ also
-has a number of examples. Note that papers may use different notation to
-that implemented in GHC.
+       let {a = 1; b = 2; c = 3; d = 4} in C {..}
 
-The rest of this section outlines the extensions to GHC that support
-GADTs. The extension is enabled with ``-XGADTs``. The ``-XGADTs`` flag
-also sets ``-XGADTSyntax`` and ``-XMonoLocalBinds``.
+   in place of
 
--  A GADT can only be declared using GADT-style syntax
-   (:ref:`gadt-style`); 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).
+   ::
 
--  It is permitted to declare an ordinary algebraic data type using
-   GADT-style 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``.
+       let {a = 1; b = 2; c = 3; d = 4} in C {a=a, b=b, c=c, d=d}
 
--  You cannot use a ``deriving`` clause for a GADT; only for an ordinary
-   data type.
+   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.
 
--  As mentioned in :ref:`gadt-style`, record syntax is supported. For
-   example:
+-  Record wildcards may *not* be used in record *updates*. For example
+   this is illegal:
 
    ::
 
-         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
+       f r = r { x = 3, .. }
 
-   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:
+-  For both pattern and expression wildcards, the "``..``" expands to
+   the missing *in-scope* record fields. Specifically the expansion of
+   "``C {..}``" includes ``f`` if and only if:
+
+   -  ``f`` is a record field of constructor ``C``.
+
+   -  The record field ``f`` is in scope somehow (either qualified or
+      unqualified).
+
+   -  In the case of expressions (but not patterns), the variable ``f``
+      is in scope unqualified, apart from the binding of the record
+      selector itself.
+
+   These rules restrict record wildcards to the situations in which the
+   user could have written the expanded version. For example
 
    ::
 
-         num :: Term Int -> Term Int
-         arg :: Term Bool -> Term Int
+       module M where
+         data R = R { a,b,c :: Int }
+       module X where
+         import M( R(a,c) )
+         f b = R { .. }
 
--  When pattern-matching against data constructors drawn from a GADT,
-   for example in a ``case`` expression, the following rules apply:
+   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).
 
-   -  The type of the scrutinee must be rigid.
+-  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:
 
-   -  The type of the entire ``case`` expression must be rigid.
+   ::
 
-   -  The type of any free variable mentioned in any of the ``case``
-      alternatives must be rigid.
+       f x = x { v=True, .. }   -- Illegal (a)
 
-   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
-   unification-based type inference for
-   GADTs <http://research.microsoft.com/%7Esimonpj/papers/gadt>`__. The
-   criteria implemented by GHC are given in the Appendix.
+       data T = MkT Int Bool
+       g = MkT { .. }           -- Illegal (b)
+       h (MkT { .. }) = True    -- Illegal (b)
 
 .. _deriving:
 
@@ -8244,6 +8402,8 @@ 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.
 
+.. _higher-rank-type-inference:
+
 Type inference
 ~~~~~~~~~~~~~~