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