[Haskell] GHC Error question

[Claus Reinke]

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 at haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users