never executed always true always false
1 -- (c) The University of Glasgow 2006
2
3 {-# LANGUAGE CPP #-}
4
5 module GHC.Core.Coercion.Opt
6 ( optCoercion
7 , checkAxInstCo
8 , OptCoercionOpts (..)
9 )
10 where
11
12 import GHC.Prelude
13
14 import GHC.Tc.Utils.TcType ( exactTyCoVarsOfType )
15
16 import GHC.Core.TyCo.Rep
17 import GHC.Core.TyCo.Subst
18 import GHC.Core.Coercion
19 import GHC.Core.Type as Type hiding( substTyVarBndr, substTy )
20 import GHC.Core.TyCon
21 import GHC.Core.Coercion.Axiom
22 import GHC.Core.Unify
23
24 import GHC.Types.Var.Set
25 import GHC.Types.Var.Env
26
27 import GHC.Data.Pair
28 import GHC.Data.List.SetOps ( getNth )
29
30 import GHC.Utils.Outputable
31 import GHC.Utils.Constants (debugIsOn)
32 import GHC.Utils.Misc
33 import GHC.Utils.Panic
34 import GHC.Utils.Panic.Plain
35 import GHC.Utils.Trace
36
37 import Control.Monad ( zipWithM )
38
39 {-
40 %************************************************************************
41 %* *
42 Optimising coercions
43 %* *
44 %************************************************************************
45
46 Note [Optimising coercion optimisation]
47 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
48 Looking up a coercion's role or kind is linear in the size of the
49 coercion. Thus, doing this repeatedly during the recursive descent
50 of coercion optimisation is disastrous. We must be careful to avoid
51 doing this if at all possible.
52
53 Because it is generally easy to know a coercion's components' roles
54 from the role of the outer coercion, we pass down the known role of
55 the input in the algorithm below. We also keep functions opt_co2
56 and opt_co3 separate from opt_co4, so that the former two do Phantom
57 checks that opt_co4 can avoid. This is a big win because Phantom coercions
58 rarely appear within non-phantom coercions -- only in some TyConAppCos
59 and some AxiomInstCos. We handle these cases specially by calling
60 opt_co2.
61
62 Note [Optimising InstCo]
63 ~~~~~~~~~~~~~~~~~~~~~~~~
64 (1) tv is a type variable
65 When we have (InstCo (ForAllCo tv h g) g2), we want to optimise.
66
67 Let's look at the typing rules.
68
69 h : k1 ~ k2
70 tv:k1 |- g : t1 ~ t2
71 -----------------------------
72 ForAllCo tv h g : (all tv:k1.t1) ~ (all tv:k2.t2[tv |-> tv |> sym h])
73
74 g1 : (all tv:k1.t1') ~ (all tv:k2.t2')
75 g2 : s1 ~ s2
76 --------------------
77 InstCo g1 g2 : t1'[tv |-> s1] ~ t2'[tv |-> s2]
78
79 We thus want some coercion proving this:
80
81 (t1[tv |-> s1]) ~ (t2[tv |-> s2 |> sym h])
82
83 If we substitute the *type* tv for the *coercion*
84 (g2 ; t2 ~ t2 |> sym h) in g, we'll get this result exactly.
85 This is bizarre,
86 though, because we're substituting a type variable with a coercion. However,
87 this operation already exists: it's called *lifting*, and defined in GHC.Core.Coercion.
88 We just need to enhance the lifting operation to be able to deal with
89 an ambient substitution, which is why a LiftingContext stores a TCvSubst.
90
91 (2) cv is a coercion variable
92 Now consider we have (InstCo (ForAllCo cv h g) g2), we want to optimise.
93
94 h : (t1 ~r t2) ~N (t3 ~r t4)
95 cv : t1 ~r t2 |- g : t1' ~r2 t2'
96 n1 = nth r 2 (downgradeRole r N h) :: t1 ~r t3
97 n2 = nth r 3 (downgradeRole r N h) :: t2 ~r t4
98 ------------------------------------------------
99 ForAllCo cv h g : (all cv:t1 ~r t2. t1') ~r2
100 (all cv:t3 ~r t4. t2'[cv |-> n1 ; cv ; sym n2])
101
102 g1 : (all cv:t1 ~r t2. t1') ~ (all cv: t3 ~r t4. t2')
103 g2 : h1 ~N h2
104 h1 : t1 ~r t2
105 h2 : t3 ~r t4
106 ------------------------------------------------
107 InstCo g1 g2 : t1'[cv |-> h1] ~ t2'[cv |-> h2]
108
109 We thus want some coercion proving this:
110
111 t1'[cv |-> h1] ~ t2'[cv |-> n1 ; h2; sym n2]
112
113 So we substitute the coercion variable c for the coercion
114 (h1 ~N (n1; h2; sym n2)) in g.
115 -}
116
117 -- | Coercion optimisation options
118 newtype OptCoercionOpts = OptCoercionOpts
119 { optCoercionEnabled :: Bool -- ^ Enable coercion optimisation (reduce its size)
120 }
121
122 optCoercion :: OptCoercionOpts -> TCvSubst -> Coercion -> NormalCo
123 -- ^ optCoercion applies a substitution to a coercion,
124 -- *and* optimises it to reduce its size
125 optCoercion opts env co
126 | optCoercionEnabled opts = optCoercion' env co
127 | otherwise = substCo env co
128
129 optCoercion' :: TCvSubst -> Coercion -> NormalCo
130 optCoercion' env co
131 | debugIsOn
132 = let out_co = opt_co1 lc False co
133 (Pair in_ty1 in_ty2, in_role) = coercionKindRole co
134 (Pair out_ty1 out_ty2, out_role) = coercionKindRole out_co
135 in
136 assertPpr (substTyUnchecked env in_ty1 `eqType` out_ty1 &&
137 substTyUnchecked env in_ty2 `eqType` out_ty2 &&
138 in_role == out_role)
139 ( text "optCoercion changed types!"
140 $$ hang (text "in_co:") 2 (ppr co)
141 $$ hang (text "in_ty1:") 2 (ppr in_ty1)
142 $$ hang (text "in_ty2:") 2 (ppr in_ty2)
143 $$ hang (text "out_co:") 2 (ppr out_co)
144 $$ hang (text "out_ty1:") 2 (ppr out_ty1)
145 $$ hang (text "out_ty2:") 2 (ppr out_ty2)
146 $$ hang (text "subst:") 2 (ppr env))
147 out_co
148
149 | otherwise = opt_co1 lc False co
150 where
151 lc = mkSubstLiftingContext env
152
153 type NormalCo = Coercion
154 -- Invariants:
155 -- * The substitution has been fully applied
156 -- * For trans coercions (co1 `trans` co2)
157 -- co1 is not a trans, and neither co1 nor co2 is identity
158
159 type NormalNonIdCo = NormalCo -- Extra invariant: not the identity
160
161 -- | Do we apply a @sym@ to the result?
162 type SymFlag = Bool
163
164 -- | Do we force the result to be representational?
165 type ReprFlag = Bool
166
167 -- | Optimize a coercion, making no assumptions. All coercions in
168 -- the lifting context are already optimized (and sym'd if nec'y)
169 opt_co1 :: LiftingContext
170 -> SymFlag
171 -> Coercion -> NormalCo
172 opt_co1 env sym co = opt_co2 env sym (coercionRole co) co
173
174 -- See Note [Optimising coercion optimisation]
175 -- | Optimize a coercion, knowing the coercion's role. No other assumptions.
176 opt_co2 :: LiftingContext
177 -> SymFlag
178 -> Role -- ^ The role of the input coercion
179 -> Coercion -> NormalCo
180 opt_co2 env sym Phantom co = opt_phantom env sym co
181 opt_co2 env sym r co = opt_co3 env sym Nothing r co
182
183 -- See Note [Optimising coercion optimisation]
184 -- | Optimize a coercion, knowing the coercion's non-Phantom role.
185 opt_co3 :: LiftingContext -> SymFlag -> Maybe Role -> Role -> Coercion -> NormalCo
186 opt_co3 env sym (Just Phantom) _ co = opt_phantom env sym co
187 opt_co3 env sym (Just Representational) r co = opt_co4_wrap env sym True r co
188 -- if mrole is Just Nominal, that can't be a downgrade, so we can ignore
189 opt_co3 env sym _ r co = opt_co4_wrap env sym False r co
190
191 -- See Note [Optimising coercion optimisation]
192 -- | Optimize a non-phantom coercion.
193 opt_co4, opt_co4_wrap :: LiftingContext -> SymFlag -> ReprFlag -> Role -> Coercion -> NormalCo
194
195 opt_co4_wrap = opt_co4
196 {-
197 opt_co4_wrap env sym rep r co
198 = pprTrace "opt_co4_wrap {"
199 ( vcat [ text "Sym:" <+> ppr sym
200 , text "Rep:" <+> ppr rep
201 , text "Role:" <+> ppr r
202 , text "Co:" <+> ppr co ]) $
203 assert (r == coercionRole co )
204 let result = opt_co4 env sym rep r co in
205 pprTrace "opt_co4_wrap }" (ppr co $$ text "---" $$ ppr result) $
206 result
207 -}
208
209 opt_co4 env _ rep r (Refl ty)
210 = assertPpr (r == Nominal)
211 (text "Expected role:" <+> ppr r $$
212 text "Found role:" <+> ppr Nominal $$
213 text "Type:" <+> ppr ty) $
214 liftCoSubst (chooseRole rep r) env ty
215
216 opt_co4 env _ rep r (GRefl _r ty MRefl)
217 = assertPpr (r == _r)
218 (text "Expected role:" <+> ppr r $$
219 text "Found role:" <+> ppr _r $$
220 text "Type:" <+> ppr ty) $
221 liftCoSubst (chooseRole rep r) env ty
222
223 opt_co4 env sym rep r (GRefl _r ty (MCo co))
224 = assertPpr (r == _r)
225 (text "Expected role:" <+> ppr r $$
226 text "Found role:" <+> ppr _r $$
227 text "Type:" <+> ppr ty) $
228 if isGReflCo co || isGReflCo co'
229 then liftCoSubst r' env ty
230 else wrapSym sym $ mkCoherenceRightCo r' ty' co' (liftCoSubst r' env ty)
231 where
232 r' = chooseRole rep r
233 ty' = substTy (lcSubstLeft env) ty
234 co' = opt_co4 env False False Nominal co
235
236 opt_co4 env sym rep r (SymCo co) = opt_co4_wrap env (not sym) rep r co
237 -- surprisingly, we don't have to do anything to the env here. This is
238 -- because any "lifting" substitutions in the env are tied to ForAllCos,
239 -- which treat their left and right sides differently. We don't want to
240 -- exchange them.
241
242 opt_co4 env sym rep r g@(TyConAppCo _r tc cos)
243 = assert (r == _r) $
244 case (rep, r) of
245 (True, Nominal) ->
246 mkTyConAppCo Representational tc
247 (zipWith3 (opt_co3 env sym)
248 (map Just (tyConRolesRepresentational tc))
249 (repeat Nominal)
250 cos)
251 (False, Nominal) ->
252 mkTyConAppCo Nominal tc (map (opt_co4_wrap env sym False Nominal) cos)
253 (_, Representational) ->
254 -- must use opt_co2 here, because some roles may be P
255 -- See Note [Optimising coercion optimisation]
256 mkTyConAppCo r tc (zipWith (opt_co2 env sym)
257 (tyConRolesRepresentational tc) -- the current roles
258 cos)
259 (_, Phantom) -> pprPanic "opt_co4 sees a phantom!" (ppr g)
260
261 opt_co4 env sym rep r (AppCo co1 co2)
262 = mkAppCo (opt_co4_wrap env sym rep r co1)
263 (opt_co4_wrap env sym False Nominal co2)
264
265 opt_co4 env sym rep r (ForAllCo tv k_co co)
266 = case optForAllCoBndr env sym tv k_co of
267 (env', tv', k_co') -> mkForAllCo tv' k_co' $
268 opt_co4_wrap env' sym rep r co
269 -- Use the "mk" functions to check for nested Refls
270
271 opt_co4 env sym rep r (FunCo _r cow co1 co2)
272 = assert (r == _r) $
273 if rep
274 then mkFunCo Representational cow' co1' co2'
275 else mkFunCo r cow' co1' co2'
276 where
277 co1' = opt_co4_wrap env sym rep r co1
278 co2' = opt_co4_wrap env sym rep r co2
279 cow' = opt_co1 env sym cow
280
281 opt_co4 env sym rep r (CoVarCo cv)
282 | Just co <- lookupCoVar (lcTCvSubst env) cv
283 = opt_co4_wrap (zapLiftingContext env) sym rep r co
284
285 | ty1 `eqType` ty2 -- See Note [Optimise CoVarCo to Refl]
286 = mkReflCo (chooseRole rep r) ty1
287
288 | otherwise
289 = assert (isCoVar cv1 )
290 wrapRole rep r $ wrapSym sym $
291 CoVarCo cv1
292
293 where
294 Pair ty1 ty2 = coVarTypes cv1
295
296 cv1 = case lookupInScope (lcInScopeSet env) cv of
297 Just cv1 -> cv1
298 Nothing -> warnPprTrace True
299 (text "opt_co: not in scope:" <+> ppr cv $$ ppr env)
300 cv
301 -- cv1 might have a substituted kind!
302
303 opt_co4 _ _ _ _ (HoleCo h)
304 = pprPanic "opt_univ fell into a hole" (ppr h)
305
306 opt_co4 env sym rep r (AxiomInstCo con ind cos)
307 -- Do *not* push sym inside top-level axioms
308 -- e.g. if g is a top-level axiom
309 -- g a : f a ~ a
310 -- then (sym (g ty)) /= g (sym ty) !!
311 = assert (r == coAxiomRole con )
312 wrapRole rep (coAxiomRole con) $
313 wrapSym sym $
314 -- some sub-cos might be P: use opt_co2
315 -- See Note [Optimising coercion optimisation]
316 AxiomInstCo con ind (zipWith (opt_co2 env False)
317 (coAxBranchRoles (coAxiomNthBranch con ind))
318 cos)
319 -- Note that the_co does *not* have sym pushed into it
320
321 opt_co4 env sym rep r (UnivCo prov _r t1 t2)
322 = assert (r == _r )
323 opt_univ env sym prov (chooseRole rep r) t1 t2
324
325 opt_co4 env sym rep r (TransCo co1 co2)
326 -- sym (g `o` h) = sym h `o` sym g
327 | sym = opt_trans in_scope co2' co1'
328 | otherwise = opt_trans in_scope co1' co2'
329 where
330 co1' = opt_co4_wrap env sym rep r co1
331 co2' = opt_co4_wrap env sym rep r co2
332 in_scope = lcInScopeSet env
333
334 opt_co4 env _sym rep r (NthCo _r n co)
335 | Just (ty, _) <- isReflCo_maybe co
336 , Just (_tc, args) <- assert (r == _r )
337 splitTyConApp_maybe ty
338 = liftCoSubst (chooseRole rep r) env (args `getNth` n)
339
340 | Just (ty, _) <- isReflCo_maybe co
341 , n == 0
342 , Just (tv, _) <- splitForAllTyCoVar_maybe ty
343 -- works for both tyvar and covar
344 = liftCoSubst (chooseRole rep r) env (varType tv)
345
346 opt_co4 env sym rep r (NthCo r1 n (TyConAppCo _ _ cos))
347 = assert (r == r1 )
348 opt_co4_wrap env sym rep r (cos `getNth` n)
349
350 -- see the definition of GHC.Builtin.Types.Prim.funTyCon
351 opt_co4 env sym rep r (NthCo r1 n (FunCo _r2 w co1 co2))
352 = assert (r == r1 )
353 opt_co4_wrap env sym rep r (mkNthCoFunCo n w co1 co2)
354
355 opt_co4 env sym rep r (NthCo _r n (ForAllCo _ eta _))
356 -- works for both tyvar and covar
357 = assert (r == _r )
358 assert (n == 0 )
359 opt_co4_wrap env sym rep Nominal eta
360
361 opt_co4 env sym rep r (NthCo _r n co)
362 | Just nth_co <- case co' of
363 TyConAppCo _ _ cos -> Just (cos `getNth` n)
364 FunCo _ w co1 co2 -> Just (mkNthCoFunCo n w co1 co2)
365 ForAllCo _ eta _ -> Just eta
366 _ -> Nothing
367 = if rep && (r == Nominal)
368 -- keep propagating the SubCo
369 then opt_co4_wrap (zapLiftingContext env) False True Nominal nth_co
370 else nth_co
371
372 | otherwise
373 = wrapRole rep r $ NthCo r n co'
374 where
375 co' = opt_co1 env sym co
376
377 opt_co4 env sym rep r (LRCo lr co)
378 | Just pr_co <- splitAppCo_maybe co
379 = assert (r == Nominal )
380 opt_co4_wrap env sym rep Nominal (pick_lr lr pr_co)
381 | Just pr_co <- splitAppCo_maybe co'
382 = assert (r == Nominal) $
383 if rep
384 then opt_co4_wrap (zapLiftingContext env) False True Nominal (pick_lr lr pr_co)
385 else pick_lr lr pr_co
386 | otherwise
387 = wrapRole rep Nominal $ LRCo lr co'
388 where
389 co' = opt_co4_wrap env sym False Nominal co
390
391 pick_lr CLeft (l, _) = l
392 pick_lr CRight (_, r) = r
393
394 -- See Note [Optimising InstCo]
395 opt_co4 env sym rep r (InstCo co1 arg)
396 -- forall over type...
397 | Just (tv, kind_co, co_body) <- splitForAllCo_ty_maybe co1
398 = opt_co4_wrap (extendLiftingContext env tv
399 (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co) sym_arg))
400 -- mkSymCo kind_co :: k1 ~ k2
401 -- sym_arg :: (t1 :: k1) ~ (t2 :: k2)
402 -- tv |-> (t1 :: k1) ~ (((t2 :: k2) |> (sym kind_co)) :: k1)
403 sym rep r co_body
404
405 -- forall over coercion...
406 | Just (cv, kind_co, co_body) <- splitForAllCo_co_maybe co1
407 , CoercionTy h1 <- t1
408 , CoercionTy h2 <- t2
409 = let new_co = mk_new_co cv (opt_co4_wrap env sym False Nominal kind_co) h1 h2
410 in opt_co4_wrap (extendLiftingContext env cv new_co) sym rep r co_body
411
412 -- See if it is a forall after optimization
413 -- If so, do an inefficient one-variable substitution, then re-optimize
414
415 -- forall over type...
416 | Just (tv', kind_co', co_body') <- splitForAllCo_ty_maybe co1'
417 = opt_co4_wrap (extendLiftingContext (zapLiftingContext env) tv'
418 (mkCoherenceRightCo Nominal t2' (mkSymCo kind_co') arg'))
419 False False r' co_body'
420
421 -- forall over coercion...
422 | Just (cv', kind_co', co_body') <- splitForAllCo_co_maybe co1'
423 , CoercionTy h1' <- t1'
424 , CoercionTy h2' <- t2'
425 = let new_co = mk_new_co cv' kind_co' h1' h2'
426 in opt_co4_wrap (extendLiftingContext (zapLiftingContext env) cv' new_co)
427 False False r' co_body'
428
429 | otherwise = InstCo co1' arg'
430 where
431 co1' = opt_co4_wrap env sym rep r co1
432 r' = chooseRole rep r
433 arg' = opt_co4_wrap env sym False Nominal arg
434 sym_arg = wrapSym sym arg'
435
436 -- Performance note: don't be alarmed by the two calls to coercionKind
437 -- here, as only one call to coercionKind is actually demanded per guard.
438 -- t1/t2 are used when checking if co1 is a forall, and t1'/t2' are used
439 -- when checking if co1' (i.e., co1 post-optimization) is a forall.
440 --
441 -- t1/t2 must come from sym_arg, not arg', since it's possible that arg'
442 -- might have an extra Sym at the front (after being optimized) that co1
443 -- lacks, so we need to use sym_arg to balance the number of Syms. (#15725)
444 Pair t1 t2 = coercionKind sym_arg
445 Pair t1' t2' = coercionKind arg'
446
447 mk_new_co cv kind_co h1 h2
448 = let -- h1 :: (t1 ~ t2)
449 -- h2 :: (t3 ~ t4)
450 -- kind_co :: (t1 ~ t2) ~ (t3 ~ t4)
451 -- n1 :: t1 ~ t3
452 -- n2 :: t2 ~ t4
453 -- new_co = (h1 :: t1 ~ t2) ~ ((n1;h2;sym n2) :: t1 ~ t2)
454 r2 = coVarRole cv
455 kind_co' = downgradeRole r2 Nominal kind_co
456 n1 = mkNthCo r2 2 kind_co'
457 n2 = mkNthCo r2 3 kind_co'
458 in mkProofIrrelCo Nominal (Refl (coercionType h1)) h1
459 (n1 `mkTransCo` h2 `mkTransCo` (mkSymCo n2))
460
461 opt_co4 env sym _rep r (KindCo co)
462 = assert (r == Nominal) $
463 let kco' = promoteCoercion co in
464 case kco' of
465 KindCo co' -> promoteCoercion (opt_co1 env sym co')
466 _ -> opt_co4_wrap env sym False Nominal kco'
467 -- This might be able to be optimized more to do the promotion
468 -- and substitution/optimization at the same time
469
470 opt_co4 env sym _ r (SubCo co)
471 = assert (r == Representational) $
472 opt_co4_wrap env sym True Nominal co
473
474 -- This could perhaps be optimized more.
475 opt_co4 env sym rep r (AxiomRuleCo co cs)
476 = assert (r == coaxrRole co) $
477 wrapRole rep r $
478 wrapSym sym $
479 AxiomRuleCo co (zipWith (opt_co2 env False) (coaxrAsmpRoles co) cs)
480
481 {- Note [Optimise CoVarCo to Refl]
482 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
483 If we have (c :: t~t) we can optimise it to Refl. That increases the
484 chances of floating the Refl upwards; e.g. Maybe c --> Refl (Maybe t)
485
486 We do so here in optCoercion, not in mkCoVarCo; see Note [mkCoVarCo]
487 in GHC.Core.Coercion.
488 -}
489
490 -------------
491 -- | Optimize a phantom coercion. The input coercion may not necessarily
492 -- be a phantom, but the output sure will be.
493 opt_phantom :: LiftingContext -> SymFlag -> Coercion -> NormalCo
494 opt_phantom env sym co
495 = opt_univ env sym (PhantomProv (mkKindCo co)) Phantom ty1 ty2
496 where
497 Pair ty1 ty2 = coercionKind co
498
499 {- Note [Differing kinds]
500 ~~~~~~~~~~~~~~~~~~~~~~
501 The two types may not have the same kind (although that would be very unusual).
502 But even if they have the same kind, and the same type constructor, the number
503 of arguments in a `CoTyConApp` can differ. Consider
504
505 Any :: forall k. k
506
507 Any * Int :: *
508 Any (*->*) Maybe Int :: *
509
510 Hence the need to compare argument lengths; see #13658
511
512 Note [opt_univ needs injectivity]
513 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
514 If opt_univ sees a coercion between `T a1 a2` and `T b1 b2` it will optimize it
515 by producing a TyConAppCo for T, and pushing the UnivCo into the arguments. But
516 this works only if T is injective. Otherwise we can have something like
517
518 type family F x where
519 F Int = Int
520 F Bool = Int
521
522 where `UnivCo :: F Int ~ F Bool` is reasonable (it is effectively just an
523 alternative representation for a couple of uses of AxiomInstCos) but we do not
524 want to produce `F (UnivCo :: Int ~ Bool)` where the inner coercion is clearly
525 inconsistent. Hence the opt_univ case for TyConApps checks isInjectiveTyCon.
526 See #19509.
527
528 -}
529
530 opt_univ :: LiftingContext -> SymFlag -> UnivCoProvenance -> Role
531 -> Type -> Type -> Coercion
532 opt_univ env sym (PhantomProv h) _r ty1 ty2
533 | sym = mkPhantomCo h' ty2' ty1'
534 | otherwise = mkPhantomCo h' ty1' ty2'
535 where
536 h' = opt_co4 env sym False Nominal h
537 ty1' = substTy (lcSubstLeft env) ty1
538 ty2' = substTy (lcSubstRight env) ty2
539
540 opt_univ env sym prov role oty1 oty2
541 | Just (tc1, tys1) <- splitTyConApp_maybe oty1
542 , Just (tc2, tys2) <- splitTyConApp_maybe oty2
543 , tc1 == tc2
544 , isInjectiveTyCon tc1 role -- see Note [opt_univ needs injectivity]
545 , equalLength tys1 tys2 -- see Note [Differing kinds]
546 -- NB: prov must not be the two interesting ones (ProofIrrel & Phantom);
547 -- Phantom is already taken care of, and ProofIrrel doesn't relate tyconapps
548 = let roles = tyConRolesX role tc1
549 arg_cos = zipWith3 (mkUnivCo prov') roles tys1 tys2
550 arg_cos' = zipWith (opt_co4 env sym False) roles arg_cos
551 in
552 mkTyConAppCo role tc1 arg_cos'
553
554 -- can't optimize the AppTy case because we can't build the kind coercions.
555
556 | Just (tv1, ty1) <- splitForAllTyVar_maybe oty1
557 , Just (tv2, ty2) <- splitForAllTyVar_maybe oty2
558 -- NB: prov isn't interesting here either
559 = let k1 = tyVarKind tv1
560 k2 = tyVarKind tv2
561 eta = mkUnivCo prov' Nominal k1 k2
562 -- eta gets opt'ed soon, but not yet.
563 ty2' = substTyWith [tv2] [TyVarTy tv1 `mkCastTy` eta] ty2
564
565 (env', tv1', eta') = optForAllCoBndr env sym tv1 eta
566 in
567 mkForAllCo tv1' eta' (opt_univ env' sym prov' role ty1 ty2')
568
569 | Just (cv1, ty1) <- splitForAllCoVar_maybe oty1
570 , Just (cv2, ty2) <- splitForAllCoVar_maybe oty2
571 -- NB: prov isn't interesting here either
572 = let k1 = varType cv1
573 k2 = varType cv2
574 r' = coVarRole cv1
575 eta = mkUnivCo prov' Nominal k1 k2
576 eta_d = downgradeRole r' Nominal eta
577 -- eta gets opt'ed soon, but not yet.
578 n_co = (mkSymCo $ mkNthCo r' 2 eta_d) `mkTransCo`
579 (mkCoVarCo cv1) `mkTransCo`
580 (mkNthCo r' 3 eta_d)
581 ty2' = substTyWithCoVars [cv2] [n_co] ty2
582
583 (env', cv1', eta') = optForAllCoBndr env sym cv1 eta
584 in
585 mkForAllCo cv1' eta' (opt_univ env' sym prov' role ty1 ty2')
586
587 | otherwise
588 = let ty1 = substTyUnchecked (lcSubstLeft env) oty1
589 ty2 = substTyUnchecked (lcSubstRight env) oty2
590 (a, b) | sym = (ty2, ty1)
591 | otherwise = (ty1, ty2)
592 in
593 mkUnivCo prov' role a b
594
595 where
596 prov' = case prov of
597 #if __GLASGOW_HASKELL__ < 901
598 -- This alt is redundant with the first match of the FunDef
599 PhantomProv kco -> PhantomProv $ opt_co4_wrap env sym False Nominal kco
600 #endif
601 ProofIrrelProv kco -> ProofIrrelProv $ opt_co4_wrap env sym False Nominal kco
602 PluginProv _ -> prov
603 CorePrepProv _ -> prov
604
605 -------------
606 opt_transList :: HasDebugCallStack => InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
607 opt_transList is = zipWithEqual "opt_transList" (opt_trans is)
608 -- The input lists must have identical length.
609
610 opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
611 opt_trans is co1 co2
612 | isReflCo co1 = co2
613 -- optimize when co1 is a Refl Co
614 | otherwise = opt_trans1 is co1 co2
615
616 opt_trans1 :: InScopeSet -> NormalNonIdCo -> NormalCo -> NormalCo
617 -- First arg is not the identity
618 opt_trans1 is co1 co2
619 | isReflCo co2 = co1
620 -- optimize when co2 is a Refl Co
621 | otherwise = opt_trans2 is co1 co2
622
623 opt_trans2 :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> NormalCo
624 -- Neither arg is the identity
625 opt_trans2 is (TransCo co1a co1b) co2
626 -- Don't know whether the sub-coercions are the identity
627 = opt_trans is co1a (opt_trans is co1b co2)
628
629 opt_trans2 is co1 co2
630 | Just co <- opt_trans_rule is co1 co2
631 = co
632
633 opt_trans2 is co1 (TransCo co2a co2b)
634 | Just co1_2a <- opt_trans_rule is co1 co2a
635 = if isReflCo co1_2a
636 then co2b
637 else opt_trans1 is co1_2a co2b
638
639 opt_trans2 _ co1 co2
640 = mkTransCo co1 co2
641
642 ------
643 -- Optimize coercions with a top-level use of transitivity.
644 opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
645
646 opt_trans_rule is in_co1@(GRefl r1 t1 (MCo co1)) in_co2@(GRefl r2 _ (MCo co2))
647 = assert (r1 == r2) $
648 fireTransRule "GRefl" in_co1 in_co2 $
649 mkGReflRightCo r1 t1 (opt_trans is co1 co2)
650
651 -- Push transitivity through matching destructors
652 opt_trans_rule is in_co1@(NthCo r1 d1 co1) in_co2@(NthCo r2 d2 co2)
653 | d1 == d2
654 , coercionRole co1 == coercionRole co2
655 , co1 `compatible_co` co2
656 = assert (r1 == r2) $
657 fireTransRule "PushNth" in_co1 in_co2 $
658 mkNthCo r1 d1 (opt_trans is co1 co2)
659
660 opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2)
661 | d1 == d2
662 , co1 `compatible_co` co2
663 = fireTransRule "PushLR" in_co1 in_co2 $
664 mkLRCo d1 (opt_trans is co1 co2)
665
666 -- Push transitivity inside instantiation
667 opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
668 | ty1 `eqCoercion` ty2
669 , co1 `compatible_co` co2
670 = fireTransRule "TrPushInst" in_co1 in_co2 $
671 mkInstCo (opt_trans is co1 co2) ty1
672
673 opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1)
674 in_co2@(UnivCo p2 r2 _tyl2 tyr2)
675 | Just prov' <- opt_trans_prov p1 p2
676 = assert (r1 == r2) $
677 fireTransRule "UnivCo" in_co1 in_co2 $
678 mkUnivCo prov' r1 tyl1 tyr2
679 where
680 -- if the provenances are different, opt'ing will be very confusing
681 opt_trans_prov (PhantomProv kco1) (PhantomProv kco2)
682 = Just $ PhantomProv $ opt_trans is kco1 kco2
683 opt_trans_prov (ProofIrrelProv kco1) (ProofIrrelProv kco2)
684 = Just $ ProofIrrelProv $ opt_trans is kco1 kco2
685 opt_trans_prov (PluginProv str1) (PluginProv str2) | str1 == str2 = Just p1
686 opt_trans_prov _ _ = Nothing
687
688 -- Push transitivity down through matching top-level constructors.
689 opt_trans_rule is in_co1@(TyConAppCo r1 tc1 cos1) in_co2@(TyConAppCo r2 tc2 cos2)
690 | tc1 == tc2
691 = assert (r1 == r2) $
692 fireTransRule "PushTyConApp" in_co1 in_co2 $
693 mkTyConAppCo r1 tc1 (opt_transList is cos1 cos2)
694
695 opt_trans_rule is in_co1@(FunCo r1 w1 co1a co1b) in_co2@(FunCo r2 w2 co2a co2b)
696 = assert (r1 == r2) $ -- Just like the TyConAppCo/TyConAppCo case
697 fireTransRule "PushFun" in_co1 in_co2 $
698 mkFunCo r1 (opt_trans is w1 w2) (opt_trans is co1a co2a) (opt_trans is co1b co2b)
699
700 opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
701 -- Must call opt_trans_rule_app; see Note [EtaAppCo]
702 = opt_trans_rule_app is in_co1 in_co2 co1a [co1b] co2a [co2b]
703
704 -- Eta rules
705 opt_trans_rule is co1@(TyConAppCo r tc cos1) co2
706 | Just cos2 <- etaTyConAppCo_maybe tc co2
707 = fireTransRule "EtaCompL" co1 co2 $
708 mkTyConAppCo r tc (opt_transList is cos1 cos2)
709
710 opt_trans_rule is co1 co2@(TyConAppCo r tc cos2)
711 | Just cos1 <- etaTyConAppCo_maybe tc co1
712 = fireTransRule "EtaCompR" co1 co2 $
713 mkTyConAppCo r tc (opt_transList is cos1 cos2)
714
715 opt_trans_rule is co1@(AppCo co1a co1b) co2
716 | Just (co2a,co2b) <- etaAppCo_maybe co2
717 = opt_trans_rule_app is co1 co2 co1a [co1b] co2a [co2b]
718
719 opt_trans_rule is co1 co2@(AppCo co2a co2b)
720 | Just (co1a,co1b) <- etaAppCo_maybe co1
721 = opt_trans_rule_app is co1 co2 co1a [co1b] co2a [co2b]
722
723 -- Push transitivity inside forall
724 -- forall over types.
725 opt_trans_rule is co1 co2
726 | Just (tv1, eta1, r1) <- splitForAllCo_ty_maybe co1
727 , Just (tv2, eta2, r2) <- etaForAllCo_ty_maybe co2
728 = push_trans tv1 eta1 r1 tv2 eta2 r2
729
730 | Just (tv2, eta2, r2) <- splitForAllCo_ty_maybe co2
731 , Just (tv1, eta1, r1) <- etaForAllCo_ty_maybe co1
732 = push_trans tv1 eta1 r1 tv2 eta2 r2
733
734 where
735 push_trans tv1 eta1 r1 tv2 eta2 r2
736 -- Given:
737 -- co1 = /\ tv1 : eta1. r1
738 -- co2 = /\ tv2 : eta2. r2
739 -- Wanted:
740 -- /\tv1 : (eta1;eta2). (r1; r2[tv2 |-> tv1 |> eta1])
741 = fireTransRule "EtaAllTy_ty" co1 co2 $
742 mkForAllCo tv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2')
743 where
744 is' = is `extendInScopeSet` tv1
745 r2' = substCoWithUnchecked [tv2] [mkCastTy (TyVarTy tv1) eta1] r2
746
747 -- Push transitivity inside forall
748 -- forall over coercions.
749 opt_trans_rule is co1 co2
750 | Just (cv1, eta1, r1) <- splitForAllCo_co_maybe co1
751 , Just (cv2, eta2, r2) <- etaForAllCo_co_maybe co2
752 = push_trans cv1 eta1 r1 cv2 eta2 r2
753
754 | Just (cv2, eta2, r2) <- splitForAllCo_co_maybe co2
755 , Just (cv1, eta1, r1) <- etaForAllCo_co_maybe co1
756 = push_trans cv1 eta1 r1 cv2 eta2 r2
757
758 where
759 push_trans cv1 eta1 r1 cv2 eta2 r2
760 -- Given:
761 -- co1 = /\ cv1 : eta1. r1
762 -- co2 = /\ cv2 : eta2. r2
763 -- Wanted:
764 -- n1 = nth 2 eta1
765 -- n2 = nth 3 eta1
766 -- nco = /\ cv1 : (eta1;eta2). (r1; r2[cv2 |-> (sym n1);cv1;n2])
767 = fireTransRule "EtaAllTy_co" co1 co2 $
768 mkForAllCo cv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2')
769 where
770 is' = is `extendInScopeSet` cv1
771 role = coVarRole cv1
772 eta1' = downgradeRole role Nominal eta1
773 n1 = mkNthCo role 2 eta1'
774 n2 = mkNthCo role 3 eta1'
775 r2' = substCo (zipCvSubst [cv2] [(mkSymCo n1) `mkTransCo`
776 (mkCoVarCo cv1) `mkTransCo` n2])
777 r2
778
779 -- Push transitivity inside axioms
780 opt_trans_rule is co1 co2
781
782 -- See Note [Why call checkAxInstCo during optimisation]
783 -- TrPushSymAxR
784 | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
785 , True <- sym
786 , Just cos2 <- matchAxiom sym con ind co2
787 , let newAxInst = AxiomInstCo con ind (opt_transList is (map mkSymCo cos2) cos1)
788 , Nothing <- checkAxInstCo newAxInst
789 = fireTransRule "TrPushSymAxR" co1 co2 $ SymCo newAxInst
790
791 -- TrPushAxR
792 | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
793 , False <- sym
794 , Just cos2 <- matchAxiom sym con ind co2
795 , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
796 , Nothing <- checkAxInstCo newAxInst
797 = fireTransRule "TrPushAxR" co1 co2 newAxInst
798
799 -- TrPushSymAxL
800 | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
801 , True <- sym
802 , Just cos1 <- matchAxiom (not sym) con ind co1
803 , let newAxInst = AxiomInstCo con ind (opt_transList is cos2 (map mkSymCo cos1))
804 , Nothing <- checkAxInstCo newAxInst
805 = fireTransRule "TrPushSymAxL" co1 co2 $ SymCo newAxInst
806
807 -- TrPushAxL
808 | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
809 , False <- sym
810 , Just cos1 <- matchAxiom (not sym) con ind co1
811 , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
812 , Nothing <- checkAxInstCo newAxInst
813 = fireTransRule "TrPushAxL" co1 co2 newAxInst
814
815 -- TrPushAxSym/TrPushSymAx
816 | Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe
817 , Just (sym2, con2, ind2, cos2) <- co2_is_axiom_maybe
818 , con1 == con2
819 , ind1 == ind2
820 , sym1 == not sym2
821 , let branch = coAxiomNthBranch con1 ind1
822 qtvs = coAxBranchTyVars branch ++ coAxBranchCoVars branch
823 lhs = coAxNthLHS con1 ind1
824 rhs = coAxBranchRHS branch
825 pivot_tvs = exactTyCoVarsOfType (if sym2 then rhs else lhs)
826 , all (`elemVarSet` pivot_tvs) qtvs
827 = fireTransRule "TrPushAxSym" co1 co2 $
828 if sym2
829 -- TrPushAxSym
830 then liftCoSubstWith role qtvs (opt_transList is cos1 (map mkSymCo cos2)) lhs
831 -- TrPushSymAx
832 else liftCoSubstWith role qtvs (opt_transList is (map mkSymCo cos1) cos2) rhs
833 where
834 co1_is_axiom_maybe = isAxiom_maybe co1
835 co2_is_axiom_maybe = isAxiom_maybe co2
836 role = coercionRole co1 -- should be the same as coercionRole co2!
837
838 opt_trans_rule _ co1 co2 -- Identity rule
839 | let ty1 = coercionLKind co1
840 r = coercionRole co1
841 ty2 = coercionRKind co2
842 , ty1 `eqType` ty2
843 = fireTransRule "RedTypeDirRefl" co1 co2 $
844 mkReflCo r ty2
845
846 opt_trans_rule _ _ _ = Nothing
847
848 -- See Note [EtaAppCo]
849 opt_trans_rule_app :: InScopeSet
850 -> Coercion -- original left-hand coercion (printing only)
851 -> Coercion -- original right-hand coercion (printing only)
852 -> Coercion -- left-hand coercion "function"
853 -> [Coercion] -- left-hand coercion "args"
854 -> Coercion -- right-hand coercion "function"
855 -> [Coercion] -- right-hand coercion "args"
856 -> Maybe Coercion
857 opt_trans_rule_app is orig_co1 orig_co2 co1a co1bs co2a co2bs
858 | AppCo co1aa co1ab <- co1a
859 , Just (co2aa, co2ab) <- etaAppCo_maybe co2a
860 = opt_trans_rule_app is orig_co1 orig_co2 co1aa (co1ab:co1bs) co2aa (co2ab:co2bs)
861
862 | AppCo co2aa co2ab <- co2a
863 , Just (co1aa, co1ab) <- etaAppCo_maybe co1a
864 = opt_trans_rule_app is orig_co1 orig_co2 co1aa (co1ab:co1bs) co2aa (co2ab:co2bs)
865
866 | otherwise
867 = assert (co1bs `equalLength` co2bs) $
868 fireTransRule ("EtaApps:" ++ show (length co1bs)) orig_co1 orig_co2 $
869 let rt1a = coercionRKind co1a
870
871 lt2a = coercionLKind co2a
872 rt2a = coercionRole co2a
873
874 rt1bs = map coercionRKind co1bs
875 lt2bs = map coercionLKind co2bs
876 rt2bs = map coercionRole co2bs
877
878 kcoa = mkKindCo $ buildCoercion lt2a rt1a
879 kcobs = map mkKindCo $ zipWith buildCoercion lt2bs rt1bs
880
881 co2a' = mkCoherenceLeftCo rt2a lt2a kcoa co2a
882 co2bs' = zipWith3 mkGReflLeftCo rt2bs lt2bs kcobs
883 co2bs'' = zipWith mkTransCo co2bs' co2bs
884 in
885 mkAppCos (opt_trans is co1a co2a')
886 (zipWith (opt_trans is) co1bs co2bs'')
887
888 fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
889 fireTransRule _rule _co1 _co2 res
890 = Just res
891
892 {-
893 Note [Conflict checking with AxiomInstCo]
894 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
895 Consider the following type family and axiom:
896
897 type family Equal (a :: k) (b :: k) :: Bool
898 type instance where
899 Equal a a = True
900 Equal a b = False
901 --
902 Equal :: forall k::*. k -> k -> Bool
903 axEqual :: { forall k::*. forall a::k. Equal k a a ~ True
904 ; forall k::*. forall a::k. forall b::k. Equal k a b ~ False }
905
906 We wish to disallow (axEqual[1] <*> <Int> <Int). (Recall that the index is
907 0-based, so this is the second branch of the axiom.) The problem is that, on
908 the surface, it seems that (axEqual[1] <*> <Int> <Int>) :: (Equal * Int Int ~
909 False) and that all is OK. But, all is not OK: we want to use the first branch
910 of the axiom in this case, not the second. The problem is that the parameters
911 of the first branch can unify with the supplied coercions, thus meaning that
912 the first branch should be taken. See also Note [Apartness] in
913 "GHC.Core.FamInstEnv".
914
915 Note [Why call checkAxInstCo during optimisation]
916 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
917 It is possible that otherwise-good-looking optimisations meet with disaster
918 in the presence of axioms with multiple equations. Consider
919
920 type family Equal (a :: *) (b :: *) :: Bool where
921 Equal a a = True
922 Equal a b = False
923 type family Id (a :: *) :: * where
924 Id a = a
925
926 axEq :: { [a::*]. Equal a a ~ True
927 ; [a::*, b::*]. Equal a b ~ False }
928 axId :: [a::*]. Id a ~ a
929
930 co1 = Equal (axId[0] Int) (axId[0] Bool)
931 :: Equal (Id Int) (Id Bool) ~ Equal Int Bool
932 co2 = axEq[1] <Int> <Bool>
933 :: Equal Int Bool ~ False
934
935 We wish to optimise (co1 ; co2). We end up in rule TrPushAxL, noting that
936 co2 is an axiom and that matchAxiom succeeds when looking at co1. But, what
937 happens when we push the coercions inside? We get
938
939 co3 = axEq[1] (axId[0] Int) (axId[0] Bool)
940 :: Equal (Id Int) (Id Bool) ~ False
941
942 which is bogus! This is because the type system isn't smart enough to know
943 that (Id Int) and (Id Bool) are Surely Apart, as they're headed by type
944 families. At the time of writing, I (Richard Eisenberg) couldn't think of
945 a way of detecting this any more efficient than just building the optimised
946 coercion and checking.
947
948 Note [EtaAppCo]
949 ~~~~~~~~~~~~~~~
950 Suppose we're trying to optimize (co1a co1b ; co2a co2b). Ideally, we'd
951 like to rewrite this to (co1a ; co2a) (co1b ; co2b). The problem is that
952 the resultant coercions might not be well kinded. Here is an example (things
953 labeled with x don't matter in this example):
954
955 k1 :: Type
956 k2 :: Type
957
958 a :: k1 -> Type
959 b :: k1
960
961 h :: k1 ~ k2
962
963 co1a :: x1 ~ (a |> (h -> <Type>)
964 co1b :: x2 ~ (b |> h)
965
966 co2a :: a ~ x3
967 co2b :: b ~ x4
968
969 First, convince yourself of the following:
970
971 co1a co1b :: x1 x2 ~ (a |> (h -> <Type>)) (b |> h)
972 co2a co2b :: a b ~ x3 x4
973
974 (a |> (h -> <Type>)) (b |> h) `eqType` a b
975
976 That last fact is due to Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep,
977 where we ignore coercions in types as long as two types' kinds are the same.
978 In our case, we meet this last condition, because
979
980 (a |> (h -> <Type>)) (b |> h) :: Type
981 and
982 a b :: Type
983
984 So the input coercion (co1a co1b ; co2a co2b) is well-formed. But the
985 suggested output coercions (co1a ; co2a) and (co1b ; co2b) are not -- the
986 kinds don't match up.
987
988 The solution here is to twiddle the kinds in the output coercions. First, we
989 need to find coercions
990
991 ak :: kind(a |> (h -> <Type>)) ~ kind(a)
992 bk :: kind(b |> h) ~ kind(b)
993
994 This can be done with mkKindCo and buildCoercion. The latter assumes two
995 types are identical modulo casts and builds a coercion between them.
996
997 Then, we build (co1a ; co2a |> sym ak) and (co1b ; co2b |> sym bk) as the
998 output coercions. These are well-kinded.
999
1000 Also, note that all of this is done after accumulated any nested AppCo
1001 parameters. This step is to avoid quadratic behavior in calling coercionKind.
1002
1003 The problem described here was first found in dependent/should_compile/dynamic-paper.
1004
1005 -}
1006
1007 -- | Check to make sure that an AxInstCo is internally consistent.
1008 -- Returns the conflicting branch, if it exists
1009 -- See Note [Conflict checking with AxiomInstCo]
1010 checkAxInstCo :: Coercion -> Maybe CoAxBranch
1011 -- defined here to avoid dependencies in GHC.Core.Coercion
1012 -- If you edit this function, you may need to update the GHC formalism
1013 -- See Note [GHC Formalism] in GHC.Core.Lint
1014 checkAxInstCo (AxiomInstCo ax ind cos)
1015 = let branch = coAxiomNthBranch ax ind
1016 tvs = coAxBranchTyVars branch
1017 cvs = coAxBranchCoVars branch
1018 incomps = coAxBranchIncomps branch
1019 (tys, cotys) = splitAtList tvs (map coercionLKind cos)
1020 co_args = map stripCoercionTy cotys
1021 subst = zipTvSubst tvs tys `composeTCvSubst`
1022 zipCvSubst cvs co_args
1023 target = Type.substTys subst (coAxBranchLHS branch)
1024 in_scope = mkInScopeSet $
1025 unionVarSets (map (tyCoVarsOfTypes . coAxBranchLHS) incomps)
1026 flattened_target = flattenTys in_scope target in
1027 check_no_conflict flattened_target incomps
1028 where
1029 check_no_conflict :: [Type] -> [CoAxBranch] -> Maybe CoAxBranch
1030 check_no_conflict _ [] = Nothing
1031 check_no_conflict flat (b@CoAxBranch { cab_lhs = lhs_incomp } : rest)
1032 -- See Note [Apartness] in GHC.Core.FamInstEnv
1033 | SurelyApart <- tcUnifyTysFG alwaysBindFun flat lhs_incomp
1034 = check_no_conflict flat rest
1035 | otherwise
1036 = Just b
1037 checkAxInstCo _ = Nothing
1038
1039
1040 -----------
1041 wrapSym :: SymFlag -> Coercion -> Coercion
1042 wrapSym sym co | sym = mkSymCo co
1043 | otherwise = co
1044
1045 -- | Conditionally set a role to be representational
1046 wrapRole :: ReprFlag
1047 -> Role -- ^ current role
1048 -> Coercion -> Coercion
1049 wrapRole False _ = id
1050 wrapRole True current = downgradeRole Representational current
1051
1052 -- | If we require a representational role, return that. Otherwise,
1053 -- return the "default" role provided.
1054 chooseRole :: ReprFlag
1055 -> Role -- ^ "default" role
1056 -> Role
1057 chooseRole True _ = Representational
1058 chooseRole _ r = r
1059
1060 -----------
1061 isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom Branched, Int, [Coercion])
1062 isAxiom_maybe (SymCo co)
1063 | Just (sym, con, ind, cos) <- isAxiom_maybe co
1064 = Just (not sym, con, ind, cos)
1065 isAxiom_maybe (AxiomInstCo con ind cos)
1066 = Just (False, con, ind, cos)
1067 isAxiom_maybe _ = Nothing
1068
1069 matchAxiom :: Bool -- True = match LHS, False = match RHS
1070 -> CoAxiom br -> Int -> Coercion -> Maybe [Coercion]
1071 matchAxiom sym ax@(CoAxiom { co_ax_tc = tc }) ind co
1072 | CoAxBranch { cab_tvs = qtvs
1073 , cab_cvs = [] -- can't infer these, so fail if there are any
1074 , cab_roles = roles
1075 , cab_lhs = lhs
1076 , cab_rhs = rhs } <- coAxiomNthBranch ax ind
1077 , Just subst <- liftCoMatch (mkVarSet qtvs)
1078 (if sym then (mkTyConApp tc lhs) else rhs)
1079 co
1080 , all (`isMappedByLC` subst) qtvs
1081 = zipWithM (liftCoSubstTyVar subst) roles qtvs
1082
1083 | otherwise
1084 = Nothing
1085
1086 -------------
1087 compatible_co :: Coercion -> Coercion -> Bool
1088 -- Check whether (co1 . co2) will be well-kinded
1089 compatible_co co1 co2
1090 = x1 `eqType` x2
1091 where
1092 x1 = coercionRKind co1
1093 x2 = coercionLKind co2
1094
1095 -------------
1096 {-
1097 etaForAllCo
1098 ~~~~~~~~~~~~~~~~~
1099 (1) etaForAllCo_ty_maybe
1100 Suppose we have
1101
1102 g : all a1:k1.t1 ~ all a2:k2.t2
1103
1104 but g is *not* a ForAllCo. We want to eta-expand it. So, we do this:
1105
1106 g' = all a1:(ForAllKindCo g).(InstCo g (a1 ~ a1 |> ForAllKindCo g))
1107
1108 Call the kind coercion h1 and the body coercion h2. We can see that
1109
1110 h2 : t1 ~ t2[a2 |-> (a1 |> h1)]
1111
1112 According to the typing rule for ForAllCo, we get that
1113
1114 g' : all a1:k1.t1 ~ all a1:k2.(t2[a2 |-> (a1 |> h1)][a1 |-> a1 |> sym h1])
1115
1116 or
1117
1118 g' : all a1:k1.t1 ~ all a1:k2.(t2[a2 |-> a1])
1119
1120 as desired.
1121
1122 (2) etaForAllCo_co_maybe
1123 Suppose we have
1124
1125 g : all c1:(s1~s2). t1 ~ all c2:(s3~s4). t2
1126
1127 Similarly, we do this
1128
1129 g' = all c1:h1. h2
1130 : all c1:(s1~s2). t1 ~ all c1:(s3~s4). t2[c2 |-> (sym eta1;c1;eta2)]
1131 [c1 |-> eta1;c1;sym eta2]
1132
1133 Here,
1134
1135 h1 = mkNthCo Nominal 0 g :: (s1~s2)~(s3~s4)
1136 eta1 = mkNthCo r 2 h1 :: (s1 ~ s3)
1137 eta2 = mkNthCo r 3 h1 :: (s2 ~ s4)
1138 h2 = mkInstCo g (cv1 ~ (sym eta1;c1;eta2))
1139 -}
1140 etaForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
1141 -- Try to make the coercion be of form (forall tv:kind_co. co)
1142 etaForAllCo_ty_maybe co
1143 | Just (tv, kind_co, r) <- splitForAllCo_ty_maybe co
1144 = Just (tv, kind_co, r)
1145
1146 | Pair ty1 ty2 <- coercionKind co
1147 , Just (tv1, _) <- splitForAllTyVar_maybe ty1
1148 , isForAllTy_ty ty2
1149 , let kind_co = mkNthCo Nominal 0 co
1150 = Just ( tv1, kind_co
1151 , mkInstCo co (mkGReflRightCo Nominal (TyVarTy tv1) kind_co))
1152
1153 | otherwise
1154 = Nothing
1155
1156 etaForAllCo_co_maybe :: Coercion -> Maybe (CoVar, Coercion, Coercion)
1157 -- Try to make the coercion be of form (forall cv:kind_co. co)
1158 etaForAllCo_co_maybe co
1159 | Just (cv, kind_co, r) <- splitForAllCo_co_maybe co
1160 = Just (cv, kind_co, r)
1161
1162 | Pair ty1 ty2 <- coercionKind co
1163 , Just (cv1, _) <- splitForAllCoVar_maybe ty1
1164 , isForAllTy_co ty2
1165 = let kind_co = mkNthCo Nominal 0 co
1166 r = coVarRole cv1
1167 l_co = mkCoVarCo cv1
1168 kind_co' = downgradeRole r Nominal kind_co
1169 r_co = (mkSymCo (mkNthCo r 2 kind_co')) `mkTransCo`
1170 l_co `mkTransCo`
1171 (mkNthCo r 3 kind_co')
1172 in Just ( cv1, kind_co
1173 , mkInstCo co (mkProofIrrelCo Nominal kind_co l_co r_co))
1174
1175 | otherwise
1176 = Nothing
1177
1178 etaAppCo_maybe :: Coercion -> Maybe (Coercion,Coercion)
1179 -- If possible, split a coercion
1180 -- g :: t1a t1b ~ t2a t2b
1181 -- into a pair of coercions (left g, right g)
1182 etaAppCo_maybe co
1183 | Just (co1,co2) <- splitAppCo_maybe co
1184 = Just (co1,co2)
1185 | (Pair ty1 ty2, Nominal) <- coercionKindRole co
1186 , Just (_,t1) <- splitAppTy_maybe ty1
1187 , Just (_,t2) <- splitAppTy_maybe ty2
1188 , let isco1 = isCoercionTy t1
1189 , let isco2 = isCoercionTy t2
1190 , isco1 == isco2
1191 = Just (LRCo CLeft co, LRCo CRight co)
1192 | otherwise
1193 = Nothing
1194
1195 etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
1196 -- If possible, split a coercion
1197 -- g :: T s1 .. sn ~ T t1 .. tn
1198 -- into [ Nth 0 g :: s1~t1, ..., Nth (n-1) g :: sn~tn ]
1199 etaTyConAppCo_maybe tc (TyConAppCo _ tc2 cos2)
1200 = assert (tc == tc2) $ Just cos2
1201
1202 etaTyConAppCo_maybe tc co
1203 | not (mustBeSaturated tc)
1204 , (Pair ty1 ty2, r) <- coercionKindRole co
1205 , Just (tc1, tys1) <- splitTyConApp_maybe ty1
1206 , Just (tc2, tys2) <- splitTyConApp_maybe ty2
1207 , tc1 == tc2
1208 , isInjectiveTyCon tc r -- See Note [NthCo and newtypes] in GHC.Core.TyCo.Rep
1209 , let n = length tys1
1210 , tys2 `lengthIs` n -- This can fail in an erroneous program
1211 -- E.g. T a ~# T a b
1212 -- #14607
1213 = assert (tc == tc1) $
1214 Just (decomposeCo n co (tyConRolesX r tc1))
1215 -- NB: n might be <> tyConArity tc
1216 -- e.g. data family T a :: * -> *
1217 -- g :: T a b ~ T c d
1218
1219 | otherwise
1220 = Nothing
1221
1222 {-
1223 Note [Eta for AppCo]
1224 ~~~~~~~~~~~~~~~~~~~~
1225 Suppose we have
1226 g :: s1 t1 ~ s2 t2
1227
1228 Then we can't necessarily make
1229 left g :: s1 ~ s2
1230 right g :: t1 ~ t2
1231 because it's possible that
1232 s1 :: * -> * t1 :: *
1233 s2 :: (*->*) -> * t2 :: * -> *
1234 and in that case (left g) does not have the same
1235 kind on either side.
1236
1237 It's enough to check that
1238 kind t1 = kind t2
1239 because if g is well-kinded then
1240 kind (s1 t2) = kind (s2 t2)
1241 and these two imply
1242 kind s1 = kind s2
1243
1244 -}
1245
1246 optForAllCoBndr :: LiftingContext -> Bool
1247 -> TyCoVar -> Coercion -> (LiftingContext, TyCoVar, Coercion)
1248 optForAllCoBndr env sym
1249 = substForAllCoBndrUsingLC sym (opt_co4_wrap env sym False Nominal) env