Implement 'left' and 'right' coercions

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.

5 files changed, 42 insertions, 5 deletions

diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs
index dcd366f381..250efdd85d 100644
--- a/compiler/coreSyn/CoreLint.lhs
+++ b/compiler/coreSyn/CoreLint.lhs
@@ -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
diff --git a/compiler/coreSyn/ExternalCore.lhs b/compiler/coreSyn/ExternalCore.lhs
index d2f6691a7c..287f08049e 100644
--- a/compiler/coreSyn/ExternalCore.lhs
+++ b/compiler/coreSyn/ExternalCore.lhs
@@ -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
diff --git a/compiler/coreSyn/MkExternalCore.lhs b/compiler/coreSyn/MkExternalCore.lhs
index 21037088e1..8844818bdc 100644
--- a/compiler/coreSyn/MkExternalCore.lhs
+++ b/compiler/coreSyn/MkExternalCore.lhs
@@ -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 =
diff --git a/compiler/coreSyn/PprExternalCore.lhs b/compiler/coreSyn/PprExternalCore.lhs
index 26e64ee641..2290810fe1 100644
--- a/compiler/coreSyn/PprExternalCore.lhs
+++ b/compiler/coreSyn/PprExternalCore.lhs
@@ -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
diff --git a/compiler/coreSyn/TrieMap.lhs b/compiler/coreSyn/TrieMap.lhs
index 7170f1cede..6bc78a8272 100644
--- a/compiler/coreSyn/TrieMap.lhs
+++ b/compiler/coreSyn/TrieMap.lhs
@@ -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}