@@ -2,14 +2,19 @@
22{-# LANGUAGE DataKinds #-}
33{-# LANGUAGE FlexibleInstances #-}
44{-# LANGUAGE FunctionalDependencies #-}
5+{-# LANGUAGE GADTs #-}
56{-# LANGUAGE PolyKinds #-}
67{-# LANGUAGE TypeFamilies #-}
78{-# LANGUAGE TypeOperators #-}
89{-# LANGUAGE UndecidableInstances #-}
910
10−module Data.Generics.Internal.Families.Changing where
11+module Data.Generics.Internal.Families.Changing
12+ ( Proxied
13+ , Infer
14+ ) where
1115
12−import GHC.TypeLits (Nat, type (+))
16+import GHC.TypeLits (TypeError, ErrorMessage (..))
17+import Data.Type.Bool (If)
1318
1419{-
1520 Note [Changing type parameters]
@@ -35,53 +40,81 @@ import GHC.TypeLits (Nat, type (+))
3540 If after doing the conversion on @s@, @field@'s type is @(P _ a), then @t@ is
3641 @s[b/a]@, otherwise @t ~ s@ and @b ~ a@.
3742-}
38−data P (i :: Nat) a
3943
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
4153
42−type family Proxied' (t :: k) (next :: Nat) :: k where
43− Proxied' (t a :: k) next = (Proxied' t (next + 1)) (P next a)
54+type Proxied t = Proxied' t 'Z
55+
56+type family Proxied' (t :: k) (next :: Peano) :: k where
57+ Proxied' (t (a :: j) :: k) next = (Proxied' t ('S next)) (P next a 'PTag)
4458 Proxied' t _ = t
4559
46−type family UnProxied (t :: k) :: k where
47− UnProxied (P _ a) = a
48− UnProxied (t (P _ a) :: k) = UnProxied t a
49− UnProxied t = t
50−
51−type family Change (t :: k) (target :: Nat) (to :: j) :: k where
52− Change (P target _) target to = (P target to)
53− Change (t (P target _) :: k) target to = t (P target to)
54− Change (t a :: k) target to = Change t target to a
55− Change t _ _ = t
56−
57−type family UnApply (a :: k) :: [*] where
58− UnApply (f x) = x ': UnApply f
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
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+--
104+--type family ArgKind (t :: k) (pos :: Peano) :: * where
105+-- ArgKind (t (a :: k)) 'Z = k
106+-- ArgKind (t _) ('S pos) = ArgKind t pos
107+--
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+
113+type family ReplaceArg (t :: k) (pos :: Peano) (to :: j) :: k where
114+ ReplaceArg (t a) 'Z to = t to
115+ ReplaceArg (t a) ('S pos) to = ReplaceArg t pos to a
116+ ReplaceArg t _ _ = t
117+
118+type family ReplaceArgs (t :: k) (subs :: [Sub]) :: k where
119+ ReplaceArgs t '[] = t
120+ ReplaceArgs t ('Sub n arg ': ss) = ReplaceArgs (ReplaceArg t n arg) ss