#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