771506b · generic-lens

generic-lens.cabal+1−1

compare with master

unifiedsplit

@@ -59,11 +59,11 @@ library

59 , Data.Generics.Sum.Internal.Subtype

60

61 , Data.Generics.Product.Internal.Positions

62+ , Data.Generics.Product.Internal.GLens

62 , Data.Generics.Product.Internal.Subtype

63 , Data.Generics.Product.Internal.Subtype

63

64

64 , Data.Generics.Product.Internal.Constraints

65 , Data.Generics.Product.Internal.Constraints

65 , Data.Generics.Product.Internal.List

66 , Data.Generics.Product.Internal.List

66− , Data.Generics.Product.Internal.Keyed

67

68 build-depends: base >= 4.9 && <= 5.0

69 , profunctors >= 5.0 && <= 6.0

src/Data/Generics/Internal/Families/Has.hs+52−9

@@ -16,6 +16,9 @@

16-----------------------------------------------------------------------------

17module Data.Generics.Internal.Families.Has

18 ( HasTotalFieldP

19+ , HasTotalTypeP

20+ , HasTotalPositionP

21+ , Pos

19 , HasPartialTypeP

22 , HasPartialTypeP

20 , HasCtorP

23 , HasCtorP

21 , GTypes

24 , GTypes

@@ -24,10 +27,13 @@ module Data.Generics.Internal.Families.Has

24import Data.Type.Bool (type (||), type (&&))

27import Data.Type.Bool (type (||), type (&&))

25import Data.Type.Equality (type (==))

28import Data.Type.Equality (type (==))

26import GHC.Generics

29import GHC.Generics

27−import GHC.TypeLits (Symbol, TypeError, ErrorMessage (..))

30+import GHC.TypeLits (Symbol, Nat)

31+import Data.Kind (Type)

28

32

29import Data.Generics.Product.Internal.List

33import Data.Generics.Product.Internal.List

30

34

35+-- Note: these could be factored out into a single traversal

36+

31type family HasTotalFieldP (field :: Symbol) f :: Bool where

37type family HasTotalFieldP (field :: Symbol) f :: Bool where

32 HasTotalFieldP field (S1 ('MetaSel ('Just field) _ _ _) _)

38 HasTotalFieldP field (S1 ('MetaSel ('Just field) _ _ _) _)

33 = 'True

39 = 'True

@@ -41,17 +47,54 @@ type family HasTotalFieldP (field :: Symbol) f :: Bool where

41 = HasTotalFieldP field f

47 = HasTotalFieldP field f

42 HasTotalFieldP field (D1 _ f)

48 HasTotalFieldP field (D1 _ f)

43 = HasTotalFieldP field f

49 = HasTotalFieldP field f

44− HasTotalFieldP field (Rec0 _)

50+ HasTotalFieldP field (K1 _ _)

45 = 'False

51 = 'False

46 HasTotalFieldP field U1

52 HasTotalFieldP field U1

47 = 'False

53 = 'False

48 HasTotalFieldP field V1

54 HasTotalFieldP field V1

49 = 'False

55 = 'False

50− HasTotalFieldP field f

56+

51− = TypeError

57+type family HasTotalTypeP (typ :: Type) f :: Bool where

52− ( 'ShowType f

58+ HasTotalTypeP typ (S1 _ (K1 _ typ))

53− ':<>: 'Text " is not a valid GHC.Generics representation type"

59+ = 'True

54− )

60+ HasTotalTypeP typ (l :*: r)

61+ = HasTotalTypeP typ l || HasTotalTypeP typ r

62+ HasTotalTypeP typ (l :+: r)

63+ = HasTotalTypeP typ l && HasTotalTypeP typ r

64+ HasTotalTypeP typ (S1 _ _)

65+ = 'False

66+ HasTotalTypeP typ (C1 _ f)

67+ = HasTotalTypeP typ f

68+ HasTotalTypeP typ (D1 _ f)

69+ = HasTotalTypeP typ f

70+ HasTotalTypeP typ (K1 _ _)

71+ = 'False

72+ HasTotalTypeP typ U1

73+ = 'False

74+ HasTotalTypeP typ V1

75+ = 'False

76+

77+data Pos (p :: Nat)

78+

79+type family HasTotalPositionP (pos :: Nat) f :: Bool where

80+ HasTotalPositionP pos (S1 _ (K1 (Pos pos) _))

81+ = 'True

82+ HasTotalPositionP pos (l :*: r)

83+ = HasTotalPositionP pos l || HasTotalPositionP pos r

84+ HasTotalPositionP pos (l :+: r)

85+ = HasTotalPositionP pos l && HasTotalPositionP pos r

86+ HasTotalPositionP pos (S1 _ _)

87+ = 'False

88+ HasTotalPositionP pos (C1 _ f)

89+ = HasTotalPositionP pos f

90+ HasTotalPositionP pos (D1 _ f)

91+ = HasTotalPositionP pos f

92+ HasTotalPositionP pos (K1 _ _)

93+ = 'False

94+ HasTotalPositionP pos U1

95+ = 'False

96+ HasTotalPositionP pos V1

97+ = 'False

55

98

56type family HasPartialTypeP a f :: Bool where

99type family HasPartialTypeP a f :: Bool where

57 HasPartialTypeP t (l :+: r)

100 HasPartialTypeP t (l :+: r)

@@ -73,10 +116,10 @@ type family HasCtorP (ctor :: Symbol) f :: Bool where

73 HasCtorP ctor _

116 HasCtorP ctor _

74 = 'False

117 = 'False

75

118

76−type family GTypes (rep :: * -> *) :: [((), *)] where

119+type family GTypes (rep :: Type -> Type) :: [((), Type)] where

77 GTypes (l :*: r)

120 GTypes (l :*: r)

78 = GTypes l ++ GTypes r

121 = GTypes l ++ GTypes r

79− GTypes (Rec0 a)

122+ GTypes (K1 _ a)

80 = '[ '( '(), a)]

123 = '[ '( '(), a)]

81 GTypes (M1 _ m a)

124 GTypes (M1 _ m a)

82 = GTypes a

125 = GTypes a

src/Data/Generics/Product/Fields.hs+10−8

@@ -40,7 +40,7 @@ module Data.Generics.Product.Fields

40import Data.Generics.Internal.Families

41import Data.Generics.Internal.VL.Lens as VL

42import Data.Generics.Internal.Void

43−import Data.Generics.Product.Internal.Keyed

43+import Data.Generics.Product.Internal.GLens

44

45import Data.Kind (Constraint, Type)

46import GHC.Generics

@@ -129,9 +129,9 @@ setField = VL.set (field' @f)

129instance

130 ( Generic s

131 , ErrorUnless field s (CollectField field (Rep s))

132− , GHasKey' field (Rep s) a

132+ , GLens' (HasTotalFieldPSym field) (Rep s) a

133 ) => HasField' field s a where

134− field' f s = VL.ravel (repLens . gkey @field) f s

134+ field' f s = VL.ravel (repLens . glens @(HasTotalFieldPSym field)) f s

135

136instance -- see Note [Changing type parameters]

137 ( Generic s

@@ -146,14 +146,13 @@ instance -- see Note [Changing type parameters]

146#endif

147 , Generic s'

148 , Generic t'

149− , GHasKey' field (Rep s) a

149+ , GLens' (HasTotalFieldPSym field) (Rep s') a'

150− , GHasKey' field (Rep s') a'

151− , GHasKey' field (Rep t') b'

150+ , GLens' (HasTotalFieldPSym field) (Rep t') b'

152− , GHasKey field (Rep s) (Rep t) a b

151+ , GLens (HasTotalFieldPSym field) (Rep s) (Rep t) a b

153 , t ~ Infer s a' b

152 , t ~ Infer s a' b

154 , s ~ Infer t b' a

153 , s ~ Infer t b' a

155 ) => HasField field s t a b where

154 ) => HasField field s t a b where

156− field f s = VL.ravel (repLens . gkey @field) f s

155+ field f s = VL.ravel (repLens . glens @(HasTotalFieldPSym field)) f s

157

156

158-- -- See Note [Uncluttering type signatures]

157-- -- See Note [Uncluttering type signatures]

159instance {-# OVERLAPPING #-} HasField f (Void1 a) (Void1 b) a b where

158instance {-# OVERLAPPING #-} HasField f (Void1 a) (Void1 b) a b where

@@ -180,3 +179,6 @@ type family ErrorUnless (field :: Symbol) (s :: Type) (stat :: TypeStat) :: Cons

180

179

181 ErrorUnless _ _ ('TypeStat '[] '[] _)

180 ErrorUnless _ _ ('TypeStat '[] '[] _)

182 = ()

181 = ()

182+

183+data HasTotalFieldPSym :: Symbol -> (TyFun (Type -> Type) Bool)

184+type instance Eval (HasTotalFieldPSym sym) tt = HasTotalFieldP sym tt

src/Data/Generics/Product/Internal/GLens.hsnew file+79

@@ -0,0 +1,79 @@

1+{-# LANGUAGE FlexibleContexts #-}

2+{-# LANGUAGE TypeInType #-}

3+{-# LANGUAGE AllowAmbiguousTypes #-}

4+{-# LANGUAGE ConstraintKinds #-}

5+{-# LANGUAGE DataKinds #-}

6+{-# LANGUAGE FlexibleInstances #-}

7+{-# LANGUAGE FunctionalDependencies #-}

8+{-# LANGUAGE KindSignatures #-}

9+{-# LANGUAGE MultiParamTypeClasses #-}

10+{-# LANGUAGE Rank2Types #-}

11+{-# LANGUAGE ScopedTypeVariables #-}

12+{-# LANGUAGE TypeApplications #-}

13+{-# LANGUAGE TypeFamilies #-}

14+{-# LANGUAGE TypeOperators #-}

15+{-# LANGUAGE UndecidableInstances #-}

16+

17+-----------------------------------------------------------------------------

18+-- |

19+-- Module : Data.Generics.Product.Internal.GLens

21+-- License : BSD3

22+-- Maintainer : Csongor Kiss <kiss.csongor.kiss@gmail.com>

23+-- Stability : experimental

24+-- Portability : non-portable

25+--

26+-- Derive record field getters and setters generically.

27+--

28+-----------------------------------------------------------------------------

29+

30+module Data.Generics.Product.Internal.GLens

31+ ( GLens (..)

32+ , GLens'

33+ , TyFun

34+ , Eval

35+ ) where

36+

37+import Data.Generics.Internal.Profunctor.Lens (Lens, choosing, first, second)

38+import Data.Generics.Internal.Profunctor.Iso (kIso, sumIso, mIso)

39+

40+import Data.Kind (Type)

41+import GHC.Generics

42+

43+type TyFun a b = a -> b -> Type

44+type family Eval (f :: TyFun a b) (x :: a) :: b

45+

46+-- A generic lens that uses some predicate to determine which field to focus on

47+class GLens (pred :: TyFun (Type -> Type) Bool) (s :: Type -> Type) (t :: Type -> Type) a b | s pred -> a, t pred -> b where

48+ glens :: Lens (s x) (t x) a b

49+

50+type GLens' pred s a = GLens pred s s a a

51+

52+instance GProductLens (Eval pred l) pred l r l' r' a b

53+ => GLens pred (l :*: r) (l' :*: r') a b where

54+

55+ glens = gproductField @(Eval pred l) @pred

56+ {-# INLINE glens #-}

57+

58+instance (GLens pred l l' a b, GLens pred r r' a b) => GLens pred (l :+: r) (l' :+: r') a b where

59+ glens = sumIso . choosing (glens @pred) (glens @pred)

60+ {-# INLINE glens #-}

61+

62+instance GLens pred (K1 r a) (K1 r b) a b where

63+ glens = kIso

64+ {-# INLINE glens #-}

65+

66+instance (Functor g, GLens pred f g a b) => GLens pred (M1 m meta f) (M1 m meta g) a b where

67+ glens = mIso . glens @pred

68+ {-# INLINE glens #-}

69+

70+class GProductLens (left :: Bool) (pred :: TyFun (Type -> Type) Bool) l r l' r' a b | pred l r -> a, pred l' r' -> b where

71+ gproductField :: Lens ((l :*: r) x) ((l' :*: r') x) a b

72+

73+instance GLens pred l l' a b => GProductLens 'True pred l r l' r a b where

74+ gproductField = first . glens @pred

75+ {-# INLINE gproductField #-}

76+

77+instance GLens pred r r' a b => GProductLens 'False pred l r l r' a b where

78+ gproductField = second . glens @pred

79+ {-# INLINE gproductField #-}

src/Data/Generics/Product/Internal/Keyed.hsdeleted−60

@@ -1,60 +0,0 @@

1−{-# LANGUAGE AllowAmbiguousTypes #-}

2−{-# LANGUAGE CPP #-}

3−{-# LANGUAGE ConstraintKinds #-}

4−{-# LANGUAGE FlexibleInstances #-}

5−{-# LANGUAGE FunctionalDependencies #-}

6−{-# LANGUAGE GADTs #-}

7−{-# LANGUAGE ScopedTypeVariables #-}

8−{-# LANGUAGE TypeApplications #-}

9−{-# LANGUAGE TypeFamilies #-}

10−{-# LANGUAGE TypeInType #-}

11−{-# LANGUAGE TypeOperators #-}

12−{-# LANGUAGE UndecidableInstances #-}

13−

14−#if __GLASGOW_HASKELL__ == 802

15−{-# OPTIONS_GHC -fno-solve-constant-dicts #-}

16−#endif

17−

18−--------------------------------------------------------------------------------

19−-- |

20−-- Module : Data.Generics.Product.Internal.Keyed

22−-- Maintainer : Csongor Kiss <kiss.csongor.kiss@gmail.com>

23−-- License : BSD3

24−-- Stability : experimental

25−-- Portability : non-portable

26−--

27−--------------------------------------------------------------------------------

28−

29−module Data.Generics.Product.Internal.Keyed

30− ( GHasKey (..)

31− , GHasKey'

32− ) where

33−

34−import Data.Generics.Product.Internal.List

35−import Data.Kind

36−import GHC.Generics

37−import Data.Generics.Internal.Profunctor.Lens

38−import Data.Generics.Internal.Profunctor.Iso

39−

40−class GHasKey (key :: k) (s :: Type -> Type) (t :: Type -> Type) a b | s key -> a, t key -> b where

41− gkey :: Lens (s x) (t x) a b

42−

43−type GHasKey' key s a = GHasKey key s s a a

44−

45−instance (GHasKey key l l' a b, GHasKey key r r' a b) => GHasKey key (l :+: r) (l' :+: r') a b where

46− gkey = sumIso . choosing (gkey @key) (gkey @key)

47− {-# INLINE gkey #-}

48−

49−instance (GHasKey key f g a b) => GHasKey key (M1 D meta f) (M1 D meta g) a b where

50− gkey = ravel (mLens . gkey @key)

51− {-# INLINE gkey #-}

52−

53−instance

54− ( Elem as key i a

55− , Elem bs key i b

56− , IndexList i as bs a b

57− , GIsList k f g as bs

58− ) => GHasKey (key :: k) (M1 C meta f) (M1 C meta g) a b where

59− gkey = mLens . glist @k . point @i

60− {-# INLINE gkey #-}

src/Data/Generics/Product/Internal/List.hs+3−1

@@ -40,8 +40,10 @@ module Data.Generics.Product.Internal.List

40 , TupleToList

41 ) where

42

43−import GHC.TypeLits

43+#if __GLASGOW_HASKELL__ < 804

44import Data.Semigroup

45+#endif

46+import GHC.TypeLits

45

47

46import Data.Kind (Type)

48import Data.Kind (Type)

47import GHC.Generics

49import GHC.Generics

src/Data/Generics/Product/Internal/Positions.hs+45−26

@@ -1,3 +1,4 @@

1+{-# LANGUAGE TypeInType #-}

1{-# LANGUAGE AllowAmbiguousTypes #-}

2{-# LANGUAGE AllowAmbiguousTypes #-}

2{-# LANGUAGE ConstraintKinds #-}

3{-# LANGUAGE ConstraintKinds #-}

3{-# LANGUAGE DataKinds #-}

4{-# LANGUAGE DataKinds #-}

@@ -27,41 +28,61 @@

27-----------------------------------------------------------------------------

28-----------------------------------------------------------------------------

28

29

29module Data.Generics.Product.Internal.Positions

30module Data.Generics.Product.Internal.Positions

30− ( GHasPosition (..)

31− , GHasPosition'

32− , type (<?)

31+ ( type (<?)

33 , Size

32 , Size

33+ , CRep

34 ) where

35

36−import Data.Generics.Product.Internal.List

36+import Data.Generics.Internal.Families.Has (Pos)

37import Data.Kind (Type)

38import Data.Type.Bool (If, Not)

39import GHC.Generics

40−import GHC.TypeLits (type (<=?), type (+), type (-), Nat)

40+import GHC.TypeLits (type (<=?), type (+), Nat)

41−import Data.Generics.Internal.Profunctor.Lens

42−import Data.Generics.Internal.Profunctor.Iso

43

41

44−-- |As 'HasPosition' but over generic representations as defined by

42+-- | Alias for the kind of the generic rep

45−-- "GHC.Generics".

43+type G k = k -> Type

46−class GHasPosition (i :: Nat) (s :: Type -> Type) (t :: Type -> Type) a b | s i -> a, t i -> b, s t i -> b where

47− gposition :: Lens (s x) (t x) a b

48

44

49−type GHasPosition' i s a = GHasPosition i s s a a

45+--------------------------------------------------------------------------------

50

46

51−instance (GHasPosition i l l' a b, GHasPosition i r r' a b) => GHasPosition i (l :+: r) (l' :+: r') a b where

47+-- | In-order labeling of the generic tree with the field positions

52− gposition = \x -> sumIso (choosing (gposition @i) (gposition @i) x)

48+--

53− {-# INLINE gposition #-}

49+-- We replace the (K1 R a) nodes with (K1 (Pos n) a), where 'n' is the position

50+-- of the field in question in the data type. This is convenient, because we

51+-- can reuse all the existing functions as long as they are polymorphic in the

52+-- first parameter of 'K1'.

53+type family CRep (a :: Type) :: G k where

54+ CRep rep = Fst (Traverse (Rep rep) 1)

54

55

55−instance GHasPosition i s t a b => GHasPosition i (M1 D meta s) (M1 D meta t) a b where

56+-- | The actual traversal.

56− gposition x = mLens (gposition @i x)

57+--

57− {-# INLINE gposition #-}

58+-- Might be cleaner if the sum and product parts were separated (as there's

59+-- and invariant that 'n' should be zero when we're at a sum node, which holds

60+-- for derived Generic instances (where the sums are strictly above the products))

61+type family Traverse (a :: G k) (n :: Nat) :: (G k, Nat) where

62+ Traverse (M1 mt m s) n

63+ = Traverse1 (M1 mt m) (Traverse s n)

64+ Traverse (l :+: r) n

65+ = '(Fst (Traverse l n) :+: Fst (Traverse r n), n)

66+ Traverse (l :*: r) n

67+ = TraverseProd (:*:) (Traverse l n) r

68+ Traverse (K1 _ p) n

69+ = '(K1 (Pos n) p, n + 1)

70+ Traverse U1 n

71+ = '(U1, n)

58

72

59−instance

73+type family Traverse1 (w :: G k -> G k) (z :: (G k, Nat)) :: (G k, Nat) where

60− ( IndexList (i - 1) as bs a b

74+ Traverse1 w '(i, n) = '(w i, n)

61− , GIsList () f g as bs

75+

62− ) => GHasPosition i (M1 C meta f) (M1 C meta g) a b where

76+-- | For products, we first traverse the left-hand side, followed by the second

63− gposition x = mIso (glist @() (point @(i - 1) x))

77+-- using the counter returned by the left traversal.

64− {-# INLINE gposition #-}

78+type family TraverseProd (c :: G k -> G k -> G k) (a :: (G k, Nat)) (r :: G k) :: (G k, Nat) where

79+ TraverseProd w '(i, n) r = Traverse1 (w i) (Traverse r n)

80+

81+--------------------------------------------------------------------------------

82+-- Utilities

83+

84+type family Fst (p :: (a, b)) :: a where

85+ Fst '(a, b) = a

65

86

66type family Size f :: Nat where

87type family Size f :: Nat where

67 Size (l :*: r)

88 Size (l :*: r)

@@ -75,8 +96,6 @@ type family Size f :: Nat where

75 Size f

96 Size f

76 = 1

97 = 1

77

98

78−--------------------------------------------------------------------------------

79−

80type x <? y = Not (y <=? x)

99type x <? y = Not (y <=? x)

81infixl 4 <?

100infixl 4 <?

82

101

src/Data/Generics/Product/Internal/Subtype.hs+11−6

@@ -1,3 +1,4 @@

1+{-# LANGUAGE TypeInType #-}

1{-# LANGUAGE AllowAmbiguousTypes #-}

2{-# LANGUAGE AllowAmbiguousTypes #-}

2{-# LANGUAGE DataKinds #-}

3{-# LANGUAGE DataKinds #-}

3{-# LANGUAGE FlexibleContexts #-}

4{-# LANGUAGE FlexibleContexts #-}

@@ -31,11 +32,12 @@ module Data.Generics.Product.Internal.Subtype

31 ) where

32 ) where

32

33

33import Data.Generics.Internal.Families

34import Data.Generics.Internal.Families

34−import Data.Generics.Product.Internal.Keyed

35+import Data.Generics.Product.Internal.GLens

35

36

36import Data.Kind (Type)

37import Data.Kind (Type)

37import GHC.Generics

38import GHC.Generics

39+import GHC.TypeLits (Symbol)

38−import Data.Generics.Internal.Profunctor.Lens

40+import Data.Generics.Internal.Profunctor.Lens (view)

39

41

40--------------------------------------------------------------------------------

42--------------------------------------------------------------------------------

41-- * Generic upcasting

43-- * Generic upcasting

@@ -47,10 +49,10 @@ instance (GUpcast sub a, GUpcast sub b) => GUpcast sub (a :*: b) where

47 gupcast rep = gupcast rep :*: gupcast rep

49 gupcast rep = gupcast rep :*: gupcast rep

48

50

49instance

51instance

50− GHasKey field sub sub t t

52+ GLens' (HasTotalFieldPSym field) sub t

51 => GUpcast sub (S1 ('MetaSel ('Just field) p f b) (Rec0 t)) where

53 => GUpcast sub (S1 ('MetaSel ('Just field) p f b) (Rec0 t)) where

52

54

53− gupcast r = M1 (K1 (view (gkey @field) r))

55+ gupcast r = M1 (K1 (view (glens @(HasTotalFieldPSym field)) r))

54

56

55instance GUpcast sub sup => GUpcast sub (C1 c sup) where

57instance GUpcast sub sup => GUpcast sub (C1 c sup) where

56 gupcast = M1 . gupcast

58 gupcast = M1 . gupcast

@@ -84,9 +86,12 @@ class GSmashLeaf sub sup (w :: Bool) where

84 gsmashLeaf :: sup p -> sub p -> sub p

86 gsmashLeaf :: sup p -> sub p -> sub p

85

87

86instance

88instance

87− GHasKey field sup sup t t

89+ GLens' (HasTotalFieldPSym field) sup t

88 => GSmashLeaf (S1 ('MetaSel ('Just field) p f b) (Rec0 t)) sup 'True where

90 => GSmashLeaf (S1 ('MetaSel ('Just field) p f b) (Rec0 t)) sup 'True where

89− gsmashLeaf sup _ = M1 (K1 (view (gkey @field) sup))

91+ gsmashLeaf sup _ = M1 (K1 (view (glens @(HasTotalFieldPSym field)) sup))

90

92

91instance GSmashLeaf (S1 ('MetaSel ('Just field) p f b) (Rec0 t)) sup 'False where

93instance GSmashLeaf (S1 ('MetaSel ('Just field) p f b) (Rec0 t)) sup 'False where

92 gsmashLeaf _ = id

94 gsmashLeaf _ = id

95+

96+data HasTotalFieldPSym :: Symbol -> (TyFun (Type -> Type) Bool)

97+type instance Eval (HasTotalFieldPSym sym) tt = HasTotalFieldP sym tt

src/Data/Generics/Product/Positions.hs+28−8

@@ -1,3 +1,5 @@

1+{-# LANGUAGE TypeInType #-}

2+{-# LANGUAGE PartialTypeSignatures #-}

1{-# LANGUAGE CPP #-}

3{-# LANGUAGE CPP #-}

2{-# LANGUAGE AllowAmbiguousTypes #-}

4{-# LANGUAGE AllowAmbiguousTypes #-}

3{-# LANGUAGE ConstraintKinds #-}

5{-# LANGUAGE ConstraintKinds #-}

@@ -42,12 +44,14 @@ import Data.Generics.Internal.VL.Lens as VL

42import Data.Generics.Internal.Void

44import Data.Generics.Internal.Void

43import Data.Generics.Internal.Families

45import Data.Generics.Internal.Families

44import Data.Generics.Product.Internal.Positions

46import Data.Generics.Product.Internal.Positions

47+import Data.Generics.Product.Internal.GLens

45

48

46import Data.Kind (Constraint, Type)

49import Data.Kind (Constraint, Type)

47import Data.Type.Bool (type (&&))

50import Data.Type.Bool (type (&&))

48import GHC.Generics

51import GHC.Generics

49import GHC.TypeLits (type (<=?), Nat, TypeError, ErrorMessage(..))

52import GHC.TypeLits (type (<=?), Nat, TypeError, ErrorMessage(..))

50−import Data.Generics.Internal.Profunctor.Lens

53+import Data.Generics.Internal.Profunctor.Lens as P

54+import Data.Coerce

51

55

52-- $setup

56-- $setup

53-- == /Running example:/

57-- == /Running example:/

@@ -101,9 +105,11 @@ setPosition = VL.set (position' @i)

101instance

105instance

102 ( Generic s

106 ( Generic s

103 , ErrorUnless i s (0 <? i && i <=? Size (Rep s))

107 , ErrorUnless i s (0 <? i && i <=? Size (Rep s))

104− , GHasPosition' i (Rep s) a

108+ , cs ~ CRep s

109+ , Coercible (Rep s) cs

110+ , GLens' (HasTotalPositionPSym i) cs a

105 ) => HasPosition' i s a where

111 ) => HasPosition' i s a where

106− position' f s = VL.ravel (repLens . gposition @i) f s

112+ position' f s = VL.ravel (repLens . coerced @cs @cs . glens @(HasTotalPositionPSym i)) f s

107 {-# INLINE position' #-}

113 {-# INLINE position' #-}

108

114

109instance -- see Note [Changing type parameters]

115instance -- see Note [Changing type parameters]

@@ -119,17 +125,28 @@ instance -- see Note [Changing type parameters]

119#endif

125#endif

120 , Generic s'

126 , Generic s'

121 , Generic t'

127 , Generic t'

122− , GHasPosition' i (Rep s) a

128+ , GLens (HasTotalPositionPSym i) cs ct a b

123− , GHasPosition' i (Rep s') a'

129+ , cs ~ CRep s

124− , GHasPosition i (Rep s) (Rep t) a b

130+ , ct ~ CRep t

131+ , GLens' (HasTotalPositionPSym i) (CRep s') a'

132+ , GLens' (HasTotalPositionPSym i) (CRep t') b'

125 , t ~ Infer s a' b

133 , t ~ Infer s a' b

126− , GHasPosition' i (Rep t') b'

127 , s ~ Infer t b' a

134 , s ~ Infer t b' a

135+ , Coercible cs (Rep s)

136+ , Coercible ct (Rep t)

128 ) => HasPosition i s t a b where

137 ) => HasPosition i s t a b where

129

138

130− position = VL.ravel (repLens . gposition @i)

139+ position = VL.ravel (repLens . coerced @cs @ct . glens @(HasTotalPositionPSym i))

131 {-# INLINE position #-}

140 {-# INLINE position #-}

132

141

142+-- We wouldn't need the universal 'x' here if we could express above that

143+-- forall x. Coercible (cs x) (Rep s x), but this requires quantified

144+-- constraints

145+coerced :: forall s t s' t' x a b. (Coercible t t', Coercible s s')

146+ => P.ALens a b (s x) (t x) -> P.ALens a b (s' x) (t' x)

147+coerced = coerce

148+{-# INLINE coerced #-}

149+

133-- See Note [Uncluttering type signatures]

150-- See Note [Uncluttering type signatures]

134instance {-# OVERLAPPING #-} HasPosition f (Void1 a) (Void1 b) a b where

151instance {-# OVERLAPPING #-} HasPosition f (Void1 a) (Void1 b) a b where

135 position = undefined

152 position = undefined

@@ -145,3 +162,6 @@ type family ErrorUnless (i :: Nat) (s :: Type) (hasP :: Bool) :: Constraint wher

145

162

146 ErrorUnless _ _ 'True

163 ErrorUnless _ _ 'True

147 = ()

164 = ()

165+

166+data HasTotalPositionPSym :: Nat -> (TyFun (Type -> Type) Bool)

167+type instance Eval (HasTotalPositionPSym t) tt = HasTotalPositionP t tt

src/Data/Generics/Product/Typed.hs+8−3

@@ -7,6 +7,7 @@

7{-# LANGUAGE ScopedTypeVariables #-}

8{-# LANGUAGE TypeApplications #-}

9{-# LANGUAGE TypeFamilies #-}

10+{-# LANGUAGE TypeInType #-}

10{-# LANGUAGE TypeOperators #-}

11{-# LANGUAGE TypeOperators #-}

11{-# LANGUAGE UndecidableInstances #-}

12{-# LANGUAGE UndecidableInstances #-}

12

13

@@ -33,7 +34,7 @@ module Data.Generics.Product.Typed

33import Data.Generics.Internal.Families

34import Data.Generics.Internal.Families

34import Data.Generics.Internal.VL.Lens as VL

35import Data.Generics.Internal.VL.Lens as VL

35import Data.Generics.Internal.Void

36import Data.Generics.Internal.Void

36−import Data.Generics.Product.Internal.Keyed

37+import Data.Generics.Product.Internal.GLens

37

38

38import Data.Kind (Constraint, Type)

39import Data.Kind (Constraint, Type)

39import GHC.Generics (Generic (Rep))

40import GHC.Generics (Generic (Rep))

@@ -110,10 +111,10 @@ class HasType a s where

110instance

111instance

111 ( Generic s

112 ( Generic s

112 , ErrorUnlessOne a s (CollectTotalType a (Rep s))

113 , ErrorUnlessOne a s (CollectTotalType a (Rep s))

113− , GHasKey a (Rep s) (Rep s) a a

114+ , GLens (HasTotalTypePSym a) (Rep s) (Rep s) a a

114 ) => HasType a s where

115 ) => HasType a s where

115

116

116− typed f s = VL.ravel (repLens . gkey @a) f s

117+ typed f s = VL.ravel (repLens . glens @(HasTotalTypePSym a)) f s

117

118

118-- See Note [Uncluttering type signatures]

119-- See Note [Uncluttering type signatures]

119instance {-# OVERLAPPING #-} HasType a Void where

120instance {-# OVERLAPPING #-} HasType a Void where

@@ -150,3 +151,7 @@ type family ErrorUnlessOne (a :: Type) (s :: Type) (stat :: TypeStat) :: Constra

150

151

151 ErrorUnlessOne _ _ ('TypeStat '[] '[] _)

152 ErrorUnlessOne _ _ ('TypeStat '[] '[] _)

152 = ()

153 = ()

154+

155+data HasTotalTypePSym :: Type -> (TyFun (Type -> Type) Bool)

156+type instance Eval (HasTotalTypePSym t) tt = HasTotalTypeP t tt

157+