[Git][ghc/ghc][wip/amg/hasfield-2020] 2 commits: Update user's guide for changes to HasField

Adam Gundry gitlab at gitlab.haskell.org
Fri Sep 25 13:23:37 UTC 2020



Adam Gundry pushed to branch wip/amg/hasfield-2020 at Glasgow Haskell Compiler / GHC


Commits:
c64bf7b3 by Adam Gundry at 2020-09-25T14:22:46+01:00
Update user's guide for changes to HasField

- - - - -
d32a697d by Adam Gundry at 2020-09-25T14:22:46+01:00
Update HasField tests

Adapt overloadedrecflds tests and T17355 to new definition of HasField
Extend hasfieldrun01 test with partial record field test
Update hasfieldfail02 test to check unlifted type case
Accept changed T14189 output due to FieldLabel additional field
Adjust expected output from dynamic-paper
Add hasfieldrun03 test for example from user's guide

 Metric Increase:
     T12227
     T12707
     T13056
     T15630
     T18304
     T9233
     T9675

- - - - -


16 changed files:

- docs/users_guide/exts/hasfield.rst
- testsuite/tests/dependent/should_compile/dynamic-paper.stderr
- testsuite/tests/overloadedrecflds/should_fail/hasfieldfail01.hs
- testsuite/tests/overloadedrecflds/should_fail/hasfieldfail02.hs
- testsuite/tests/overloadedrecflds/should_fail/hasfieldfail02.stderr
- testsuite/tests/overloadedrecflds/should_fail/hasfieldfail03.hs
- testsuite/tests/overloadedrecflds/should_run/all.T
- testsuite/tests/overloadedrecflds/should_run/hasfieldrun01.hs
- + testsuite/tests/overloadedrecflds/should_run/hasfieldrun01.stderr
- testsuite/tests/overloadedrecflds/should_run/hasfieldrun01.stdout
- + testsuite/tests/overloadedrecflds/should_run/hasfieldrun03.hs
- + testsuite/tests/overloadedrecflds/should_run/hasfieldrun03.stdout
- testsuite/tests/overloadedrecflds/should_run/overloadedrecfldsrun07.hs
- testsuite/tests/overloadedrecflds/should_run/overloadedrecfldsrun07.stdout
- testsuite/tests/parser/should_compile/T14189.stderr
- testsuite/tests/typecheck/should_fail/T17355.hs


Changes:

=====================================
docs/users_guide/exts/hasfield.rst
=====================================
@@ -6,15 +6,23 @@ Record field selector polymorphism
 The module :base-ref:`GHC.Records.` defines the following: ::
 
   class HasField (x :: k) r a | x r -> a where
-    getField :: r -> a
+    hasField :: r -> (a -> 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.
+``hasField`` method gives the ability to select and update the field.
 
-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``: ::
+This module also defines: ::
+
+  getField :: forall x r a . HasField x r a => r -> a
+  getField = snd . hasField @x
+
+  setField :: forall x r a . HasField x r a => r -> a -> r
+  setField = fst . hasField @x
+
+These make it possible to write functions 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)
@@ -31,8 +39,8 @@ 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
+will automatically solve the constraint by generating a suitable
+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 ::
@@ -52,12 +60,12 @@ 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:
+Solving ``HasField`` constraints depends on the type of the field:
 
--  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, ::
+-  If a record field has a type containing an existential variable, it cannot
+   have a selector function, and the corresponding ``HasField`` constraint will
+   not be solved, because this would allow the existential variable to escape.
+   For example, ::
 
      {-# LANGUAGE ExistentialQuantification #-}
      data Exists t = forall x . MkExists { unExists :: t x }
@@ -67,14 +75,16 @@ are generated for each datatype definition:
 
 -  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, ::
+   because doing so would violate the functional dependency on ``HasField``
+   and/or require an impredicative constraint (which is not allowed even with
+   :extension:`ImpredicativeTypes`).  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``.
+   not lead to solution of the constraint ``HasField "unHigher" Higher a`` (which
+   would require an impredicative instantiation of ``a`` with ``forall t . t -> t``).
 
 -  A record GADT may have a restricted type for a selector function, which may lead
    to additional unification when solving ``HasField`` constraints.  For example, ::
@@ -116,7 +126,7 @@ For example, this instance would make the ``name`` field of ``Person``
 accessible using ``#fullname`` as well: ::
 
   instance HasField "fullname" Person String where
-    getField = name
+    hasField r = (\n -> r { name = n }, name r)
 
 More substantially, an anonymous records library could provide
 ``HasField`` instances for its anonymous records, and thus be
@@ -125,19 +135,34 @@ 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: ::
 
+  {-# LANGUAGE DataKinds #-}
+  {-# LANGUAGE FlexibleContexts #-}
+  {-# LANGUAGE GADTs #-}
+  {-# LANGUAGE PolyKinds #-}
+  {-# LANGUAGE ScopedTypeVariables #-}
+  {-# LANGUAGE TypeApplications #-}
+  {-# LANGUAGE TypeOperators #-}
+  {-# LANGUAGE UndecidableInstances #-}
+
+  import Data.Kind (Type)
+  import Data.Proxy (Proxy(..))
+  import GHC.Records
+
   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 {-# OVERLAPS #-} HasField x (Record ('(x, a) ': xs)) a where
+    hasField (Cons p v r) = (\v' -> Cons p v' r, v)
   instance HasField x (Record xs) a => HasField x (Record ('(y, b) ': xs)) a where
-    getField (Cons _ _ r) = getField @x r
+    hasField (Cons p v r) = (\v' -> Cons p v (set v'), a)
+      where
+        (set,a) = hasField @x r
 
   r :: Record '[ '("name", String) ]
-  r = Cons Proxy "R" Nil)
+  r = Cons Proxy "R" Nil
 
-  x = getField @"name" r
+  x = getField @"name" (setField @"name" r "S")
 
 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
@@ -173,5 +198,27 @@ 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.
 
+.. _compatibility-notes:
+
+Compatibility notes
+~~~~~~~~~~~~~~~~~~~
+
+``HasField`` was introduced in GHC 8.2.
+
+In versions of GHC prior to 9.2, the ``HasField`` class provided only a
+``getField`` method, so it was not possibly to update fields in a polymorphic
+way.  This means:
+
+- Code using ``hasField`` or ``setField`` will require at least GHC 9.2.
+
+- Code using ``getField`` only may support GHC 8.2 and later, and should use
+  ``import GHC.Records (HasField, getField)`` which works regardless of whether
+  ``getField`` is a class method (prior to 9.2) or a function (9.2 and later).
 
+- User-defined ``HasField`` instances must use :extension:`CPP` to support GHC
+  versions before and after 9.2.
 
+:ref:`record-patsyn` do not lead to automatic solution of ``HasField`` instances
+for their fields, so if you replace a datatype with a pattern synonym where
+``HasField`` is in use, you may need to define :ref:`virtual-record-fields`
+manually.


=====================================
testsuite/tests/dependent/should_compile/dynamic-paper.stderr
=====================================
@@ -12,4 +12,4 @@ Simplifier ticks exhausted
   simplifier non-termination has been judged acceptable.
    
   To see detailed counts use -ddump-simpl-stats
-  Total ticks: 136961
+  Total ticks: 139362


=====================================
testsuite/tests/overloadedrecflds/should_fail/hasfieldfail01.hs
=====================================
@@ -2,7 +2,7 @@
 
 import HasFieldFail01_A (T(MkT))
 
-import GHC.Records (HasField(..))
+import GHC.Records (HasField, getField)
 
 -- This should fail to solve the HasField constraint, because foo is
 -- not in scope.


=====================================
testsuite/tests/overloadedrecflds/should_fail/hasfieldfail02.hs
=====================================
@@ -1,10 +1,12 @@
 {-# LANGUAGE DataKinds, ExistentialQuantification, MagicHash, RankNTypes,
              TypeApplications #-}
 
-import GHC.Records (HasField(..))
+import GHC.Prim (Int#)
+import GHC.Records (HasField, getField)
 
 data T = MkT { foo :: forall a . a -> a }
 data U = forall b . MkU { bar :: b }
+data V = MkV { baz :: Int# }
 
 -- This should fail because foo is higher-rank.
 x = getField @"foo" (MkT id)
@@ -13,4 +15,7 @@ x = getField @"foo" (MkT id)
 -- involves an existential).
 y = getField @"bar" (MkU True)
 
+-- This should fail because baz is not of kind Type.
+z = getField @"baz" (MkV 3#)
+
 main = return ()


=====================================
testsuite/tests/overloadedrecflds/should_fail/hasfieldfail02.stderr
=====================================
@@ -1,13 +1,18 @@
 
-hasfieldfail02.hs:10:5: error:
-    • No instance for (HasField "foo" T a1)
+hasfieldfail02.hs:12:5: error:
+    • No instance for (HasField "foo" T a2)
         arising from a use of ‘getField’
     • In the expression: getField @"foo" (MkT id)
-      In an equation for ‘x’:
-          x = getField @"foo" (MkT id)
+      In an equation for ‘x’: x = getField @"foo" (MkT id)
 
-hasfieldfail02.hs:14:5: error:
-    • No instance for (HasField "bar" U a0)
+hasfieldfail02.hs:16:5: error:
+    • No instance for (HasField "bar" U a1)
         arising from a use of ‘getField’
     • In the expression: getField @"bar" (MkU True)
       In an equation for ‘y’: y = getField @"bar" (MkU True)
+
+hasfieldfail02.hs:19:5: error:
+    • No instance for (HasField "baz" V a0)
+        arising from a use of ‘getField’
+    • In the expression: getField @"baz" (MkV 3#)
+      In an equation for ‘z’: z = getField @"baz" (MkV 3#)


=====================================
testsuite/tests/overloadedrecflds/should_fail/hasfieldfail03.hs
=====================================
@@ -7,23 +7,23 @@ data T = MkT { foo :: Int, bar :: Int }
 
 -- This is far too polymorphic
 instance HasField "woo" a Bool where
-  getField = const True
+  hasField = undefined
 
 -- This conflicts with the built-in instance
 instance HasField "foo" T Int where
-  getField = foo
+  hasField = undefined
 
 -- So does this
 instance HasField "bar" T Bool where
-  getField = const True
+  hasField = undefined
 
 -- This doesn't conflict because there is no "baz" field in T
 instance HasField "baz" T Bool where
-  getField = const True
+  hasField = undefined
 
 -- Bool has no fields, so this is okay
 instance HasField a Bool Bool where
-  getField = id
+  hasField = undefined
 
 
 data family V a b c d
@@ -32,8 +32,8 @@ data instance V x Int y [z] = MkVInt { baz :: (x, y, z, Bool) }
 -- Data families cannot have HasField instances, because they may get
 -- fields defined later on
 instance HasField "baz" (V a b c d) Bool where
-  getField = const True
+  hasField = undefined
 
 -- Function types can have HasField instances, in case it's useful
 instance HasField "woo" (a -> b) Bool where
-  getField = const True
+  hasField = undefined


=====================================
testsuite/tests/overloadedrecflds/should_run/all.T
=====================================
@@ -14,6 +14,7 @@ test('overloadedlabelsrun03', normal, compile_and_run, [''])
 test('overloadedlabelsrun04', [extra_files(['OverloadedLabelsRun04_A.hs']),
                                omit_ways(prof_ways)], multimod_compile_and_run,
      ['overloadedlabelsrun04', config.ghc_th_way_flags])
-test('hasfieldrun01', normal, compile_and_run, [''])
+test('hasfieldrun01', [exit_code(1)], compile_and_run, [''])
 test('hasfieldrun02', normal, compile_and_run, [''])
+test('hasfieldrun03', normal, compile_and_run, [''])
 test('T12243', normal, compile_and_run, [''])


=====================================
testsuite/tests/overloadedrecflds/should_run/hasfieldrun01.hs
=====================================
@@ -6,14 +6,19 @@
            , TypeFamilies
            , TypeApplications
   #-}
+{-# OPTIONS_GHC -dcore-lint #-}
 
-import GHC.Records (HasField(..))
+import GHC.Records (HasField(..), getField, setField)
+
+data S a where
+  MkS :: { soo :: Either p q } -> S (p,q)
 
 type family B where B = Bool
 
 data T = MkT { foo :: Int, bar :: B }
 
 data U a b = MkU { baf :: a }
+  deriving Show
 
 data family V a b c d
 data instance V x Int y [z] = MkVInt { baz :: (x, y, z, Bool) }
@@ -22,8 +27,16 @@ data W a where
   MkW :: { woo :: a } -> W [a]
 
 data Eq a => X a = MkX { xoo :: a }
+  deriving Show
 data Y a = Eq a => MkY { yoo :: a }
 
+data Z = MkZ1 { partial :: Int, total :: Bool }
+       | MkZ2 { total :: Bool }
+  deriving Show
+
+s :: S ((), Bool)
+s = MkS (Right True)
+
 t = MkT 42 True
 
 u :: U Char Char
@@ -37,15 +50,28 @@ x = MkX True
 
 y = MkY True
 
+z = MkZ2 False
+
 -- A virtual foo field for U
 instance HasField "foo" (U a b) [Char] where
-  getField _ = "virtual"
+  hasField r = (const r, "virtual")
 
-main = do print (getField @"foo" t)
+main = do print (getField @"soo" s)
+          print (getField @"foo" t)
+          print (getField @"foo" (setField @"foo" t 11))
           print (getField @"bar" t)
+          print (getField @"bar" (setField @"bar" t False))
           print (getField @"baf" u)
+          print (setField @"baf" u 'y')
           print (getField @"foo" u)
+          print (setField @"foo" u "ignored")
           print (getField @"baz" v)
+          print (getField @"baz" (setField @"baz" v (40 :: Int, 'y', False, True)))
           print (getField @"woo" w)
+          print (getField @"woo" (setField @"woo" w False))
           print (getField @"xoo" x)
+          print (setField @"xoo" x False)
           print (getField @"yoo" y)
+          print (getField @"yoo" (setField @"yoo" y False))
+          print (getField @"total" (setField @"total" z True))
+          print (setField @"partial" z 42)  -- Should throw a "No match" error


=====================================
testsuite/tests/overloadedrecflds/should_run/hasfieldrun01.stderr
=====================================
@@ -0,0 +1 @@
+hasfieldrun01: No match in record selector partial


=====================================
testsuite/tests/overloadedrecflds/should_run/hasfieldrun01.stdout
=====================================
@@ -1,8 +1,18 @@
+Right True
 42
+11
 True
+False
 'x'
+MkU {baf = 'y'}
 "virtual"
+MkU {baf = 'x'}
 (42,'x',True,False)
+(40,'y',False,True)
 True
+False
 True
+MkX {xoo = False}
+True
+False
 True


=====================================
testsuite/tests/overloadedrecflds/should_run/hasfieldrun03.hs
=====================================
@@ -0,0 +1,33 @@
+  -- This tests an example included in the GHC user's guide (see hasfield.rst).
+  -- Please update the user's guide if it needs to be changed!
+
+  {-# LANGUAGE DataKinds #-}
+  {-# LANGUAGE FlexibleContexts #-}
+  {-# LANGUAGE GADTs #-}
+  {-# LANGUAGE PolyKinds #-}
+  {-# LANGUAGE ScopedTypeVariables #-}
+  {-# LANGUAGE TypeApplications #-}
+  {-# LANGUAGE TypeOperators #-}
+  {-# LANGUAGE UndecidableInstances #-}
+
+  import Data.Kind (Type)
+  import Data.Proxy (Proxy(..))
+  import GHC.Records
+
+  data Record (xs :: [(k, Type)]) where
+    Nil  :: Record '[]
+    Cons :: Proxy x -> a -> Record xs -> Record ('(x, a) ': xs)
+
+  instance {-# OVERLAPS #-} HasField x (Record ('(x, a) ': xs)) a where
+    hasField (Cons p v r) = (\v' -> Cons p v' r, v)
+  instance HasField x (Record xs) a => HasField x (Record ('(y, b) ': xs)) a where
+    hasField (Cons p v r) = (\v' -> Cons p v (set v'), a)
+      where
+        (set,a) = hasField @x r
+
+  r :: Record '[ '("name", String) ]
+  r = Cons Proxy "R" Nil
+
+  x = getField @"name" (setField @"name" r "S")
+
+  main = print x


=====================================
testsuite/tests/overloadedrecflds/should_run/hasfieldrun03.stdout
=====================================
@@ -0,0 +1 @@
+"S"


=====================================
testsuite/tests/overloadedrecflds/should_run/overloadedrecfldsrun07.hs
=====================================
@@ -6,6 +6,7 @@
            , MultiParamTypeClasses
            , OverloadedLabels
            , ScopedTypeVariables
+           , StandaloneDeriving
            , TypeApplications
            , TypeOperators
            , UndecidableInstances
@@ -15,20 +16,29 @@ import GHC.OverloadedLabels
 import GHC.Records
 import GHC.TypeLits
 import Data.Kind
+import Data.Proxy
 
 data Label (x :: Symbol) = Label
+
+instance KnownSymbol x => Show (Label x) where
+  show _ = "#" ++ symbolVal (Proxy @x)
+
 data Labelled x a = Label x := a
+  deriving Show
 
 data Rec :: forall k. [(k, Type)] -> Type where
   Nil  :: Rec '[]
   (:>) :: Labelled x a -> Rec xs -> Rec ('(x, a) ': xs)
+instance Show (Rec '[]) where
+  show Nil = "Nil"
+deriving instance (KnownSymbol x, Show a, Show (Rec xs)) => Show (Rec ('(x, a) ': xs))
 infixr 5 :>
 
 instance {-# OVERLAPS #-} a ~ b => HasField foo (Rec ('(foo, a) ': xs)) b where
-  getField ((_ := v) :> _) = v
+  hasField ((l := v) :> xs) = (\ v' -> (l := v') :> xs, v)
 
 instance HasField foo (Rec xs) b => HasField foo (Rec ('(bar, a) ': xs)) b where
-  getField (_ :> vs) = getField @foo vs
+  hasField (x :> vs) = (\ v -> x :> setField @foo vs v, getField @foo vs)
 
 instance y ~ x => IsLabel y (Label x) where
   fromLabel = Label
@@ -44,3 +54,4 @@ y = #bar := 'x' :> undefined
 main = do print (#foo x)
           print (#bar x)
           print (#bar y)
+          print (setField @"foo" x 11)


=====================================
testsuite/tests/overloadedrecflds/should_run/overloadedrecfldsrun07.stdout
=====================================
@@ -1,3 +1,4 @@
 42
 True
 'x'
+#foo := 11 :> (#bar := True :> Nil)


=====================================
testsuite/tests/parser/should_compile/T14189.stderr
=====================================
@@ -134,6 +134,7 @@
          (FieldLabel
           {FastString: "f"}
           (False)
+          (())
           {Name: T14189.f}))]))
      [(AvailTC
        {Name: T14189.MyType}
@@ -142,6 +143,7 @@
        [(FieldLabel
          {FastString: "f"}
          (False)
+         (())
          {Name: T14189.f})])])])
   (Nothing)))
 


=====================================
testsuite/tests/typecheck/should_fail/T17355.hs
=====================================
@@ -8,4 +8,4 @@ data Foo = Foo { poly :: forall a. a -> a }
 
 instance Generic (forall a . a)
 instance HasField "myPoly" Foo (forall a. a -> a) where
-    getField (Foo x) = x
+    hasField (Foo x) = (undefined, x)



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/fd42d100ea2701fc103e7766262db3f793625cd5...d32a697da0445cdda59ac72fa23fb54b8952475f

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/fd42d100ea2701fc103e7766262db3f793625cd5...d32a697da0445cdda59ac72fa23fb54b8952475f
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200925/8d1b6b34/attachment-0001.html>


More information about the ghc-commits mailing list