Opened 3 years ago
Last modified 2 years ago
#13327 new bug
Figure out how to make sense of Data instances for poly-kinded datatypes
Reported by: | RyanGlScott | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | libraries/base | Version: | 8.0.1 |
Keywords: | deriving | Cc: | dreixel |
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: |
Description
Something's funny with Data.Data
. In particular, what instance do you expect when you write this?
data T phantom = T deriving Data
You might expect:
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:
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:
data T (phantom :: k) = T deriving Data
Then you do not get instance Data phantom => Data (T phantom)
as above. Instead, you get this:
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:
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:
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:
- Should we expand the special-casing for datatypes of kind
k -> *
ork1 -> k2 -> *
? Or dodataCast1
anddataCast2
even make sense for poly-kinded datatypes? - Is there a way to modify
DeriveDataTypeable
such that emitting definitions fordataCast1
anddataCast2
don't require us to default some kind variables to*
? PerhapsTypeInType
could help us here somehow.
Change History (4)
comment:1 Changed 3 years ago by
comment:2 Changed 3 years ago by
Discussion on the GHC devs mailing list: https://mail.haskell.org/pipermail/ghc-devs/2017-February/013845.html
comment:3 Changed 3 years ago by
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.
comment:4 Changed 2 years ago by
Keywords: | deriving added |
---|
The whole
dataCast1
,dataCast2
business is clearly a hack. It predates kind polymorphism. Could it be cleaned up now we have kind polymorphism?