[Haskell] GHC Error question

[Lennart Augustsson]

What Claus says.  What is the real type that ghc infers?
If it's really what it claims it to be, then this is definitely a bug.
And it might not be common to you, but I have several places in my  
code base where I have to leave off type signatures, because the  
inferred signature is not accepted.  And I turn on the warning for a  
missing type sig.  And if it were feasible to make this an error I  
would.

	-- Lennart

On Dec 13, 2006, at 13:42 , Claus Reinke wrote:

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