Ki Yung Ahn posed a problem of first-order syntactic unification over GADTs. There posted code seem to exhibit two problems: one deals with kind equality, and the other with unification. Let's start with the latter. You have chosen to represent substitutions as functions from terms to terms. That's OK. However, the following lines seems weird:

unify (t1 :-> t2) (t1' :-> t2') = unify t1 t1' . unify t2 t2'

We wish to unify two composite (constructed terms) whose head is :->. Unification of t1 t1' gives a substitution, and so does the unification of t2 and t2'. Now we should prove that the results are compatible, that is, if the domains of both substitutions overlap, the common variables are associated with unifyable values. But the composition is the wrong operation here: the composition is a total operation. So, if we unify (X :-> X) (term1 :-> term2) where X is a free variable and term1 is distinct from term2, we are successful? Indeed, unify X term1 succeeds, so is unify X term2. The composition is total. The result can't be right. The line has to be re-written as follows

unify (t1 :-> t2) (t1' :-> t2') = let s = unify t1 t1' in s `compose` unify (s t2) (s t2')

where

compose s1 s2 t = loop t where s = s1 . s2 loop t = let t1 = s t in if t1 == t then t else loop t1

The fixpoint assures the substitution is idempotent, as behooves to the result of unify. Now, the type of unify is also a bit wrong:

unify :: (Show v,Ord v) => Ty v k -> Ty v k -> Ty v k -> Ty v k It should be unify :: (Show v,Ord v) => Ty v k -> Ty v k -> Ty v k' -> Ty v k'

Finally, we come to the issue of kind equality. In

data Ty v k where TyA :: Ty v (k1 :~> k2) -> Ty v k1 -> Ty v k2

k1 is an existentially quantified type variable. When we wish to compare (TyA t1l t1r) with (TyA t2l t2r), we first have to prove that the kind of t1r is the same as t2r. Both kinds are existentially quantified, there is no reason they must always be equal. So, we have to use intensional equality.

data Star = Star deriving (Show,Eq) -- the kind * data k1 :~> k2 = k1 :~> k2 deriving (Show,Eq)

Well, deriving Eq is not useful here: we can't actually compare Star with (k1 :~> k2) because they have different types. So, we need an intensional representation of kinds, with a useful comparison function. We should also re-write

TyC :: v -> k -> Ty v k

to use that representation. The final code follows. {-# OPTIONS -fglasgow-exts #-} import List infixr :~> -- kind arrow -- term algebra of kinds data Star data k1 :~> k2 -- A representation of kinds data K k where KStar :: K Star KArr :: K k1 -> K k2 -> K (k1 :~> k2) infixr :-> -- type arrow data Ty v k where TyV :: v -> Ty v Star -- all type vars are of kind *. (:->) :: Ty v Star -> Ty v Star -> Ty v Star TyC :: v -> K k -> Ty v k TyA :: Ty v (k1 :~> k2) -> Ty v k1 -> Ty v k2 -- Kind equality data EQ a b where Refl :: EQ a a -- compare two kinds. Return either Nothing or the witness of their -- equality keq:: K k1 -> K k2 -> Maybe (EQ k1 k2) keq KStar KStar = Just Refl keq (KArr k1l k1r) (KArr k2l k2r) = keq' (keq k1l k2l) (keq k1r k2r) keq _ _ = Nothing keq' :: Maybe (EQ k1l k2l) -> Maybe (EQ k1r k2r) -> Maybe (EQ (k1l :~> k1r) (k2l :~> k2r)) keq' (Just Refl) (Just Refl) = Just Refl keq' _ _ = Nothing -- inverse of the above keqa :: Maybe (EQ (k1l :~> k1r) (k2l :~> k2r)) -> Maybe (EQ k1r k2r) keqa (Just Refl) = Just Refl keqa _ = Nothing -- compare two types for their kinds. tykeq :: Ty v k1 -> Ty v k2 -> Maybe (EQ k1 k2) tykeq (TyV _) (TyV _) = Just Refl tykeq (_ :-> _) (_ :-> _) = Just Refl tykeq (TyC _ k1) (TyC _ k2) = keq k1 k2 tykeq (TyA t1 _) (TyA t1' _) = keqa (tykeq t1 t1') -- term equality instance Eq v => Eq (Ty v k) where TyV v1 == TyV v2 = v1 == v2 (t1l :-> t1r) == (t2l :-> t2r) = t1l == t2l && t1r == t2r TyC v1 _ == TyC v2 _ = v1 == v2 (TyA t1l t1r) == (TyA t2l t2r) = teq'' (tykeq t1r t2r) t1r t2r && teq'' (tykeq t1l t2l) t1l t2l _ == _ = False teq'' :: Eq v => Maybe (EQ k1 k2) -> Ty v k1 -> Ty v k2 -> Bool teq'' (Just Refl) t1 t2 = t1 == t2 teq'' _ _ _ = False list = TyC "List" (KArr KStar KStar) nil_t = TyA list (TyV "a") -- the `List a' type nil'_t = TyA list (TyV "b") -- the `List b' type cons_t = TyV "b" :-> TyA list (TyV "b") :-> TyA list (TyV "b") instance Show v => Show (Ty v k) where show (TyV v) = show v show (t1 :-> t2) = "("++show t1++"->"++show t2++")" show (TyC v _) = show v show (TyA t1 t2) = "("++show t1++" "++show t2++")" occurs :: Eq v => v -> Ty v k -> Bool occurs x (TyV y) = x == y occurs x (t1:->t2) = occurs x t1 || occurs x t2 occurs _ (TyC _ _) = False occurs x (TyA t1 t2) = occurs x t1 || occurs x t2 -- A substitution on types can be written as follows: type Subst v k = Ty v k -> Ty v k substt :: Eq v => (v,Ty v Star) -> Subst v k substt (x,t1) t@(TyV y) | x == y = t1 | otherwise = t substt p (t1 :-> t2) = substt p t1 :-> substt p t2 substt _ t@(TyC _ _) = t substt p (TyA t1 t2) = substt p t1`TyA`substt p t2 compose s1 s2 t = loop t where s = s1 . s2 loop t = let t1 = s t in if t1 == t then t else loop t1 unify_gen :: (Show v,Ord v) => Maybe (EQ k1 k2) -> Ty v k1 -> Ty v k2 -> Subst v k' unify_gen (Just Refl) t1 t2 = unify t1 t2 unify_gen _ _ _ = error "incompat kinds" unify :: (Show v,Ord v) => Ty v k -> Ty v k -> Subst v k' unify t1@(TyV x) t2@(TyV y) | x == y = id | x <= y = substt (x,t2) | otherwise = substt (y,t1) unify (TyV x) t | occurs x t = error(show x++" occurs in " ++show t) | otherwise = substt (x,t) unify t1 t@(TyV _) = unify t t1 unify (t1 :-> t2) (t1' :-> t2') = let s = unify t1 t1' in s `compose` unify (s t2) (s t2') unify (TyC a _) (TyC b _) | a == b = id | otherwise = error(show a++" is not " ++show b) unify (TyA t1 t2) (TyA t1' t2') = let s = unify_gen (tykeq t2 t2') t2 t2' tn1 = s t1 tn1' = s t1' in s `compose` unify_gen (tykeq tn1 tn1') tn1 tn1' unify t1 t2 = error(show t1++" is not " ++show t2) test1 = unify nil_t nil_t $ nil_t test2 = unify nil_t cons_t $ nil_t test3 = let s = unify nil_t nil'_t in (s nil_t, s nil'_t) test4 = let t1 = (TyV "a" :-> TyV "b") t2 = (TyV "b" :-> TyC "unit" KStar) s = unify t1 t2 in (s t1, s t2) -- (("unit"->"unit"),("unit"->"unit")) -- Indeed, both types are the same