git.iko.soy/generic-lens
on master help sign in
Fix #23
c0e2c24Csongor Kiss
examples/Examples.hs+29−14
compare with master
unifiedsplit
@@ -1,17 +1,18 @@
1−{-# LANGUAGE AllowAmbiguousTypes #-}
1+{-# LANGUAGE AllowAmbiguousTypes #-}
2−{-# LANGUAGE DataKinds #-}
2+{-# LANGUAGE DataKinds #-}
3−{-# LANGUAGE DeriveGeneric #-}
3+{-# LANGUAGE DeriveGeneric #-}
4−{-# LANGUAGE DuplicateRecordFields #-}
4+{-# LANGUAGE DuplicateRecordFields #-}
5−{-# LANGUAGE FlexibleContexts #-}
5+{-# LANGUAGE FlexibleContexts #-}
6−{-# LANGUAGE GADTs #-}
6+{-# LANGUAGE GADTs #-}
7−{-# LANGUAGE NoMonomorphismRestriction #-}
7+{-# LANGUAGE NoMonomorphismRestriction #-}
8+{-# LANGUAGE OverloadedLabels #-}
8−{-# LANGUAGE PartialTypeSignatures #-}
9+{-# LANGUAGE PartialTypeSignatures #-}
9−{-# LANGUAGE Rank2Types #-}
10+{-# LANGUAGE Rank2Types #-}
10−{-# LANGUAGE ScopedTypeVariables #-}
11+{-# LANGUAGE ScopedTypeVariables #-}
11−{-# LANGUAGE TypeApplications #-}
12+{-# LANGUAGE TypeApplications #-}
12−{-# LANGUAGE UndecidableInstances #-}
13+{-# LANGUAGE UndecidableInstances #-}
13−{-# OPTIONS_GHC -Wno-missing-signatures #-}
14+{-# OPTIONS_GHC -Wno-missing-signatures #-}
14−{-# OPTIONS_GHC -fno-warn-unused-imports #-}
15+{-# OPTIONS_GHC -fno-warn-unused-imports #-}
15
16
16module Examples where
17module Examples where
17
18
@@ -110,3 +111,17 @@ stuff' ::
110 , HasField "bar" a' b' s t
111 , HasField "bar" a' b' s t
111 ) => s' -> t'
112 ) => s' -> t'
112stuff' r = r & #test . #bar . position @15 .~ "hello"
113stuff' r = r & #test . #bar . position @15 .~ "hello"
114+
115+data Foo m s = Foo
116+ { foo1 :: m s
117+ , foo2 :: [s]
118+ } deriving Generic
119+
120+modifyFoo2 :: Foo (Either String) Int -> Foo Maybe Int
121+modifyFoo2 x = x & field @"foo1" .~ pure (1 :: Int)
122+
123+data Bar a b = Bar
124+ { barField :: (a, b)
125+ } deriving Generic
126+
127+modifiedBar = (Bar ("hello", "world")) & field @"barField" .~ ('c', 1 :: Int)
src/Data/Generics/Internal/Families/Changing.hs+81−48
@@ -2,14 +2,19 @@
2{-# LANGUAGE DataKinds #-}
2{-# LANGUAGE DataKinds #-}
3{-# LANGUAGE FlexibleInstances #-}
3{-# LANGUAGE FlexibleInstances #-}
4{-# LANGUAGE FunctionalDependencies #-}
4{-# LANGUAGE FunctionalDependencies #-}
5+{-# LANGUAGE GADTs #-}
5{-# LANGUAGE PolyKinds #-}
6{-# LANGUAGE PolyKinds #-}
6{-# LANGUAGE TypeFamilies #-}
7{-# LANGUAGE TypeFamilies #-}
7{-# LANGUAGE TypeOperators #-}
8{-# LANGUAGE TypeOperators #-}
8{-# LANGUAGE UndecidableInstances #-}
9{-# LANGUAGE UndecidableInstances #-}
9
10
10−module Data.Generics.Internal.Families.Changing where
11+module Data.Generics.Internal.Families.Changing
12+ ( Proxied
13+ , Infer
14+ ) where
11
15
12−import GHC.TypeLits (Nat, type (+))
16+import GHC.TypeLits (TypeError, ErrorMessage (..))
17+import Data.Type.Bool (If)
13
18
14{-
19{-
15 Note [Changing type parameters]
20 Note [Changing type parameters]
@@ -35,53 +40,81 @@ import GHC.TypeLits (Nat, type (+))
35 If after doing the conversion on @s@, @field@'s type is @(P _ a), then @t@ is
40 If after doing the conversion on @s@, @field@'s type is @(P _ a), then @t@ is
36 @s[b/a]@, otherwise @t ~ s@ and @b ~ a@.
41 @s[b/a]@, otherwise @t ~ s@ and @b ~ a@.
37-}
42-}
38−data P (i :: Nat) a
39
43
40−type Proxied t = Proxied' t 0
44+-- `P` can be used in place of any type parameter, which means that it can have
45+-- any kind, not just *, so a data type won't work.
46+-- (this caused https://github.com/kcsongor/generic-lens/issues/23)
47+-- Instead, we use a matchable type family to wrap any `k` - however, we can no longer directly
48+-- pattern match on `P`, as it's not a type constructor. But we can still take it apart as a polymorphic
49+-- application form. In order to distinguish between applications of P and other type constructors, we use a tag, `PTag`
50+-- to fake a type constructor.
51+data PTag = PTag
52+type family P :: Peano -> k -> PTag -> k
41
53
54+type Proxied t = Proxied' t 'Z
55+
42−type family Proxied' (t :: k) (next :: Nat) :: k where
56+type family Proxied' (t :: k) (next :: Peano) :: k where
43− Proxied' (t a :: k) next = (Proxied' t (next + 1)) (P next a)
57+ Proxied' (t (a :: j) :: k) next = (Proxied' t ('S next)) (P next a 'PTag)
44 Proxied' t _ = t
58 Proxied' t _ = t
45
59
60+data Sub where
61+ Sub :: Peano -> k -> Sub
62+
63+type family Unify (a :: k) (b :: k) :: [Sub] where
64+ Unify (a b) a' = If (IsPTag b) '[Bar (a b) a'] (Baz (a b) a')
65+ Unify a a = '[]
66+ Unify a b = TypeError
67+ ( 'Text "Couldn't match type "
68+ ':<>: 'ShowType a
69+ ':<>: 'Text " with "
70+ ':<>: 'ShowType b
71+ )
72+
73+type family Bar a b where
74+ Bar (p n _ 'PTag) a' = 'Sub n a'
75+
76+type family Baz a b where
77+ Baz (a x) (b y) = Unify x y ++ Unify a b
78+ Baz a a = '[]
79+ Baz a b = TypeError
80+ ( 'Text "Couldn't match type "
81+ ':<>: 'ShowType a
82+ ':<>: 'Text " with "
83+ ':<>: 'ShowType b
84+ )
85+
86+type family IsPTag (a :: k) :: Bool where
87+ IsPTag 'PTag = 'True
88+ IsPTag _ = 'False
89+
90+type family (xs :: [k]) ++ (ys :: [k]) :: [k] where
91+ '[] ++ ys = ys
92+ (x ': xs) ++ ys = x ': (xs ++ ys)
93+
94+type family Infer (s :: *) (a' :: *) (b :: *) :: * where
95+ Infer s a' b
96+ = ReplaceArgs s (Unify a' b)
97+
98+--------------------------------------------------------------------------------
99+
100+data Peano = Z | S Peano
101+
102+-- [TODO]: work this out
103+--
46−type family UnProxied (t :: k) :: k where
104+--type family ArgKind (t :: k) (pos :: Peano) :: * where
47− UnProxied (P _ a) = a
105+-- ArgKind (t (a :: k)) 'Z = k
48− UnProxied (t (P _ a) :: k) = UnProxied t a
106+-- ArgKind (t _) ('S pos) = ArgKind t pos
49− UnProxied t = t
107+--
50−
108+--type family ReplaceArg (t :: k) (pos :: Peano) (to :: ArgKind t pos) :: k where
109+-- ReplaceArg (t a) 'Z to = t to
110+-- ReplaceArg (t a) ('S pos) to = ReplaceArg t pos to a
111+-- ReplaceArg t _ _ = t
112+
51−type family Change (t :: k) (target :: Nat) (to :: j) :: k where
113+type family ReplaceArg (t :: k) (pos :: Peano) (to :: j) :: k where
52− Change (P target _) target to = (P target to)
114+ ReplaceArg (t a) 'Z to = t to
53− Change (t (P target _) :: k) target to = t (P target to)
115+ ReplaceArg (t a) ('S pos) to = ReplaceArg t pos to a
54− Change (t a :: k) target to = Change t target to a
116+ ReplaceArg t _ _ = t
55− Change t _ _ = t
117+
56−
118+type family ReplaceArgs (t :: k) (subs :: [Sub]) :: k where
57−type family UnApply (a :: k) :: [*] where
119+ ReplaceArgs t '[] = t
58− UnApply (f x) = x ': UnApply f
120+ ReplaceArgs t ('Sub n arg ': ss) = ReplaceArgs (ReplaceArg t n arg) ss
59− UnApply x = '[]
60−
61−type family Unify a b :: [(*, *)] where
62− Unify (P n a') a = '[ '(P n a', a)]
63− Unify a b = Zip (UnApply a) (UnApply b)
64−
65−type family PSub (subs :: [(*, *)]) :: [(Nat, *)] where
66− PSub '[] = '[]
67− PSub ('(P n _, b) ': xs) = '(n, b) ': PSub xs
68− PSub (_ ': xs) = PSub xs
69−
70−type family Zip (xs :: [k]) (ys :: [l]) :: [(k, l)] where
71− Zip '[] '[] = '[]
72− Zip (x ': xs) (y ': ys) = '(x, y) ': Zip xs ys
73−
74−type family Infer (s :: *) (a' :: *) (a :: *) (w :: *) :: (*, *) where
75− Infer s' a' a w
76− = Infer' s' a' (PSub (Unify a' a)) w
77−
78−type family Infer' (s :: *) (a' :: *) (subs :: [(Nat, k)]) w :: (*, *) where
79− Infer' s' a' '[ '(p, _)] w
80− = '(UnProxied (Change s' p w), UnProxied (Change a' p w))
81− Infer' s' a' _ _
82− = '(UnProxied s', UnProxied a')
83−
84−type family PickTv (a :: k) (b :: k) :: * where
85− PickTv (P _ _) b = b
86− PickTv (f (P _ _)) (g b) = b
87− PickTv (f a) (g b) = PickTv f g
src/Data/Generics/Product/Fields.hs+1−1
@@ -132,7 +132,7 @@ instance -- see Note [Changing type parameters]
132 , GHasField' field (Rep s) a
132 , GHasField' field (Rep s) a
133 , GHasField' field (Rep s') a'
133 , GHasField' field (Rep s') a'
134 , GHasField field (Rep s) (Rep t) a b
134 , GHasField field (Rep s) (Rep t) a b
135− , '(t, b) ~ Infer s' a' a (PickTv a' b)
135+ , t ~ Infer s a' b
136 ) => HasField field s t a b where
136 ) => HasField field s t a b where
137
137
138 field f s = ravel (repLens . gfield @field) f s
138 field f s = ravel (repLens . gfield @field) f s
src/Data/Generics/Product/Positions.hs+1−1
@@ -103,7 +103,7 @@ instance -- see Note [Changing type parameters]
103 , GHasPosition' i (Rep s) a
103 , GHasPosition' i (Rep s) a
104 , GHasPosition' i (Rep s') a'
104 , GHasPosition' i (Rep s') a'
105 , GHasPosition 1 i (Rep s) (Rep t) a b
105 , GHasPosition 1 i (Rep s) (Rep t) a b
106− , '(t, b) ~ Infer s' a' a (PickTv a' b)
106+ , t ~ Infer s a' b
107 ) => HasPosition i s t a b where
107 ) => HasPosition i s t a b where
108
108
109 position f s = ravel (repLens . gposition @1 @i) f s
109 position f s = ravel (repLens . gposition @1 @i) f s
src/Data/Generics/Sum/Constructors.hs+1−1
@@ -107,7 +107,7 @@ instance
107 , GAsConstructor' ctor (Rep s) a
107 , GAsConstructor' ctor (Rep s) a
108 , GAsConstructor' ctor (Rep s') a'
108 , GAsConstructor' ctor (Rep s') a'
109 , GAsConstructor ctor (Rep s) (Rep t) a b
109 , GAsConstructor ctor (Rep s) (Rep t) a b
110− , '(t, b) ~ Infer s' a' a (PickTv a' b)
110+ , t ~ Infer s' a' b
111 ) => AsConstructor ctor s t a b where
111 ) => AsConstructor ctor s t a b where
112
112
113 _Ctor = repIso . _GCtor @ctor
113 _Ctor = repIso . _GCtor @ctor