I don't agree. It's just another example of ambiguity, just like (show (read x)). Any old instantiation will do, but the meaning of the program might be different for each one -- that's incoherence. It's perfectly sound to give f the type f :: forall t b. (C t b) => t -> t because many calls to f will give rise to an ambiguous constraint (C t b), so the call will be rejected.
Why not reject it right away as ambiguous? Because ambiguity can be pretty hard to spot. Suppose class C had an instance thus: instance D t b => C [t] b where class D t b | t -> b Now if we call f in a context requiring a function of type [x]->[x], we'll get a required constraint (C [x] b). Using the instance decl gives a constraint (D x b). And now b is indeed fixed by a functional dependency! So the call is perfectly unambiguous and coherent. Simon | -----Original Message----- | From: Claus Reinke [mailto:[EMAIL PROTECTED] | Sent: 13 December 2006 18:42 | To: Simon Peyton-Jones; Lennart Augustsson | Cc: GHC users | Subject: Re: [Haskell] GHC Error question | | 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" <[EMAIL PROTECTED]> | To: "Lennart Augustsson" <[EMAIL PROTECTED]> | Cc: "GHC users" <glasgow-haskell-users@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:[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 _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users