Update OverloadedLabels docs and document HasField

Test Plan: n/a

Reviewers: bgamari, austin

Reviewed By: bgamari

Subscribers: thomie

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

2 files changed, 213 insertions, 21 deletions

diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index dbb17351d3..edb28d2c14 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -1444,6 +1444,9 @@ not the Prelude versions:
    via rebindable syntax if you use `-XOverloadedLists`;
    see :ref:`overloaded-lists`.
 
+-  An overloaded label "``#foo``" means "``fromLabel @"foo"``", rather than
+   "``GHC.OverloadedLabels.fromLabel @"foo"``" (see :ref:`overloaded-labels`).
+
 :ghc-flag:`-XRebindableSyntax` implies :ghc-flag:`-XNoImplicitPrelude`.
 
 In all cases (apart from arrow notation), the static semantics should be
@@ -3187,6 +3190,183 @@ More details:
        g = MkT { .. }           -- Illegal (b)
        h (MkT { .. }) = True    -- Illegal (b)
 
+
+.. _record-field-selector-polymorphism:
+
+Record field selector polymorphism
+----------------------------------
+
+The module :base-ref:`GHC.Records <GHC-Records.html>` defines the following: ::
+
+  class HasField (x :: k) r a | x r -> a where
+    getField :: r -> a
+
+A ``HasField x r a`` constraint represents the fact that ``x`` is a
+field of type ``a`` belonging to a record type ``r``.  The
+``getField`` method gives the record selector function.
+
+This allows definitions that are polymorphic over record types with a specified
+field.  For example, the following works with any record type that has a field
+``name :: String``: ::
+
+  foo :: HasField "name" r String => r -> String
+  foo r = reverse (getField @"name" r)
+
+``HasField`` is a magic built-in typeclass (similar to ``Coercible``, for
+example).  It is given special treatment by the constraint solver (see
+:ref:`solving-hasfield-constraints`).  Users may define their own instances of
+``HasField`` also (see :ref:`virtual-record-fields`).
+
+.. _solving-hasfield-constraints:
+
+Solving HasField constraints
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+If the constraint solver encounters a constraint ``HasField x r a``
+where ``r`` is a concrete datatype with a field ``x`` in scope, it
+will automatically solve the constraint using the field selector as
+the dictionary, unifying ``a`` with the type of the field if
+necessary.  This happens irrespective of which extensions are enabled.
+
+For example, if the following datatype is in scope ::
+
+  data Person = Person { name :: String }
+
+the end result is rather like having an instance ::
+
+  instance HasField "name" Person String where
+    getField = name
+
+except that this instance is not actually generated anywhere, rather
+the constraint is solved directly by the constraint solver.
+
+A field must be in scope for the corresponding ``HasField`` constraint
+to be solved.  This retains the existing representation hiding
+mechanism, whereby a module may choose not to export a field,
+preventing client modules from accessing or updating it directly.
+
+Solving ``HasField`` constraints depends on the field selector functions that
+are generated for each datatype definition:
+
+-  If a record field does not have a selector function because its type would allow
+   an existential variable to escape, the corresponding ``HasField`` constraint
+   will not be solved.  For example, ::
+
+     {-# LANGUAGE ExistentialQuantification #-}
+     data Exists t = forall x . MkExists { unExists :: t x }
+
+   does not give rise to a selector ``unExists :: Exists t -> t x`` and we will not
+   solve ``HasField "unExists" (Exists t) a`` automatically.
+
+-  If a record field has a polymorphic type (and hence the selector function is
+   higher-rank), the corresponding ``HasField`` constraint will not be solved,
+   because doing so would violate the functional dependency on ``HasField`` and/or
+   require impredicativity.  For example, ::
+
+     {-# LANGUAGE RankNTypes #-}
+     data Higher = MkHigher { unHigher :: forall t . t -> t }
+
+   gives rise to a selector ``unHigher :: Higher -> (forall t . t -> t)`` but does
+   not lead to solution of the constraint ``HasField "unHigher" Higher a``.
+
+-  A record GADT may have a restricted type for a selector function, which may lead
+   to additional unification when solving ``HasField`` constraints.  For example, ::
+
+     {-# LANGUAGE GADTs #-}
+     data Gadt t where
+       MkGadt :: { unGadt :: Maybe v } -> Gadt [v]
+
+   gives rise to a selector ``unGadt :: Gadt [v] -> Maybe v``, so the solver will reduce
+   the constraint ``HasField "unGadt" (Gadt t) b`` by unifying ``t ~ [v]`` and
+   ``b ~ Maybe v`` for some fresh metavariable ``v``, rather as if we had an instance ::
+
+     instance (t ~ [v], b ~ Maybe v) => HasField "unGadt" (Gadt t) b
+
+-  If a record type has an old-fashioned datatype context, the ``HasField``
+   constraint will be reduced to solving the constraints from the context.
+   For example, ::
+
+     {-# LANGUAGE DatatypeContexts #-}
+     data Eq a => Silly a = MkSilly { unSilly :: a }
+
+   gives rise to a selector ``unSilly :: Eq a => Silly a -> a``, so
+   the solver will reduce the constraint ``HasField "unSilly" (Silly a) b`` to
+   ``Eq a`` (and unify ``a`` with ``b``), rather as if we had an instance ::
+
+     instance (Eq a, a ~ b) => HasField "unSilly" (Silly a) b
+
+.. _virtual-record-fields:
+
+Virtual record fields
+~~~~~~~~~~~~~~~~~~~~~
+
+Users may define their own instances of ``HasField``, provided they do
+not conflict with the built-in constraint solving behaviour.  This
+allows "virtual" record fields to be defined for datatypes that do not
+otherwise have them.
+
+For example, this instance would make the ``name`` field of ``Person``
+accessible using ``#fullname`` as well: ::
+
+  instance HasField "fullname" Person String where
+    getField = name
+
+More substantially, an anonymous records library could provide
+``HasField`` instances for its anonymous records, and thus be
+compatible with the polymorphic record selectors introduced by this
+proposal.  For example, something like this makes it possible to use
+``getField`` to access ``Record`` values with the appropriate
+string in the type-level list of fields: ::
+
+  data Record (xs :: [(k, Type)]) where
+    Nil  :: Record '[]
+    Cons :: Proxy x -> a -> Record xs -> Record ('(x, a) ': xs)
+
+  instance HasField x (Record ('(x, a) ': xs)) a where
+    getField (Cons _ v _) = v
+  instance HasField x (Record xs) a => HasField x (Record ('(y, b) ': xs)) a where
+    getField (Cons _ _ r) = getField @x r
+
+  r :: Record '[ '("name", String) ]
+  r = Cons Proxy "R" Nil)
+
+  x = getField @"name" r
+
+Since representations such as this can support field labels with kinds other
+than ``Symbol``, the ``HasField`` class is poly-kinded (even though the built-in
+constraint solving works only at kind ``Symbol``).  In particular, this allows
+users to declare scoped field labels such as in the following example: ::
+
+  data PersonFields = Name
+
+  s :: Record '[ '(Name, String) ]
+  s = Cons Proxy "S" Nil
+
+  y = getField @Name s
+
+In order to avoid conflicting with the built-in constraint solving,
+the following user-defined ``HasField`` instances are prohibited (in
+addition to the usual rules, such as the prohibition on type
+families appearing in instance heads):
+
+-  ``HasField _ r _`` where ``r`` is a variable;
+
+-  ``HasField _ (T ...) _`` if ``T`` is a data family (because it
+   might have fields introduced later, using data instance declarations);
+
+-  ``HasField x (T ...) _`` if ``x`` is a variable and ``T`` has any
+   fields at all (but this instance is permitted if ``T`` has no fields);
+
+-  ``HasField "foo" (T ...) _`` if ``T`` has a field ``foo`` (but this
+   instance is permitted if it does not).
+
+If a field has a higher-rank or existential type, the corresponding ``HasField``
+constraint will not be solved automatically (as described above), but in the
+interests of simplicity we do not permit users to define their own instances
+either.  If a field is not in scope, the corresponding instance is still
+prohibited, to avoid conflicts in downstream modules.
+
+
 .. _deriving:
 
 Extensions to the "deriving" mechanism
@@ -6010,42 +6190,47 @@ The class ``IsLabel`` is defined as:
 ::
 
     class IsLabel (x :: Symbol) a where
-      fromLabel :: Proxy# x -> a
+      fromLabel :: a
 
 This is rather similar to the class ``IsString`` (see
 :ref:`overloaded-strings`), but with an additional type parameter that makes the
 text of the label available as a type-level string (see
-:ref:`type-level-literals`).
+:ref:`type-level-literals`).  Note that ``fromLabel`` had an extra ``Proxy# x``
+argument in GHC 8.0, but this was removed in GHC 8.2 as a type application (see
+:ref:`visible-type-application`) can be used instead.
 
 There are no predefined instances of this class.  It is not in scope by default,
 but can be brought into scope by importing
-:base-ref:`GHC.OverloadedLabels <GHC-OverloadedLabels.html>`:.  Unlike
+:base-ref:`GHC.OverloadedLabels <GHC-OverloadedLabels.html>`.  Unlike
 ``IsString``, there are no special defaulting rules for ``IsLabel``.
 
 During typechecking, GHC will replace an occurrence of an overloaded label like
-``#foo`` with
-
-::
-
-    fromLabel (proxy# :: Proxy# "foo")
-
-This will have some type ``alpha`` and require the solution of a class
-constraint ``IsLabel "foo" alpha``.
+``#foo`` with ``fromLabel @"foo"``.  This will have some type ``alpha`` and
+require the solution of a class constraint ``IsLabel "foo" alpha``.
 
 The intention is for ``IsLabel`` to be used to support overloaded record fields
 and perhaps anonymous records.  Thus, it may be given instances for base
 datatypes (in particular ``(->)``) in the future.
 
-When writing an overloaded label, there must be no space between the hash sign
-and the following identifier.  :ref:`magic-hash` makes use of postfix hash
-signs; if ``OverloadedLabels`` and ``MagicHash`` are both enabled then ``x#y``
-means ``x# y``, but if only ``OverloadedLabels`` is enabled then it means ``x
-#y``.  To avoid confusion, you are strongly encouraged to put a space before the
-hash when using ``OverloadedLabels``.
+If :ghc-flag:`-XRebindableSyntax` is enabled, overloaded
+labels will be desugared using whatever ``fromLabel`` function is in scope,
+rather than always using ``GHC.OverloadedLabels.fromLabel``.
 
-When using ``OverloadedLabels`` (or ``MagicHash``) in a ``.hsc`` file (see
-:ref:`hsc2hs`), the hash signs must be doubled (write ``##foo`` instead of
-``#foo``) to avoid them being treated as ``hsc2hs`` directives.
+When writing an overloaded label, there must be no space between the hash sign
+and the following identifier.  The :ghc-flag:`-XMagicHash` extension makes use
+of postfix hash signs; if :ghc-flag:`-XOverloadedLabels` and
+:ghc-flag:`-XMagicHash` are both enabled then ``x#y`` means ``x# y``, but if
+only :ghc-flag:`-XOverloadedLabels` is enabled then it means ``x #y``.  The
+:ghc-flag:`-XUnboxedTuples` extension makes ``(#`` a single lexeme, so when
+:ghc-flag:`-XUnboxedTuples` is enabled you must write a space between an opening
+parenthesis and an overloaded label.  To avoid confusion, you are strongly
+encouraged to put a space before the hash when using
+:ghc-flag:`-XOverloadedLabels`.
+
+When using :ghc-flag:`-XOverloadedLabels` (or other extensions that make use of
+hash signs) in a ``.hsc`` file (see :ref:`hsc2hs`), the hash signs must be
+doubled (write ``##foo`` instead of ``#foo``) to avoid them being treated as
+``hsc2hs`` directives.
 
 Here is an extension of the record access example in :ref:`type-level-literals`
 showing how an overloaded label can be used as a record selector:
@@ -6070,7 +6255,7 @@ showing how an overloaded label can be used as a record selector:
     instance Has Point "y" Int where from (Point _ y) _ = y
 
     instance Has a l b => IsLabel l (a -> b) where
-      fromLabel _ x = from x (Get :: Label l)
+      fromLabel x = from x (Get :: Label l)
 
     example = #x (Point 1 2)
 
diff --git a/utils/mkUserGuidePart/Options/Language.hs b/utils/mkUserGuidePart/Options/Language.hs
index f86b27d6c7..11adca106d 100644
--- a/utils/mkUserGuidePart/Options/Language.hs
+++ b/utils/mkUserGuidePart/Options/Language.hs
@@ -484,6 +484,13 @@ languageOptions =
          , flagReverse = "-XNoOverlappingInstances"
          , flagSince = "6.8.1"
          }
+  , flag { flagName = "-XOverloadedLabels"
+         , flagDescription =
+           "Enable :ref:`overloaded labels <overloaded-labels>`."
+         , flagType = DynamicFlag
+         , flagReverse = "-XNoOverloadedLabels"
+         , flagSince = "8.0.1"
+         }
   , flag { flagName = "-XOverloadedLists"
          , flagDescription =
            "Enable :ref:`overloaded lists <overloaded-lists>`."