#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

#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

#10431: EqualityConstraints extension? -------------------------------------+------------------------------------- Reporter: adamgundry | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10431#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10431: EqualityConstraints extension? -------------------------------------+------------------------------------- Reporter: adamgundry | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.4.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 AntC): However this gets resolved, please doco which extensions enable the `(~)` syntax. Currently at 8.0.1: * Section 10.14.1 'Equality Constraints' tells how to use `(~)`, but not how to enable it. * Section 10.8.3.3 'Relaxed rules for instance contexts' mentions -XGADTs or -XTypeFamilies, as an aside.\\I'd call that a less than obvious place to look. It's not too bad: if you use `(~)` without either of those switched on, GHC's error message is very clear. (See this post https://mail.haskell.org/pipermail/glasgow-haskell- users/2017-April/026521.html.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10431#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler