Implement 'left' and 'right' coercions
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 17 Sep 2012 10:34:28 +0000 (11:34 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Mon, 17 Sep 2012 12:46:28 +0000 (13:46 +0100)
This patch finally adds 'left' and 'right' coercions back into
GHC.  Trac #7205 gives the details.

The main change is to add a new constructor to Coercion:

  data Coercion
    = ...
    | NthCo  Int         Coercion     -- OLD, still there
    | LRCo   LeftOrRight Coercion     -- NEW

  data LeftOrRight = CLeft | CRight

Plus:
  * Similar change to TcCoercion
  * Use LRCo when decomposing AppTys
  * Coercion optimisation needs to handle left/right

The rest is just knock-on effects.

15 files changed:
compiler/coreSyn/CoreLint.lhs
compiler/coreSyn/ExternalCore.lhs
compiler/coreSyn/MkExternalCore.lhs
compiler/coreSyn/PprExternalCore.lhs
compiler/coreSyn/TrieMap.lhs
compiler/deSugar/DsBinds.lhs
compiler/iface/BinIface.hs
compiler/iface/IfaceType.lhs
compiler/iface/TcIface.lhs
compiler/typecheck/TcCanonical.lhs
compiler/typecheck/TcEvidence.lhs
compiler/typecheck/TcHsSyn.lhs
compiler/typecheck/TcType.lhs
compiler/types/Coercion.lhs
compiler/types/OptCoercion.lhs

index dcd366f..250efdd 100644 (file)
@@ -838,6 +838,19 @@ lintCoercion the_co@(NthCo n co)
            _ -> failWithL (hang (ptext (sLit "Bad getNth:"))
                               2 (ppr the_co $$ ppr s $$ ppr t)) }
 
+lintCoercion the_co@(LRCo lr co)
+  = do { (_,s,t) <- lintCoercion co
+       ; case (splitAppTy_maybe s, splitAppTy_maybe t) of
+           (Just s_pr, Just t_pr) 
+             -> return (k, s_pick, t_pick)
+             where
+               s_pick = pickLR lr s_pr
+               t_pick = pickLR lr t_pr
+               k = typeKind s_pick
+
+           _ -> failWithL (hang (ptext (sLit "Bad LRCo:"))
+                              2 (ppr the_co $$ ppr s $$ ppr t)) }
+
 lintCoercion (InstCo co arg_ty)
   = do { (k,s,t)  <- lintCoercion co
        ; arg_kind <- lintType arg_ty
index d2f6691..287f080 100644 (file)
@@ -74,6 +74,9 @@ data Ty
   | UnsafeCoercion Ty Ty
   | InstCoercion Ty Ty
   | NthCoercion Int Ty
+  | LRCoercion LeftOrRight Ty
+
+data LeftOrRight = CLeft | CRight
 
 data Kind 
   = Klifted
index 2103708..8844818 100644 (file)
@@ -326,8 +326,13 @@ make_co dflags (UnsafeCo t1 t2)      = C.UnsafeCoercion (make_ty dflags t1) (mak
 make_co dflags (SymCo co)            = C.SymCoercion (make_co dflags co)
 make_co dflags (TransCo c1 c2)       = C.TransCoercion (make_co dflags c1) (make_co dflags c2)
 make_co dflags (NthCo d co)          = C.NthCoercion d (make_co dflags co)
+make_co dflags (LRCo lr co)          = C.LRCoercion (make_lr lr) (make_co dflags co)
 make_co dflags (InstCo co ty)        = C.InstCoercion (make_co dflags co) (make_ty dflags ty)
 
+make_lr :: LeftOrRight -> C.LeftOrRight
+make_lr CLeft  = C.CLeft
+make_lr CRight = C.CRight
+
 -- Used for both tycon app coercions and axiom instantiations.
 make_conAppCo :: DynFlags -> C.Qual C.Tcon -> [Coercion] -> C.Ty
 make_conAppCo dflags con cos =
index 26e64ee..2290810 100644 (file)
@@ -114,6 +114,10 @@ pty (UnsafeCoercion t1 t2) =
   sep [text "%unsafe", paty t1, paty t2]
 pty (NthCoercion n t) =
   sep [text "%nth", int n, paty t]
+pty (LRCoercion CLeft t) =
+  sep [text "%left", paty t]
+pty (LRCoercion CRight t) =
+  sep [text "%right", paty t]
 pty (InstCoercion t1 t2) =
   sep [text "%inst", paty t1, paty t2]
 pty t = pbty t
index 7170f1c..6bc78a8 100644 (file)
@@ -470,6 +470,8 @@ data CoercionMap a
        , km_sym    :: CoercionMap a
        , km_trans  :: CoercionMap (CoercionMap a)
        , km_nth    :: IntMap.IntMap (CoercionMap a)
+       , km_left   :: CoercionMap a
+       , km_right  :: CoercionMap a
        , km_inst   :: CoercionMap (TypeMap a) }
 
 wrapEmptyKM :: CoercionMap a
@@ -477,7 +479,8 @@ wrapEmptyKM = KM { km_refl = emptyTM, km_tc_app = emptyNameEnv
                  , km_app = emptyTM, km_forall = emptyTM
                  , km_var = emptyTM, km_axiom = emptyNameEnv
                  , km_unsafe = emptyTM, km_sym = emptyTM, km_trans = emptyTM
-                 , km_nth = emptyTM, km_inst = emptyTM }
+                 , km_nth = emptyTM, km_left = emptyTM, km_right = emptyTM
+                 , km_inst = emptyTM }
 
 instance TrieMap CoercionMap where
    type Key CoercionMap = Coercion
@@ -493,7 +496,8 @@ mapC f (KM { km_refl = krefl, km_tc_app = ktc
            , km_app = kapp, km_forall = kforall
            , km_var = kvar, km_axiom = kax
            , km_unsafe = kunsafe, km_sym = ksym, km_trans = ktrans
-           , km_nth = knth, km_inst = kinst })
+           , km_nth = knth, km_left = kml, km_right = kmr
+           , km_inst = kinst })
   = KM { km_refl   = mapTM f krefl
        , km_tc_app = mapNameEnv (mapTM f) ktc
        , km_app    = mapTM (mapTM f) kapp
@@ -504,6 +508,8 @@ mapC f (KM { km_refl = krefl, km_tc_app = ktc
        , km_sym    = mapTM f ksym
        , km_trans  = mapTM (mapTM f) ktrans
        , km_nth    = IntMap.map (mapTM f) knth
+       , km_left   = mapTM f kml
+       , km_right  = mapTM f kmr
        , km_inst   = mapTM (mapTM f) kinst }
 
 lkC :: CmEnv -> Coercion -> CoercionMap a -> Maybe a
@@ -522,6 +528,8 @@ lkC env co m
     go (CoVarCo v)         = km_var    >.> lkVar env v
     go (SymCo c)           = km_sym    >.> lkC env c
     go (NthCo n c)         = km_nth    >.> lookupTM n >=> lkC env c
+    go (LRCo CLeft  c)     = km_left   >.> lkC env c
+    go (LRCo CRight c)     = km_right  >.> lkC env c
 
 xtC :: CmEnv -> Coercion -> XT a -> CoercionMap a -> CoercionMap a
 xtC env co f EmptyKM = xtC env co f wrapEmptyKM
@@ -534,9 +542,11 @@ xtC env (UnsafeCo t1 t2)    f m = m { km_unsafe = km_unsafe m |> xtT env t1 |>>
 xtC env (InstCo c t)        f m = m { km_inst   = km_inst m   |> xtC env c  |>> xtT env t  f }
 xtC env (ForAllCo v c)      f m = m { km_forall = km_forall m |> xtC (extendCME env v) c 
                                                   |>> xtBndr env v f }
-xtC env (CoVarCo v)         f m = m { km_var   = km_var m |> xtVar env  v f }
-xtC env (SymCo c)           f m = m { km_sym   = km_sym m |> xtC env    c f }
-xtC env (NthCo n c)         f m = m { km_nth   = km_nth m |> xtInt n |>> xtC env c f } 
+xtC env (CoVarCo v)         f m = m { km_var   = km_var m   |> xtVar env v f }
+xtC env (SymCo c)           f m = m { km_sym   = km_sym m   |> xtC env   c f }
+xtC env (NthCo n c)         f m = m { km_nth   = km_nth m   |> xtInt n |>> xtC env c f } 
+xtC env (LRCo CLeft  c)     f m = m { km_left  = km_left  m |> xtC env c f } 
+xtC env (LRCo CRight c)     f m = m { km_right         = km_right m |> xtC env c f } 
 
 fdC :: (a -> b -> b) -> CoercionMap a -> b -> b
 fdC _ EmptyKM = \z -> z
@@ -550,6 +560,8 @@ fdC k m = foldTM k (km_refl m)
         . foldTM k (km_sym m)
         . foldTM (foldTM k) (km_trans m)
         . foldTM (foldTM k) (km_nth m)
+        . foldTM k          (km_left m)
+        . foldTM k          (km_right m)
         . foldTM (foldTM k) (km_inst m)
 \end{code}
 
index 803cdd8..b418c8d 100644 (file)
@@ -834,6 +834,7 @@ ds_tc_coercion subst tc_co
     go (TcSymCo co)           = mkSymCo (go co)
     go (TcTransCo co1 co2)    = mkTransCo (go co1) (go co2)
     go (TcNthCo n co)         = mkNthCo n (go co)
+    go (TcLRCo lr co)         = mkLRCo lr (go co)
     go (TcInstCo co ty)       = mkInstCo (go co) ty
     go (TcLetCo bs co)        = ds_tc_coercion (ds_co_binds bs) co
     go (TcCastCo co1 co2)     = mkCoCast (go co1) (go co2)
index a319f6e..362df3f 100644 (file)
@@ -20,11 +20,12 @@ module BinIface (
 #include "HsVersions.h"
 
 import TcRnMonad
-import TyCon      (TyCon, tyConName, tupleTyConSort, tupleTyConArity, isTupleTyCon)
+import TyCon
 import DataCon    (dataConName, dataConWorkId, dataConTyCon)
 import PrelInfo   (wiredInThings, basicKnownKeyNames)
 import Id         (idName, isDataConWorkId_maybe)
 import CoreSyn    (DFunArg(..))
+import Coercion   (LeftOrRight(..))
 import TysWiredIn
 import IfaceEnv
 import HscTypes
@@ -1037,6 +1038,15 @@ instance Binary IfaceTyCon where
    put_ bh (IfaceTc ext) = put_ bh ext
    get bh = liftM IfaceTc (get bh)
 
+instance Binary LeftOrRight where
+   put_ bh CLeft  = putByte bh 0
+   put_ bh CRight = putByte bh 1
+
+   get bh = do { h <- getByte bh
+               ; case h of
+                   0 -> return CLeft
+                   _ -> return CRight }
+
 instance Binary IfaceCoCon where
    put_ bh (IfaceCoAx n)       = do { putByte bh 0; put_ bh n }
    put_ bh IfaceReflCo         = putByte bh 1
@@ -1045,6 +1055,7 @@ instance Binary IfaceCoCon where
    put_ bh IfaceTransCo        = putByte bh 4
    put_ bh IfaceInstCo         = putByte bh 5
    put_ bh (IfaceNthCo d)      = do { putByte bh 6; put_ bh d }
+   put_ bh (IfaceLRCo lr)      = do { putByte bh 7; put_ bh lr }
 
    get bh = do
         h <- getByte bh
@@ -1056,6 +1067,7 @@ instance Binary IfaceCoCon where
           4 -> return IfaceTransCo
           5 -> return IfaceInstCo
           6 -> do { d <- get bh; return (IfaceNthCo d) }
+          7 -> do { lr <- get bh; return (IfaceLRCo lr) }
           _ -> panic ("get IfaceCoCon " ++ show h)
 
 -------------------------------------------------------------------------
index 225a3c8..4a35f00 100644 (file)
@@ -99,7 +99,7 @@ data IfaceCoCon
   = IfaceCoAx IfExtName
   | IfaceReflCo    | IfaceUnsafeCo  | IfaceSymCo
   | IfaceTransCo   | IfaceInstCo
-  | IfaceNthCo Int
+  | IfaceNthCo Int | IfaceLRCo LeftOrRight
 \end{code}
 
 %************************************************************************
@@ -278,6 +278,7 @@ instance Outputable IfaceCoCon where
   ppr IfaceTransCo     = ptext (sLit "Trans")
   ppr IfaceInstCo      = ptext (sLit "Inst")
   ppr (IfaceNthCo d)   = ptext (sLit "Nth:") <> int d
+  ppr (IfaceLRCo lr)   = ppr lr
 
 instance Outputable IfaceTyLit where
   ppr = ppr_tylit
@@ -376,6 +377,8 @@ coToIfaceType (TransCo co1 co2)     = IfaceCoConApp IfaceTransCo
                                                     , coToIfaceType co2 ]
 coToIfaceType (NthCo d co)          = IfaceCoConApp (IfaceNthCo d)
                                                     [ coToIfaceType co ]
+coToIfaceType (LRCo lr co)          = IfaceCoConApp (IfaceLRCo lr)
+                                                    [ coToIfaceType co ]
 coToIfaceType (InstCo co ty)        = IfaceCoConApp IfaceInstCo 
                                                     [ coToIfaceType co
                                                     , toIfaceType ty ]
index 80c2029..eb9e5dd 100644 (file)
@@ -962,6 +962,7 @@ tcIfaceCoApp IfaceSymCo       [t]     = SymCo        <$> tcIfaceCo t
 tcIfaceCoApp IfaceTransCo     [t1,t2] = TransCo      <$> tcIfaceCo t1 <*> tcIfaceCo t2
 tcIfaceCoApp IfaceInstCo      [t1,t2] = InstCo       <$> tcIfaceCo t1 <*> tcIfaceType t2
 tcIfaceCoApp (IfaceNthCo d)   [t]     = NthCo d      <$> tcIfaceCo t
+tcIfaceCoApp (IfaceLRCo lr)   [t]     = LRCo lr      <$> tcIfaceCo t
 tcIfaceCoApp cc ts = pprPanic "toIfaceCoApp" (ppr cc <+> ppr ts)
 
 tcIfaceCoVar :: FastString -> IfL CoVar
index e755d69..dbb9de1 100644 (file)
@@ -809,19 +809,11 @@ canEqAppTy :: CtLoc -> CtEvidence
            -> TcS StopOrContinue
 canEqAppTy loc ev s1 t1 s2 t2
   = ASSERT( not (isKind t1) && not (isKind t2) )
-    if isGiven ev then 
-        do { traceTcS "canEq (app case)" $
-                text "Ommitting decomposition of given equality between: " 
-                    <+> ppr (AppTy s1 t1) <+> text "and" <+> ppr (AppTy s2 t2)
-                   -- We cannot decompose given applications
-                   -- because we no longer have 'left' and 'right'
-           ; return Stop }
-    else 
     do { let xevcomp [x,y] = EvCoercion (mkTcAppCo (evTermCoercion x) (evTermCoercion y))
              xevcomp _ = error "canEqAppTy: can't happen" -- Can't happen
-             xev = XEvTerm { ev_comp = xevcomp
-                           , ev_decomp = error "canEqAppTy: can't happen" }
-       ; ctevs <- xCtFlavor ev [mkTcEqPred s1 s2, mkTcEqPred t1 t2] xev 
+             xevdecomp x = let xco = evTermCoercion x 
+                           in [EvCoercion (mkTcLRCo CLeft xco), EvCoercion (mkTcLRCo CRight xco)]
+       ; ctevs <- xCtFlavor ev [mkTcEqPred s1 s2, mkTcEqPred t1 t2] (XEvTerm xevcomp xevdecomp)
        ; canEvVarsCreated loc ctevs }
 
 canEqFailure :: CtLoc -> CtEvidence -> TcS StopOrContinue
index 321809f..c88b350 100644 (file)
@@ -20,10 +20,10 @@ module TcEvidence (
   EvLit(..), evTermCoercion,
 
   -- TcCoercion
-  TcCoercion(..), 
+  TcCoercion(..), LeftOrRight(..), pickLR,
   mkTcReflCo, mkTcTyConAppCo, mkTcAppCo, mkTcAppCos, mkTcFunCo,
   mkTcAxInstCo, mkTcForAllCo, mkTcForAllCos, 
-  mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcInstCos,
+  mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcInstCos,
   tcCoercionKind, coVarsOfTcCo, isEqVar, mkTcCoVarCo, 
   isTcReflCo, isTcReflCo_maybe, getTcCoVar_maybe,
   liftTcCoSubstWith
@@ -32,7 +32,7 @@ module TcEvidence (
 #include "HsVersions.h"
 
 import Var
-
+import Coercion( LeftOrRight(..), pickLR )
 import PprCore ()   -- Instance OutputableBndr TyVar
 import TypeRep  -- Knows type representation
 import TcType
@@ -102,6 +102,7 @@ data TcCoercion
   | TcSymCo TcCoercion
   | TcTransCo TcCoercion TcCoercion
   | TcNthCo Int TcCoercion
+  | TcLRCo LeftOrRight TcCoercion
   | TcCastCo TcCoercion TcCoercion     -- co1 |> co2
   | TcLetCo TcEvBinds TcCoercion
   deriving (Data.Data, Data.Typeable)
@@ -167,6 +168,10 @@ mkTcNthCo :: Int -> TcCoercion -> TcCoercion
 mkTcNthCo n (TcRefl ty) = TcRefl (tyConAppArgN n ty)
 mkTcNthCo n co          = TcNthCo n co
 
+mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion
+mkTcLRCo lr (TcRefl ty) = TcRefl (pickLR lr (tcSplitAppTy ty))
+mkTcLRCo lr co          = TcLRCo lr co
+
 mkTcAppCos :: TcCoercion -> [TcCoercion] -> TcCoercion
 mkTcAppCos co1 tys = foldl mkTcAppCo co1 tys
 
@@ -211,6 +216,7 @@ tcCoercionKind co = go co
     go (TcSymCo co)           = swap (go co)
     go (TcTransCo co1 co2)    = Pair (pFst (go co1)) (pSnd (go co2))
     go (TcNthCo d co)         = tyConAppArgN d <$> go co
+    go (TcLRCo lr co)         = (pickLR lr . tcSplitAppTy) <$> go co
 
     -- c.f. Coercion.coercionKind
     go_inst (TcInstCo co ty) tys = go_inst co (ty:tys)
@@ -239,6 +245,7 @@ coVarsOfTcCo tc_co
     go (TcSymCo co)              = go co
     go (TcTransCo co1 co2)       = go co1 `unionVarSet` go co2
     go (TcNthCo _ co)            = go co
+    go (TcLRCo  _ co)            = go co
     go (TcLetCo (EvBinds bs) co) = foldrBag (unionVarSet . go_bind) (go co) bs
                                    `minusVarSet` get_bndrs bs
     go (TcLetCo {}) = emptyVarSet    -- Harumph. This does legitimately happen in the call
@@ -306,6 +313,7 @@ ppr_co p (TcTransCo co1 co2) = maybeParen p FunPrec $
                                <+> ppr_co FunPrec co2
 ppr_co p (TcSymCo co)         = pprPrefixApp p (ptext (sLit "Sym")) [pprParendTcCo co]
 ppr_co p (TcNthCo n co)       = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendTcCo co]
+ppr_co p (TcLRCo lr co)       = pprPrefixApp p (ppr lr) [pprParendTcCo co]
 
 ppr_fun_co :: Prec -> TcCoercion -> SDoc
 ppr_fun_co p co = pprArrowChain p (split co)
index d56f7af..ef53f4e 100644 (file)
@@ -1357,6 +1357,7 @@ zonkTcLCoToLCo env co
                                    ; return (TcCastCo co1' co2') }
     go (TcSymCo co)           = do { co' <- go co; return (mkTcSymCo co')  }
     go (TcNthCo n co)         = do { co' <- go co; return (mkTcNthCo n co')  }
+    go (TcLRCo lr co)         = do { co' <- go co; return (mkTcLRCo lr co')  }
     go (TcTransCo co1 co2)    = do { co1' <- go co1; co2' <- go co2
                                    ; return (mkTcTransCo co1' co2')  }
     go (TcForAllCo tv co)     = ASSERT( isImmutableTyVar tv )
index 758573d..e129bac 100644 (file)
@@ -662,6 +662,7 @@ tidyCo env@(_, subst) co
     go (SymCo co)            = SymCo $! go co
     go (TransCo co1 co2)     = (TransCo $! go co1) $! go co2
     go (NthCo d co)          = NthCo d $! go co
+    go (LRCo lr co)          = LRCo lr $! go co
     go (InstCo co ty)        = (InstCo $! go co) $! tidyType env ty
 
 tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
index 42e54ba..30e71fd 100644 (file)
@@ -17,6 +17,7 @@
 module Coercion (
         -- * Main data type
         Coercion(..), Var, CoVar,
+        LeftOrRight(..), pickLR,
 
         -- ** Functions over coercions
         coVarKind,
@@ -31,7 +32,7 @@ module Coercion (
         mkReflCo, mkCoVarCo, 
         mkAxInstCo, mkAxInstRHS,
         mkPiCo, mkPiCos, mkCoCast,
-        mkSymCo, mkTransCo, mkNthCo,
+        mkSymCo, mkTransCo, mkNthCo, mkLRCo,
        mkInstCo, mkAppCo, mkTyConAppCo, mkFunCo,
         mkForAllCo, mkUnsafeCo,
         mkNewTypeCo, 
@@ -148,9 +149,17 @@ data Coercion
   | TransCo Coercion Coercion
 
   -- These are destructors
-  | NthCo Int Coercion          -- Zero-indexed
+  | NthCo  Int         Coercion     -- Zero-indexed; decomposes (T t0 ... tn)
+  | LRCo   LeftOrRight Coercion     -- Decomposes (t_left t_right)
   | InstCo Coercion Type
   deriving (Data.Data, Data.Typeable)
+
+data LeftOrRight = CLeft | CRight 
+                 deriving( Eq, Data.Data, Data.Typeable )
+
+pickLR :: LeftOrRight -> (a,a) -> a
+pickLR CLeft  (l,_) = l
+pickLR CRight (_,r) = r
 \end{code}
 
 
@@ -337,6 +346,7 @@ tyCoVarsOfCo (UnsafeCo ty1 ty2)  = tyVarsOfType ty1 `unionVarSet` tyVarsOfType t
 tyCoVarsOfCo (SymCo co)          = tyCoVarsOfCo co
 tyCoVarsOfCo (TransCo co1 co2)   = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2
 tyCoVarsOfCo (NthCo _ co)        = tyCoVarsOfCo co
+tyCoVarsOfCo (LRCo _ co)         = tyCoVarsOfCo co
 tyCoVarsOfCo (InstCo co ty)      = tyCoVarsOfCo co `unionVarSet` tyVarsOfType ty
 
 tyCoVarsOfCos :: [Coercion] -> VarSet
@@ -354,6 +364,7 @@ coVarsOfCo (UnsafeCo _ _)      = emptyVarSet
 coVarsOfCo (SymCo co)          = coVarsOfCo co
 coVarsOfCo (TransCo co1 co2)   = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
 coVarsOfCo (NthCo _ co)        = coVarsOfCo co
+coVarsOfCo (LRCo _ co)         = coVarsOfCo co
 coVarsOfCo (InstCo co _)       = coVarsOfCo co
 
 coVarsOfCos :: [Coercion] -> VarSet
@@ -370,6 +381,7 @@ coercionSize (UnsafeCo ty1 ty2)  = typeSize ty1 + typeSize ty2
 coercionSize (SymCo co)          = 1 + coercionSize co
 coercionSize (TransCo co1 co2)   = 1 + coercionSize co1 + coercionSize co2
 coercionSize (NthCo _ co)        = 1 + coercionSize co
+coercionSize (LRCo  _ co)        = 1 + coercionSize co
 coercionSize (InstCo co ty)      = 1 + coercionSize co + typeSize ty
 \end{code}
 
@@ -416,8 +428,12 @@ ppr_co p (InstCo co ty) = maybeParen p TyConPrec $
 ppr_co p (UnsafeCo ty1 ty2) = pprPrefixApp p (ptext (sLit "UnsafeCo")) 
                                            [pprParendType ty1, pprParendType ty2]
 ppr_co p (SymCo co)         = pprPrefixApp p (ptext (sLit "Sym")) [pprParendCo co]
-ppr_co p (NthCo n co)       = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendCo co]
+ppr_co p (NthCo n co)       = pprPrefixApp p (ptext (sLit "Nth:") <> int n) [pprParendCo co]
+ppr_co p (LRCo sel co)      = pprPrefixApp p (ppr sel) [pprParendCo co]
 
+instance Outputable LeftOrRight where
+  ppr CLeft    = ptext (sLit "Left")
+  ppr CRight   = ptext (sLit "Right")
 
 ppr_fun_co :: Prec -> Coercion -> SDoc
 ppr_fun_co p co = pprArrowChain p (split co)
@@ -625,6 +641,10 @@ mkNthCo n co        = ASSERT( ok_tc_app _ty1 n && ok_tc_app _ty2 n )
                     where
                       Pair _ty1 _ty2 = coercionKind co
 
+mkLRCo :: LeftOrRight -> Coercion -> Coercion
+mkLRCo lr (Refl ty) = Refl (pickLR lr (splitAppTy ty))
+mkLRCo lr co        = LRCo lr co
+
 ok_tc_app :: Type -> Int -> Bool
 ok_tc_app ty n = case splitTyConApp_maybe ty of
                    Just (_, tys) -> tys `lengthExceeds` n
@@ -759,6 +779,8 @@ coreEqCoercion2 env (TransCo co11 co12) (TransCo co21 co22)
 
 coreEqCoercion2 env (NthCo d1 co1) (NthCo d2 co2)
   = d1 == d2 && coreEqCoercion2 env co1 co2
+coreEqCoercion2 env (LRCo d1 co1) (LRCo d2 co2)
+  = d1 == d2 && coreEqCoercion2 env co1 co2
 
 coreEqCoercion2 env (InstCo co1 ty1) (InstCo co2 ty2)
   = coreEqCoercion2 env co1 co2 && eqTypeX env ty1 ty2
@@ -900,6 +922,7 @@ subst_co subst co
     go (SymCo co)            = mkSymCo (go co)
     go (TransCo co1 co2)     = mkTransCo (go co1) (go co2)
     go (NthCo d co)          = mkNthCo d (go co)
+    go (LRCo lr co)          = mkLRCo lr (go co)
     go (InstCo co ty)        = mkInstCo (go co) $! go_ty ty
 
 substCoVar :: CvSubst -> CoVar -> Coercion
@@ -1073,6 +1096,7 @@ seqCo (UnsafeCo ty1 ty2)    = seqType ty1 `seq` seqType ty2
 seqCo (SymCo co)            = seqCo co
 seqCo (TransCo co1 co2)     = seqCo co1 `seq` seqCo co2
 seqCo (NthCo _ co)          = seqCo co
+seqCo (LRCo _ co)           = seqCo co
 seqCo (InstCo co ty)        = seqCo co `seq` seqType ty
 
 seqCos :: [Coercion] -> ()
@@ -1114,6 +1138,7 @@ coercionKind co = go co
     go (SymCo co)           = swap $ go co
     go (TransCo co1 co2)    = Pair (pFst $ go co1) (pSnd $ go co2)
     go (NthCo d co)         = tyConAppArgN d <$> go co
+    go (LRCo lr co)         = (pickLR lr . splitAppTy) <$> go co
     go (InstCo aco ty)      = go_app aco [ty]
 
     go_app :: Coercion -> [Type] -> Pair Type
index 7d707c3..c699163 100644 (file)
@@ -145,7 +145,7 @@ opt_co' env sym (TransCo co1 co2)
 
 opt_co' env sym (NthCo n co)
   | TyConAppCo tc cos <- co'
-  , isDecomposableTyCon tc             -- Not synonym families
+  , isDecomposableTyCon tc   -- Not synonym families
   = ASSERT( n < length cos )
     cos !! n
   | otherwise
@@ -153,6 +153,14 @@ opt_co' env sym (NthCo n co)
   where
     co' = opt_co env sym co
 
+opt_co' env sym (LRCo lr co)
+  | Just pr_co <- splitAppCo_maybe co'
+  = pickLR lr pr_co
+  | otherwise
+  = LRCo lr co'
+  where
+    co' = opt_co env sym co
+
 opt_co' env sym (InstCo co ty)
     -- See if the first arg is already a forall
     -- ...then we can just extend the current substitution
@@ -165,7 +173,6 @@ opt_co' env sym (InstCo co ty)
   = substCoWithTy (getCvInScope env) tv ty' co'_body   
 
   | otherwise = InstCo co' ty'
-
   where
     co' = opt_co env sym co
     ty' = substTy env ty
@@ -208,18 +215,19 @@ opt_trans2 _ co1 co2
 -- Optimize coercions with a top-level use of transitivity.
 opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
 
--- push transitivity down through matching top-level constructors.
-opt_trans_rule is in_co1@(TyConAppCo tc1 cos1) in_co2@(TyConAppCo tc2 cos2)
-  | tc1 == tc2 = fireTransRule "PushTyConApp" in_co1 in_co2 $
-                 TyConAppCo tc1 (opt_transList is cos1 cos2)
-
--- push transitivity through matching destructors
+-- Push transitivity through matching destructors
 opt_trans_rule is in_co1@(NthCo d1 co1) in_co2@(NthCo d2 co2)
   | d1 == d2
   , co1 `compatible_co` co2
   = fireTransRule "PushNth" in_co1 in_co2 $
     mkNthCo d1 (opt_trans is co1 co2)
 
+opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2)
+  | d1 == d2
+  , co1 `compatible_co` co2
+  = fireTransRule "PushLR" in_co1 in_co2 $
+    mkLRCo d1 (opt_trans is co1 co2)
+
 -- Push transitivity inside instantiation
 opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
   | ty1 `eqType` ty2
@@ -227,11 +235,17 @@ opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
   = fireTransRule "TrPushInst" in_co1 in_co2 $
     mkInstCo (opt_trans is co1 co2) ty1
  
--- Push transitivity inside apply
+-- Push transitivity down through matching top-level constructors.
+opt_trans_rule is in_co1@(TyConAppCo tc1 cos1) in_co2@(TyConAppCo tc2 cos2)
+  | tc1 == tc2 
+  = fireTransRule "PushTyConApp" in_co1 in_co2 $
+    TyConAppCo tc1 (opt_transList is cos1 cos2)
+
 opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
   = fireTransRule "TrPushApp" in_co1 in_co2 $
     mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
 
+-- Eta rules
 opt_trans_rule is co1@(TyConAppCo tc cos1) co2
   | Just cos2 <- etaTyConAppCo_maybe tc co2
   = ASSERT( length cos1 == length cos2 )
@@ -244,6 +258,16 @@ opt_trans_rule is co1 co2@(TyConAppCo tc cos2)
     fireTransRule "EtaCompR" co1 co2 $
     TyConAppCo tc (opt_transList is cos1 cos2)
 
+opt_trans_rule is co1@(AppCo co1a co1b) co2
+  | Just (co2a,co2b) <- etaAppCo_maybe co2
+  = fireTransRule "EtaAppL" co1 co2 $
+    mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
+
+opt_trans_rule is co1 co2@(AppCo co2a co2b)
+  | Just (co1a,co1b) <- etaAppCo_maybe co1
+  = fireTransRule "EtaAppR" co1 co2 $
+    mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
+
 -- Push transitivity inside forall
 opt_trans_rule is co1 co2
   | Just (tv1,r1) <- splitForAllCo_maybe co1
@@ -359,6 +383,20 @@ etaForAllCo_maybe co
   | otherwise
   = Nothing
 
+etaAppCo_maybe :: Coercion -> Maybe (Coercion,Coercion)
+-- If possible, split a coercion
+--   g :: t1a t1b ~ t2a t2b
+-- into a pair of coercions (left g, right g)
+etaAppCo_maybe co
+  | Just (co1,co2) <- splitAppCo_maybe co
+  = Just (co1,co2)
+  | Pair ty1 ty2 <- coercionKind co
+  , Just {} <- splitAppTy_maybe ty1
+  , Just {} <- splitAppTy_maybe ty2
+  = Just (LRCo CLeft co, LRCo CRight co)
+  | otherwise
+  = Nothing
+
 etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
 -- If possible, split a coercion 
 --       g :: T s1 .. sn ~ T t1 .. tn