Define MCoercion type

An attempt on #14975:
During compilation, reflexive casts is discarded for computation.
Currently in some places we use Maybe coercion as inputs. So if a cast
is reflexive it is denoted as Nothing, otherwise Just coercion.

This patch defines the type

data MCoercion = MRefl | MCo Coercion

which is isomorphic to Maybe Coercion but useful in a number of places,
and super-helpful documentation.

Test Plan: validate

Reviewers: bgamari, goldfire, simonpj

Reviewed By: goldfire

Subscribers: mpickering, rwbarton, thomie, carter

GHC Trac Issues: #14975

Differential Revision: https://phabricator.haskell.org/D4699

2 files changed, 15 insertions, 14 deletions

diff --git a/compiler/coreSyn/CoreOpt.hs b/compiler/coreSyn/CoreOpt.hs
index 2027928e3f..73bb427614 100644
--- a/compiler/coreSyn/CoreOpt.hs
+++ b/compiler/coreSyn/CoreOpt.hs
@@ -754,8 +754,8 @@ exprIsConApp_maybe (in_scope, id_unf) expr
        | Just (args', m_co1') <- pushCoArgs (subst_co subst co1) args
             -- See Note [Push coercions in exprIsConApp_maybe]
        = case m_co1' of
-           Just co1' -> go subst expr (CC args' (co1' `mkTransCo` co2))
-           Nothing   -> go subst expr (CC args' co2)
+           MCo co1' -> go subst expr (CC args' (co1' `mkTransCo` co2))
+           MRefl    -> go subst expr (CC args' co2)
     go subst (App fun arg) (CC args co)
        = go subst fun (CC (subst_arg subst arg : args) co)
     go subst (Lam var body) (CC (arg:args) co)
@@ -949,15 +949,15 @@ Here we implement the "push rules" from FC papers:
   by pushing the coercion into the arguments
 -}
 
-pushCoArgs :: CoercionR -> [CoreArg] -> Maybe ([CoreArg], Maybe Coercion)
-pushCoArgs co []         = return ([], Just co)
+pushCoArgs :: CoercionR -> [CoreArg] -> Maybe ([CoreArg], MCoercion)
+pushCoArgs co []         = return ([], MCo co)
 pushCoArgs co (arg:args) = do { (arg',  m_co1) <- pushCoArg  co  arg
                               ; case m_co1 of
-                                  Just co1 -> do { (args', m_co2) <- pushCoArgs co1 args
+                                  MCo co1 -> do { (args', m_co2) <- pushCoArgs co1 args
                                                  ; return (arg':args', m_co2) }
-                                  Nothing  -> return (arg':args, Nothing) }
+                                  MRefl  -> return (arg':args, MRefl) }
 
-pushCoArg :: CoercionR -> CoreArg -> Maybe (CoreArg, Maybe Coercion)
+pushCoArg :: CoercionR -> CoreArg -> Maybe (CoreArg, MCoercion)
 -- We have (fun |> co) arg, and we want to transform it to
 --         (fun arg) |> co
 -- This may fail, e.g. if (fun :: N) where N is a newtype
@@ -969,7 +969,7 @@ pushCoArg co (Type ty) = do { (ty', m_co') <- pushCoTyArg co ty
 pushCoArg co val_arg   = do { (arg_co, m_co') <- pushCoValArg co
                             ; return (val_arg `mkCast` arg_co, m_co') }
 
-pushCoTyArg :: CoercionR -> Type -> Maybe (Type, Maybe CoercionR)
+pushCoTyArg :: CoercionR -> Type -> Maybe (Type, MCoercionR)
 -- We have (fun |> co) @ty
 -- Push the coercion through to return
 --         (fun @ty') |> co'
@@ -983,11 +983,11 @@ pushCoTyArg co ty
   -- -- = Just (ty, Nothing)
 
   | isReflCo co
-  = Just (ty, Nothing)
+  = Just (ty, MRefl)
 
   | isForAllTy tyL
   = ASSERT2( isForAllTy tyR, ppr co $$ ppr ty )
-    Just (ty `mkCastTy` mkSymCo co1, Just co2)
+    Just (ty `mkCastTy` mkSymCo co1, MCo co2)
 
   | otherwise
   = Nothing
@@ -1007,7 +1007,7 @@ pushCoTyArg co ty
         -- co2 :: ty1[ (ty|>co1)/a1 ] ~ ty2[ ty/a2 ]
         -- Arg of mkInstCo is always nominal, hence mkNomReflCo
 
-pushCoValArg :: CoercionR -> Maybe (Coercion, Maybe Coercion)
+pushCoValArg :: CoercionR -> Maybe (Coercion, MCoercion)
 -- We have (fun |> co) arg
 -- Push the coercion through to return
 --         (fun (arg |> co_arg)) |> co_res
@@ -1021,7 +1021,7 @@ pushCoValArg co
   -- -- = Just (mkRepReflCo arg, Nothing)
 
   | isReflCo co
-  = Just (mkRepReflCo arg, Nothing)
+  = Just (mkRepReflCo arg, MRefl)
 
   | isFunTy tyL
   , (co1, co2) <- decomposeFunCo Representational co
@@ -1029,7 +1029,7 @@ pushCoValArg co
               -- then co1 :: tyL1 ~ tyR1
               --      co2 :: tyL2 ~ tyR2
   = ASSERT2( isFunTy tyR, ppr co $$ ppr arg )
-    Just (mkSymCo co1, Just co2)
+    Just (mkSymCo co1, MCo co2)
 
   | otherwise
   = Nothing
diff --git a/compiler/coreSyn/CoreSyn.hs b/compiler/coreSyn/CoreSyn.hs
index 2cb8079feb..729825fd98 100644
--- a/compiler/coreSyn/CoreSyn.hs
+++ b/compiler/coreSyn/CoreSyn.hs
@@ -18,7 +18,7 @@ module CoreSyn (
         InId, InBind, InExpr, InAlt, InArg, InType, InKind,
                InBndr, InVar, InCoercion, InTyVar, InCoVar,
         OutId, OutBind, OutExpr, OutAlt, OutArg, OutType, OutKind,
-               OutBndr, OutVar, OutCoercion, OutTyVar, OutCoVar,
+               OutBndr, OutVar, OutCoercion, OutTyVar, OutCoVar, MOutCoercion,
 
         -- ** 'Expr' construction
         mkLet, mkLets, mkLetNonRec, mkLetRec, mkLams,
@@ -793,6 +793,7 @@ type OutBind     = CoreBind
 type OutExpr     = CoreExpr
 type OutAlt      = CoreAlt
 type OutArg      = CoreArg
+type MOutCoercion = MCoercion
 
 
 {- *********************************************************************