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