Your two examples are different, the second one is rejected by the
type checker, with or without a signature. The first one isn't.
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. And it is
either is step 2 or 3.
Maybe in step 2 ghc is lying to me, and what it tells me isn't the
type of f. Then ghc is broken.
Maybe in step 3 ghc misunderstands my type and doesn't know what I
mean. Then ghc is broken.
I don't see how steps 1-3 can happen unless there is something
broken. And I think the problem is in step 2. The b there isn't
quite what it seems to be. And if it isn't, it should be marked as
such.
-- Lennart
On Dec 8, 2006, at 10:48 , Simon Peyton-Jones wrote:
> | 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