<div dir="ltr">Some thoughts on the topic: admittedly, probably not very useful.<br><br>A couple of obvious statements:<br><br><br><br><div>1) </div><div><br></div><div>gcast1 itself operationally makes sense regardless of the kind of the argument you're skipping past.<br></div><div><div><br></div><div><font face="monospace, monospace">gcast1 :: forall c t t' a. (Typeable t, Typeable t') => c (t a) -> Maybe (c (t' a))</font></div><div><font face="monospace, monospace"><br></font></div><div>This is an operation we can define pretty easily, however we want. It works more or less by definition. It was included in the original paper.<br></div><div><br></div><div><br></div><div><br></div><div><div>2) </div><div><br></div><div>dataCast1 on the other hand is an member of the class, and it needs that 'Data d' constraint or it can't do its job.</div></div><div><br></div><div><font face="monospace, monospace">dataCast1 :: (Data a, Typeable t) => (forall d. Data d => c (t d)) -> Maybe (c a)</font></div><div><font face="monospace, monospace"><br></font><div>Attempting to weaken the Data d constraint there doesn't work, because then dataCast1 wouldn't be able to do its job. <font face="arial, helvetica, sans-serif">Without it you can't write ext1Q in terms of dataCast1, as n</font><font face="arial, helvetica, sans-serif">oted in the but about 'bogusDataCast' in the original paper: </font><a href="https://github.com/aistrate/Articles/blob/master/Haskell/Scrap%20More%20Boilerplate%20-%20Reflection,%20Zips,%20and%20Generalised%20Casts%20(Laemmel,%20Peyton%20Jones).pdf">Scrap More Boilerplate: Reflection, Zips and Generalized Casts</a></div><div><br></div><div><br></div><div><br></div><div><br></div><div><font face="arial, helvetica, sans-serif">Since then we obviously picked up polymorphic kinds, which muddled the story about when a data instance is for a type that looks like `T d`.</font></div><div><font face="arial, helvetica, sans-serif"><br></font></div></div><div><font face="arial, helvetica, sans-serif">On the other hand, the user will be the one calling this method, and they'll have to take Data instances for d and use them to generate c (t d). Knowledge of if argument is of kind * is purely local, though. If t is Typeable and d is Data, then (t d), d is kind *, t :: * -> *. So to call dataCast1, the user has to already know the argument is kind *, and that the type t that they are trying to use (maybe not the T in the data instance itself) is of kind * -> *.<br><br>There is no contradiction in trying to call this on a data type with the wrong kind for it to succeed. T is not necessarily t. It is our job to check if it is.</font></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif">Supplying the default shouldn't lock our data instance to the form T a. If for some reason adding </font><span style="font-family:arial,helvetica,sans-serif">this default would break the instance We can make a more interesting default that does something like look at the kind of the argument first to determine if it is kind * before proceeding after casting to ensure the kinds match.</span><br></div><div><br></div><div><b>tl;dr</b><i> yes, it would seem it would be worth fixing the instances of Data produced to supply dataCast1 when the kind of the argument is polymorphic. Otherwise turning on PolyKinds in a package will simply break dataCast1 for basically all of its data types.</i></div><div><i><br></i>-Edward<i><br><br></i></div><div>P.S. Ultimately, in a perfect world we'd be able to unify dataCast1 and dataCast2 with some tricky base case for kind k1 = * and induction over k -> k1. Off hand, I don't see how to do it. I played for a while with trying to write a higher kinded Data to support this, but my scribbles didn't cohere into usable code. gfoldl pretty much locks you into kind *. I even tried playing with profunctors and powers here to no real avail. I do have some old Data1 code in an syb-extras package that I use to write a few 'impossible' Data instances, but that seems to be solving a different, if related, problem, and doesn't scale up to arbitrary kinds. Ideally there'd be a plausible Data that makes sense for other kinds k, and everything could become dataCast1, w/ dataCast2, and the missing higher versions just an iterated application of it. I just don't see that there is a way to turn it into code.</div><div><br></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Feb 23, 2017 at 2:51 PM, Ryan Scott <span dir="ltr"><<a href="mailto:ryan.gl.scott@gmail.com" target="_blank">ryan.gl.scott@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Pedro,<br>
<br>
I'm quite confused by a peculiarity of deriving Data (more info in<br>
Trac #13327 [1]). In particular, if you write this:<br>
<br>
data T phantom = T<br>
deriving Data<br>
<br>
Then the derived Data instance is NOT this:<br>
<br>
instance Typeable phantom => Data (T phantom) where<br>
...<br>
<br>
But instead, it's this:<br>
<br>
instance Data phantom => Data (T phantom) where<br>
...<br>
dataCast1 f = gcast1 f<br>
<br>
The gcast1 part is why it requires the stronger (Data phantom)<br>
context, as you noted in Trac #4028 [2].<br>
<br>
What confuses me, however, is that is apparently does not carry over<br>
to poly-kinded datatypes. For instance, if you write this:<br>
<br>
data T (phantom :: k) = T<br>
deriving Data<br>
<br>
Then you do NOT get this instance:<br>
<br>
instance Data (phantom :: *) => Data (T phantom) where<br>
...<br>
dataCast1 f = gcast1 f<br>
<br>
But instead, you get this instance!<br>
<br>
instance (Typeable k, Typeable (phantom :: k)) => Data (T phantom) where<br>
...<br>
-- No implementation for dataCast1<br>
<br>
This is quite surprising to me. I'm not knowledgeable enough about<br>
Data to know for sure if this is an oversight, expected behavior, or<br>
something else, so I was hoping you (or someone else highly<br>
knowledgeable about SYB-style generic programming) could help me out<br>
here.<br>
<br>
In particular:<br>
<br>
1. Does emitting "dataCast1 f = gcast1 f" for datatypes of kind (k -><br>
*) make sense? Or does it only make sense for types of kind (* -> *)?<br>
2. Is there an alternate way to define dataCast1 that doesn't require<br>
the stronger Data context, but instead only requires the more general<br>
Typeable context?<br>
<br>
Ryan S.<br>
-----<br>
[1] <a href="https://ghc.haskell.org/trac/ghc/ticket/13327" rel="noreferrer" target="_blank">https://ghc.haskell.org/trac/<wbr>ghc/ticket/13327</a><br>
[2] <a href="https://ghc.haskell.org/trac/ghc/ticket/4028#comment:5" rel="noreferrer" target="_blank">https://ghc.haskell.org/trac/<wbr>ghc/ticket/4028#comment:5</a><br>
______________________________<wbr>_________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div><br></div>