I am investigating mixing FunDeps with the type equality GADT data Teq a b where Teq :: Teq a a Basically, I would like to write something like proof :: (C a b1, C a b2) => Teq b1 b2 proof = unsafeCoerce# Teq provided the FunDep class C a b | a -> b Is this safe? Any caveat? Regards, Roberto Zunino.