@@ -62,7 +62,7 @@ data Sub where
6262 Sub :: Peano -> k -> Sub
6363
6464type family Unify (a :: k) (b :: k) :: [Sub] where
65− Unify (a b) a' = If (IsPTag b) '[Bar (a b) a'] (Baz (a b) a')
65+ Unify (a b) a' = If (IsPTag b) '[HandleP (a b) a'] (HandleOther (a b) a')
6666 Unify a a = '[]
6767 Unify a b = TypeError
6868 ( 'Text "Couldn't match type "
@@ -71,18 +71,18 @@ type family Unify (a :: k) (b :: k) :: [Sub] where
7171 ':<>: 'ShowType b
7272 )
7373
74−type family Bar a b where
75− Bar (p n _ 'PTag) a' = 'Sub n a'
76−
77−type family Baz a b where
78− Baz (a x) (b y) = Unify x y ++ Unify a b
79− Baz a a = '[]
80− Baz a b = TypeError
81− ( 'Text "Couldn't match type "
82− ':<>: 'ShowType a
83− ':<>: 'Text " with "
84− ':<>: 'ShowType b
85− )
74+type family HandleP a b where
75+ HandleP (p n _ 'PTag) a' = 'Sub n a'
76+
77+type family HandleOther a b where
78+ HandleOther (a x) (b y) = Unify x y ++ Unify a b
79+ HandleOther a a = '[]
80+ HandleOther a b = TypeError
81+ ( 'Text "Couldn't match type "
82+ ':<>: 'ShowType a
83+ ':<>: 'Text " with "
84+ ':<>: 'ShowType b
85+ )
8686
8787type family IsPTag (a :: k) :: Bool where
8888 IsPTag 'PTag = 'True