No join-point from an INLINE function with wrong arity
[ghc.git] / compiler / coreSyn / CoreOpt.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 -}
5
6 {-# LANGUAGE CPP #-}
7 module CoreOpt (
8 -- ** Simple expression optimiser
9 simpleOptPgm, simpleOptExpr, simpleOptExprWith,
10
11 -- ** Join points
12 joinPointBinding_maybe, joinPointBindings_maybe,
13
14 -- ** Predicates on expressions
15 exprIsConApp_maybe, exprIsLiteral_maybe, exprIsLambda_maybe,
16
17 -- ** Coercions and casts
18 pushCoArg, pushCoValArg, pushCoTyArg, collectBindersPushingCo
19 ) where
20
21 #include "HsVersions.h"
22
23 import CoreArity( joinRhsArity, etaExpandToJoinPoint )
24
25 import CoreSyn
26 import CoreSubst
27 import CoreUtils
28 import CoreFVs
29 import PprCore ( pprCoreBindings, pprRules )
30 import OccurAnal( occurAnalyseExpr, occurAnalysePgm )
31 import Literal ( Literal(MachStr) )
32 import Id
33 import Var ( varType )
34 import VarSet
35 import VarEnv
36 import DataCon
37 import OptCoercion ( optCoercion )
38 import Type hiding ( substTy, extendTvSubst, extendCvSubst, extendTvSubstList
39 , isInScope, substTyVarBndr, cloneTyVarBndr )
40 import Coercion hiding ( substCo, substCoVarBndr )
41 import TyCon ( tyConArity )
42 import TysWiredIn
43 import PrelNames
44 import BasicTypes
45 import Module ( Module )
46 import ErrUtils
47 import DynFlags
48 import Outputable
49 import Pair
50 import Util
51 import Maybes ( orElse )
52 import FastString
53 import Data.List
54 import qualified Data.ByteString as BS
55
56 {-
57 ************************************************************************
58 * *
59 The Simple Optimiser
60 * *
61 ************************************************************************
62
63 Note [The simple optimiser]
64 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
65 The simple optimiser is a lightweight, pure (non-monadic) function
66 that rapidly does a lot of simple optimisations, including
67
68 - inlining things that occur just once,
69 or whose RHS turns out to be trivial
70 - beta reduction
71 - case of known constructor
72 - dead code elimination
73
74 It does NOT do any call-site inlining; it only inlines a function if
75 it can do so unconditionally, dropping the binding. It thereby
76 guarantees to leave no un-reduced beta-redexes.
77
78 It is careful to follow the guidance of "Secrets of the GHC inliner",
79 and in particular the pre-inline-unconditionally and
80 post-inline-unconditionally story, to do effective beta reduction on
81 functions called precisely once, without repeatedly optimising the same
82 expression. In fact, the simple optimiser is a good example of this
83 little dance in action; the full Simplifier is a lot more complicated.
84
85 -}
86
87 simpleOptExpr :: CoreExpr -> CoreExpr
88 -- See Note [The simple optimiser]
89 -- Do simple optimisation on an expression
90 -- The optimisation is very straightforward: just
91 -- inline non-recursive bindings that are used only once,
92 -- or where the RHS is trivial
93 --
94 -- We also inline bindings that bind a Eq# box: see
95 -- See Note [Getting the map/coerce RULE to work].
96 --
97 -- Also we convert functions to join points where possible (as
98 -- the occurrence analyser does most of the work anyway).
99 --
100 -- The result is NOT guaranteed occurrence-analysed, because
101 -- in (let x = y in ....) we substitute for x; so y's occ-info
102 -- may change radically
103
104 simpleOptExpr expr
105 = -- pprTrace "simpleOptExpr" (ppr init_subst $$ ppr expr)
106 simpleOptExprWith init_subst expr
107 where
108 init_subst = mkEmptySubst (mkInScopeSet (exprFreeVars expr))
109 -- It's potentially important to make a proper in-scope set
110 -- Consider let x = ..y.. in \y. ...x...
111 -- Then we should remember to clone y before substituting
112 -- for x. It's very unlikely to occur, because we probably
113 -- won't *be* substituting for x if it occurs inside a
114 -- lambda.
115 --
116 -- It's a bit painful to call exprFreeVars, because it makes
117 -- three passes instead of two (occ-anal, and go)
118
119 simpleOptExprWith :: Subst -> InExpr -> OutExpr
120 -- See Note [The simple optimiser]
121 simpleOptExprWith subst expr
122 = simple_opt_expr init_env (occurAnalyseExpr expr)
123 where
124 init_env = SOE { soe_inl = emptyVarEnv, soe_subst = subst }
125
126 ----------------------
127 simpleOptPgm :: DynFlags -> Module
128 -> CoreProgram -> [CoreRule] -> [CoreVect]
129 -> IO (CoreProgram, [CoreRule], [CoreVect])
130 -- See Note [The simple optimiser]
131 simpleOptPgm dflags this_mod binds rules vects
132 = do { dumpIfSet_dyn dflags Opt_D_dump_occur_anal "Occurrence analysis"
133 (pprCoreBindings occ_anald_binds $$ pprRules rules );
134
135 ; return (reverse binds', rules', vects') }
136 where
137 occ_anald_binds = occurAnalysePgm this_mod (\_ -> False) {- No rules active -}
138 rules vects emptyVarSet binds
139
140 (final_env, binds') = foldl do_one (emptyEnv, []) occ_anald_binds
141 final_subst = soe_subst final_env
142
143 rules' = substRulesForImportedIds final_subst rules
144 vects' = substVects final_subst vects
145 -- We never unconditionally inline into rules,
146 -- hence pasing just a substitution
147
148 do_one (env, binds') bind
149 = case simple_opt_bind env bind of
150 (env', Nothing) -> (env', binds')
151 (env', Just bind') -> (env', bind':binds')
152
153 -- In these functions the substitution maps InVar -> OutExpr
154
155 ----------------------
156 type SimpleClo = (SimpleOptEnv, InExpr)
157
158 data SimpleOptEnv
159 = SOE { soe_inl :: IdEnv SimpleClo
160 -- Deals with preInlineUnconditionally; things
161 -- that occur exactly once and are inlined
162 -- without having first been simplified
163
164 , soe_subst :: Subst
165 -- Deals with cloning; includes the InScopeSet
166 }
167
168 instance Outputable SimpleOptEnv where
169 ppr (SOE { soe_inl = inl, soe_subst = subst })
170 = text "SOE {" <+> vcat [ text "soe_inl =" <+> ppr inl
171 , text "soe_subst =" <+> ppr subst ]
172 <+> text "}"
173
174 emptyEnv :: SimpleOptEnv
175 emptyEnv = SOE { soe_inl = emptyVarEnv
176 , soe_subst = emptySubst }
177
178 soeZapSubst :: SimpleOptEnv -> SimpleOptEnv
179 soeZapSubst (SOE { soe_subst = subst })
180 = SOE { soe_inl = emptyVarEnv, soe_subst = zapSubstEnv subst }
181
182 soeSetInScope :: SimpleOptEnv -> SimpleOptEnv -> SimpleOptEnv
183 -- Take in-scope set from env1, and the rest from env2
184 soeSetInScope (SOE { soe_subst = subst1 })
185 env2@(SOE { soe_subst = subst2 })
186 = env2 { soe_subst = setInScope subst2 (substInScope subst1) }
187
188 ---------------
189 simple_opt_clo :: SimpleOptEnv -> SimpleClo -> OutExpr
190 simple_opt_clo env (e_env, e)
191 = simple_opt_expr (soeSetInScope env e_env) e
192
193 simple_opt_expr :: SimpleOptEnv -> InExpr -> OutExpr
194 simple_opt_expr env expr
195 = go expr
196 where
197 subst = soe_subst env
198 in_scope = substInScope subst
199 in_scope_env = (in_scope, simpleUnfoldingFun)
200
201 go (Var v)
202 | Just clo <- lookupVarEnv (soe_inl env) v
203 = simple_opt_clo env clo
204 | otherwise
205 = lookupIdSubst (text "simpleOptExpr") (soe_subst env) v
206
207 go (App e1 e2) = simple_app env e1 [(env,e2)]
208 go (Type ty) = Type (substTy subst ty)
209 go (Coercion co) = Coercion (optCoercion (getTCvSubst subst) co)
210 go (Lit lit) = Lit lit
211 go (Tick tickish e) = mkTick (substTickish subst tickish) (go e)
212 go (Cast e co) | isReflCo co' = go e
213 | otherwise = Cast (go e) co'
214 where
215 co' = optCoercion (getTCvSubst subst) co
216
217 go (Let bind body) = case simple_opt_bind env bind of
218 (env', Nothing) -> simple_opt_expr env' body
219 (env', Just bind) -> Let bind (simple_opt_expr env' body)
220
221 go lam@(Lam {}) = go_lam env [] lam
222 go (Case e b ty as)
223 -- See Note [Getting the map/coerce RULE to work]
224 | isDeadBinder b
225 , Just (con, _tys, es) <- exprIsConApp_maybe in_scope_env e'
226 , Just (altcon, bs, rhs) <- findAlt (DataAlt con) as
227 = case altcon of
228 DEFAULT -> go rhs
229 _ -> foldr wrapLet (simple_opt_expr env' rhs) mb_prs
230 where
231 (env', mb_prs) = mapAccumL simple_out_bind env $
232 zipEqual "simpleOptExpr" bs es
233
234 -- Note [Getting the map/coerce RULE to work]
235 | isDeadBinder b
236 , [(DEFAULT, _, rhs)] <- as
237 , isCoercionType (varType b)
238 , (Var fun, _args) <- collectArgs e
239 , fun `hasKey` coercibleSCSelIdKey
240 -- without this last check, we get #11230
241 = go rhs
242
243 | otherwise
244 = Case e' b' (substTy subst ty)
245 (map (go_alt env') as)
246 where
247 e' = go e
248 (env', b') = subst_opt_bndr env b
249
250 ----------------------
251 go_alt env (con, bndrs, rhs)
252 = (con, bndrs', simple_opt_expr env' rhs)
253 where
254 (env', bndrs') = subst_opt_bndrs env bndrs
255
256 ----------------------
257 -- go_lam tries eta reduction
258 go_lam env bs' (Lam b e)
259 = go_lam env' (b':bs') e
260 where
261 (env', b') = subst_opt_bndr env b
262 go_lam env bs' e
263 | Just etad_e <- tryEtaReduce bs e' = etad_e
264 | otherwise = mkLams bs e'
265 where
266 bs = reverse bs'
267 e' = simple_opt_expr env e
268
269 ----------------------
270 -- simple_app collects arguments for beta reduction
271 simple_app :: SimpleOptEnv -> InExpr -> [SimpleClo] -> CoreExpr
272
273 simple_app env (Var v) as
274 | Just (env', e) <- lookupVarEnv (soe_inl env) v
275 = simple_app (soeSetInScope env env') e as
276
277 | let unf = idUnfolding v
278 , isCompulsoryUnfolding (idUnfolding v)
279 , isAlwaysActive (idInlineActivation v)
280 -- See Note [Unfold compulsory unfoldings in LHSs]
281 = simple_app (soeZapSubst env) (unfoldingTemplate unf) as
282
283 | otherwise
284 , let out_fn = lookupIdSubst (text "simple_app") (soe_subst env) v
285 = finish_app env out_fn as
286
287 simple_app env (App e1 e2) as
288 = simple_app env e1 ((env, e2) : as)
289
290 simple_app env (Lam b e) (a:as)
291 = wrapLet mb_pr (simple_app env' e as)
292 where
293 (env', mb_pr) = simple_bind_pair env b Nothing a
294
295 simple_app env (Tick t e) as
296 -- Okay to do "(Tick t e) x ==> Tick t (e x)"?
297 | t `tickishScopesLike` SoftScope
298 = mkTick t $ simple_app env e as
299
300 simple_app env e as
301 = finish_app env (simple_opt_expr env e) as
302
303 finish_app :: SimpleOptEnv -> OutExpr -> [SimpleClo] -> OutExpr
304 finish_app _ fun []
305 = fun
306 finish_app env fun (arg:args)
307 = finish_app env (App fun (simple_opt_clo env arg)) args
308
309 ----------------------
310 simple_opt_bind :: SimpleOptEnv -> InBind
311 -> (SimpleOptEnv, Maybe OutBind)
312 simple_opt_bind env (NonRec b r)
313 = (env', case mb_pr of
314 Nothing -> Nothing
315 Just (b,r) -> Just (NonRec b r))
316 where
317 (b', r') = joinPointBinding_maybe b r `orElse` (b, r)
318 (env', mb_pr) = simple_bind_pair env b' Nothing (env,r')
319
320 simple_opt_bind env (Rec prs)
321 = (env'', res_bind)
322 where
323 res_bind = Just (Rec (reverse rev_prs'))
324 prs' = joinPointBindings_maybe prs `orElse` prs
325 (env', bndrs') = subst_opt_bndrs env (map fst prs')
326 (env'', rev_prs') = foldl do_pr (env', []) (prs' `zip` bndrs')
327 do_pr (env, prs) ((b,r), b')
328 = (env', case mb_pr of
329 Just pr -> pr : prs
330 Nothing -> prs)
331 where
332 (env', mb_pr) = simple_bind_pair env b (Just b') (env,r)
333
334 ----------------------
335 simple_bind_pair :: SimpleOptEnv
336 -> InVar -> Maybe OutVar
337 -> SimpleClo
338 -> (SimpleOptEnv, Maybe (OutVar, OutExpr))
339 -- (simple_bind_pair subst in_var out_rhs)
340 -- either extends subst with (in_var -> out_rhs)
341 -- or returns Nothing
342 simple_bind_pair env@(SOE { soe_inl = inl_env, soe_subst = subst })
343 in_bndr mb_out_bndr clo@(rhs_env, in_rhs)
344 | Type ty <- in_rhs -- let a::* = TYPE ty in <body>
345 , let out_ty = substTy (soe_subst rhs_env) ty
346 = ASSERT( isTyVar in_bndr )
347 (env { soe_subst = extendTvSubst subst in_bndr out_ty }, Nothing)
348
349 | Coercion co <- in_rhs
350 , let out_co = optCoercion (getTCvSubst (soe_subst rhs_env)) co
351 = ASSERT( isCoVar in_bndr )
352 (env { soe_subst = extendCvSubst subst in_bndr out_co }, Nothing)
353
354 | pre_inline_unconditionally
355 = (env { soe_inl = extendVarEnv inl_env in_bndr clo }, Nothing)
356
357 | otherwise
358 = simple_out_bind_pair env in_bndr mb_out_bndr
359 (simple_opt_clo env clo)
360 occ active stable_unf
361 where
362 stable_unf = isStableUnfolding (idUnfolding in_bndr)
363 active = isAlwaysActive (idInlineActivation in_bndr)
364 occ = idOccInfo in_bndr
365
366 pre_inline_unconditionally :: Bool
367 pre_inline_unconditionally
368 | isCoVar in_bndr = False -- See Note [Do not inline CoVars unconditionally]
369 | isExportedId in_bndr = False -- in SimplUtils
370 | stable_unf = False
371 | not active = False -- Note [Inline prag in simplOpt]
372 | not (safe_to_inline occ) = False
373 | otherwise = True
374
375 -- Unconditionally safe to inline
376 safe_to_inline :: OccInfo -> Bool
377 safe_to_inline (IAmALoopBreaker {}) = False
378 safe_to_inline IAmDead = True
379 safe_to_inline occ@(OneOcc {}) = not (occ_in_lam occ)
380 && occ_one_br occ
381 safe_to_inline (ManyOccs {}) = False
382
383 -------------------
384 simple_out_bind :: SimpleOptEnv -> (InVar, OutExpr)
385 -> (SimpleOptEnv, Maybe (OutVar, OutExpr))
386 simple_out_bind env@(SOE { soe_subst = subst }) (in_bndr, out_rhs)
387 | Type out_ty <- out_rhs
388 = ASSERT( isTyVar in_bndr )
389 (env { soe_subst = extendTvSubst subst in_bndr out_ty }, Nothing)
390
391 | Coercion out_co <- out_rhs
392 = ASSERT( isCoVar in_bndr )
393 (env { soe_subst = extendCvSubst subst in_bndr out_co }, Nothing)
394
395 | otherwise
396 = simple_out_bind_pair env in_bndr Nothing out_rhs
397 (idOccInfo in_bndr) True False
398
399 -------------------
400 simple_out_bind_pair :: SimpleOptEnv
401 -> InId -> Maybe OutId -> OutExpr
402 -> OccInfo -> Bool -> Bool
403 -> (SimpleOptEnv, Maybe (OutVar, OutExpr))
404 simple_out_bind_pair env in_bndr mb_out_bndr out_rhs
405 occ_info active stable_unf
406 | post_inline_unconditionally
407 = ( env' { soe_subst = extendIdSubst (soe_subst env) in_bndr out_rhs }
408 , Nothing)
409
410 | otherwise
411 = ( env', Just (out_bndr, out_rhs) )
412 where
413 (env', bndr1) = case mb_out_bndr of
414 Just out_bndr -> (env, out_bndr)
415 Nothing -> subst_opt_bndr env in_bndr
416 out_bndr = add_info env' in_bndr bndr1
417
418 post_inline_unconditionally :: Bool
419 post_inline_unconditionally
420 | not active = False
421 | isWeakLoopBreaker occ_info = False -- If it's a loop-breaker of any kind, don't inline
422 -- because it might be referred to "earlier"
423 | stable_unf = False -- Note [Stable unfoldings and postInlineUnconditionally]
424 | isExportedId in_bndr = False -- Note [Exported Ids and trivial RHSs]
425 | exprIsTrivial out_rhs = True
426 | coercible_hack = True
427 | otherwise = False
428
429 -- See Note [Getting the map/coerce RULE to work]
430 coercible_hack | (Var fun, args) <- collectArgs out_rhs
431 , Just dc <- isDataConWorkId_maybe fun
432 , dc `hasKey` heqDataConKey || dc `hasKey` coercibleDataConKey
433 = all exprIsTrivial args
434 | otherwise
435 = False
436
437 {- Note [Exported Ids and trivial RHSs]
438 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
439 We obviously do not want to unconditionally inline an Id that is exported.
440 In SimplUtils, Note [Top level and postInlineUnconditionally], we
441 explain why we don't inline /any/ top-level things unconditionally, even
442 trivial ones. But we do here! Why? In the simple optimiser
443
444 * We do no rule rewrites
445 * We do no call-site inlining
446
447 Those differences obviate the reasons for not inlining a trivial rhs,
448 and increase the benefit for doing so. So we unconditionally inline trivial
449 rhss here.
450 -}
451
452 ----------------------
453 subst_opt_bndrs :: SimpleOptEnv -> [InVar] -> (SimpleOptEnv, [OutVar])
454 subst_opt_bndrs env bndrs = mapAccumL subst_opt_bndr env bndrs
455
456 subst_opt_bndr :: SimpleOptEnv -> InVar -> (SimpleOptEnv, OutVar)
457 subst_opt_bndr env bndr
458 | isTyVar bndr = (env { soe_subst = subst_tv }, tv')
459 | isCoVar bndr = (env { soe_subst = subst_cv }, cv')
460 | otherwise = subst_opt_id_bndr env bndr
461 where
462 subst = soe_subst env
463 (subst_tv, tv') = substTyVarBndr subst bndr
464 (subst_cv, cv') = substCoVarBndr subst bndr
465
466 subst_opt_id_bndr :: SimpleOptEnv -> InId -> (SimpleOptEnv, OutId)
467 -- Nuke all fragile IdInfo, unfolding, and RULES;
468 -- it gets added back later by add_info
469 -- Rather like SimplEnv.substIdBndr
470 --
471 -- It's important to zap fragile OccInfo (which CoreSubst.substIdBndr
472 -- carefully does not do) because simplOptExpr invalidates it
473
474 subst_opt_id_bndr (SOE { soe_subst = subst, soe_inl = inl }) old_id
475 = (SOE { soe_subst = new_subst, soe_inl = new_inl }, new_id)
476 where
477 Subst in_scope id_subst tv_subst cv_subst = subst
478
479 id1 = uniqAway in_scope old_id
480 id2 = setIdType id1 (substTy subst (idType old_id))
481 new_id = zapFragileIdInfo id2
482 -- Zaps rules, worker-info, unfolding, and fragile OccInfo
483 -- The unfolding and rules will get added back later, by add_info
484
485 new_in_scope = in_scope `extendInScopeSet` new_id
486
487 no_change = new_id == old_id
488
489 -- Extend the substitution if the unique has changed,
490 -- See the notes with substTyVarBndr for the delSubstEnv
491 new_id_subst
492 | no_change = delVarEnv id_subst old_id
493 | otherwise = extendVarEnv id_subst old_id (Var new_id)
494
495 new_subst = Subst new_in_scope new_id_subst tv_subst cv_subst
496 new_inl = delVarEnv inl old_id
497
498 ----------------------
499 add_info :: SimpleOptEnv -> InVar -> OutVar -> OutVar
500 add_info env old_bndr new_bndr
501 | isTyVar old_bndr = new_bndr
502 | otherwise = maybeModifyIdInfo mb_new_info new_bndr
503 where
504 subst = soe_subst env
505 mb_new_info = substIdInfo subst new_bndr (idInfo old_bndr)
506
507 simpleUnfoldingFun :: IdUnfoldingFun
508 simpleUnfoldingFun id
509 | isAlwaysActive (idInlineActivation id) = idUnfolding id
510 | otherwise = noUnfolding
511
512 wrapLet :: Maybe (Id,CoreExpr) -> CoreExpr -> CoreExpr
513 wrapLet Nothing body = body
514 wrapLet (Just (b,r)) body = Let (NonRec b r) body
515
516 ------------------
517 substVects :: Subst -> [CoreVect] -> [CoreVect]
518 substVects subst = map (substVect subst)
519
520 ------------------
521 substVect :: Subst -> CoreVect -> CoreVect
522 substVect subst (Vect v rhs) = Vect v (simpleOptExprWith subst rhs)
523 substVect _subst vd@(NoVect _) = vd
524 substVect _subst vd@(VectType _ _ _) = vd
525 substVect _subst vd@(VectClass _) = vd
526 substVect _subst vd@(VectInst _) = vd
527
528 {-
529 Note [Inline prag in simplOpt]
530 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
531 If there's an INLINE/NOINLINE pragma that restricts the phase in
532 which the binder can be inlined, we don't inline here; after all,
533 we don't know what phase we're in. Here's an example
534
535 foo :: Int -> Int -> Int
536 {-# INLINE foo #-}
537 foo m n = inner m
538 where
539 {-# INLINE [1] inner #-}
540 inner m = m+n
541
542 bar :: Int -> Int
543 bar n = foo n 1
544
545 When inlining 'foo' in 'bar' we want the let-binding for 'inner'
546 to remain visible until Phase 1
547
548 Note [Unfold compulsory unfoldings in LHSs]
549 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
550 When the user writes `RULES map coerce = coerce` as a rule, the rule
551 will only ever match if simpleOptExpr replaces coerce by its unfolding
552 on the LHS, because that is the core that the rule matching engine
553 will find. So do that for everything that has a compulsory
554 unfolding. Also see Note [Desugaring coerce as cast] in Desugar.
555
556 However, we don't want to inline 'seq', which happens to also have a
557 compulsory unfolding, so we only do this unfolding only for things
558 that are always-active. See Note [User-defined RULES for seq] in MkId.
559
560 Note [Getting the map/coerce RULE to work]
561 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
562 We wish to allow the "map/coerce" RULE to fire:
563
564 {-# RULES "map/coerce" map coerce = coerce #-}
565
566 The naive core produced for this is
567
568 forall a b (dict :: Coercible * a b).
569 map @a @b (coerce @a @b @dict) = coerce @[a] @[b] @dict'
570
571 where dict' :: Coercible [a] [b]
572 dict' = ...
573
574 This matches literal uses of `map coerce` in code, but that's not what we
575 want. We want it to match, say, `map MkAge` (where newtype Age = MkAge Int)
576 too. Some of this is addressed by compulsorily unfolding coerce on the LHS,
577 yielding
578
579 forall a b (dict :: Coercible * a b).
580 map @a @b (\(x :: a) -> case dict of
581 MkCoercible (co :: a ~R# b) -> x |> co) = ...
582
583 Getting better. But this isn't exactly what gets produced. This is because
584 Coercible essentially has ~R# as a superclass, and superclasses get eagerly
585 extracted during solving. So we get this:
586
587 forall a b (dict :: Coercible * a b).
588 case Coercible_SCSel @* @a @b dict of
589 _ [Dead] -> map @a @b (\(x :: a) -> case dict of
590 MkCoercible (co :: a ~R# b) -> x |> co) = ...
591
592 Unfortunately, this still abstracts over a Coercible dictionary. We really
593 want it to abstract over the ~R# evidence. So, we have Desugar.unfold_coerce,
594 which transforms the above to (see also Note [Desugaring coerce as cast] in
595 Desugar)
596
597 forall a b (co :: a ~R# b).
598 let dict = MkCoercible @* @a @b co in
599 case Coercible_SCSel @* @a @b dict of
600 _ [Dead] -> map @a @b (\(x :: a) -> case dict of
601 MkCoercible (co :: a ~R# b) -> x |> co) = let dict = ... in ...
602
603 Now, we need simpleOptExpr to fix this up. It does so by taking three
604 separate actions:
605 1. Inline certain non-recursive bindings. The choice whether to inline
606 is made in simple_bind_pair. Note the rather specific check for
607 MkCoercible in there.
608
609 2. Stripping case expressions like the Coercible_SCSel one.
610 See the `Case` case of simple_opt_expr's `go` function.
611
612 3. Look for case expressions that unpack something that was
613 just packed and inline them. This is also done in simple_opt_expr's
614 `go` function.
615
616 This is all a fair amount of special-purpose hackery, but it's for
617 a good cause. And it won't hurt other RULES and such that it comes across.
618
619
620 ************************************************************************
621 * *
622 Join points
623 * *
624 ************************************************************************
625 -}
626
627 -- | Returns Just (bndr,rhs) if the binding is a join point:
628 -- If it's a JoinId, just return it
629 -- If it's not yet a JoinId but is always tail-called,
630 -- make it into a JoinId and return it.
631 -- In the latter case, eta-expand the RHS if necessary, to make the
632 -- lambdas explicit, as is required for join points
633 --
634 -- Precondition: the InBndr has been occurrence-analysed,
635 -- so its OccInfo is valid
636 joinPointBinding_maybe :: InBndr -> InExpr -> Maybe (InBndr, InExpr)
637 joinPointBinding_maybe bndr rhs
638 | not (isId bndr)
639 = Nothing
640
641 | isJoinId bndr
642 = Just (bndr, rhs)
643
644 | AlwaysTailCalled join_arity <- tailCallInfo (idOccInfo bndr)
645 , not (bad_unfolding join_arity (idUnfolding bndr))
646 , (bndrs, body) <- etaExpandToJoinPoint join_arity rhs
647 = Just (bndr `asJoinId` join_arity, mkLams bndrs body)
648
649 | otherwise
650 = Nothing
651
652 where
653 -- bad_unfolding returns True if we should /not/ convert a non-join-id
654 -- into a join-id, even though it is AlwaysTailCalled
655 -- See Note [Join points and INLINE pragmas]
656 bad_unfolding join_arity (CoreUnfolding { uf_src = src, uf_tmpl = rhs })
657 = isStableSource src && join_arity > joinRhsArity rhs
658 bad_unfolding _ (DFunUnfolding {})
659 = True
660 bad_unfolding _ _
661 = False
662
663 joinPointBindings_maybe :: [(InBndr, InExpr)] -> Maybe [(InBndr, InExpr)]
664 joinPointBindings_maybe bndrs
665 = mapM (uncurry joinPointBinding_maybe) bndrs
666
667
668 {- Note [Join points and INLINE pragmas]
669 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
670 Consider
671 f x = let g = \x. not -- Arity 1
672 {-# INLINE g #-}
673 in case x of
674 A -> g True True
675 B -> g True False
676 C -> blah2
677
678 Here 'g' is always tail-called applied to 2 args, but the stable
679 unfolding captured by the INLINE pragma has arity 1. If we try to
680 convert g to be a join point, its unfolding will still have arity 1
681 (since it is stable, and we don't meddle with stable unfoldings), and
682 Lint will complain (see Note [Invariants on join points], (2a), in
683 CoreSyn. Trac #13413.
684
685 Moreover, since g is going to be inlined anyway, there is no benefit
686 from making it a join point.
687
688 If it is recursive, and uselessly marked INLINE, this will stop us
689 making it a join point, which is a annoying. But occasionally
690 (notably in class methods; see Note [Instances and loop breakers] in
691 TcInstDcls) we mark recurive things as INLINE but the recursion
692 unravels; so ignoring INLINE pragmas on recursive things isn't good
693 either.
694
695
696 ************************************************************************
697 * *
698 exprIsConApp_maybe
699 * *
700 ************************************************************************
701
702 Note [exprIsConApp_maybe]
703 ~~~~~~~~~~~~~~~~~~~~~~~~~
704 exprIsConApp_maybe is a very important function. There are two principal
705 uses:
706 * case e of { .... }
707 * cls_op e, where cls_op is a class operation
708
709 In both cases you want to know if e is of form (C e1..en) where C is
710 a data constructor.
711
712 However e might not *look* as if
713
714
715 Note [exprIsConApp_maybe on literal strings]
716 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
717 See #9400 and #13317.
718
719 Conceptually, a string literal "abc" is just ('a':'b':'c':[]), but in Core
720 they are represented as unpackCString# "abc"# by MkCore.mkStringExprFS, or
721 unpackCStringUtf8# when the literal contains multi-byte UTF8 characters.
722
723 For optimizations we want to be able to treat it as a list, so they can be
724 decomposed when used in a case-statement. exprIsConApp_maybe detects those
725 calls to unpackCString# and returns:
726
727 Just (':', [Char], ['a', unpackCString# "bc"]).
728
729 We need to be careful about UTF8 strings here. ""# contains a ByteString, so
730 we must parse it back into a FastString to split off the first character.
731 That way we can treat unpackCString# and unpackCStringUtf8# in the same way.
732
733 We must also be caeful about
734 lvl = "foo"#
735 ...(unpackCString# lvl)...
736 to ensure that we see through the let-binding for 'lvl'. Hence the
737 (exprIsLiteral_maybe .. arg) in the guard before the call to
738 dealWithStringLiteral.
739
740 Note [Push coercions in exprIsConApp_maybe]
741 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
742 In Trac #13025 I found a case where we had
743 op (df @t1 @t2) -- op is a ClassOp
744 where
745 df = (/\a b. K e1 e2) |> g
746
747 To get this to come out we need to simplify on the fly
748 ((/\a b. K e1 e2) |> g) @t1 @t2
749
750 Hence the use of pushCoArgs.
751 -}
752
753 data ConCont = CC [CoreExpr] Coercion
754 -- Substitution already applied
755
756 -- | Returns @Just (dc, [t1..tk], [x1..xn])@ if the argument expression is
757 -- a *saturated* constructor application of the form @dc t1..tk x1 .. xn@,
758 -- where t1..tk are the *universally-qantified* type args of 'dc'
759 exprIsConApp_maybe :: InScopeEnv -> CoreExpr -> Maybe (DataCon, [Type], [CoreExpr])
760 exprIsConApp_maybe (in_scope, id_unf) expr
761 = go (Left in_scope) expr (CC [] (mkRepReflCo (exprType expr)))
762 where
763 go :: Either InScopeSet Subst
764 -- Left in-scope means "empty substitution"
765 -- Right subst means "apply this substitution to the CoreExpr"
766 -> CoreExpr -> ConCont
767 -> Maybe (DataCon, [Type], [CoreExpr])
768 go subst (Tick t expr) cont
769 | not (tickishIsCode t) = go subst expr cont
770 go subst (Cast expr co1) (CC args co2)
771 | Just (args', co1') <- pushCoArgs (subst_co subst co1) args
772 -- See Note [Push coercions in exprIsConApp_maybe]
773 = go subst expr (CC args' (co1' `mkTransCo` co2))
774 go subst (App fun arg) (CC args co)
775 = go subst fun (CC (subst_arg subst arg : args) co)
776 go subst (Lam var body) (CC (arg:args) co)
777 | exprIsTrivial arg -- Don't duplicate stuff!
778 = go (extend subst var arg) body (CC args co)
779 go (Right sub) (Var v) cont
780 = go (Left (substInScope sub))
781 (lookupIdSubst (text "exprIsConApp" <+> ppr expr) sub v)
782 cont
783
784 go (Left in_scope) (Var fun) cont@(CC args co)
785
786 | Just con <- isDataConWorkId_maybe fun
787 , count isValArg args == idArity fun
788 = pushCoDataCon con args co
789
790 -- Look through dictionary functions; see Note [Unfolding DFuns]
791 | DFunUnfolding { df_bndrs = bndrs, df_con = con, df_args = dfun_args } <- unfolding
792 , bndrs `equalLength` args -- See Note [DFun arity check]
793 , let subst = mkOpenSubst in_scope (bndrs `zip` args)
794 = pushCoDataCon con (map (substExpr (text "exprIsConApp1") subst) dfun_args) co
795
796 -- Look through unfoldings, but only arity-zero one;
797 -- if arity > 0 we are effectively inlining a function call,
798 -- and that is the business of callSiteInline.
799 -- In practice, without this test, most of the "hits" were
800 -- CPR'd workers getting inlined back into their wrappers,
801 | idArity fun == 0
802 , Just rhs <- expandUnfolding_maybe unfolding
803 , let in_scope' = extendInScopeSetSet in_scope (exprFreeVars rhs)
804 = go (Left in_scope') rhs cont
805
806 -- See Note [exprIsConApp_maybe on literal strings]
807 | (fun `hasKey` unpackCStringIdKey) ||
808 (fun `hasKey` unpackCStringUtf8IdKey)
809 , [arg] <- args
810 , Just (MachStr str) <- exprIsLiteral_maybe (in_scope, id_unf) arg
811 = dealWithStringLiteral fun str co
812 where
813 unfolding = id_unf fun
814
815 go _ _ _ = Nothing
816
817 ----------------------------
818 -- Operations on the (Either InScopeSet CoreSubst)
819 -- The Left case is wildly dominant
820 subst_co (Left {}) co = co
821 subst_co (Right s) co = CoreSubst.substCo s co
822
823 subst_arg (Left {}) e = e
824 subst_arg (Right s) e = substExpr (text "exprIsConApp2") s e
825
826 extend (Left in_scope) v e = Right (extendSubst (mkEmptySubst in_scope) v e)
827 extend (Right s) v e = Right (extendSubst s v e)
828
829
830 -- See Note [exprIsConApp_maybe on literal strings]
831 dealWithStringLiteral :: Var -> BS.ByteString -> Coercion
832 -> Maybe (DataCon, [Type], [CoreExpr])
833
834 -- This is not possible with user-supplied empty literals, MkCore.mkStringExprFS
835 -- turns those into [] automatically, but just in case something else in GHC
836 -- generates a string literal directly.
837 dealWithStringLiteral _ str co
838 | BS.null str
839 = pushCoDataCon nilDataCon [Type charTy] co
840
841 dealWithStringLiteral fun str co
842 = let strFS = mkFastStringByteString str
843
844 char = mkConApp charDataCon [mkCharLit (headFS strFS)]
845 charTail = fastStringToByteString (tailFS strFS)
846
847 -- In singleton strings, just add [] instead of unpackCstring# ""#.
848 rest = if BS.null charTail
849 then mkConApp nilDataCon [Type charTy]
850 else App (Var fun)
851 (Lit (MachStr charTail))
852
853 in pushCoDataCon consDataCon [Type charTy, char, rest] co
854
855 {-
856 Note [Unfolding DFuns]
857 ~~~~~~~~~~~~~~~~~~~~~~
858 DFuns look like
859
860 df :: forall a b. (Eq a, Eq b) -> Eq (a,b)
861 df a b d_a d_b = MkEqD (a,b) ($c1 a b d_a d_b)
862 ($c2 a b d_a d_b)
863
864 So to split it up we just need to apply the ops $c1, $c2 etc
865 to the very same args as the dfun. It takes a little more work
866 to compute the type arguments to the dictionary constructor.
867
868 Note [DFun arity check]
869 ~~~~~~~~~~~~~~~~~~~~~~~
870 Here we check that the total number of supplied arguments (inclding
871 type args) matches what the dfun is expecting. This may be *less*
872 than the ordinary arity of the dfun: see Note [DFun unfoldings] in CoreSyn
873 -}
874
875 exprIsLiteral_maybe :: InScopeEnv -> CoreExpr -> Maybe Literal
876 -- Same deal as exprIsConApp_maybe, but much simpler
877 -- Nevertheless we do need to look through unfoldings for
878 -- Integer and string literals, which are vigorously hoisted to top level
879 -- and not subsequently inlined
880 exprIsLiteral_maybe env@(_, id_unf) e
881 = case e of
882 Lit l -> Just l
883 Tick _ e' -> exprIsLiteral_maybe env e' -- dubious?
884 Var v | Just rhs <- expandUnfolding_maybe (id_unf v)
885 -> exprIsLiteral_maybe env rhs
886 _ -> Nothing
887
888 {-
889 Note [exprIsLambda_maybe]
890 ~~~~~~~~~~~~~~~~~~~~~~~~~~
891 exprIsLambda_maybe will, given an expression `e`, try to turn it into the form
892 `Lam v e'` (returned as `Just (v,e')`). Besides using lambdas, it looks through
893 casts (using the Push rule), and it unfolds function calls if the unfolding
894 has a greater arity than arguments are present.
895
896 Currently, it is used in Rules.match, and is required to make
897 "map coerce = coerce" match.
898 -}
899
900 exprIsLambda_maybe :: InScopeEnv -> CoreExpr
901 -> Maybe (Var, CoreExpr,[Tickish Id])
902 -- See Note [exprIsLambda_maybe]
903
904 -- The simple case: It is a lambda already
905 exprIsLambda_maybe _ (Lam x e)
906 = Just (x, e, [])
907
908 -- Still straightforward: Ticks that we can float out of the way
909 exprIsLambda_maybe (in_scope_set, id_unf) (Tick t e)
910 | tickishFloatable t
911 , Just (x, e, ts) <- exprIsLambda_maybe (in_scope_set, id_unf) e
912 = Just (x, e, t:ts)
913
914 -- Also possible: A casted lambda. Push the coercion inside
915 exprIsLambda_maybe (in_scope_set, id_unf) (Cast casted_e co)
916 | Just (x, e,ts) <- exprIsLambda_maybe (in_scope_set, id_unf) casted_e
917 -- Only do value lambdas.
918 -- this implies that x is not in scope in gamma (makes this code simpler)
919 , not (isTyVar x) && not (isCoVar x)
920 , ASSERT( not $ x `elemVarSet` tyCoVarsOfCo co) True
921 , Just (x',e') <- pushCoercionIntoLambda in_scope_set x e co
922 , let res = Just (x',e',ts)
923 = --pprTrace "exprIsLambda_maybe:Cast" (vcat [ppr casted_e,ppr co,ppr res)])
924 res
925
926 -- Another attempt: See if we find a partial unfolding
927 exprIsLambda_maybe (in_scope_set, id_unf) e
928 | (Var f, as, ts) <- collectArgsTicks tickishFloatable e
929 , idArity f > count isValArg as
930 -- Make sure there is hope to get a lambda
931 , Just rhs <- expandUnfolding_maybe (id_unf f)
932 -- Optimize, for beta-reduction
933 , let e' = simpleOptExprWith (mkEmptySubst in_scope_set) (rhs `mkApps` as)
934 -- Recurse, because of possible casts
935 , Just (x', e'', ts') <- exprIsLambda_maybe (in_scope_set, id_unf) e'
936 , let res = Just (x', e'', ts++ts')
937 = -- pprTrace "exprIsLambda_maybe:Unfold" (vcat [ppr e, ppr (x',e'')])
938 res
939
940 exprIsLambda_maybe _ _e
941 = -- pprTrace "exprIsLambda_maybe:Fail" (vcat [ppr _e])
942 Nothing
943
944
945 {- *********************************************************************
946 * *
947 The "push rules"
948 * *
949 ************************************************************************
950
951 Here we implement the "push rules" from FC papers:
952
953 * The push-argument rules, where we can move a coercion past an argument.
954 We have
955 (fun |> co) arg
956 and we want to transform it to
957 (fun arg') |> co'
958 for some suitable co' and tranformed arg'.
959
960 * The PushK rule for data constructors. We have
961 (K e1 .. en) |> co
962 and we want to tranform to
963 (K e1' .. en')
964 by pushing the coercion into the oarguments
965 -}
966
967 pushCoArgs :: Coercion -> [CoreArg] -> Maybe ([CoreArg], Coercion)
968 pushCoArgs co [] = return ([], co)
969 pushCoArgs co (arg:args) = do { (arg', co1) <- pushCoArg co arg
970 ; (args', co2) <- pushCoArgs co1 args
971 ; return (arg':args', co2) }
972
973 pushCoArg :: Coercion -> CoreArg -> Maybe (CoreArg, Coercion)
974 -- We have (fun |> co) arg, and we want to transform it to
975 -- (fun arg) |> co
976 -- This may fail, e.g. if (fun :: N) where N is a newtype
977 -- C.f. simplCast in Simplify.hs
978 -- 'co' is always Representational
979
980 pushCoArg co (Type ty) = do { (ty', co') <- pushCoTyArg co ty
981 ; return (Type ty', co') }
982 pushCoArg co val_arg = do { (arg_co, co') <- pushCoValArg co
983 ; return (mkCast val_arg arg_co, co') }
984
985 pushCoTyArg :: Coercion -> Type -> Maybe (Type, Coercion)
986 -- We have (fun |> co) @ty
987 -- Push the coercion through to return
988 -- (fun @ty') |> co'
989 -- 'co' is always Representational
990 pushCoTyArg co ty
991 | tyL `eqType` tyR
992 = Just (ty, mkRepReflCo (piResultTy tyR ty))
993
994 | isForAllTy tyL
995 = ASSERT2( isForAllTy tyR, ppr co $$ ppr ty )
996 Just (ty `mkCastTy` mkSymCo co1, co2)
997
998 | otherwise
999 = Nothing
1000 where
1001 Pair tyL tyR = coercionKind co
1002 -- co :: tyL ~ tyR
1003 -- tyL = forall (a1 :: k1). ty1
1004 -- tyR = forall (a2 :: k2). ty2
1005
1006 co1 = mkNthCo 0 co
1007 -- co1 :: k1 ~ k2
1008 -- Note that NthCo can extract an equality between the kinds
1009 -- of the types related by a coercion between forall-types.
1010 -- See the NthCo case in CoreLint.
1011
1012 co2 = mkInstCo co (mkCoherenceLeftCo (mkNomReflCo ty) co1)
1013 -- co2 :: ty1[ (ty|>co1)/a1 ] ~ ty2[ ty/a2 ]
1014 -- Arg of mkInstCo is always nominal, hence mkNomReflCo
1015
1016 pushCoValArg :: Coercion -> Maybe (Coercion, Coercion)
1017 -- We have (fun |> co) arg
1018 -- Push the coercion through to return
1019 -- (fun (arg |> co_arg)) |> co_res
1020 -- 'co' is always Representational
1021 pushCoValArg co
1022 | tyL `eqType` tyR
1023 = Just (mkRepReflCo arg, mkRepReflCo res)
1024
1025 | isFunTy tyL
1026 , (co1, co2) <- decomposeFunCo co
1027 -- If co :: (tyL1 -> tyL2) ~ (tyR1 -> tyR2)
1028 -- then co1 :: tyL1 ~ tyR1
1029 -- co2 :: tyL2 ~ tyR2
1030 = ASSERT2( isFunTy tyR, ppr co $$ ppr arg )
1031 Just (mkSymCo co1, co2)
1032
1033 | otherwise
1034 = Nothing
1035 where
1036 (arg, res) = splitFunTy tyR
1037 Pair tyL tyR = coercionKind co
1038
1039 pushCoercionIntoLambda
1040 :: InScopeSet -> Var -> CoreExpr -> Coercion -> Maybe (Var, CoreExpr)
1041 -- This implements the Push rule from the paper on coercions
1042 -- (\x. e) |> co
1043 -- ===>
1044 -- (\x'. e |> co')
1045 pushCoercionIntoLambda in_scope x e co
1046 | ASSERT(not (isTyVar x) && not (isCoVar x)) True
1047 , Pair s1s2 t1t2 <- coercionKind co
1048 , Just (_s1,_s2) <- splitFunTy_maybe s1s2
1049 , Just (t1,_t2) <- splitFunTy_maybe t1t2
1050 = let (co1, co2) = decomposeFunCo co
1051 -- Should we optimize the coercions here?
1052 -- Otherwise they might not match too well
1053 x' = x `setIdType` t1
1054 in_scope' = in_scope `extendInScopeSet` x'
1055 subst = extendIdSubst (mkEmptySubst in_scope')
1056 x
1057 (mkCast (Var x') co1)
1058 in Just (x', substExpr (text "pushCoercionIntoLambda") subst e `mkCast` co2)
1059 | otherwise
1060 = pprTrace "exprIsLambda_maybe: Unexpected lambda in case" (ppr (Lam x e))
1061 Nothing
1062
1063 pushCoDataCon :: DataCon -> [CoreExpr] -> Coercion
1064 -> Maybe (DataCon
1065 , [Type] -- Universal type args
1066 , [CoreExpr]) -- All other args incl existentials
1067 -- Implement the KPush reduction rule as described in "Down with kinds"
1068 -- The transformation applies iff we have
1069 -- (C e1 ... en) `cast` co
1070 -- where co :: (T t1 .. tn) ~ to_ty
1071 -- The left-hand one must be a T, because exprIsConApp returned True
1072 -- but the right-hand one might not be. (Though it usually will.)
1073 pushCoDataCon dc dc_args co
1074 | isReflCo co || from_ty `eqType` to_ty -- try cheap test first
1075 , let (univ_ty_args, rest_args) = splitAtList (dataConUnivTyVars dc) dc_args
1076 = Just (dc, map exprToType univ_ty_args, rest_args)
1077
1078 | Just (to_tc, to_tc_arg_tys) <- splitTyConApp_maybe to_ty
1079 , to_tc == dataConTyCon dc
1080 -- These two tests can fail; we might see
1081 -- (C x y) `cast` (g :: T a ~ S [a]),
1082 -- where S is a type function. In fact, exprIsConApp
1083 -- will probably not be called in such circumstances,
1084 -- but there't nothing wrong with it
1085
1086 = let
1087 tc_arity = tyConArity to_tc
1088 dc_univ_tyvars = dataConUnivTyVars dc
1089 dc_ex_tyvars = dataConExTyVars dc
1090 arg_tys = dataConRepArgTys dc
1091
1092 non_univ_args = dropList dc_univ_tyvars dc_args
1093 (ex_args, val_args) = splitAtList dc_ex_tyvars non_univ_args
1094
1095 -- Make the "Psi" from the paper
1096 omegas = decomposeCo tc_arity co
1097 (psi_subst, to_ex_arg_tys)
1098 = liftCoSubstWithEx Representational
1099 dc_univ_tyvars
1100 omegas
1101 dc_ex_tyvars
1102 (map exprToType ex_args)
1103
1104 -- Cast the value arguments (which include dictionaries)
1105 new_val_args = zipWith cast_arg arg_tys val_args
1106 cast_arg arg_ty arg = mkCast arg (psi_subst arg_ty)
1107
1108 to_ex_args = map Type to_ex_arg_tys
1109
1110 dump_doc = vcat [ppr dc, ppr dc_univ_tyvars, ppr dc_ex_tyvars,
1111 ppr arg_tys, ppr dc_args,
1112 ppr ex_args, ppr val_args, ppr co, ppr from_ty, ppr to_ty, ppr to_tc ]
1113 in
1114 ASSERT2( eqType from_ty (mkTyConApp to_tc (map exprToType $ takeList dc_univ_tyvars dc_args)), dump_doc )
1115 ASSERT2( equalLength val_args arg_tys, dump_doc )
1116 Just (dc, to_tc_arg_tys, to_ex_args ++ new_val_args)
1117
1118 | otherwise
1119 = Nothing
1120
1121 where
1122 Pair from_ty to_ty = coercionKind co
1123
1124 collectBindersPushingCo :: CoreExpr -> ([Var], CoreExpr)
1125 -- Collect lambda binders, pushing coercions inside if possible
1126 -- E.g. (\x.e) |> g g :: <Int> -> blah
1127 -- = (\x. e |> Nth 1 g)
1128 --
1129 -- That is,
1130 --
1131 -- collectBindersPushingCo ((\x.e) |> g) === ([x], e |> Nth 1 g)
1132 collectBindersPushingCo e
1133 = go [] e
1134 where
1135 -- Peel off lambdas until we hit a cast.
1136 go :: [Var] -> CoreExpr -> ([Var], CoreExpr)
1137 -- The accumulator is in reverse order
1138 go bs (Lam b e) = go (b:bs) e
1139 go bs (Cast e co) = go_c bs e co
1140 go bs e = (reverse bs, e)
1141
1142 -- We are in a cast; peel off casts until we hit a lambda.
1143 go_c :: [Var] -> CoreExpr -> Coercion -> ([Var], CoreExpr)
1144 -- (go_c bs e c) is same as (go bs e (e |> c))
1145 go_c bs (Cast e co1) co2 = go_c bs e (co1 `mkTransCo` co2)
1146 go_c bs (Lam b e) co = go_lam bs b e co
1147 go_c bs e co = (reverse bs, mkCast e co)
1148
1149 -- We are in a lambda under a cast; peel off lambdas and build a
1150 -- new coercion for the body.
1151 go_lam :: [Var] -> Var -> CoreExpr -> Coercion -> ([Var], CoreExpr)
1152 -- (go_lam bs b e c) is same as (go_c bs (\b.e) c)
1153 go_lam bs b e co
1154 | isTyVar b
1155 , let Pair tyL tyR = coercionKind co
1156 , ASSERT( isForAllTy tyL )
1157 isForAllTy tyR
1158 , isReflCo (mkNthCo 0 co) -- See Note [collectBindersPushingCo]
1159 = go_c (b:bs) e (mkInstCo co (mkNomReflCo (mkTyVarTy b)))
1160
1161 | isId b
1162 , let Pair tyL tyR = coercionKind co
1163 , ASSERT( isFunTy tyL) isFunTy tyR
1164 , (co_arg, co_res) <- decomposeFunCo co
1165 , isReflCo co_arg -- See Note [collectBindersPushingCo]
1166 = go_c (b:bs) e co_res
1167
1168 | otherwise = (reverse bs, mkCast (Lam b e) co)
1169
1170 {- Note [collectBindersPushingCo]
1171 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1172 We just look for coercions of form
1173 <type> -> blah
1174 (and similarly for foralls) to keep this function simple. We could do
1175 more elaborate stuff, but it'd involve substitution etc.
1176 -}