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

[Simon Peyton Jones]

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!

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