Hi Cafe, With this class definition with this instance: class C a where instance C b => C (a, b) GHC can of course infer, given 'C b', that 'C (a, b)'. This is nothing more than the meaning of the instance declaration above. However, GHC cannot infer the inverse: {-# LANGUAGE FlexibleContexts #-} foo :: C a => a -> Int foo = undefined bar1 :: C (a, b) => a -> b -> Int bar1 _ = foo This gives an error on the right-hand side of 'bar1': "Could not deduce (C b) arising from a use of ‘foo’; from the context: C (a, b)". The same happens in similar cases: {-# LANGUAGE GADTs #-} bar2 :: (C p, p ~ (a, b)) => a -> b -> Int bar2 _ = foo data Thing a where Tup :: a -> b -> Thing (a, b) bar3 :: C a => Thing a -> Int bar3 (Tup x y) = foo y Both these usages of 'foo' yield the same error. My use-case is 'bar3', where I would like GHC to determine that the call to 'foo' is valid. (I don't actually care directly about bar1 and bar2.) Is there a way to make 'bar3' compile? Note that: - In my actual use case, 'C' is of course not empty. - In my actual use case, my type class instances _are_ in fact injective, even though I do enable FlexibleInstances to be able to write e.g. 'instance C (T a Int)'. - Above, the dictionary for 'C (a, b)' includes a dictionary for 'C b', doesn't it? So if inference can resolve 'C b', then the compilation to Core can find the right dictionary, I think? (Not sure about this part.) Thanks a lot for your help. Cheers, Tom