Re: [GHC] #10431: EqualityConstraints extension?

29 Dec 2015

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

 Ad 1:

 The `data A = forall a. A a` syntax is enabled by `ExplicitForAll` +
 `GADTs` or by `ExistentialQuantification` (which implies
 `ExplicitForAll`). I imagine having explicit foralls is a feature separate
 from GADTs, so I see your point. The way I think about this is

 {{{
 ExistentialQuantification = ExplicitForAll + existentials
 GADTs = GADTSyntax + EqualityConstraints + existentials
 }}}

 We could have a flag "existentials" (which would be useless without
 ExplicitForAll or GADTSyntax) but it does not seem to be worth it. I
 suggest that whenever the compiler needs to check for existentials it
 would check whether either `ExistentialQuantification` or `GADTs` is
 enabled. This way we have the equality `GADTs = ExistentialQuantification
 + EqualityConstraints + GADTSyntax` except that the right hand side also
 implies `ExplicitForAll`.

 Ad 3:

 I think making GADT pattern matches require `-XEqualityConstraints` is a
 step in right direction. However, the current check in `TcPat` has holes
 in it. For example, consider

 {{{
 {-# LANGUAGE GADTs, MultiParamTypeClasses, FlexibleInstances #-}
 module X where
 class a ~ b => Equal a b
 instance Equal a a
 data E a b = Equal a b => E
 }}}

 {{{
 module Y where
 import X
 f :: E a b -> a -> b
 f E x = x
 }}}

 This compiles as of current GHC, and introduces type equality in module Y
 without -XGADTs. (If you change the definition of `E` to `data E a b = a ~
 b => E`, GHC will ask you to enable `-XGADTs`). Is this example a cheap
 trick or does it show a deeper problem? If we keep the check, I'd like to
 have a clear definition when a flag is required.

 Ad 4:

 I would prefer if the declaration was accepted with `GADTSyntax +
 ExistentialQuantification + EqualityConstraints`, because this way the
 flag `GADTs` would have clearer semantics. Otherwise we would have a
 distinction between `Eq :: a ~ b => Eq a b` and `Eq :: Eq a a`.

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