[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.
_______________________________________________
Haskell-Cafe mailing list
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe