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