[ghc-steering-committee] #425: invisible binders in type declarations; rec: accept

[Richard Eisenberg]

Hi all,

I am the shepherd for proposal #425, https://github.com/ghc-proposals/ghc-proposals/pull/425, proposing to add invisible binders in type declarations.

The main payload of the proposal is to allow definitions like

> data Proxy @k (a :: k) = Proxy

instead of today's

> data Proxy (a :: k) = Proxy

which has no explicit binding site for k.

This new syntax solves a number of smallish syntax conundra, as very well outlined in the proposal.

In addition, the proposal includes two small unrelated tweaks to the syntax of type family instances; these are points (6) and (7) in the proposal. Both changes will break some obscure (but still realistic, knowing Haskell) programs, but both fixes are backward compatible.

---

I recommend acceptance. The proposal is motivated nicely (do check out the examples) and solves a real problem. The new syntax fits in with other similar features. The small cleanups to existing syntax will lead to better error messages.

The one drawback, as I see it, is that this proposal includes point (5), which is a breaking change to the way type synonyms work. Right now, we can say

> type P = (Proxy :: k -> Type)

and GHC will infer P :: forall k. k -> Type. Under this proposal, you would have to write

> type P @k = (Proxy :: k -> Type)

bringing k into scope explicitly. The fix is not backward compatible, and so I think this proposal should come with a migration strategy, where we warn about the former version for some releases before banning it. (Continuing to support it is possible, but it's very awkward to have a variable mentioned only in a synonym's right-hand side.)

Sorry for the delay in producing this recommendation!
Richard