Re: Type checker's expected and inferred types (reformatted)

[Isaac Dupree]

C Rodrigues wrote:

fun1 produces the error message:
Couldn't match expected type `Maybe a' against inferred type `IO ()'
In the first argument of `(>>=)', namely `bar'


fun2 produces the error message:
Couldn't match expected type `IO ()' against inferred type `Maybe ()'
In a stmt of a 'do' expression: bar


It's confusing because 'bar' is inferred to have type Maybe (), even though 
it's explicitly declared to be an IO ().


Which message do you prefer? I couldn't tell which it was.

For myself, I never understood the difference between "expected" and 
"inferred": it works better for me to just think "there were at least 
two different ways that determined the 'type' of this expression, and 
the results contradicted each other, and here are two of those results. 
 Now, dear user, go and look at your code to intuit *what* those ways 
of determining the type might have been" (or sometimes it's easier just 
to look for mistakes, ignoring the particular details of the error)


-Isaac
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Type checker's expected and inferred types (reformatted)

[David Menendez]

On Fri, Oct 23, 2009 at 9:46 PM, Isaac Dupree
 wrote:
> C Rodrigues wrote:
>>
>> fun1 produces the error message:
>> Couldn't match expected type `Maybe a' against inferred type `IO ()'
>> In the first argument of `(>>=)', namely `bar'
>>
>>
>> fun2 produces the error message:
>> Couldn't match expected type `IO ()' against inferred type `Maybe ()'
>> In a stmt of a 'do' expression: bar
>>
>>
>> It's confusing because 'bar' is inferred to have type Maybe (), even
>> though it's explicitly declared to be an IO ().
>
> Which message do you prefer? I couldn't tell which it was.
>
> For myself, I never understood the difference between "expected" and
> "inferred": it works better for me to just think "there were at least two
> different ways that determined the 'type' of this expression, and the
> results contradicted each other, and here are two of those results.  Now,
> dear user, go and look at your code to intuit *what* those ways of
> determining the type might have been" (or sometimes it's easier just to look
> for mistakes, ignoring the particular details of the error)

The expected type is what the context wants (it's *ex*ternal). The
inferred type is what the expression itself has (it's *in*ternal).

So inferring the type Maybe () for bar seems wrong. I'm guessing it's
a bug in the way do-expressions are handled. Note that this doesn't
happen if the bar is last.

Prelude> :t let fooThen m = foo >> m in fooThen (do undefined; bar)

:1:51:
Couldn't match expected type `Maybe b'
   against inferred type `IO ()'
In the expression: bar
In the first argument of `fooThen', namely
`(do undefined
 bar)'
In the expression:
fooThen
  (do undefined
  bar)

Prelude> :t do foo; bar

:1:8:
Couldn't match expected type `Maybe b'
   against inferred type `IO ()'
In the expression: bar
In the expression:
do foo
   bar
Prelude> :t do foo; bar; foo

:1:8:
Couldn't match expected type `IO ()'
   against inferred type `Maybe ()'
In a stmt of a 'do' expression: bar
In the expression:
do foo
   bar
   foo

-- 
Dave Menendez 

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Type checker's expected and inferred types (reformatted)

[Albert Y. C. Lai]

For the record, and to speak up as part of a possible silent majority,

I completely understand the type error messages. I find enough 
information in them. I like them.


I find it unnecessary to "decrypt" the two words "expected" and 
"inferred". They have their own definitions and they stand for 
themselves; "external" and "internal" are helpful mnemonics, useful 
approximation, but not decryption.


I support work on ghc to prioritize professional use over pedagogical 
use, that is, if a proposed pedagogical improvement conflicts with 
professional use concerns, or even if simply no one has time to 
implement, I support sacrificing the pedagogical improvement. To 
mitigate the sacrifice, we users write tutorials for each other.

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Type checker's expected and inferred types (reformatted)

[Daniel Fischer]

Am Samstag 24 Oktober 2009 21:21:51 schrieb Albert Y. C. Lai:
> For the record, and to speak up as part of a possible silent majority,
>
> I completely understand the type error messages.

Mostly, I do, too. But I can't get why IO () is *expected* and Maybe () is 
*inferred* for 
bar in fun2.
Can you explain?

> I find enough information in them. I like them.

Generally, it's the same for me, though some are better than others.
Even if one doesn't completely understand them, it's rare that one can't get 
enough out of 
them to start fixing the code.

>
> I find it unnecessary to "decrypt" the two words "expected" and
> "inferred". They have their own definitions and they stand for
> themselves; "external" and "internal" are helpful mnemonics, useful
> approximation, but not decryption.
>
> I support work on ghc to prioritize professional use over pedagogical
> use, that is, if a proposed pedagogical improvement conflicts with
> professional use concerns, or even if simply no one has time to
> implement, I support sacrificing the pedagogical improvement.

Seconded.

> To mitigate the sacrifice, we users write tutorials for each other.


___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Type checker's expected and inferred types (reformatted)

[Isaac Dupree]

David Menendez wrote:

The expected type is what the context wants (it's *ex*ternal). The
inferred type is what the expression itself has (it's *in*ternal).

So inferring the type Maybe () for bar seems wrong.


well, maybe GHC just gets it wrong enough of the time, that I got confused.

Or maybe ... When there are bound variables interacting, on the inside 
and outside, it gets confusing.



ghci:
Prelude> \x -> (3+x) + (length x)

:1:15:
Couldn't match expected type `[a]' against inferred type `Int'
In the second argument of `(+)', namely `(length x)'
In the expression: (3 + x) + (length x)
In the expression: \ x -> (3 + x) + (length x)

Your explanation of "expected" and "inferred" could make sense to me if 
the error message followed the "Couldn't match" line with, instead,

"In the first argument of `length', namely `x'"
because 'length' gives the context of expected list-type, but we've 
found out from elsewhere (a vague word) that 'x' needs to have type Int.


If we flip around the expression-order, we get
Prelude> \x -> (length x) + (3+x)

:1:20:
Couldn't match expected type `Int' against inferred type `[a]'
In the second argument of `(+)', namely `(3 + x)'
In the expression: (length x) + (3 + x)
In the expression: \ x -> (length x) + (3 + x)

...and yes, technically your explanation of expected/inferred works. But 
the location/parity depends on the evaluation-order that the type 
checker uses.  The error messages don't seem to specify location 
precisely enough that I can easily use the information about which type 
is the 'expected' type and which type is the 'inferred' one.  There are 
usually more chains of inference, let-clauses, etc. through which a 
contradiction is found, that muddy the issue.


hmm. Yes, I think I would appreciate for error messages to tell me 
exactly which piece of the expression is expected/inferred to be those 
types. (Is this always a sensible question? or are there sometimes 
typing-conflicts that can't be / aren't reduced to the expected/inferred 
type of a particular expression in the code?)


-Isaac
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Type checker's expected and inferred types (reformatted)

[David Menendez]

On Sun, Oct 25, 2009 at 1:37 PM, Isaac Dupree
 wrote:
> David Menendez wrote:
>>
>> The expected type is what the context wants (it's *ex*ternal). The
>> inferred type is what the expression itself has (it's *in*ternal).
>>
>> So inferring the type Maybe () for bar seems wrong.
>
> well, maybe GHC just gets it wrong enough of the time, that I got confused.
>
> Or maybe ... When there are bound variables interacting, on the inside and
> outside, it gets confusing.
>
>
> ghci:
> Prelude> \x -> (3+x) + (length x)
>
> :1:15:
>    Couldn't match expected type `[a]' against inferred type `Int'
>    In the second argument of `(+)', namely `(length x)'
>    In the expression: (3 + x) + (length x)
>    In the expression: \ x -> (3 + x) + (length x)
>
> Your explanation of "expected" and "inferred" could make sense to me if the
> error message followed the "Couldn't match" line with, instead,
>    "In the first argument of `length', namely `x'"
> because 'length' gives the context of expected list-type, but we've found
> out from elsewhere (a vague word) that 'x' needs to have type Int.

This had me confused for a while, but I think I've worked out what's
happening. (+) is polymorphic, and GHC is giving it the type [a] ->
[a] -> [a]. So the context is expecting [a], but we infer length x ::
Int from the definition of length.

In the alternate case, \x -> length x + (3+x), GHC gives the outer (+)
the type Int -> Int -> Int, and the inner (+) the type [a] -> [a] ->
[a], which is why we get the type mismatch complaint for 3+x instead
of x.

Note what happens if we use a monomorphic operator:

Prelude> let (<>) = undefined :: Int -> Int -> Int
Prelude> \x -> (3+x) <> length x

:1:22:
Couldn't match expected type `[a]' against inferred type `Int'
In the first argument of `length', namely `x'
In the second argument of `(<>)', namely `length x'
In the expression: (3 + x) <> length x
Prelude> \x -> (3+x) + length x

Here, GHC has concluded that x must be an Int, and thus can't be
passed to length.

Prelude> \x -> length x <> (3+x)

:1:19:
Couldn't match expected type `Int' against inferred type `[a]'
In the second argument of `(<>)', namely `(3 + x)'
In the expression: length x <> (3 + x)
In the expression: \ x -> length x <> (3 + x)

Here, GHC has concluded that x must be [a], and thus 3+x must be [a],
which can't be used with <>.

-- 
Dave Menendez 

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Type checker's expected and inferred types (reformatted)

[Isaac Dupree]

David Menendez wrote:

On Sun, Oct 25, 2009 at 1:37 PM, Isaac Dupree
 wrote:

David Menendez wrote:

The expected type is what the context wants (it's *ex*ternal). The
inferred type is what the expression itself has (it's *in*ternal).

So inferring the type Maybe () for bar seems wrong.

well, maybe GHC just gets it wrong enough of the time, that I got confused.

Or maybe ... When there are bound variables interacting, on the inside and
outside, it gets confusing.


ghci:
Prelude> \x -> (3+x) + (length x)

:1:15:
   Couldn't match expected type `[a]' against inferred type `Int'
   In the second argument of `(+)', namely `(length x)'
   In the expression: (3 + x) + (length x)
   In the expression: \ x -> (3 + x) + (length x)

Your explanation of "expected" and "inferred" could make sense to me if the
error message followed the "Couldn't match" line with, instead,
   "In the first argument of `length', namely `x'"
because 'length' gives the context of expected list-type, but we've found
out from elsewhere (a vague word) that 'x' needs to have type Int.


This had me confused for a while, but I think I've worked out what's
happening. (+) is polymorphic,   ...


Oh darn, it sounds like you're right. And polymorphism is so common.  I 
just came up with that example randomly as the first nontrivial 
type-error-with-a-lambda I could think of...


I wonder if it would help for the message to also output what it thinks 
the complete type of the function is (so far).


I wonder if it could look something like this:
Couldn't match expected type `[a]' against inferred type `Int'
In the second argument of `(+) :: [a] -> [a]',
namely `(length x) :: Int'

(always, at the risk/tradeoff of taking up space with lots of useless 
information. sadly. hmm.)



Ideally I would like GHC to pick a location for the error that's more 
intuitive, but that sounds like an awfully vague desire :-)


-Isaac
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Type checker's expected and inferred types (reformatted)

[John Lato]

> From: Isaac Dupree 
> David Menendez wrote:
>> On Sun, Oct 25, 2009 at 1:37 PM, Isaac Dupree
>>  wrote:
>>> David Menendez wrote:
 The expected type is what the context wants (it's *ex*ternal). The
 inferred type is what the expression itself has (it's *in*ternal).

 So inferring the type Maybe () for bar seems wrong.
>>> well, maybe GHC just gets it wrong enough of the time, that I got confused.
>>>
>>> Or maybe ... When there are bound variables interacting, on the inside and
>>> outside, it gets confusing.
>>>
>>>
>>> ghci:
>>> Prelude> \x -> (3+x) + (length x)
>>>
>>> :1:15:
>>>    Couldn't match expected type `[a]' against inferred type `Int'
>>>    In the second argument of `(+)', namely `(length x)'
>>>    In the expression: (3 + x) + (length x)
>>>    In the expression: \ x -> (3 + x) + (length x)
>>>
>>> Your explanation of "expected" and "inferred" could make sense to me if the
>>> error message followed the "Couldn't match" line with, instead,
>>>    "In the first argument of `length', namely `x'"
>>> because 'length' gives the context of expected list-type, but we've found
>>> out from elsewhere (a vague word) that 'x' needs to have type Int.
>>
>> This had me confused for a while, but I think I've worked out what's
>> happening. (+) is polymorphic,   ...
>
> Oh darn, it sounds like you're right. And polymorphism is so common.  I
> just came up with that example randomly as the first nontrivial
> type-error-with-a-lambda I could think of...

I think this is a great example of why the current type errors are not
as helpful as they could be.  The code where the type checker
determines 'x' has type [a] is several steps removed from where the
error arises.  This is how I understand this process (I've probably
left out some details):

1.  checker infers x :: [a] from 'length x'
2.  checker infers (3 + x) :: [a] from (+) and step 1
3.  checker infers the second (+) :: [a] -> [a] -> [a] from step 2
4.  conflict - checker expects (length x) :: [a] from step 3
 and infers (length x) :: Int from definition of 'length'.

Even with this simple example the error message given doesn't directly
point to the problem.  I don't think it's uncommon for there to be
more steps in practice.  I frequently find myself adding explicit type
signatures to let-bound functions to debug these.  This is a pain
because it also usually involves enabling ScopedTypeVariables.

I personally would find it useful if error messages showed the
sequence of how the type checker determined the given context.
Especially if it would also do so for infinite type errors, which
don't provide much useful information to me.

Cheers,
John
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Type checker's expected and inferred types (reformatted)

[Philip K.F.]

Dear GHCers,


On Wed, 2009-10-28 at 12:14 +, John Lato wrote:
> >> This had me confused for a while, but I think I've worked out what's
> >> happening. (+) is polymorphic,   ...
> >
> > Oh darn, it sounds like you're right. And polymorphism is so common.  I
> > just came up with that example randomly as the first nontrivial
> > type-error-with-a-lambda I could think of...
> 
> I think this is a great example of why the current type errors are not
> as helpful as they could be.  The code where the type checker
> determines 'x' has type [a] is several steps removed from where the
> error arises.  This is how I understand this process (I've probably
> left out some details):

I am a little ambiguous on this issue; I usually find GHC's type errors
make me realize what I did wrong very quickly, i.e. until I start
messing with combinations of GADTs, type classes and type families. When
I've looked at an error for too long without understanding what's
happening, I usually look for ways to express the same problem in
simpler constructs.

This case has me stumped, though.

> 1.  checker infers x :: [a] from 'length x'
> 2.  checker infers (3 + x) :: [a] from (+) and step 1
> 3.  checker infers the second (+) :: [a] -> [a] -> [a] from step 2

Pardon? Judging from the error GHC gives, you must be right, but isn't
*this* the point where things should go wrong? I'm not too intimately
familiar with the type checker's internals, so this example leads me to
speculate that "normal" types are inferred and checked *before* type
class constraints are evaluated. However, I would have wanted this
error:

Prelude> [1] + [2]

:1:0:
No instance for (Num [t])
  arising from a use of `+' at :1:0-8
Possible fix: add an instance declaration for (Num [t])
In the expression: [1] + [2]
In the definition of `it': it = [1] + [2]

In other words: isn't the problem in this case that the type checker
does not gather all information (no instance of type class Num) to give
the proper error? Is gathering type class information after "normal"
types have already conflicted even possible?

Regards,
Philip

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Type checker's expected and inferred types (reformatted)

[John Lato]

On Thu, Oct 29, 2009 at 8:37 AM, Philip K.F.
 wrote:
> Dear GHCers,
>
>
> On Wed, 2009-10-28 at 12:14 +, John Lato wrote:
>> >> This had me confused for a while, but I think I've worked out what's
>> >> happening. (+) is polymorphic,   ...
>> >
>> > Oh darn, it sounds like you're right. And polymorphism is so common.  I
>> > just came up with that example randomly as the first nontrivial
>> > type-error-with-a-lambda I could think of...
>>
>> I think this is a great example of why the current type errors are not
>> as helpful as they could be.  The code where the type checker
>> determines 'x' has type [a] is several steps removed from where the
>> error arises.  This is how I understand this process (I've probably
>> left out some details):
>
> I am a little ambiguous on this issue; I usually find GHC's type errors
> make me realize what I did wrong very quickly, i.e. until I start
> messing with combinations of GADTs, type classes and type families. When
> I've looked at an error for too long without understanding what's
> happening, I usually look for ways to express the same problem in
> simpler constructs.
>
> This case has me stumped, though.
>
>> 1.  checker infers x :: [a] from 'length x'
>> 2.  checker infers (3 + x) :: [a] from (+) and step 1
>> 3.  checker infers the second (+) :: [a] -> [a] -> [a] from step 2
>
> Pardon? Judging from the error GHC gives, you must be right, but isn't
> *this* the point where things should go wrong? I'm not too intimately
> familiar with the type checker's internals, so this example leads me to
> speculate that "normal" types are inferred and checked *before* type
> class constraints are evaluated.

This "(+) :: [a] -> [a] -> [a]" seems wrong from an intuitive sense,
but the type checker doesn't know that.  We know that

  (+) :: Num t => t -> t -> t

It's completely legal (though maybe ill-advised) to construct a Num
instance for [a].  Even if that instance isn't in scope when this code
is compiled, it could be added later.

I should probably wait for a GHC guru to respond to this one, because
I'm in the realm of speculation here, but I expect that "normal" types
need to be inferred, unified, and checked before type class
constraints can be applied.  In the case where a constraint is
necessary, either the type is a concrete type, e.g. Int, Char, for
which the class instance must be in scope, or the type is polymorphic,
e.g. [a], in which case the constraint must be passed up to the
context of where it's used.  The compiler doesn't know which is the
case (or exactly what context is necessary) until it's finished
checking the "normal" types.

> However, I would have wanted this
> error:
>
> Prelude> [1] + [2]
>
> :1:0:
>    No instance for (Num [t])
>      arising from a use of `+' at :1:0-8
>    Possible fix: add an instance declaration for (Num [t])
>    In the expression: [1] + [2]
>    In the definition of `it': it = [1] + [2]
>
> In other words: isn't the problem in this case that the type checker
> does not gather all information (no instance of type class Num) to give
> the proper error? Is gathering type class information after "normal"
> types have already conflicted even possible?
>

Just because a type class isn't in scope doesn't mean it will never be
in scope.  In order for this to work, you'd need to distinguish
between code that will never be linked to from elsewhere and code that
will.  I don't think this is possible without completely changing the
compilation chain.  Ghci can do it because, as an interpreter, it
doesn't produce object code to be linked to anyway.

John
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Type checker's expected and inferred types (reformatted)

[Scott Turner]

On Wednesday 28 October 2009 08:14:46 John Lato wrote:
> >> Isaac Dupree  wrote:
> >>> ghci:
> >>> Prelude> \x -> (3+x) + (length x)
> >>>
> >>> :1:15:
> >>>Couldn't match expected type `[a]' against inferred type `Int'
> >>>In the second argument of `(+)', namely `(length x)'
> >>>In the expression: (3 + x) + (length x)
> >>>In the expression: \ x -> (3 + x) + (length x)
> 
> This is how I understand this process 
> 
> 1.  checker infers x :: [a] from 'length x'
> 2.  checker infers (3 + x) :: [a] from (+) and step 1
> 3.  checker infers the second (+) :: [a] -> [a] -> [a] from step 2
> 4.  conflict - checker expects (length x) :: [a] from step 3
>  and infers (length x) :: Int from definition of 'length'.
> 
> Even with this simple example the error message given doesn't directly
> point to the problem.  I don't think it's uncommon for there to be
> more steps in practice.  I frequently find myself adding explicit type
> signatures to let-bound functions to debug these.  This is a pain
> because it also usually involves enabling ScopedTypeVariables.

I'll second that.

On Saturday 24 October 2009 15:21:51 Albert Y. C. Lai wrote:
>I find it unnecessary to "decrypt" the two words "expected" and
>"inferred". They have their own definitions and they stand for
>themselves;

On the contrary, this is a perfect example of why the error message's choice 
of words is bad. One type is "expected" and the other is "inferred".  In the 
example the contextual type [a] is inferred via steps 1-2-3, and the internal 
type Int is determined so trivially that the "inferred" designation is 
somewhere between confusing and misleading. 

I'd love to see "expected" kept, and "inferred" removed from the message.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users