[GHC] #11310: Surprising accepted constructor for GADT instance of data family
#11310: Surprising accepted constructor for GADT instance of data family -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs -- Accepted: data family Foo (x :: *) :: * -> * data instance Foo Int Char where Foo :: Foo Int Char -- Not accepted data Bar Char where Bar :: Bar Char }}} It seems the second example, using a simple GADT, is syntactically barred from having a specific type constructor in its "head". That syntactic restriction is relaxed, however, for ''all'' arguments of the data instance, even though I'd expect it only for the first argument. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11310 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11310: Surprising accepted constructor for GADT instance of data family -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 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 goldfire): This is a documentation bug more than an implementation bug (or perhaps a design bug). In contrast to type families, data family results must always have kind `*`. And the variables in a data family declaration have no scope anyway (ignoring `TypeInType` stuff), so a user may usefully say {{{#!hs data family DF1 :: * -> Nat -> * }}} as equivalent to {{{#!hs data family DF2 x (y :: Nat) }}} Because type families may have higher-kinded results (that is, result kinds with arrows), type families have to distinguish between proper arguments and components of the result. Do you have an improvement to suggest, in either the design or documentation? I admit this inconsistency is quite surprising, but I don't have a better approach in mind. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11310#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC