Hello, I came across the following problem: I define a class with a functional dependency like so: class C a b | a -> b Then I want to define a datatype using the fact that the second argument of C is dependent on the first: data C a b => T a = MkT a b But unfortunately, this doesn’t work, at least not in GHC. I can try this: data T a = forall b. C a b => MkT a b But if I do pattern matching on a value of T a, GHC doesn’t recognize that the type of MkT’s second argument is determined by the type of the first. For example, the following function definition is not accepted: useB :: C a b => T a -> (b -> ()) -> () useB (MkT a b) f = f b In my opinion, the problem is that GHC doesn’t see that because of the functional dependency the type exists b. C a b => b is at least as general as the type forall b. C a b => b. Is there a solution to this problem? Best wishes, Wolfgang