[Haskell-cafe] Re: Error message reform

[wren ng thornton]

Tillmann Rendel wrote:
> wren ng thornton wrote:
> > (Though it doesn't necessarily generalize to cover similar messages like:
> >
> >     Prelude> :t (\x -> x) :: a -> b
> >     <interactive>:1:7:
> >         Couldn't match expected type `b' against inferred type `a'
> >           `b' is a rigid type variable bound by
> >           the polymorphic type `forall a b. a -> b' at <interactive>:1:0
> >           `a' is a rigid type variable bound by
> >           the polymorphic type `forall a b. a -> b' at <interactive>:1:0
> >         In the expression: x
> 
> I find this slightly more complicated case quite confusing with the 
> current wording:
> 
>   Prelude> :t (\x -> x) :: (a -> b) -> (a -> a)
>   <interactive>:1:7:
>       Couldn't match expected type `a' against inferred type `b'
>         `a' is a rigid type variable bound by
>             an expression type signature at <interactive>:1:14
>         `b' is a rigid type variable bound by
>             an expression type signature at <interactive>:1:19
>       In the expression: x
>       In the expression: (\ x -> x) :: (a -> b) -> (a -> a)
> 
> This message suggests that ghc has inferred type b for x.


I agree with Claus that this (both of these, actually) are symptoms of 
not giving enough type information for the user to reconstruct what the 
problem actually is.

I think an initial solution should be to print out _some_ type inferred 
for x. We can't print out "the" type, because the error is that there 
isn't one. As for which type to print for x, it'd be most informative 
(though perhaps not most helpful) to print both types that are being 
unified, and to alter the rigidity messages to indicate which type 
they're rigid for. For example, perhaps something like this:

     Couldn't match expected type `a' against inferred type `b'
     In the expression: x
         which should have type: (a -> a)
             where `a' is a rigid type variable bound by
                 an expression with type signature at <interactive>:1:14
         but actually has type: (a -> b)
             where `b' is a rigid type variable bound by
                 an expression with type signature at <interactive>:1:19
     In the expression: (\ x -> x) :: (a -> b) -> (a -> a)

It's too wordy, but it's a start. This is also prime ground for wanting 
to have configurable levels of error reports, since some users will find 
it helpful to see both types but others will find it confusing.


Sometimes, even when the complete type is given, that's not enough 
information because each of the type variables are non-linear and so 
it's not clear where exactly the problem crept up. We can see a little 
of this in the above example where, even with the new message, `a' 
occurs twice in the first type. By presenting both types, users can 
figure it out here--- though with only the last type signature given it 
wouldn't be clear whether it wants ((b->b)->a->a) or ((a->b)->a->b) or 
even ((a->b)->b->a).

In more complex examples I've often found non-linearity to be the most 
uninformative part of the current messages. Perhaps a message like above 
which gives both types will be enough in practice to clear it up. If 
not, then it may be worth providing some sort of metasyntax to 
distinguish what subpart of the type is being discussed (e.g. bold face, 
or an underlining carrot on the next line, etc).

For really intricate type hacking, even this isn't enough because the 
programming errors often happen far from where the type errors are 
finally caught. In an ideal world, ghc could dump the entire proof 
forest generated by inference, so an external tool[1] could be used to 
browse through it and track the complete history of where inferred types 
came from. This gives a partial view of the inferred types for a 
compilation unit, something I've often wanted (rather than the manual 
comment/reload/uncomment routine). The proof forest could even be used 
as an interlingua over which people can write filters to generate 
messages they find most helpful.

Ah the joys of ideal worlds... ;)


[1] Something like the Dynasty[2] debugger for logic programming in Dyna.

[2] http://www.cs.jhu.edu/~jason/papers/eisner+al.infovis06-poster.pdf

-- 
Live well,
~wren