@@ -1,6 +1,7 @@
1{-# LANGUAGE AllowAmbiguousTypes #-}
1{-# LANGUAGE AllowAmbiguousTypes #-}
2{-# LANGUAGE DataKinds #-}
2{-# LANGUAGE DataKinds #-}
3{-# LANGUAGE FlexibleInstances #-}
3{-# LANGUAGE FlexibleInstances #-}
4+{-# LANGUAGE FunctionalDependencies #-}
4{-# LANGUAGE GADTs #-}
5{-# LANGUAGE GADTs #-}
5{-# LANGUAGE PolyKinds #-}
6{-# LANGUAGE PolyKinds #-}
6{-# LANGUAGE TypeFamilies #-}
7{-# LANGUAGE TypeFamilies #-}
@@ -13,6 +14,7 @@ module Data.Generics.Internal.Families.Changing
15import GHC.TypeLits (TypeError, ErrorMessage (..))
16import GHC.TypeLits (TypeError, ErrorMessage (..))
17+import Data.Type.Bool (If)
18 Note [Changing type parameters]
20 Note [Changing type parameters]
@@ -59,8 +61,7 @@ data Sub where
59 Sub :: Peano -> k -> Sub
61 Sub :: Peano -> k -> Sub
61type family Unify (a :: k) (b :: k) :: [Sub] where
63type family Unify (a :: k) (b :: k) :: [Sub] where
62− Unify (a n _ 'PTag) a' = '[ 'Sub n a']
64+ Unify (a b) a' = If (IsPTag b) '[HandleP (a b) a'] (HandleOther (a b) a')
63− Unify (a x) (b y) = Unify x y ++ Unify a b
64 Unify a a = '[]
65 Unify a a = '[]
65 Unify a b = TypeError
66 Unify a b = TypeError
66 ( 'Text "Couldn't match type "
67 ( 'Text "Couldn't match type "
@@ -69,6 +70,23 @@ type family Unify (a :: k) (b :: k) :: [Sub] where
69 ':<>: 'ShowType b
70 ':<>: 'ShowType b
73+type family HandleP a b where
74+ HandleP (p n _ 'PTag) a' = 'Sub n a'
76+type family HandleOther a b where
77+ HandleOther (a x) (b y) = Unify x y ++ Unify a b
78+ HandleOther a a = '[]
79+ HandleOther a b = TypeError
80+ ( 'Text "Couldn't match type "
86+type family IsPTag (a :: k) :: Bool where
72type family (xs :: [k]) ++ (ys :: [k]) :: [k] where
90type family (xs :: [k]) ++ (ys :: [k]) :: [k] where
73 '[] ++ ys = ys
91 '[] ++ ys = ys
74 (x ': xs) ++ ys = x ': (xs ++ ys)
92 (x ': xs) ++ ys = x ': (xs ++ ys)