[Haskell] GHC Error question
Simon PeytonJones
simonpj at microsoft.com
Wed Dec 13 12:19:14 EST 2006
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
 >
More information about the Glasgowhaskellusers
mailing list