[commit: ghc] master: Improve implementation of unSubCo_maybe. (a3896ab)

[Richard Eisenberg]

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.

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.

Richard

On Apr 29, 2014, at 1:08 PM, Simon Marlow <marlowsd at gmail.com> wrote:

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