Patch 1652 replace GADTs extension by GADTSyntax and ExistentialQuantification

Title replace GADTs extension by GADTSyntax and ExistentialQuantification
Superseder Nosy List gh
Related Issues
Status accepted Assigned To

Created on 2018-02-22.15:20:19 by gh, last changed 2018-03-09.20:02:37 by gh.

File name Status Uploaded Type Edit Remove
also-use-gadtsyntax-in-test-harness_-disable-all-extensions-for-executable.dpatch gh, 2018-02-24.15:11:47 application/octet-stream
replace-gadts-extension-by-gadtsyntax-and-existentialquantification.dpatch gh, 2018-02-22.15:20:18 application/octet-stream
See mailing list archives for discussion on individual patches.
msg19912 (view) Author: gh Date: 2018-02-22.15:20:18
It turns out that Darcs never actually uses the full power of the GADTs
extension, that is, to restrict sum and products of some ADT *by
replacing some type variable by a concrete type* (see eg [1]).

Darcs' code does, however, restrict certain ADT by repeating the same
type variable:

    -- | Forward lists
    data FL a wX wZ where
        (:>:) :: a wX wY -> FL a wY wZ -> FL a wX wZ
        NilFL :: FL a wX wX

However (and to my surprise) this is handled already by the strictly
less poweful GADTSyntax extension (that exists since GHC 7.2) [2], which
now must be accompanied by ExistentialQuantification.

I haven't measured whether this change makes Darcs' compilation faster.
I hope so!

Anyway I think it is a good idea that we use the smallest language
extensions possible; when we need real GADTs we can activate them again.

[1] http://darcs.net/Internals/200801-ganesh-gadts.pdf

1 patch for repository http://darcs.net:

patch 4fe172b29bfc4da016ec2f78c81c20a5f093f999
Author: Guillaume Hoffmann <guillaumh@gmail.com>
Date:   Thu Feb 22 12:04:27 -03 2018
  * replace GADTs extension by GADTSyntax and ExistentialQuantification
msg19917 (view) Author: gh Date: 2018-02-24.15:11:47
So the explanation for why can we repeat type variables even with just
GADTSyntax is that it is enabled by the ExistentialQuantification extension.

I'm attaching and screening a patch that does the same as the previous
one for the test harness, and also disables all extensions for the darcs
msg19954 (view) Author: gh Date: 2018-03-09.20:02:37
Date User Action Args
2018-02-22 15:20:19ghcreate
2018-02-22 15:21:10ghsetstatus: needs-screening -> needs-review
2018-02-24 15:11:48ghsetfiles: + also-use-gadtsyntax-in-test-harness_-disable-all-extensions-for-executable.dpatch
messages: + msg19917
2018-03-09 20:02:37ghsetstatus: needs-review -> accepted
messages: + msg19954