Hello, The HList paper gives a type cast: class TypeCast a b | a -> b, b->a where typeCast :: a -> b class TypeCast' t a b | t a -> b, t b -> a where typeCast' :: t->a->b class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b instance TypeCast' () a b => TypeCast a b where typeCast x = typeCast' () x instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast'' instance TypeCast'' () a a where typeCast'' _ x = x and a type equality check: class TypeEq x y b | x y -> b instance TypeEq x x HTrue instance TypeCast HFalse b => TypeEq x y b The type cast succeeds causing its two argument types to be unified, or simply fails if the arguments are not unifiable. The type equality always succeeds "returning" HTrue if the arguments are syntactically equal, and HFalse if the arguments are not syntactically equal; thus the type equality will return false for two arguments which could be unified. If I understand correctly, these two classes do not provide a way to check for unifiability. Is it possible to write a class which checks to see if two given type arguments are unifiable? thanks, Jeff