[Haskell] GHC Error question

[Claus Reinke]

call me a stickler for details, if you must, but I am still worried that this is
not an undesirable inability to use the type signature, but rather a real bug
in how the result of type inference is presented.

note that Lennart considers both options, and asks which option is the
one relevant for this example (or: what is the internal representation of
the type inferred by GHCi?).

without further constraints, there is nothing linking the b1 needed for
op :: C a b1 => a -> a to the b2 provided by f :: C a b2 => a -> a
(and the original example had several uses of class method, with no
indication that they were all linked to the same dictionary).

so I think that GHC is perfectly right in not using the signature to
discharge the constraint for op. imho, there is a real error in the
way GHCi presents the type of f:

    *Main> :t f
    f :: forall t b. (C t b) => t -> t

in spite of this presentation, we can not use any old b here!
the body of f requires a specific b' for op, we just happen to
have not a single clue about which b' that might be.

which is why I suggested that the type should be represented
differently, by marking b as not free, or by using existential
quantification:

http://www.haskell.org/pipermail/glasgow-haskell-users/2006-December/011758.html

with such a change, GHC would still not be able to use the
signature inferred by GHCi, but it would now be clear why
that is the case (and why the signature above does not work).

Claus

----- Original Message ----- 
From: "Simon Peyton-Jones" <simonpj at microsoft.com>
To: "Lennart Augustsson" <lennart at augustsson.net>
Cc: "GHC users" <glasgow-haskell-users at haskell.org>
Sent: Wednesday, December 13, 2006 5:19 PM
Subject: RE: [Haskell] GHC Error question


Hmm.  GHC currently uses the signature to drive typechecking the expression; it does not infer a 
type and compare. (Much better error messages that way.)

So (a) it's very undesirable that using the inferred type as a signature can ever not work, but (b) 
it affects only very few programs and ones that are almost certainly ambiguous anyway, and (c) I 
can't see an easy way to fix it.  So my current plan is: let it lie.

I'll open a low-priority bug report for it though.

Simon

| -----Original Message-----
| From: Lennart Augustsson [mailto:lennart at augustsson.net]
| Sent: 13 December 2006 13:42
| To: Simon Peyton-Jones
| Cc: GHC users
| Subject: Re: [Haskell] GHC Error question
|
| 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
| >

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users at haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users