[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 monoidal):

 I like this idea, however, a proper implementation will have some
 consequences. Can you review?

 The intended result is that GADTs becomes a synonym for three extensions
 (GADTSyntax, EqualityConstraints and ExistentialQuantification), and the
 compiler never checks for -XGADTs, but always for one of the three flags.

 1) Make GADTs imply ExistentialQuantification

 This will mean that GADTs will enable syntax `data A = forall a. A a`.

 2) Add EqualityConstraints extension

 This extension will imply `MonoLocalBinds` and be implied by `GADTs` and
 `TypeFamilies`. It will be checked in `check_eq_pred`.

 The remaining work is removing two places where the compiler reads
 `-XGADTs` flag.

 3) Allow pattern matches on GADTs without `-XGADTs`

 Currently pattern matching on GADTs requires `-XGADTs` or `-XTypeFamilies`
 due to #2905. This restriction was made due to `-XRelaxedPolyRec` flag.
 However, `-XRelaxedPolyRec` cannot be disabled since GHC 7.0, the original
 motivation is lost. I suggest to remove the check altogether - generally
 we check for flags at definition sites but not call sites.

 4) Check for EqualityConstraints when defining a GADT

 This step is optional and I'm not sure about it.

 Consider this code

 {{{
 {-# LANGUAGE GADTSyntax, ExistentialQuantification #-}
 data Eq a b where
   Eq :: Eq a a
 }}}

 Currently this code compiles, however, it might be argued that
 `-XEqualityConstraints` is needed here, since the same datatype in non-
 GADT syntax requires it (`data Eq a b = a ~ b => Eq`) and `-XGADTSyntax`
 is not supposed to add extra expressiveness. However, this change is not
 backwards compatible and would probably require a deprecation period. The
 rule would be that existentials and contexts require
 `-XExistentialQuantification`, but if there is a specialized result type
 it would require both `-XExistentialQuantification` and
 `-XEqualityConstraints`.

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