Re: [Haskell] GHC Error question
Hello, The same oddity with type checking can happen in Haskell 98 as well: http://www.mail-archive.com/haskell@haskell.org/msg06754.html -Iavor ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: [Haskell] GHC Error question
| 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 ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: [Haskell] GHC Error question
please note that I'm not sure I'm right. I'm just trying to argue my view consistently until someone convinces me it is wrong, or I convince you it is right!-) 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. any old instantiation will do, in the sense that it would provide an op. but, because of incoherence, the type system is not free to choose any old instantiation that happens to be in scope - it has to be uniquely determined. and a type signature alone is not strong enough to fix variables in the context, unless they are reachable from the type: *Main> :t op :: C Int b => Int -> Int :1:0: Ambiguous constraint `C Int b' At least one of the forall'd type variables mentioned by the constraint must be reachable from the type after the '=>' In an expression type signature: (C Int b) => Int -> Int (this is with an instance "C Int b" added) 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. if that was the type of f, then I should be able to use f with any old t for which there is any old instance (C t b). but I can't. even if I have an instance (C Int Int), say: *Main> f (0::Int) :1:0: No instance for (C Int b) arising from use of `f' at :1:0-9 Possible fix: add an instance declaration for (C Int b) In the call (f (0 :: Int)) In the expression: f (0 :: Int) In the definition of `it': it = f (0 :: Int) the only way I can see of using f is with a specific t for which there is a general (wrt b) instance (forall b. C t b). so if I change that (C Int Int) instance to (C Int b), say: *Main> f (0::Int) Loading package haskell98-1.0 ... linking ... done. *** Exception: C:/Documents and Settings/cr3/Desktop/T.hs:4:0: No instance nor default method for class operation Main.op 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) 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"? Claus ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: [Haskell] GHC Error question
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" | 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 constr
RE: [Haskell] GHC Error question
| What Claus says. What is the real type that ghc infers? It's this: forall a b . C a b => a -> a | 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. I'd love to see those examples. Can you extract them? You could add them to http://hackage.haskell.org/trac/ghc/ticket/1050 Simon ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: [Haskell] GHC Error question
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
Re: [Haskell] GHC Error question
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" <[EMAIL PROTECTED]> To: "Lennart Augustsson" <[EMAIL PROTECTED]> 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:[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 |
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" 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
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
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
Re: [Haskell] GHC Error question
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 ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: [Haskell] GHC Error question
Well it might not be ambiguous. Consider instance C Int b where... Simon | -Original Message- | From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] | On Behalf Of Ross Paterson | Sent: 11 December 2006 12:41 | To: glasgow-haskell-users@haskell.org | Subject: Re: [Haskell] GHC Error question | | On Mon, Dec 11, 2006 at 12:16:06PM +, 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#type-restrictions | | 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 | | ___ | 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
Re: [Haskell] GHC Error question
On Mon, Dec 11, 2006 at 12:16:06PM +, 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#type-restrictions 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 ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: [Haskell] GHC Error question
| 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
Re: [Haskell] GHC Error question
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 ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: [Haskell] GHC Error question
Rene de Visser wrote: > 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 I can't quite do that but I have a trick: In GHC 6.6 with -fglasgow-exts this works: > module Foo where > > data CInst a b > > class C a b where > cInst :: CInst a b > cInst = undefined > op :: a -> a > op' :: CInst a b -> a -> a > > instance C Int Int where > op a = -a > op' _ a = (-a) > > intInst :: CInst Int Int > intInst = cInst > > test x = (op' intInst) x And test is inferred to have type: > *Foo> :i test > test :: Int -> Int-- Defined at /tmp/test.hs:18:0 Essentially the trick used in this case is to reify the instance (C Int Int) as the value (undefined :: CInst Int Int). Then you can specify to "op" -- Chris ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: [Haskell] GHC Error question
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 ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: [Haskell] GHC Error question
| 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 ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type wildcards, was: Re: [Haskell] GHC Error question
On Thu, Dec 07, 2006 at 10:53:38AM -0500, J. Garrett Morris wrote: > On 12/7/06, Lennart Augustsson <[EMAIL PROTECTED]> 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⑈ ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type wildcards, was: Re: [Haskell] GHC Error question
My (off-the-top-of-my-head) suggestion was much more modest. A context synonym would only allow you to shorten contexts, it would not be a new class. On Dec 7, 2006, at 10:53 , J. Garrett Morris wrote: On 12/7/06, Lennart Augustsson <[EMAIL PROTECTED]> 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. ___ 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
Re: Type wildcards, was: Re: [Haskell] GHC Error question
I should have said that the situation in H98 is quite bad. There you can't make default instances. On Dec 7, 2006, at 07:49 , Johannes Waldmann wrote: 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/ --- ___ 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
Re: Type wildcards, was: Re: [Haskell] GHC Error question
On 12/7/06, Lennart Augustsson <[EMAIL PROTECTED]> 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. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type wildcards, was: Re: [Haskell] GHC Error question
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/ --- ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type wildcards, was: Re: [Haskell] GHC Error question
I would treat multiple _ in a type the same way as multiple _ in a pattern. They can all be different. It might be useful to have multiple "variables", say _a, in a type too, all standing for the same type. But I'd settle for _ for now. :) And yes, contexts even more so! Contexts are really annoying in Haskell, they can become quite large, but they cannot be named. 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. Well, you can leave out type signatures altogether (but only a few people advocate this (hello John!)). -- Lennart On Dec 7, 2006, at 07:20 , Johannes Waldmann wrote: 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/ --- ___ 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
Type wildcards, was: Re: [Haskell] GHC Error question
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/ --- ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: [Haskell] GHC Error question
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. Or is the inferred type forall a . C a b1 => a -> a 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." -- Lennart On Dec 6, 2006, at 02:46 , Simon Peyton-Jones wrote: 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! 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 Simon | -Original Message- | From: [EMAIL PROTECTED] [mailto:glasgow- haskell-users- | [EMAIL PROTECTED] 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 ___ 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
Re: [Haskell] GHC Error question
> 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: > | [EMAIL PROTECTED] [mailto:glasgow-haskell-users- > | [EMAIL PROTECTED] 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 ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: [Haskell] GHC Error question
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! 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 Simon | -Original Message- | From: [EMAIL PROTECTED] [mailto:glasgow-haskell-users- | [EMAIL PROTECTED] 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 ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
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
RE: [Haskell] GHC Error question
[redirecting to ghc users] It looks like a splendid error to me. The call of compile1 is obliged to pass to compile1 a dictionary of type (Builder b box), *for any type box*. There are no further constraints on box, so compile1 can make no assumptions about how the caller chooses to instantiate 'box'. But in the body you'll need a dictionary of type (Builder b box1), but there is nothing to ensure that the caller chooses the "right" box. Maybe you want the Builder class to have a functional dependency (b -> box), so that fixing b fixes box. I can't say more without seeing the code. can you give a small repo case? Simon | -Original Message- | From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On Behalf Of Norman | Ramsey | Sent: 05 December 2006 21:21 | To: haskell@haskell.org | Cc: [EMAIL PROTECTED] | Subject: [Haskell] GHC Error question | | Without going too deep into the details of my type classes, I have | written the following code (focusing on compile1): | | {-# OPTIONS -fglasgow-exts #-} | | compile1 :: (Builder b box) => t -> Name -> Ir.ANF -> b t | compile1 f x body = do env <- compile body empty | wire (Arg W) (env x) | return f | | compile :: (Builder b box) => Ir.ANF -> Env box -> b (Env box) | | class (Monad b) => Builder b box where | wire:: Source box -> Sink box -> b () | ... | | type Env box = Name -> Sink box | | 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. | | Am I misusing the type-class system in some way, or should I be | reporting a bug in GHC? | | | Norman | | ___ | Haskell mailing list | Haskell@haskell.org | http://www.haskell.org/mailman/listinfo/haskell ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users