#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