[GHC] #13327: Figure out how to make sense of Data instances for poly-kinded datatypes

#13327: Figure out how to make sense of Data instances for poly-kinded datatypes -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: | Version: 8.0.1 libraries/base | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: #4028 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Something's funny with `Data.Data`. In particular, what instance do you expect when you write this? {{{#!hs data T phantom = T deriving Data }}} You might expect: {{{#!hs instance Typeable phantom => Data (T phantom) where ... }}} And indeed, it is possible to define a `Data` instance like this. But in practice, GHC actually derives this instance: {{{#!hs instance Data phantom => Data (T phantom) where ... dataCast1 f = gcast1 f }}} The reason is because GHC has special cases for when it derives `Data` instances for datatypes of kind `* -> *` or `* -> * -> *`. These special cases cause the derived `Data` instances to insert definitions for `dataCast1` or `dataCast2`, respectively, and their implementations (`gcast1` or `gcast2`, respectively) require the stronger instance context. See #4028 for a longer discussion about this. Things get far less predictable when you throw in `PolyKinds`, however. If you try this instead: {{{#!hs data T (phantom :: k) = T deriving Data }}} Then you do //not// get `instance Data phantom => Data (T phantom)` as above. Instead, you get this: {{{#!hs instance (Typeable k, Typeable (phantom :: k)) => Data (T phantom) where ... -- No implementation for dataCast1 }}} As it turns out, GHC's special-casing for deriving `Data` is not privy to datatypes of kind `k -> *` or `k1 -> k2 -> *`, just `* -> *` and `* -> * -> *`. This is all a bit disconcerting because if you look at `Data.Data`, there are many instances of the flavor: {{{#!hs deriving instance Data (p :: *) => Data (U1 p) -- U1 :: k -> * }}} This makes sense in a pre-`PolyKinds` world, but really, the most general type for this `Data` instance would be: {{{#!hs deriving instance (Typeable k, Typeable (p :: k)) => Data (U1 p) }}} Even worse, choosing the less polymorphic instance `Data (p :: *) => Data (U1 p)` via `StandaloneDeriving` doesn't even cause GHC to emit a definition for `dataCast1`—it just restricts the kind with no benefit! This whole situation doesn't sit well with me, especially since as we add more poly-kinded `Data` instances to `Data.Data`, we have to ask ourselves each time what the "right" `Data` instance is. It would be great if we could answer these questions: 1. Should we expand the special-casing for datatypes of kind `k -> *` or `k1 -> k2 -> *`? Or do `dataCast1` and `dataCast2` even make sense for poly-kinded datatypes? 2. Is there a way to modify `DeriveDataTypeable` such that emitting definitions for `dataCast1` and `dataCast2` don't require us to default some kind variables to `*`? Perhaps `TypeInType` could help us here somehow. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13327 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13327: Figure out how to make sense of Data instances for poly-kinded datatypes -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: libraries/base | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #4028 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): The whole `dataCast1`, `dataCast2` business is clearly a hack. It predates kind polymorphism. Could it be cleaned up now we have kind polymorphism? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13327#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13327: Figure out how to make sense of Data instances for poly-kinded datatypes -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: libraries/base | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #4028 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Discussion on the GHC devs mailing list: https://mail.haskell.org/pipermail/ghc-devs/2017-February/013845.html -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13327#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13327: Figure out how to make sense of Data instances for poly-kinded datatypes -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: libraries/base | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #4028 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Edward Kmett laid out an interesting (albeit not terribly practical) proposal for cleaning up the current story in https://mail.haskell.org/pipermail/ghc-devs/2017-February/013850.html. Sadly, his code doesn't actually typecheck due to what I believe is a corollary of #13337. I came up with an even grosser proposal in https://mail.haskell.org/pipermail/ghc-devs/2017-February/013852.html that //does// typecheck, but with emphasis on the "even grosser" part. There's certainly no way I'd want `Data.Data` to adopt that approach as-is. I need to think more on how I can take the programming patterns in these two proposals and clean them up into something palatable. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13327#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13327: Figure out how to make sense of Data instances for poly-kinded datatypes -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: libraries/base | Version: 8.0.1 Resolution: | Keywords: deriving Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #4028 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: => deriving -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13327#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC