Explicit Data instance is too kind-restricted

[dbaynard]

Automatically deriving an instance of Data for Tagged generates a poly-kinded version, instance (Data a, Typeable s, Typeable k) => Data (Tagged k s a), whereas the manual implementation in this library is instance (Data a, Data b) => Data (Tagged * a b).

I would like to implement Data instances for types tagged with (promoted) uninhabited types.

Would it be possible to replace the existing * restricted version for the more general version?

If so I have a very simple PR ready to go.

However, I don't understand the consequences of such a generalisation — and I'm not familiar enough with Data to appreciate the ways in which changes may break.

(My current workaround involves an {#- OVERLAPS -#} pragma.)

[RyanGlScott]

There's one annoying issue that gets in the way of this idea. If you look at the instance in its current incarnation, you'll see:

instance (Data s, Data b) => Data (Tagged s b) where
  ...
  dataCast2 f = gcast2 f

The dataCast2 implementation forces s to be of kind *. If you try deriving the instance with -ddump-deriv on, however, it'll emit an instance without an explicit dataCast2 implementation, which allows s to be poly-kinded.

Leaving off this explicit dataCast2 implementation is not without cost, as it prevents you from doing a proper implementation of polymorphic function extension, as described in section 7 of Scrap More Boilerplate: Reflection, Zips, and Generalized Casts. See also this GHC devs mailing list discussion and GHC Trac #13327.

The punchline is that you currently have to choose between full kind generality and cast-correctness with datatypes such as Tagged. I'm not sure which approach @ekmett would prefer, however.

[dbaynard]

Thanks for the quick response — I knew I wasn't the first person to notice this… and I'm glad you've added those links here, as I stumbled across this issue through the kind restriction in tagged.

[ekmett]

I'm somewhat inclined to trade the current manual instance in for the automatically generated polykinded one. dataCast2 is used very very little, compared to how much code uses Tagged at different kinds.

Using OVERLAPS / OVERLAPPING here to allow you to have your cake and eat it too, letting it work at more general kinds, but upgrade to supporting dataCast2 at kind * seems acceptable to me on the surface as well, but I haven't experimented to see how annoying the delayed refinement -- when the kind of the tagged argument is not yet fully known -- might be in practice.

[ekmett]

A similar issue arises with the Data instance for Proxy, so whatever we do here we should do there and ripple it into base.