Sure, inferring and comparing for alpha-equal is not the best thing pragmatically. But you asked for an algorithm that would work. :) So the band-aid solution would be to first try with the signature, if that fails, try without and then then use the sig. -- Lennart On Dec 13, 2006, at 12:19 , Simon Peyton-Jones wrote:
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@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 | >