@@ -1,6 +1,7 @@
11{-# LANGUAGE AllowAmbiguousTypes #-}
22{-# LANGUAGE DataKinds #-}
33{-# LANGUAGE FlexibleInstances #-}
4+{-# LANGUAGE FunctionalDependencies #-}
45{-# LANGUAGE GADTs #-}
56{-# LANGUAGE PolyKinds #-}
67{-# LANGUAGE TypeFamilies #-}
@@ -13,6 +14,7 @@ module Data.Generics.Internal.Families.Changing
1314 ) where
1415
1516import GHC.TypeLits (TypeError, ErrorMessage (..))
17+import Data.Type.Bool (If)
1618
1719{-
1820 Note [Changing type parameters]
@@ -59,8 +61,7 @@ data Sub where
5961 Sub :: Peano -> k -> Sub
6062
6163type family Unify (a :: k) (b :: k) :: [Sub] where
62− Unify (a n _ 'PTag) a' = '[ 'Sub n a']
63− Unify (a x) (b y) = Unify x y ++ Unify a b
64+ Unify (a b) a' = If (IsPTag b) '[HandleP (a b) a'] (HandleOther (a b) a')
6465 Unify a a = '[]
6566 Unify a b = TypeError
6667 ( 'Text "Couldn't match type "
@@ -69,6 +70,23 @@ type family Unify (a :: k) (b :: k) :: [Sub] where
6970 ':<>: 'ShowType b
7071 )
7172
73+type family HandleP a b where
74+ HandleP (p n _ 'PTag) a' = 'Sub n a'
75+
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 "
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+
7290type family (xs :: [k]) ++ (ys :: [k]) :: [k] where
7391 '[] ++ ys = ys
7492 (x ': xs) ++ ys = x ': (xs ++ ys)