Re: [Haskell] GHC Error question

[Iavor Diatchki]

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

[Simon Peyton-Jones]

| 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

[Claus Reinke]

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

[Simon Peyton-Jones]

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

[Simon Peyton-Jones]

| 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

[Lennart Augustsson]

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

[Lennart Augustsson]

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

[Claus Reinke]

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

[Simon Peyton-Jones]

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

[Lennart Augustsson]

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

[Claus Reinke]

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

[Simon Peyton-Jones]

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

[Ross Paterson]

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

[Simon Peyton-Jones]

| 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

[Lennart Augustsson]

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

[Chris Kuklewicz]

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

[Rene de Visser]

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

[Simon Peyton-Jones]

| 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

[John Meacham]

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

[Lennart Augustsson]

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

[Lennart Augustsson]

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

[J. Garrett Morris]

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

[Johannes 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/ ---

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

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

[Johannes Waldmann]

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

[Lennart Augustsson]

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

[Norman Ramsey]

 > 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

[Simon Peyton-Jones]

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

[Norman Ramsey]

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

[Simon Peyton-Jones]

[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