"skolem type variable" is bad for usability (and beginners)
I believe the new type error message in GHC7 that mentions "skolem" is a hindrance to usability because "skolem" is not a well known term, even in the Haskell community.
I believe using this terminology, even though correct, is going to confuse people. When I do a google search for:
haskell skolem type variable
This wiki page does show up: http://hackage.haskell.org/trac/ghc/blog/LetGeneralisationInGhc7
Which is great, but after reading it I still don't know *what* a skolem type variable is. I now have a trick for working around some instances of the problem created by the changes in the ghc7 type checker, but I'm still none of the wiser as to what is skolem (or why I should care).
I consider this change in error message text to be a regression in the usability of GHC, which in version 6 had the best type error messages of any Haskell compiler. I don't think mentioning skolem is a bad thing (interested parties will learn about skolems), but I think throwing the term around as if the average Haskell programmer already knows what it means is a regression.
Please consider rephrasing this error message.
In the example from the wiki page linked above, what about changing the error message to be similar to this:
Foo.hs:7:11:
Couldn't match type `s' with `s1'
because the type variable `s' would escape: `s1'
Hint: `s' is a skolem type variable
The type variable `s' bound by the polymorphic type `forall s. ST s a'
The following variables have types that mention s
fill :: STRef s a -> ST s () (bound at Foo.hs:10:11)
In the first argument of `runST', namely
`(do { r <- newSTRef x; fill r; readSTRef r })'
My point is that the new term, skolem, is de-emphasized but still mentioned for the sake of googling and experts.
Trac metadata
Trac field | Value |
---|---|
Version | 7.0.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | dagitj@gmail.com |
Operating system | |
Architecture |