No join-point from an INLINE function with wrong arity
[ghc.git] / compiler / coreSyn / CoreArity.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4
5
6 Arity and eta expansion
7 -}
8
9 {-# LANGUAGE CPP #-}
10
11 -- | Arity and eta expansion
12 module CoreArity (
13 manifestArity, joinRhsArity, exprArity, typeArity,
14 exprEtaExpandArity, findRhsArity, CheapFun, etaExpand,
15 etaExpandToJoinPoint, etaExpandToJoinPointRule,
16 exprBotStrictness_maybe
17 ) where
18
19 #include "HsVersions.h"
20
21 import CoreSyn
22 import CoreFVs
23 import CoreUtils
24 import CoreSubst
25 import Demand
26 import Var
27 import VarEnv
28 import Id
29 import Type
30 import TyCon ( initRecTc, checkRecTc )
31 import Coercion
32 import BasicTypes
33 import Unique
34 import DynFlags ( DynFlags, GeneralFlag(..), gopt )
35 import Outputable
36 import FastString
37 import Pair
38 import Util ( debugIsOn )
39
40 {-
41 ************************************************************************
42 * *
43 manifestArity and exprArity
44 * *
45 ************************************************************************
46
47 exprArity is a cheap-and-cheerful version of exprEtaExpandArity.
48 It tells how many things the expression can be applied to before doing
49 any work. It doesn't look inside cases, lets, etc. The idea is that
50 exprEtaExpandArity will do the hard work, leaving something that's easy
51 for exprArity to grapple with. In particular, Simplify uses exprArity to
52 compute the ArityInfo for the Id.
53
54 Originally I thought that it was enough just to look for top-level lambdas, but
55 it isn't. I've seen this
56
57 foo = PrelBase.timesInt
58
59 We want foo to get arity 2 even though the eta-expander will leave it
60 unchanged, in the expectation that it'll be inlined. But occasionally it
61 isn't, because foo is blacklisted (used in a rule).
62
63 Similarly, see the ok_note check in exprEtaExpandArity. So
64 f = __inline_me (\x -> e)
65 won't be eta-expanded.
66
67 And in any case it seems more robust to have exprArity be a bit more intelligent.
68 But note that (\x y z -> f x y z)
69 should have arity 3, regardless of f's arity.
70 -}
71
72 manifestArity :: CoreExpr -> Arity
73 -- ^ manifestArity sees how many leading value lambdas there are,
74 -- after looking through casts
75 manifestArity (Lam v e) | isId v = 1 + manifestArity e
76 | otherwise = manifestArity e
77 manifestArity (Tick t e) | not (tickishIsCode t) = manifestArity e
78 manifestArity (Cast e _) = manifestArity e
79 manifestArity _ = 0
80
81 joinRhsArity :: CoreExpr -> JoinArity
82 -- Join points are supposed to have manifestly-visible
83 -- lambdas at the top: no ticks, no casts, nothing
84 -- Moreover, type lambdas count in JoinArity
85 joinRhsArity (Lam _ e) = 1 + joinRhsArity e
86 joinRhsArity _ = 0
87
88
89 ---------------
90 exprArity :: CoreExpr -> Arity
91 -- ^ An approximate, fast, version of 'exprEtaExpandArity'
92 exprArity e = go e
93 where
94 go (Var v) = idArity v
95 go (Lam x e) | isId x = go e + 1
96 | otherwise = go e
97 go (Tick t e) | not (tickishIsCode t) = go e
98 go (Cast e co) = trim_arity (go e) (pSnd (coercionKind co))
99 -- Note [exprArity invariant]
100 go (App e (Type _)) = go e
101 go (App f a) | exprIsTrivial a = (go f - 1) `max` 0
102 -- See Note [exprArity for applications]
103 -- NB: coercions count as a value argument
104
105 go _ = 0
106
107 trim_arity :: Arity -> Type -> Arity
108 trim_arity arity ty = arity `min` length (typeArity ty)
109
110 ---------------
111 typeArity :: Type -> [OneShotInfo]
112 -- How many value arrows are visible in the type?
113 -- We look through foralls, and newtypes
114 -- See Note [exprArity invariant]
115 typeArity ty
116 = go initRecTc ty
117 where
118 go rec_nts ty
119 | Just (_, ty') <- splitForAllTy_maybe ty
120 = go rec_nts ty'
121
122 | Just (arg,res) <- splitFunTy_maybe ty
123 = typeOneShot arg : go rec_nts res
124
125 | Just (tc,tys) <- splitTyConApp_maybe ty
126 , Just (ty', _) <- instNewTyCon_maybe tc tys
127 , Just rec_nts' <- checkRecTc rec_nts tc -- See Note [Expanding newtypes]
128 -- in TyCon
129 -- , not (isClassTyCon tc) -- Do not eta-expand through newtype classes
130 -- -- See Note [Newtype classes and eta expansion]
131 -- (no longer required)
132 = go rec_nts' ty'
133 -- Important to look through non-recursive newtypes, so that, eg
134 -- (f x) where f has arity 2, f :: Int -> IO ()
135 -- Here we want to get arity 1 for the result!
136 --
137 -- AND through a layer of recursive newtypes
138 -- e.g. newtype Stream m a b = Stream (m (Either b (a, Stream m a b)))
139
140 | otherwise
141 = []
142
143 ---------------
144 exprBotStrictness_maybe :: CoreExpr -> Maybe (Arity, StrictSig)
145 -- A cheap and cheerful function that identifies bottoming functions
146 -- and gives them a suitable strictness signatures. It's used during
147 -- float-out
148 exprBotStrictness_maybe e
149 = case getBotArity (arityType env e) of
150 Nothing -> Nothing
151 Just ar -> Just (ar, sig ar)
152 where
153 env = AE { ae_ped_bot = True, ae_cheap_fn = \ _ _ -> False }
154 sig ar = mkClosedStrictSig (replicate ar topDmd) exnRes
155 -- For this purpose we can be very simple
156 -- exnRes is a bit less aggressive than botRes
157
158 {-
159 Note [exprArity invariant]
160 ~~~~~~~~~~~~~~~~~~~~~~~~~~
161 exprArity has the following invariant:
162
163 (1) If typeArity (exprType e) = n,
164 then manifestArity (etaExpand e n) = n
165
166 That is, etaExpand can always expand as much as typeArity says
167 So the case analysis in etaExpand and in typeArity must match
168
169 (2) exprArity e <= typeArity (exprType e)
170
171 (3) Hence if (exprArity e) = n, then manifestArity (etaExpand e n) = n
172
173 That is, if exprArity says "the arity is n" then etaExpand really
174 can get "n" manifest lambdas to the top.
175
176 Why is this important? Because
177 - In TidyPgm we use exprArity to fix the *final arity* of
178 each top-level Id, and in
179 - In CorePrep we use etaExpand on each rhs, so that the visible lambdas
180 actually match that arity, which in turn means
181 that the StgRhs has the right number of lambdas
182
183 An alternative would be to do the eta-expansion in TidyPgm, at least
184 for top-level bindings, in which case we would not need the trim_arity
185 in exprArity. That is a less local change, so I'm going to leave it for today!
186
187 Note [Newtype classes and eta expansion]
188 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
189 NB: this nasty special case is no longer required, because
190 for newtype classes we don't use the class-op rule mechanism
191 at all. See Note [Single-method classes] in TcInstDcls. SLPJ May 2013
192
193 -------- Old out of date comments, just for interest -----------
194 We have to be careful when eta-expanding through newtypes. In general
195 it's a good idea, but annoyingly it interacts badly with the class-op
196 rule mechanism. Consider
197
198 class C a where { op :: a -> a }
199 instance C b => C [b] where
200 op x = ...
201
202 These translate to
203
204 co :: forall a. (a->a) ~ C a
205
206 $copList :: C b -> [b] -> [b]
207 $copList d x = ...
208
209 $dfList :: C b -> C [b]
210 {-# DFunUnfolding = [$copList] #-}
211 $dfList d = $copList d |> co@[b]
212
213 Now suppose we have:
214
215 dCInt :: C Int
216
217 blah :: [Int] -> [Int]
218 blah = op ($dfList dCInt)
219
220 Now we want the built-in op/$dfList rule will fire to give
221 blah = $copList dCInt
222
223 But with eta-expansion 'blah' might (and in Trac #3772, which is
224 slightly more complicated, does) turn into
225
226 blah = op (\eta. ($dfList dCInt |> sym co) eta)
227
228 and now it is *much* harder for the op/$dfList rule to fire, because
229 exprIsConApp_maybe won't hold of the argument to op. I considered
230 trying to *make* it hold, but it's tricky and I gave up.
231
232 The test simplCore/should_compile/T3722 is an excellent example.
233 -------- End of old out of date comments, just for interest -----------
234
235
236 Note [exprArity for applications]
237 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
238 When we come to an application we check that the arg is trivial.
239 eg f (fac x) does not have arity 2,
240 even if f has arity 3!
241
242 * We require that is trivial rather merely cheap. Suppose f has arity 2.
243 Then f (Just y)
244 has arity 0, because if we gave it arity 1 and then inlined f we'd get
245 let v = Just y in \w. <f-body>
246 which has arity 0. And we try to maintain the invariant that we don't
247 have arity decreases.
248
249 * The `max 0` is important! (\x y -> f x) has arity 2, even if f is
250 unknown, hence arity 0
251
252
253 ************************************************************************
254 * *
255 Computing the "arity" of an expression
256 * *
257 ************************************************************************
258
259 Note [Definition of arity]
260 ~~~~~~~~~~~~~~~~~~~~~~~~~~
261 The "arity" of an expression 'e' is n if
262 applying 'e' to *fewer* than n *value* arguments
263 converges rapidly
264
265 Or, to put it another way
266
267 there is no work lost in duplicating the partial
268 application (e x1 .. x(n-1))
269
270 In the divegent case, no work is lost by duplicating because if the thing
271 is evaluated once, that's the end of the program.
272
273 Or, to put it another way, in any context C
274
275 C[ (\x1 .. xn. e x1 .. xn) ]
276 is as efficient as
277 C[ e ]
278
279 It's all a bit more subtle than it looks:
280
281 Note [One-shot lambdas]
282 ~~~~~~~~~~~~~~~~~~~~~~~
283 Consider one-shot lambdas
284 let x = expensive in \y z -> E
285 We want this to have arity 1 if the \y-abstraction is a 1-shot lambda.
286
287 Note [Dealing with bottom]
288 ~~~~~~~~~~~~~~~~~~~~~~~~~~
289 A Big Deal with computing arities is expressions like
290
291 f = \x -> case x of
292 True -> \s -> e1
293 False -> \s -> e2
294
295 This happens all the time when f :: Bool -> IO ()
296 In this case we do eta-expand, in order to get that \s to the
297 top, and give f arity 2.
298
299 This isn't really right in the presence of seq. Consider
300 (f bot) `seq` 1
301
302 This should diverge! But if we eta-expand, it won't. We ignore this
303 "problem" (unless -fpedantic-bottoms is on), because being scrupulous
304 would lose an important transformation for many programs. (See
305 Trac #5587 for an example.)
306
307 Consider also
308 f = \x -> error "foo"
309 Here, arity 1 is fine. But if it is
310 f = \x -> case x of
311 True -> error "foo"
312 False -> \y -> x+y
313 then we want to get arity 2. Technically, this isn't quite right, because
314 (f True) `seq` 1
315 should diverge, but it'll converge if we eta-expand f. Nevertheless, we
316 do so; it improves some programs significantly, and increasing convergence
317 isn't a bad thing. Hence the ABot/ATop in ArityType.
318
319 So these two transformations aren't always the Right Thing, and we
320 have several tickets reporting unexpected bahaviour resulting from
321 this transformation. So we try to limit it as much as possible:
322
323 (1) Do NOT move a lambda outside a known-bottom case expression
324 case undefined of { (a,b) -> \y -> e }
325 This showed up in Trac #5557
326
327 (2) Do NOT move a lambda outside a case if all the branches of
328 the case are known to return bottom.
329 case x of { (a,b) -> \y -> error "urk" }
330 This case is less important, but the idea is that if the fn is
331 going to diverge eventually anyway then getting the best arity
332 isn't an issue, so we might as well play safe
333
334 (3) Do NOT move a lambda outside a case unless
335 (a) The scrutinee is ok-for-speculation, or
336 (b) more liberally: the scrutinee is cheap (e.g. a variable), and
337 -fpedantic-bottoms is not enforced (see Trac #2915 for an example)
338
339 Of course both (1) and (2) are readily defeated by disguising the bottoms.
340
341 4. Note [Newtype arity]
342 ~~~~~~~~~~~~~~~~~~~~~~~~
343 Non-recursive newtypes are transparent, and should not get in the way.
344 We do (currently) eta-expand recursive newtypes too. So if we have, say
345
346 newtype T = MkT ([T] -> Int)
347
348 Suppose we have
349 e = coerce T f
350 where f has arity 1. Then: etaExpandArity e = 1;
351 that is, etaExpandArity looks through the coerce.
352
353 When we eta-expand e to arity 1: eta_expand 1 e T
354 we want to get: coerce T (\x::[T] -> (coerce ([T]->Int) e) x)
355
356 HOWEVER, note that if you use coerce bogusly you can ge
357 coerce Int negate
358 And since negate has arity 2, you might try to eta expand. But you can't
359 decopose Int to a function type. Hence the final case in eta_expand.
360
361 Note [The state-transformer hack]
362 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
363 Suppose we have
364 f = e
365 where e has arity n. Then, if we know from the context that f has
366 a usage type like
367 t1 -> ... -> tn -1-> t(n+1) -1-> ... -1-> tm -> ...
368 then we can expand the arity to m. This usage type says that
369 any application (x e1 .. en) will be applied to uniquely to (m-n) more args
370 Consider f = \x. let y = <expensive>
371 in case x of
372 True -> foo
373 False -> \(s:RealWorld) -> e
374 where foo has arity 1. Then we want the state hack to
375 apply to foo too, so we can eta expand the case.
376
377 Then we expect that if f is applied to one arg, it'll be applied to two
378 (that's the hack -- we don't really know, and sometimes it's false)
379 See also Id.isOneShotBndr.
380
381 Note [State hack and bottoming functions]
382 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
383 It's a terrible idea to use the state hack on a bottoming function.
384 Here's what happens (Trac #2861):
385
386 f :: String -> IO T
387 f = \p. error "..."
388
389 Eta-expand, using the state hack:
390
391 f = \p. (\s. ((error "...") |> g1) s) |> g2
392 g1 :: IO T ~ (S -> (S,T))
393 g2 :: (S -> (S,T)) ~ IO T
394
395 Extrude the g2
396
397 f' = \p. \s. ((error "...") |> g1) s
398 f = f' |> (String -> g2)
399
400 Discard args for bottomming function
401
402 f' = \p. \s. ((error "...") |> g1 |> g3
403 g3 :: (S -> (S,T)) ~ (S,T)
404
405 Extrude g1.g3
406
407 f'' = \p. \s. (error "...")
408 f' = f'' |> (String -> S -> g1.g3)
409
410 And now we can repeat the whole loop. Aargh! The bug is in applying the
411 state hack to a function which then swallows the argument.
412
413 This arose in another guise in Trac #3959. Here we had
414
415 catch# (throw exn >> return ())
416
417 Note that (throw :: forall a e. Exn e => e -> a) is called with [a = IO ()].
418 After inlining (>>) we get
419
420 catch# (\_. throw {IO ()} exn)
421
422 We must *not* eta-expand to
423
424 catch# (\_ _. throw {...} exn)
425
426 because 'catch#' expects to get a (# _,_ #) after applying its argument to
427 a State#, not another function!
428
429 In short, we use the state hack to allow us to push let inside a lambda,
430 but not to introduce a new lambda.
431
432
433 Note [ArityType]
434 ~~~~~~~~~~~~~~~~
435 ArityType is the result of a compositional analysis on expressions,
436 from which we can decide the real arity of the expression (extracted
437 with function exprEtaExpandArity).
438
439 Here is what the fields mean. If an arbitrary expression 'f' has
440 ArityType 'at', then
441
442 * If at = ABot n, then (f x1..xn) definitely diverges. Partial
443 applications to fewer than n args may *or may not* diverge.
444
445 We allow ourselves to eta-expand bottoming functions, even
446 if doing so may lose some `seq` sharing,
447 let x = <expensive> in \y. error (g x y)
448 ==> \y. let x = <expensive> in error (g x y)
449
450 * If at = ATop as, and n=length as,
451 then expanding 'f' to (\x1..xn. f x1 .. xn) loses no sharing,
452 assuming the calls of f respect the one-shot-ness of
453 its definition.
454
455 NB 'f' is an arbitrary expression, eg (f = g e1 e2). This 'f'
456 can have ArityType as ATop, with length as > 0, only if e1 e2 are
457 themselves.
458
459 * In both cases, f, (f x1), ... (f x1 ... f(n-1)) are definitely
460 really functions, or bottom, but *not* casts from a data type, in
461 at least one case branch. (If it's a function in one case branch but
462 an unsafe cast from a data type in another, the program is bogus.)
463 So eta expansion is dynamically ok; see Note [State hack and
464 bottoming functions], the part about catch#
465
466 Example:
467 f = \x\y. let v = <expensive> in
468 \s(one-shot) \t(one-shot). blah
469 'f' has ArityType [ManyShot,ManyShot,OneShot,OneShot]
470 The one-shot-ness means we can, in effect, push that
471 'let' inside the \st.
472
473
474 Suppose f = \xy. x+y
475 Then f :: AT [False,False] ATop
476 f v :: AT [False] ATop
477 f <expensive> :: AT [] ATop
478
479 -------------------- Main arity code ----------------------------
480 -}
481
482 -- See Note [ArityType]
483 data ArityType = ATop [OneShotInfo] | ABot Arity
484 -- There is always an explicit lambda
485 -- to justify the [OneShot], or the Arity
486
487 vanillaArityType :: ArityType
488 vanillaArityType = ATop [] -- Totally uninformative
489
490 -- ^ The Arity returned is the number of value args the
491 -- expression can be applied to without doing much work
492 exprEtaExpandArity :: DynFlags -> CoreExpr -> Arity
493 -- exprEtaExpandArity is used when eta expanding
494 -- e ==> \xy -> e x y
495 exprEtaExpandArity dflags e
496 = case (arityType env e) of
497 ATop oss -> length oss
498 ABot n -> n
499 where
500 env = AE { ae_cheap_fn = mk_cheap_fn dflags isCheapApp
501 , ae_ped_bot = gopt Opt_PedanticBottoms dflags }
502
503 getBotArity :: ArityType -> Maybe Arity
504 -- Arity of a divergent function
505 getBotArity (ABot n) = Just n
506 getBotArity _ = Nothing
507
508 mk_cheap_fn :: DynFlags -> CheapAppFun -> CheapFun
509 mk_cheap_fn dflags cheap_app
510 | not (gopt Opt_DictsCheap dflags)
511 = \e _ -> exprIsOk cheap_app e
512 | otherwise
513 = \e mb_ty -> exprIsOk cheap_app e
514 || case mb_ty of
515 Nothing -> False
516 Just ty -> isDictLikeTy ty
517
518
519 ----------------------
520 findRhsArity :: DynFlags -> Id -> CoreExpr -> Arity -> Arity
521 -- This implements the fixpoint loop for arity analysis
522 -- See Note [Arity analysis]
523 findRhsArity dflags bndr rhs old_arity
524 = go (rhsEtaExpandArity dflags init_cheap_app rhs)
525 -- We always call exprEtaExpandArity once, but usually
526 -- that produces a result equal to old_arity, and then
527 -- we stop right away (since arities should not decrease)
528 -- Result: the common case is that there is just one iteration
529 where
530 init_cheap_app :: CheapAppFun
531 init_cheap_app fn n_val_args
532 | fn == bndr = True -- On the first pass, this binder gets infinite arity
533 | otherwise = isCheapApp fn n_val_args
534
535 go :: Arity -> Arity
536 go cur_arity
537 | cur_arity <= old_arity = cur_arity
538 | new_arity == cur_arity = cur_arity
539 | otherwise = ASSERT( new_arity < cur_arity )
540 #ifdef DEBUG
541 pprTrace "Exciting arity"
542 (vcat [ ppr bndr <+> ppr cur_arity <+> ppr new_arity
543 , ppr rhs])
544 #endif
545 go new_arity
546 where
547 new_arity = rhsEtaExpandArity dflags cheap_app rhs
548
549 cheap_app :: CheapAppFun
550 cheap_app fn n_val_args
551 | fn == bndr = n_val_args < cur_arity
552 | otherwise = isCheapApp fn n_val_args
553
554 -- ^ The Arity returned is the number of value args the
555 -- expression can be applied to without doing much work
556 rhsEtaExpandArity :: DynFlags -> CheapAppFun -> CoreExpr -> Arity
557 -- exprEtaExpandArity is used when eta expanding
558 -- e ==> \xy -> e x y
559 rhsEtaExpandArity dflags cheap_app e
560 = case (arityType env e) of
561 ATop (os:oss)
562 | isOneShotInfo os || has_lam e -> 1 + length oss
563 -- Don't expand PAPs/thunks
564 -- Note [Eta expanding thunks]
565 | otherwise -> 0
566 ATop [] -> 0
567 ABot n -> n
568 where
569 env = AE { ae_cheap_fn = mk_cheap_fn dflags cheap_app
570 , ae_ped_bot = gopt Opt_PedanticBottoms dflags }
571
572 has_lam (Tick _ e) = has_lam e
573 has_lam (Lam b e) = isId b || has_lam e
574 has_lam _ = False
575
576 {-
577 Note [Arity analysis]
578 ~~~~~~~~~~~~~~~~~~~~~
579 The motivating example for arity analysis is this:
580
581 f = \x. let g = f (x+1)
582 in \y. ...g...
583
584 What arity does f have? Really it should have arity 2, but a naive
585 look at the RHS won't see that. You need a fixpoint analysis which
586 says it has arity "infinity" the first time round.
587
588 This example happens a lot; it first showed up in Andy Gill's thesis,
589 fifteen years ago! It also shows up in the code for 'rnf' on lists
590 in Trac #4138.
591
592 The analysis is easy to achieve because exprEtaExpandArity takes an
593 argument
594 type CheapFun = CoreExpr -> Maybe Type -> Bool
595 used to decide if an expression is cheap enough to push inside a
596 lambda. And exprIsCheap' in turn takes an argument
597 type CheapAppFun = Id -> Int -> Bool
598 which tells when an application is cheap. This makes it easy to
599 write the analysis loop.
600
601 The analysis is cheap-and-cheerful because it doesn't deal with
602 mutual recursion. But the self-recursive case is the important one.
603
604
605 Note [Eta expanding through dictionaries]
606 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
607 If the experimental -fdicts-cheap flag is on, we eta-expand through
608 dictionary bindings. This improves arities. Thereby, it also
609 means that full laziness is less prone to floating out the
610 application of a function to its dictionary arguments, which
611 can thereby lose opportunities for fusion. Example:
612 foo :: Ord a => a -> ...
613 foo = /\a \(d:Ord a). let d' = ...d... in \(x:a). ....
614 -- So foo has arity 1
615
616 f = \x. foo dInt $ bar x
617
618 The (foo DInt) is floated out, and makes ineffective a RULE
619 foo (bar x) = ...
620
621 One could go further and make exprIsCheap reply True to any
622 dictionary-typed expression, but that's more work.
623
624 See Note [Dictionary-like types] in TcType.hs for why we use
625 isDictLikeTy here rather than isDictTy
626
627 Note [Eta expanding thunks]
628 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
629 We don't eta-expand
630 * Trivial RHSs x = y
631 * PAPs x = map g
632 * Thunks f = case y of p -> \x -> blah
633
634 When we see
635 f = case y of p -> \x -> blah
636 should we eta-expand it? Well, if 'x' is a one-shot state token
637 then 'yes' because 'f' will only be applied once. But otherwise
638 we (conservatively) say no. My main reason is to avoid expanding
639 PAPSs
640 f = g d ==> f = \x. g d x
641 because that might in turn make g inline (if it has an inline pragma),
642 which we might not want. After all, INLINE pragmas say "inline only
643 when saturated" so we don't want to be too gung-ho about saturating!
644 -}
645
646 arityLam :: Id -> ArityType -> ArityType
647 arityLam id (ATop as) = ATop (idStateHackOneShotInfo id : as)
648 arityLam _ (ABot n) = ABot (n+1)
649
650 floatIn :: Bool -> ArityType -> ArityType
651 -- We have something like (let x = E in b),
652 -- where b has the given arity type.
653 floatIn _ (ABot n) = ABot n
654 floatIn True (ATop as) = ATop as
655 floatIn False (ATop as) = ATop (takeWhile isOneShotInfo as)
656 -- If E is not cheap, keep arity only for one-shots
657
658 arityApp :: ArityType -> Bool -> ArityType
659 -- Processing (fun arg) where at is the ArityType of fun,
660 -- Knock off an argument and behave like 'let'
661 arityApp (ABot 0) _ = ABot 0
662 arityApp (ABot n) _ = ABot (n-1)
663 arityApp (ATop []) _ = ATop []
664 arityApp (ATop (_:as)) cheap = floatIn cheap (ATop as)
665
666 andArityType :: ArityType -> ArityType -> ArityType -- Used for branches of a 'case'
667 andArityType (ABot n1) (ABot n2) = ABot (n1 `max` n2) -- Note [ABot branches: use max]
668 andArityType (ATop as) (ABot _) = ATop as
669 andArityType (ABot _) (ATop bs) = ATop bs
670 andArityType (ATop as) (ATop bs) = ATop (as `combine` bs)
671 where -- See Note [Combining case branches]
672 combine (a:as) (b:bs) = (a `bestOneShot` b) : combine as bs
673 combine [] bs = takeWhile isOneShotInfo bs
674 combine as [] = takeWhile isOneShotInfo as
675
676 {- Note [ABot branches: use max]
677 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
678 Consider case x of
679 True -> \x. error "urk"
680 False -> \xy. error "urk2"
681
682 Remember: ABot n means "if you apply to n args, it'll definitely diverge".
683 So we need (ABot 2) for the whole thing, the /max/ of the ABot arities.
684
685 Note [Combining case branches]
686 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
687 Consider
688 go = \x. let z = go e0
689 go2 = \x. case x of
690 True -> z
691 False -> \s(one-shot). e1
692 in go2 x
693 We *really* want to eta-expand go and go2.
694 When combining the barnches of the case we have
695 ATop [] `andAT` ATop [OneShotLam]
696 and we want to get ATop [OneShotLam]. But if the inner
697 lambda wasn't one-shot we don't want to do this.
698 (We need a proper arity analysis to justify that.)
699
700 So we combine the best of the two branches, on the (slightly dodgy)
701 basis that if we know one branch is one-shot, then they all must be.
702 -}
703
704 ---------------------------
705 type CheapFun = CoreExpr -> Maybe Type -> Bool
706 -- How to decide if an expression is cheap
707 -- If the Maybe is Just, the type is the type
708 -- of the expression; Nothing means "don't know"
709
710 data ArityEnv
711 = AE { ae_cheap_fn :: CheapFun
712 , ae_ped_bot :: Bool -- True <=> be pedantic about bottoms
713 }
714
715 arityType :: ArityEnv -> CoreExpr -> ArityType
716
717 arityType env (Cast e co)
718 = case arityType env e of
719 ATop os -> ATop (take co_arity os)
720 ABot n -> ABot (n `min` co_arity)
721 where
722 co_arity = length (typeArity (pSnd (coercionKind co)))
723 -- See Note [exprArity invariant] (2); must be true of
724 -- arityType too, since that is how we compute the arity
725 -- of variables, and they in turn affect result of exprArity
726 -- Trac #5441 is a nice demo
727 -- However, do make sure that ATop -> ATop and ABot -> ABot!
728 -- Casts don't affect that part. Getting this wrong provoked #5475
729
730 arityType _ (Var v)
731 | strict_sig <- idStrictness v
732 , not $ isTopSig strict_sig
733 , (ds, res) <- splitStrictSig strict_sig
734 , let arity = length ds
735 = if isBotRes res then ABot arity
736 else ATop (take arity one_shots)
737 | otherwise
738 = ATop (take (idArity v) one_shots)
739 where
740 one_shots :: [OneShotInfo] -- One-shot-ness derived from the type
741 one_shots = typeArity (idType v)
742
743 -- Lambdas; increase arity
744 arityType env (Lam x e)
745 | isId x = arityLam x (arityType env e)
746 | otherwise = arityType env e
747
748 -- Applications; decrease arity, except for types
749 arityType env (App fun (Type _))
750 = arityType env fun
751 arityType env (App fun arg )
752 = arityApp (arityType env fun) (ae_cheap_fn env arg Nothing)
753
754 -- Case/Let; keep arity if either the expression is cheap
755 -- or it's a 1-shot lambda
756 -- The former is not really right for Haskell
757 -- f x = case x of { (a,b) -> \y. e }
758 -- ===>
759 -- f x y = case x of { (a,b) -> e }
760 -- The difference is observable using 'seq'
761 --
762 arityType env (Case scrut _ _ alts)
763 | exprIsBottom scrut || null alts
764 = ABot 0 -- Do not eta expand
765 -- See Note [Dealing with bottom (1)]
766 | otherwise
767 = case alts_type of
768 ABot n | n>0 -> ATop [] -- Don't eta expand
769 | otherwise -> ABot 0 -- if RHS is bottomming
770 -- See Note [Dealing with bottom (2)]
771
772 ATop as | not (ae_ped_bot env) -- See Note [Dealing with bottom (3)]
773 , ae_cheap_fn env scrut Nothing -> ATop as
774 | exprOkForSpeculation scrut -> ATop as
775 | otherwise -> ATop (takeWhile isOneShotInfo as)
776 where
777 alts_type = foldr1 andArityType [arityType env rhs | (_,_,rhs) <- alts]
778
779 arityType env (Let b e)
780 = floatIn (cheap_bind b) (arityType env e)
781 where
782 cheap_bind (NonRec b e) = is_cheap (b,e)
783 cheap_bind (Rec prs) = all is_cheap prs
784 is_cheap (b,e) = ae_cheap_fn env e (Just (idType b))
785
786 arityType env (Tick t e)
787 | not (tickishIsCode t) = arityType env e
788
789 arityType _ _ = vanillaArityType
790
791 {-
792 %************************************************************************
793 %* *
794 The main eta-expander
795 %* *
796 %************************************************************************
797
798 We go for:
799 f = \x1..xn -> N ==> f = \x1..xn y1..ym -> N y1..ym
800 (n >= 0)
801
802 where (in both cases)
803
804 * The xi can include type variables
805
806 * The yi are all value variables
807
808 * N is a NORMAL FORM (i.e. no redexes anywhere)
809 wanting a suitable number of extra args.
810
811 The biggest reason for doing this is for cases like
812
813 f = \x -> case x of
814 True -> \y -> e1
815 False -> \y -> e2
816
817 Here we want to get the lambdas together. A good example is the nofib
818 program fibheaps, which gets 25% more allocation if you don't do this
819 eta-expansion.
820
821 We may have to sandwich some coerces between the lambdas
822 to make the types work. exprEtaExpandArity looks through coerces
823 when computing arity; and etaExpand adds the coerces as necessary when
824 actually computing the expansion.
825
826 Note [No crap in eta-expanded code]
827 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
828 The eta expander is careful not to introduce "crap". In particular,
829 given a CoreExpr satisfying the 'CpeRhs' invariant (in CorePrep), it
830 returns a CoreExpr satisfying the same invariant. See Note [Eta
831 expansion and the CorePrep invariants] in CorePrep.
832
833 This means the eta-expander has to do a bit of on-the-fly
834 simplification but it's not too hard. The alernative, of relying on
835 a subsequent clean-up phase of the Simplifier to de-crapify the result,
836 means you can't really use it in CorePrep, which is painful.
837
838 Note [Eta expansion and SCCs]
839 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
840 Note that SCCs are not treated specially by etaExpand. If we have
841 etaExpand 2 (\x -> scc "foo" e)
842 = (\xy -> (scc "foo" e) y)
843 So the costs of evaluating 'e' (not 'e y') are attributed to "foo"
844
845 Note [Eta expansion and source notes]
846 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
847 CorePrep puts floatable ticks outside of value applications, but not
848 type applications. As a result we might be trying to eta-expand an
849 expression like
850
851 (src<...> v) @a
852
853 which we want to lead to code like
854
855 \x -> src<...> v @a x
856
857 This means that we need to look through type applications and be ready
858 to re-add floats on the top.
859
860 -}
861
862 -- | @etaExpand n e@ returns an expression with
863 -- the same meaning as @e@, but with arity @n@.
864 --
865 -- Given:
866 --
867 -- > e' = etaExpand n e
868 --
869 -- We should have that:
870 --
871 -- > ty = exprType e = exprType e'
872 etaExpand :: Arity -- ^ Result should have this number of value args
873 -> CoreExpr -- ^ Expression to expand
874 -> CoreExpr
875 -- etaExpand arity e = res
876 -- Then 'res' has at least 'arity' lambdas at the top
877 --
878 -- etaExpand deals with for-alls. For example:
879 -- etaExpand 1 E
880 -- where E :: forall a. a -> a
881 -- would return
882 -- (/\b. \y::a -> E b y)
883 --
884 -- It deals with coerces too, though they are now rare
885 -- so perhaps the extra code isn't worth it
886
887 etaExpand n orig_expr
888 = go n orig_expr
889 where
890 -- Strip off existing lambdas and casts
891 -- Note [Eta expansion and SCCs]
892 go 0 expr = expr
893 go n (Lam v body) | isTyVar v = Lam v (go n body)
894 | otherwise = Lam v (go (n-1) body)
895 go n (Cast expr co) = Cast (go n expr) co
896 go n expr
897 = -- pprTrace "ee" (vcat [ppr orig_expr, ppr expr, ppr etas]) $
898 retick $ etaInfoAbs etas (etaInfoApp subst' sexpr etas)
899 where
900 in_scope = mkInScopeSet (exprFreeVars expr)
901 (in_scope', etas) = mkEtaWW n orig_expr in_scope (exprType expr)
902 subst' = mkEmptySubst in_scope'
903
904 -- Find ticks behind type apps.
905 -- See Note [Eta expansion and source notes]
906 (expr', args) = collectArgs expr
907 (ticks, expr'') = stripTicksTop tickishFloatable expr'
908 sexpr = foldl App expr'' args
909 retick expr = foldr mkTick expr ticks
910
911 -- Wrapper Unwrapper
912 --------------
913 data EtaInfo = EtaVar Var -- /\a. [], [] a
914 -- \x. [], [] x
915 | EtaCo Coercion -- [] |> co, [] |> (sym co)
916
917 instance Outputable EtaInfo where
918 ppr (EtaVar v) = text "EtaVar" <+> ppr v
919 ppr (EtaCo co) = text "EtaCo" <+> ppr co
920
921 pushCoercion :: Coercion -> [EtaInfo] -> [EtaInfo]
922 pushCoercion co1 (EtaCo co2 : eis)
923 | isReflCo co = eis
924 | otherwise = EtaCo co : eis
925 where
926 co = co1 `mkTransCo` co2
927
928 pushCoercion co eis = EtaCo co : eis
929
930 --------------
931 etaInfoAbs :: [EtaInfo] -> CoreExpr -> CoreExpr
932 etaInfoAbs [] expr = expr
933 etaInfoAbs (EtaVar v : eis) expr = Lam v (etaInfoAbs eis expr)
934 etaInfoAbs (EtaCo co : eis) expr = Cast (etaInfoAbs eis expr) (mkSymCo co)
935
936 --------------
937 etaInfoApp :: Subst -> CoreExpr -> [EtaInfo] -> CoreExpr
938 -- (etaInfoApp s e eis) returns something equivalent to
939 -- ((substExpr s e) `appliedto` eis)
940
941 etaInfoApp subst (Lam v1 e) (EtaVar v2 : eis)
942 = etaInfoApp (CoreSubst.extendSubstWithVar subst v1 v2) e eis
943
944 etaInfoApp subst (Cast e co1) eis
945 = etaInfoApp subst e (pushCoercion co' eis)
946 where
947 co' = CoreSubst.substCo subst co1
948
949 etaInfoApp subst (Case e b ty alts) eis
950 = Case (subst_expr subst e) b1 (mk_alts_ty (CoreSubst.substTy subst ty) eis) alts'
951 where
952 (subst1, b1) = substBndr subst b
953 alts' = map subst_alt alts
954 subst_alt (con, bs, rhs) = (con, bs', etaInfoApp subst2 rhs eis)
955 where
956 (subst2,bs') = substBndrs subst1 bs
957
958 mk_alts_ty ty [] = ty
959 mk_alts_ty ty (EtaVar v : eis) = mk_alts_ty (applyTypeToArg ty (varToCoreExpr v)) eis
960 mk_alts_ty _ (EtaCo co : eis) = mk_alts_ty (pSnd (coercionKind co)) eis
961
962 etaInfoApp subst (Let b e) eis
963 = Let b' (etaInfoApp subst' e eis)
964 where
965 (subst', b') = etaInfoAppBind subst b eis
966
967 etaInfoApp subst (Tick t e) eis
968 = Tick (substTickish subst t) (etaInfoApp subst e eis)
969
970 etaInfoApp subst expr _
971 | (Var fun, _) <- collectArgs expr
972 , Var fun' <- lookupIdSubst (text "etaInfoApp" <+> ppr fun) subst fun
973 , isJoinId fun'
974 = subst_expr subst expr
975
976 etaInfoApp subst e eis
977 = go (subst_expr subst e) eis
978 where
979 go e [] = e
980 go e (EtaVar v : eis) = go (App e (varToCoreExpr v)) eis
981 go e (EtaCo co : eis) = go (Cast e co) eis
982
983 --------------
984 -- | Apply the eta info to a local binding. Mostly delegates to
985 -- `etaInfoAppLocalBndr` and `etaInfoAppRhs`.
986 etaInfoAppBind :: Subst -> CoreBind -> [EtaInfo] -> (Subst, CoreBind)
987 etaInfoAppBind subst (NonRec bndr rhs) eis
988 = (subst', NonRec bndr' rhs')
989 where
990 bndr_w_new_type = etaInfoAppLocalBndr bndr eis
991 (subst', bndr1) = substBndr subst bndr_w_new_type
992 rhs' = etaInfoAppRhs subst bndr1 rhs eis
993 bndr' | isJoinId bndr = bndr1 `setIdArity` manifestArity rhs'
994 -- Arity may have changed
995 -- (see etaInfoAppRhs example)
996 | otherwise = bndr1
997 etaInfoAppBind subst (Rec pairs) eis
998 = (subst', Rec (bndrs' `zip` rhss'))
999 where
1000 (bndrs, rhss) = unzip pairs
1001 bndrs_w_new_types = map (\bndr -> etaInfoAppLocalBndr bndr eis) bndrs
1002 (subst', bndrs1) = substRecBndrs subst bndrs_w_new_types
1003 rhss' = zipWith process bndrs1 rhss
1004 process bndr' rhs = etaInfoAppRhs subst' bndr' rhs eis
1005 bndrs' | isJoinId (head bndrs)
1006 = [ bndr1 `setIdArity` manifestArity rhs'
1007 | (bndr1, rhs') <- bndrs1 `zip` rhss' ]
1008 -- Arities may have changed
1009 -- (see etaInfoAppRhs example)
1010 | otherwise
1011 = bndrs1
1012
1013 --------------
1014 -- | Apply the eta info to a binder's RHS. Only interesting for a join point,
1015 -- where we might have this:
1016 -- join j :: a -> [a] -> [a]
1017 -- j x = \xs -> x : xs in jump j z
1018 -- Eta-expanding produces this:
1019 -- \ys -> (join j :: a -> [a] -> [a]
1020 -- j x = \xs -> x : xs in jump j z) ys
1021 -- Now when we push the application to ys inward (see Note [No crap in
1022 -- eta-expanded code]), it goes to the body of the RHS of the join point (after
1023 -- the lambda x!):
1024 -- \ys -> join j :: a -> [a]
1025 -- j x = x : ys in jump j z
1026 -- Note that the type and arity of j have both changed.
1027 etaInfoAppRhs :: Subst -> CoreBndr -> CoreExpr -> [EtaInfo] -> CoreExpr
1028 etaInfoAppRhs subst bndr expr eis
1029 | Just arity <- isJoinId_maybe bndr
1030 = do_join_point arity
1031 | otherwise
1032 = subst_expr subst expr
1033 where
1034 do_join_point arity = mkLams join_bndrs' join_body'
1035 where
1036 (join_bndrs, join_body) = collectNBinders arity expr
1037 (subst', join_bndrs') = substBndrs subst join_bndrs
1038 join_body' = etaInfoApp subst' join_body eis
1039
1040
1041 --------------
1042 -- | Apply the eta info to a local binder. A join point will have the EtaInfos
1043 -- applied to its RHS, so its type may change. See comment on etaInfoAppRhs for
1044 -- an example. See Note [No crap in eta-expanded code] for why all this is
1045 -- necessary.
1046 etaInfoAppLocalBndr :: CoreBndr -> [EtaInfo] -> CoreBndr
1047 etaInfoAppLocalBndr bndr orig_eis
1048 = case isJoinId_maybe bndr of
1049 Just arity -> bndr `setIdType` modifyJoinResTy arity (app orig_eis) ty
1050 Nothing -> bndr
1051 where
1052 ty = idType bndr
1053
1054 -- | Apply the given EtaInfos to the result type of the join point.
1055 app :: [EtaInfo] -- To apply
1056 -> Type -- Result type of join point
1057 -> Type -- New result type
1058 app [] ty
1059 = ty
1060 app (EtaVar v : eis) ty
1061 | isId v = app eis (funResultTy ty)
1062 | otherwise = app eis (piResultTy ty (mkTyVarTy v))
1063 app (EtaCo co : eis) ty
1064 = ASSERT2(from_ty `eqType` ty, fsep ([text "can't apply", ppr orig_eis,
1065 text "to", ppr bndr <+> dcolon <+>
1066 ppr (idType bndr)]))
1067 app eis to_ty
1068 where
1069 Pair from_ty to_ty = coercionKind co
1070
1071 --------------
1072 mkEtaWW :: Arity -> CoreExpr -> InScopeSet -> Type
1073 -> (InScopeSet, [EtaInfo])
1074 -- EtaInfo contains fresh variables,
1075 -- not free in the incoming CoreExpr
1076 -- Outgoing InScopeSet includes the EtaInfo vars
1077 -- and the original free vars
1078
1079 mkEtaWW orig_n orig_expr in_scope orig_ty
1080 = go orig_n empty_subst orig_ty []
1081 where
1082 empty_subst = mkEmptyTCvSubst in_scope
1083
1084 go n subst ty eis -- See Note [exprArity invariant]
1085 | n == 0
1086 = (getTCvInScope subst, reverse eis)
1087
1088 | Just (tv,ty') <- splitForAllTy_maybe ty
1089 , let (subst', tv') = Type.substTyVarBndr subst tv
1090 -- Avoid free vars of the original expression
1091 = go n subst' ty' (EtaVar tv' : eis)
1092
1093 | Just (arg_ty, res_ty) <- splitFunTy_maybe ty
1094 , not (isTypeLevPoly arg_ty)
1095 -- See Note [Levity polymorphism invariants] in CoreSyn
1096 -- See also test case typecheck/should_run/EtaExpandLevPoly
1097
1098 , let (subst', eta_id') = freshEtaId n subst arg_ty
1099 -- Avoid free vars of the original expression
1100 = go (n-1) subst' res_ty (EtaVar eta_id' : eis)
1101
1102 | Just (co, ty') <- topNormaliseNewType_maybe ty
1103 = -- Given this:
1104 -- newtype T = MkT ([T] -> Int)
1105 -- Consider eta-expanding this
1106 -- eta_expand 1 e T
1107 -- We want to get
1108 -- coerce T (\x::[T] -> (coerce ([T]->Int) e) x)
1109 go n subst ty' (EtaCo co : eis)
1110
1111 | otherwise -- We have an expression of arity > 0,
1112 -- but its type isn't a function, or a binder
1113 -- is levity-polymorphic
1114 = WARN( True, (ppr orig_n <+> ppr orig_ty) $$ ppr orig_expr )
1115 (getTCvInScope subst, reverse eis)
1116 -- This *can* legitmately happen:
1117 -- e.g. coerce Int (\x. x) Essentially the programmer is
1118 -- playing fast and loose with types (Happy does this a lot).
1119 -- So we simply decline to eta-expand. Otherwise we'd end up
1120 -- with an explicit lambda having a non-function type
1121
1122
1123
1124 --------------
1125 -- Don't use short-cutting substitution - we may be changing the types of join
1126 -- points, so applying the in-scope set is necessary
1127 -- TODO Check if we actually *are* changing any join points' types
1128
1129 subst_expr :: Subst -> CoreExpr -> CoreExpr
1130 subst_expr = substExpr (text "CoreArity:substExpr")
1131
1132
1133 --------------
1134
1135 -- | Split an expression into the given number of binders and a body,
1136 -- eta-expanding if necessary. Counts value *and* type binders.
1137 etaExpandToJoinPoint :: JoinArity -> CoreExpr -> ([CoreBndr], CoreExpr)
1138 etaExpandToJoinPoint join_arity expr
1139 = go join_arity [] expr
1140 where
1141 go 0 rev_bs e = (reverse rev_bs, e)
1142 go n rev_bs (Lam b e) = go (n-1) (b : rev_bs) e
1143 go n rev_bs e = case etaBodyForJoinPoint n e of
1144 (bs, e') -> (reverse rev_bs ++ bs, e')
1145
1146 etaExpandToJoinPointRule :: JoinArity -> CoreRule -> CoreRule
1147 etaExpandToJoinPointRule _ rule@(BuiltinRule {})
1148 = WARN(True, (sep [text "Can't eta-expand built-in rule:", ppr rule]))
1149 -- How did a local binding get a built-in rule anyway? Probably a plugin.
1150 rule
1151 etaExpandToJoinPointRule join_arity rule@(Rule { ru_bndrs = bndrs, ru_rhs = rhs
1152 , ru_args = args })
1153 | need_args == 0
1154 = rule
1155 | need_args < 0
1156 = pprPanic "etaExpandToJoinPointRule" (ppr join_arity $$ ppr rule)
1157 | otherwise
1158 = rule { ru_bndrs = bndrs ++ new_bndrs, ru_args = args ++ new_args
1159 , ru_rhs = new_rhs }
1160 where
1161 need_args = join_arity - length args
1162 (new_bndrs, new_rhs) = etaBodyForJoinPoint need_args rhs
1163 new_args = varsToCoreExprs new_bndrs
1164
1165 -- Adds as many binders as asked for; assumes expr is not a lambda
1166 etaBodyForJoinPoint :: Int -> CoreExpr -> ([CoreBndr], CoreExpr)
1167 etaBodyForJoinPoint need_args body
1168 = go need_args (exprType body) (init_subst body) [] body
1169 where
1170 go 0 _ _ rev_bs e
1171 = (reverse rev_bs, e)
1172 go n ty subst rev_bs e
1173 | Just (tv, res_ty) <- splitForAllTy_maybe ty
1174 , let (subst', tv') = Type.substTyVarBndr subst tv
1175 = go (n-1) res_ty subst' (tv' : rev_bs) (e `App` Type (mkTyVarTy tv'))
1176 | Just (arg_ty, res_ty) <- splitFunTy_maybe ty
1177 , let (subst', b) = freshEtaId n subst arg_ty
1178 = go (n-1) res_ty subst' (b : rev_bs) (e `App` Var b)
1179 | otherwise
1180 = pprPanic "etaBodyForJoinPoint" $ int need_args $$
1181 ppr body $$ ppr (exprType body)
1182
1183 init_subst e = mkEmptyTCvSubst (mkInScopeSet (exprFreeVars e))
1184
1185 --------------
1186 freshEtaId :: Int -> TCvSubst -> Type -> (TCvSubst, Id)
1187 -- Make a fresh Id, with specified type (after applying substitution)
1188 -- It should be "fresh" in the sense that it's not in the in-scope set
1189 -- of the TvSubstEnv; and it should itself then be added to the in-scope
1190 -- set of the TvSubstEnv
1191 --
1192 -- The Int is just a reasonable starting point for generating a unique;
1193 -- it does not necessarily have to be unique itself.
1194 freshEtaId n subst ty
1195 = (subst', eta_id')
1196 where
1197 ty' = Type.substTy subst ty
1198 eta_id' = uniqAway (getTCvInScope subst) $
1199 mkSysLocalOrCoVar (fsLit "eta") (mkBuiltinUnique n) ty'
1200 subst' = extendTCvInScope subst eta_id'