[Haskell-cafe] GADT proofs of FunDeps?

[Roberto Zunino]

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.