I agree that this is confusing. Here is a cut-down example:

class C a b where op :: a -> a

-- f :: C a b => a -> a f x = op x

It doesn't get much simpler than that!

Indeed not. I salaam in your general direction.

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

Pity. Do you see a way for the error message to avoid suggesting the 'possible fix', and indeed instead suggesting 'possible fix: remove the type signature from f'?

Simon

| -----Original Message----- From: | glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users- | bounces@haskell.org] On Behalf Of Norman Ramsey Sent: 06 December 2006 | 01:41 To: Simon Peyton-Jones Cc: GHC users Subject: Re: [Haskell] GHC | Error question | | > [redirecting to ghc users] | > | > It looks like a splendid error to me. | | I'm not sure if you meant the error or the message was splendid :-) | I yelled for help because my usual strategy failed. That strategy is | | 1. Remove the type annotation. | 2. Get ghci to tell me what the 'right type' is. | 3. Put the 'right type' in the type annotation. | | I find it a bit depressing that the most general type inferred by ghci | does not work as a type signature. | | > I can't say more without seeing the code. can you give a small repo | > case? | | Yes, here's a case that fits in one screen of emacs :-) | | | {-# OPTIONS -fglasgow-exts #-} | module Ccomp where | | type Name = String | | data Inface = N | W | data Outface = S | E | | data Sink box = Boxin Inface box | Result | data Source box = Boxout Outface box | Arg Inface | | data Command = Send0 | | class (Monad b) => Builder b box where | box :: Command -> b box | wire :: Source box -> Sink box -> b () | | type Env box = Name -> Sink box | | empty = \x -> error (x ++ " not connected or multiply connected in | circuit") | | -- either of these explicit signatures causes the compiler to fail -- | although the inferred signature is the second. --compile1 :: (Builder b | box) => Name -> Name -> ANF -> b Name compile1 :: (Builder t box) => t1 | -> Name -> ANF -> t t1 -- generated by ghci compile1 f x body = do env <- | compile body empty | wire (Arg W) (env x) | return f | | data ANF = ANF () | | compile :: (Builder b box) => ANF -> Env box -> b (Env box) | compile (ANF m) out = undefined | | > | This program is rejected by GHC with the following message: | > | | > | Ccomp.hs:54:23: | > | Could not deduce (Builder b box1) from the context (Builder b | > | box) | > | arising from use of `wire' at Ccomp.hs:54:23-42 | > | Possible fix: | > | add (Builder b box1) to the type signature(s) for `compile1' | > | In the expression: wire (Arg W) (env x) | > | In a 'do' expression: wire (Arg W) (env x) | > | In the expression: | > | do env <- compile body empty | > | wire (Arg W) (env x) | > | return f | > | | > | Note that compile1 has an explicit type signature much along the | > | lines suggested by GHC. If I *remove* this type signature, the | > | function compiles successfully, and ghci reporets this type for | > | compile1: | > | | > | compile1 :: (Builder t box) => t1 -> Name -> Ir.ANF -> t t1 | > | | > | I believe this signature is isomorphic to the explicit signature I | > | had attempted to use. | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Lennart Augustsson wrote:

Btw, this reminds me again that I'd like to be able to use _ in type signatures. With the meaning of _ being, "there's a type here, but I can't be bothered to write it out in full."

you're not alone ... what is the meaning of two _ in one expression? do they necessarily denote the same type? (probably not.) what about type classes? for example, given sort :: Ord a => [a] -> [a], would it be ok to write sort :: [ _ ] -> [ _ ] (that is, omitting the context) or is it more like sort :: _ => [ _ ] -> [ _ ] BTW, this "_ for context" would be useful on its own! I have several cases where the conxtext for the type decl is longer than the implementation of the function. Well, nearly. With previous ghc versions, I could get this effect by omitting the type decl but writing f ( x :: type1) ( y :: type2 ) = ... I sometimes wish haddock would understand that. (*) Because - if you write a haddoc comment for a type declaration, then you don't have names for the function's arguments. This leads to either awkward prose (random example, from Data.Maybe:)

The maybe function takes a default value, a function, and a Maybe value. If the Maybe value is Nothing ...

(this only works here because all the argument types are different in this case) or you have to re-invent names, random example:

approxRational :: RealFrac a => a -> a -> Rational approxRational, applied to two real fractional numbers x and epsilon,

which looks like duplication of work. (*) of course the full form would include the return type fun (x :: type1 ) (y :: type2) :: type3 = ... I expect strong opposition from those who write functions with pattern matching (then there is a group of declarations and which one should be type-annotated?) but that's bad style anyway since constructors should not be exported :-) Best regards, -- -- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 -- ---- http://www.imn.htwk-leipzig.de/~waldmann/ -------

Lennart Augustsson wrote:

Speaking of wishlist, I'd also like to see context synonyms, e.g., context C a = (Ord a, Num a)

The current situation is quite bad, there's no way to abstract contexts.

except by writing extra classes that encode the context, see for example class NFAC: http://141.57.11.163/cgi-bin/cvsweb/lib/Autolib/NFA/Data.hs.drift?rev=1.16 but this is of course only a hack, and it duplicates information since you have to repeat the context in the default instance. At least this happens only in one place, so it is useful. -- -- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 -- ---- http://www.imn.htwk-leipzig.de/~waldmann/ -------

On 12/7/06, Lennart Augustsson wrote:

Speaking of wishlist, I'd also like to see context synonyms, e.g., context C a = (Ord a, Num a)

This is equivalent to John Meacham's class alias proposal, right? (http://repetae.net/john/recent/out/classalias.html) /g -- It is myself I have never met, whose face is pasted on the underside of my mind.

On Thu, Dec 07, 2006 at 10:53:38AM -0500, J. Garrett Morris wrote:

On 12/7/06, Lennart Augustsson wrote:

...

Speaking of wishlist, I'd also like to see context synonyms, e.g., context C a = (Ord a, Num a)

This is equivalent to John Meacham's class alias proposal, right? (http://repetae.net/john/recent/out/classalias.html)

is is a small part of it, the class alias proposal gives both a shorthand form of refering to a set of class constraints, and a 'template language' of sorts for declaring class instances. the instance declarations part is the "meat" of the proposal, the shorthand form is more of a natural consequence of it. John -- John Meacham - ⑆repetae.net⑆john⑈

There may be a heuristic that would help more programs to go through... but I prefer asking the programmer to make the desired behaviour explicit. Simon How can the user make this explicit? With the class C a b where op :: a -> a instance C Int Int where op a = -a test d = op d example, I have been unable to figure out what type annotations I need to add to 'test', for exampl,e to define test to be for the C Int Int instance. Or is it simply impossible in GHC to give test a type signature and to use it as a useful function? Example

Your two examples are different, the second one is rejected by the type checker, with or without a signature. The first one isn't. 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. And it is either is step 2 or 3. Maybe in step 2 ghc is lying to me, and what it tells me isn't the type of f. Then ghc is broken. Maybe in step 3 ghc misunderstands my type and doesn't know what I mean. Then ghc is broken. I don't see how steps 1-3 can happen unless there is something broken. And I think the problem is in step 2. The b there isn't quite what it seems to be. And if it isn't, it should be marked as such. -- Lennart On Dec 8, 2006, at 10:48 , Simon Peyton-Jones wrote:

| And why isn't C a b equivalent to C a b1? | forall a b . C a b => a -> a | and | forall a b1 . C a b1 => a -> a | look alpha convertible to me.

You may say it's just common sense: a) I have a dictionary of type (C a b) provided by the caller b) I need a dictionary of type (C a b1) , where b1 is an as- yet-unknown type (a unification variable in the type inference system) c) There are no other constraints on b1 So, in view of (c), perhaps we can simply choose b1 to be b, and we're done!

Sounds attractive. But consider this:

f :: (Read a, Show a) => String -> String f x = show (read x)

...

From this I get a) I have a dictionary of type (Show a) provided by the caller b) I need a dictionary of type (Show a1), arising from the call to show c) There are no other constraints on a1

So perhaps I should choose a1 to be a, thereby resolving the ambiguity! Well, perhaps. Or I could choose a1 to be Int, or Bool. (A similar ambiguity exists in Norman's example, if there were instances for (C a Int) or (C a Bool).)

There may be a heuristic that would help more programs to go through... but I prefer asking the programmer to make the desired behaviour explicit.

Simon

On Mon, Dec 11, 2006 at 12:16:06PM +0000, Simon Peyton-Jones wrote:

[...] 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

PS: the complete program is this: class C a b where op :: a -> a

f :: C a b => a -> a f x = op x

That raises a point I'd wondered about. GHC requires only that each type variable in the context be reachable from the type via a chain of assertions: http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html... What's the rationale for that, rather than calling types like the above type of f ambiguous? The examples given in the User's Guide involve functional dependencies, albeit obscured by superclasses

I think Lennart was referring to the representation problem rather than the inference problem: if we leave out the annotation, the type given by ghci gives no indication that the second parameter of the C constraint is not free, but linked to something within f (whereas that is obvious for C's first parameter). So when we put in the annotation suggested by ghci, we promise an arbitrary dictionary, and ghci complains that it can't deduce the specific one it needs from that. The issue is not that this deduction can't succeed, but that ghci suggests a type that does not distinguish between arbitrary and specific (at least not in any obvious way): *Main> :t f f :: (C a b) => a -> a here, the same notation is used for a, which can be arbitrary (but linked to the rest of the type), and for b, which has to relate to a specific type (which just is not mentioned). If the inferred type would be represented as something like this: f :: forall a. exists b. (C a b => a -> a) or this: f :: forall a. ((forall b. C a b) => a -> a) the problem would be obvious, wouldn't it? A C instance with specific a, but arbitrary b, will do, no C instance with specific b will do. Claus

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.

| 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

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 | >

What Claus says. What is the real type that ghc infers? If it's really what it claims it to be, then this is definitely a bug. And it might not be common to you, but I have several places in my code base where I have to leave off type signatures, because the inferred signature is not accepted. And I turn on the warning for a missing type sig. And if it were feasible to make this an error I would. -- Lennart On Dec 13, 2006, at 13:42 , Claus Reinke wrote:

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 _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

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

| it works as expected. which is why I think that the type should be: | | f :: forall t. ((forall b. C t b) => t -> t) | | or, bringing the quantifiers to the front: | | f :: forall t. exists b. (C t b => t -> t) My brain is too small to figure out the consequences of adding first-class existentials to Haskell; nor of how to decide when to universally quantify and when to existentially quantify; nor of what to do when calling a function like f. Oleg's recent message gives many other examples you might like to consider. http://www.haskell.org/pipermail/haskell-cafe/2006-December/020538.html | >Why not reject it right away as ambiguous? | | I thought the reason for that was simply that there are situations in | which f can actually | be called, and op be used, such as "f (0::Int)" with "instance C Int | b"? yes, that's right. Simon

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 | >