| And why isn't C a b equivalent to C a b1? | forall a b . C a b => a -> a | and | forall a b1 . C a b1 => a -> a | look alpha convertible to me. You may say it's just common sense: a) I have a dictionary of type (C a b) provided by the caller b) I need a dictionary of type (C a b1) , where b1 is an as-yet-unknown type (a unification variable in the type inference system) c) There are no other constraints on b1 So, in view of (c), perhaps we can simply choose b1 to be b, and we're done! Sounds attractive. But consider this: f :: (Read a, Show a) => String -> String f x = show (read x)
From this I get a) I have a dictionary of type (Show a) provided by the caller b) I need a dictionary of type (Show a1), arising from the call to show c) There are no other constraints on a1
So perhaps I should choose a1 to be a, thereby resolving the ambiguity! Well, perhaps. Or I could choose a1 to be Int, or Bool. (A similar ambiguity exists in Norman's example, if there were instances for (C a Int) or (C a Bool).) There may be a heuristic that would help more programs to go through... but I prefer asking the programmer to make the desired behaviour explicit. Simon