2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
8 -- ** Simple expression optimiser
9 simpleOptPgm
, simpleOptExpr
, simpleOptExprWith
,
12 joinPointBinding_maybe
, joinPointBindings_maybe
,
14 -- ** Predicates on expressions
15 exprIsConApp_maybe
, exprIsLiteral_maybe
, exprIsLambda_maybe
,
17 -- ** Coercions and casts
18 pushCoArg
, pushCoValArg
, pushCoTyArg
, collectBindersPushingCo
21 #include
"HsVersions.h"
25 import CoreArity
( etaExpandToJoinPoint
)
31 import PprCore
( pprCoreBindings
, pprRules
)
32 import OccurAnal
( occurAnalyseExpr
, occurAnalysePgm
)
33 import Literal
( Literal
(LitString
) )
35 import Var
( isNonCoVarId
)
39 import Demand
( etaExpandStrictSig
)
40 import OptCoercion
( optCoercion
)
41 import Type
hiding ( substTy
, extendTvSubst
, extendCvSubst
, extendTvSubstList
42 , isInScope
, substTyVarBndr
, cloneTyVarBndr
)
43 import Coercion
hiding ( substCo
, substCoVarBndr
)
44 import TyCon
( tyConArity
)
48 import Module
( Module
)
54 import Maybes
( orElse
)
57 import qualified Data
.ByteString
as BS
60 ************************************************************************
64 ************************************************************************
66 Note [The simple optimiser]
67 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
68 The simple optimiser is a lightweight, pure (non-monadic) function
69 that rapidly does a lot of simple optimisations, including
71 - inlining things that occur just once,
72 or whose RHS turns out to be trivial
74 - case of known constructor
75 - dead code elimination
77 It does NOT do any call-site inlining; it only inlines a function if
78 it can do so unconditionally, dropping the binding. It thereby
79 guarantees to leave no un-reduced beta-redexes.
81 It is careful to follow the guidance of "Secrets of the GHC inliner",
82 and in particular the pre-inline-unconditionally and
83 post-inline-unconditionally story, to do effective beta reduction on
84 functions called precisely once, without repeatedly optimising the same
85 expression. In fact, the simple optimiser is a good example of this
86 little dance in action; the full Simplifier is a lot more complicated.
90 simpleOptExpr
:: DynFlags
-> CoreExpr
-> CoreExpr
91 -- See Note [The simple optimiser]
92 -- Do simple optimisation on an expression
93 -- The optimisation is very straightforward: just
94 -- inline non-recursive bindings that are used only once,
95 -- or where the RHS is trivial
97 -- We also inline bindings that bind a Eq# box: see
98 -- See Note [Getting the map/coerce RULE to work].
100 -- Also we convert functions to join points where possible (as
101 -- the occurrence analyser does most of the work anyway).
103 -- The result is NOT guaranteed occurrence-analysed, because
104 -- in (let x = y in ....) we substitute for x; so y's occ-info
105 -- may change radically
107 simpleOptExpr dflags expr
108 = -- pprTrace "simpleOptExpr" (ppr init_subst $$ ppr expr)
109 simpleOptExprWith dflags init_subst expr
111 init_subst
= mkEmptySubst
(mkInScopeSet
(exprFreeVars expr
))
112 -- It's potentially important to make a proper in-scope set
113 -- Consider let x = ..y.. in \y. ...x...
114 -- Then we should remember to clone y before substituting
115 -- for x. It's very unlikely to occur, because we probably
116 -- won't *be* substituting for x if it occurs inside a
119 -- It's a bit painful to call exprFreeVars, because it makes
120 -- three passes instead of two (occ-anal, and go)
122 simpleOptExprWith
:: DynFlags
-> Subst
-> InExpr
-> OutExpr
123 -- See Note [The simple optimiser]
124 simpleOptExprWith dflags subst expr
125 = simple_opt_expr init_env
(occurAnalyseExpr expr
)
127 init_env
= SOE
{ soe_dflags
= dflags
128 , soe_inl
= emptyVarEnv
129 , soe_subst
= subst
}
131 ----------------------
132 simpleOptPgm
:: DynFlags
-> Module
133 -> CoreProgram
-> [CoreRule
]
134 -> IO (CoreProgram
, [CoreRule
])
135 -- See Note [The simple optimiser]
136 simpleOptPgm dflags this_mod binds rules
137 = do { dumpIfSet_dyn dflags Opt_D_dump_occur_anal
"Occurrence analysis"
138 (pprCoreBindings occ_anald_binds
$$ pprRules rules
);
140 ; return (reverse binds
', rules
') }
142 occ_anald_binds
= occurAnalysePgm this_mod
143 (\_
-> True) {- All unfoldings active -}
144 (\_
-> False) {- No rules active -}
147 (final_env
, binds
') = foldl' do_one
(emptyEnv dflags
, []) occ_anald_binds
148 final_subst
= soe_subst final_env
150 rules
' = substRulesForImportedIds final_subst rules
151 -- We never unconditionally inline into rules,
152 -- hence paying just a substitution
154 do_one
(env
, binds
') bind
155 = case simple_opt_bind env bind
of
156 (env
', Nothing
) -> (env
', binds
')
157 (env
', Just bind
') -> (env
', bind
':binds
')
159 -- In these functions the substitution maps InVar -> OutExpr
161 ----------------------
162 type SimpleClo
= (SimpleOptEnv
, InExpr
)
165 = SOE
{ soe_dflags
:: DynFlags
166 , soe_inl
:: IdEnv SimpleClo
167 -- Deals with preInlineUnconditionally; things
168 -- that occur exactly once and are inlined
169 -- without having first been simplified
172 -- Deals with cloning; includes the InScopeSet
175 instance Outputable SimpleOptEnv
where
176 ppr
(SOE
{ soe_inl
= inl
, soe_subst
= subst
})
177 = text
"SOE {" <+> vcat
[ text
"soe_inl =" <+> ppr inl
178 , text
"soe_subst =" <+> ppr subst
]
181 emptyEnv
:: DynFlags
-> SimpleOptEnv
183 = SOE
{ soe_dflags
= dflags
184 , soe_inl
= emptyVarEnv
185 , soe_subst
= emptySubst
}
187 soeZapSubst
:: SimpleOptEnv
-> SimpleOptEnv
188 soeZapSubst env
@(SOE
{ soe_subst
= subst
})
189 = env
{ soe_inl
= emptyVarEnv
, soe_subst
= zapSubstEnv subst
}
191 soeSetInScope
:: SimpleOptEnv
-> SimpleOptEnv
-> SimpleOptEnv
192 -- Take in-scope set from env1, and the rest from env2
193 soeSetInScope
(SOE
{ soe_subst
= subst1
})
194 env2
@(SOE
{ soe_subst
= subst2
})
195 = env2
{ soe_subst
= setInScope subst2
(substInScope subst1
) }
198 simple_opt_clo
:: SimpleOptEnv
-> SimpleClo
-> OutExpr
199 simple_opt_clo env
(e_env
, e
)
200 = simple_opt_expr
(soeSetInScope env e_env
) e
202 simple_opt_expr
:: SimpleOptEnv
-> InExpr
-> OutExpr
203 simple_opt_expr env expr
206 subst
= soe_subst env
207 in_scope
= substInScope subst
208 in_scope_env
= (in_scope
, simpleUnfoldingFun
)
211 | Just clo
<- lookupVarEnv
(soe_inl env
) v
212 = simple_opt_clo env clo
214 = lookupIdSubst
(text
"simpleOptExpr") (soe_subst env
) v
216 go
(App e1 e2
) = simple_app env e1
[(env
,e2
)]
217 go
(Type ty
) = Type
(substTy subst ty
)
218 go
(Coercion co
) = Coercion
(optCoercion
(soe_dflags env
) (getTCvSubst subst
) co
)
219 go
(Lit lit
) = Lit lit
220 go
(Tick tickish e
) = mkTick
(substTickish subst tickish
) (go e
)
221 go
(Cast e co
) | isReflCo co
' = go e
222 |
otherwise = Cast
(go e
) co
'
224 co
' = optCoercion
(soe_dflags env
) (getTCvSubst subst
) co
226 go
(Let bind body
) = case simple_opt_bind env bind
of
227 (env
', Nothing
) -> simple_opt_expr env
' body
228 (env
', Just bind
) -> Let bind
(simple_opt_expr env
' body
)
230 go lam
@(Lam
{}) = go_lam env
[] lam
232 -- See Note [Getting the map/coerce RULE to work]
234 , Just
(con
, _tys
, es
) <- exprIsConApp_maybe in_scope_env e
'
235 , Just
(altcon
, bs
, rhs
) <- findAlt
(DataAlt con
) as
238 _
-> foldr wrapLet
(simple_opt_expr env
' rhs
) mb_prs
240 (env
', mb_prs
) = mapAccumL simple_out_bind env
$
241 zipEqual
"simpleOptExpr" bs es
243 -- Note [Getting the map/coerce RULE to work]
245 , [(DEFAULT
, _
, rhs
)] <- as
246 , isCoVarType
(varType b
)
247 , (Var fun
, _args
) <- collectArgs e
248 , fun `hasKey` coercibleSCSelIdKey
249 -- without this last check, we get #11230
253 = Case e
' b
' (substTy subst ty
)
254 (map (go_alt env
') as)
257 (env
', b
') = subst_opt_bndr env b
259 ----------------------
260 go_alt env
(con
, bndrs
, rhs
)
261 = (con
, bndrs
', simple_opt_expr env
' rhs
)
263 (env
', bndrs
') = subst_opt_bndrs env bndrs
265 ----------------------
266 -- go_lam tries eta reduction
267 go_lam env bs
' (Lam b e
)
268 = go_lam env
' (b
':bs
') e
270 (env
', b
') = subst_opt_bndr env b
272 | Just etad_e
<- tryEtaReduce bs e
' = etad_e
273 |
otherwise = mkLams bs e
'
276 e
' = simple_opt_expr env e
278 ----------------------
279 -- simple_app collects arguments for beta reduction
280 simple_app
:: SimpleOptEnv
-> InExpr
-> [SimpleClo
] -> CoreExpr
282 simple_app env
(Var v
) as
283 | Just
(env
', e
) <- lookupVarEnv
(soe_inl env
) v
284 = simple_app
(soeSetInScope env env
') e
as
286 |
let unf
= idUnfolding v
287 , isCompulsoryUnfolding
(idUnfolding v
)
288 , isAlwaysActive
(idInlineActivation v
)
289 -- See Note [Unfold compulsory unfoldings in LHSs]
290 = simple_app
(soeZapSubst env
) (unfoldingTemplate unf
) as
293 , let out_fn
= lookupIdSubst
(text
"simple_app") (soe_subst env
) v
294 = finish_app env out_fn
as
296 simple_app env
(App e1 e2
) as
297 = simple_app env e1
((env
, e2
) : as)
299 simple_app env
(Lam b e
) (a
:as)
300 = wrapLet mb_pr
(simple_app env
' e
as)
302 (env
', mb_pr
) = simple_bind_pair env b Nothing a
304 simple_app env
(Tick t e
) as
305 -- Okay to do "(Tick t e) x ==> Tick t (e x)"?
306 | t `tickishScopesLike` SoftScope
307 = mkTick t
$ simple_app env e
as
310 = finish_app env
(simple_opt_expr env e
) as
312 finish_app
:: SimpleOptEnv
-> OutExpr
-> [SimpleClo
] -> OutExpr
315 finish_app env fun
(arg
:args
)
316 = finish_app env
(App fun
(simple_opt_clo env arg
)) args
318 ----------------------
319 simple_opt_bind
:: SimpleOptEnv
-> InBind
320 -> (SimpleOptEnv
, Maybe OutBind
)
321 simple_opt_bind env
(NonRec b r
)
322 = (env
', case mb_pr
of
324 Just
(b
,r
) -> Just
(NonRec b r
))
326 (b
', r
') = joinPointBinding_maybe b r `orElse`
(b
, r
)
327 (env
', mb_pr
) = simple_bind_pair env b
' Nothing
(env
,r
')
329 simple_opt_bind env
(Rec prs
)
332 res_bind
= Just
(Rec
(reverse rev_prs
'))
333 prs
' = joinPointBindings_maybe prs `orElse` prs
334 (env
', bndrs
') = subst_opt_bndrs env
(map fst prs
')
335 (env
'', rev_prs
') = foldl' do_pr
(env
', []) (prs
' `
zip` bndrs
')
336 do_pr
(env
, prs
) ((b
,r
), b
')
337 = (env
', case mb_pr
of
341 (env
', mb_pr
) = simple_bind_pair env b
(Just b
') (env
,r
)
343 ----------------------
344 simple_bind_pair
:: SimpleOptEnv
345 -> InVar
-> Maybe OutVar
347 -> (SimpleOptEnv
, Maybe (OutVar
, OutExpr
))
348 -- (simple_bind_pair subst in_var out_rhs)
349 -- either extends subst with (in_var -> out_rhs)
350 -- or returns Nothing
351 simple_bind_pair env
@(SOE
{ soe_inl
= inl_env
, soe_subst
= subst
})
352 in_bndr mb_out_bndr clo
@(rhs_env
, in_rhs
)
353 | Type ty
<- in_rhs
-- let a::* = TYPE ty in <body>
354 , let out_ty
= substTy
(soe_subst rhs_env
) ty
355 = ASSERT
( isTyVar in_bndr
)
356 (env
{ soe_subst
= extendTvSubst subst in_bndr out_ty
}, Nothing
)
358 | Coercion co
<- in_rhs
359 , let out_co
= optCoercion
(soe_dflags env
) (getTCvSubst
(soe_subst rhs_env
)) co
360 = ASSERT
( isCoVar in_bndr
)
361 (env
{ soe_subst
= extendCvSubst subst in_bndr out_co
}, Nothing
)
363 | ASSERT2
( isNonCoVarId in_bndr
, ppr in_bndr
)
364 -- The previous two guards got rid of tyvars and coercions
365 -- See Note [CoreSyn type and coercion invariant] in CoreSyn
366 pre_inline_unconditionally
367 = (env
{ soe_inl
= extendVarEnv inl_env in_bndr clo
}, Nothing
)
370 = simple_out_bind_pair env in_bndr mb_out_bndr out_rhs
371 occ active stable_unf
373 stable_unf
= isStableUnfolding
(idUnfolding in_bndr
)
374 active
= isAlwaysActive
(idInlineActivation in_bndr
)
375 occ
= idOccInfo in_bndr
377 out_rhs | Just join_arity
<- isJoinId_maybe in_bndr
378 = simple_join_rhs join_arity
380 = simple_opt_clo env clo
382 simple_join_rhs join_arity
-- See Note [Preserve join-binding arity]
383 = mkLams join_bndrs
' (simple_opt_expr env_body join_body
)
385 env0
= soeSetInScope env rhs_env
386 (join_bndrs
, join_body
) = collectNBinders join_arity in_rhs
387 (env_body
, join_bndrs
') = subst_opt_bndrs env0 join_bndrs
389 pre_inline_unconditionally
:: Bool
390 pre_inline_unconditionally
391 | isExportedId in_bndr
= False
393 |
not active
= False -- Note [Inline prag in simplOpt]
394 |
not (safe_to_inline occ
) = False
397 -- Unconditionally safe to inline
398 safe_to_inline
:: OccInfo
-> Bool
399 safe_to_inline
(IAmALoopBreaker
{}) = False
400 safe_to_inline IAmDead
= True
401 safe_to_inline occ
@(OneOcc
{}) = not (occ_in_lam occ
)
403 safe_to_inline
(ManyOccs
{}) = False
406 simple_out_bind
:: SimpleOptEnv
-> (InVar
, OutExpr
)
407 -> (SimpleOptEnv
, Maybe (OutVar
, OutExpr
))
408 simple_out_bind env
@(SOE
{ soe_subst
= subst
}) (in_bndr
, out_rhs
)
409 | Type out_ty
<- out_rhs
410 = ASSERT
( isTyVar in_bndr
)
411 (env
{ soe_subst
= extendTvSubst subst in_bndr out_ty
}, Nothing
)
413 | Coercion out_co
<- out_rhs
414 = ASSERT
( isCoVar in_bndr
)
415 (env
{ soe_subst
= extendCvSubst subst in_bndr out_co
}, Nothing
)
418 = simple_out_bind_pair env in_bndr Nothing out_rhs
419 (idOccInfo in_bndr
) True False
422 simple_out_bind_pair
:: SimpleOptEnv
423 -> InId
-> Maybe OutId
-> OutExpr
424 -> OccInfo
-> Bool -> Bool
425 -> (SimpleOptEnv
, Maybe (OutVar
, OutExpr
))
426 simple_out_bind_pair env in_bndr mb_out_bndr out_rhs
427 occ_info active stable_unf
428 | ASSERT2
( isNonCoVarId in_bndr
, ppr in_bndr
)
429 -- Type and coercion bindings are caught earlier
430 -- See Note [CoreSyn type and coercion invariant]
431 post_inline_unconditionally
432 = ( env
' { soe_subst
= extendIdSubst
(soe_subst env
) in_bndr out_rhs
}
436 = ( env
', Just
(out_bndr
, out_rhs
) )
438 (env
', bndr1
) = case mb_out_bndr
of
439 Just out_bndr
-> (env
, out_bndr
)
440 Nothing
-> subst_opt_bndr env in_bndr
441 out_bndr
= add_info env
' in_bndr bndr1
443 post_inline_unconditionally
:: Bool
444 post_inline_unconditionally
445 | isExportedId in_bndr
= False -- Note [Exported Ids and trivial RHSs]
446 | stable_unf
= False -- Note [Stable unfoldings and postInlineUnconditionally]
447 |
not active
= False -- in SimplUtils
448 | is_loop_breaker
= False -- If it's a loop-breaker of any kind, don't inline
449 -- because it might be referred to "earlier"
450 | exprIsTrivial out_rhs
= True
451 | coercible_hack
= True
454 is_loop_breaker
= isWeakLoopBreaker occ_info
456 -- See Note [Getting the map/coerce RULE to work]
457 coercible_hack |
(Var fun
, args
) <- collectArgs out_rhs
458 , Just dc
<- isDataConWorkId_maybe fun
459 , dc `hasKey` heqDataConKey || dc `hasKey` coercibleDataConKey
460 = all exprIsTrivial args
464 {- Note [Exported Ids and trivial RHSs]
465 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
466 We obviously do not want to unconditionally inline an Id that is exported.
467 In SimplUtils, Note [Top level and postInlineUnconditionally], we
468 explain why we don't inline /any/ top-level things unconditionally, even
469 trivial ones. But we do here! Why? In the simple optimiser
471 * We do no rule rewrites
472 * We do no call-site inlining
474 Those differences obviate the reasons for not inlining a trivial rhs,
475 and increase the benefit for doing so. So we unconditionally inline trivial
478 Note [Preserve join-binding arity]
479 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
480 Be careful /not/ to eta-reduce the RHS of a join point, lest we lose
481 the join-point arity invariant. Trac #15108 was caused by simplifying
482 the RHS with simple_opt_expr, which does eta-reduction. Solution:
483 simplify the RHS of a join point by simplifying under the lambdas
484 (which of course should be there).
487 ----------------------
488 subst_opt_bndrs
:: SimpleOptEnv
-> [InVar
] -> (SimpleOptEnv
, [OutVar
])
489 subst_opt_bndrs env bndrs
= mapAccumL subst_opt_bndr env bndrs
491 subst_opt_bndr
:: SimpleOptEnv
-> InVar
-> (SimpleOptEnv
, OutVar
)
492 subst_opt_bndr env bndr
493 | isTyVar bndr
= (env
{ soe_subst
= subst_tv
}, tv
')
494 | isCoVar bndr
= (env
{ soe_subst
= subst_cv
}, cv
')
495 |
otherwise = subst_opt_id_bndr env bndr
497 subst
= soe_subst env
498 (subst_tv
, tv
') = substTyVarBndr subst bndr
499 (subst_cv
, cv
') = substCoVarBndr subst bndr
501 subst_opt_id_bndr
:: SimpleOptEnv
-> InId
-> (SimpleOptEnv
, OutId
)
502 -- Nuke all fragile IdInfo, unfolding, and RULES;
503 -- it gets added back later by add_info
504 -- Rather like SimplEnv.substIdBndr
506 -- It's important to zap fragile OccInfo (which CoreSubst.substIdBndr
507 -- carefully does not do) because simplOptExpr invalidates it
509 subst_opt_id_bndr env
@(SOE
{ soe_subst
= subst
, soe_inl
= inl
}) old_id
510 = (env
{ soe_subst
= new_subst
, soe_inl
= new_inl
}, new_id
)
512 Subst in_scope id_subst tv_subst cv_subst
= subst
514 id1
= uniqAway in_scope old_id
515 id2
= setIdType id1
(substTy subst
(idType old_id
))
516 new_id
= zapFragileIdInfo id2
517 -- Zaps rules, unfolding, and fragile OccInfo
518 -- The unfolding and rules will get added back later, by add_info
520 new_in_scope
= in_scope `extendInScopeSet` new_id
522 no_change
= new_id
== old_id
524 -- Extend the substitution if the unique has changed,
525 -- See the notes with substTyVarBndr for the delSubstEnv
527 | no_change
= delVarEnv id_subst old_id
528 |
otherwise = extendVarEnv id_subst old_id
(Var new_id
)
530 new_subst
= Subst new_in_scope new_id_subst tv_subst cv_subst
531 new_inl
= delVarEnv inl old_id
533 ----------------------
534 add_info
:: SimpleOptEnv
-> InVar
-> OutVar
-> OutVar
535 add_info env old_bndr new_bndr
536 | isTyVar old_bndr
= new_bndr
537 |
otherwise = maybeModifyIdInfo mb_new_info new_bndr
539 subst
= soe_subst env
540 mb_new_info
= substIdInfo subst new_bndr
(idInfo old_bndr
)
542 simpleUnfoldingFun
:: IdUnfoldingFun
543 simpleUnfoldingFun
id
544 | isAlwaysActive
(idInlineActivation
id) = idUnfolding
id
545 |
otherwise = noUnfolding
547 wrapLet
:: Maybe (Id
,CoreExpr
) -> CoreExpr
-> CoreExpr
548 wrapLet Nothing body
= body
549 wrapLet
(Just
(b
,r
)) body
= Let
(NonRec b r
) body
552 Note [Inline prag in simplOpt]
553 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
554 If there's an INLINE/NOINLINE pragma that restricts the phase in
555 which the binder can be inlined, we don't inline here; after all,
556 we don't know what phase we're in. Here's an example
558 foo :: Int -> Int -> Int
562 {-# INLINE [1] inner #-}
568 When inlining
'foo
' in 'bar
' we want the
let-binding for
'inner
'
569 to remain visible
until Phase
1
571 Note
[Unfold compulsory unfoldings
in LHSs
]
572 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
573 When the user writes `RULES
map coerce
= coerce`
as a rule
, the rule
574 will only ever match
if simpleOptExpr replaces coerce by its unfolding
575 on the LHS
, because that is the core that the rule matching engine
576 will
find. So
do that for everything that has a compulsory
577 unfolding
. Also see Note
[Desugaring coerce
as cast
] in Desugar
.
579 However
, we don
't want to inline
'seq', which happens to also have a
580 compulsory unfolding
, so we only
do this unfolding only for things
581 that are always
-active
. See Note
[User
-defined RULES for
seq] in MkId
.
583 Note
[Getting the
map/coerce RULE to work
]
584 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
585 We wish to allow the
"map/coerce" RULE to fire
:
587 {-# RULES "map/coerce" map coerce = coerce #-}
589 The naive core produced for this is
591 forall a b
(dict
:: Coercible
* a b
).
592 map @a
@b
(coerce
@a
@b
@dict
) = coerce
@[a
] @[b
] @dict
'
594 where dict
' :: Coercible
[a
] [b
]
597 This matches literal uses
of `
map coerce`
in code
, but that
's
not what we
598 want
. We want it to match
, say
, `
map MkAge`
(where newtype Age
= MkAge
Int)
599 too
. Some
of this is addressed by compulsorily unfolding coerce on the LHS
,
602 forall a b
(dict
:: Coercible
* a b
).
603 map @a
@b
(\(x
:: a
) -> case dict
of
604 MkCoercible
(co
:: a ~R
# b
) -> x |
> co
) = ...
606 Getting better
. But this isn
't exactly what gets produced
. This is because
607 Coercible essentially has ~R
# as a superclass
, and superclasses get eagerly
608 extracted during solving
. So we get this
:
610 forall a b
(dict
:: Coercible
* a b
).
611 case Coercible_SCSel
@* @a
@b dict
of
612 _
[Dead
] -> map @a
@b
(\(x
:: a
) -> case dict
of
613 MkCoercible
(co
:: a ~R
# b
) -> x |
> co
) = ...
615 Unfortunately
, this still abstracts over a Coercible dictionary
. We really
616 want it to abstract over the ~R
# evidence
. So
, we have Desugar
.unfold_coerce
,
617 which transforms the above to
(see also Note
[Desugaring coerce
as cast
] in
620 forall a b
(co
:: a ~R
# b
).
621 let dict
= MkCoercible
@* @a
@b co
in
622 case Coercible_SCSel
@* @a
@b dict
of
623 _
[Dead
] -> map @a
@b
(\(x
:: a
) -> case dict
of
624 MkCoercible
(co
:: a ~R
# b
) -> x |
> co
) = let dict
= ... in ...
626 Now
, we need simpleOptExpr to fix this up
. It does so by taking three
628 1. Inline certain non
-recursive bindings
. The choice whether to inline
629 is made
in simple_bind_pair
. Note the rather specific check for
630 MkCoercible
in there
.
632 2. Stripping
case expressions like the Coercible_SCSel one
.
633 See the `Case`
case of simple_opt_expr
's `go`
function.
635 3. Look for
case expressions that unpack something that was
636 just packed
and inline them
. This is also done
in simple_opt_expr
's
639 This is
all a fair amount
of special
-purpose hackery
, but it
's for
640 a good cause
. And it won
't hurt other RULES
and such that it comes across
.
643 ************************************************************************
647 ************************************************************************
650 -- | Returns Just (bndr,rhs) if the binding is a join point:
651 -- If it's a JoinId, just return it
652 -- If it's not yet a JoinId but is always tail-called,
653 -- make it into a JoinId and return it.
654 -- In the latter case, eta-expand the RHS if necessary, to make the
655 -- lambdas explicit, as is required for join points
657 -- Precondition: the InBndr has been occurrence-analysed,
658 -- so its OccInfo is valid
659 joinPointBinding_maybe
:: InBndr
-> InExpr
-> Maybe (InBndr
, InExpr
)
660 joinPointBinding_maybe bndr rhs
667 | AlwaysTailCalled join_arity
<- tailCallInfo
(idOccInfo bndr
)
668 , (bndrs
, body
) <- etaExpandToJoinPoint join_arity rhs
669 , let str_sig
= idStrictness bndr
670 str_arity
= count isId bndrs
-- Strictness demands are for Ids only
671 join_bndr
= bndr `asJoinId` join_arity
672 `setIdStrictness` etaExpandStrictSig str_arity str_sig
673 = Just
(join_bndr
, mkLams bndrs body
)
678 joinPointBindings_maybe
:: [(InBndr
, InExpr
)] -> Maybe [(InBndr
, InExpr
)]
679 joinPointBindings_maybe bndrs
680 = mapM (uncurry joinPointBinding_maybe
) bndrs
683 {- Note [Strictness and join points]
684 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
687 let f = \x. if x>200 then e1 else e1
689 and we know that f is strict in x. Then if we subsequently
690 discover that f is an arity-2 join point, we'll eta-expand it to
692 let f = \x y. if x>200 then e1 else e1
694 and now it's only strict if applied to two arguments. So we should
695 adjust the strictness info.
697 A more common case is when
701 and again its arity increses (Trac #15517)
704 {- *********************************************************************
708 ************************************************************************
710 Note [exprIsConApp_maybe]
711 ~~~~~~~~~~~~~~~~~~~~~~~~~
712 exprIsConApp_maybe is a very important function. There are two principal
715 * cls_op e, where cls_op is a class operation
717 In both cases you want to know if e is of form (C e1..en) where C is
720 However e might not *look* as if
723 Note [exprIsConApp_maybe on literal strings]
724 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
725 See #9400 and #13317.
727 Conceptually, a string literal "abc" is just ('a':'b':'c':[]), but in Core
728 they are represented as unpackCString# "abc"# by MkCore.mkStringExprFS, or
729 unpackCStringUtf8# when the literal contains multi-byte UTF8 characters.
731 For optimizations we want to be able to treat it as a list, so they can be
732 decomposed when used in a case-statement. exprIsConApp_maybe detects those
733 calls to unpackCString# and returns:
735 Just (':', [Char], ['a', unpackCString# "bc"]).
737 We need to be careful about UTF8 strings here. ""# contains a ByteString, so
738 we must parse it back into a FastString to split off the first character.
739 That way we can treat unpackCString# and unpackCStringUtf8# in the same way.
741 We must also be caeful about
743 ...(unpackCString# lvl)...
744 to ensure that we see through the let-binding for 'lvl'. Hence the
745 (exprIsLiteral_maybe .. arg) in the guard before the call to
746 dealWithStringLiteral.
748 Note [Push coercions in exprIsConApp_maybe]
749 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
750 In Trac #13025 I found a case where we had
751 op (df @t1 @t2) -- op is a ClassOp
753 df = (/\a b. K e1 e2) |> g
755 To get this to come out we need to simplify on the fly
756 ((/\a b. K e1 e2) |> g) @t1 @t2
758 Hence the use of pushCoArgs.
761 data ConCont
= CC
[CoreExpr
] Coercion
762 -- Substitution already applied
764 -- | Returns @Just (dc, [t1..tk], [x1..xn])@ if the argument expression is
765 -- a *saturated* constructor application of the form @dc t1..tk x1 .. xn@,
766 -- where t1..tk are the *universally-quantified* type args of 'dc'
767 exprIsConApp_maybe
:: InScopeEnv
-> CoreExpr
-> Maybe (DataCon
, [Type
], [CoreExpr
])
768 exprIsConApp_maybe
(in_scope
, id_unf
) expr
769 = go
(Left in_scope
) expr
(CC
[] (mkRepReflCo
(exprType expr
)))
771 go
:: Either InScopeSet Subst
772 -- Left in-scope means "empty substitution"
773 -- Right subst means "apply this substitution to the CoreExpr"
774 -> CoreExpr
-> ConCont
775 -> Maybe (DataCon
, [Type
], [CoreExpr
])
776 go subst
(Tick t expr
) cont
777 |
not (tickishIsCode t
) = go subst expr cont
778 go subst
(Cast expr co1
) (CC args co2
)
779 | Just
(args
', m_co1
') <- pushCoArgs
(subst_co subst co1
) args
780 -- See Note [Push coercions in exprIsConApp_maybe]
782 MCo co1
' -> go subst expr
(CC args
' (co1
' `mkTransCo` co2
))
783 MRefl
-> go subst expr
(CC args
' co2
)
784 go subst
(App fun arg
) (CC args co
)
785 = go subst fun
(CC
(subst_arg subst arg
: args
) co
)
786 go subst
(Lam var body
) (CC
(arg
:args
) co
)
787 | exprIsTrivial arg
-- Don't duplicate stuff!
788 = go
(extend subst var arg
) body
(CC args co
)
789 go
(Right sub
) (Var v
) cont
790 = go
(Left
(substInScope sub
))
791 (lookupIdSubst
(text
"exprIsConApp" <+> ppr expr
) sub v
)
794 go
(Left in_scope
) (Var fun
) cont
@(CC args co
)
796 | Just con
<- isDataConWorkId_maybe fun
797 , count isValArg args
== idArity fun
798 = pushCoDataCon con args co
800 -- Look through dictionary functions; see Note [Unfolding DFuns]
801 | DFunUnfolding
{ df_bndrs
= bndrs
, df_con
= con
, df_args
= dfun_args
} <- unfolding
802 , bndrs `equalLength` args
-- See Note [DFun arity check]
803 , let subst
= mkOpenSubst in_scope
(bndrs `
zip` args
)
804 = pushCoDataCon con
(map (substExpr
(text
"exprIsConApp1") subst
) dfun_args
) co
806 -- Look through unfoldings, but only arity-zero one;
807 -- if arity > 0 we are effectively inlining a function call,
808 -- and that is the business of callSiteInline.
809 -- In practice, without this test, most of the "hits" were
810 -- CPR'd workers getting inlined back into their wrappers,
812 , Just rhs
<- expandUnfolding_maybe unfolding
813 , let in_scope
' = extendInScopeSetSet in_scope
(exprFreeVars rhs
)
814 = go
(Left in_scope
') rhs cont
816 -- See Note [exprIsConApp_maybe on literal strings]
817 |
(fun `hasKey` unpackCStringIdKey
) ||
818 (fun `hasKey` unpackCStringUtf8IdKey
)
820 , Just
(LitString str
) <- exprIsLiteral_maybe
(in_scope
, id_unf
) arg
821 = dealWithStringLiteral fun str co
823 unfolding
= id_unf fun
827 ----------------------------
828 -- Operations on the (Either InScopeSet CoreSubst)
829 -- The Left case is wildly dominant
830 subst_co
(Left
{}) co
= co
831 subst_co
(Right s
) co
= CoreSubst
.substCo s co
833 subst_arg
(Left
{}) e
= e
834 subst_arg
(Right s
) e
= substExpr
(text
"exprIsConApp2") s e
836 extend
(Left in_scope
) v e
= Right
(extendSubst
(mkEmptySubst in_scope
) v e
)
837 extend
(Right s
) v e
= Right
(extendSubst s v e
)
840 -- See Note [exprIsConApp_maybe on literal strings]
841 dealWithStringLiteral
:: Var
-> BS
.ByteString
-> Coercion
842 -> Maybe (DataCon
, [Type
], [CoreExpr
])
844 -- This is not possible with user-supplied empty literals, MkCore.mkStringExprFS
845 -- turns those into [] automatically, but just in case something else in GHC
846 -- generates a string literal directly.
847 dealWithStringLiteral _ str co
849 = pushCoDataCon nilDataCon
[Type charTy
] co
851 dealWithStringLiteral fun str co
852 = let strFS
= mkFastStringByteString str
854 char
= mkConApp charDataCon
[mkCharLit
(headFS strFS
)]
855 charTail
= fastStringToByteString
(tailFS strFS
)
857 -- In singleton strings, just add [] instead of unpackCstring# ""#.
858 rest
= if BS
.null charTail
859 then mkConApp nilDataCon
[Type charTy
]
861 (Lit
(LitString charTail
))
863 in pushCoDataCon consDataCon
[Type charTy
, char
, rest
] co
866 Note [Unfolding DFuns]
867 ~~~~~~~~~~~~~~~~~~~~~~
870 df :: forall a b. (Eq a, Eq b) -> Eq (a,b)
871 df a b d_a d_b = MkEqD (a,b) ($c1 a b d_a d_b)
874 So to split it up we just need to apply the ops $c1, $c2 etc
875 to the very same args as the dfun. It takes a little more work
876 to compute the type arguments to the dictionary constructor.
878 Note [DFun arity check]
879 ~~~~~~~~~~~~~~~~~~~~~~~
880 Here we check that the total number of supplied arguments (inclding
881 type args) matches what the dfun is expecting. This may be *less*
882 than the ordinary arity of the dfun: see Note [DFun unfoldings] in CoreSyn
885 exprIsLiteral_maybe
:: InScopeEnv
-> CoreExpr
-> Maybe Literal
886 -- Same deal as exprIsConApp_maybe, but much simpler
887 -- Nevertheless we do need to look through unfoldings for
888 -- Integer and string literals, which are vigorously hoisted to top level
889 -- and not subsequently inlined
890 exprIsLiteral_maybe env
@(_
, id_unf
) e
893 Tick _ e
' -> exprIsLiteral_maybe env e
' -- dubious?
894 Var v | Just rhs
<- expandUnfolding_maybe
(id_unf v
)
895 -> exprIsLiteral_maybe env rhs
899 Note [exprIsLambda_maybe]
900 ~~~~~~~~~~~~~~~~~~~~~~~~~~
901 exprIsLambda_maybe will, given an expression `e`, try to turn it into the form
902 `Lam v e'` (returned as `Just (v,e')`). Besides using lambdas, it looks through
903 casts (using the Push rule), and it unfolds function calls if the unfolding
904 has a greater arity than arguments are present.
906 Currently, it is used in Rules.match, and is required to make
907 "map coerce = coerce" match.
910 exprIsLambda_maybe
:: InScopeEnv
-> CoreExpr
911 -> Maybe (Var
, CoreExpr
,[Tickish Id
])
912 -- See Note [exprIsLambda_maybe]
914 -- The simple case: It is a lambda already
915 exprIsLambda_maybe _
(Lam x e
)
918 -- Still straightforward: Ticks that we can float out of the way
919 exprIsLambda_maybe
(in_scope_set
, id_unf
) (Tick t e
)
921 , Just
(x
, e
, ts
) <- exprIsLambda_maybe
(in_scope_set
, id_unf
) e
924 -- Also possible: A casted lambda. Push the coercion inside
925 exprIsLambda_maybe
(in_scope_set
, id_unf
) (Cast casted_e co
)
926 | Just
(x
, e
,ts
) <- exprIsLambda_maybe
(in_scope_set
, id_unf
) casted_e
927 -- Only do value lambdas.
928 -- this implies that x is not in scope in gamma (makes this code simpler)
929 , not (isTyVar x
) && not (isCoVar x
)
930 , ASSERT
( not $ x `elemVarSet` tyCoVarsOfCo co
) True
931 , Just
(x
',e
') <- pushCoercionIntoLambda in_scope_set x e co
932 , let res
= Just
(x
',e
',ts
)
933 = --pprTrace "exprIsLambda_maybe:Cast" (vcat [ppr casted_e,ppr co,ppr res)])
936 -- Another attempt: See if we find a partial unfolding
937 exprIsLambda_maybe
(in_scope_set
, id_unf
) e
938 |
(Var f
, as, ts
) <- collectArgsTicks tickishFloatable e
939 , idArity f
> count isValArg
as
940 -- Make sure there is hope to get a lambda
941 , Just rhs
<- expandUnfolding_maybe
(id_unf f
)
942 -- Optimize, for beta-reduction
943 , let e
' = simpleOptExprWith unsafeGlobalDynFlags
(mkEmptySubst in_scope_set
) (rhs `mkApps`
as)
944 -- Recurse, because of possible casts
945 , Just
(x
', e
'', ts
') <- exprIsLambda_maybe
(in_scope_set
, id_unf
) e
'
946 , let res
= Just
(x
', e
'', ts
++ts
')
947 = -- pprTrace "exprIsLambda_maybe:Unfold" (vcat [ppr e, ppr (x',e'')])
950 exprIsLambda_maybe _ _e
951 = -- pprTrace "exprIsLambda_maybe:Fail" (vcat [ppr _e])
955 {- *********************************************************************
959 ************************************************************************
961 Here we implement the "push rules" from FC papers:
963 * The push-argument rules, where we can move a coercion past an argument.
966 and we want to transform it to
968 for some suitable co' and tranformed arg'.
970 * The PushK rule for data constructors. We have
972 and we want to tranform to
974 by pushing the coercion into the arguments
977 pushCoArgs
:: CoercionR
-> [CoreArg
] -> Maybe ([CoreArg
], MCoercion
)
978 pushCoArgs co
[] = return ([], MCo co
)
979 pushCoArgs co
(arg
:args
) = do { (arg
', m_co1
) <- pushCoArg co arg
981 MCo co1
-> do { (args
', m_co2
) <- pushCoArgs co1 args
982 ; return (arg
':args
', m_co2
) }
983 MRefl
-> return (arg
':args
, MRefl
) }
985 pushCoArg
:: CoercionR
-> CoreArg
-> Maybe (CoreArg
, MCoercion
)
986 -- We have (fun |> co) arg, and we want to transform it to
988 -- This may fail, e.g. if (fun :: N) where N is a newtype
989 -- C.f. simplCast in Simplify.hs
990 -- 'co' is always Representational
991 -- If the returned coercion is Nothing, then it would have been reflexive
992 pushCoArg co
(Type ty
) = do { (ty
', m_co
') <- pushCoTyArg co ty
993 ; return (Type ty
', m_co
') }
994 pushCoArg co val_arg
= do { (arg_co
, m_co
') <- pushCoValArg co
995 ; return (val_arg `mkCast` arg_co
, m_co
') }
997 pushCoTyArg
:: CoercionR
-> Type
-> Maybe (Type
, MCoercionR
)
998 -- We have (fun |> co) @ty
999 -- Push the coercion through to return
1000 -- (fun @ty') |> co'
1001 -- 'co' is always Representational
1002 -- If the returned coercion is Nothing, then it would have been reflexive;
1003 -- it's faster not to compute it, though.
1005 -- The following is inefficient - don't do `eqType` here, the coercion
1006 -- optimizer will take care of it. See Trac #14737.
1007 -- -- | tyL `eqType` tyR
1008 -- -- = Just (ty, Nothing)
1014 = ASSERT2
( isForAllTy_ty tyR
, ppr co
$$ ppr ty
)
1015 Just
(ty `mkCastTy` co1
, MCo co2
)
1020 Pair tyL tyR
= coercionKind co
1022 -- tyL = forall (a1 :: k1). ty1
1023 -- tyR = forall (a2 :: k2). ty2
1025 co1
= mkSymCo
(mkNthCo Nominal
0 co
)
1027 -- Note that NthCo can extract a Nominal equality between the
1028 -- kinds of the types related by a coercion between forall-types.
1029 -- See the NthCo case in CoreLint.
1031 co2
= mkInstCo co
(mkGReflLeftCo Nominal ty co1
)
1032 -- co2 :: ty1[ (ty|>co1)/a1 ] ~ ty2[ ty/a2 ]
1033 -- Arg of mkInstCo is always nominal, hence mkNomReflCo
1035 pushCoValArg
:: CoercionR
-> Maybe (Coercion
, MCoercion
)
1036 -- We have (fun |> co) arg
1037 -- Push the coercion through to return
1038 -- (fun (arg |> co_arg)) |> co_res
1039 -- 'co' is always Representational
1040 -- If the second returned Coercion is actually Nothing, then no cast is necessary;
1041 -- the returned coercion would have been reflexive.
1043 -- The following is inefficient - don't do `eqType` here, the coercion
1044 -- optimizer will take care of it. See Trac #14737.
1045 -- -- | tyL `eqType` tyR
1046 -- -- = Just (mkRepReflCo arg, Nothing)
1049 = Just
(mkRepReflCo arg
, MRefl
)
1052 , (co1
, co2
) <- decomposeFunCo Representational co
1053 -- If co :: (tyL1 -> tyL2) ~ (tyR1 -> tyR2)
1054 -- then co1 :: tyL1 ~ tyR1
1055 -- co2 :: tyL2 ~ tyR2
1056 = ASSERT2
( isFunTy tyR
, ppr co
$$ ppr arg
)
1057 Just
(mkSymCo co1
, MCo co2
)
1063 Pair tyL tyR
= coercionKind co
1065 pushCoercionIntoLambda
1066 :: InScopeSet
-> Var
-> CoreExpr
-> CoercionR
-> Maybe (Var
, CoreExpr
)
1067 -- This implements the Push rule from the paper on coercions
1071 pushCoercionIntoLambda in_scope x e co
1072 | ASSERT
(not (isTyVar x
) && not (isCoVar x
)) True
1073 , Pair s1s2 t1t2
<- coercionKind co
1074 , Just
(_s1
,_s2
) <- splitFunTy_maybe s1s2
1075 , Just
(t1
,_t2
) <- splitFunTy_maybe t1t2
1076 = let (co1
, co2
) = decomposeFunCo Representational co
1077 -- Should we optimize the coercions here?
1078 -- Otherwise they might not match too well
1079 x
' = x `setIdType` t1
1080 in_scope
' = in_scope `extendInScopeSet` x
'
1081 subst
= extendIdSubst
(mkEmptySubst in_scope
')
1083 (mkCast
(Var x
') co1
)
1084 in Just
(x
', substExpr
(text
"pushCoercionIntoLambda") subst e `mkCast` co2
)
1086 = pprTrace
"exprIsLambda_maybe: Unexpected lambda in case" (ppr
(Lam x e
))
1089 pushCoDataCon
:: DataCon
-> [CoreExpr
] -> Coercion
1091 , [Type
] -- Universal type args
1092 , [CoreExpr
]) -- All other args incl existentials
1093 -- Implement the KPush reduction rule as described in "Down with kinds"
1094 -- The transformation applies iff we have
1095 -- (C e1 ... en) `cast` co
1096 -- where co :: (T t1 .. tn) ~ to_ty
1097 -- The left-hand one must be a T, because exprIsConApp returned True
1098 -- but the right-hand one might not be. (Though it usually will.)
1099 pushCoDataCon dc dc_args co
1100 | isReflCo co || from_ty `eqType` to_ty
-- try cheap test first
1101 , let (univ_ty_args
, rest_args
) = splitAtList
(dataConUnivTyVars dc
) dc_args
1102 = Just
(dc
, map exprToType univ_ty_args
, rest_args
)
1104 | Just
(to_tc
, to_tc_arg_tys
) <- splitTyConApp_maybe to_ty
1105 , to_tc
== dataConTyCon dc
1106 -- These two tests can fail; we might see
1107 -- (C x y) `cast` (g :: T a ~ S [a]),
1108 -- where S is a type function. In fact, exprIsConApp
1109 -- will probably not be called in such circumstances,
1110 -- but there's nothing wrong with it
1113 tc_arity
= tyConArity to_tc
1114 dc_univ_tyvars
= dataConUnivTyVars dc
1115 dc_ex_tcvars
= dataConExTyCoVars dc
1116 arg_tys
= dataConRepArgTys dc
1118 non_univ_args
= dropList dc_univ_tyvars dc_args
1119 (ex_args
, val_args
) = splitAtList dc_ex_tcvars non_univ_args
1121 -- Make the "Psi" from the paper
1122 omegas
= decomposeCo tc_arity co
(tyConRolesRepresentational to_tc
)
1123 (psi_subst
, to_ex_arg_tys
)
1124 = liftCoSubstWithEx Representational
1128 (map exprToType ex_args
)
1130 -- Cast the value arguments (which include dictionaries)
1131 new_val_args
= zipWith cast_arg arg_tys val_args
1132 cast_arg arg_ty arg
= mkCast arg
(psi_subst arg_ty
)
1134 to_ex_args
= map Type to_ex_arg_tys
1136 dump_doc
= vcat
[ppr dc
, ppr dc_univ_tyvars
, ppr dc_ex_tcvars
,
1137 ppr arg_tys
, ppr dc_args
,
1138 ppr ex_args
, ppr val_args
, ppr co
, ppr from_ty
, ppr to_ty
, ppr to_tc
]
1140 ASSERT2
( eqType from_ty
(mkTyConApp to_tc
(map exprToType
$ takeList dc_univ_tyvars dc_args
)), dump_doc
)
1141 ASSERT2
( equalLength val_args arg_tys
, dump_doc
)
1142 Just
(dc
, to_tc_arg_tys
, to_ex_args
++ new_val_args
)
1148 Pair from_ty to_ty
= coercionKind co
1150 collectBindersPushingCo
:: CoreExpr
-> ([Var
], CoreExpr
)
1151 -- Collect lambda binders, pushing coercions inside if possible
1152 -- E.g. (\x.e) |> g g :: <Int> -> blah
1153 -- = (\x. e |> Nth 1 g)
1157 -- collectBindersPushingCo ((\x.e) |> g) === ([x], e |> Nth 1 g)
1158 collectBindersPushingCo e
1161 -- Peel off lambdas until we hit a cast.
1162 go
:: [Var
] -> CoreExpr
-> ([Var
], CoreExpr
)
1163 -- The accumulator is in reverse order
1164 go bs
(Lam b e
) = go
(b
:bs
) e
1165 go bs
(Cast e co
) = go_c bs e co
1166 go bs e
= (reverse bs
, e
)
1168 -- We are in a cast; peel off casts until we hit a lambda.
1169 go_c
:: [Var
] -> CoreExpr
-> CoercionR
-> ([Var
], CoreExpr
)
1170 -- (go_c bs e c) is same as (go bs e (e |> c))
1171 go_c bs
(Cast e co1
) co2
= go_c bs e
(co1 `mkTransCo` co2
)
1172 go_c bs
(Lam b e
) co
= go_lam bs b e co
1173 go_c bs e co
= (reverse bs
, mkCast e co
)
1175 -- We are in a lambda under a cast; peel off lambdas and build a
1176 -- new coercion for the body.
1177 go_lam
:: [Var
] -> Var
-> CoreExpr
-> CoercionR
-> ([Var
], CoreExpr
)
1178 -- (go_lam bs b e c) is same as (go_c bs (\b.e) c)
1181 , let Pair tyL tyR
= coercionKind co
1182 , ASSERT
( isForAllTy_ty tyL
)
1184 , isReflCo
(mkNthCo Nominal
0 co
) -- See Note [collectBindersPushingCo]
1185 = go_c
(b
:bs
) e
(mkInstCo co
(mkNomReflCo
(mkTyVarTy b
)))
1188 , let Pair tyL tyR
= coercionKind co
1189 , ASSERT
( isForAllTy_co tyL
)
1191 , isReflCo
(mkNthCo Nominal
0 co
) -- See Note [collectBindersPushingCo]
1192 , let cov
= mkCoVarCo b
1193 = go_c
(b
:bs
) e
(mkInstCo co
(mkNomReflCo
(mkCoercionTy cov
)))
1196 , let Pair tyL tyR
= coercionKind co
1197 , ASSERT
( isFunTy tyL
) isFunTy tyR
1198 , (co_arg
, co_res
) <- decomposeFunCo Representational co
1199 , isReflCo co_arg
-- See Note [collectBindersPushingCo]
1200 = go_c
(b
:bs
) e co_res
1202 |
otherwise = (reverse bs
, mkCast
(Lam b e
) co
)
1204 {- Note [collectBindersPushingCo]
1205 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1206 We just look for coercions of form
1208 (and similarly for foralls) to keep this function simple. We could do
1209 more elaborate stuff, but it'd involve substitution etc.