"skolem type variable" is bad for usability (and beginners)

[guest]

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.

[simonpj]

Hmm, yes.

We used to say "rigid type variable". Would that be better?

[guest]

Yes, I think that sounds better with one caveat:

• Finding the wiki article describing how to fix it seems important. At least, I found that article very helpful and I only found it because 'skolem' was in my google search.

Hence my suggestion to mention 'skolem' somewhere in the error (just de-emphasized). Does that make sense?

[simonpj]

For this porgram

{-# LANGUAGE RankNTypes #-}
module Foo where

f :: (forall a. a->a) -> Int
f = error "urk"

g x = f (\v -> x)

currently we get

Foo.hs:8:7:
    Couldn't match type `t' with `a'
      because this skolem type variable would escape: `a'
    This skolem is bound by the polymorphic type `forall a. a -> a'
    The following variables have types that mention t
      x :: t (bound at Foo.hs:8:3)
...

what about

    Couldn't match type `t' with `a'
      because the type variable 'a' would escape its scope
    The (rigid, skolem) type variable 'a' is is bound by
      the polymorphic type `forall a. a -> a'
    The following variables have types that mention t
      x :: t (bound at Foo.hs:8:3)}}}

[guest]

Nice! I like it. Thanks.

[simonpj]

OK done

Thu Nov 18 00:53:06 PST 2010  simonpj@microsoft.com
  * Improve error message on advice from a user
  
  See Trac #4499

    M ./compiler/typecheck/TcErrors.lhs -7 +8

There's a testsuite patch too

Thu Nov 18 00:53:49 PST 2010  simonpj@microsoft.com
  * Follow error message change (Trac #4499)

    M ./tests/ghc-regress/typecheck/should_fail/tcfail032.stderr -2 +3
    M ./tests/ghc-regress/typecheck/should_fail/tcfail099.stderr -2 +2

Probably worth merging.

[igloo]

Merged.