[Haskell] GHC Error question

[Claus Reinke]

please note that I'm not sure I'm right. I'm just trying to argue my view consistently
until someone convinces me it is wrong, or I convince you it is right!-)

>I don't agree.  It's just another example of ambiguity, just like (show (read x)).  Any
>old instantiation will do, but the meaning of the program might be different for each
>one -- that's incoherence.

any old instantiation will do, in the sense that it would provide an op. but, because of
incoherence, the type system is not free to choose any old instantiation that happens
to be in scope - it has to be uniquely determined. and a type signature alone is not
strong enough to fix variables in the context, unless they are reachable from the type:

    *Main> :t op :: C Int b => Int -> Int

    <interactive>:1:0:
        Ambiguous constraint `C Int b'
            At least one of the forall'd type variables mentioned by the constraint
            must be reachable from the type after the '=>'
        In an expression type signature:
          (C Int b) => Int -> Int

(this is with an instance "C Int b" added)

>It's perfectly sound to give f the type
>             f :: forall t b. (C t b) => t -> t
>because many calls to f will give rise to an ambiguous constraint (C t b), so the call will be 
>rejected.

if that was the type of f, then I should be able to use f with any old t for which there is any old
instance (C t b). but I can't. even if I have an instance (C Int Int), say:

    *Main> f (0::Int)

    <interactive>:1:0:
        No instance for (C Int b)
          arising from use of `f' at <interactive>:1:0-9
        Possible fix: add an instance declaration for (C Int b)
        In the call (f (0 :: Int))
        In the expression: f (0 :: Int)
        In the definition of `it': it = f (0 :: Int)

the only way I can see of using f is with a specific t for which there is a general (wrt b)
instance (forall b. C t b). so if I change that (C Int Int) instance to (C Int b), say:

    *Main> f (0::Int)
    Loading package haskell98-1.0 ... linking ... done.
    *** Exception: C:/Documents and Settings/cr3/Desktop/T.hs:4:0:
    No instance nor default method for class operation Main.op

it works as expected. which is why I think that the type should be:

    f :: forall t. ((forall b. C t b) => t -> t)

or, bringing the quantifiers to the front:

    f :: forall t. exists b. (C t b => t -> t)

>Why not reject it right away as ambiguous?

I thought the reason for that was simply that there are situations in which f can actually
be called, and op be used, such as "f (0::Int)" with "instance C Int b"?

Claus