[ghc-steering-committee] Proposal #532: Clean up and simplify the treatment of implicit bindings. Recommendation: partially accept (maybe)

[Arnaud Spiwack]

Dear all,

Proposal https://github.com/ghc-proposals/ghc-proposals/pull/532
Rendered link for the proposal (although several other files are modified):
https://github.com/Ericson2314/ghc-proposals/blob/type-variables/proposals/0532-type-variable-scoping.rst

John Ericson proposes to amend Richard's recent Modern Scoped Type
Variables Proposal [
https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0448-type-variable-scoping.rst
]

There are two essential parts to the change:
1. The Explicit Binding Principle is modified
2. Change the two extensions introduced by Proposal #285 [
https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0285-no-implicit-binds.rst
], -XImplicitForalls and -XPatternSignatureBinds (so that they can be
deactivated), and consolidated in Richard's proposal (where
-XPatternSignatureBinds is turned into a binding) into a single
-XImplicitBinds extension

---------

The new Explicit Binding Principle is now somewhat stronger, in that it
requires that there is a form with an explicit binder which “regardless of
the context, is unambiguously a binding site”.  The Lexical Binding
Principle is changed, as well, to refer to this new change but it's not
substantial.

I personally don't think this change to the principles is valuable, it
simply blurs the distinction between the Explicit Binding Principle and the
Lexical Binding Principle. I find the current phrasing more useful. And I
don't think the semantics of the conjunction is actually changed. So I
recommend that we reject the changes to the Principles.

------------

John makes a good point: `-XPatternSignature` being a warning has a
limitation. This is pointed out in section “Unified Namespacing and
extension monotonicity” of the patch to the Modern Scoped Type Variables
Proposal. Namely that  in

t = Int
(x :: t) = 0

The current semantics is to have `t` be a binder (because `t` is not bound
in the type namespace). If we add a warning for pattern signatures binders,
`t` will still be a binder. But we are starting to introduce a new
semantics where failing to lookup `t` in the type namespace, we will fall
back to look it up in the term namespace instead. The current semantics of
considering `t` a binder in this case is at odds with the fallback
strategy. (crucially for this recommendation, the same issue occurs in
signatures where `forall`-s are implicitly inferred)

(Context: At the time where #285 was proposed, I was in favour of a single
extension. Simon PJ strongly pushed for two extensions.)

My inclination today is that we have a choice: we can either
- consider the problem above to be a serious issue, in which case we
probably want to eventually deprecate both implicit foralls and pattern
signature binds. If this is the case, then they should be gated behind an
extension (see also the discussion on the meaning of extensions that we're
currently having). I find it healthy to have a single extension for both
features because the problem that the extension is solving is the same,
hence, in this case, I recommend accepting the changes.
- be happy that the semantics is a little quirky, with the fallback
happening only when an explicit forall is specified (and never in pattern
signatures). In which case both should probably be warnings, it makes sense
for the warnings to be separate categories as these are two different
features. In this case I recommend rejection of the proposed changes.

------------

I realise I'm leaving a big choice hanging. It's a big decision, I think,
which we should weigh carefully (which is kind of funny because the
proposed change itself is rather small).

Personally, I'd be happy with all implicit foralls and pattern signature
binds to be deprecated (so I'm actually taking a position I guess). But I'm
not sure that it's super realistic considering the quantity of Haskell that
has been written so far. I imagine that there are millions of implicit
foralls on Hackage.

PS: I'll be on holiday for the next three weeks (starting on Friday night),
so you'll have a little while to debate this while I'm away.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20221214/cebe534a/attachment-0001.html>