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:claus.reinke@talk21.com]
| 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"
| To: "Lennart Augustsson"
| Cc: "GHC users"
| 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: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
| | >
|
| _______________________________________________
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users@haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
