<p dir="ltr">No problem - I assumed that Conal had some code that demonstrated the difference.</p>
<div class="gmail_quote">On 29 Apr 2014 19:36, "Richard Eisenberg" <<a href="mailto:eir@cis.upenn.edu">eir@cis.upenn.edu</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I’m surely agreed about the Note -- I also did some helpful name-changing of related functions and am validating my work as I write.<br>
<br>
About a test case: this seems like a challenging thing to test. The new code affects only coercion optimizations. The only time the extra code would be triggered is when we, say, have a coercion built with transitivity buried inside of a TyConAppCo that needs to be split up in order to interact with the use of an axiom. (The obscurity of the case is one reason I believe I didn’t implement it this way to begin with!) So, I think I’m going to leave off the test case for now.<br>

<br>
Richard<br>
<br>
On Apr 29, 2014, at 1:08 PM, Simon Marlow <<a href="mailto:marlowsd@gmail.com">marlowsd@gmail.com</a>> wrote:<br>
<br>
> On 29/04/2014 08:56, Simon Peyton Jones wrote:<br>
>> Richard,<br>
>><br>
>> Looks good, but *surely* worth a Note [unSubCo] in the file?  It's manifestly non-obvious or you'd have done this from day 1.  Moreover, the *reason* Conal needed it, and the new optimsations it enables, are also non-obvious and deserve examples!<br>

><br>
> And let's not forget a test too :-)<br>
><br>
> Cheers,<br>
> Simon<br>
><br>
><br>
>> Evernyone: my obsession with Notes is born of the hours I have spent staring at code that has cases I don't understand; or "fixing" something turned out to be there for a good but undocumented reason.<br>

>><br>
>> Going back to unSubCo, I think the start of the documentation could be<br>
>>      if              g :: t1 ~R t2<br>
>>      then    unSubCo g :: t ~N t2<br>
>> (if it succeeds at all).<br>
>><br>
>> But why do we need it?  And what optimisations do we get?<br>
>><br>
>> Thanks<br>
>><br>
>> Simon<br>
>><br>
>><br>
>> | -----Original Message-----<br>
>> | From: ghc-commits [mailto:<a href="mailto:ghc-commits-bounces@haskell.org">ghc-commits-bounces@haskell.org</a>] On Behalf Of<br>
>> | <a href="mailto:git@git.haskell.org">git@git.haskell.org</a><br>
>> | Sent: 29 April 2014 00:51<br>
>> | To: <a href="mailto:ghc-commits@haskell.org">ghc-commits@haskell.org</a><br>
>> | Subject: [commit: ghc] master: Improve implementation of unSubCo_maybe.<br>
>> | (a3896ab)<br>
>> |<br>
>> | Repository : ssh://<a href="http://git@git.haskell.org/ghc" target="_blank">git@git.haskell.org/ghc</a><br>
>> |<br>
>> | On branch  : master<br>
>> | Link       :<br>
>> | <a href="http://ghc.haskell.org/trac/ghc/changeset/a3896ab5d2dc88160f710705bf23e6" target="_blank">http://ghc.haskell.org/trac/ghc/changeset/a3896ab5d2dc88160f710705bf23e6</a><br>
>> | e25e327da5/ghc<br>
>> |<br>
>> | >---------------------------------------------------------------<br>
>> |<br>
>> | commit a3896ab5d2dc88160f710705bf23e6e25e327da5<br>
>> | Author: Richard Eisenberg <<a href="mailto:eir@cis.upenn.edu">eir@cis.upenn.edu</a>><br>
>> | Date:   Mon Apr 28 13:33:13 2014 -0400<br>
>> |<br>
>> |     Improve implementation of unSubCo_maybe.<br>
>> |<br>
>> |     This is the result of an email conversation (off list) with<br>
>> |     Conal Elliott, who needed a stronger unSubCo_maybe. This<br>
>> |     commit adds cases to upgrade the role of a coercion when<br>
>> |     recursion is necessary to do say (for example, for a use of<br>
>> |     TransCo). As a side effect, more coercion optimizations are<br>
>> |     now possible.<br>
>> |<br>
>> |     This was not done previously because unSubCo_maybe was used<br>
>> |     only during coercion optimization, and the recursive cases<br>
>> |     looked to be unlikely. However, adding them can cause no harm.<br>
>> |<br>
>> |     unSubCo_maybe is now also exported from Coercion, for use<br>
>> |     cases like Conal's.<br>
>> |<br>
>> |<br>
>> | >---------------------------------------------------------------<br>
>> |<br>
>> | a3896ab5d2dc88160f710705bf23e6e25e327da5<br>
>> |  compiler/types/Coercion.lhs |   20 +++++++++++++++-----<br>
>> |  1 file changed, 15 insertions(+), 5 deletions(-)<br>
>> |<br>
>> | diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs<br>
>> | index af2b2fa..f60fcbd 100644<br>
>> | --- a/compiler/types/Coercion.lhs<br>
>> | +++ b/compiler/types/Coercion.lhs<br>
>> | @@ -38,7 +38,7 @@ module Coercion (<br>
>> |          splitAppCo_maybe,<br>
>> |          splitForAllCo_maybe,<br>
>> |          nthRole, tyConRolesX,<br>
>> | -        nextRole,<br>
>> | +        nextRole, unSubCo_maybe,<br>
>> |<br>
>> |          -- ** Coercion variables<br>
>> |          mkCoVar, isCoVar, isCoVarType, coVarName, setCoVarName,<br>
>> | setCoVarUnique, @@ -1051,16 +1051,26 @@ maybeSubCo2 r1 r2 co<br>
>> |<br>
>> |  -- if co is Nominal, returns it; otherwise, unwraps a SubCo; otherwise,<br>
>> | fails  unSubCo_maybe :: Coercion -> Maybe Coercion<br>
>> | +unSubCo_maybe co<br>
>> | +  | Nominal <- coercionRole co = Just co<br>
>> |  unSubCo_maybe (SubCo co)  = Just co<br>
>> |  unSubCo_maybe (Refl _ ty) = Just $ Refl Nominal ty -unSubCo_maybe<br>
>> | (TyConAppCo Representational tc cos)<br>
>> | -  = do { cos' <- mapM unSubCo_maybe cos<br>
>> | +unSubCo_maybe (TyConAppCo Representational tc coes)<br>
>> | +  = do { cos' <- mapM unSubCo_maybe coes<br>
>> |         ; return $ TyConAppCo Nominal tc cos' }  unSubCo_maybe (UnivCo<br>
>> | Representational ty1 ty2) = Just $ UnivCo Nominal ty1 ty2<br>
>> |    -- We do *not* promote UnivCo Phantom, as that's unsafe.<br>
>> |    -- UnivCo Nominal is no more unsafe than UnivCo Representational -<br>
>> | unSubCo_maybe co<br>
>> | -  | Nominal <- coercionRole co = Just co<br>
>> | +unSubCo_maybe (TransCo co1 co2)<br>
>> | +  = TransCo <$> unSubCo_maybe co1 <*> unSubCo_maybe co2 unSubCo_maybe<br>
>> | +(AppCo co1 co2)<br>
>> | +  = AppCo <$> unSubCo_maybe co1 <*> pure co2 unSubCo_maybe (ForAllCo tv<br>
>> | +co)<br>
>> | +  = ForAllCo tv <$> unSubCo_maybe co<br>
>> | +unSubCo_maybe (NthCo n co)<br>
>> | +  = NthCo n <$> unSubCo_maybe co<br>
>> | +unSubCo_maybe (InstCo co ty)<br>
>> | +  = InstCo <$> unSubCo_maybe co <*> pure ty<br>
>> |  unSubCo_maybe _ = Nothing<br>
>> |<br>
>> |  -- takes any coercion and turns it into a Phantom coercion<br>
>> |<br>
>> | _______________________________________________<br>
>> | ghc-commits mailing list<br>
>> | <a href="mailto:ghc-commits@haskell.org">ghc-commits@haskell.org</a><br>
>> | <a href="http://www.haskell.org/mailman/listinfo/ghc-commits" target="_blank">http://www.haskell.org/mailman/listinfo/ghc-commits</a><br>
>> _______________________________________________<br>
>> ghc-devs mailing list<br>
>> <a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>
>> <a href="http://www.haskell.org/mailman/listinfo/ghc-devs" target="_blank">http://www.haskell.org/mailman/listinfo/ghc-devs</a><br>
>><br>
> _______________________________________________<br>
> ghc-devs mailing list<br>
> <a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>
> <a href="http://www.haskell.org/mailman/listinfo/ghc-devs" target="_blank">http://www.haskell.org/mailman/listinfo/ghc-devs</a><br>
<br>
</blockquote></div>