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

 1. Sounds good to me. I think this is probably already the case. The
 "existentials" flag can be spelled `-XExistentialQuantification
 -XNoExplicitForAll` and it is indeed useless; here's a poor if obscure
 error message:

 {{{
 Prelude> set -XExistentialQuantification -XNoExplicitForAll
 Prelude> data T = forall a . MkT a

 <interactive>:3:10:
     Not a data constructor: ‘forall’
     Perhaps you intended to use ExistentialQuantification
 }}}

 3. Hmm, this is an interesting point. The current specification is
 something like this: `GADTs` (or `TypeFamilies`, and perhaps in the future
 `EqualityConstraints`) is required if pattern matching on a constructor
 whose context (at the type at which the pattern is being checked) directly
 includes a nominal equality. Here's another curious example:
 {{{#!hs
 data Dict c where
   MkDict :: c => Dict c

 f :: Dict (Int ~ Bool) -> Bool
 f MkDict = True -- requires GADTs

 g :: Dict a -> Bool
 g MkDict = True -- doesn't
 }}}
 I don't think we should do constraint solving to determine whether an
 extension is required by a pattern match. So perhaps it's better not to
 check at all. (But I wouldn't mind terribly if we retain the check as-is.)

 4. Fair enough.

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