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