#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): Thanks for thinking through the implications of this! I'm now not sure that the principle I articulated (`GADTs = GADTSyntax + ExistentialQuantification + EqualityConstraints`) is essential. My instinctive reactions are: 1. Perhaps it would be better if this still required `ExistentialQuantification`, i.e. `GADTs` would enable existential GADTs but not plain existential datatypes? 2. Yes. 3. I'm in two minds about this. I know our general policy is to require flags only at definition sites, but type refinement on pattern matching is the whole point of GADTs, and is significantly different to non-GADT matching, so it seems like it is reasonable to mark the use sites as well. Perhaps GADT pattern matches should require `EqualityConstraints` (and hence `GADTs` would suffice)? 4. I'm surprised that `GADTs` is not required in your example: my vote is to treat it as a bug and fix it without a deprecation period. I'd expect `GADTSyntax + ExistentialQuantification` to allow data constructors with existential variables and contexts, but not specialized result types. I don't particularly mind whether this declaration is or is not accepted by `GADTSyntax + ExistentialQuantification + EqualityConstraints` without `GADTs`. I'd be interested to hear what others think. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10431#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler