I think Lennart was referring to the representation problem rather than the inference problem: if we leave out the annotation, the type given by ghci gives no indication that the second parameter of the C constraint is not free, but linked to something within f (whereas that is obvious for C's first parameter). So when we put in the annotation suggested by ghci, we promise an arbitrary dictionary, and ghci complains that it can't deduce the specific one it needs from that. The issue is not that this deduction can't succeed, but that ghci suggests a type that does not distinguish between arbitrary and specific (at least not in any obvious way): *Main> :t f f :: (C a b) => a -> a here, the same notation is used for a, which can be arbitrary (but linked to the rest of the type), and for b, which has to relate to a specific type (which just is not mentioned). If the inferred type would be represented as something like this: f :: forall a. exists b. (C a b => a -> a) or this: f :: forall a. ((forall b. C a b) => a -> a) the problem would be obvious, wouldn't it? A C instance with specific a, but arbitrary b, will do, no C instance with specific b will do. Claus
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.
| 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 _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users