never executed always true always false
1 {-# LANGUAGE BangPatterns #-}
2
3 {-# LANGUAGE DeriveFunctor #-}
4
5 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
6
7 module GHC.Tc.Solver.Rewrite(
8 rewrite, rewriteKind, rewriteArgsNom,
9 rewriteType
10 ) where
11
12 import GHC.Prelude
13
14 import GHC.Core.TyCo.Ppr ( pprTyVar )
15 import GHC.Tc.Types ( TcGblEnv(tcg_tc_plugin_rewriters),
16 TcPluginRewriter, TcPluginRewriteResult(..),
17 RewriteEnv(..),
18 runTcPluginM )
19 import GHC.Tc.Types.Constraint
20 import GHC.Core.Predicate
21 import GHC.Tc.Utils.TcType
22 import GHC.Core.Type
23 import GHC.Tc.Types.Evidence
24 import GHC.Core.TyCon
25 import GHC.Core.TyCo.Rep -- performs delicate algorithm on types
26 import GHC.Core.Coercion
27 import GHC.Core.Reduction
28 import GHC.Types.Unique.FM
29 import GHC.Types.Var
30 import GHC.Types.Var.Set
31 import GHC.Types.Var.Env
32 import GHC.Driver.Session
33 import GHC.Utils.Outputable
34 import GHC.Utils.Panic
35 import GHC.Utils.Panic.Plain
36 import GHC.Tc.Solver.Monad as TcS
37 import GHC.Tc.Solver.Types
38 import GHC.Utils.Misc
39 import GHC.Data.Maybe
40 import GHC.Exts (oneShot)
41 import Control.Monad
42 import GHC.Utils.Monad ( zipWith3M )
43 import Data.List.NonEmpty ( NonEmpty(..) )
44 import Control.Applicative (liftA3)
45 import GHC.Builtin.Types.Prim (tYPETyCon)
46
47 {-
48 ************************************************************************
49 * *
50 * RewriteEnv & RewriteM
51 * The rewriting environment & monad
52 * *
53 ************************************************************************
54 -}
55
56 -- | The 'RewriteM' monad is a wrapper around 'TcS' with a 'RewriteEnv'
57 newtype RewriteM a
58 = RewriteM { runRewriteM :: RewriteEnv -> TcS a }
59 deriving (Functor)
60
61 -- | Smart constructor for 'RewriteM', as describe in Note [The one-shot state
62 -- monad trick] in "GHC.Utils.Monad".
63 mkRewriteM :: (RewriteEnv -> TcS a) -> RewriteM a
64 mkRewriteM f = RewriteM (oneShot f)
65 {-# INLINE mkRewriteM #-}
66
67 instance Monad RewriteM where
68 m >>= k = mkRewriteM $ \env ->
69 do { a <- runRewriteM m env
70 ; runRewriteM (k a) env }
71
72 instance Applicative RewriteM where
73 pure x = mkRewriteM $ \_ -> pure x
74 (<*>) = ap
75
76 instance HasDynFlags RewriteM where
77 getDynFlags = liftTcS getDynFlags
78
79 liftTcS :: TcS a -> RewriteM a
80 liftTcS thing_inside
81 = mkRewriteM $ \_ -> thing_inside
82
83 -- convenient wrapper when you have a CtEvidence describing
84 -- the rewriting operation
85 runRewriteCtEv :: CtEvidence -> RewriteM a -> TcS a
86 runRewriteCtEv ev
87 = runRewrite (ctEvLoc ev) (ctEvFlavour ev) (ctEvEqRel ev)
88
89 -- Run thing_inside (which does the rewriting)
90 runRewrite :: CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS a
91 runRewrite loc flav eq_rel thing_inside
92 = runRewriteM thing_inside fmode
93 where
94 fmode = FE { fe_loc = loc
95 , fe_flavour = flav
96 , fe_eq_rel = eq_rel }
97
98 traceRewriteM :: String -> SDoc -> RewriteM ()
99 traceRewriteM herald doc = liftTcS $ traceTcS herald doc
100 {-# INLINE traceRewriteM #-} -- see Note [INLINE conditional tracing utilities]
101
102 getRewriteEnv :: RewriteM RewriteEnv
103 getRewriteEnv
104 = mkRewriteM $ \env -> return env
105
106 getRewriteEnvField :: (RewriteEnv -> a) -> RewriteM a
107 getRewriteEnvField accessor
108 = mkRewriteM $ \env -> return (accessor env)
109
110 getEqRel :: RewriteM EqRel
111 getEqRel = getRewriteEnvField fe_eq_rel
112
113 getRole :: RewriteM Role
114 getRole = eqRelRole <$> getEqRel
115
116 getFlavour :: RewriteM CtFlavour
117 getFlavour = getRewriteEnvField fe_flavour
118
119 getFlavourRole :: RewriteM CtFlavourRole
120 getFlavourRole
121 = do { flavour <- getFlavour
122 ; eq_rel <- getEqRel
123 ; return (flavour, eq_rel) }
124
125 getLoc :: RewriteM CtLoc
126 getLoc = getRewriteEnvField fe_loc
127
128 checkStackDepth :: Type -> RewriteM ()
129 checkStackDepth ty
130 = do { loc <- getLoc
131 ; liftTcS $ checkReductionDepth loc ty }
132
133 -- | Change the 'EqRel' in a 'RewriteM'.
134 setEqRel :: EqRel -> RewriteM a -> RewriteM a
135 setEqRel new_eq_rel thing_inside
136 = mkRewriteM $ \env ->
137 if new_eq_rel == fe_eq_rel env
138 then runRewriteM thing_inside env
139 else runRewriteM thing_inside (env { fe_eq_rel = new_eq_rel })
140 {-# INLINE setEqRel #-}
141
142 -- | Make sure that rewriting actually produces a coercion (in other
143 -- words, make sure our flavour is not Derived)
144 -- Note [No derived kind equalities]
145 noBogusCoercions :: RewriteM a -> RewriteM a
146 noBogusCoercions thing_inside
147 = mkRewriteM $ \env ->
148 -- No new thunk is made if the flavour hasn't changed (note the bang).
149 let !env' = case fe_flavour env of
150 Derived -> env { fe_flavour = Wanted WDeriv }
151 _ -> env
152 in
153 runRewriteM thing_inside env'
154
155 bumpDepth :: RewriteM a -> RewriteM a
156 bumpDepth (RewriteM thing_inside)
157 = mkRewriteM $ \env -> do
158 -- bumpDepth can be called a lot during rewriting so we force the
159 -- new env to avoid accumulating thunks.
160 { let !env' = env { fe_loc = bumpCtLocDepth (fe_loc env) }
161 ; thing_inside env' }
162
163 {-
164 Note [Rewriter EqRels]
165 ~~~~~~~~~~~~~~~~~~~~~~~
166 When rewriting, we need to know which equality relation -- nominal
167 or representation -- we should be respecting. The only difference is
168 that we rewrite variables by representational equalities when fe_eq_rel
169 is ReprEq, and that we unwrap newtypes when rewriting w.r.t.
170 representational equality.
171
172 Note [Rewriter CtLoc]
173 ~~~~~~~~~~~~~~~~~~~~~~
174 The rewriter does eager type-family reduction.
175 Type families might loop, and we
176 don't want GHC to do so. A natural solution is to have a bounded depth
177 to these processes. A central difficulty is that such a solution isn't
178 quite compositional. For example, say it takes F Int 10 steps to get to Bool.
179 How many steps does it take to get from F Int -> F Int to Bool -> Bool?
180 10? 20? What about getting from Const Char (F Int) to Char? 11? 1? Hard to
181 know and hard to track. So, we punt, essentially. We store a CtLoc in
182 the RewriteEnv and just update the environment when recurring. In the
183 TyConApp case, where there may be multiple type families to rewrite,
184 we just copy the current CtLoc into each branch. If any branch hits the
185 stack limit, then the whole thing fails.
186
187 A consequence of this is that setting the stack limits appropriately
188 will be essentially impossible. So, the official recommendation if a
189 stack limit is hit is to disable the check entirely. Otherwise, there
190 will be baffling, unpredictable errors.
191
192 Note [Phantoms in the rewriter]
193 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
194 Suppose we have
195
196 data Proxy p = Proxy
197
198 and we're rewriting (Proxy ty) w.r.t. ReprEq. Then, we know that `ty`
199 is really irrelevant -- it will be ignored when solving for representational
200 equality later on. So, we omit rewriting `ty` entirely. This may
201 violate the expectation of "xi"s for a bit, but the canonicaliser will
202 soon throw out the phantoms when decomposing a TyConApp. (Or, the
203 canonicaliser will emit an insoluble, in which case we get
204 a better error message anyway.)
205
206 Note [No derived kind equalities]
207 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
208 A kind-level coercion can appear in types, via mkCastTy. So, whenever
209 we are generating a coercion in a dependent context (in other words,
210 in a kind) we need to make sure that our flavour is never Derived
211 (as Derived constraints have no evidence). The noBogusCoercions function
212 changes the flavour from Derived just for this purpose.
213
214 -}
215
216 {- *********************************************************************
217 * *
218 * Externally callable rewriting functions *
219 * *
220 ************************************************************************
221 -}
222
223 -- | See Note [Rewriting].
224 -- If (xi, co) <- rewrite mode ev ty, then co :: xi ~r ty
225 -- where r is the role in @ev@.
226 rewrite :: CtEvidence -> TcType
227 -> TcS Reduction
228 rewrite ev ty
229 = do { traceTcS "rewrite {" (ppr ty)
230 ; redn <- runRewriteCtEv ev (rewrite_one ty)
231 ; traceTcS "rewrite }" (ppr $ reductionReducedType redn)
232 ; return redn }
233
234 -- specialized to rewriting kinds: never Derived, always Nominal
235 -- See Note [No derived kind equalities]
236 -- See Note [Rewriting]
237 rewriteKind :: CtLoc -> CtFlavour -> TcType -> TcS ReductionN
238 rewriteKind loc flav ty
239 = do { traceTcS "rewriteKind {" (ppr flav <+> ppr ty)
240 ; let flav' = case flav of
241 Derived -> Wanted WDeriv -- the WDeriv/WOnly choice matters not
242 _ -> flav
243 ; redn <- runRewrite loc flav' NomEq (rewrite_one ty)
244 ; traceTcS "rewriteKind }" (ppr redn) -- the coercion inside the reduction is never a panic
245 ; return redn }
246
247 -- See Note [Rewriting]
248 rewriteArgsNom :: CtEvidence -> TyCon -> [TcType]
249 -> TcS Reductions
250 -- Externally-callable, hence runRewrite
251 -- Rewrite a vector of types all at once; in fact they are
252 -- always the arguments of type family or class, so
253 -- ctEvFlavour ev = Nominal
254 -- and we want to rewrite all at nominal role
255 -- The kind passed in is the kind of the type family or class, call it T
256 -- The kind of T args must be constant (i.e. not depend on the args)
257 --
258 -- For Derived constraints the returned coercion may be undefined
259 -- because rewriting may use a Derived equality ([D] a ~ ty)
260 rewriteArgsNom ev tc tys
261 = do { traceTcS "rewrite_args {" (vcat (map ppr tys))
262 ; ArgsReductions redns@(Reductions _ tys') kind_co
263 <- runRewriteCtEv ev (rewrite_args_tc tc Nothing tys)
264 ; massert (isReflMCo kind_co)
265 ; traceTcS "rewrite }" (vcat (map ppr tys'))
266 ; return redns }
267
268 -- | Rewrite a type w.r.t. nominal equality. This is useful to rewrite
269 -- a type w.r.t. any givens. It does not do type-family reduction. This
270 -- will never emit new constraints. Call this when the inert set contains
271 -- only givens.
272 rewriteType :: CtLoc -> TcType -> TcS TcType
273 rewriteType loc ty
274 = do { redn <- runRewrite loc Given NomEq $
275 rewrite_one ty
276 -- use Given flavor so that it is rewritten
277 -- only w.r.t. Givens, never Wanteds/Deriveds
278 -- (Shouldn't matter, if only Givens are present
279 -- anyway)
280 ; return $ reductionReducedType redn }
281
282 {- *********************************************************************
283 * *
284 * The main rewriting functions
285 * *
286 ********************************************************************* -}
287
288 {- Note [Rewriting]
289 ~~~~~~~~~~~~~~~~~~~~
290 rewrite ty ==> Reduction co xi
291 where
292 xi has no reducible type functions
293 has no skolems that are mapped in the inert set
294 has no filled-in metavariables
295 co :: ty ~ xi (coercions in reductions are always left-to-right)
296
297 Key invariants:
298 (F0) co :: zonk(ty') ~ xi where zonk(ty') ~ zonk(ty)
299 (F1) tcTypeKind(xi) succeeds and returns a fully zonked kind
300 (F2) tcTypeKind(xi) `eqType` zonk(tcTypeKind(ty))
301
302 Note that it is rewrite's job to try to reduce *every type function it sees*.
303
304 Rewriting also:
305 * zonks, removing any metavariables, and
306 * applies the substitution embodied in the inert set
307
308 Because rewriting zonks and the returned coercion ("co" above) is also
309 zonked, it's possible that (co :: ty ~ xi) isn't quite true. So, instead,
310 we can rely on this fact:
311
312 (F0) co :: zonk(ty') ~ xi, where zonk(ty') ~ zonk(ty)
313
314 Note that the right-hand type of co is *always* precisely xi. The left-hand
315 type may or may not be ty, however: if ty has unzonked filled-in metavariables,
316 then the left-hand type of co will be the zonk-equal to ty.
317 It is for this reason that we occasionally have to explicitly zonk,
318 when (co :: ty ~ xi) is important even before we zonk the whole program.
319 For example, see the RTRNotFollowed case in rewriteTyVar.
320
321 Why have these invariants on rewriting? Because we sometimes use tcTypeKind
322 during canonicalisation, and we want this kind to be zonked (e.g., see
323 GHC.Tc.Solver.Canonical.canEqCanLHS).
324
325 Rewriting is always homogeneous. That is, the kind of the result of rewriting is
326 always the same as the kind of the input, modulo zonking. More formally:
327
328 (F2) zonk(tcTypeKind(ty)) `eqType` tcTypeKind(xi)
329
330 This invariant means that the kind of a rewritten type might not itself be rewritten.
331
332 Note that we prefer to leave type synonyms unexpanded when possible,
333 so when the rewriter encounters one, it first asks whether its
334 transitive expansion contains any type function applications or is
335 forgetful -- that is, omits one or more type variables in its RHS. If so,
336 it expands the synonym and proceeds; if not, it simply returns the
337 unexpanded synonym. See also Note [Rewriting synonyms].
338
339 Where do we actually perform rewriting within a type? See Note [Rewritable] in
340 GHC.Tc.Solver.InertSet.
341
342 Note [rewrite_args performance]
343 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
344 In programs with lots of type-level evaluation, rewrite_args becomes
345 part of a tight loop. For example, see test perf/compiler/T9872a, which
346 calls rewrite_args a whopping 7,106,808 times. It is thus important
347 that rewrite_args be efficient.
348
349 Performance testing showed that the current implementation is indeed
350 efficient. It's critically important that zipWithAndUnzipM be
351 specialized to TcS, and it's also quite helpful to actually `inline`
352 it. On test T9872a, here are the allocation stats (Dec 16, 2014):
353
354 * Unspecialized, uninlined: 8,472,613,440 bytes allocated in the heap
355 * Specialized, uninlined: 6,639,253,488 bytes allocated in the heap
356 * Specialized, inlined: 6,281,539,792 bytes allocated in the heap
357
358 To improve performance even further, rewrite_args_nom is split off
359 from rewrite_args, as nominal equality is the common case. This would
360 be natural to write using mapAndUnzipM, but even inlined, that function
361 is not as performant as a hand-written loop.
362
363 * mapAndUnzipM, inlined: 7,463,047,432 bytes allocated in the heap
364 * hand-written recursion: 5,848,602,848 bytes allocated in the heap
365
366 If you make any change here, pay close attention to the T9872{a,b,c} tests
367 and T5321Fun.
368
369 If we need to make this yet more performant, a possible way forward is to
370 duplicate the rewriter code for the nominal case, and make that case
371 faster. This doesn't seem quite worth it, yet.
372
373 Note [rewrite_exact_fam_app performance]
374 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
375 Once we've got a rewritten rhs, we extend the famapp-cache to record
376 the result. Doing so can save lots of work when the same redex shows up more
377 than once. Note that we record the link from the redex all the way to its
378 *final* value, not just the single step reduction.
379
380 If we can reduce the family application right away (the first call
381 to try_to_reduce), we do *not* add to the cache. There are two possibilities
382 here: 1) we just read the result from the cache, or 2) we used one type
383 family instance. In either case, recording the result in the cache doesn't
384 save much effort the next time around. And adding to the cache here is
385 actually disastrous: it more than doubles the allocations for T9872a. So
386 we skip adding to the cache here.
387 -}
388
389 {-# INLINE rewrite_args_tc #-}
390 rewrite_args_tc
391 :: TyCon -- T
392 -> Maybe [Role] -- Nothing: ambient role is Nominal; all args are Nominal
393 -- Otherwise: no assumptions; use roles provided
394 -> [Type]
395 -> RewriteM ArgsReductions -- See the commentary on rewrite_args
396 rewrite_args_tc tc = rewrite_args all_bndrs any_named_bndrs inner_ki emptyVarSet
397 -- NB: TyCon kinds are always closed
398 where
399 -- There are many bang patterns in here. It's been observed that they
400 -- greatly improve performance of an optimized build.
401 -- The T9872 test cases are good witnesses of this fact.
402
403 (bndrs, named)
404 = ty_con_binders_ty_binders' (tyConBinders tc)
405 -- it's possible that the result kind has arrows (for, e.g., a type family)
406 -- so we must split it
407 (inner_bndrs, inner_ki, inner_named) = split_pi_tys' (tyConResKind tc)
408 !all_bndrs = bndrs `chkAppend` inner_bndrs
409 !any_named_bndrs = named || inner_named
410 -- NB: Those bangs there drop allocations in T9872{a,c,d} by 8%.
411
412 {-# INLINE rewrite_args #-}
413 rewrite_args :: [TyCoBinder] -> Bool -- Binders, and True iff any of them are
414 -- named.
415 -> Kind -> TcTyCoVarSet -- function kind; kind's free vars
416 -> Maybe [Role] -> [Type] -- these are in 1-to-1 correspondence
417 -- Nothing: use all Nominal
418 -> RewriteM ArgsReductions
419 -- This function returns ArgsReductions (Reductions cos xis) res_co
420 -- coercions: co_i :: ty_i ~ xi_i, at roles given
421 -- types: xi_i
422 -- coercion: res_co :: tcTypeKind(fun tys) ~N tcTypeKind(fun xis)
423 -- That is, the result coercion relates the kind of some function (whose kind is
424 -- passed as the first parameter) instantiated at tys to the kind of that
425 -- function instantiated at the xis. This is useful in keeping rewriting
426 -- homogeneous. The list of roles must be at least as long as the list of
427 -- types.
428 rewrite_args orig_binders
429 any_named_bndrs
430 orig_inner_ki
431 orig_fvs
432 orig_m_roles
433 orig_tys
434 = case (orig_m_roles, any_named_bndrs) of
435 (Nothing, False) -> rewrite_args_fast orig_tys
436 _ -> rewrite_args_slow orig_binders orig_inner_ki orig_fvs orig_roles orig_tys
437 where orig_roles = fromMaybe (repeat Nominal) orig_m_roles
438
439 {-# INLINE rewrite_args_fast #-}
440 -- | fast path rewrite_args, in which none of the binders are named and
441 -- therefore we can avoid tracking a lifting context.
442 rewrite_args_fast :: [Type] -> RewriteM ArgsReductions
443 rewrite_args_fast orig_tys
444 = fmap finish (iterate orig_tys)
445 where
446
447 iterate :: [Type] -> RewriteM Reductions
448 iterate (ty : tys) = do
449 Reduction co xi <- rewrite_one ty
450 Reductions cos xis <- iterate tys
451 pure $ Reductions (co : cos) (xi : xis)
452 iterate [] = pure $ Reductions [] []
453
454 {-# INLINE finish #-}
455 finish :: Reductions -> ArgsReductions
456 finish redns = ArgsReductions redns MRefl
457
458 {-# INLINE rewrite_args_slow #-}
459 -- | Slow path, compared to rewrite_args_fast, because this one must track
460 -- a lifting context.
461 rewrite_args_slow :: [TyCoBinder] -> Kind -> TcTyCoVarSet
462 -> [Role] -> [Type]
463 -> RewriteM ArgsReductions
464 rewrite_args_slow binders inner_ki fvs roles tys
465 -- Arguments used dependently must be rewritten with proper coercions, but
466 -- we're not guaranteed to get a proper coercion when rewriting with the
467 -- "Derived" flavour. So we must call noBogusCoercions when rewriting arguments
468 -- corresponding to binders that are dependent. However, we might legitimately
469 -- have *more* arguments than binders, in the case that the inner_ki is a variable
470 -- that gets instantiated with a Π-type. We conservatively choose not to produce
471 -- bogus coercions for these, too. Note that this might miss an opportunity for
472 -- a Derived rewriting a Derived. The solution would be to generate evidence for
473 -- Deriveds, thus avoiding this whole noBogusCoercions idea. See also
474 -- Note [No derived kind equalities]
475 = do { rewritten_args <- zipWith3M rw (map isNamedBinder binders ++ repeat True)
476 roles tys
477 ; return $ simplifyArgsWorker binders inner_ki fvs roles rewritten_args }
478 where
479 {-# INLINE rw #-}
480 rw :: Bool -- must we ensure to produce a real coercion here?
481 -- see comment at top of function
482 -> Role -> Type -> RewriteM Reduction
483 rw True r ty = noBogusCoercions $ rw1 r ty
484 rw False r ty = rw1 r ty
485
486 {-# INLINE rw1 #-}
487 rw1 :: Role -> Type -> RewriteM Reduction
488 rw1 Nominal ty
489 = setEqRel NomEq $
490 rewrite_one ty
491
492 rw1 Representational ty
493 = setEqRel ReprEq $
494 rewrite_one ty
495
496 rw1 Phantom ty
497 -- See Note [Phantoms in the rewriter]
498 = do { ty <- liftTcS $ zonkTcType ty
499 ; return $ mkReflRedn Phantom ty }
500
501 ------------------
502 rewrite_one :: TcType -> RewriteM Reduction
503 -- Rewrite a type to get rid of type function applications, returning
504 -- the new type-function-free type, and a collection of new equality
505 -- constraints. See Note [Rewriting] for more detail.
506 --
507 -- Postcondition:
508 -- the role on the result coercion matches the EqRel in the RewriteEnv
509
510 rewrite_one ty
511 | Just ty' <- rewriterView ty -- See Note [Rewriting synonyms]
512 = rewrite_one ty'
513
514 rewrite_one xi@(LitTy {})
515 = do { role <- getRole
516 ; return $ mkReflRedn role xi }
517
518 rewrite_one (TyVarTy tv)
519 = rewriteTyVar tv
520
521 rewrite_one (AppTy ty1 ty2)
522 = rewrite_app_tys ty1 [ty2]
523
524 rewrite_one (TyConApp tc tys)
525 -- If it's a type family application, try to reduce it
526 | isTypeFamilyTyCon tc
527 = rewrite_fam_app tc tys
528
529 -- For * a normal data type application
530 -- * data family application
531 -- we just recursively rewrite the arguments.
532 | otherwise
533 = rewrite_ty_con_app tc tys
534
535 rewrite_one (FunTy { ft_af = vis, ft_mult = mult, ft_arg = ty1, ft_res = ty2 })
536 = do { arg_redn <- rewrite_one ty1
537 ; res_redn <- rewrite_one ty2
538
539 -- Important: look at the *reduced* type, so that any unzonked variables
540 -- in kinds are gone and the getRuntimeRep succeeds.
541 -- cf. Note [Decomposing FunTy] in GHC.Tc.Solver.Canonical.
542 ; let arg_rep = getRuntimeRep (reductionReducedType arg_redn)
543 res_rep = getRuntimeRep (reductionReducedType res_redn)
544
545 ; (w_redn, arg_rep_redn, res_rep_redn) <- setEqRel NomEq $
546 liftA3 (,,) (rewrite_one mult)
547 (rewrite_one arg_rep)
548 (rewrite_one res_rep)
549 ; role <- getRole
550
551 ; let arg_rep_co = reductionCoercion arg_rep_redn
552 -- :: arg_rep ~ arg_rep_xi
553 arg_ki_co = mkTyConAppCo Nominal tYPETyCon [arg_rep_co]
554 -- :: TYPE arg_rep ~ TYPE arg_rep_xi
555 casted_arg_redn = mkCoherenceRightRedn role arg_redn arg_ki_co
556 -- :: ty1 ~> arg_xi |> arg_ki_co
557
558 res_rep_co = reductionCoercion res_rep_redn
559 res_ki_co = mkTyConAppCo Nominal tYPETyCon [res_rep_co]
560 casted_res_redn = mkCoherenceRightRedn role res_redn res_ki_co
561
562 -- We must rewrite the representations, because that's what would
563 -- be done if we used TyConApp instead of FunTy. These rewritten
564 -- representations are seen only in casts of the arg and res, below.
565 -- Forgetting this caused #19677.
566 ; return $ mkFunRedn role vis w_redn casted_arg_redn casted_res_redn }
567
568 rewrite_one ty@(ForAllTy {})
569 -- TODO (RAE): This is inadequate, as it doesn't rewrite the kind of
570 -- the bound tyvar. Doing so will require carrying around a substitution
571 -- and the usual substTyVarBndr-like silliness. Argh.
572
573 -- We allow for-alls when, but only when, no type function
574 -- applications inside the forall involve the bound type variables.
575 = do { let (bndrs, rho) = tcSplitForAllTyVarBinders ty
576 ; redn <- rewrite_one rho
577 ; return $ mkHomoForAllRedn bndrs redn }
578
579 rewrite_one (CastTy ty g)
580 = do { redn <- rewrite_one ty
581 ; g' <- rewrite_co g
582 ; role <- getRole
583 ; return $ mkCastRedn1 role ty g' redn }
584 -- This calls castCoercionKind1.
585 -- It makes a /big/ difference to call castCoercionKind1 not
586 -- the more general castCoercionKind2.
587 -- See Note [castCoercionKind1] in GHC.Core.Coercion
588
589 rewrite_one (CoercionTy co)
590 = do { co' <- rewrite_co co
591 ; role <- getRole
592 ; return $ mkReflCoRedn role co' }
593
594 -- | "Rewrite" a coercion. Really, just zonk it so we can uphold
595 -- (F1) of Note [Rewriting]
596 rewrite_co :: Coercion -> RewriteM Coercion
597 rewrite_co co = liftTcS $ zonkCo co
598
599 -- | Rewrite a reduction, composing the resulting coercions.
600 rewrite_reduction :: Reduction -> RewriteM Reduction
601 rewrite_reduction (Reduction co xi)
602 = do { redn <- bumpDepth $ rewrite_one xi
603 ; return $ co `mkTransRedn` redn }
604
605 -- rewrite (nested) AppTys
606 rewrite_app_tys :: Type -> [Type] -> RewriteM Reduction
607 -- commoning up nested applications allows us to look up the function's kind
608 -- only once. Without commoning up like this, we would spend a quadratic amount
609 -- of time looking up functions' types
610 rewrite_app_tys (AppTy ty1 ty2) tys = rewrite_app_tys ty1 (ty2:tys)
611 rewrite_app_tys fun_ty arg_tys
612 = do { redn <- rewrite_one fun_ty
613 ; rewrite_app_ty_args redn arg_tys }
614
615 -- Given a rewritten function (with the coercion produced by rewriting) and
616 -- a bunch of unrewritten arguments, rewrite the arguments and apply.
617 -- The coercion argument's role matches the role stored in the RewriteM monad.
618 --
619 -- The bang patterns used here were observed to improve performance. If you
620 -- wish to remove them, be sure to check for regressions in allocations.
621 rewrite_app_ty_args :: Reduction -> [Type] -> RewriteM Reduction
622 rewrite_app_ty_args redn []
623 -- this will be a common case when called from rewrite_fam_app, so shortcut
624 = return redn
625 rewrite_app_ty_args fun_redn@(Reduction fun_co fun_xi) arg_tys
626 = do { het_redn <- case tcSplitTyConApp_maybe fun_xi of
627 Just (tc, xis) ->
628 do { let tc_roles = tyConRolesRepresentational tc
629 arg_roles = dropList xis tc_roles
630 ; ArgsReductions (Reductions arg_cos arg_xis) kind_co
631 <- rewrite_vector (tcTypeKind fun_xi) arg_roles arg_tys
632
633 -- We start with a reduction of the form
634 -- fun_co :: ty ~ T xi_1 ... xi_n
635 -- and further arguments a_1, ..., a_m.
636 -- We rewrite these arguments, and obtain coercions:
637 -- arg_co_i :: a_i ~ zeta_i
638 -- Now, we need to apply fun_co to the arg_cos. The problem is
639 -- that using mkAppCo is wrong because that function expects
640 -- its second coercion to be Nominal, and the arg_cos might
641 -- not be. The solution is to use transitivity:
642 -- fun_co <a_1> ... <a_m> ;; T <xi_1> .. <xi_n> arg_co_1 ... arg_co_m
643 ; eq_rel <- getEqRel
644 ; let app_xi = mkTyConApp tc (xis ++ arg_xis)
645 app_co = case eq_rel of
646 NomEq -> mkAppCos fun_co arg_cos
647 ReprEq -> mkAppCos fun_co (map mkNomReflCo arg_tys)
648 `mkTcTransCo`
649 mkTcTyConAppCo Representational tc
650 (zipWith mkReflCo tc_roles xis ++ arg_cos)
651
652 ; return $
653 mkHetReduction
654 (mkReduction app_co app_xi )
655 kind_co }
656 Nothing ->
657 do { ArgsReductions redns kind_co
658 <- rewrite_vector (tcTypeKind fun_xi) (repeat Nominal) arg_tys
659 ; return $ mkHetReduction (mkAppRedns fun_redn redns) kind_co }
660
661 ; role <- getRole
662 ; return (homogeniseHetRedn role het_redn) }
663
664 rewrite_ty_con_app :: TyCon -> [TcType] -> RewriteM Reduction
665 rewrite_ty_con_app tc tys
666 = do { role <- getRole
667 ; let m_roles | Nominal <- role = Nothing
668 | otherwise = Just $ tyConRolesX role tc
669 ; ArgsReductions redns kind_co <- rewrite_args_tc tc m_roles tys
670 ; let tyconapp_redn
671 = mkHetReduction
672 (mkTyConAppRedn role tc redns)
673 kind_co
674 ; return $ homogeniseHetRedn role tyconapp_redn }
675
676 -- Rewrite a vector (list of arguments).
677 rewrite_vector :: Kind -- of the function being applied to these arguments
678 -> [Role] -- If we're rewriting w.r.t. ReprEq, what roles do the
679 -- args have?
680 -> [Type] -- the args to rewrite
681 -> RewriteM ArgsReductions
682 rewrite_vector ki roles tys
683 = do { eq_rel <- getEqRel
684 ; let mb_roles = case eq_rel of { NomEq -> Nothing; ReprEq -> Just roles }
685 ; rewrite_args bndrs any_named_bndrs inner_ki fvs mb_roles tys
686 }
687 where
688 (bndrs, inner_ki, any_named_bndrs) = split_pi_tys' ki
689 fvs = tyCoVarsOfType ki
690 {-# INLINE rewrite_vector #-}
691
692 {-
693 Note [Rewriting synonyms]
694 ~~~~~~~~~~~~~~~~~~~~~~~~~~
695 Not expanding synonyms aggressively improves error messages, and
696 keeps types smaller. But we need to take care.
697
698 Suppose
699 type Syn a = Int
700 type instance F Bool = Syn (F Bool)
701 [G] F Bool ~ Syn (F Bool)
702
703 If we don't expand the synonym, we'll get a spurious occurs-check
704 failure. This is normally what occCheckExpand takes care of, but
705 the LHS is a type family application, and occCheckExpand (already
706 complex enough as it is) does not know how to expand to avoid
707 a type family application.
708
709 In addition, expanding the forgetful synonym like this
710 will generally yield a *smaller* type. To wit, if we spot
711 S ( ... F tys ... ), where S is forgetful, we don't want to bother
712 doing hard work simplifying (F tys). We thus expand forgetful
713 synonyms, but not others.
714
715 isForgetfulSynTyCon returns True more often than it needs to, so
716 we err on the side of more expansion.
717
718 We also, of course, must expand type synonyms that mention type families,
719 so those families can get reduced.
720
721 ************************************************************************
722 * *
723 Rewriting a type-family application
724 * *
725 ************************************************************************
726
727 Note [How to normalise a family application]
728 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
729 Given an exactly saturated family application, how should we normalise it?
730 This Note spells out the algorithm and its reasoning.
731
732 First, we attempt to directly rewrite the type family application,
733 without simplifying any of the arguments first, in an attempt to avoid
734 doing unnecessary work.
735
736 STEP 1a. Call the rewriting plugins. If any plugin rewrites the type family
737 application, jump to FINISH.
738
739 STEP 1b. Try the famapp-cache. If we get a cache hit, jump to FINISH.
740
741 STEP 1c. Try top-level instances. Remember: we haven't simplified the arguments
742 yet. Example:
743 type instance F (Maybe a) = Int
744 target: F (Maybe (G Bool))
745 Instead of first trying to simplify (G Bool), we use the instance first. This
746 avoids the work of simplifying G Bool.
747
748 If an instance is found, jump to FINISH.
749
750 STEP 2: At this point we rewrite all arguments. This might expose more
751 information, which might allow plugins to make progress, or allow us to
752 pick up a top-level instance.
753
754 STEP 3. Try the inerts. Note that we try the inerts *after* rewriting the
755 arguments, because the inerts will have rewritten LHSs.
756
757 If an inert is found, jump to FINISH.
758
759 Next, we try STEP 1 again, as we might be able to make further progress after
760 having rewritten the arguments:
761
762 STEP 4a. Query the rewriting plugins again.
763
764 If any plugin supplies a rewriting, jump to FINISH.
765
766 STEP 4b. Try the famapp-cache again.
767
768 If we get a cache hit, jump to FINISH.
769
770 STEP 4c. Try top-level instances again.
771
772 If an instance is found, jump to FINISH.
773
774 STEP 5: GIVEUP. No progress to be made. Return what we have. (Do not FINISH.)
775
776 FINISH 1. We've made a reduction, but the new type may still have more
777 work to do. So rewrite the new type.
778
779 FINISH 2. Add the result to the famapp-cache, connecting the type we started
780 with to the one we ended with.
781
782 Because STEP 1{a,b,c} and STEP 4{a,b,c} happen the same way, they are abstracted into
783 try_to_reduce.
784
785 FINISH is naturally implemented in `finish`. But, Note [rewrite_exact_fam_app performance]
786 tells us that we should not add to the famapp-cache after STEP 1. So `finish`
787 is inlined in that case, and only FINISH 1 is performed.
788
789 -}
790
791 rewrite_fam_app :: TyCon -> [TcType] -> RewriteM Reduction
792 -- rewrite_fam_app can be over-saturated
793 -- rewrite_exact_fam_app lifts out the application to top level
794 -- Postcondition: Coercion :: Xi ~ F tys
795 rewrite_fam_app tc tys -- Can be over-saturated
796 = assertPpr (tys `lengthAtLeast` tyConArity tc)
797 (ppr tc $$ ppr (tyConArity tc) $$ ppr tys) $
798
799 -- Type functions are saturated
800 -- The type function might be *over* saturated
801 -- in which case the remaining arguments should
802 -- be dealt with by AppTys
803 do { let (tys1, tys_rest) = splitAt (tyConArity tc) tys
804 ; redn <- rewrite_exact_fam_app tc tys1
805 ; rewrite_app_ty_args redn tys_rest }
806
807 -- the [TcType] exactly saturate the TyCon
808 -- See Note [How to normalise a family application]
809 rewrite_exact_fam_app :: TyCon -> [TcType] -> RewriteM Reduction
810 rewrite_exact_fam_app tc tys
811 = do { checkStackDepth (mkTyConApp tc tys)
812
813 -- Query the typechecking plugins for all their rewriting functions
814 -- which apply to a type family application headed by the TyCon 'tc'.
815 ; tc_rewriters <- getTcPluginRewritersForTyCon tc
816
817 -- STEP 1. Try to reduce without reducing arguments first.
818 ; result1 <- try_to_reduce tc tys tc_rewriters
819 ; case result1 of
820 -- Don't use the cache;
821 -- See Note [rewrite_exact_fam_app performance]
822 { Just redn -> finish False redn
823 ; Nothing ->
824
825 -- That didn't work. So reduce the arguments, in STEP 2.
826 do { eq_rel <- getEqRel
827 -- checking eq_rel == NomEq saves ~0.5% in T9872a
828 ; ArgsReductions (Reductions cos xis) kind_co <-
829 if eq_rel == NomEq
830 then rewrite_args_tc tc Nothing tys
831 else setEqRel NomEq $
832 rewrite_args_tc tc Nothing tys
833
834 -- If we manage to rewrite the type family application after
835 -- rewriting the arguments, we will need to compose these
836 -- reductions.
837 --
838 -- We have:
839 --
840 -- arg_co_i :: ty_i ~ xi_i
841 -- fam_co :: F xi_1 ... xi_n ~ zeta
842 --
843 -- The full reduction is obtained as a composite:
844 --
845 -- full_co :: F ty_1 ... ty_n ~ zeta
846 -- full_co = F co_1 ... co_n ;; fam_co
847 ; let
848 role = eqRelRole eq_rel
849 args_co = mkTyConAppCo role tc cos
850 ; let homogenise :: Reduction -> Reduction
851 homogenise redn
852 = homogeniseHetRedn role
853 $ mkHetReduction
854 (args_co `mkTransRedn` redn)
855 kind_co
856
857 give_up :: Reduction
858 give_up = homogenise $ mkReflRedn role reduced
859 where reduced = mkTyConApp tc xis
860
861 -- STEP 3: try the inerts
862 ; result2 <- liftTcS $ lookupFamAppInert tc xis
863 ; flavour <- getFlavour
864 ; case result2 of
865 { Just (redn, fr@(_, inert_eq_rel))
866
867 | fr `eqCanRewriteFR` (flavour, eq_rel) ->
868 do { traceRewriteM "rewrite family application with inert"
869 (ppr tc <+> ppr xis $$ ppr redn)
870 ; finish True (homogenise downgraded_redn) }
871 -- this will sometimes duplicate an inert in the cache,
872 -- but avoiding doing so had no impact on performance, and
873 -- it seems easier not to weed out that special case
874 where
875 inert_role = eqRelRole inert_eq_rel
876 role = eqRelRole eq_rel
877 downgraded_redn = downgradeRedn role inert_role redn
878
879 ; _ ->
880
881 -- inerts didn't work. Try to reduce again, in STEP 4.
882 do { result3 <- try_to_reduce tc xis tc_rewriters
883 ; case result3 of
884 Just redn -> finish True (homogenise redn)
885 -- we have made no progress at all: STEP 5 (GIVEUP).
886 _ -> return give_up }}}}}
887 where
888 -- call this if the above attempts made progress.
889 -- This recursively rewrites the result and then adds to the cache
890 finish :: Bool -- add to the cache?
891 -> Reduction -> RewriteM Reduction
892 finish use_cache redn
893 = do { -- rewrite the result: FINISH 1
894 final_redn <- rewrite_reduction redn
895 ; eq_rel <- getEqRel
896 ; flavour <- getFlavour
897
898 -- extend the cache: FINISH 2
899 ; when (use_cache && eq_rel == NomEq && flavour /= Derived) $
900 -- the cache only wants Nominal eqs
901 -- and Wanteds can rewrite Deriveds; the cache
902 -- has only Givens
903 liftTcS $ extendFamAppCache tc tys final_redn
904 ; return final_redn }
905 {-# INLINE finish #-}
906
907 -- Returned coercion is input ~r output, where r is the role in the RewriteM monad
908 -- See Note [How to normalise a family application]
909 try_to_reduce :: TyCon -> [TcType] -> [TcPluginRewriter]
910 -> RewriteM (Maybe Reduction)
911 try_to_reduce tc tys tc_rewriters
912 = do { rewrite_env <- getRewriteEnv
913 ; result <-
914 liftTcS $ firstJustsM
915 [ runTcPluginRewriters rewrite_env tc_rewriters tys -- STEP 1a & STEP 4a
916 , lookupFamAppCache tc tys -- STEP 1b & STEP 4b
917 , matchFam tc tys ] -- STEP 1c & STEP 4c
918 ; traverse downgrade result }
919 where
920 -- The result above is always Nominal. We might want a Representational
921 -- coercion; this downgrades (and prints, out of convenience).
922 downgrade :: Reduction -> RewriteM Reduction
923 downgrade redn
924 = do { traceRewriteM "Eager T.F. reduction success" $
925 vcat [ ppr tc
926 , ppr tys
927 , ppr redn
928 ]
929 ; eq_rel <- getEqRel
930 -- manually doing it this way avoids allocation in the vastly
931 -- common NomEq case
932 ; case eq_rel of
933 NomEq -> return redn
934 ReprEq -> return $ mkSubRedn redn }
935
936 -- Retrieve all type-checking plugins that can rewrite a (saturated) type-family application
937 -- headed by the given 'TyCon`.
938 getTcPluginRewritersForTyCon :: TyCon -> RewriteM [TcPluginRewriter]
939 getTcPluginRewritersForTyCon tc
940 = liftTcS $ do { rewriters <- tcg_tc_plugin_rewriters <$> getGblEnv
941 ; return (lookupWithDefaultUFM rewriters [] tc) }
942
943 -- Run a collection of rewriting functions obtained from type-checking plugins,
944 -- querying in sequence if any plugin wants to rewrite the type family
945 -- applied to the given arguments.
946 --
947 -- Note that the 'TcPluginRewriter's provided all pertain to the same type family
948 -- (the 'TyCon' of which has been obtained ahead of calling this function).
949 runTcPluginRewriters :: RewriteEnv
950 -> [TcPluginRewriter]
951 -> [TcType]
952 -> TcS (Maybe Reduction)
953 runTcPluginRewriters rewriteEnv rewriterFunctions tys
954 | null rewriterFunctions
955 = return Nothing -- short-circuit for common case
956 | otherwise
957 = do { givens <- getInertGivens
958 ; runRewriters givens rewriterFunctions }
959 where
960 runRewriters :: [Ct] -> [TcPluginRewriter] -> TcS (Maybe Reduction)
961 runRewriters _ []
962 = return Nothing
963 runRewriters givens (rewriter:rewriters)
964 = do
965 rewriteResult <- wrapTcS . runTcPluginM $ rewriter rewriteEnv givens tys
966 case rewriteResult of
967 TcPluginRewriteTo
968 { tcPluginReduction = redn
969 , tcRewriterNewWanteds = wanteds
970 } -> do { emitWork wanteds; return $ Just redn }
971 TcPluginNoRewrite {} -> runRewriters givens rewriters
972
973 {-
974 ************************************************************************
975 * *
976 Rewriting a type variable
977 * *
978 ********************************************************************* -}
979
980 -- | The result of rewriting a tyvar "one step".
981 data RewriteTvResult
982 = RTRNotFollowed
983 -- ^ The inert set doesn't make the tyvar equal to anything else
984
985 | RTRFollowed !Reduction
986 -- ^ The tyvar rewrites to a not-necessarily rewritten other type.
987 -- The role is determined by the RewriteEnv.
988 --
989 -- With Quick Look, the returned TcType can be a polytype;
990 -- that is, in the constraint solver, a unification variable
991 -- can contain a polytype. See GHC.Tc.Gen.App
992 -- Note [Instantiation variables are short lived]
993
994 rewriteTyVar :: TyVar -> RewriteM Reduction
995 rewriteTyVar tv
996 = do { mb_yes <- rewrite_tyvar1 tv
997 ; case mb_yes of
998 RTRFollowed redn -> rewrite_reduction redn
999
1000 RTRNotFollowed -- Done, but make sure the kind is zonked
1001 -- Note [Rewriting] invariant (F0) and (F1)
1002 -> do { tv' <- liftTcS $ updateTyVarKindM zonkTcType tv
1003 ; role <- getRole
1004 ; let ty' = mkTyVarTy tv'
1005 ; return $ mkReflRedn role ty' } }
1006
1007 rewrite_tyvar1 :: TcTyVar -> RewriteM RewriteTvResult
1008 -- "Rewriting" a type variable means to apply the substitution to it
1009 -- Specifically, look up the tyvar in
1010 -- * the internal MetaTyVar box
1011 -- * the inerts
1012 -- See also the documentation for RewriteTvResult
1013
1014 rewrite_tyvar1 tv
1015 = do { mb_ty <- liftTcS $ isFilledMetaTyVar_maybe tv
1016 ; case mb_ty of
1017 Just ty -> do { traceRewriteM "Following filled tyvar"
1018 (ppr tv <+> equals <+> ppr ty)
1019 ; role <- getRole
1020 ; return $ RTRFollowed $
1021 mkReflRedn role ty }
1022 Nothing -> do { traceRewriteM "Unfilled tyvar" (pprTyVar tv)
1023 ; fr <- getFlavourRole
1024 ; rewrite_tyvar2 tv fr } }
1025
1026 rewrite_tyvar2 :: TcTyVar -> CtFlavourRole -> RewriteM RewriteTvResult
1027 -- The tyvar is not a filled-in meta-tyvar
1028 -- Try in the inert equalities
1029 -- See Definition [Applying a generalised substitution] in GHC.Tc.Solver.Monad
1030 -- See Note [Stability of rewriting] in GHC.Tc.Solver.Monad
1031
1032 rewrite_tyvar2 tv fr@(_, eq_rel)
1033 = do { ieqs <- liftTcS $ getInertEqs
1034 ; case lookupDVarEnv ieqs tv of
1035 Just (EqualCtList (ct :| _)) -- If the first doesn't work,
1036 -- the subsequent ones won't either
1037 | CEqCan { cc_ev = ctev, cc_lhs = TyVarLHS tv
1038 , cc_rhs = rhs_ty, cc_eq_rel = ct_eq_rel } <- ct
1039 , let ct_fr = (ctEvFlavour ctev, ct_eq_rel)
1040 , ct_fr `eqCanRewriteFR` fr -- This is THE key call of eqCanRewriteFR
1041 -> do { traceRewriteM "Following inert tyvar"
1042 (ppr tv <+>
1043 equals <+>
1044 ppr rhs_ty $$ ppr ctev)
1045 ; let rewriting_co1 = ctEvCoercion ctev
1046 rewriting_co = case (ct_eq_rel, eq_rel) of
1047 (ReprEq, _rel) -> assert (_rel == ReprEq )
1048 -- if this ASSERT fails, then
1049 -- eqCanRewriteFR answered incorrectly
1050 rewriting_co1
1051 (NomEq, NomEq) -> rewriting_co1
1052 (NomEq, ReprEq) -> mkSubCo rewriting_co1
1053
1054 ; return $ RTRFollowed $ mkReduction rewriting_co rhs_ty }
1055 -- NB: ct is Derived then fmode must be also, hence
1056 -- we are not going to touch the returned coercion
1057 -- so ctEvCoercion is fine.
1058
1059 _other -> return RTRNotFollowed }
1060
1061 {-
1062 Note [An alternative story for the inert substitution]
1063 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1064 (This entire note is just background, left here in case we ever want
1065 to return the previous state of affairs)
1066
1067 We used (GHC 7.8) to have this story for the inert substitution inert_eqs
1068
1069 * 'a' is not in fvs(ty)
1070 * They are *inert* in the weaker sense that there is no infinite chain of
1071 (i1 `eqCanRewrite` i2), (i2 `eqCanRewrite` i3), etc
1072
1073 This means that rewriting must be recursive, but it does allow
1074 [G] a ~ [b]
1075 [G] b ~ Maybe c
1076
1077 This avoids "saturating" the Givens, which can save a modest amount of work.
1078 It is easy to implement, in GHC.Tc.Solver.Interact.kick_out, by only kicking out an inert
1079 only if (a) the work item can rewrite the inert AND
1080 (b) the inert cannot rewrite the work item
1081
1082 This is significantly harder to think about. It can save a LOT of work
1083 in occurs-check cases, but we don't care about them much. #5837
1084 is an example, but it causes trouble only with the old (pre-Fall 2020)
1085 rewriting story. It is unclear if there is any gain w.r.t. to
1086 the new story.
1087
1088 -}
1089
1090 --------------------------------------
1091 -- Utilities
1092
1093 -- | Like 'splitPiTys'' but comes with a 'Bool' which is 'True' iff there is at
1094 -- least one named binder.
1095 split_pi_tys' :: Type -> ([TyCoBinder], Type, Bool)
1096 split_pi_tys' ty = split ty ty
1097 where
1098 -- put common cases first
1099 split _ (ForAllTy b res) = let -- This bang is necessary lest we see rather
1100 -- terrible reboxing, as noted in #19102.
1101 !(bs, ty, _) = split res res
1102 in (Named b : bs, ty, True)
1103 split _ (FunTy { ft_af = af, ft_mult = w, ft_arg = arg, ft_res = res })
1104 = let -- See #19102
1105 !(bs, ty, named) = split res res
1106 in (Anon af (mkScaled w arg) : bs, ty, named)
1107
1108 split orig_ty ty | Just ty' <- coreView ty = split orig_ty ty'
1109 split orig_ty _ = ([], orig_ty, False)
1110 {-# INLINE split_pi_tys' #-}
1111
1112 -- | Like 'tyConBindersTyCoBinders' but you also get a 'Bool' which is true iff
1113 -- there is at least one named binder.
1114 ty_con_binders_ty_binders' :: [TyConBinder] -> ([TyCoBinder], Bool)
1115 ty_con_binders_ty_binders' = foldr go ([], False)
1116 where
1117 go (Bndr tv (NamedTCB vis)) (bndrs, _)
1118 = (Named (Bndr tv vis) : bndrs, True)
1119 go (Bndr tv (AnonTCB af)) (bndrs, n)
1120 = (Anon af (tymult (tyVarKind tv)) : bndrs, n)
1121 {-# INLINE go #-}
1122 {-# INLINE ty_con_binders_ty_binders' #-}