[Haskell] GHC Error question
Claus Reinke
claus.reinke at talk21.com
Wed Dec 13 13:42:04 EST 2006
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/glasgowhaskellusers/2006December/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 PeytonJones" <simonpj at microsoft.com>
To: "Lennart Augustsson" <lennart at augustsson.net>
Cc: "GHC users" <glasgowhaskellusers 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 lowpriority bug report for it though.
Simon
 Original Message
 From: Lennart Augustsson [mailto:lennart at augustsson.net]
 Sent: 13 December 2006 13:42
 To: Simon PeytonJones
 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
 alphaconvertible 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 PeytonJones 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
 >
_______________________________________________
Glasgowhaskellusers mailing list
Glasgowhaskellusers at haskell.org
http://www.haskell.org/mailman/listinfo/glasgowhaskellusers
More information about the Glasgowhaskellusers
mailing list