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:[EMAIL PROTECTED]
| 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@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
