[Haskell-cafe] type hackery question

[jeff p]

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