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

5 files changed, 30 insertions, 19 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
 
 
 {- *********************************************************************
diff --git a/compiler/simplCore/Simplify.hs b/compiler/simplCore/Simplify.hs
index 5e514c5ecf..6d1b434b8f 100644
--- a/compiler/simplCore/Simplify.hs
+++ b/compiler/simplCore/Simplify.hs
@@ -1248,11 +1248,11 @@ simplCast env body co0 cont0
                    else addCoerce co1 cont0
         ; {-#SCC "simplCast-simplExprF" #-} simplExprF env body cont1 }
   where
-        -- If the first parameter is Nothing, then simplifying revealed a
+        -- If the first parameter is MRefl, then simplifying revealed a
         -- reflexive coercion. Omit.
-        addCoerceM :: Maybe OutCoercion -> SimplCont -> SimplM SimplCont
-        addCoerceM Nothing   cont = return cont
-        addCoerceM (Just co) cont = addCoerce co cont
+        addCoerceM :: MOutCoercion -> SimplCont -> SimplM SimplCont
+        addCoerceM MRefl   cont = return cont
+        addCoerceM (MCo co) cont = addCoerce co cont
 
         addCoerce :: OutCoercion -> SimplCont -> SimplM SimplCont
         addCoerce co1 (CastIt co2 cont)  -- See Note [Optimising reflexivity]
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index d0c5eeda69..8085e10f2b 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -10,7 +10,7 @@
 --
 module Coercion (
         -- * Main data type
-        Coercion, CoercionN, CoercionR, CoercionP,
+        Coercion, CoercionN, CoercionR, CoercionP, MCoercion(..), MCoercionR,
         UnivCoProvenance, CoercionHole(..), coHoleCoVar, setCoHoleCoVar,
         LeftOrRight(..),
         Var, CoVar, TyCoVar,
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 27f28ae429..bd10ac8cf3 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -34,6 +34,7 @@ module TyCoRep (
         UnivCoProvenance(..),
         CoercionHole(..), coHoleCoVar, setCoHoleCoVar,
         CoercionN, CoercionR, CoercionP, KindCoercion,
+        MCoercion(..), MCoercionR,
 
         -- * Functions over types
         mkTyConTy, mkTyVarTy, mkTyVarTys,
@@ -942,6 +943,15 @@ type CoercionR = Coercion       -- always representational
 type CoercionP = Coercion       -- always phantom
 type KindCoercion = CoercionN   -- always nominal
 
+-- | A semantically more meaningful type to represent what may or may not be a
+-- useful 'Coercion'.
+data MCoercion
+  = MRefl
+    -- A trivial Reflexivity coercion
+  | MCo Coercion
+    -- Other coercions
+type MCoercionR = MCoercion
+
 {-
 Note [Refl invariant]
 ~~~~~~~~~~~~~~~~~~~~~