diff options
Diffstat (limited to 'compiler/coreSyn/CoreOpt.hs')
| -rw-r--r-- | compiler/coreSyn/CoreOpt.hs | 306 |
1 files changed, 170 insertions, 136 deletions
diff --git a/compiler/coreSyn/CoreOpt.hs b/compiler/coreSyn/CoreOpt.hs index 4a196057b1..2367c4548d 100644 --- a/compiler/coreSyn/CoreOpt.hs +++ b/compiler/coreSyn/CoreOpt.hs @@ -20,7 +20,9 @@ module CoreOpt ( #include "HsVersions.h" -import CoreArity( joinRhsArity, etaExpandToJoinPoint ) +import GhcPrelude + +import CoreArity( etaExpandToJoinPoint ) import CoreSyn import CoreSubst @@ -30,10 +32,11 @@ import PprCore ( pprCoreBindings, pprRules ) import OccurAnal( occurAnalyseExpr, occurAnalysePgm ) import Literal ( Literal(MachStr) ) import Id -import Var ( varType ) +import Var ( varType, isNonCoVarId ) import VarSet import VarEnv import DataCon +import Demand( etaExpandStrictSig ) import OptCoercion ( optCoercion ) import Type hiding ( substTy, extendTvSubst, extendCvSubst, extendTvSubstList , isInScope, substTyVarBndr, cloneTyVarBndr ) @@ -84,7 +87,7 @@ little dance in action; the full Simplifier is a lot more complicated. -} -simpleOptExpr :: CoreExpr -> CoreExpr +simpleOptExpr :: DynFlags -> CoreExpr -> CoreExpr -- See Note [The simple optimiser] -- Do simple optimisation on an expression -- The optimisation is very straightforward: just @@ -101,9 +104,9 @@ simpleOptExpr :: CoreExpr -> CoreExpr -- in (let x = y in ....) we substitute for x; so y's occ-info -- may change radically -simpleOptExpr expr +simpleOptExpr dflags expr = -- pprTrace "simpleOptExpr" (ppr init_subst $$ ppr expr) - simpleOptExprWith init_subst expr + simpleOptExprWith dflags init_subst expr where init_subst = mkEmptySubst (mkInScopeSet (exprFreeVars expr)) -- It's potentially important to make a proper in-scope set @@ -116,32 +119,35 @@ simpleOptExpr expr -- It's a bit painful to call exprFreeVars, because it makes -- three passes instead of two (occ-anal, and go) -simpleOptExprWith :: Subst -> InExpr -> OutExpr +simpleOptExprWith :: DynFlags -> Subst -> InExpr -> OutExpr -- See Note [The simple optimiser] -simpleOptExprWith subst expr +simpleOptExprWith dflags subst expr = simple_opt_expr init_env (occurAnalyseExpr expr) where - init_env = SOE { soe_inl = emptyVarEnv, soe_subst = subst } + init_env = SOE { soe_dflags = dflags + , soe_inl = emptyVarEnv + , soe_subst = subst } ---------------------- simpleOptPgm :: DynFlags -> Module - -> CoreProgram -> [CoreRule] -> [CoreVect] - -> IO (CoreProgram, [CoreRule], [CoreVect]) + -> CoreProgram -> [CoreRule] + -> IO (CoreProgram, [CoreRule]) -- See Note [The simple optimiser] -simpleOptPgm dflags this_mod binds rules vects +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', vects') } + ; return (reverse binds', rules') } where - occ_anald_binds = occurAnalysePgm this_mod (\_ -> False) {- No rules active -} - rules vects emptyVarSet binds + occ_anald_binds = occurAnalysePgm this_mod + (\_ -> True) {- All unfoldings active -} + (\_ -> False) {- No rules active -} + rules binds - (final_env, binds') = foldl do_one (emptyEnv, []) occ_anald_binds + (final_env, binds') = foldl' do_one (emptyEnv dflags, []) occ_anald_binds final_subst = soe_subst final_env rules' = substRulesForImportedIds final_subst rules - vects' = substVects final_subst vects -- We never unconditionally inline into rules, -- hence paying just a substitution @@ -156,7 +162,8 @@ simpleOptPgm dflags this_mod binds rules vects type SimpleClo = (SimpleOptEnv, InExpr) data SimpleOptEnv - = SOE { soe_inl :: IdEnv SimpleClo + = SOE { soe_dflags :: DynFlags + , soe_inl :: IdEnv SimpleClo -- Deals with preInlineUnconditionally; things -- that occur exactly once and are inlined -- without having first been simplified @@ -171,13 +178,15 @@ instance Outputable SimpleOptEnv where , text "soe_subst =" <+> ppr subst ] <+> text "}" -emptyEnv :: SimpleOptEnv -emptyEnv = SOE { soe_inl = emptyVarEnv - , soe_subst = emptySubst } +emptyEnv :: DynFlags -> SimpleOptEnv +emptyEnv dflags + = SOE { soe_dflags = dflags + , soe_inl = emptyVarEnv + , soe_subst = emptySubst } soeZapSubst :: SimpleOptEnv -> SimpleOptEnv -soeZapSubst (SOE { soe_subst = subst }) - = SOE { soe_inl = emptyVarEnv, soe_subst = zapSubstEnv subst } +soeZapSubst env@(SOE { soe_subst = subst }) + = env { soe_inl = emptyVarEnv, soe_subst = zapSubstEnv subst } soeSetInScope :: SimpleOptEnv -> SimpleOptEnv -> SimpleOptEnv -- Take in-scope set from env1, and the rest from env2 @@ -206,13 +215,13 @@ simple_opt_expr env expr go (App e1 e2) = simple_app env e1 [(env,e2)] go (Type ty) = Type (substTy subst ty) - go (Coercion co) = Coercion (optCoercion (getTCvSubst subst) co) + 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 (getTCvSubst subst) co + 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 @@ -323,7 +332,7 @@ simple_opt_bind env (Rec prs) 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') + (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 @@ -347,30 +356,43 @@ simple_bind_pair env@(SOE { soe_inl = inl_env, soe_subst = subst }) (env { soe_subst = extendTvSubst subst in_bndr out_ty }, Nothing) | Coercion co <- in_rhs - , let out_co = optCoercion (getTCvSubst (soe_subst rhs_env)) co + , 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 + | ASSERT2( isNonCoVarId in_bndr, ppr in_bndr ) + -- The previous two guards got rid of tyvars and coercions + -- See Note [CoreSyn type and coercion invariant] in CoreSyn + pre_inline_unconditionally = (env { soe_inl = extendVarEnv inl_env in_bndr clo }, Nothing) | otherwise - = simple_out_bind_pair env in_bndr mb_out_bndr - (simple_opt_clo env clo) + = 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 -- See Note [Preserve join-binding 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 -- See Note [Do not inline CoVars unconditionally] - | isExportedId in_bndr = False -- in SimplUtils + | isExportedId in_bndr = False | stable_unf = False | not active = False -- Note [Inline prag in simplOpt] | not (safe_to_inline occ) = False - | otherwise = True + | otherwise = True -- Unconditionally safe to inline safe_to_inline :: OccInfo -> Bool @@ -403,7 +425,10 @@ simple_out_bind_pair :: SimpleOptEnv -> (SimpleOptEnv, Maybe (OutVar, OutExpr)) simple_out_bind_pair env in_bndr mb_out_bndr out_rhs occ_info active stable_unf - | post_inline_unconditionally + | ASSERT2( isNonCoVarId in_bndr, ppr in_bndr ) + -- Type and coercion bindings are caught earlier + -- See Note [CoreSyn type and coercion invariant] + post_inline_unconditionally = ( env' { soe_subst = extendIdSubst (soe_subst env) in_bndr out_rhs } , Nothing) @@ -417,14 +442,16 @@ simple_out_bind_pair env in_bndr mb_out_bndr out_rhs post_inline_unconditionally :: Bool post_inline_unconditionally - | not active = False - | isWeakLoopBreaker occ_info = False -- If it's a loop-breaker of any kind, don't inline - -- because it might be referred to "earlier" - | stable_unf = False -- Note [Stable unfoldings and postInlineUnconditionally] - | isExportedId in_bndr = False -- Note [Exported Ids and trivial RHSs] - | exprIsTrivial out_rhs = True - | coercible_hack = True - | otherwise = False + | isExportedId in_bndr = False -- Note [Exported Ids and trivial RHSs] + | stable_unf = False -- Note [Stable unfoldings and postInlineUnconditionally] + | not active = False -- in SimplUtils + | is_loop_breaker = False -- If it's a loop-breaker of any kind, don't inline + -- because it might be referred to "earlier" + | exprIsTrivial out_rhs = True + | coercible_hack = True + | otherwise = False + + is_loop_breaker = isWeakLoopBreaker occ_info -- See Note [Getting the map/coerce RULE to work] coercible_hack | (Var fun, args) <- collectArgs out_rhs @@ -447,6 +474,14 @@ trivial ones. But we do here! Why? In the simple optimiser Those differences obviate the reasons for not inlining a trivial rhs, and increase the benefit for doing so. So we unconditionally inline trivial rhss here. + +Note [Preserve join-binding arity] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Be careful /not/ to eta-reduce the RHS of a join point, lest we lose +the join-point arity invariant. Trac #15108 was caused by simplifying +the RHS with simple_opt_expr, which does eta-reduction. Solution: +simplify the RHS of a join point by simplifying under the lambdas +(which of course should be there). -} ---------------------- @@ -471,8 +506,8 @@ subst_opt_id_bndr :: SimpleOptEnv -> InId -> (SimpleOptEnv, OutId) -- It's important to zap fragile OccInfo (which CoreSubst.substIdBndr -- carefully does not do) because simplOptExpr invalidates it -subst_opt_id_bndr (SOE { soe_subst = subst, soe_inl = inl }) old_id - = (SOE { soe_subst = new_subst, soe_inl = new_inl }, new_id) +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 @@ -513,18 +548,6 @@ wrapLet :: Maybe (Id,CoreExpr) -> CoreExpr -> CoreExpr wrapLet Nothing body = body wrapLet (Just (b,r)) body = Let (NonRec b r) body ------------------- -substVects :: Subst -> [CoreVect] -> [CoreVect] -substVects subst = map (substVect subst) - ------------------- -substVect :: Subst -> CoreVect -> CoreVect -substVect subst (Vect v rhs) = Vect v (simpleOptExprWith subst rhs) -substVect _subst vd@(NoVect _) = vd -substVect _subst vd@(VectType _ _ _) = vd -substVect _subst vd@(VectClass _) = vd -substVect _subst vd@(VectInst _) = vd - {- Note [Inline prag in simplOpt] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -642,58 +665,43 @@ joinPointBinding_maybe bndr rhs = Just (bndr, rhs) | AlwaysTailCalled join_arity <- tailCallInfo (idOccInfo bndr) - , not (bad_unfolding join_arity (idUnfolding bndr)) , (bndrs, body) <- etaExpandToJoinPoint join_arity rhs - = Just (bndr `asJoinId` join_arity, mkLams bndrs body) + , let str_sig = idStrictness bndr + str_arity = count isId bndrs -- Strictness demands are for Ids only + join_bndr = bndr `asJoinId` join_arity + `setIdStrictness` etaExpandStrictSig str_arity str_sig + = Just (join_bndr, mkLams bndrs body) | otherwise = Nothing - where - -- bad_unfolding returns True if we should /not/ convert a non-join-id - -- into a join-id, even though it is AlwaysTailCalled - -- See Note [Join points and INLINE pragmas] - bad_unfolding join_arity (CoreUnfolding { uf_src = src, uf_tmpl = rhs }) - = isStableSource src && join_arity > joinRhsArity rhs - bad_unfolding _ (DFunUnfolding {}) - = True - bad_unfolding _ _ - = False - joinPointBindings_maybe :: [(InBndr, InExpr)] -> Maybe [(InBndr, InExpr)] joinPointBindings_maybe bndrs = mapM (uncurry joinPointBinding_maybe) bndrs -{- Note [Join points and INLINE pragmas] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider - f x = let g = \x. not -- Arity 1 - {-# INLINE g #-} - in case x of - A -> g True True - B -> g True False - C -> blah2 +{- Note [Strictness and join points] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have -Here 'g' is always tail-called applied to 2 args, but the stable -unfolding captured by the INLINE pragma has arity 1. If we try to -convert g to be a join point, its unfolding will still have arity 1 -(since it is stable, and we don't meddle with stable unfoldings), and -Lint will complain (see Note [Invariants on join points], (2a), in -CoreSyn. Trac #13413. + let f = \x. if x>200 then e1 else e1 -Moreover, since g is going to be inlined anyway, there is no benefit -from making it a join point. +and we know that f is strict in x. Then if we subsequently +discover that f is an arity-2 join point, we'll eta-expand it to -If it is recursive, and uselessly marked INLINE, this will stop us -making it a join point, which is annoying. But occasionally -(notably in class methods; see Note [Instances and loop breakers] in -TcInstDcls) we mark recursive things as INLINE but the recursion -unravels; so ignoring INLINE pragmas on recursive things isn't good -either. + let f = \x y. if x>200 then e1 else e1 +and now it's only strict if applied to two arguments. So we should +adjust the strictness info. -************************************************************************ +A more common case is when + + f = \x. error ".." + +and again its arity increses (Trac #15517) +-} + +{- ********************************************************************* * * exprIsConApp_maybe * * @@ -768,9 +776,11 @@ exprIsConApp_maybe (in_scope, id_unf) expr go subst (Tick t expr) cont | not (tickishIsCode t) = go subst expr cont go subst (Cast expr co1) (CC args co2) - | Just (args', co1') <- pushCoArgs (subst_co subst co1) args + | Just (args', m_co1') <- pushCoArgs (subst_co subst co1) args -- See Note [Push coercions in exprIsConApp_maybe] - = go subst expr (CC args' (co1' `mkTransCo` co2)) + = 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) @@ -930,7 +940,7 @@ exprIsLambda_maybe (in_scope_set, id_unf) e -- Make sure there is hope to get a lambda , Just rhs <- expandUnfolding_maybe (id_unf f) -- Optimize, for beta-reduction - , let e' = simpleOptExprWith (mkEmptySubst in_scope_set) (rhs `mkApps` as) + , let e' = simpleOptExprWith unsafeGlobalDynFlags (mkEmptySubst in_scope_set) (rhs `mkApps` as) -- Recurse, because of possible casts , Just (x', e'', ts') <- exprIsLambda_maybe (in_scope_set, id_unf) e' , let res = Just (x', e'', ts++ts') @@ -964,36 +974,45 @@ Here we implement the "push rules" from FC papers: by pushing the coercion into the arguments -} -pushCoArgs :: Coercion -> [CoreArg] -> Maybe ([CoreArg], Coercion) -pushCoArgs co [] = return ([], co) -pushCoArgs co (arg:args) = do { (arg', co1) <- pushCoArg co arg - ; (args', co2) <- pushCoArgs co1 args - ; return (arg':args', co2) } +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 :: Coercion -> CoreArg -> Maybe (CoreArg, 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 -- C.f. simplCast in Simplify.hs -- 'co' is always Representational +-- If the returned coercion is Nothing, then it would have been reflexive +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') } -pushCoArg co (Type ty) = do { (ty', co') <- pushCoTyArg co ty - ; return (Type ty', co') } -pushCoArg co val_arg = do { (arg_co, co') <- pushCoValArg co - ; return (mkCast val_arg arg_co, co') } - -pushCoTyArg :: Coercion -> Type -> Maybe (Type, Coercion) +pushCoTyArg :: CoercionR -> Type -> Maybe (Type, MCoercionR) -- We have (fun |> co) @ty -- Push the coercion through to return -- (fun @ty') |> co' -- 'co' is always Representational +-- If the returned coercion is Nothing, then it would have been reflexive; +-- it's faster not to compute it, though. pushCoTyArg co ty - | tyL `eqType` tyR - = Just (ty, mkRepReflCo (piResultTy tyR ty)) + -- The following is inefficient - don't do `eqType` here, the coercion + -- optimizer will take care of it. See Trac #14737. + -- -- | tyL `eqType` tyR + -- -- = Just (ty, Nothing) + + | isReflCo co + = Just (ty, MRefl) - | isForAllTy tyL - = ASSERT2( isForAllTy tyR, ppr co $$ ppr ty ) - Just (ty `mkCastTy` mkSymCo co1, co2) + | isForAllTy_ty tyL + = ASSERT2( isForAllTy_ty tyR, ppr co $$ ppr ty ) + Just (ty `mkCastTy` co1, MCo co2) | otherwise = Nothing @@ -1003,41 +1022,48 @@ pushCoTyArg co ty -- tyL = forall (a1 :: k1). ty1 -- tyR = forall (a2 :: k2). ty2 - co1 = mkNthCo 0 co - -- co1 :: k1 ~ k2 - -- Note that NthCo can extract an equality between the kinds - -- of the types related by a coercion between forall-types. + co1 = mkSymCo (mkNthCo Nominal 0 co) + -- co1 :: k2 ~N k1 + -- Note that NthCo can extract a Nominal equality between the + -- kinds of the types related by a coercion between forall-types. -- See the NthCo case in CoreLint. - co2 = mkInstCo co (mkCoherenceLeftCo (mkNomReflCo ty) co1) + co2 = mkInstCo co (mkGReflLeftCo Nominal ty co1) -- co2 :: ty1[ (ty|>co1)/a1 ] ~ ty2[ ty/a2 ] -- Arg of mkInstCo is always nominal, hence mkNomReflCo -pushCoValArg :: Coercion -> Maybe (Coercion, Coercion) +pushCoValArg :: CoercionR -> Maybe (Coercion, MCoercion) -- We have (fun |> co) arg -- Push the coercion through to return -- (fun (arg |> co_arg)) |> co_res -- 'co' is always Representational +-- If the second returned Coercion is actually Nothing, then no cast is necessary; +-- the returned coercion would have been reflexive. pushCoValArg co - | tyL `eqType` tyR - = Just (mkRepReflCo arg, mkRepReflCo res) + -- The following is inefficient - don't do `eqType` here, the coercion + -- optimizer will take care of it. See Trac #14737. + -- -- | tyL `eqType` tyR + -- -- = Just (mkRepReflCo arg, Nothing) + + | isReflCo co + = Just (mkRepReflCo arg, MRefl) | isFunTy tyL - , (co1, co2) <- decomposeFunCo co + , (co1, co2) <- decomposeFunCo Representational co -- If co :: (tyL1 -> tyL2) ~ (tyR1 -> tyR2) -- then co1 :: tyL1 ~ tyR1 -- co2 :: tyL2 ~ tyR2 = ASSERT2( isFunTy tyR, ppr co $$ ppr arg ) - Just (mkSymCo co1, co2) + Just (mkSymCo co1, MCo co2) | otherwise = Nothing where - (arg, res) = splitFunTy tyR + arg = funArgTy tyR Pair tyL tyR = coercionKind co pushCoercionIntoLambda - :: InScopeSet -> Var -> CoreExpr -> Coercion -> Maybe (Var, CoreExpr) + :: InScopeSet -> Var -> CoreExpr -> CoercionR -> Maybe (Var, CoreExpr) -- This implements the Push rule from the paper on coercions -- (\x. e) |> co -- ===> @@ -1047,7 +1073,7 @@ pushCoercionIntoLambda in_scope x e co , Pair s1s2 t1t2 <- coercionKind co , Just (_s1,_s2) <- splitFunTy_maybe s1s2 , Just (t1,_t2) <- splitFunTy_maybe t1t2 - = let (co1, co2) = decomposeFunCo co + = let (co1, co2) = decomposeFunCo Representational co -- Should we optimize the coercions here? -- Otherwise they might not match too well x' = x `setIdType` t1 @@ -1086,19 +1112,19 @@ pushCoDataCon dc dc_args co = let tc_arity = tyConArity to_tc dc_univ_tyvars = dataConUnivTyVars dc - dc_ex_tyvars = dataConExTyVars dc + dc_ex_tcvars = dataConExTyCoVars 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 + (ex_args, val_args) = splitAtList dc_ex_tcvars non_univ_args -- Make the "Psi" from the paper - omegas = decomposeCo tc_arity co + omegas = decomposeCo tc_arity co (tyConRolesRepresentational to_tc) (psi_subst, to_ex_arg_tys) = liftCoSubstWithEx Representational dc_univ_tyvars omegas - dc_ex_tyvars + dc_ex_tcvars (map exprToType ex_args) -- Cast the value arguments (which include dictionaries) @@ -1107,7 +1133,7 @@ pushCoDataCon dc dc_args co to_ex_args = map Type to_ex_arg_tys - dump_doc = vcat [ppr dc, ppr dc_univ_tyvars, ppr dc_ex_tyvars, + dump_doc = vcat [ppr dc, ppr dc_univ_tyvars, ppr dc_ex_tcvars, ppr arg_tys, ppr dc_args, ppr ex_args, ppr val_args, ppr co, ppr from_ty, ppr to_ty, ppr to_tc ] in @@ -1140,7 +1166,7 @@ collectBindersPushingCo e go bs e = (reverse bs, e) -- We are in a cast; peel off casts until we hit a lambda. - go_c :: [Var] -> CoreExpr -> Coercion -> ([Var], CoreExpr) + go_c :: [Var] -> CoreExpr -> CoercionR -> ([Var], CoreExpr) -- (go_c bs e c) is same as (go bs e (e |> c)) 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 @@ -1148,20 +1174,28 @@ collectBindersPushingCo e -- We are in a lambda under a cast; peel off lambdas and build a -- new coercion for the body. - go_lam :: [Var] -> Var -> CoreExpr -> Coercion -> ([Var], CoreExpr) + go_lam :: [Var] -> Var -> CoreExpr -> CoercionR -> ([Var], CoreExpr) -- (go_lam bs b e c) is same as (go_c bs (\b.e) c) go_lam bs b e co | isTyVar b , let Pair tyL tyR = coercionKind co - , ASSERT( isForAllTy tyL ) - isForAllTy tyR - , isReflCo (mkNthCo 0 co) -- See Note [collectBindersPushingCo] + , ASSERT( isForAllTy_ty tyL ) + isForAllTy_ty tyR + , isReflCo (mkNthCo Nominal 0 co) -- See Note [collectBindersPushingCo] = go_c (b:bs) e (mkInstCo co (mkNomReflCo (mkTyVarTy b))) + | isCoVar b + , let Pair tyL tyR = coercionKind co + , ASSERT( isForAllTy_co tyL ) + isForAllTy_co tyR + , isReflCo (mkNthCo Nominal 0 co) -- See Note [collectBindersPushingCo] + , let cov = mkCoVarCo b + = go_c (b:bs) e (mkInstCo co (mkNomReflCo (mkCoercionTy cov))) + | isId b , let Pair tyL tyR = coercionKind co , ASSERT( isFunTy tyL) isFunTy tyR - , (co_arg, co_res) <- decomposeFunCo co + , (co_arg, co_res) <- decomposeFunCo Representational co , isReflCo co_arg -- See Note [collectBindersPushingCo] = go_c (b:bs) e co_res |