ghc: implement OverloadedRecordFieldswip/orf

This fully implements the new ORF extension, developed during the Google
Summer of Code 2013, and as described on the wiki:

  https://ghc.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields

This also updates the Haddock submodule.

Reviewed-by: Simon Peyton Jones <simonpj@microsoft.com>
Signed-off-by: Austin Seipp <austin@well-typed.com>

4 files changed, 258 insertions, 3 deletions

diff --git a/libraries/base/GHC/Base.lhs b/libraries/base/GHC/Base.lhs
index 1c8e144b7f..89ee79b72a 100644
--- a/libraries/base/GHC/Base.lhs
+++ b/libraries/base/GHC/Base.lhs
@@ -122,6 +122,9 @@ import GHC.Tuple ()
 -- Likewise we need Integer when deriving things like Eq instances, and
 -- this is a convenient place to force it to be built
 import GHC.Integer ()
+-- We need GHC.Records before declaring datatypes with record fields
+-- (see Note [Dependency on GHC.Records] in GHC.Records).
+import GHC.Records ()
 
 infixr 9  .
 infixr 5  ++
diff --git a/libraries/base/GHC/Records.hs b/libraries/base/GHC/Records.hs
new file mode 100644
index 0000000000..cc1ea600fa
--- /dev/null
+++ b/libraries/base/GHC/Records.hs
@@ -0,0 +1,249 @@
+{-# LANGUAGE MultiParamTypeClasses, KindSignatures, DataKinds,
+             TypeFamilies, RankNTypes, FlexibleInstances, FlexibleContexts,
+             NoImplicitPrelude, EmptyDataDecls, MagicHash, UndecidableInstances #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  GHC.Records
+-- Copyright   :  (c) Adam Gundry, 2013-2014
+-- License     :  BSD-style (see libraries/base/LICENSE)
+--
+-- Maintainer  :  libraries@haskell.org
+-- Stability   :  internal
+-- Portability :  non-portable (GHC extensions)
+--
+-- This is an internal GHC module that defines classes relating to the
+-- OverloadedRecordFields extension.  For notes on the implementation
+-- of OverloadedRecordFields, see
+-- https://ghc.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields/Implementation
+-----------------------------------------------------------------------------
+
+{-
+Note [Dependency on GHC.Records]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+This module must be compiled before any module that declares a record
+field, because the class declarations below are loaded in order to
+generate the supporting definitions for overloaded record fields. To
+achieve this, this module is imported by GHC.Base. If you receive the
+error "Failed to load interface for ‛GHC.Records’" while compiling
+base, this module has not been compiled early enough.
+-}
+
+module GHC.Records where
+
+import GHC.Integer ()
+import GHC.Prim (Proxy#)
+
+-- | (Kind) This is the kind of type-level symbols.
+data Symbol
+
+
+{-
+The OverloadedRecordFields extension generates instances for the
+following type classes ('Has' and 'Upd') and type families
+('FldTy' and 'UpdTy'). For example, the datatype
+
+    data T a = MkT { foo :: [a] }
+
+gives rise to the instances
+
+    type instance FldTy (T a) "foo"     = [a]
+    type instance UpdTy (T a) "foo" [c] = T c
+    instance b ~ [a] => Has (T a) "foo" b
+    instance b ~ [c] => Upd (T a) "foo" b
+
+See compiler/typecheck/TcFldInsts.lhs for the code that generates
+these instances.  The instances are generated for every datatype,
+regardless of whether the extension is enabled, but they are not
+exported using the normal mechanism, because the instances in scope
+correspond exactly to the record fields in scope.  See
+Note [Instance scoping for OverloadedRecordFields] in TcFldInsts.
+-}
+
+
+-- | @FldTy r n@ is the type of the field @n@ in record type @r@.
+type family FldTy (r :: *) (n :: Symbol) :: *
+-- See Note [Why not associated types]
+
+-- | @UpdTy r n t@ is the record type that results from setting
+-- the field @n@ of record type @r@ to @t@.
+type family UpdTy (r :: *) (n :: Symbol) (t :: *) :: *
+
+-- | @Has r n t@ means that @r@ is a record type with field @n@ of type @t@.
+class t ~ FldTy r n  -- See Note [Functional dependency via equality superclass]
+          => Has r (n :: Symbol) t where
+  -- | Polymorphic field selector
+  getField :: Proxy# n -> r -> t
+
+-- | @Upd r n t@ means that @r@ is a record type with field @n@ which
+-- can be assigned type @t@.
+class (Has r n (FldTy r n), r ~ UpdTy r n (FldTy r n))
+              -- See Note [Superclasses of Upd]
+          => Upd (r :: *) (n :: Symbol) (t :: *) where
+  -- | Polymorphic field update
+  setField :: Proxy# n -> r -> t -> UpdTy r n t
+
+
+{-
+Note [Functional dependency via equality superclass]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The third parameter of the 'Has' class (the field type) is
+functionally dependent on the first two (the record type and field
+name), but is present to allow for syntactic sugar:
+
+    r { f :: t }    translates to    Has r "f" t
+
+The functional dependency is encoded using the 'FldTy' type
+family, via the equality superclass 't ~ FldTy r n' in the
+declaration of 'Has'. Thanks to this superclass, if we have a
+constraint
+
+    [Wanted] Has (T alpha) "foo" beta
+
+then we get
+
+    [Derived] beta ~ FldTy (T alpha) "foo".
+
+Now substituting for 'beta' in the wanted constraint and reducing
+'FldTy' gives
+
+    [Wanted] Has (T alpha) "foo" [alpha].
+
+This constraint could be solved via
+
+    instance Has (T a) "foo" [a].
+
+However, if the field type involved a type family, for example
+
+    type family F x
+    data U a = MkU { foo :: F a }
+
+then we would end up with
+
+    [Wanted] Has (U alpha) "foo" (F alpha)
+
+which does not obviously match
+
+    instance Has (U a) "foo" (F a).
+
+Thus we always generate an instance like
+
+    instance b ~ F a => Has (U a) "foo" b
+
+that matches only on the first two parameters.
+
+
+In any case, the third parameter of 'Upd' is not functionally
+dependent on the first two, because it represents the new type being
+assigned to the field, not its current type. Thus we must generate
+
+    instance b ~ [c] => Upd (T a) "foo" b
+
+to ensure that a constraint like
+
+    [Wanted] Upd (T alpha) "foo" beta
+
+will be solved.
+
+
+Note [Why not associated types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+'FldTy' could be an associated type, but 'UpdTy' cannot, so
+for consistency both are separate top-level type families.  The
+parameters of associated types must be exactly the same as the class
+header (they cannot be more specific instances), so this is currently
+illegal:
+
+    instance t ~ [b] => Upd (T a) "foo" t where
+        type UpdTy (T a) "foo" [b] = T b
+
+If this were allowed, both type families could become associated
+types. See Trac #8161. The difference is minimal, however.
+
+
+Note [Superclasses of Upd]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+The superclasses of 'Upd' ensure that there is always a corresponding
+'Has' instance, and that the invariant
+
+    r ~ UpdTy r n (FldTy r n)
+
+always holds. This says that setting a field without changing its type
+does not change the type of the record. It is included so that
+
+    [Given] Upd r n (FldTy r n)
+
+implies
+
+    setField :: Proxy# n -> r -> FldTy r n -> r
+
+which may make it easier to write some very polymorphic code to update
+fields. If you can think of a concrete example of why this is useful,
+please add it here!
+-}
+
+
+-- | @Accessor p r n t@ means that @p@ is a type into which a field
+-- with name @n@ having type @t@ in record @r@ can be translated.  The
+-- canonical instance is for the function space (->), which just
+-- returns the getter (completely ignoring the setter).  Lens
+-- libraries may give instances of 'Accessor' so that overloaded
+-- fields can be used as lenses.
+class Accessor (p :: * -> * -> *) (r :: *) (n :: Symbol) (t :: *) where
+  -- | @accessField z getter setter@ injects a getter and setter pair into @p@
+  accessField :: Proxy# n ->
+                 (Has r n t => r -> t) ->
+                 (forall t' . Upd r n t' => r -> t' -> UpdTy r n t') ->
+                 p r t
+
+instance Has r n t => Accessor (->) r n t where
+  accessField _ getter _ = getter
+
+
+{-
+When the OverloadedRecordFields extension is enabled, a field @foo@ in
+an expression is translated into
+
+    field (proxy# :: Proxy# "foo") :: Accessor p r "foo" t => p r t
+-}
+
+-- | Target for translation of overloaded record field occurrences
+field :: forall p r n t . Accessor p r n t => Proxy# n -> p r t
+field z = accessField z (getField z) (setField z)
+
+
+{-
+Note [On the multiplicity of parameters]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+One might me tempted to remove the third redundant parameter of the
+'Has' class, since it is always determined by the first two.
+Similarly, the 'Accessor' class can be defined using only the 'p' and
+'n' parameters.  However, apart from the three-parameter version of
+'Has' naturally supporting the syntactic sugar, this approach leads to
+better error messages for misues of fields.  For example, we get
+
+    No instance for (Int -> Int) {x :: Bool}
+      arising from a use of the record selector ‛x’
+    The type ‛(->)’ does not have a field ‛x’
+
+instead of
+
+    Couldn't match type ‛GHC.Records.FldTy (Int -> Int) "x"’
+                  with ‛Bool’
+    Expected type: (Int -> Int) -> Bool
+      Actual type: (Int -> Int) -> GHC.Records.FldTy (Int -> Int) "x"
+
+Crucially, the type of 'field', into which overloaded fields are
+translated, does not mention the 'FldTy' type family.  Thus we get an
+error from failing to find the necessary 'Has' instance instead of
+failing to expand 'FldTy'.
+
+This also means that the type of an overloaded field 'foo' is
+
+    GHC.Records.Accessor t t1 "foo" t2 => t t1 t2
+
+rather than
+
+     GHC.Records.Accessor t t1 "foo" => t t1 (GHC.Records.FldTy t1 "foo")
+-}
diff --git a/libraries/base/GHC/TypeLits.hs b/libraries/base/GHC/TypeLits.hs
index 083ae4d144..6b287dddd1 100644
--- a/libraries/base/GHC/TypeLits.hs
+++ b/libraries/base/GHC/TypeLits.hs
@@ -40,6 +40,7 @@ import GHC.Num(Integer)
 import GHC.Base(String)
 import GHC.Show(Show(..))
 import GHC.Read(Read(..))
+import GHC.Records(Symbol)
 import GHC.Prim(magicDict)
 import Data.Maybe(Maybe(..))
 import Data.Proxy(Proxy(..))
@@ -49,9 +50,10 @@ import Unsafe.Coerce(unsafeCoerce)
 -- | (Kind) This is the kind of type-level natural numbers.
 data Nat
 
--- | (Kind) This is the kind of type-level symbols.
-data Symbol
-
+-- The kind Symbol of type-level symbols is defined in GHC.Records,
+-- because it is used there and that module must be compiled very
+-- early (see Note [Dependency on GHC.Records] in GHC.Records).
+-- It is re-exported by this module.
 
 --------------------------------------------------------------------------------
 
diff --git a/libraries/base/base.cabal b/libraries/base/base.cabal
index a70a661920..d6fad6c919 100644
--- a/libraries/base/base.cabal
+++ b/libraries/base/base.cabal
@@ -234,6 +234,7 @@ Library
         GHC.Ptr
         GHC.Read
         GHC.Real
+        GHC.Records
         GHC.ST
         GHC.STRef
         GHC.Show