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

[Simon Peyton Jones]

I'm sympathetic about not having a test for this kind of thing.

Simon

| -----Original Message-----
| From: Richard Eisenberg [mailto:eir at cis.upenn.edu]
| Sent: 29 April 2014 19:36
| To: Simon Marlow
| Cc: Simon Peyton Jones; ghc-devs at haskell.org
| Subject: Re: [commit: ghc] master: Improve implementation of
| unSubCo_maybe. (a3896ab)
| 
| 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