[Haskell] GHC Error question

[Simon Peyton-Jones]

| Tell me how this make sense:
|     1. I enter the definition for f.
|     2. I ask ghc for the type of f and get an answer.
|     3. I take the answer and tell ghc this is the type of f, and ghc
| tells me I'm wrong.
| Somewhere in this sequence something is going wrong.

I agree!  Indeed I wrote:

| It doesn't get much simpler than that!  With the type sig, GHC can't see that the (C a b) provided can
| satisfy the (C a b1) which arises from the call to op.   However, without the constraint, GHC simply
| abstracts over the constrains arising in the RHS, namely (C a b1), and hence infers the type
|         f :: C a b1 => a -> a
| It is extremely undesirable that the inferred type does not work as a type signature, but I don't see
| how to fix it

If you have an idea for an inference algorithm that would typecheck this program, I'd be glad to hear it.  Just to summarise, the difficulty is this:
        I have a dictionary of type (C a b1)
        I need a dictionary of type (C a b2)
        There is no functional dependency between C's parameters

Simon

PS: the complete program is this:
        class C a b where
                op :: a -> a

        f :: C a b => a -> a
        f x = op x