Coercion Quantification
[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, isNonCoVarId )
36 import VarSet
37 import VarEnv
38 import DataCon
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 )
45 import TysWiredIn
46 import PrelNames
47 import BasicTypes
48 import Module ( Module )
49 import ErrUtils
50 import DynFlags
51 import Outputable
52 import Pair
53 import Util
54 import Maybes ( orElse )
55 import FastString
56 import Data.List
57 import qualified Data.ByteString as BS
58
59 {-
60 ************************************************************************
61 * *
62 The Simple Optimiser
63 * *
64 ************************************************************************
65
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
70
71 - inlining things that occur just once,
72 or whose RHS turns out to be trivial
73 - beta reduction
74 - case of known constructor
75 - dead code elimination
76
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.
80
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.
87
88 -}
89
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
96 --
97 -- We also inline bindings that bind a Eq# box: see
98 -- See Note [Getting the map/coerce RULE to work].
99 --
100 -- Also we convert functions to join points where possible (as
101 -- the occurrence analyser does most of the work anyway).
102 --
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
106
107 simpleOptExpr dflags expr
108 = -- pprTrace "simpleOptExpr" (ppr init_subst $$ ppr expr)
109 simpleOptExprWith dflags init_subst expr
110 where
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
117 -- lambda.
118 --
119 -- It's a bit painful to call exprFreeVars, because it makes
120 -- three passes instead of two (occ-anal, and go)
121
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)
126 where
127 init_env = SOE { soe_dflags = dflags
128 , soe_inl = emptyVarEnv
129 , soe_subst = subst }
130
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 );
139
140 ; return (reverse binds', rules') }
141 where
142 occ_anald_binds = occurAnalysePgm this_mod
143 (\_ -> True) {- All unfoldings active -}
144 (\_ -> False) {- No rules active -}
145 rules binds
146
147 (final_env, binds') = foldl' do_one (emptyEnv dflags, []) occ_anald_binds
148 final_subst = soe_subst final_env
149
150 rules' = substRulesForImportedIds final_subst rules
151 -- We never unconditionally inline into rules,
152 -- hence paying just a substitution
153
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')
158
159 -- In these functions the substitution maps InVar -> OutExpr
160
161 ----------------------
162 type SimpleClo = (SimpleOptEnv, InExpr)
163
164 data SimpleOptEnv
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
170
171 , soe_subst :: Subst
172 -- Deals with cloning; includes the InScopeSet
173 }
174
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 ]
179 <+> text "}"
180
181 emptyEnv :: DynFlags -> SimpleOptEnv
182 emptyEnv dflags
183 = SOE { soe_dflags = dflags
184 , soe_inl = emptyVarEnv
185 , soe_subst = emptySubst }
186
187 soeZapSubst :: SimpleOptEnv -> SimpleOptEnv
188 soeZapSubst env@(SOE { soe_subst = subst })
189 = env { soe_inl = emptyVarEnv, soe_subst = zapSubstEnv subst }
190
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) }
196
197 ---------------
198 simple_opt_clo :: SimpleOptEnv -> SimpleClo -> OutExpr
199 simple_opt_clo env (e_env, e)
200 = simple_opt_expr (soeSetInScope env e_env) e
201
202 simple_opt_expr :: SimpleOptEnv -> InExpr -> OutExpr
203 simple_opt_expr env expr
204 = go expr
205 where
206 subst = soe_subst env
207 in_scope = substInScope subst
208 in_scope_env = (in_scope, simpleUnfoldingFun)
209
210 go (Var v)
211 | Just clo <- lookupVarEnv (soe_inl env) v
212 = simple_opt_clo env clo
213 | otherwise
214 = lookupIdSubst (text "simpleOptExpr") (soe_subst env) v
215
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'
223 where
224 co' = optCoercion (soe_dflags env) (getTCvSubst subst) co
225
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)
229
230 go lam@(Lam {}) = go_lam env [] lam
231 go (Case e b ty as)
232 -- See Note [Getting the map/coerce RULE to work]
233 | isDeadBinder b
234 , Just (con, _tys, es) <- exprIsConApp_maybe in_scope_env e'
235 , Just (altcon, bs, rhs) <- findAlt (DataAlt con) as
236 = case altcon of
237 DEFAULT -> go rhs
238 _ -> foldr wrapLet (simple_opt_expr env' rhs) mb_prs
239 where
240 (env', mb_prs) = mapAccumL simple_out_bind env $
241 zipEqual "simpleOptExpr" bs es
242
243 -- Note [Getting the map/coerce RULE to work]
244 | isDeadBinder b
245 , [(DEFAULT, _, rhs)] <- as
246 , isCoercionType (varType b)
247 , (Var fun, _args) <- collectArgs e
248 , fun `hasKey` coercibleSCSelIdKey
249 -- without this last check, we get #11230
250 = go rhs
251
252 | otherwise
253 = Case e' b' (substTy subst ty)
254 (map (go_alt env') as)
255 where
256 e' = go e
257 (env', b') = subst_opt_bndr env b
258
259 ----------------------
260 go_alt env (con, bndrs, rhs)
261 = (con, bndrs', simple_opt_expr env' rhs)
262 where
263 (env', bndrs') = subst_opt_bndrs env bndrs
264
265 ----------------------
266 -- go_lam tries eta reduction
267 go_lam env bs' (Lam b e)
268 = go_lam env' (b':bs') e
269 where
270 (env', b') = subst_opt_bndr env b
271 go_lam env bs' e
272 | Just etad_e <- tryEtaReduce bs e' = etad_e
273 | otherwise = mkLams bs e'
274 where
275 bs = reverse bs'
276 e' = simple_opt_expr env e
277
278 ----------------------
279 -- simple_app collects arguments for beta reduction
280 simple_app :: SimpleOptEnv -> InExpr -> [SimpleClo] -> CoreExpr
281
282 simple_app env (Var v) as
283 | Just (env', e) <- lookupVarEnv (soe_inl env) v
284 = simple_app (soeSetInScope env env') e as
285
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
291
292 | otherwise
293 , let out_fn = lookupIdSubst (text "simple_app") (soe_subst env) v
294 = finish_app env out_fn as
295
296 simple_app env (App e1 e2) as
297 = simple_app env e1 ((env, e2) : as)
298
299 simple_app env (Lam b e) (a:as)
300 = wrapLet mb_pr (simple_app env' e as)
301 where
302 (env', mb_pr) = simple_bind_pair env b Nothing a
303
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
308
309 simple_app env e as
310 = finish_app env (simple_opt_expr env e) as
311
312 finish_app :: SimpleOptEnv -> OutExpr -> [SimpleClo] -> OutExpr
313 finish_app _ fun []
314 = fun
315 finish_app env fun (arg:args)
316 = finish_app env (App fun (simple_opt_clo env arg)) args
317
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
323 Nothing -> Nothing
324 Just (b,r) -> Just (NonRec b r))
325 where
326 (b', r') = joinPointBinding_maybe b r `orElse` (b, r)
327 (env', mb_pr) = simple_bind_pair env b' Nothing (env,r')
328
329 simple_opt_bind env (Rec prs)
330 = (env'', res_bind)
331 where
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
338 Just pr -> pr : prs
339 Nothing -> prs)
340 where
341 (env', mb_pr) = simple_bind_pair env b (Just b') (env,r)
342
343 ----------------------
344 simple_bind_pair :: SimpleOptEnv
345 -> InVar -> Maybe OutVar
346 -> SimpleClo
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)
357
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)
362
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)
368
369 | otherwise
370 = simple_out_bind_pair env in_bndr mb_out_bndr out_rhs
371 occ active stable_unf
372 where
373 stable_unf = isStableUnfolding (idUnfolding in_bndr)
374 active = isAlwaysActive (idInlineActivation in_bndr)
375 occ = idOccInfo in_bndr
376
377 out_rhs | Just join_arity <- isJoinId_maybe in_bndr
378 = simple_join_rhs join_arity
379 | otherwise
380 = simple_opt_clo env clo
381
382 simple_join_rhs join_arity -- See Note [Preserve join-binding arity]
383 = mkLams join_bndrs' (simple_opt_expr env_body join_body)
384 where
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
388
389 pre_inline_unconditionally :: Bool
390 pre_inline_unconditionally
391 | isExportedId in_bndr = False
392 | stable_unf = False
393 | not active = False -- Note [Inline prag in simplOpt]
394 | not (safe_to_inline occ) = False
395 | otherwise = True
396
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)
402 && occ_one_br occ
403 safe_to_inline (ManyOccs {}) = False
404
405 -------------------
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)
412
413 | Coercion out_co <- out_rhs
414 = ASSERT( isCoVar in_bndr )
415 (env { soe_subst = extendCvSubst subst in_bndr out_co }, Nothing)
416
417 | otherwise
418 = simple_out_bind_pair env in_bndr Nothing out_rhs
419 (idOccInfo in_bndr) True False
420
421 -------------------
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 }
433 , Nothing)
434
435 | otherwise
436 = ( env', Just (out_bndr, out_rhs) )
437 where
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
442
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
452 | otherwise = False
453
454 is_loop_breaker = isWeakLoopBreaker occ_info
455
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
461 | otherwise
462 = False
463
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
470
471 * We do no rule rewrites
472 * We do no call-site inlining
473
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
476 rhss here.
477
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).
485 -}
486
487 ----------------------
488 subst_opt_bndrs :: SimpleOptEnv -> [InVar] -> (SimpleOptEnv, [OutVar])
489 subst_opt_bndrs env bndrs = mapAccumL subst_opt_bndr env bndrs
490
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
496 where
497 subst = soe_subst env
498 (subst_tv, tv') = substTyVarBndr subst bndr
499 (subst_cv, cv') = substCoVarBndr subst bndr
500
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
505 --
506 -- It's important to zap fragile OccInfo (which CoreSubst.substIdBndr
507 -- carefully does not do) because simplOptExpr invalidates it
508
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)
511 where
512 Subst in_scope id_subst tv_subst cv_subst = subst
513
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
519
520 new_in_scope = in_scope `extendInScopeSet` new_id
521
522 no_change = new_id == old_id
523
524 -- Extend the substitution if the unique has changed,
525 -- See the notes with substTyVarBndr for the delSubstEnv
526 new_id_subst
527 | no_change = delVarEnv id_subst old_id
528 | otherwise = extendVarEnv id_subst old_id (Var new_id)
529
530 new_subst = Subst new_in_scope new_id_subst tv_subst cv_subst
531 new_inl = delVarEnv inl old_id
532
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
538 where
539 subst = soe_subst env
540 mb_new_info = substIdInfo subst new_bndr (idInfo old_bndr)
541
542 simpleUnfoldingFun :: IdUnfoldingFun
543 simpleUnfoldingFun id
544 | isAlwaysActive (idInlineActivation id) = idUnfolding id
545 | otherwise = noUnfolding
546
547 wrapLet :: Maybe (Id,CoreExpr) -> CoreExpr -> CoreExpr
548 wrapLet Nothing body = body
549 wrapLet (Just (b,r)) body = Let (NonRec b r) body
550
551 {-
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
557
558 foo :: Int -> Int -> Int
559 {-# INLINE foo #-}
560 foo m n = inner m
561 where
562 {-# INLINE [1] inner #-}
563 inner m = m+n
564
565 bar :: Int -> Int
566 bar n = foo n 1
567
568 When inlining 'foo' in 'bar' we want the let-binding for 'inner'
569 to remain visible until Phase 1
570
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.
578
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.
582
583 Note [Getting the map/coerce RULE to work]
584 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
585 We wish to allow the "map/coerce" RULE to fire:
586
587 {-# RULES "map/coerce" map coerce = coerce #-}
588
589 The naive core produced for this is
590
591 forall a b (dict :: Coercible * a b).
592 map @a @b (coerce @a @b @dict) = coerce @[a] @[b] @dict'
593
594 where dict' :: Coercible [a] [b]
595 dict' = ...
596
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,
600 yielding
601
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) = ...
605
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:
609
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) = ...
614
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
618 Desugar)
619
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 ...
625
626 Now, we need simpleOptExpr to fix this up. It does so by taking three
627 separate actions:
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.
631
632 2. Stripping case expressions like the Coercible_SCSel one.
633 See the `Case` case of simple_opt_expr's `go` function.
634
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
637 `go` function.
638
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.
641
642
643 ************************************************************************
644 * *
645 Join points
646 * *
647 ************************************************************************
648 -}
649
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
656 --
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
661 | not (isId bndr)
662 = Nothing
663
664 | isJoinId bndr
665 = Just (bndr, rhs)
666
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)
674
675 | otherwise
676 = Nothing
677
678 joinPointBindings_maybe :: [(InBndr, InExpr)] -> Maybe [(InBndr, InExpr)]
679 joinPointBindings_maybe bndrs
680 = mapM (uncurry joinPointBinding_maybe) bndrs
681
682
683 {- Note [Strictness and join points]
684 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
685 Suppose we have
686
687 let f = \x. if x>200 then e1 else e1
688
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
691
692 let f = \x y. if x>200 then e1 else e1
693
694 and now it's only strict if applied to two arguments. So we should
695 adjust the strictness info.
696
697 A more common case is when
698
699 f = \x. error ".."
700
701 and again its arity increses (Trac #15517)
702 -}
703
704 {- *********************************************************************
705 * *
706 exprIsConApp_maybe
707 * *
708 ************************************************************************
709
710 Note [exprIsConApp_maybe]
711 ~~~~~~~~~~~~~~~~~~~~~~~~~
712 exprIsConApp_maybe is a very important function. There are two principal
713 uses:
714 * case e of { .... }
715 * cls_op e, where cls_op is a class operation
716
717 In both cases you want to know if e is of form (C e1..en) where C is
718 a data constructor.
719
720 However e might not *look* as if
721
722
723 Note [exprIsConApp_maybe on literal strings]
724 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
725 See #9400 and #13317.
726
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.
730
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:
734
735 Just (':', [Char], ['a', unpackCString# "bc"]).
736
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.
740
741 We must also be caeful about
742 lvl = "foo"#
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.
747
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
752 where
753 df = (/\a b. K e1 e2) |> g
754
755 To get this to come out we need to simplify on the fly
756 ((/\a b. K e1 e2) |> g) @t1 @t2
757
758 Hence the use of pushCoArgs.
759 -}
760
761 data ConCont = CC [CoreExpr] Coercion
762 -- Substitution already applied
763
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)))
770 where
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]
781 = case m_co1' of
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)
792 cont
793
794 go (Left in_scope) (Var fun) cont@(CC args co)
795
796 | Just con <- isDataConWorkId_maybe fun
797 , count isValArg args == idArity fun
798 = pushCoDataCon con args co
799
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
805
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,
811 | idArity fun == 0
812 , Just rhs <- expandUnfolding_maybe unfolding
813 , let in_scope' = extendInScopeSetSet in_scope (exprFreeVars rhs)
814 = go (Left in_scope') rhs cont
815
816 -- See Note [exprIsConApp_maybe on literal strings]
817 | (fun `hasKey` unpackCStringIdKey) ||
818 (fun `hasKey` unpackCStringUtf8IdKey)
819 , [arg] <- args
820 , Just (MachStr str) <- exprIsLiteral_maybe (in_scope, id_unf) arg
821 = dealWithStringLiteral fun str co
822 where
823 unfolding = id_unf fun
824
825 go _ _ _ = Nothing
826
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
832
833 subst_arg (Left {}) e = e
834 subst_arg (Right s) e = substExpr (text "exprIsConApp2") s e
835
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)
838
839
840 -- See Note [exprIsConApp_maybe on literal strings]
841 dealWithStringLiteral :: Var -> BS.ByteString -> Coercion
842 -> Maybe (DataCon, [Type], [CoreExpr])
843
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
848 | BS.null str
849 = pushCoDataCon nilDataCon [Type charTy] co
850
851 dealWithStringLiteral fun str co
852 = let strFS = mkFastStringByteString str
853
854 char = mkConApp charDataCon [mkCharLit (headFS strFS)]
855 charTail = fastStringToByteString (tailFS strFS)
856
857 -- In singleton strings, just add [] instead of unpackCstring# ""#.
858 rest = if BS.null charTail
859 then mkConApp nilDataCon [Type charTy]
860 else App (Var fun)
861 (Lit (MachStr charTail))
862
863 in pushCoDataCon consDataCon [Type charTy, char, rest] co
864
865 {-
866 Note [Unfolding DFuns]
867 ~~~~~~~~~~~~~~~~~~~~~~
868 DFuns look like
869
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)
872 ($c2 a b d_a d_b)
873
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.
877
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
883 -}
884
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
891 = case e of
892 Lit l -> Just l
893 Tick _ e' -> exprIsLiteral_maybe env e' -- dubious?
894 Var v | Just rhs <- expandUnfolding_maybe (id_unf v)
895 -> exprIsLiteral_maybe env rhs
896 _ -> Nothing
897
898 {-
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.
905
906 Currently, it is used in Rules.match, and is required to make
907 "map coerce = coerce" match.
908 -}
909
910 exprIsLambda_maybe :: InScopeEnv -> CoreExpr
911 -> Maybe (Var, CoreExpr,[Tickish Id])
912 -- See Note [exprIsLambda_maybe]
913
914 -- The simple case: It is a lambda already
915 exprIsLambda_maybe _ (Lam x e)
916 = Just (x, e, [])
917
918 -- Still straightforward: Ticks that we can float out of the way
919 exprIsLambda_maybe (in_scope_set, id_unf) (Tick t e)
920 | tickishFloatable t
921 , Just (x, e, ts) <- exprIsLambda_maybe (in_scope_set, id_unf) e
922 = Just (x, e, t:ts)
923
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)])
934 res
935
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'')])
948 res
949
950 exprIsLambda_maybe _ _e
951 = -- pprTrace "exprIsLambda_maybe:Fail" (vcat [ppr _e])
952 Nothing
953
954
955 {- *********************************************************************
956 * *
957 The "push rules"
958 * *
959 ************************************************************************
960
961 Here we implement the "push rules" from FC papers:
962
963 * The push-argument rules, where we can move a coercion past an argument.
964 We have
965 (fun |> co) arg
966 and we want to transform it to
967 (fun arg') |> co'
968 for some suitable co' and tranformed arg'.
969
970 * The PushK rule for data constructors. We have
971 (K e1 .. en) |> co
972 and we want to tranform to
973 (K e1' .. en')
974 by pushing the coercion into the arguments
975 -}
976
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
980 ; case m_co1 of
981 MCo co1 -> do { (args', m_co2) <- pushCoArgs co1 args
982 ; return (arg':args', m_co2) }
983 MRefl -> return (arg':args, MRefl) }
984
985 pushCoArg :: CoercionR -> CoreArg -> Maybe (CoreArg, MCoercion)
986 -- We have (fun |> co) arg, and we want to transform it to
987 -- (fun arg) |> co
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') }
996
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.
1004 pushCoTyArg co ty
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)
1009
1010 | isReflCo co
1011 = Just (ty, MRefl)
1012
1013 | isForAllTy_ty tyL
1014 = ASSERT2( isForAllTy_ty tyR, ppr co $$ ppr ty )
1015 Just (ty `mkCastTy` co1, MCo co2)
1016
1017 | otherwise
1018 = Nothing
1019 where
1020 Pair tyL tyR = coercionKind co
1021 -- co :: tyL ~ tyR
1022 -- tyL = forall (a1 :: k1). ty1
1023 -- tyR = forall (a2 :: k2). ty2
1024
1025 co1 = mkSymCo (mkNthCo Nominal 0 co)
1026 -- co1 :: k2 ~N k1
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.
1030
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
1034
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.
1042 pushCoValArg co
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)
1047
1048 | isReflCo co
1049 = Just (mkRepReflCo arg, MRefl)
1050
1051 | isFunTy tyL
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)
1058
1059 | otherwise
1060 = Nothing
1061 where
1062 arg = funArgTy tyR
1063 Pair tyL tyR = coercionKind co
1064
1065 pushCoercionIntoLambda
1066 :: InScopeSet -> Var -> CoreExpr -> CoercionR -> Maybe (Var, CoreExpr)
1067 -- This implements the Push rule from the paper on coercions
1068 -- (\x. e) |> co
1069 -- ===>
1070 -- (\x'. e |> co')
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')
1082 x
1083 (mkCast (Var x') co1)
1084 in Just (x', substExpr (text "pushCoercionIntoLambda") subst e `mkCast` co2)
1085 | otherwise
1086 = pprTrace "exprIsLambda_maybe: Unexpected lambda in case" (ppr (Lam x e))
1087 Nothing
1088
1089 pushCoDataCon :: DataCon -> [CoreExpr] -> Coercion
1090 -> Maybe (DataCon
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)
1103
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
1111
1112 = let
1113 tc_arity = tyConArity to_tc
1114 dc_univ_tyvars = dataConUnivTyVars dc
1115 dc_ex_tcvars = dataConExTyCoVars dc
1116 arg_tys = dataConRepArgTys dc
1117
1118 non_univ_args = dropList dc_univ_tyvars dc_args
1119 (ex_args, val_args) = splitAtList dc_ex_tcvars non_univ_args
1120
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
1125 dc_univ_tyvars
1126 omegas
1127 dc_ex_tcvars
1128 (map exprToType ex_args)
1129
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)
1133
1134 to_ex_args = map Type to_ex_arg_tys
1135
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 ]
1139 in
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)
1143
1144 | otherwise
1145 = Nothing
1146
1147 where
1148 Pair from_ty to_ty = coercionKind co
1149
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)
1154 --
1155 -- That is,
1156 --
1157 -- collectBindersPushingCo ((\x.e) |> g) === ([x], e |> Nth 1 g)
1158 collectBindersPushingCo e
1159 = go [] e
1160 where
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)
1167
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)
1174
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)
1179 go_lam bs b e co
1180 | isTyVar b
1181 , let Pair tyL tyR = coercionKind co
1182 , ASSERT( isForAllTy_ty tyL )
1183 isForAllTy_ty tyR
1184 , isReflCo (mkNthCo Nominal 0 co) -- See Note [collectBindersPushingCo]
1185 = go_c (b:bs) e (mkInstCo co (mkNomReflCo (mkTyVarTy b)))
1186
1187 | isCoVar b
1188 , let Pair tyL tyR = coercionKind co
1189 , ASSERT( isForAllTy_co tyL )
1190 isForAllTy_co tyR
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)))
1194
1195 | isId b
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
1201
1202 | otherwise = (reverse bs, mkCast (Lam b e) co)
1203
1204 {- Note [collectBindersPushingCo]
1205 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1206 We just look for coercions of form
1207 <type> -> blah
1208 (and similarly for foralls) to keep this function simple. We could do
1209 more elaborate stuff, but it'd involve substitution etc.
1210 -}