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