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