Of course -- that worked. I was very muddled in my thinking yesterday, figuring that the error was legitimate. Thanks, Richard On 2013-07-23 20:11, Simon Peyton-Jones wrote:

I'd suggest using "WithinType" as the argument to synifyType that's currently an error call in Haddock.Convert line 356

Simon

| -----Original Message----- | From: Richard Eisenberg [mailto:eir@cis.upenn.edu] | Sent: 23 July 2013 15:12 | To: Edward Kmett | Cc: José Pedro Magalhães; Dimitrios Vytiniotis; Simon Peyton-Jones; Stephanie | Weirich; josepedromagalhaes@gmail.com; libraries@haskell.org; Conor McBride | Subject: Re: new-typeable, new cast? | | Well, there was another surprise. Haddock can't deal with Proxy for some | reason. (It dies with the error "synifyKind". I looked but couldn't | figure out what was going on there.) I've posted a bug report on the | haddock Trac (http://trac.haskell.org/haddock/ticket/242), but | validation currently fails on the branch (data-proxy) with this work in | it. So, I can't merge with master. | | At this point, I'm going to wait until the haddock folks fix that bug, | then assuming all is well, I will merge. | | Richard | | | | On 2013-07-23 09:59, Richard Eisenberg wrote: | > I think that we really only need (eqT :: (Typeable a, Typeable b) => | > Maybe (a :=: b)). All of the gcasts can be defined in terms of that | > function. | > | > However, I concretely propose (and plan to do) this: Leave gcast1 and | > gcast2 in and undeprecated. Simon is right that there is an infinite | > family of gcasts, and there may be no great reason to have gcast1 and | > gcast2 and none of the others, but there also doesn't seem to be a | > compelling reason to remove them (or deprecate them) and break code. | > In any case, this debate doesn't seem to be a good reason to hold up | > wrapping the rest of these details up, because we can always revisit | > and add or remove functions in the coming weeks. I'm not trying to | > ramrod my ideas through here, just trying to favor action over | > inaction -- anyone can feel free to come back and make edits after I | > push. | > | > Barring another surprise, I believe I'll push before lunch (in the UK). | > | > Richard | > | > On 2013-07-23 03:04, Edward Kmett wrote: | >> If we have gcast1 then can't the others just be applications of that | >> under various wrappers? | >> | >> In practice we should be able to implement gcast2 by working on a | >> single argument with a product kind, and so on and so forth, but we | >> need at least gcast1 as a base case. | >> | >> In theory this is the more fundamental operation, and gcast is | >> defineable in terms of gcast1 with a wrapper with a unit-kinded | >> argument, but I wouldn't want to invert the relationship. | >> | >> This is based on the same trick that Conor uses to show that a single | >> (poly-kinded) type argument is enough for all of the indexed monad | >> machinery, no matter how complicated it gets. | >> | >> TL;DR We only need gcast1, the others are window-dressing. | >> | >> -Edward | >> | >> On Mon, Jul 22, 2013 at 9:31 PM, Simon Peyton-Jones | >> wrote: | >> | >>> Harump.  There is *still* an infinite family going on here, isn't | >>> there? | >>> | >>> gcast :: forall a b c. (Typeable a, Typeable b) => c a -> Maybe (c | >>> b) | >>> | >>> but what about this | >>> | >>> gcast_2 :: forall a b c d e. (Typeable a, Typeable b, Typeable d, | >>> Typeable e) | >>>              => c a b -> c d e | >>> | >>> Then, as you point out, we have gcast1 and 2 (etc).  And there are | >>> more.  What about | >>> | >>> gcast1' :: forall c t a a'. (Typeable a, Typeable a') | >>>        => c (t a) -> Maybe (c (t a')) | >>> | >>> One could imagine all sorts of combinations of bits that stay the | >>> same (and hence do not need to be Typeable) and bits that change | >>> (and hence do need to be Typable). | >>> | >>> As Edward says, all these functions can be polykinded, which makes | >>> them more useful, but there still seem too many of them. | >>> | >>> I wonder if we could instead make a combinatory library that lets | >>> us build these functions easily.  It think we are going to offer a | >>> function that computes an equality witness: | >>> | >>> mkEqWit :: (Typable a, Typeable b) => Maybe (EQ a b) | >>> | >>> Now we need to be able to compose witnesses: | >>> | >>> appEqWit :: Eq a b -> Eq c d -> Eq (a c) (b d) | >>> reflEqWit :: Eq a a | >>> | >>> Now, I think you can make all those other casts. | >>> | >>> Would that do the job better? | >>> | >>> Simon | >>> | >>> |  -----Original Message----- | >>> |  From: Richard Eisenberg [mailto:eir@cis.upenn.edu] | >>> |  Sent: 22 July 2013 10:20 | >>> |  To: José Pedro Magalhães | >>> |  Cc: Dimitrios Vytiniotis; Simon Peyton-Jones; Stephanie | >>> Weirich; | >>> |  josepedromagalhaes@gmail.com; libraries@haskell.org; Conor | >>> McBride | >>> |  Subject: Re: new-typeable, new cast? | >>> | | >>> | >>> |  There seems to be a small tangle. The proposal includes | >>> deprecating | >>> |  gcast1 and gcast2 in favor of the poly-kinded gcast. But, there | >>> is a | >>> |  small discrepancy between these. Here are the type signatures: | >>> | | >>> |  > gcast :: forall a b c. (Typeable a, Typeable b) => c a -> | >>> Maybe (c b) | >>> |  > gcast1 :: forall c t t' a. (Typeable (t :: * -> *), Typeable | >>> t') | >>> |  >        => c (t a) -> Maybe (c (t' a)) | >>> | | >>> |  The difference is that gcast1 does *not* require the variable | >>> `a` to be | >>> |  Typeable, whereas defining gcast1 = gcast does require this. | >>> Not | >>> |  requiring `a` to be Typeable seems correct to me, as the type | >>> signature | >>> |  of gcast1 requires both uses of `a` to be the same. But, gcast | >>> isn't | >>> |  smart enough to know that. Here are some ideas of how to | >>> proceed: | >>> | | >>> |  - Keep gcast1 and gcast2 undeprecated. | >>> |  - Require clients to add more Typeable constraints (for | >>> example, in | >>> |  Data.Data) to get their code to compile with gcast. | >>> |  - Come up with some other workaround, but none is striking me | >>> at the | >>> |  moment. | >>> | | >>> |  Thoughts? | >>> | | >>> |  Richard | >>> | | >>> |  On 2013-07-22 09:44, Richard Eisenberg wrote: | >>> |  > I was waiting to respond to Shachaf's email saying "pushed", | >>> but | >>> |  > instead, I have to say "currently validating". | >>> |  > | >>> |  > Expect this by the end of the day. Sorry it's taken so long! | >>> |  > | >>> |  > Richard | >>> |  > | >>> |  > On 2013-07-22 09:23, José Pedro Magalhães wrote: | >>> |  >> Thanks for bringing this up again. This was started in my | >>> data-proxy | >>> |  >> branch of base [1], | >>> |  >> but never really finished. We definitely want to have this | >>> in 7.8, and | >>> |  >> I think there's | >>> |  >>  only some minor finishing work to do (check if we have all | >>> the | >>> |  >> instances we want, | >>> |  >> document, etc.). Perhaps you can look through what's there | >>> already, | >>> |  >> and what you | >>> |  >> think is missing? I'm more than happy to accept contributing | >>> patches | >>> |  >> too :-) | >>> |  >> | >>> |  >> Thanks, | >>> |  >> Pedro | >>> |  >> | >>> |  >> On Sun, Jul 21, 2013 at 3:09 AM, Shachaf Ben-Kiki | >>> | >>> |  >> wrote: | >>> |  >> | >>> |  >>> On Mon, Mar 4, 2013 at 11:12 AM, José Pedro Magalhães | >>> |  >>> wrote: | >>> |  >>>> Hi, | >>> |  >>>> | >>> |  >>>> On Mon, Mar 4, 2013 at 4:51 PM, Richard Eisenberg | >>> |  >>> wrote: | >>> |  >>>>> | >>> |  >>>>> Unless I'm missing something, this all looks very | >>> |  >>> straightforward. The | >>> |  >>>>> implementation is there, already, in the guise of (gcast | >>> Refl). | >>> |  >>> We would | >>> |  >>>>> just shuffle the definitions around a bit. Am I indeed | >>> missing | >>> |  >>> something? | >>> |  >>>> | >>> |  >>>> | >>> |  >>>> I think that is the case indeed. Though I agree that it | >>> would be | >>> |  >>> a nice | >>> |  >>>> addition to Data.Typeable. | >>> |  >>>> | >>> |  >>>> | >>> |  >>> | >>> |  >>> This thread is a few months old now, but it looks like | >>> people were | >>> |  >>> generally in favor of adding (gcast Refl) to Data.Typeable. | >>> I've | >>> |  >>> used | >>> |  >>> it in real code in at least one place since then (where I | >>> just | >>> |  >>> defined | >>> |  >>> it locally). It doesn't look like it's actually been added, | >>> though | >>> |  >>> -- | >>> |  >>> is it planned to go into HEAD eventually? | >>> |  >>> | >>> |  >>>     Shachaf | >>> |  >> | >>> |  >> | >>> |  >> | >>> |  >> Links: | >>> |  >> ------ | >>> |  >> [1] https://github.com/ghc/packages-base/tree/data-proxy [1] | >>> |  > | >>> |  > _______________________________________________ | >>> |  > Libraries mailing list | >>> |  > Libraries@haskell.org | >>> |  > http://www.haskell.org/mailman/listinfo/libraries [2] | >>> | >>> _______________________________________________ | >>> Libraries mailing list | >>> Libraries@haskell.org | >>> http://www.haskell.org/mailman/listinfo/libraries [2] | >> | >> | >> | >> Links: | >> ------ | >> [1] https://github.com/ghc/packages-base/tree/data-proxy | >> [2] http://www.haskell.org/mailman/listinfo/libraries | > | > _______________________________________________ | > Libraries mailing list | > Libraries@haskell.org | > http://www.haskell.org/mailman/listinfo/libraries