never executed always true always false
1 {-# LANGUAGE BangPatterns #-}
2 {-# LANGUAGE ScopedTypeVariables #-}
3 {-# LANGUAGE FlexibleContexts #-}
4
5 module GHC.Core.Reduction
6 (
7 -- * Reductions
8 Reduction(..), ReductionN, ReductionR, HetReduction(..),
9 Reductions(..),
10 mkReduction, mkReductions, mkHetReduction, coercionRedn,
11 reductionOriginalType,
12 downgradeRedn, mkSubRedn,
13 mkTransRedn, mkCoherenceRightRedn, mkCoherenceRightMRedn,
14 mkCastRedn1, mkCastRedn2,
15 mkReflRedn, mkGReflRightRedn, mkGReflRightMRedn,
16 mkGReflLeftRedn, mkGReflLeftMRedn,
17 mkAppRedn, mkAppRedns, mkFunRedn,
18 mkForAllRedn, mkHomoForAllRedn, mkTyConAppRedn, mkClassPredRedn,
19 mkProofIrrelRedn, mkReflCoRedn,
20 homogeniseHetRedn,
21 unzipRedns,
22
23 -- * Rewriting type arguments
24 ArgsReductions(..),
25 simplifyArgsWorker
26
27 ) where
28
29 import GHC.Prelude
30
31 import GHC.Core.Class ( Class(classTyCon) )
32 import GHC.Core.Coercion
33 import GHC.Core.Predicate ( mkClassPred )
34 import GHC.Core.TyCon ( TyCon )
35 import GHC.Core.Type
36
37 import GHC.Data.Pair ( Pair(Pair) )
38
39 import GHC.Types.Var ( setTyVarKind )
40 import GHC.Types.Var.Env ( mkInScopeSet )
41 import GHC.Types.Var.Set ( TyCoVarSet )
42
43 import GHC.Utils.Misc ( HasDebugCallStack, equalLength )
44 import GHC.Utils.Outputable
45 import GHC.Utils.Panic ( assertPpr, panic )
46
47 {-
48 %************************************************************************
49 %* *
50 Reductions
51 %* *
52 %************************************************************************
53
54 Note [The Reduction type]
55 ~~~~~~~~~~~~~~~~~~~~~~~~~
56 Many functions in the type-checker rewrite a type, using Given type equalitie
57 or type-family reductions, and return a Reduction, which is just a pair of the
58 coercion and the RHS type of the coercion:
59 data Reduction = Reduction Coercion !Type
60
61 The order of the arguments to the constructor serves as a reminder
62 of what the Type is. In
63 Reduction co ty
64 `ty` appears to the right of `co`, reminding us that we must have:
65 co :: unrewritten_ty ~ ty
66
67 Example functions that use this datatype:
68 GHC.Core.FamInstEnv.topNormaliseType_maybe
69 :: FamInstEnvs -> Type -> Maybe Reduction
70 GHC.Tc.Solver.Rewrite.rewrite
71 :: CtEvidence -> TcType -> TcS Reduction
72
73 Having Reduction as a data type, with a strict Type field, rather than using
74 a pair (Coercion,Type) gives several advantages (see #20161)
75 * The strictness in Type improved performance in rewriting of type families
76 (around 2.5% improvement in T9872),
77 * Compared to the situation before, it gives improved consistency around
78 orientation of rewritings, as a Reduction is always left-to-right
79 (the coercion's RHS type is always the type stored in the 'Reduction').
80 No more 'mkSymCo's needed to convert between left-to-right and right-to-left.
81
82 One could imagine storing the LHS type of the coercion in the Reduction as well,
83 but in fact `reductionOriginalType` is very seldom used, so it's not worth it.
84 -}
85
86 -- | A 'Reduction' is the result of an operation that rewrites a type @ty_in@.
87 -- The 'Reduction' includes the rewritten type @ty_out@ and a 'Coercion' @co@
88 -- such that @co :: ty_in ~ ty_out@, where the role of the coercion is determined
89 -- by the context. That is, the LHS type of the coercion is the original type
90 -- @ty_in@, while its RHS type is the rewritten type @ty_out@.
91 --
92 -- A Reduction is always homogeneous, unless it is wrapped inside a 'HetReduction',
93 -- which separately stores the kind coercion.
94 --
95 -- See Note [The Reduction type].
96 data Reduction =
97 Reduction
98 { reductionCoercion :: Coercion
99 , reductionReducedType :: !Type
100 }
101 -- N.B. the 'Coercion' field must be lazy: see for instance GHC.Tc.Solver.Rewrite.rewrite_tyvar2
102 -- which returns an error in the 'Coercion' field when dealing with a Derived constraint
103 -- (which is OK as this Coercion gets ignored later).
104 -- We might want to revisit the strictness once Deriveds are removed.
105
106 -- | Stores a heterogeneous reduction.
107 --
108 -- The stored kind coercion must relate the kinds of the
109 -- stored reduction. That is, in @HetReduction (Reduction co xi) kco@,
110 -- we must have:
111 --
112 -- > co :: ty ~ xi
113 -- > kco :: typeKind ty ~ typeKind xi
114 data HetReduction =
115 HetReduction
116 Reduction
117 MCoercionN
118 -- N.B. strictness annotations don't seem to make a difference here
119
120 -- | Create a heterogeneous reduction.
121 --
122 -- Pre-condition: the provided kind coercion (second argument)
123 -- relates the kinds of the stored reduction.
124 -- That is, if the coercion stored in the 'Reduction' is of the form
125 --
126 -- > co :: ty ~ xi
127 --
128 -- Then the kind coercion supplied must be of the form:
129 --
130 -- > kco :: typeKind ty ~ typeKind xi
131 mkHetReduction :: Reduction -- ^ heterogeneous reduction
132 -> MCoercionN -- ^ kind coercion
133 -> HetReduction
134 mkHetReduction redn mco = HetReduction redn mco
135 {-# INLINE mkHetReduction #-}
136
137 -- | Homogenise a heterogeneous reduction.
138 --
139 -- Given @HetReduction (Reduction co xi) kco@, with
140 --
141 -- > co :: ty ~ xi
142 -- > kco :: typeKind(ty) ~ typeKind(xi)
143 --
144 -- this returns the homogeneous reduction:
145 --
146 -- > hco :: ty ~ ( xi |> sym kco )
147 homogeniseHetRedn :: Role -> HetReduction -> Reduction
148 homogeniseHetRedn role (HetReduction redn kco)
149 = mkCoherenceRightMRedn role redn (mkSymMCo kco)
150 {-# INLINE homogeniseHetRedn #-}
151
152 -- | Create a 'Reduction' from a pair of a 'Coercion' and a 'Type.
153 --
154 -- Pre-condition: the RHS type of the coercion matches the provided type
155 -- (perhaps up to zonking).
156 --
157 -- Use 'coercionRedn' when you only have the coercion.
158 mkReduction :: Coercion -> Type -> Reduction
159 mkReduction co ty = Reduction co ty
160 {-# INLINE mkReduction #-}
161
162 instance Outputable Reduction where
163 ppr redn =
164 braces $ vcat
165 [ text "reductionOriginalType:" <+> ppr (reductionOriginalType redn)
166 , text " reductionReducedType:" <+> ppr (reductionReducedType redn)
167 , text " reductionCoercion:" <+> ppr (reductionCoercion redn)
168 ]
169
170 -- | A 'Reduction' in which the 'Coercion' has 'Nominal' role.
171 type ReductionN = Reduction
172
173 -- | A 'Reduction' in which the 'Coercion' has 'Representational' role.
174 type ReductionR = Reduction
175
176 -- | Get the original, unreduced type corresponding to a 'Reduction'.
177 --
178 -- This is obtained by computing the LHS kind of the stored coercion,
179 -- which may be slow.
180 reductionOriginalType :: Reduction -> Type
181 reductionOriginalType = coercionLKind . reductionCoercion
182 {-# INLINE reductionOriginalType #-}
183
184 -- | Turn a 'Coercion' into a 'Reduction'
185 -- by inspecting the RHS type of the coercion.
186 --
187 -- Prefer using 'mkReduction' when you already know
188 -- the RHS type of the coercion, to avoid computing it anew.
189 coercionRedn :: Coercion -> Reduction
190 coercionRedn co = Reduction co (coercionRKind co)
191 {-# INLINE coercionRedn #-}
192
193 -- | Downgrade the role of the coercion stored in the 'Reduction'.
194 downgradeRedn :: Role -- ^ desired role
195 -> Role -- ^ current role
196 -> Reduction
197 -> Reduction
198 downgradeRedn new_role old_role redn@(Reduction co _)
199 = redn { reductionCoercion = downgradeRole new_role old_role co }
200 {-# INLINE downgradeRedn #-}
201
202 -- | Downgrade the role of the coercion stored in the 'Reduction',
203 -- from 'Nominal' to 'Representational'.
204 mkSubRedn :: Reduction -> Reduction
205 mkSubRedn redn@(Reduction co _) = redn { reductionCoercion = mkSubCo co }
206 {-# INLINE mkSubRedn #-}
207
208 -- | Compose a reduction with a coercion on the left.
209 --
210 -- Pre-condition: the provided coercion's RHS type must match the LHS type
211 -- of the coercion that is stored in the reduction.
212 mkTransRedn :: Coercion -> Reduction -> Reduction
213 mkTransRedn co1 redn@(Reduction co2 _)
214 = redn { reductionCoercion = co1 `mkTransCo` co2 }
215 {-# INLINE mkTransRedn #-}
216
217 -- | The reflexive reduction.
218 mkReflRedn :: Role -> Type -> Reduction
219 mkReflRedn r ty = mkReduction (mkReflCo r ty) ty
220
221 -- | Create a 'Reduction' from a kind cast, in which
222 -- the casted type is the rewritten type.
223 --
224 -- Given @ty :: k1@, @mco :: k1 ~ k2@,
225 -- produces the 'Reduction' @ty ~res_co~> (ty |> mco)@
226 -- at the given 'Role'.
227 mkGReflRightRedn :: Role -> Type -> CoercionN -> Reduction
228 mkGReflRightRedn role ty co
229 = mkReduction
230 (mkGReflRightCo role ty co)
231 (mkCastTy ty co)
232 {-# INLINE mkGReflRightRedn #-}
233
234 -- | Create a 'Reduction' from a kind cast, in which
235 -- the casted type is the rewritten type.
236 --
237 -- Given @ty :: k1@, @mco :: k1 ~ k2@,
238 -- produces the 'Reduction' @ty ~res_co~> (ty |> mco)@
239 -- at the given 'Role'.
240 mkGReflRightMRedn :: Role -> Type -> MCoercionN -> Reduction
241 mkGReflRightMRedn role ty mco
242 = mkReduction
243 (mkGReflRightMCo role ty mco)
244 (mkCastTyMCo ty mco)
245 {-# INLINE mkGReflRightMRedn #-}
246
247 -- | Create a 'Reduction' from a kind cast, in which
248 -- the casted type is the original (non-rewritten) type.
249 --
250 -- Given @ty :: k1@, @mco :: k1 ~ k2@,
251 -- produces the 'Reduction' @(ty |> mco) ~res_co~> ty@
252 -- at the given 'Role'.
253 mkGReflLeftRedn :: Role -> Type -> CoercionN -> Reduction
254 mkGReflLeftRedn role ty co
255 = mkReduction
256 (mkGReflLeftCo role ty co)
257 ty
258 {-# INLINE mkGReflLeftRedn #-}
259
260 -- | Create a 'Reduction' from a kind cast, in which
261 -- the casted type is the original (non-rewritten) type.
262 --
263 -- Given @ty :: k1@, @mco :: k1 ~ k2@,
264 -- produces the 'Reduction' @(ty |> mco) ~res_co~> ty@
265 -- at the given 'Role'.
266 mkGReflLeftMRedn :: Role -> Type -> MCoercionN -> Reduction
267 mkGReflLeftMRedn role ty mco
268 = mkReduction
269 (mkGReflLeftMCo role ty mco)
270 ty
271 {-# INLINE mkGReflLeftMRedn #-}
272
273 -- | Apply a cast to the result of a 'Reduction'.
274 --
275 -- Given a 'Reduction' @ty1 ~co1~> (ty2 :: k2)@ and a kind coercion @kco@
276 -- with LHS kind @k2@, produce a new 'Reduction' @ty1 ~co2~> ( ty2 |> kco )@
277 -- of the given 'Role' (which must match the role of the coercion stored
278 -- in the 'Reduction' argument).
279 mkCoherenceRightRedn :: Role -> Reduction -> CoercionN -> Reduction
280 mkCoherenceRightRedn r (Reduction co1 ty2) kco
281 = mkReduction
282 (mkCoherenceRightCo r ty2 kco co1)
283 (mkCastTy ty2 kco)
284 {-# INLINE mkCoherenceRightRedn #-}
285
286 -- | Apply a cast to the result of a 'Reduction', using an 'MCoercionN'.
287 --
288 -- Given a 'Reduction' @ty1 ~co1~> (ty2 :: k2)@ and a kind coercion @mco@
289 -- with LHS kind @k2@, produce a new 'Reduction' @ty1 ~co2~> ( ty2 |> mco )@
290 -- of the given 'Role' (which must match the role of the coercion stored
291 -- in the 'Reduction' argument).
292 mkCoherenceRightMRedn :: Role -> Reduction -> MCoercionN -> Reduction
293 mkCoherenceRightMRedn r (Reduction co1 ty2) kco
294 = mkReduction
295 (mkCoherenceRightMCo r ty2 kco co1)
296 (mkCastTyMCo ty2 kco)
297 {-# INLINE mkCoherenceRightMRedn #-}
298
299 -- | Apply a cast to a 'Reduction', casting both the original and the reduced type.
300 --
301 -- Given @cast_co@ and 'Reduction' @ty ~co~> xi@, this function returns
302 -- the 'Reduction' @(ty |> cast_co) ~return_co~> (xi |> cast_co)@
303 -- of the given 'Role' (which must match the role of the coercion stored
304 -- in the 'Reduction' argument).
305 --
306 -- Pre-condition: the 'Type' passed in is the same as the LHS type
307 -- of the coercion stored in the 'Reduction'.
308 mkCastRedn1 :: Role
309 -> Type -- ^ original type
310 -> CoercionN -- ^ coercion to cast with
311 -> Reduction -- ^ rewritten type, with rewriting coercion
312 -> Reduction
313 mkCastRedn1 r ty cast_co (Reduction co xi)
314 -- co :: ty ~r ty'
315 -- return_co :: (ty |> cast_co) ~r (ty' |> cast_co)
316 = mkReduction
317 (castCoercionKind1 co r ty xi cast_co)
318 (mkCastTy xi cast_co)
319 {-# INLINE mkCastRedn1 #-}
320
321 -- | Apply casts on both sides of a 'Reduction' (of the given 'Role').
322 --
323 -- Use 'mkCastRedn1' when you want to cast both the original and reduced types
324 -- in a 'Reduction' using the same coercion.
325 --
326 -- Pre-condition: the 'Type' passed in is the same as the LHS type
327 -- of the coercion stored in the 'Reduction'.
328 mkCastRedn2 :: Role
329 -> Type -- ^ original type
330 -> CoercionN -- ^ coercion to cast with on the left
331 -> Reduction -- ^ rewritten type, with rewriting coercion
332 -> CoercionN -- ^ coercion to cast with on the right
333 -> Reduction
334 mkCastRedn2 r ty cast_co (Reduction nco nty) cast_co'
335 = mkReduction
336 (castCoercionKind2 nco r ty nty cast_co cast_co')
337 (mkCastTy nty cast_co')
338 {-# INLINE mkCastRedn2 #-}
339
340 -- | Apply one 'Reduction' to another.
341 --
342 -- Combines 'mkAppCo' and 'mkAppTy`.
343 mkAppRedn :: Reduction -> Reduction -> Reduction
344 mkAppRedn (Reduction co1 ty1) (Reduction co2 ty2)
345 = mkReduction (mkAppCo co1 co2) (mkAppTy ty1 ty2)
346 {-# INLINE mkAppRedn #-}
347
348 -- | Create a function 'Reduction'.
349 --
350 -- Combines 'mkFunCo' and 'mkFunTy'.
351 mkFunRedn :: Role
352 -> AnonArgFlag
353 -> ReductionN -- ^ multiplicity reduction
354 -> Reduction -- ^ argument reduction
355 -> Reduction -- ^ result reduction
356 -> Reduction
357 mkFunRedn r vis
358 (Reduction w_co w_ty)
359 (Reduction arg_co arg_ty)
360 (Reduction res_co res_ty)
361 = mkReduction
362 (mkFunCo r w_co arg_co res_co)
363 (mkFunTy vis w_ty arg_ty res_ty)
364 {-# INLINE mkFunRedn #-}
365
366 -- | Create a 'Reduction' associated to a Π type,
367 -- from a kind 'Reduction' and a body 'Reduction'.
368 --
369 -- Combines 'mkForAllCo' and 'mkForAllTy'.
370 mkForAllRedn :: ArgFlag
371 -> TyVar
372 -> ReductionN -- ^ kind reduction
373 -> Reduction -- ^ body reduction
374 -> Reduction
375 mkForAllRedn vis tv1 (Reduction h ki') (Reduction co ty)
376 = mkReduction
377 (mkForAllCo tv1 h co)
378 (mkForAllTy tv2 vis ty)
379 where
380 tv2 = setTyVarKind tv1 ki'
381 {-# INLINE mkForAllRedn #-}
382
383 -- | Create a 'Reduction' of a quantified type from a
384 -- 'Reduction' of the body.
385 --
386 -- Combines 'mkHomoForAllCos' and 'mkForAllTys'.
387 mkHomoForAllRedn :: [TyVarBinder] -> Reduction -> Reduction
388 mkHomoForAllRedn bndrs (Reduction co ty)
389 = mkReduction
390 (mkHomoForAllCos (binderVars bndrs) co)
391 (mkForAllTys bndrs ty)
392 {-# INLINE mkHomoForAllRedn #-}
393
394 -- | Create a 'Reduction' from a coercion between coercions.
395 --
396 -- Combines 'mkProofIrrelCo' and 'mkCoercionTy'.
397 mkProofIrrelRedn :: Role -- ^ role of the created coercion, "r"
398 -> CoercionN -- ^ co :: phi1 ~N phi2
399 -> Coercion -- ^ g1 :: phi1
400 -> Coercion -- ^ g2 :: phi2
401 -> Reduction -- ^ res_co :: g1 ~r g2
402 mkProofIrrelRedn role co g1 g2
403 = mkReduction
404 (mkProofIrrelCo role co g1 g2)
405 (mkCoercionTy g2)
406 {-# INLINE mkProofIrrelRedn #-}
407
408 -- | Create a reflexive 'Reduction' whose RHS is the given 'Coercion',
409 -- with the specified 'Role'.
410 mkReflCoRedn :: Role -> Coercion -> Reduction
411 mkReflCoRedn role co
412 = mkReduction
413 (mkReflCo role co_ty)
414 co_ty
415 where
416 co_ty = mkCoercionTy co
417 {-# INLINE mkReflCoRedn #-}
418
419 -- | A collection of 'Reduction's where the coercions and the types are stored separately.
420 --
421 -- Use 'unzipRedns' to obtain 'Reductions' from a list of 'Reduction's.
422 --
423 -- This datatype is used in 'mkAppRedns', 'mkClassPredRedns' and 'mkTyConAppRedn',
424 -- which expect separate types and coercions.
425 --
426 -- Invariant: the two stored lists are of the same length,
427 -- and the RHS type of each coercion is the corresponding type.
428 data Reductions = Reductions [Coercion] [Type]
429
430 -- | Create 'Reductions' from individual lists of coercions and types.
431 --
432 -- The lists should be of the same length, and the RHS type of each coercion
433 -- should match the specified type in the other list.
434 mkReductions :: [Coercion] -> [Type] -> Reductions
435 mkReductions cos tys = Reductions cos tys
436 {-# INLINE mkReductions #-}
437
438 -- | Combines 'mkAppCos' and 'mkAppTys'.
439 mkAppRedns :: Reduction -> Reductions -> Reduction
440 mkAppRedns (Reduction co ty) (Reductions cos tys)
441 = mkReduction (mkAppCos co cos) (mkAppTys ty tys)
442 {-# INLINE mkAppRedns #-}
443
444 -- | 'TyConAppCo' for 'Reduction's: combines 'mkTyConAppCo' and `mkTyConApp`.
445 mkTyConAppRedn :: Role -> TyCon -> Reductions -> Reduction
446 mkTyConAppRedn role tc (Reductions cos tys)
447 = mkReduction (mkTyConAppCo role tc cos) (mkTyConApp tc tys)
448 {-# INLINE mkTyConAppRedn #-}
449
450 -- | Reduce the arguments of a 'Class' 'TyCon'.
451 mkClassPredRedn :: Class -> Reductions -> Reduction
452 mkClassPredRedn cls (Reductions cos tys)
453 = mkReduction
454 (mkTyConAppCo Nominal (classTyCon cls) cos)
455 (mkClassPred cls tys)
456 {-# INLINE mkClassPredRedn #-}
457
458 -- | Obtain 'Reductions' from a list of 'Reduction's by unzipping.
459 unzipRedns :: [Reduction] -> Reductions
460 unzipRedns = foldr accRedn (Reductions [] [])
461 where
462 accRedn :: Reduction -> Reductions -> Reductions
463 accRedn (Reduction co xi) (Reductions cos xis)
464 = Reductions (co:cos) (xi:xis)
465 {-# INLINE unzipRedns #-}
466 -- NB: this function is currently used in two locations:
467 --
468 -- - GHC.Tc.Gen.Foreign.normaliseFfiType', with one call of the form:
469 --
470 -- unzipRedns <$> zipWithM f tys roles
471 --
472 -- - GHC.Tc.Solver.Monad.breakTyVarCycle_maybe, with two calls of the form:
473 --
474 -- unzipRedns <$> mapM f tys
475 --
476 -- It is possible to write 'mapAndUnzipM' functions to handle these cases,
477 -- but the above locations aren't performance critical, so it was deemed
478 -- to not be worth it.
479
480 {-
481 %************************************************************************
482 %* *
483 Simplifying types
484 %* *
485 %************************************************************************
486
487 The function below morally belongs in GHC.Tc.Solver.Rewrite, but it is used also in
488 FamInstEnv, and so lives here.
489
490 Note [simplifyArgsWorker]
491 ~~~~~~~~~~~~~~~~~~~~~~~~~
492 Invariant (F2) of Note [Rewriting] in GHC.Tc.Solver.Rewrite says that
493 rewriting is homogeneous.
494 This causes some trouble when rewriting a function applied to a telescope
495 of arguments, perhaps with dependency. For example, suppose
496
497 type family F :: forall (j :: Type) (k :: Type). Maybe j -> Either j k -> Bool -> [k]
498
499 and we wish to rewrite the args of (with kind applications explicit)
500
501 F @a @b (Just @a c) (Right @a @b d) False
502
503 where all variables are skolems and
504
505 a :: Type
506 b :: Type
507 c :: a
508 d :: b
509
510 [G] aco :: a ~ fa
511 [G] bco :: b ~ fb
512 [G] cco :: c ~ fc
513 [G] dco :: d ~ fd
514
515 The first step is to rewrite all the arguments. This is done before calling
516 simplifyArgsWorker. We start from
517
518 a
519 b
520 Just @a c
521 Right @a @b d
522 False
523
524 and get left-to-right reductions whose coercions are as follows:
525
526 co1 :: a ~ fa
527 co2 :: b ~ fb
528 co3 :: (Just @a c) ~ (Just @fa (fc |> aco) |> co6)
529 co4 :: (Right @a @b d) ~ (Right @fa @fb (fd |> bco) |> co7)
530 co5 :: False ~ False
531
532 where
533 co6 = Maybe (sym aco) :: Maybe fa ~ Maybe a
534 co7 = Either (sym aco) (sym bco) :: Either fa fb ~ Either a b
535
536 We now process the rewritten args in left-to-right order. The first two args
537 need no further processing. But now consider the third argument. Let f3 = the rewritten
538 result, Just fa (fc |> aco) |> co6.
539 This f3 rewritten argument has kind (Maybe a), due to homogeneity of rewriting (F2).
540 And yet, when we build the application (F @fa @fb ...), we need this
541 argument to have kind (Maybe fa), not (Maybe a). We must cast this argument.
542 The coercion to use is determined by the kind of F:
543 we see in F's kind that the third argument has kind Maybe j.
544 Critically, we also know that the argument corresponding to j
545 (in our example, a) rewrote with a coercion co1. We can thus know the
546 coercion needed for the 3rd argument is (Maybe co1), thus building
547 (f3 |> Maybe co1)
548
549 More generally, we must use the Lifting Lemma, as implemented in
550 Coercion.liftCoSubst. As we work left-to-right, any variable that is a
551 dependent parameter (j and k, in our example) gets mapped in a lifting context
552 to the coercion that is output from rewriting the corresponding argument (co1
553 and co2, in our example). Then, after rewriting later arguments, we lift the
554 kind of these arguments in the lifting context that we've be building up.
555 This coercion is then used to keep the result of rewriting well-kinded.
556
557 Working through our example, this is what happens:
558
559 1. Extend the (empty) LC with [j |-> co1]. No new casting must be done,
560 because the binder associated with the first argument has a closed type (no
561 variables).
562
563 2. Extend the LC with [k |-> co2]. No casting to do.
564
565 3. Lifting the kind (Maybe j) with our LC
566 yields co8 :: Maybe a ~ Maybe fa. Use (f3 |> co8) as the argument to F.
567
568 4. Lifting the kind (Either j k) with our LC
569 yields co9 :: Either a b ~ Either fa fb. Use (f4 |> co9) as the 4th
570 argument to F, where f4 is the rewritten form of argument 4, written above.
571
572 5. We lift Bool with our LC, getting <Bool>; casting has no effect.
573
574 We're now almost done, but the new application
575
576 F @fa @fb (f3 |> co8) (f4 |> co9) False
577
578 has the wrong kind. Its kind is [fb], instead of the original [b].
579 So we must use our LC one last time to lift the result kind [k],
580 getting res_co :: [fb] ~ [b], and we cast our result.
581
582 Accordingly, the final result is
583
584 F
585 @fa
586 @fb
587 (Just @fa (fc |> aco) |> Maybe (sym aco) |> sym (Maybe (sym aco)))
588 (Right @fa @fb (fd |> bco) |> Either (sym aco) (sym bco) |> sym (Either (sym aco) (sym bco)))
589 False
590 |> [sym bco]
591
592 The res_co (in this case, [sym bco]) is the third component of the
593 tuple returned by simplifyArgsWorker.
594
595 Note [Last case in simplifyArgsWorker]
596 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
597 In writing simplifyArgsWorker's `go`, we know here that args cannot be empty,
598 because that case is first. We've run out of
599 binders. But perhaps inner_ki is a tyvar that has been instantiated with a
600 Π-type.
601
602 Here is an example.
603
604 a :: forall (k :: Type). k -> k
605 Proxy :: forall j. j -> Type
606 type family Star
607 axStar :: Star ~ Type
608 type family NoWay :: Bool
609 axNoWay :: NoWay ~ False
610 bo :: Type
611 [G] bc :: bo ~ Bool (in inert set)
612
613 co :: (forall j. j -> Type) ~ (forall (j :: Star). (j |> axStar) -> Star)
614 co = forall (j :: sym axStar). (<j> -> sym axStar)
615
616 We are rewriting:
617 a (forall (j :: Star). (j |> axStar) -> Star) -- 1
618 (Proxy |> co) -- 2
619 (bo |> sym axStar) -- 3
620 (NoWay |> sym bc) -- 4
621 :: Star
622
623 First, we rewrite all the arguments (before simplifyArgsWorker), like so:
624
625 co1 :: (forall (j :: Star). (j |> axStar) -> Star) ~ (forall j. j -> Type) -- 1
626 co2 :: (Proxy |> co) ~ (Proxy |> co) -- 2
627 co3 :: (bo |> sym axStar) ~ (Bool |> sym axStar) -- 3
628 co4 :: (NoWay |> sym bc) ~ (False |> sym bc) -- 4
629
630 Then we do the process described in Note [simplifyArgsWorker].
631
632 1. Lifting Type (the kind of the first arg) gives us a reflexive coercion, so we
633 don't use it. But we do build a lifting context [k -> co1] (where co1 is a
634 result of rewriting an argument, written above).
635
636 2. Lifting k gives us co1, so the second argument becomes (Proxy |> co |> co1).
637 This is not a dependent argument, so we don't extend the lifting context.
638
639 Now we need to deal with argument (3).
640 The way we normally proceed is to lift the kind of the binder, to see whether
641 it's dependent.
642 But here, the remainder of the kind of `a` that we're left with
643 after processing two arguments is just `k`.
644
645 The way forward is look up k in the lifting context, getting co1. If we're at
646 all well-typed, co1 will be a coercion between Π-types, with at least one binder.
647 So, let's decompose co1 with decomposePiCos. This decomposition needs arguments to use
648 to instantiate any kind parameters. Look at the type of co1. If we just
649 decomposed it, we would end up with coercions whose types include j, which is
650 out of scope here. Accordingly, decomposePiCos takes a list of types whose
651 kinds are the *unrewritten* types in the decomposed coercion. (See comments on
652 decomposePiCos.) Because the rewritten types have unrewritten kinds (because
653 rewriting is homogeneous), passing the list of rewritten types to decomposePiCos
654 just won't do: later arguments' kinds won't be as expected. So we need to get
655 the *unrewritten* types to pass to decomposePiCos. We can do this easily enough
656 by taking the kind of the argument coercions, passed in originally.
657
658 (Alternative 1: We could re-engineer decomposePiCos to deal with this situation.
659 But that function is already gnarly, and other call sites of decomposePiCos
660 would suffer from the change, even though they are much more common than this one.)
661
662 (Alternative 2: We could avoid calling decomposePiCos entirely, integrating its
663 behavior into simplifyArgsWorker. This would work, I think, but then all of the
664 complication of decomposePiCos would end up layered on top of all the complication
665 here. Please, no.)
666
667 (Alternative 3: We could pass the unrewritten arguments into simplifyArgsWorker
668 so that we don't have to recreate them. But that would complicate the interface
669 of this function to handle a very dark, dark corner case. Better to keep our
670 demons to ourselves here instead of exposing them to callers. This decision is
671 easily reversed if there is ever any performance trouble due to the call of
672 coercionKind.)
673
674 So we now call
675
676 decomposePiCos co1
677 (Pair (forall (j :: Star). (j |> axStar) -> Star) (forall j. j -> Type))
678 [bo |> sym axStar, NoWay |> sym bc]
679
680 to get
681
682 co5 :: Star ~ Type
683 co6 :: (j |> axStar) ~ (j |> co5), substituted to
684 (bo |> sym axStar |> axStar) ~ (bo |> sym axStar |> co5)
685 == bo ~ bo
686 res_co :: Type ~ Star
687
688 We then use these casts on (the rewritten) (3) and (4) to get
689
690 (Bool |> sym axStar |> co5 :: Type) -- (C3)
691 (False |> sym bc |> co6 :: bo) -- (C4)
692
693 We can simplify to
694
695 Bool -- (C3)
696 (False |> sym bc :: bo) -- (C4)
697
698 Of course, we still must do the processing in Note [simplifyArgsWorker] to finish
699 the job. We thus want to recur. Our new function kind is the left-hand type of
700 co1 (gotten, recall, by lifting the variable k that was the return kind of the
701 original function). Why the left-hand type (as opposed to the right-hand type)?
702 Because we have casted all the arguments according to decomposePiCos, which gets
703 us from the right-hand type to the left-hand one. We thus recur with that new
704 function kind, zapping our lifting context, because we have essentially applied
705 it.
706
707 This recursive call returns ([Bool, False], [...], Refl). The Bool and False
708 are the correct arguments we wish to return. But we must be careful about the
709 result coercion: our new, rewritten application will have kind Type, but we
710 want to make sure that the result coercion casts this back to Star. (Why?
711 Because we started with an application of kind Star, and rewriting is homogeneous.)
712
713 So, we have to twiddle the result coercion appropriately.
714
715 Let's check whether this is well-typed. We know
716
717 a :: forall (k :: Type). k -> k
718
719 a (forall j. j -> Type) :: (forall j. j -> Type) -> forall j. j -> Type
720
721 a (forall j. j -> Type)
722 Proxy
723 :: forall j. j -> Type
724
725 a (forall j. j -> Type)
726 Proxy
727 Bool
728 :: Bool -> Type
729
730 a (forall j. j -> Type)
731 Proxy
732 Bool
733 False
734 :: Type
735
736 a (forall j. j -> Type)
737 Proxy
738 Bool
739 False
740 |> res_co
741 :: Star
742
743 as desired.
744
745 Whew.
746
747 Historical note: I (Richard E) once thought that the final part of the kind
748 had to be a variable k (as in the example above). But it might not be: it could
749 be an application of a variable. Here is the example:
750
751 let f :: forall (a :: Type) (b :: a -> Type). b (Any @a)
752 k :: Type
753 x :: k
754
755 rewrite (f @Type @((->) k) x)
756
757 After instantiating [a |-> Type, b |-> ((->) k)], we see that `b (Any @a)`
758 is `k -> Any @a`, and thus the third argument of `x :: k` is well-kinded.
759
760 -}
761
762 -- | Stores 'Reductions' as well as a kind coercion.
763 --
764 -- Used when rewriting arguments to a type function @f@.
765 --
766 -- Invariant:
767 -- when the stored reductions are of the form
768 -- co_i :: ty_i ~ xi_i,
769 -- the kind coercion is of the form
770 -- kco :: typeKind (f ty_1 ... ty_n) ~ typeKind (f xi_1 ... xi_n)
771 --
772 -- The type function @f@ depends on context.
773 data ArgsReductions =
774 ArgsReductions
775 {-# UNPACK #-} !Reductions
776 !MCoercionN
777 -- The strictness annotations and UNPACK pragma here are crucial
778 -- to getting good performance in simplifyArgsWorker's tight loop.
779
780 -- This is shared between the rewriter and the normaliser in GHC.Core.FamInstEnv.
781 -- See Note [simplifyArgsWorker]
782 {-# INLINE simplifyArgsWorker #-}
783 -- NB. INLINE yields a ~1% decrease in allocations in T9872d compared to INLINEABLE
784 -- This function is only called in two locations, so the amount of code duplication
785 -- should be rather reasonable despite the size of the function.
786 simplifyArgsWorker :: HasDebugCallStack
787 => [TyCoBinder] -> Kind
788 -- the binders & result kind (not a Π-type) of the function applied to the args
789 -- list of binders can be shorter or longer than the list of args
790 -> TyCoVarSet -- free vars of the args
791 -> [Role] -- list of roles, r
792 -> [Reduction] -- rewritten type arguments, arg_i
793 -- each comes with the coercion used to rewrite it,
794 -- arg_co_i :: ty_i ~ arg_i
795 -> ArgsReductions
796 -- Returns ArgsReductions (Reductions cos xis) res_co, where co_i :: ty_i ~ xi_i,
797 -- and res_co :: kind (f ty_1 ... ty_n) ~ kind (f xi_1 ... xi_n), where f is the function
798 -- that we are applying.
799 -- Precondition: if f :: forall bndrs. inner_ki (where bndrs and inner_ki are passed in),
800 -- then (f ty_1 ... ty_n) is well kinded. Note that (f arg_1 ... arg_n) might *not* be well-kinded.
801 -- Massaging the arg_i in order to make the function application well-kinded is what this
802 -- function is all about. That is, (f xi_1 ... xi_n), where xi_i are the returned arguments,
803 -- *is* well kinded.
804 simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
805 orig_roles orig_simplified_args
806 = go orig_lc
807 orig_ki_binders orig_inner_ki
808 orig_roles orig_simplified_args
809 where
810 orig_lc = emptyLiftingContext $ mkInScopeSet orig_fvs
811
812 go :: LiftingContext -- mapping from tyvars to rewriting coercions
813 -> [TyCoBinder] -- Unsubsted binders of function's kind
814 -> Kind -- Unsubsted result kind of function (not a Pi-type)
815 -> [Role] -- Roles at which to rewrite these ...
816 -> [Reduction] -- rewritten arguments, with their rewriting coercions
817 -> ArgsReductions
818 go !lc binders inner_ki _ []
819 -- The !lc makes the function strict in the lifting context
820 -- which means GHC can unbox that pair. A modest win.
821 = ArgsReductions
822 (mkReductions [] [])
823 kind_co
824 where
825 final_kind = mkPiTys binders inner_ki
826 kind_co | noFreeVarsOfType final_kind = MRefl
827 | otherwise = MCo $ liftCoSubst Nominal lc final_kind
828
829 go lc (binder:binders) inner_ki (role:roles) (arg_redn:arg_redns)
830 = -- We rewrite an argument ty with arg_redn = Reduction arg_co arg
831 -- By Note [Rewriting] in GHC.Tc.Solver.Rewrite invariant (F2),
832 -- tcTypeKind(ty) = tcTypeKind(arg).
833 -- However, it is possible that arg will be used as an argument to a function
834 -- whose kind is different, if earlier arguments have been rewritten.
835 -- We thus need to compose the reduction with a kind coercion to ensure
836 -- well-kindedness (see the call to mkCoherenceRightRedn below).
837 --
838 -- The bangs here have been observed to improve performance
839 -- significantly in optimized builds; see #18502
840 let !kind_co = liftCoSubst Nominal lc (tyCoBinderType binder)
841 !(Reduction casted_co casted_xi)
842 = mkCoherenceRightRedn role arg_redn kind_co
843 -- now, extend the lifting context with the new binding
844 !new_lc | Just tv <- tyCoBinderVar_maybe binder
845 = extendLiftingContextAndInScope lc tv casted_co
846 | otherwise
847 = lc
848 !(ArgsReductions (Reductions cos xis) final_kind_co)
849 = go new_lc binders inner_ki roles arg_redns
850 in ArgsReductions
851 (Reductions (casted_co:cos) (casted_xi:xis))
852 final_kind_co
853
854 -- See Note [Last case in simplifyArgsWorker]
855 go lc [] inner_ki roles arg_redns
856 = let co1 = liftCoSubst Nominal lc inner_ki
857 co1_kind = coercionKind co1
858 unrewritten_tys = map reductionOriginalType arg_redns
859 (arg_cos, res_co) = decomposePiCos co1 co1_kind unrewritten_tys
860 casted_args = assertPpr (equalLength arg_redns arg_cos)
861 (ppr arg_redns $$ ppr arg_cos)
862 $ zipWith3 mkCoherenceRightRedn roles arg_redns arg_cos
863 -- In general decomposePiCos can return fewer cos than tys,
864 -- but not here; because we're well typed, there will be enough
865 -- binders. Note that decomposePiCos does substitutions, so even
866 -- if the original substitution results in something ending with
867 -- ... -> k, that k will be substituted to perhaps reveal more
868 -- binders.
869 zapped_lc = zapLiftingContext lc
870 Pair rewritten_kind _ = co1_kind
871 (bndrs, new_inner) = splitPiTys rewritten_kind
872
873 ArgsReductions redns_out res_co_out
874 = go zapped_lc bndrs new_inner roles casted_args
875 in
876 ArgsReductions redns_out (res_co `mkTransMCoR` res_co_out)
877
878 go _ _ _ _ _ = panic
879 "simplifyArgsWorker wandered into deeper water than usual"
880 -- This debug information is commented out because leaving it in
881 -- causes a ~2% increase in allocations in T9872d.
882 -- That's independent of the analogous case in rewrite_args_fast
883 -- in GHC.Tc.Solver.Rewrite:
884 -- each of these causes a 2% increase on its own, so commenting them
885 -- both out gives a 4% decrease in T9872d.
886 {-
887
888 (vcat [ppr orig_binders,
889 ppr orig_inner_ki,
890 ppr (take 10 orig_roles), -- often infinite!
891 ppr orig_tys])
892 -}