<div dir="ltr"><div>That is a right mess.</div><div><br></div><div>I've now stepped a bit outside of what I think is a practical recommendation, but let's just keep playing for the fun of it.</div><div><br></div><div>This is going to be hard to do without access to GHC at the moment but here goes:</div><div><br></div>If phantom was of kind * then dataCast1 would need the (Data phantom), so we need some sort of way to supply it.<div><br></div><div>Looks like we'd need some 'Data if *'. We don't have exponentials in the type checker though. They are admissable, just not a thing GHC does today. We could fake it with some nastiness perhaps:</div><div><br><div>class (Typeable t, Typeable k) => DataIfStar (k :: t) where</div><div>  dataIf :: (t ~ Type) => proxy k -> (Data k => r) -> r</div><div><br></div><div>You might be able to make a couple of overlapping instances, as much as it pains me to consider. (Here be dragons, I haven't thought this through.</div><div><br>instance Data k => DataIfStar k where -- overlapping</div><div>  dataIf _ r = r</div><div><br></div><div>instance DataIfStar k where -- overlapped</div><div>  dataIf _ _ = undefined</div><div><br>Then after you check k ~ Type in the instance you could invoke dataIf using the knowledge that k ~ Type to pull the Data phantom instance into scope. You'd get a type signature like:<br><br>dataCast1T :: forall k c t (phantom :: k).<br>                  (Typeable t, DataIfStar phantom)<br><span class="gmail-">               => (forall d. Data d => c (t d))<br></span>               -> Maybe (c (T phantom))<br><br>which would mean the Data instance for T phantom would get a constraint like:<br><br>instance DataIfStar phantom => Data (T phantom)</div><div><br>Does that make sense?<br><br></div></div><div>-Edward</div><div><br></div><div><br></div><div><br></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Feb 23, 2017 at 10:30 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:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><span class="gmail-">> Supplying the default shouldn't lock our data instance to the form T a. If for some reason adding 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.<br>
<br>
</span>Interesting. Do you happen to know how to write this "more interesting<br>
default"? I've tried various things, but sadly I can't escape past the<br>
typechecker. My attempt that made it the furthest was this:<br>
<br>
    {-# LANGUAGE GADTs #-}<br>
    {-# LANGUAGE PolyKinds #-}<br>
    {-# LANGUAGE RankNTypes #-}<br>
    {-# LANGUAGE ScopedTypeVariables #-}<br>
    {-# LANGUAGE TypeInType #-}<br>
    {-# LANGUAGE TypeOperators #-}<br>
    module DataCast where<br>
<br>
    import Data.Data<br>
    import Data.Kind (Type)<br>
<span class="gmail-"><br>
    data T (phantom :: k) = T<br>
<br>
</span>    dataCast1T :: forall k c t (phantom :: k).<br>
                  (Typeable k, Typeable t, Typeable phantom)<br>
<span class="gmail-">               => (forall d. Data d => c (t d))<br>
</span>               -> Maybe (c (T phantom))<br>
    dataCast1T f = case eqT :: Maybe (k :~: Type) of<br>
                     Nothing   -> Nothing<br>
                     Just Refl -> gcast1 f<br>
<br>
This would work were it not for the constraints involved:<br>
<br>
    Could not deduce (Data phantom) arising from a use of ‘f’<br>
<br>
It seems that applying f is forcing the type parameter to T (phantom)<br>
to be a Data instance, which obviously can't happen if (phantom :: k).<br>
I don't know a way around this, though, as I'm not aware of a way to<br>
"defer" a class constraint (unlike equality constraints, which can be<br>
deferred via Typeable).<br>
<br>
Ryan S.<br>
<div class="gmail-HOEnZb"><div class="gmail-h5"><br>
On Thu, Feb 23, 2017 at 5:49 PM, Edward Kmett <<a href="mailto:ekmett@gmail.com">ekmett@gmail.com</a>> wrote:<br>
> Some thoughts on the topic: admittedly, probably not very useful.<br>
><br>
> A couple of obvious statements:<br>
><br>
><br>
><br>
> 1)<br>
><br>
> gcast1 itself operationally makes sense regardless of the kind of the<br>
> argument you're skipping past.<br>
><br>
> gcast1 :: forall c t t' a. (Typeable t, Typeable t') => c (t a) -> Maybe (c<br>
> (t' a))<br>
><br>
> This is an operation we can define pretty easily, however we want. It works<br>
> more or less by definition. It was included in the original paper.<br>
><br>
><br>
><br>
> 2)<br>
><br>
> dataCast1 on the other hand is an member of the class, and it needs that<br>
> 'Data d' constraint or it can't do its job.<br>
><br>
> dataCast1 :: (Data a, Typeable t) => (forall d. Data d => c (t d)) -> Maybe<br>
> (c a)<br>
><br>
> Attempting to weaken the Data d constraint there doesn't work, because then<br>
> dataCast1 wouldn't be able to do its job. Without it you can't write ext1Q<br>
> in terms of dataCast1, as noted in the but about 'bogusDataCast' in the<br>
> original paper: Scrap More Boilerplate: Reflection, Zips and Generalized<br>
> Casts<br>
><br>
><br>
><br>
><br>
> Since then we obviously picked up polymorphic kinds, which muddled the story<br>
> about when a data instance is for a type that looks like `T d`.<br>
><br>
> On the other hand, the user will be the one calling this method, and they'll<br>
> have to take Data instances for d and use them to generate c (t d).<br>
> Knowledge of if argument is of kind * is purely local, though. If t is<br>
> Typeable and d is Data, then (t d), d is kind *, t :: * -> *. So to call<br>
> dataCast1, the user has to already know the argument is kind *, and that the<br>
> type t that they are trying to use (maybe not the T in the data instance<br>
> itself) is of kind * -> *.<br>
><br>
> There is no contradiction in trying to call this on a data type with the<br>
> wrong kind for it to succeed. T is not necessarily t. It is our job to check<br>
> if it is.<br>
><br>
> Supplying the default shouldn't lock our data instance to the form T a. If<br>
> for some reason adding this default would break the instance We can make a<br>
> more interesting default that does something like look at the kind of the<br>
> argument first to determine if it is kind * before proceeding after casting<br>
> to ensure the kinds match.<br>
><br>
> tl;dr yes, it would seem it would be worth fixing the instances of Data<br>
> produced to supply dataCast1 when the kind of the argument is polymorphic.<br>
> Otherwise turning on PolyKinds in a package will simply break dataCast1 for<br>
> basically all of its data types.<br>
><br>
> -Edward<br>
><br>
> P.S. Ultimately, in a perfect world we'd be able to unify dataCast1 and<br>
> dataCast2 with some tricky base case for kind k1 = * and induction over k -><br>
> k1. Off hand, I don't see how to do it. I played for a while with trying to<br>
> write a higher kinded Data to support this, but my scribbles didn't cohere<br>
> into usable code. gfoldl pretty much locks you into kind *. I even tried<br>
> playing with profunctors and powers here to no real avail. I do have some<br>
> old Data1 code in an syb-extras package that I use to write a few<br>
> 'impossible' Data instances, but that seems to be solving a different, if<br>
> related, problem, and doesn't scale up to arbitrary kinds. Ideally there'd<br>
> be a plausible Data that makes sense for other kinds k, and everything could<br>
> become dataCast1, w/ dataCast2, and the missing higher versions just an<br>
> iterated application of it. I just don't see that there is a way to turn it<br>
> into code.<br>
><br>
><br>
> On Thu, Feb 23, 2017 at 2:51 PM, Ryan Scott <<a href="mailto:ryan.gl.scott@gmail.com">ryan.gl.scott@gmail.com</a>> wrote:<br>
>><br>
>> 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)<br>
>> 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>
><br>
><br>
</div></div></blockquote></div><br></div></div>