[GHC] #11169: Remove the word "skolem" from user error messages

GHC ghc-devs at haskell.org
Sun Dec 6 03:52:37 UTC 2015


#11169: Remove the word "skolem" from user error messages
-------------------------------------+-------------------------------------
           Reporter:  dfeuer         |             Owner:
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  7.10.2
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Other
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Skolem variables are not, as best I can tell, part of the type system;
 they are part of the implementation of the type checking algorithm. As
 such, it seems inappropriate to mention them in error messages. Instead,
 the error messages should explain things at the Haskell level.

 {{{
     Couldn't match expected type ‘t’ with actual type ‘a’
       because type variable ‘a’ would escape its scope
     This (rigid, skolem) type variable is bound by...
 }}}

 I'd much rather see an explanation using words like "existentially
 quantified" and "right-hand side of a pattern match".

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11169>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler


More information about the ghc-tickets mailing list