Commit 9aac442f authored by Ningning Xie's avatar Ningning Xie Committed by Ben Gamari

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
parent 34464fed
......@@ -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
......
......@@ -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
{- *********************************************************************
......
......@@ -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]
......
......@@ -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,
......
......@@ -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]
~~~~~~~~~~~~~~~~~~~~~
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment