[Haskell-cafe] Counterintuitive ScopedTypeVariables behaviour

[Alexis King]

> On Aug 19, 2020, at 18:22, Viktor Dukhovni <ietf-dane at dukhovni.org> wrote:
> 
> Though perhaps much too careful/complete a read of the documentation is
> needed to see support in the documentation for the conclusions I
> ultimately reached, I do believe that the text is on some level there

I do not agree with your interpretation. :)

> But when we get to "9.17.4. Pattern type signatures" […] we see that are they are rather different beasts, that deviate from the description in the overview.  In particular, "2" no longer holds, because these are neither generalised, nor universally quantified.

It is true that such variables are not generalized, but the documentation does not say “generalized”—it says rigid. If we consider that the primary purpose of this feature is to bring existentials into scope, then there is no violation of the principle when used in the intended way. After all, existentials brought into scope via `case` are very much rigid (and distinct from all other variables).

It is true that GHC implements a much more flexible behavior that allows entirely different things to be brought into scope. But that is just part of the divergence from the documentation—there’s nothing that says pattern signatures are exempt from that restriction. It only states that pattern signatures that refer to unbound variables bring those variables into scope, nothing more.

Of course, this is all somewhat immaterial—there is no way to objectively determine which interpretation is “correct,” and the docs are unambiguously unclear regardless, so they should be changed. But purely as a matter of friendly debate, I stand by my interpretation.

Alexis
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20200821/a972a0f3/attachment.html>