@@ -62,7 +62,7 @@ data Sub where
62 Sub :: Peano -> k -> Sub
62 Sub :: Peano -> k -> Sub
64type family Unify (a :: k) (b :: k) :: [Sub] where
64type 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')
66 Unify a a = '[]
66 Unify a a = '[]
67 Unify a b = TypeError
67 Unify a b = TypeError
68 ( 'Text "Couldn't match type "
68 ( 'Text "Couldn't match type "
@@ -71,18 +71,18 @@ type family Unify (a :: k) (b :: k) :: [Sub] where
71 ':<>: 'ShowType b
71 ':<>: 'ShowType b
74−type family Bar a b where
74+type family HandleP a b where
75− Bar (p n _ 'PTag) a' = 'Sub n a'
75+ HandleP (p n _ 'PTag) a' = 'Sub n a'
77−type family Baz a b where
77+type family HandleOther a b where
78− Baz (a x) (b y) = Unify x y ++ Unify a b
78+ HandleOther (a x) (b y) = Unify x y ++ Unify a b
79− Baz a a = '[]
79+ HandleOther a a = '[]
80− Baz a b = TypeError
80+ HandleOther a b = TypeError
81− ( 'Text "Couldn't match type "
81+ ( 'Text "Couldn't match type "
82− ':<>: 'ShowType a
82+ ':<>: 'ShowType a
83− ':<>: 'Text " with "
83+ ':<>: 'Text " with "
84− ':<>: 'ShowType b
84+ ':<>: 'ShowType b
87type family IsPTag (a :: k) :: Bool where
87type family IsPTag (a :: k) :: Bool where
88 IsPTag 'PTag = 'True
88 IsPTag 'PTag = 'True