#12087: Inconsistency in GADTs? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: GADTs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11540 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) * status: closed => new * resolution: invalid => * related: => #11540 Comment: I disagree that this not "valid" Haskell. It's certainly not //standard// Haskell, but I don't see why it ought to be rejected. Perhaps one day after #11540 is fixed, we'll need some extra language extension enabled to use this feature, but I think GHC is more than capable of handling such a thing. For background context: the structure of GADT type signatures are currently validity checked in a rather simple-minded way in [http://git.haskell.org/ghc.git/blob/86abe0e03f6cc2392758d6b45390177d44896113... gadtDeclDetails]. It splits apart a single `forall` with `splitLHsSigmaTy` and checks if the return type is of the form `T a_1 ... a_n`, where `T` is the GADT tycon. But since there's nested sigma types here, GHC mistakenly believes that the return type is `Eq a => a -> F a`, which is bad news. I think it would be possible to tweak this check to accommodate nested foralls, though. Essentially, I think we'd need to create a version of [http://git.haskell.org/ghc.git/blob/86abe0e03f6cc2392758d6b45390177d44896113... tcSplitNestedSigmaTys] that works over `LHsType` instead of `Type`, and replace the use of `splitLHsSigmaTy` with that in `gadtDeclDetails`. Then we'd typecheck `MkF` as if it had the type `forall a. (Ord a, Eq a) => a -> F a`. This isn't exactly what the user //wrote//, but it's equivalent and serviceable. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12087#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12087: Inconsistency in GADTs? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: RyanGlScott Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: GADTs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11540 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I agree this is possible in principle but it is fiddly in practice. What about {{{ MkF :: Ord a => a -> Eq a => F a }}} which ought to work too.

This isn't exactly what the user wrote, but it's equivalent and serviceable.

Yes but we'll soon have people asking that `:t MkF` prints out the type they wrote. Nothing deep here I think, but I'm not persuaded that it's a high priority. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12087#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12087: Inconsistency in GADTs? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: RyanGlScott Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: GADTs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11540 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): The underlying issue here -- that the type of GADT constructors is a bit inflexible -- is important in the context of Dependent Haskell. For example, I might want to say {{{#!hs data Foo a where MkFoo :: pi (x :: Type) -> (F x ~ Bool) => Foo x }}} This takes a ''visible'' type `x` and then asserts some constraint on `x`. The constraint must come ''after'' binding `x`, of course! So loosening up these rules will actually increase expressiveness once we have dependent types. Re comment:5, recall that `:type` takes an ''expression'', upon which it performs type inference. Thus it stands to reason that quantifiers, etc., will get shuffled around. This is why `:type +v` got added, so that the type is just reported as is, without any instantiation/regeneralization. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12087#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12087: Inconsistency in GADTs? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: GADTs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11540 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: patch => new * owner: RyanGlScott => (none) * differential: Phab:D3831 => Comment: Richard and I decided that the approach taken in Phab:D3831 wasn't the best course of action. Although it would allow exotic GADT constructor type signatures like `Ord a => Eq a => a -> F a`, it would come at a steep price: GHC would normalize the type signature to `(Ord a, Eq a) => a -> F a` behind the scenes, so you'd no longer see the type you originally wrote when you queried it with `:type +v`. For this reason, I've decided to try to improve the current error message instead, which doesn't make it very clear what the underlying problem is (nor how to fix it). Patch coming soon. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12087#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12087: Inconsistency in GADTs? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: task | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: GADTs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11540 | Differential Rev(s): Phab:D3851 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Ryan Scott ): In [changeset:"039fa1b994a8b0d6be25eb1bc711904db9661db2/ghc" 039fa1b9/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="039fa1b994a8b0d6be25eb1bc711904db9661db2" Suggest how to fix illegally nested foralls in GADT constructor type signatures Summary: Although the code from #12087 isn't accepted by GHC, we can at least do a better job of letting users know what the problem is, and how to fix it. Test Plan: make test TEST=T12087 Reviewers: goldfire, austin, bgamari Reviewed By: goldfire Subscribers: rwbarton, thomie GHC Trac Issues: #12087 Differential Revision: https://phabricator.haskell.org/D3851 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12087#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler