[Haskell-cafe] GADT proofs of FunDeps?

Roberto Zunino zunino at di.unipi.it
Wed Jan 3 21:28:05 EST 2007

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?

Roberto Zunino.

More information about the Haskell-Cafe mailing list