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