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

#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

#11169: Remove the word "skolem" from user error messages -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I would say that skolems are a part of the type system. (For example, see the "Practical Type Inference" paper, JFP'07.) But the word is utterly opaque to users, and I fully support its removal. Or, if it is absolutely essential somewhere, the error message should include a link to a page explaining what it is. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11169#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11169: Remove the word "skolem" from user error messages -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by kanetw): I agree, opaque words like rigid/skolem here should be replaced with something more comprehensible to normal users. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11169#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC