[Haskell] GHC Error question
Lennart Augustsson
lennart at augustsson.net
Wed Dec 13 08:42:24 EST 2006
If the type checker really deduces the type 'forall a b . C a b => a -
> a' then an inference algorithm that works seems easy. Do type
inference for f, then check that the signature the user has given is
alpha-convertible with the deduced type (well, in general it's more
complicated than that, of course).
If the type checker doesn't really deduce 'forall a b . C a b => a ->
a' then it shouldn't print what it does.
So I'm curious, what is the exact deduced type?
-- Lennart
On Dec 11, 2006, at 07:16 , Simon Peyton-Jones wrote:
> | 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.
>
> I agree! Indeed I wrote:
>
> | 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
>
More information about the Glasgow-haskell-users
mailing list