Drop GHC 7.10 compatibility
[ghc.git] / compiler / types / OptCoercion.hs
1 -- (c) The University of Glasgow 2006
2
3 {-# LANGUAGE CPP #-}
4
5 -- The default iteration limit is a bit too low for the definitions
6 -- in this module.
7 {-# OPTIONS_GHC -fmax-pmcheck-iterations=10000000 #-}
8
9 module OptCoercion ( optCoercion, checkAxInstCo ) where
10
11 #include "HsVersions.h"
12
13 import DynFlags
14 import TyCoRep
15 import Coercion
16 import Type hiding( substTyVarBndr, substTy )
17 import TcType ( exactTyCoVarsOfType )
18 import TyCon
19 import CoAxiom
20 import VarSet
21 import VarEnv
22 import Outputable
23 import FamInstEnv ( flattenTys )
24 import Pair
25 import ListSetOps ( getNth )
26 import Util
27 import Unify
28 import InstEnv
29 import Control.Monad ( zipWithM )
30
31 {-
32 %************************************************************************
33 %* *
34 Optimising coercions
35 %* *
36 %************************************************************************
37
38 Note [Optimising coercion optimisation]
39 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
40 Looking up a coercion's role or kind is linear in the size of the
41 coercion. Thus, doing this repeatedly during the recursive descent
42 of coercion optimisation is disastrous. We must be careful to avoid
43 doing this if at all possible.
44
45 Because it is generally easy to know a coercion's components' roles
46 from the role of the outer coercion, we pass down the known role of
47 the input in the algorithm below. We also keep functions opt_co2
48 and opt_co3 separate from opt_co4, so that the former two do Phantom
49 checks that opt_co4 can avoid. This is a big win because Phantom coercions
50 rarely appear within non-phantom coercions -- only in some TyConAppCos
51 and some AxiomInstCos. We handle these cases specially by calling
52 opt_co2.
53
54 Note [Optimising InstCo]
55 ~~~~~~~~~~~~~~~~~~~~~~~~
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 `mkCoherenceRightCo` 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 -}
83
84 optCoercion :: TCvSubst -> Coercion -> NormalCo
85 -- ^ optCoercion applies a substitution to a coercion,
86 -- *and* optimises it to reduce its size
87 optCoercion env co
88 | hasNoOptCoercion unsafeGlobalDynFlags = substCo env co
89 | debugIsOn
90 = let out_co = opt_co1 lc False co
91 (Pair in_ty1 in_ty2, in_role) = coercionKindRole co
92 (Pair out_ty1 out_ty2, out_role) = coercionKindRole out_co
93 in
94 ASSERT2( substTyUnchecked env in_ty1 `eqType` out_ty1 &&
95 substTyUnchecked env in_ty2 `eqType` out_ty2 &&
96 in_role == out_role
97 , text "optCoercion changed types!"
98 $$ hang (text "in_co:") 2 (ppr co)
99 $$ hang (text "in_ty1:") 2 (ppr in_ty1)
100 $$ hang (text "in_ty2:") 2 (ppr in_ty2)
101 $$ hang (text "out_co:") 2 (ppr out_co)
102 $$ hang (text "out_ty1:") 2 (ppr out_ty1)
103 $$ hang (text "out_ty2:") 2 (ppr out_ty2)
104 $$ hang (text "subst:") 2 (ppr env) )
105 out_co
106
107 | otherwise = opt_co1 lc False co
108 where
109 lc = mkSubstLiftingContext env
110
111 type NormalCo = Coercion
112 -- Invariants:
113 -- * The substitution has been fully applied
114 -- * For trans coercions (co1 `trans` co2)
115 -- co1 is not a trans, and neither co1 nor co2 is identity
116
117 type NormalNonIdCo = NormalCo -- Extra invariant: not the identity
118
119 -- | Do we apply a @sym@ to the result?
120 type SymFlag = Bool
121
122 -- | Do we force the result to be representational?
123 type ReprFlag = Bool
124
125 -- | Optimize a coercion, making no assumptions. All coercions in
126 -- the lifting context are already optimized (and sym'd if nec'y)
127 opt_co1 :: LiftingContext
128 -> SymFlag
129 -> Coercion -> NormalCo
130 opt_co1 env sym co = opt_co2 env sym (coercionRole co) co
131
132 -- See Note [Optimising coercion optimisation]
133 -- | Optimize a coercion, knowing the coercion's role. No other assumptions.
134 opt_co2 :: LiftingContext
135 -> SymFlag
136 -> Role -- ^ The role of the input coercion
137 -> Coercion -> NormalCo
138 opt_co2 env sym Phantom co = opt_phantom env sym co
139 opt_co2 env sym r co = opt_co3 env sym Nothing r co
140
141 -- See Note [Optimising coercion optimisation]
142 -- | Optimize a coercion, knowing the coercion's non-Phantom role.
143 opt_co3 :: LiftingContext -> SymFlag -> Maybe Role -> Role -> Coercion -> NormalCo
144 opt_co3 env sym (Just Phantom) _ co = opt_phantom env sym co
145 opt_co3 env sym (Just Representational) r co = opt_co4_wrap env sym True r co
146 -- if mrole is Just Nominal, that can't be a downgrade, so we can ignore
147 opt_co3 env sym _ r co = opt_co4_wrap env sym False r co
148
149 -- See Note [Optimising coercion optimisation]
150 -- | Optimize a non-phantom coercion.
151 opt_co4, opt_co4_wrap :: LiftingContext -> SymFlag -> ReprFlag -> Role -> Coercion -> NormalCo
152
153 opt_co4_wrap = opt_co4
154 {-
155 opt_co4_wrap env sym rep r co
156 = pprTrace "opt_co4_wrap {"
157 ( vcat [ text "Sym:" <+> ppr sym
158 , text "Rep:" <+> ppr rep
159 , text "Role:" <+> ppr r
160 , text "Co:" <+> ppr co ]) $
161 ASSERT( r == coercionRole co )
162 let result = opt_co4 env sym rep r co in
163 pprTrace "opt_co4_wrap }" (ppr co $$ text "---" $$ ppr result) $
164 result
165 -}
166
167 opt_co4 env _ rep r (Refl _r ty)
168 = ASSERT2( r == _r, text "Expected role:" <+> ppr r $$
169 text "Found role:" <+> ppr _r $$
170 text "Type:" <+> ppr ty )
171 liftCoSubst (chooseRole rep r) env ty
172
173 opt_co4 env sym rep r (SymCo co) = opt_co4_wrap env (not sym) rep r co
174 -- surprisingly, we don't have to do anything to the env here. This is
175 -- because any "lifting" substitutions in the env are tied to ForAllCos,
176 -- which treat their left and right sides differently. We don't want to
177 -- exchange them.
178
179 opt_co4 env sym rep r g@(TyConAppCo _r tc cos)
180 = ASSERT( r == _r )
181 case (rep, r) of
182 (True, Nominal) ->
183 mkTyConAppCo Representational tc
184 (zipWith3 (opt_co3 env sym)
185 (map Just (tyConRolesRepresentational tc))
186 (repeat Nominal)
187 cos)
188 (False, Nominal) ->
189 mkTyConAppCo Nominal tc (map (opt_co4_wrap env sym False Nominal) cos)
190 (_, Representational) ->
191 -- must use opt_co2 here, because some roles may be P
192 -- See Note [Optimising coercion optimisation]
193 mkTyConAppCo r tc (zipWith (opt_co2 env sym)
194 (tyConRolesRepresentational tc) -- the current roles
195 cos)
196 (_, Phantom) -> pprPanic "opt_co4 sees a phantom!" (ppr g)
197
198 opt_co4 env sym rep r (AppCo co1 co2)
199 = mkAppCo (opt_co4_wrap env sym rep r co1)
200 (opt_co4_wrap env sym False Nominal co2)
201
202 opt_co4 env sym rep r (ForAllCo tv k_co co)
203 = case optForAllCoBndr env sym tv k_co of
204 (env', tv', k_co') -> mkForAllCo tv' k_co' $
205 opt_co4_wrap env' sym rep r co
206 -- Use the "mk" functions to check for nested Refls
207
208 opt_co4 env sym rep r (FunCo _r co1 co2)
209 = ASSERT( r == _r )
210 if rep
211 then mkFunCo Representational co1' co2'
212 else mkFunCo r co1' co2'
213 where
214 co1' = opt_co4_wrap env sym rep r co1
215 co2' = opt_co4_wrap env sym rep r co2
216
217 opt_co4 env sym rep r (CoVarCo cv)
218 | Just co <- lookupCoVar (lcTCvSubst env) cv
219 = opt_co4_wrap (zapLiftingContext env) sym rep r co
220
221 | ty1 `eqType` ty2 -- See Note [Optimise CoVarCo to Refl]
222 = Refl (chooseRole rep r) ty1
223
224 | otherwise
225 = ASSERT( isCoVar cv1 )
226 wrapRole rep r $ wrapSym sym $
227 CoVarCo cv1
228
229 where
230 Pair ty1 ty2 = coVarTypes cv1
231
232 cv1 = case lookupInScope (lcInScopeSet env) cv of
233 Just cv1 -> cv1
234 Nothing -> WARN( True, text "opt_co: not in scope:"
235 <+> ppr cv $$ ppr env)
236 cv
237 -- cv1 might have a substituted kind!
238
239
240 opt_co4 env sym rep r (AxiomInstCo con ind cos)
241 -- Do *not* push sym inside top-level axioms
242 -- e.g. if g is a top-level axiom
243 -- g a : f a ~ a
244 -- then (sym (g ty)) /= g (sym ty) !!
245 = ASSERT( r == coAxiomRole con )
246 wrapRole rep (coAxiomRole con) $
247 wrapSym sym $
248 -- some sub-cos might be P: use opt_co2
249 -- See Note [Optimising coercion optimisation]
250 AxiomInstCo con ind (zipWith (opt_co2 env False)
251 (coAxBranchRoles (coAxiomNthBranch con ind))
252 cos)
253 -- Note that the_co does *not* have sym pushed into it
254
255 opt_co4 env sym rep r (UnivCo prov _r t1 t2)
256 = ASSERT( r == _r )
257 opt_univ env sym prov (chooseRole rep r) t1 t2
258
259 opt_co4 env sym rep r (TransCo co1 co2)
260 -- sym (g `o` h) = sym h `o` sym g
261 | sym = opt_trans in_scope co2' co1'
262 | otherwise = opt_trans in_scope co1' co2'
263 where
264 co1' = opt_co4_wrap env sym rep r co1
265 co2' = opt_co4_wrap env sym rep r co2
266 in_scope = lcInScopeSet env
267
268
269 opt_co4 env sym rep r co@(NthCo {}) = opt_nth_co env sym rep r co
270
271 opt_co4 env sym rep r (LRCo lr co)
272 | Just pr_co <- splitAppCo_maybe co
273 = ASSERT( r == Nominal )
274 opt_co4_wrap env sym rep Nominal (pick_lr lr pr_co)
275 | Just pr_co <- splitAppCo_maybe co'
276 = ASSERT( r == Nominal )
277 if rep
278 then opt_co4_wrap (zapLiftingContext env) False True Nominal (pick_lr lr pr_co)
279 else pick_lr lr pr_co
280 | otherwise
281 = wrapRole rep Nominal $ LRCo lr co'
282 where
283 co' = opt_co4_wrap env sym False Nominal co
284
285 pick_lr CLeft (l, _) = l
286 pick_lr CRight (_, r) = r
287
288 -- See Note [Optimising InstCo]
289 opt_co4 env sym rep r (InstCo co1 arg)
290 -- forall over type...
291 | Just (tv, kind_co, co_body) <- splitForAllCo_maybe co1
292 = opt_co4_wrap (extendLiftingContext env tv
293 (arg' `mkCoherenceRightCo` mkSymCo kind_co))
294 sym rep r co_body
295
296 -- See if it is a forall after optimization
297 -- If so, do an inefficient one-variable substitution, then re-optimize
298
299 -- forall over type...
300 | Just (tv', kind_co', co_body') <- splitForAllCo_maybe co1'
301 = opt_co4_wrap (extendLiftingContext (zapLiftingContext env) tv'
302 (arg' `mkCoherenceRightCo` mkSymCo kind_co'))
303 False False r' co_body'
304
305 | otherwise = InstCo co1' arg'
306 where
307 co1' = opt_co4_wrap env sym rep r co1
308 r' = chooseRole rep r
309 arg' = opt_co4_wrap env sym False Nominal arg
310
311 opt_co4 env sym rep r (CoherenceCo co1 co2)
312 | TransCo col1 cor1 <- co1
313 = opt_co4_wrap env sym rep r (mkTransCo (mkCoherenceCo col1 co2) cor1)
314
315 | TransCo col1' cor1' <- co1'
316 = if sym then opt_trans in_scope col1'
317 (optCoercion (zapTCvSubst (lcTCvSubst env))
318 (mkCoherenceRightCo cor1' co2'))
319 else opt_trans in_scope (mkCoherenceCo col1' co2') cor1'
320
321 | otherwise
322 = wrapSym sym $ mkCoherenceCo (opt_co4_wrap env False rep r co1) co2'
323 where co1' = opt_co4_wrap env sym rep r co1
324 co2' = opt_co4_wrap env False False Nominal co2
325 in_scope = lcInScopeSet env
326
327 opt_co4 env sym _rep r (KindCo co)
328 = ASSERT( r == Nominal )
329 let kco' = promoteCoercion co in
330 case kco' of
331 KindCo co' -> promoteCoercion (opt_co1 env sym co')
332 _ -> opt_co4_wrap env sym False Nominal kco'
333 -- This might be able to be optimized more to do the promotion
334 -- and substitution/optimization at the same time
335
336 opt_co4 env sym _ r (SubCo co)
337 = ASSERT( r == Representational )
338 opt_co4_wrap env sym True Nominal co
339
340 -- This could perhaps be optimized more.
341 opt_co4 env sym rep r (AxiomRuleCo co cs)
342 = ASSERT( r == coaxrRole co )
343 wrapRole rep r $
344 wrapSym sym $
345 AxiomRuleCo co (zipWith (opt_co2 env False) (coaxrAsmpRoles co) cs)
346
347 {- Note [Optimise CoVarCo to Refl]
348 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
349 If we have (c :: t~t) we can optimise it to Refl. That increases the
350 chances of floating the Refl upwards; e.g. Maybe c --> Refl (Maybe t)
351
352 We do so here in optCoercion, not in mkCoVarCo; see Note [mkCoVarCo]
353 in Coercion.
354 -}
355
356 -------------
357 -- | Optimize a phantom coercion. The input coercion may not necessarily
358 -- be a phantom, but the output sure will be.
359 opt_phantom :: LiftingContext -> SymFlag -> Coercion -> NormalCo
360 opt_phantom env sym co
361 = opt_univ env sym (PhantomProv (mkKindCo co)) Phantom ty1 ty2
362 where
363 Pair ty1 ty2 = coercionKind co
364
365 {- Note [Differing kinds]
366 ~~~~~~~~~~~~~~~~~~~~~~
367 The two types may not have the same kind (although that would be very unusual).
368 But even if they have the same kind, and the same type constructor, the number
369 of arguments in a `CoTyConApp` can differ. Consider
370
371 Any :: forall k. k
372
373 Any * Int :: *
374 Any (*->*) Maybe Int :: *
375
376 Hence the need to compare argument lengths; see Trac #13658
377 -}
378
379 opt_univ :: LiftingContext -> SymFlag -> UnivCoProvenance -> Role
380 -> Type -> Type -> Coercion
381 opt_univ env sym (PhantomProv h) _r ty1 ty2
382 | sym = mkPhantomCo h' ty2' ty1'
383 | otherwise = mkPhantomCo h' ty1' ty2'
384 where
385 h' = opt_co4 env sym False Nominal h
386 ty1' = substTy (lcSubstLeft env) ty1
387 ty2' = substTy (lcSubstRight env) ty2
388
389 opt_univ env sym prov role oty1 oty2
390 | Just (tc1, tys1) <- splitTyConApp_maybe oty1
391 , Just (tc2, tys2) <- splitTyConApp_maybe oty2
392 , tc1 == tc2
393 , equalLength tys1 tys2 -- see Note [Differing kinds]
394 -- NB: prov must not be the two interesting ones (ProofIrrel & Phantom);
395 -- Phantom is already taken care of, and ProofIrrel doesn't relate tyconapps
396 = let roles = tyConRolesX role tc1
397 arg_cos = zipWith3 (mkUnivCo prov) roles tys1 tys2
398 arg_cos' = zipWith (opt_co4 env sym False) roles arg_cos
399 in
400 mkTyConAppCo role tc1 arg_cos'
401
402 -- can't optimize the AppTy case because we can't build the kind coercions.
403
404 | Just (tv1, ty1) <- splitForAllTy_maybe oty1
405 , Just (tv2, ty2) <- splitForAllTy_maybe oty2
406 -- NB: prov isn't interesting here either
407 = let k1 = tyVarKind tv1
408 k2 = tyVarKind tv2
409 eta = mkUnivCo prov Nominal k1 k2
410 -- eta gets opt'ed soon, but not yet.
411 ty2' = substTyWith [tv2] [TyVarTy tv1 `mkCastTy` eta] ty2
412
413 (env', tv1', eta') = optForAllCoBndr env sym tv1 eta
414 in
415 mkForAllCo tv1' eta' (opt_univ env' sym prov role ty1 ty2')
416
417 | otherwise
418 = let ty1 = substTyUnchecked (lcSubstLeft env) oty1
419 ty2 = substTyUnchecked (lcSubstRight env) oty2
420 (a, b) | sym = (ty2, ty1)
421 | otherwise = (ty1, ty2)
422 in
423 mkUnivCo prov' role a b
424
425 where
426 prov' = case prov of
427 UnsafeCoerceProv -> prov
428 PhantomProv kco -> PhantomProv $ opt_co4_wrap env sym False Nominal kco
429 ProofIrrelProv kco -> ProofIrrelProv $ opt_co4_wrap env sym False Nominal kco
430 PluginProv _ -> prov
431 HoleProv h -> pprPanic "opt_univ fell into a hole" (ppr h)
432
433
434 -------------
435 -- NthCo must be handled separately, because it's the one case where we can't
436 -- tell quickly what the component coercion's role is from the containing
437 -- coercion. To avoid repeated coercionRole calls as opt_co1 calls opt_co2,
438 -- we just look for nested NthCo's, which can happen in practice.
439 opt_nth_co :: LiftingContext -> SymFlag -> ReprFlag -> Role -> Coercion -> NormalCo
440 opt_nth_co env sym rep r = go []
441 where
442 go ns (NthCo n co) = go (n:ns) co
443 -- previous versions checked if the tycon is decomposable. This
444 -- is redundant, because a non-decomposable tycon under an NthCo
445 -- is entirely bogus. See docs/core-spec/core-spec.pdf.
446 go ns co
447 = opt_nths ns co
448
449 -- try to resolve 1 Nth
450 push_nth n (Refl r1 ty)
451 | Just (tc, args) <- splitTyConApp_maybe ty
452 = Just (Refl (nthRole r1 tc n) (args `getNth` n))
453 | n == 0
454 , Just (tv, _) <- splitForAllTy_maybe ty
455 = Just (Refl Nominal (tyVarKind tv))
456 push_nth n (TyConAppCo _ _ cos)
457 = Just (cos `getNth` n)
458 push_nth 0 (ForAllCo _ eta _)
459 = Just eta
460 push_nth _ _ = Nothing
461
462 -- input coercion is *not* yet sym'd or opt'd
463 opt_nths [] co = opt_co4_wrap env sym rep r co
464 opt_nths (n:ns) co
465 | Just co' <- push_nth n co
466 = opt_nths ns co'
467
468 -- here, the co isn't a TyConAppCo, so we opt it, hoping to get
469 -- a TyConAppCo as output. We don't know the role, so we use
470 -- opt_co1. This is slightly annoying, because opt_co1 will call
471 -- coercionRole, but as long as we don't have a long chain of
472 -- NthCo's interspersed with some other coercion former, we should
473 -- be OK.
474 opt_nths ns co = opt_nths' ns (opt_co1 env sym co)
475
476 -- input coercion *is* sym'd and opt'd
477 opt_nths' [] co
478 = if rep && (r == Nominal)
479 -- propagate the SubCo:
480 then opt_co4_wrap (zapLiftingContext env) False True r co
481 else co
482 opt_nths' (n:ns) co
483 | Just co' <- push_nth n co
484 = opt_nths' ns co'
485 opt_nths' ns co = wrapRole rep r (mk_nths ns co)
486
487 mk_nths [] co = co
488 mk_nths (n:ns) co = mk_nths ns (mkNthCo n co)
489
490 -------------
491 opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
492 opt_transList is = zipWith (opt_trans is)
493
494 opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
495 opt_trans is co1 co2
496 | isReflCo co1 = co2
497 | otherwise = opt_trans1 is co1 co2
498
499 opt_trans1 :: InScopeSet -> NormalNonIdCo -> NormalCo -> NormalCo
500 -- First arg is not the identity
501 opt_trans1 is co1 co2
502 | isReflCo co2 = co1
503 | otherwise = opt_trans2 is co1 co2
504
505 opt_trans2 :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> NormalCo
506 -- Neither arg is the identity
507 opt_trans2 is (TransCo co1a co1b) co2
508 -- Don't know whether the sub-coercions are the identity
509 = opt_trans is co1a (opt_trans is co1b co2)
510
511 opt_trans2 is co1 co2
512 | Just co <- opt_trans_rule is co1 co2
513 = co
514
515 opt_trans2 is co1 (TransCo co2a co2b)
516 | Just co1_2a <- opt_trans_rule is co1 co2a
517 = if isReflCo co1_2a
518 then co2b
519 else opt_trans1 is co1_2a co2b
520
521 opt_trans2 _ co1 co2
522 = mkTransCo co1 co2
523
524 ------
525 -- Optimize coercions with a top-level use of transitivity.
526 opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
527
528 -- Push transitivity through matching destructors
529 opt_trans_rule is in_co1@(NthCo d1 co1) in_co2@(NthCo d2 co2)
530 | d1 == d2
531 , co1 `compatible_co` co2
532 = fireTransRule "PushNth" in_co1 in_co2 $
533 mkNthCo d1 (opt_trans is co1 co2)
534
535 opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2)
536 | d1 == d2
537 , co1 `compatible_co` co2
538 = fireTransRule "PushLR" in_co1 in_co2 $
539 mkLRCo d1 (opt_trans is co1 co2)
540
541 -- Push transitivity inside instantiation
542 opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
543 | ty1 `eqCoercion` ty2
544 , co1 `compatible_co` co2
545 = fireTransRule "TrPushInst" in_co1 in_co2 $
546 mkInstCo (opt_trans is co1 co2) ty1
547
548 opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1)
549 in_co2@(UnivCo p2 r2 _tyl2 tyr2)
550 | Just prov' <- opt_trans_prov p1 p2
551 = ASSERT( r1 == r2 )
552 fireTransRule "UnivCo" in_co1 in_co2 $
553 mkUnivCo prov' r1 tyl1 tyr2
554 where
555 -- if the provenances are different, opt'ing will be very confusing
556 opt_trans_prov UnsafeCoerceProv UnsafeCoerceProv = Just UnsafeCoerceProv
557 opt_trans_prov (PhantomProv kco1) (PhantomProv kco2)
558 = Just $ PhantomProv $ opt_trans is kco1 kco2
559 opt_trans_prov (ProofIrrelProv kco1) (ProofIrrelProv kco2)
560 = Just $ ProofIrrelProv $ opt_trans is kco1 kco2
561 opt_trans_prov (PluginProv str1) (PluginProv str2) | str1 == str2 = Just p1
562 opt_trans_prov _ _ = Nothing
563
564 -- Push transitivity down through matching top-level constructors.
565 opt_trans_rule is in_co1@(TyConAppCo r1 tc1 cos1) in_co2@(TyConAppCo r2 tc2 cos2)
566 | tc1 == tc2
567 = ASSERT( r1 == r2 )
568 fireTransRule "PushTyConApp" in_co1 in_co2 $
569 mkTyConAppCo r1 tc1 (opt_transList is cos1 cos2)
570
571 opt_trans_rule is in_co1@(FunCo r1 co1a co1b) in_co2@(FunCo r2 co2a co2b)
572 = ASSERT( r1 == r2 ) -- Just like the TyConAppCo/TyConAppCo case
573 fireTransRule "PushFun" in_co1 in_co2 $
574 mkFunCo r1 (opt_trans is co1a co2a) (opt_trans is co1b co2b)
575
576 opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
577 = fireTransRule "TrPushApp" in_co1 in_co2 $
578 mkAppCo (opt_trans is co1a co2a)
579 (opt_trans is co1b co2b)
580
581 -- Eta rules
582 opt_trans_rule is co1@(TyConAppCo r tc cos1) co2
583 | Just cos2 <- etaTyConAppCo_maybe tc co2
584 = ASSERT( cos1 `equalLength` cos2 )
585 fireTransRule "EtaCompL" co1 co2 $
586 mkTyConAppCo r tc (opt_transList is cos1 cos2)
587
588 opt_trans_rule is co1 co2@(TyConAppCo r tc cos2)
589 | Just cos1 <- etaTyConAppCo_maybe tc co1
590 = ASSERT( cos1 `equalLength` cos2 )
591 fireTransRule "EtaCompR" co1 co2 $
592 mkTyConAppCo r tc (opt_transList is cos1 cos2)
593
594 opt_trans_rule is co1@(AppCo co1a co1b) co2
595 | Just (co2a,co2b) <- etaAppCo_maybe co2
596 = fireTransRule "EtaAppL" co1 co2 $
597 mkAppCo (opt_trans is co1a co2a)
598 (opt_trans is co1b co2b)
599
600 opt_trans_rule is co1 co2@(AppCo co2a co2b)
601 | Just (co1a,co1b) <- etaAppCo_maybe co1
602 = fireTransRule "EtaAppR" co1 co2 $
603 mkAppCo (opt_trans is co1a co2a)
604 (opt_trans is co1b co2b)
605
606 -- Push transitivity inside forall
607 opt_trans_rule is co1 co2
608 | ForAllCo tv1 eta1 r1 <- co1
609 , Just (tv2,eta2,r2) <- etaForAllCo_maybe co2
610 = push_trans tv1 eta1 r1 tv2 eta2 r2
611
612 | ForAllCo tv2 eta2 r2 <- co2
613 , Just (tv1,eta1,r1) <- etaForAllCo_maybe co1
614 = push_trans tv1 eta1 r1 tv2 eta2 r2
615
616 where
617 push_trans tv1 eta1 r1 tv2 eta2 r2
618 = fireTransRule "EtaAllTy" co1 co2 $
619 mkForAllCo tv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2')
620 where
621 is' = is `extendInScopeSet` tv1
622 r2' = substCoWithUnchecked [tv2] [TyVarTy tv1] r2
623
624 -- Push transitivity inside axioms
625 opt_trans_rule is co1 co2
626
627 -- See Note [Why call checkAxInstCo during optimisation]
628 -- TrPushSymAxR
629 | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
630 , True <- sym
631 , Just cos2 <- matchAxiom sym con ind co2
632 , let newAxInst = AxiomInstCo con ind (opt_transList is (map mkSymCo cos2) cos1)
633 , Nothing <- checkAxInstCo newAxInst
634 = fireTransRule "TrPushSymAxR" co1 co2 $ SymCo newAxInst
635
636 -- TrPushAxR
637 | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
638 , False <- sym
639 , Just cos2 <- matchAxiom sym con ind co2
640 , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
641 , Nothing <- checkAxInstCo newAxInst
642 = fireTransRule "TrPushAxR" co1 co2 newAxInst
643
644 -- TrPushSymAxL
645 | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
646 , True <- sym
647 , Just cos1 <- matchAxiom (not sym) con ind co1
648 , let newAxInst = AxiomInstCo con ind (opt_transList is cos2 (map mkSymCo cos1))
649 , Nothing <- checkAxInstCo newAxInst
650 = fireTransRule "TrPushSymAxL" co1 co2 $ SymCo newAxInst
651
652 -- TrPushAxL
653 | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
654 , False <- sym
655 , Just cos1 <- matchAxiom (not sym) con ind co1
656 , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
657 , Nothing <- checkAxInstCo newAxInst
658 = fireTransRule "TrPushAxL" co1 co2 newAxInst
659
660 -- TrPushAxSym/TrPushSymAx
661 | Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe
662 , Just (sym2, con2, ind2, cos2) <- co2_is_axiom_maybe
663 , con1 == con2
664 , ind1 == ind2
665 , sym1 == not sym2
666 , let branch = coAxiomNthBranch con1 ind1
667 qtvs = coAxBranchTyVars branch ++ coAxBranchCoVars branch
668 lhs = coAxNthLHS con1 ind1
669 rhs = coAxBranchRHS branch
670 pivot_tvs = exactTyCoVarsOfType (if sym2 then rhs else lhs)
671 , all (`elemVarSet` pivot_tvs) qtvs
672 = fireTransRule "TrPushAxSym" co1 co2 $
673 if sym2
674 -- TrPushAxSym
675 then liftCoSubstWith role qtvs (opt_transList is cos1 (map mkSymCo cos2)) lhs
676 -- TrPushSymAx
677 else liftCoSubstWith role qtvs (opt_transList is (map mkSymCo cos1) cos2) rhs
678 where
679 co1_is_axiom_maybe = isAxiom_maybe co1
680 co2_is_axiom_maybe = isAxiom_maybe co2
681 role = coercionRole co1 -- should be the same as coercionRole co2!
682
683 opt_trans_rule is co1 co2
684 | Just (lco, lh) <- isCohRight_maybe co1
685 , Just (rco, rh) <- isCohLeft_maybe co2
686 , (coercionType lh) `eqType` (coercionType rh)
687 = opt_trans_rule is lco rco
688
689 opt_trans_rule _ co1 co2 -- Identity rule
690 | (Pair ty1 _, r) <- coercionKindRole co1
691 , Pair _ ty2 <- coercionKind co2
692 , ty1 `eqType` ty2
693 = fireTransRule "RedTypeDirRefl" co1 co2 $
694 Refl r ty2
695
696 opt_trans_rule _ _ _ = Nothing
697
698 fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
699 fireTransRule _rule _co1 _co2 res
700 = -- pprTrace ("Trans rule fired: " ++ _rule) (vcat [ppr _co1, ppr _co2, ppr res]) $
701 Just res
702
703 {-
704 Note [Conflict checking with AxiomInstCo]
705 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
706 Consider the following type family and axiom:
707
708 type family Equal (a :: k) (b :: k) :: Bool
709 type instance where
710 Equal a a = True
711 Equal a b = False
712 --
713 Equal :: forall k::*. k -> k -> Bool
714 axEqual :: { forall k::*. forall a::k. Equal k a a ~ True
715 ; forall k::*. forall a::k. forall b::k. Equal k a b ~ False }
716
717 We wish to disallow (axEqual[1] <*> <Int> <Int). (Recall that the index is
718 0-based, so this is the second branch of the axiom.) The problem is that, on
719 the surface, it seems that (axEqual[1] <*> <Int> <Int>) :: (Equal * Int Int ~
720 False) and that all is OK. But, all is not OK: we want to use the first branch
721 of the axiom in this case, not the second. The problem is that the parameters
722 of the first branch can unify with the supplied coercions, thus meaning that
723 the first branch should be taken. See also Note [Apartness] in
724 types/FamInstEnv.hs.
725
726 Note [Why call checkAxInstCo during optimisation]
727 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
728 It is possible that otherwise-good-looking optimisations meet with disaster
729 in the presence of axioms with multiple equations. Consider
730
731 type family Equal (a :: *) (b :: *) :: Bool where
732 Equal a a = True
733 Equal a b = False
734 type family Id (a :: *) :: * where
735 Id a = a
736
737 axEq :: { [a::*]. Equal a a ~ True
738 ; [a::*, b::*]. Equal a b ~ False }
739 axId :: [a::*]. Id a ~ a
740
741 co1 = Equal (axId[0] Int) (axId[0] Bool)
742 :: Equal (Id Int) (Id Bool) ~ Equal Int Bool
743 co2 = axEq[1] <Int> <Bool>
744 :: Equal Int Bool ~ False
745
746 We wish to optimise (co1 ; co2). We end up in rule TrPushAxL, noting that
747 co2 is an axiom and that matchAxiom succeeds when looking at co1. But, what
748 happens when we push the coercions inside? We get
749
750 co3 = axEq[1] (axId[0] Int) (axId[0] Bool)
751 :: Equal (Id Int) (Id Bool) ~ False
752
753 which is bogus! This is because the type system isn't smart enough to know
754 that (Id Int) and (Id Bool) are Surely Apart, as they're headed by type
755 families. At the time of writing, I (Richard Eisenberg) couldn't think of
756 a way of detecting this any more efficient than just building the optimised
757 coercion and checking.
758 -}
759
760 -- | Check to make sure that an AxInstCo is internally consistent.
761 -- Returns the conflicting branch, if it exists
762 -- See Note [Conflict checking with AxiomInstCo]
763 checkAxInstCo :: Coercion -> Maybe CoAxBranch
764 -- defined here to avoid dependencies in Coercion
765 -- If you edit this function, you may need to update the GHC formalism
766 -- See Note [GHC Formalism] in CoreLint
767 checkAxInstCo (AxiomInstCo ax ind cos)
768 = let branch = coAxiomNthBranch ax ind
769 tvs = coAxBranchTyVars branch
770 cvs = coAxBranchCoVars branch
771 incomps = coAxBranchIncomps branch
772 (tys, cotys) = splitAtList tvs (map (pFst . coercionKind) cos)
773 co_args = map stripCoercionTy cotys
774 subst = zipTvSubst tvs tys `composeTCvSubst`
775 zipCvSubst cvs co_args
776 target = Type.substTys subst (coAxBranchLHS branch)
777 in_scope = mkInScopeSet $
778 unionVarSets (map (tyCoVarsOfTypes . coAxBranchLHS) incomps)
779 flattened_target = flattenTys in_scope target in
780 check_no_conflict flattened_target incomps
781 where
782 check_no_conflict :: [Type] -> [CoAxBranch] -> Maybe CoAxBranch
783 check_no_conflict _ [] = Nothing
784 check_no_conflict flat (b@CoAxBranch { cab_lhs = lhs_incomp } : rest)
785 -- See Note [Apartness] in FamInstEnv
786 | SurelyApart <- tcUnifyTysFG instanceBindFun flat lhs_incomp
787 = check_no_conflict flat rest
788 | otherwise
789 = Just b
790 checkAxInstCo _ = Nothing
791
792
793 -----------
794 wrapSym :: SymFlag -> Coercion -> Coercion
795 wrapSym sym co | sym = mkSymCo co
796 | otherwise = co
797
798 -- | Conditionally set a role to be representational
799 wrapRole :: ReprFlag
800 -> Role -- ^ current role
801 -> Coercion -> Coercion
802 wrapRole False _ = id
803 wrapRole True current = downgradeRole Representational current
804
805 -- | If we require a representational role, return that. Otherwise,
806 -- return the "default" role provided.
807 chooseRole :: ReprFlag
808 -> Role -- ^ "default" role
809 -> Role
810 chooseRole True _ = Representational
811 chooseRole _ r = r
812
813 -----------
814 isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom Branched, Int, [Coercion])
815 isAxiom_maybe (SymCo co)
816 | Just (sym, con, ind, cos) <- isAxiom_maybe co
817 = Just (not sym, con, ind, cos)
818 isAxiom_maybe (AxiomInstCo con ind cos)
819 = Just (False, con, ind, cos)
820 isAxiom_maybe _ = Nothing
821
822 matchAxiom :: Bool -- True = match LHS, False = match RHS
823 -> CoAxiom br -> Int -> Coercion -> Maybe [Coercion]
824 matchAxiom sym ax@(CoAxiom { co_ax_tc = tc }) ind co
825 | CoAxBranch { cab_tvs = qtvs
826 , cab_cvs = [] -- can't infer these, so fail if there are any
827 , cab_roles = roles
828 , cab_lhs = lhs
829 , cab_rhs = rhs } <- coAxiomNthBranch ax ind
830 , Just subst <- liftCoMatch (mkVarSet qtvs)
831 (if sym then (mkTyConApp tc lhs) else rhs)
832 co
833 , all (`isMappedByLC` subst) qtvs
834 = zipWithM (liftCoSubstTyVar subst) roles qtvs
835
836 | otherwise
837 = Nothing
838
839 -------------
840 -- destruct a CoherenceCo
841 isCohLeft_maybe :: Coercion -> Maybe (Coercion, Coercion)
842 isCohLeft_maybe (CoherenceCo co1 co2) = Just (co1, co2)
843 isCohLeft_maybe _ = Nothing
844
845 -- destruct a (sym (co1 |> co2)).
846 -- if isCohRight_maybe co = Just (co1, co2), then (sym co1) `mkCohRightCo` co2 = co
847 isCohRight_maybe :: Coercion -> Maybe (Coercion, Coercion)
848 isCohRight_maybe (SymCo (CoherenceCo co1 co2)) = Just (mkSymCo co1, co2)
849 isCohRight_maybe _ = Nothing
850
851 -------------
852 compatible_co :: Coercion -> Coercion -> Bool
853 -- Check whether (co1 . co2) will be well-kinded
854 compatible_co co1 co2
855 = x1 `eqType` x2
856 where
857 Pair _ x1 = coercionKind co1
858 Pair x2 _ = coercionKind co2
859
860 -------------
861 {-
862 etaForAllCo_maybe
863 ~~~~~~~~~~~~~~~~~
864 Suppose we have
865
866 g : all a1:k1.t1 ~ all a2:k2.t2
867
868 but g is *not* a ForAllCo. We want to eta-expand it. So, we do this:
869
870 g' = all a1:(ForAllKindCo g).(InstCo g (a1 `mkCoherenceRightCo` ForAllKindCo g))
871
872 Call the kind coercion h1 and the body coercion h2. We can see that
873
874 h2 : t1 ~ t2[a2 |-> (a1 |> h2)]
875
876 According to the typing rule for ForAllCo, we get that
877
878 g' : all a1:k1.t1 ~ all a1:k2.(t2[a2 |-> (a1 |> h2)][a1 |-> a1 |> sym h2])
879
880 or
881
882 g' : all a1:k1.t1 ~ all a1:k2.(t2[a2 |-> a1])
883
884 as desired.
885 -}
886 etaForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
887 -- Try to make the coercion be of form (forall tv:kind_co. co)
888 etaForAllCo_maybe co
889 | ForAllCo tv kind_co r <- co
890 = Just (tv, kind_co, r)
891
892 | Pair ty1 ty2 <- coercionKind co
893 , Just (tv1, _) <- splitForAllTy_maybe ty1
894 , isForAllTy ty2
895 , let kind_co = mkNthCo 0 co
896 = Just ( tv1, kind_co
897 , mkInstCo co (mkNomReflCo (TyVarTy tv1) `mkCoherenceRightCo` kind_co) )
898
899 | otherwise
900 = Nothing
901
902 etaAppCo_maybe :: Coercion -> Maybe (Coercion,Coercion)
903 -- If possible, split a coercion
904 -- g :: t1a t1b ~ t2a t2b
905 -- into a pair of coercions (left g, right g)
906 etaAppCo_maybe co
907 | Just (co1,co2) <- splitAppCo_maybe co
908 = Just (co1,co2)
909 | (Pair ty1 ty2, Nominal) <- coercionKindRole co
910 , Just (_,t1) <- splitAppTy_maybe ty1
911 , Just (_,t2) <- splitAppTy_maybe ty2
912 , let isco1 = isCoercionTy t1
913 , let isco2 = isCoercionTy t2
914 , isco1 == isco2
915 = Just (LRCo CLeft co, LRCo CRight co)
916 | otherwise
917 = Nothing
918
919 etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
920 -- If possible, split a coercion
921 -- g :: T s1 .. sn ~ T t1 .. tn
922 -- into [ Nth 0 g :: s1~t1, ..., Nth (n-1) g :: sn~tn ]
923 etaTyConAppCo_maybe tc (TyConAppCo _ tc2 cos2)
924 = ASSERT( tc == tc2 ) Just cos2
925
926 etaTyConAppCo_maybe tc co
927 | mightBeUnsaturatedTyCon tc
928 , (Pair ty1 ty2, r) <- coercionKindRole co
929 , Just (tc1, tys1) <- splitTyConApp_maybe ty1
930 , Just (tc2, tys2) <- splitTyConApp_maybe ty2
931 , tc1 == tc2
932 , isInjectiveTyCon tc r -- See Note [NthCo and newtypes] in TyCoRep
933 , let n = length tys1
934 = ASSERT( tc == tc1 )
935 ASSERT( tys2 `lengthIs` n )
936 Just (decomposeCo n co)
937 -- NB: n might be <> tyConArity tc
938 -- e.g. data family T a :: * -> *
939 -- g :: T a b ~ T c d
940
941 | otherwise
942 = Nothing
943
944 {-
945 Note [Eta for AppCo]
946 ~~~~~~~~~~~~~~~~~~~~
947 Suppose we have
948 g :: s1 t1 ~ s2 t2
949
950 Then we can't necessarily make
951 left g :: s1 ~ s2
952 right g :: t1 ~ t2
953 because it's possible that
954 s1 :: * -> * t1 :: *
955 s2 :: (*->*) -> * t2 :: * -> *
956 and in that case (left g) does not have the same
957 kind on either side.
958
959 It's enough to check that
960 kind t1 = kind t2
961 because if g is well-kinded then
962 kind (s1 t2) = kind (s2 t2)
963 and these two imply
964 kind s1 = kind s2
965
966 -}
967
968 optForAllCoBndr :: LiftingContext -> Bool
969 -> TyVar -> Coercion -> (LiftingContext, TyVar, Coercion)
970 optForAllCoBndr env sym
971 = substForAllCoBndrCallbackLC sym (opt_co4_wrap env sym False Nominal) env