[GHC] #10431: EqualityConstraints extension?

[GHC]

#10431: EqualityConstraints extension?
-------------------------------------+-------------------------------------
        Reporter:  adamgundry        |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:  8.0.1
       Component:  Compiler (Type    |              Version:  7.11
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by adamgundry):

 Thanks for thinking through the implications of this! I'm now not sure
 that the principle I articulated (`GADTs = GADTSyntax +
 ExistentialQuantification + EqualityConstraints`) is essential. My
 instinctive reactions are:

 1. Perhaps it would be better if this still required
 `ExistentialQuantification`, i.e. `GADTs` would enable existential GADTs
 but not plain existential datatypes?

 2. Yes.

 3. I'm in two minds about this. I know our general policy is to require
 flags only at definition sites, but type refinement on pattern matching is
 the whole point of GADTs, and is significantly different to non-GADT
 matching, so it seems like it is reasonable to mark the use sites as well.
 Perhaps GADT pattern matches should require `EqualityConstraints` (and
 hence `GADTs` would suffice)?

 4. I'm surprised that `GADTs` is not required in your example: my vote is
 to treat it as a bug and fix it without a deprecation period. I'd expect
 `GADTSyntax + ExistentialQuantification` to allow data constructors with
 existential variables and contexts, but not specialized result types. I
 don't particularly mind whether this declaration is or is not accepted by
 `GADTSyntax + ExistentialQuantification + EqualityConstraints` without
 `GADTs`.

 I'd be interested to hear what others think.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10431#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler