module CoreOpt (
simpleOptPgm, simpleOptExpr, simpleOptExprWith,
joinPointBinding_maybe, joinPointBindings_maybe,
exprIsConApp_maybe, exprIsLiteral_maybe, exprIsLambda_maybe,
pushCoArg, pushCoValArg, pushCoTyArg, collectBindersPushingCo
) where
#include "HsVersions.h"
import GhcPrelude
import CoreArity( etaExpandToJoinPoint )
import CoreSyn
import CoreSubst
import CoreUtils
import CoreFVs
import PprCore ( pprCoreBindings, pprRules )
import OccurAnal( occurAnalyseExpr, occurAnalysePgm )
import Literal ( Literal(MachStr) )
import Id
import Var ( varType )
import VarSet
import VarEnv
import DataCon
import Demand( etaExpandStrictSig )
import OptCoercion ( optCoercion )
import Type hiding ( substTy, extendTvSubst, extendCvSubst, extendTvSubstList
, isInScope, substTyVarBndr, cloneTyVarBndr )
import Coercion hiding ( substCo, substCoVarBndr )
import TyCon ( tyConArity )
import TysWiredIn
import PrelNames
import BasicTypes
import Module ( Module )
import ErrUtils
import DynFlags
import Outputable
import Pair
import Util
import Maybes ( orElse )
import FastString
import Data.List
import qualified Data.ByteString as BS
simpleOptExpr :: DynFlags -> CoreExpr -> CoreExpr
simpleOptExpr dflags expr
=
simpleOptExprWith dflags init_subst expr
where
init_subst = mkEmptySubst (mkInScopeSet (exprFreeVars expr))
simpleOptExprWith :: DynFlags -> Subst -> InExpr -> OutExpr
simpleOptExprWith dflags subst expr
= simple_opt_expr init_env (occurAnalyseExpr expr)
where
init_env = SOE { soe_dflags = dflags
, soe_inl = emptyVarEnv
, soe_subst = subst }
simpleOptPgm :: DynFlags -> Module
-> CoreProgram -> [CoreRule]
-> IO (CoreProgram, [CoreRule])
simpleOptPgm dflags this_mod binds rules
= do { dumpIfSet_dyn dflags Opt_D_dump_occur_anal "Occurrence analysis"
(pprCoreBindings occ_anald_binds $$ pprRules rules );
; return (reverse binds', rules') }
where
occ_anald_binds = occurAnalysePgm this_mod
(\_ -> True)
(\_ -> False)
rules binds
(final_env, binds') = foldl do_one (emptyEnv dflags, []) occ_anald_binds
final_subst = soe_subst final_env
rules' = substRulesForImportedIds final_subst rules
do_one (env, binds') bind
= case simple_opt_bind env bind of
(env', Nothing) -> (env', binds')
(env', Just bind') -> (env', bind':binds')
type SimpleClo = (SimpleOptEnv, InExpr)
data SimpleOptEnv
= SOE { soe_dflags :: DynFlags
, soe_inl :: IdEnv SimpleClo
, soe_subst :: Subst
}
instance Outputable SimpleOptEnv where
ppr (SOE { soe_inl = inl, soe_subst = subst })
= text "SOE {" <+> vcat [ text "soe_inl =" <+> ppr inl
, text "soe_subst =" <+> ppr subst ]
<+> text "}"
emptyEnv :: DynFlags -> SimpleOptEnv
emptyEnv dflags
= SOE { soe_dflags = dflags
, soe_inl = emptyVarEnv
, soe_subst = emptySubst }
soeZapSubst :: SimpleOptEnv -> SimpleOptEnv
soeZapSubst env@(SOE { soe_subst = subst })
= env { soe_inl = emptyVarEnv, soe_subst = zapSubstEnv subst }
soeSetInScope :: SimpleOptEnv -> SimpleOptEnv -> SimpleOptEnv
soeSetInScope (SOE { soe_subst = subst1 })
env2@(SOE { soe_subst = subst2 })
= env2 { soe_subst = setInScope subst2 (substInScope subst1) }
simple_opt_clo :: SimpleOptEnv -> SimpleClo -> OutExpr
simple_opt_clo env (e_env, e)
= simple_opt_expr (soeSetInScope env e_env) e
simple_opt_expr :: SimpleOptEnv -> InExpr -> OutExpr
simple_opt_expr env expr
= go expr
where
subst = soe_subst env
in_scope = substInScope subst
in_scope_env = (in_scope, simpleUnfoldingFun)
go (Var v)
| Just clo <- lookupVarEnv (soe_inl env) v
= simple_opt_clo env clo
| otherwise
= lookupIdSubst (text "simpleOptExpr") (soe_subst env) v
go (App e1 e2) = simple_app env e1 [(env,e2)]
go (Type ty) = Type (substTy subst ty)
go (Coercion co) = Coercion (optCoercion (soe_dflags env) (getTCvSubst subst) co)
go (Lit lit) = Lit lit
go (Tick tickish e) = mkTick (substTickish subst tickish) (go e)
go (Cast e co) | isReflCo co' = go e
| otherwise = Cast (go e) co'
where
co' = optCoercion (soe_dflags env) (getTCvSubst subst) co
go (Let bind body) = case simple_opt_bind env bind of
(env', Nothing) -> simple_opt_expr env' body
(env', Just bind) -> Let bind (simple_opt_expr env' body)
go lam@(Lam {}) = go_lam env [] lam
go (Case e b ty as)
| isDeadBinder b
, Just (con, _tys, es) <- exprIsConApp_maybe in_scope_env e'
, Just (altcon, bs, rhs) <- findAlt (DataAlt con) as
= case altcon of
DEFAULT -> go rhs
_ -> foldr wrapLet (simple_opt_expr env' rhs) mb_prs
where
(env', mb_prs) = mapAccumL simple_out_bind env $
zipEqual "simpleOptExpr" bs es
| isDeadBinder b
, [(DEFAULT, _, rhs)] <- as
, isCoercionType (varType b)
, (Var fun, _args) <- collectArgs e
, fun `hasKey` coercibleSCSelIdKey
= go rhs
| otherwise
= Case e' b' (substTy subst ty)
(map (go_alt env') as)
where
e' = go e
(env', b') = subst_opt_bndr env b
go_alt env (con, bndrs, rhs)
= (con, bndrs', simple_opt_expr env' rhs)
where
(env', bndrs') = subst_opt_bndrs env bndrs
go_lam env bs' (Lam b e)
= go_lam env' (b':bs') e
where
(env', b') = subst_opt_bndr env b
go_lam env bs' e
| Just etad_e <- tryEtaReduce bs e' = etad_e
| otherwise = mkLams bs e'
where
bs = reverse bs'
e' = simple_opt_expr env e
simple_app :: SimpleOptEnv -> InExpr -> [SimpleClo] -> CoreExpr
simple_app env (Var v) as
| Just (env', e) <- lookupVarEnv (soe_inl env) v
= simple_app (soeSetInScope env env') e as
| let unf = idUnfolding v
, isCompulsoryUnfolding (idUnfolding v)
, isAlwaysActive (idInlineActivation v)
= simple_app (soeZapSubst env) (unfoldingTemplate unf) as
| otherwise
, let out_fn = lookupIdSubst (text "simple_app") (soe_subst env) v
= finish_app env out_fn as
simple_app env (App e1 e2) as
= simple_app env e1 ((env, e2) : as)
simple_app env (Lam b e) (a:as)
= wrapLet mb_pr (simple_app env' e as)
where
(env', mb_pr) = simple_bind_pair env b Nothing a
simple_app env (Tick t e) as
| t `tickishScopesLike` SoftScope
= mkTick t $ simple_app env e as
simple_app env e as
= finish_app env (simple_opt_expr env e) as
finish_app :: SimpleOptEnv -> OutExpr -> [SimpleClo] -> OutExpr
finish_app _ fun []
= fun
finish_app env fun (arg:args)
= finish_app env (App fun (simple_opt_clo env arg)) args
simple_opt_bind :: SimpleOptEnv -> InBind
-> (SimpleOptEnv, Maybe OutBind)
simple_opt_bind env (NonRec b r)
= (env', case mb_pr of
Nothing -> Nothing
Just (b,r) -> Just (NonRec b r))
where
(b', r') = joinPointBinding_maybe b r `orElse` (b, r)
(env', mb_pr) = simple_bind_pair env b' Nothing (env,r')
simple_opt_bind env (Rec prs)
= (env'', res_bind)
where
res_bind = Just (Rec (reverse rev_prs'))
prs' = joinPointBindings_maybe prs `orElse` prs
(env', bndrs') = subst_opt_bndrs env (map fst prs')
(env'', rev_prs') = foldl do_pr (env', []) (prs' `zip` bndrs')
do_pr (env, prs) ((b,r), b')
= (env', case mb_pr of
Just pr -> pr : prs
Nothing -> prs)
where
(env', mb_pr) = simple_bind_pair env b (Just b') (env,r)
simple_bind_pair :: SimpleOptEnv
-> InVar -> Maybe OutVar
-> SimpleClo
-> (SimpleOptEnv, Maybe (OutVar, OutExpr))
simple_bind_pair env@(SOE { soe_inl = inl_env, soe_subst = subst })
in_bndr mb_out_bndr clo@(rhs_env, in_rhs)
| Type ty <- in_rhs
, let out_ty = substTy (soe_subst rhs_env) ty
= ASSERT( isTyVar in_bndr )
(env { soe_subst = extendTvSubst subst in_bndr out_ty }, Nothing)
| Coercion co <- in_rhs
, let out_co = optCoercion (soe_dflags env) (getTCvSubst (soe_subst rhs_env)) co
= ASSERT( isCoVar in_bndr )
(env { soe_subst = extendCvSubst subst in_bndr out_co }, Nothing)
| pre_inline_unconditionally
= (env { soe_inl = extendVarEnv inl_env in_bndr clo }, Nothing)
| otherwise
= simple_out_bind_pair env in_bndr mb_out_bndr out_rhs
occ active stable_unf
where
stable_unf = isStableUnfolding (idUnfolding in_bndr)
active = isAlwaysActive (idInlineActivation in_bndr)
occ = idOccInfo in_bndr
out_rhs | Just join_arity <- isJoinId_maybe in_bndr
= simple_join_rhs join_arity
| otherwise
= simple_opt_clo env clo
simple_join_rhs join_arity
= mkLams join_bndrs' (simple_opt_expr env_body join_body)
where
env0 = soeSetInScope env rhs_env
(join_bndrs, join_body) = collectNBinders join_arity in_rhs
(env_body, join_bndrs') = subst_opt_bndrs env0 join_bndrs
pre_inline_unconditionally :: Bool
pre_inline_unconditionally
| isCoVar in_bndr = False
| isExportedId in_bndr = False
| stable_unf = False
| not active = False
| not (safe_to_inline occ) = False
| otherwise = True
safe_to_inline :: OccInfo -> Bool
safe_to_inline (IAmALoopBreaker {}) = False
safe_to_inline IAmDead = True
safe_to_inline occ@(OneOcc {}) = not (occ_in_lam occ)
&& occ_one_br occ
safe_to_inline (ManyOccs {}) = False
simple_out_bind :: SimpleOptEnv -> (InVar, OutExpr)
-> (SimpleOptEnv, Maybe (OutVar, OutExpr))
simple_out_bind env@(SOE { soe_subst = subst }) (in_bndr, out_rhs)
| Type out_ty <- out_rhs
= ASSERT( isTyVar in_bndr )
(env { soe_subst = extendTvSubst subst in_bndr out_ty }, Nothing)
| Coercion out_co <- out_rhs
= ASSERT( isCoVar in_bndr )
(env { soe_subst = extendCvSubst subst in_bndr out_co }, Nothing)
| otherwise
= simple_out_bind_pair env in_bndr Nothing out_rhs
(idOccInfo in_bndr) True False
simple_out_bind_pair :: SimpleOptEnv
-> InId -> Maybe OutId -> OutExpr
-> OccInfo -> Bool -> Bool
-> (SimpleOptEnv, Maybe (OutVar, OutExpr))
simple_out_bind_pair env in_bndr mb_out_bndr out_rhs
occ_info active stable_unf
| post_inline_unconditionally
= ( env' { soe_subst = extendIdSubst (soe_subst env) in_bndr out_rhs }
, Nothing)
| otherwise
= ( env', Just (out_bndr, out_rhs) )
where
(env', bndr1) = case mb_out_bndr of
Just out_bndr -> (env, out_bndr)
Nothing -> subst_opt_bndr env in_bndr
out_bndr = add_info env' in_bndr bndr1
post_inline_unconditionally :: Bool
post_inline_unconditionally
| not active = False
| isWeakLoopBreaker occ_info = False
| stable_unf = False
| isExportedId in_bndr = False
| exprIsTrivial out_rhs = True
| coercible_hack = True
| otherwise = False
coercible_hack | (Var fun, args) <- collectArgs out_rhs
, Just dc <- isDataConWorkId_maybe fun
, dc `hasKey` heqDataConKey || dc `hasKey` coercibleDataConKey
= all exprIsTrivial args
| otherwise
= False
subst_opt_bndrs :: SimpleOptEnv -> [InVar] -> (SimpleOptEnv, [OutVar])
subst_opt_bndrs env bndrs = mapAccumL subst_opt_bndr env bndrs
subst_opt_bndr :: SimpleOptEnv -> InVar -> (SimpleOptEnv, OutVar)
subst_opt_bndr env bndr
| isTyVar bndr = (env { soe_subst = subst_tv }, tv')
| isCoVar bndr = (env { soe_subst = subst_cv }, cv')
| otherwise = subst_opt_id_bndr env bndr
where
subst = soe_subst env
(subst_tv, tv') = substTyVarBndr subst bndr
(subst_cv, cv') = substCoVarBndr subst bndr
subst_opt_id_bndr :: SimpleOptEnv -> InId -> (SimpleOptEnv, OutId)
subst_opt_id_bndr env@(SOE { soe_subst = subst, soe_inl = inl }) old_id
= (env { soe_subst = new_subst, soe_inl = new_inl }, new_id)
where
Subst in_scope id_subst tv_subst cv_subst = subst
id1 = uniqAway in_scope old_id
id2 = setIdType id1 (substTy subst (idType old_id))
new_id = zapFragileIdInfo id2
new_in_scope = in_scope `extendInScopeSet` new_id
no_change = new_id == old_id
new_id_subst
| no_change = delVarEnv id_subst old_id
| otherwise = extendVarEnv id_subst old_id (Var new_id)
new_subst = Subst new_in_scope new_id_subst tv_subst cv_subst
new_inl = delVarEnv inl old_id
add_info :: SimpleOptEnv -> InVar -> OutVar -> OutVar
add_info env old_bndr new_bndr
| isTyVar old_bndr = new_bndr
| otherwise = maybeModifyIdInfo mb_new_info new_bndr
where
subst = soe_subst env
mb_new_info = substIdInfo subst new_bndr (idInfo old_bndr)
simpleUnfoldingFun :: IdUnfoldingFun
simpleUnfoldingFun id
| isAlwaysActive (idInlineActivation id) = idUnfolding id
| otherwise = noUnfolding
wrapLet :: Maybe (Id,CoreExpr) -> CoreExpr -> CoreExpr
wrapLet Nothing body = body
wrapLet (Just (b,r)) body = Let (NonRec b r) body
joinPointBinding_maybe :: InBndr -> InExpr -> Maybe (InBndr, InExpr)
joinPointBinding_maybe bndr rhs
| not (isId bndr)
= Nothing
| isJoinId bndr
= Just (bndr, rhs)
| AlwaysTailCalled join_arity <- tailCallInfo (idOccInfo bndr)
, (bndrs, body) <- etaExpandToJoinPoint join_arity rhs
, let str_sig = idStrictness bndr
str_arity = count isId bndrs
join_bndr = bndr `asJoinId` join_arity
`setIdStrictness` etaExpandStrictSig str_arity str_sig
= Just (join_bndr, mkLams bndrs body)
| otherwise
= Nothing
joinPointBindings_maybe :: [(InBndr, InExpr)] -> Maybe [(InBndr, InExpr)]
joinPointBindings_maybe bndrs
= mapM (uncurry joinPointBinding_maybe) bndrs
data ConCont = CC [CoreExpr] Coercion
exprIsConApp_maybe :: InScopeEnv -> CoreExpr -> Maybe (DataCon, [Type], [CoreExpr])
exprIsConApp_maybe (in_scope, id_unf) expr
= go (Left in_scope) expr (CC [] (mkRepReflCo (exprType expr)))
where
go :: Either InScopeSet Subst
-> CoreExpr -> ConCont
-> Maybe (DataCon, [Type], [CoreExpr])
go subst (Tick t expr) cont
| not (tickishIsCode t) = go subst expr cont
go subst (Cast expr co1) (CC args co2)
| Just (args', m_co1') <- pushCoArgs (subst_co subst co1) args
= case m_co1' of
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)
| exprIsTrivial arg
= go (extend subst var arg) body (CC args co)
go (Right sub) (Var v) cont
= go (Left (substInScope sub))
(lookupIdSubst (text "exprIsConApp" <+> ppr expr) sub v)
cont
go (Left in_scope) (Var fun) cont@(CC args co)
| Just con <- isDataConWorkId_maybe fun
, count isValArg args == idArity fun
= pushCoDataCon con args co
| DFunUnfolding { df_bndrs = bndrs, df_con = con, df_args = dfun_args } <- unfolding
, bndrs `equalLength` args
, let subst = mkOpenSubst in_scope (bndrs `zip` args)
= pushCoDataCon con (map (substExpr (text "exprIsConApp1") subst) dfun_args) co
| idArity fun == 0
, Just rhs <- expandUnfolding_maybe unfolding
, let in_scope' = extendInScopeSetSet in_scope (exprFreeVars rhs)
= go (Left in_scope') rhs cont
| (fun `hasKey` unpackCStringIdKey) ||
(fun `hasKey` unpackCStringUtf8IdKey)
, [arg] <- args
, Just (MachStr str) <- exprIsLiteral_maybe (in_scope, id_unf) arg
= dealWithStringLiteral fun str co
where
unfolding = id_unf fun
go _ _ _ = Nothing
subst_co (Left {}) co = co
subst_co (Right s) co = CoreSubst.substCo s co
subst_arg (Left {}) e = e
subst_arg (Right s) e = substExpr (text "exprIsConApp2") s e
extend (Left in_scope) v e = Right (extendSubst (mkEmptySubst in_scope) v e)
extend (Right s) v e = Right (extendSubst s v e)
dealWithStringLiteral :: Var -> BS.ByteString -> Coercion
-> Maybe (DataCon, [Type], [CoreExpr])
dealWithStringLiteral _ str co
| BS.null str
= pushCoDataCon nilDataCon [Type charTy] co
dealWithStringLiteral fun str co
= let strFS = mkFastStringByteString str
char = mkConApp charDataCon [mkCharLit (headFS strFS)]
charTail = fastStringToByteString (tailFS strFS)
rest = if BS.null charTail
then mkConApp nilDataCon [Type charTy]
else App (Var fun)
(Lit (MachStr charTail))
in pushCoDataCon consDataCon [Type charTy, char, rest] co
exprIsLiteral_maybe :: InScopeEnv -> CoreExpr -> Maybe Literal
exprIsLiteral_maybe env@(_, id_unf) e
= case e of
Lit l -> Just l
Tick _ e' -> exprIsLiteral_maybe env e'
Var v | Just rhs <- expandUnfolding_maybe (id_unf v)
-> exprIsLiteral_maybe env rhs
_ -> Nothing
exprIsLambda_maybe :: InScopeEnv -> CoreExpr
-> Maybe (Var, CoreExpr,[Tickish Id])
exprIsLambda_maybe _ (Lam x e)
= Just (x, e, [])
exprIsLambda_maybe (in_scope_set, id_unf) (Tick t e)
| tickishFloatable t
, Just (x, e, ts) <- exprIsLambda_maybe (in_scope_set, id_unf) e
= Just (x, e, t:ts)
exprIsLambda_maybe (in_scope_set, id_unf) (Cast casted_e co)
| Just (x, e,ts) <- exprIsLambda_maybe (in_scope_set, id_unf) casted_e
, not (isTyVar x) && not (isCoVar x)
, ASSERT( not $ x `elemVarSet` tyCoVarsOfCo co) True
, Just (x',e') <- pushCoercionIntoLambda in_scope_set x e co
, let res = Just (x',e',ts)
=
res
exprIsLambda_maybe (in_scope_set, id_unf) e
| (Var f, as, ts) <- collectArgsTicks tickishFloatable e
, idArity f > count isValArg as
, Just rhs <- expandUnfolding_maybe (id_unf f)
, let e' = simpleOptExprWith unsafeGlobalDynFlags (mkEmptySubst in_scope_set) (rhs `mkApps` as)
, Just (x', e'', ts') <- exprIsLambda_maybe (in_scope_set, id_unf) e'
, let res = Just (x', e'', ts++ts')
=
res
exprIsLambda_maybe _ _e
=
Nothing
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
MCo co1 -> do { (args', m_co2) <- pushCoArgs co1 args
; return (arg':args', m_co2) }
MRefl -> return (arg':args, MRefl) }
pushCoArg :: CoercionR -> CoreArg -> Maybe (CoreArg, MCoercion)
pushCoArg co (Type ty) = do { (ty', m_co') <- pushCoTyArg co ty
; return (Type ty', m_co') }
pushCoArg co val_arg = do { (arg_co, m_co') <- pushCoValArg co
; return (val_arg `mkCast` arg_co, m_co') }
pushCoTyArg :: CoercionR -> Type -> Maybe (Type, MCoercionR)
pushCoTyArg co ty
| isReflCo co
= Just (ty, MRefl)
| isForAllTy tyL
= ASSERT2( isForAllTy tyR, ppr co $$ ppr ty )
Just (ty `mkCastTy` co1, MCo co2)
| otherwise
= Nothing
where
Pair tyL tyR = coercionKind co
co1 = mkSymCo (mkNthCo Nominal 0 co)
co2 = mkInstCo co (mkCoherenceLeftCo (mkNomReflCo ty) co1)
pushCoValArg :: CoercionR -> Maybe (Coercion, MCoercion)
pushCoValArg co
| isReflCo co
= Just (mkRepReflCo arg, MRefl)
| isFunTy tyL
, (co1, co2) <- decomposeFunCo Representational co
= ASSERT2( isFunTy tyR, ppr co $$ ppr arg )
Just (mkSymCo co1, MCo co2)
| otherwise
= Nothing
where
arg = funArgTy tyR
Pair tyL tyR = coercionKind co
pushCoercionIntoLambda
:: InScopeSet -> Var -> CoreExpr -> CoercionR -> Maybe (Var, CoreExpr)
pushCoercionIntoLambda in_scope x e co
| ASSERT(not (isTyVar x) && not (isCoVar x)) True
, Pair s1s2 t1t2 <- coercionKind co
, Just (_s1,_s2) <- splitFunTy_maybe s1s2
, Just (t1,_t2) <- splitFunTy_maybe t1t2
= let (co1, co2) = decomposeFunCo Representational co
x' = x `setIdType` t1
in_scope' = in_scope `extendInScopeSet` x'
subst = extendIdSubst (mkEmptySubst in_scope')
x
(mkCast (Var x') co1)
in Just (x', substExpr (text "pushCoercionIntoLambda") subst e `mkCast` co2)
| otherwise
= pprTrace "exprIsLambda_maybe: Unexpected lambda in case" (ppr (Lam x e))
Nothing
pushCoDataCon :: DataCon -> [CoreExpr] -> Coercion
-> Maybe (DataCon
, [Type]
, [CoreExpr])
pushCoDataCon dc dc_args co
| isReflCo co || from_ty `eqType` to_ty
, let (univ_ty_args, rest_args) = splitAtList (dataConUnivTyVars dc) dc_args
= Just (dc, map exprToType univ_ty_args, rest_args)
| Just (to_tc, to_tc_arg_tys) <- splitTyConApp_maybe to_ty
, to_tc == dataConTyCon dc
= let
tc_arity = tyConArity to_tc
dc_univ_tyvars = dataConUnivTyVars dc
dc_ex_tyvars = dataConExTyVars dc
arg_tys = dataConRepArgTys dc
non_univ_args = dropList dc_univ_tyvars dc_args
(ex_args, val_args) = splitAtList dc_ex_tyvars non_univ_args
omegas = decomposeCo tc_arity co (tyConRolesRepresentational to_tc)
(psi_subst, to_ex_arg_tys)
= liftCoSubstWithEx Representational
dc_univ_tyvars
omegas
dc_ex_tyvars
(map exprToType ex_args)
new_val_args = zipWith cast_arg arg_tys val_args
cast_arg arg_ty arg = mkCast arg (psi_subst arg_ty)
to_ex_args = map Type to_ex_arg_tys
dump_doc = vcat [ppr dc, ppr dc_univ_tyvars, ppr dc_ex_tyvars,
ppr arg_tys, ppr dc_args,
ppr ex_args, ppr val_args, ppr co, ppr from_ty, ppr to_ty, ppr to_tc ]
in
ASSERT2( eqType from_ty (mkTyConApp to_tc (map exprToType $ takeList dc_univ_tyvars dc_args)), dump_doc )
ASSERT2( equalLength val_args arg_tys, dump_doc )
Just (dc, to_tc_arg_tys, to_ex_args ++ new_val_args)
| otherwise
= Nothing
where
Pair from_ty to_ty = coercionKind co
collectBindersPushingCo :: CoreExpr -> ([Var], CoreExpr)
collectBindersPushingCo e
= go [] e
where
go :: [Var] -> CoreExpr -> ([Var], CoreExpr)
go bs (Lam b e) = go (b:bs) e
go bs (Cast e co) = go_c bs e co
go bs e = (reverse bs, e)
go_c :: [Var] -> CoreExpr -> CoercionR -> ([Var], CoreExpr)
go_c bs (Cast e co1) co2 = go_c bs e (co1 `mkTransCo` co2)
go_c bs (Lam b e) co = go_lam bs b e co
go_c bs e co = (reverse bs, mkCast e co)
go_lam :: [Var] -> Var -> CoreExpr -> CoercionR -> ([Var], CoreExpr)
go_lam bs b e co
| isTyVar b
, let Pair tyL tyR = coercionKind co
, ASSERT( isForAllTy tyL )
isForAllTy tyR
, isReflCo (mkNthCo Nominal 0 co)
= go_c (b:bs) e (mkInstCo co (mkNomReflCo (mkTyVarTy b)))
| isId b
, let Pair tyL tyR = coercionKind co
, ASSERT( isFunTy tyL) isFunTy tyR
, (co_arg, co_res) <- decomposeFunCo Representational co
, isReflCo co_arg
= go_c (b:bs) e co_res
| otherwise = (reverse bs, mkCast (Lam b e) co)