#15146: Documentation: ScopedTypeVariables feature not mentioned/misleadingly described -------------------------------------+------------------------------------- Reporter: AntC | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Documentation | Version: 8.2.2 Keywords: | Operating System: Unknown/Multiple ScopedTypeVariables | Architecture: | Type of failure: Documentation Unknown/Multiple | bug Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider these dead-simple examples that use a signature with `tyvars` on a pattern {{{ -- no separate signature for bar, baz; tyvar aa not in scope from anywhere bar (x :: aa) = x :: aa baz (Just (x :: aa)) = x :: aa -- there could be signatures for bar, baz; they might use tyvar aa; but -- bar :: aa -> aa -- } no explicit forall -- baz :: Maybe aa -> aa -- } }}} Those equations with signatures on the patterns aren't valid Haskell 2010, so ghc rejects and suggests you need `ScopedTypeVariables`. Then they compile OK. Would I expect from [https://downloads.haskell.org/~ghc/8.4.2/docs/html/users_guide/glasgow_exts.... #lexically-scoped-type-variables the User Guide documentation] those equations to be valid? I think not, and I see lots of questions on StackOverflow from people confused why they must use explicit `forall` -- and some equally confused answers failing to mention that no you don't necessarily. Arguably, all of the examples in the docos could be expressed equivalently (and less confusingly for beginners) using this style with pattern signatures rather than explicit `forall` bindings. (Misleading) snippets from the docos: [[BR]][[BR]]

10.16 Enable lexical scoping of type variables explicitly introduced with `forall`.

This comment is indented, so is really explaining that `ScopedTypeVariables` implies `ExplicitForall`. But it fails to explain that you're not forced to use explicit `forall`. [[BR]][[BR]]

10.16 opening example[[BR]] The type signature for `f` brings the type variable `a` into scope, because of the explicit `forall` ...

Fails to mentin that you could achieve the same effect without explicit `forall`. [[BR]][[BR]]

10.16.4 ... in all patterns ''other'' than pattern bindings, a pattern type signature may mention a type variable that is not in scope; in this case, ''the signature brings that type variable into scope''.

This ''might'' be telling that the `bar, baz` above examples are valid, but there is not an example. Furthermore the comment following the `MkT` existential data constructor example undermines that interpretation:

... in this situation (and only then), a pattern type signature can mention a type variable that is not already in scope ... If all this seems a little odd, ...

What is "this situation"? What is "this" that seems odd? The pattern signature binding `(MkT [t :: a])` looks the same as `baz` above's `(Just (x :: aa))`; it's merely that `Just` is not existential. There might be a signature given for `baz`, and it might use `tyvar aa`. But it ''doesn't'' bring `aa` into scope for the equations **unless** that signature has explicit `forall`. That's not made clear. My first several readings of "situation (and only then) ... odd ..." were that this style of pattern signature to bind a `tyvar` applied only for existentials. [[BR]][[BR]][[BR]] BTW, some of the examples in the docos are not valid Haskell/give compilation errors because of lack of `( )` round the patterns with signatures. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15146 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler